LConvolution

📁 Source: Mathlib/Analysis/LConvolution.lean

Statistics

Metric	Count
Definitions lconvolution, mlconvolution, «term_⋆ₗ[_]_», «term_⋆ₗ_», «term_⋆ₘₗ[_]_», «term_⋆ₘₗ_»	6
Theorems aemeasurable_lconvolution, aemeasurable_mlconvolution, lconvolution_assoc, lconvolution_assoc₀, lconvolution_comm, lconvolution_def, lconvolution_zero, measurable_lconvolution, measurable_mlconvolution, mlconvolution_assoc, mlconvolution_assoc₀, mlconvolution_comm, mlconvolution_def, mlconvolution_zero, zero_lconvolution, zero_mlconvolution	16
Total	22

MeasureTheory

Definitions

Name	Category	Theorems
lconvolution 📖	CompOp	15 math math: measurable_lconvolution, rnDeriv_conv, ProbabilityTheory.IndepFun.pdf_add_eq_lconvolution_pdf', aemeasurable_lconvolution, ProbabilityTheory.IndepFun.pdf_add_eq_lconvolution_pdf, conv_withDensity_eq_lconvolution, lconvolution_def, zero_lconvolution, rnDeriv_conv', conv_eq_withDensity_lconvolution_rnDeriv, lconvolution_comm, lconvolution_assoc₀, lconvolution_zero, conv_withDensity_eq_mlconvolution₀, lconvolution_assoc
mlconvolution 📖	CompOp	15 math math: mlconvolution_assoc₀, mconv_withDensity_eq_mlconvolution, mlconvolution_zero, mconv_eq_withDensity_mlconvolution_rnDeriv, ProbabilityTheory.IndepFun.pdf_mul_eq_mlconvolution_pdf, rnDeriv_mconv, rnDeriv_mconv', ProbabilityTheory.IndepFun.pdf_mul_eq_mlconvolution_pdf', measurable_mlconvolution, mlconvolution_def, mlconvolution_assoc, mconv_withDensity_eq_mlconvolution₀, mlconvolution_comm, aemeasurable_mlconvolution, zero_mlconvolution
«term_⋆ₗ[_]_» 📖	CompOp	—
«term_⋆ₗ_» 📖	CompOp	—
«term_⋆ₘₗ[_]_» 📖	CompOp	—
«term_⋆ₘₗ_» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
aemeasurable_lconvolution 📖	mathematical	AEMeasurable ENNReal ENNReal.measurableSpace	lconvolution AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	AEMeasurable.lintegral_prod_left AEMeasurable.mul ENNReal.instMeasurableMul₂ AEMeasurable.comp_quasiMeasurePreserving QuasiMeasurePreserving.fst Measure.QuasiMeasurePreserving.id quasiMeasurePreserving_neg_add
aemeasurable_mlconvolution 📖	mathematical	AEMeasurable ENNReal ENNReal.measurableSpace	mlconvolution MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	AEMeasurable.lintegral_prod_left AEMeasurable.mul ENNReal.instMeasurableMul₂ AEMeasurable.comp_quasiMeasurePreserving QuasiMeasurePreserving.fst Measure.QuasiMeasurePreserving.id quasiMeasurePreserving_inv_mul
lconvolution_assoc 📖	mathematical	Measurable ENNReal ENNReal.measurableSpace	lconvolution AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	lconvolution_assoc₀ Measurable.aemeasurable
lconvolution_assoc₀ 📖	mathematical	AEMeasurable ENNReal ENNReal.measurableSpace	lconvolution AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	lintegral_const_mul'' AEMeasurable.mul ENNReal.instMeasurableMul₂ AEMeasurable.comp_quasiMeasurePreserving Measure.QuasiMeasurePreserving.comp quasiMeasurePreserving_add_right quasiMeasurePreserving_neg lintegral_add_left_eq_self MeasurableAdd₂.toMeasurableAdd lintegral_mul_const'' lintegral_lintegral_swap neg_add_rev neg_neg add_assoc add_neg_cancel_left QuasiMeasurePreserving.fst Measure.QuasiMeasurePreserving.id quasiMeasurePreserving_neg_add QuasiMeasurePreserving.snd mul_assoc
lconvolution_comm 📖	mathematical	—	lconvolution AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	lintegral_add_left_eq_self MeasurableAdd₂.toMeasurableAdd lintegral_neg_eq_self neg_add_rev neg_neg add_comm add_neg_cancel_comm_assoc mul_comm
lconvolution_def 📖	mathematical	—	lconvolution lintegral ENNReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring	—	—
lconvolution_zero 📖	mathematical	—	lconvolution Pi.instZero ENNReal instZeroENNReal	—	MulZeroClass.mul_zero lintegral_const MulZeroClass.zero_mul
measurable_lconvolution 📖	mathematical	Measurable ENNReal ENNReal.measurableSpace	lconvolution	—	Measurable.lintegral_prod_left Measurable.mul ENNReal.instMeasurableMul₂ Measurable.fun_comp Measurable.fst measurable_id' Measurable.add Measurable.neg Measurable.snd
measurable_mlconvolution 📖	mathematical	Measurable ENNReal ENNReal.measurableSpace	mlconvolution	—	Measurable.lintegral_prod_left Measurable.mul ENNReal.instMeasurableMul₂ Measurable.fun_comp Measurable.fst measurable_id' Measurable.inv Measurable.snd
mlconvolution_assoc 📖	mathematical	Measurable ENNReal ENNReal.measurableSpace	mlconvolution MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	mlconvolution_assoc₀ Measurable.aemeasurable
mlconvolution_assoc₀ 📖	mathematical	AEMeasurable ENNReal ENNReal.measurableSpace	mlconvolution MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	lintegral_const_mul'' AEMeasurable.mul ENNReal.instMeasurableMul₂ AEMeasurable.comp_quasiMeasurePreserving Measure.QuasiMeasurePreserving.comp quasiMeasurePreserving_mul_right quasiMeasurePreserving_inv lintegral_mul_left_eq_self MeasurableMul₂.toMeasurableMul lintegral_mul_const'' lintegral_lintegral_swap mul_inv_rev inv_inv mul_assoc mul_inv_cancel_left QuasiMeasurePreserving.fst Measure.QuasiMeasurePreserving.id quasiMeasurePreserving_inv_mul QuasiMeasurePreserving.snd
mlconvolution_comm 📖	mathematical	—	mlconvolution MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid	—	lintegral_mul_left_eq_self MeasurableMul₂.toMeasurableMul lintegral_inv_eq_self mul_inv_rev inv_inv mul_comm mul_inv_cancel_comm_assoc
mlconvolution_def 📖	mathematical	—	mlconvolution lintegral ENNReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring	—	—
mlconvolution_zero 📖	mathematical	—	mlconvolution Pi.instZero ENNReal instZeroENNReal	—	MulZeroClass.mul_zero lintegral_const MulZeroClass.zero_mul
zero_lconvolution 📖	mathematical	—	lconvolution Pi.instZero ENNReal instZeroENNReal	—	MulZeroClass.zero_mul lintegral_const
zero_mlconvolution 📖	mathematical	—	mlconvolution Pi.instZero ENNReal instZeroENNReal	—	MulZeroClass.zero_mul lintegral_const

---

← Back to Index