Convolution

📁 Source: Mathlib/MeasureTheory/Group/Convolution.lean

Statistics

Metric	Count
Definitions `mconv`, `«term_∗_»`, `«term_∗ₘ_»`	3
Theorems `add_conv`, `add_mconv`, `conv_absolutelyContinuous`, `conv_add`, `conv_assoc`, `conv_comm`, `conv_dirac`, `conv_dirac_zero`, `conv_smul_left`, `conv_zero`, `dirac_conv`, `dirac_conv_dirac`, `dirac_mconv`, `dirac_mconv_dirac`, `dirac_one_mconv`, `dirac_zero_conv`, `finite_of_finite_conv`, `finite_of_finite_mconv`, `lintegral_conv`, `lintegral_conv_eq_lintegral_sum`, `lintegral_mconv`, `lintegral_mconv_eq_lintegral_prod`, `map_conv_addMonoidHom`, `map_conv_continuousLinearMap`, `map_mconv_monoidHom`, `mconv_absolutelyContinuous`, `mconv_add`, `mconv_assoc`, `mconv_comm`, `mconv_dirac`, `mconv_dirac_one`, `mconv_smul_left`, `mconv_zero`, `probabilitymeasure_of_probabilitymeasures_conv`, `probabilitymeasure_of_probabilitymeasures_mconv`, `sfinite_conv_of_sfinite`, `sfinite_mconv_of_sfinite`, `zero_conv`, `zero_mconv`	39
Total	42

MeasureTheory

Definitions

Name	Category	Theorems
`«term_∗_»` 📖	CompOp	—
`«term_∗ₘ_»` 📖	CompOp	—

MeasureTheory.Measure

Definitions

Name	Category	Theorems
`mconv` 📖	CompOp	32 math math: `ProbabilityTheory.IndepFun.map_mul_eq_map_mconv_map₀`, `mconv_assoc`, `sfinite_mconv_of_sfinite`, `map_mconv_monoidHom`, `ProbabilityTheory.IndepFun.hasLaw_mul`, `lintegral_mconv`, `ProbabilityTheory.IndepFun.map_mul_eq_map_mconv_map`, `MeasureTheory.mconv_withDensity_eq_mlconvolution`, `mconv_dirac_one`, `dirac_mconv_dirac`, `MeasureTheory.mconv_eq_withDensity_mlconvolution_rnDeriv`, `finite_of_finite_mconv`, `MeasureTheory.rnDeriv_mconv`, `add_mconv`, `MeasureTheory.rnDeriv_mconv'`, `MeasureTheory.HaveLebesgueDecomposition.mconv`, `ProbabilityTheory.IndepFun.hasLaw_fun_mul`, `dirac_one_mconv`, `mconv_absolutelyContinuous`, `ProbabilityTheory.IndepFun.map_mul_eq_map_mconv_map'`, `ProbabilityTheory.IndepFun.map_mul_eq_map_mconv_map₀'`, `mconv_smul_right`, `zero_mconv`, `mconv_dirac`, `dirac_mconv`, `mconv_smul_left`, `probabilitymeasure_of_probabilitymeasures_mconv`, `mconv_comm`, `MeasureTheory.mconv_withDensity_eq_mlconvolution₀`, `mconv_zero`, `mconv_add`, `lintegral_mconv_eq_lintegral_prod`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_conv` 📖	mathematical	—	`conv` `MeasureTheory.Measure` `instAdd`	—	`add_prod` `map_add` `Measurable.add` `Measurable.fst` `measurable_id'` `Measurable.snd`
`add_mconv` 📖	mathematical	—	`mconv` `MeasureTheory.Measure` `instAdd`	—	`add_prod` `map_add` `Measurable.mul` `Measurable.fst` `measurable_id'` `Measurable.snd`
`conv_absolutelyContinuous` 📖	mathematical	`AbsolutelyContinuous`	`conv`	—	`MeasureTheory.lintegral_indicator_one` `lintegral_conv` `Measurable.indicator` `measurable_one` `Set.indicator_comp_right` `MeasurableSet.preimage` `Measurable.const_add` `MeasurableAdd₂.toMeasurableAdd` `measurable_id'` `map_apply` `IsAddLeftInvariant.map_add_left_eq_self` `MeasureTheory.lintegral_const` `MulZeroClass.zero_mul`
`conv_add` 📖	mathematical	—	`conv` `MeasureTheory.Measure` `instAdd`	—	`prod_add` `map_add` `Measurable.add` `Measurable.fst` `measurable_id'` `Measurable.snd`
`conv_assoc` 📖	mathematical	—	`conv`	—	`ext_of_lintegral` `lintegral_conv` `Measurable.lintegral_prod_left` `Measurable.fun_comp` `Measurable.add` `Measurable.snd` `measurable_id'` `Measurable.fst` `sfinite_conv_of_sfinite` `MeasureTheory.lintegral_congr` `Measurable.const_add` `MeasurableAdd₂.toMeasurableAdd` `add_assoc`
`conv_comm` 📖	mathematical	—	`conv` `AddCommMonoid.toAddMonoid`	—	`prod_swap` `map_map` `Measurable.add` `Measurable.fst` `measurable_id'` `Measurable.snd` `measurable_swap` `add_comm`
`conv_dirac` 📖	mathematical	—	`conv` `dirac` `map` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	`prod_dirac` `map_map` `Measurable.add` `Measurable.fst` `measurable_id'` `Measurable.snd` `Measurable.prodMk` `measurable_const`
`conv_dirac_zero` 📖	mathematical	—	`conv` `dirac` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	`conv_dirac` `add_zero` `map_id'`
`conv_smul_left` 📖	mathematical	—	`conv` `ENNReal` `MeasureTheory.Measure` `instSMul` `Algebra.toSMul` `ENNReal.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `IsScalarTower.right`	—	`IsScalarTower.right` `map_smul` `prod_smul_left`
`conv_zero` 📖	mathematical	—	`conv` `MeasureTheory.Measure` `instZero`	—	`prod_zero` `map_zero`
`dirac_conv` 📖	mathematical	—	`conv` `dirac` `map` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	`dirac_prod` `map_map` `Measurable.add` `Measurable.fst` `measurable_id'` `Measurable.snd` `Measurable.prodMk` `measurable_const`
`dirac_conv_dirac` 📖	mathematical	—	`conv` `dirac` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	`conv_dirac` `MeasureTheory.instSFiniteOfSigmaFinite` `dirac.instSigmaFinite` `map_dirac` `Measurable.add_const` `MeasurableAdd₂.toMeasurableAdd` `measurable_id'`
`dirac_mconv` 📖	mathematical	—	`mconv` `dirac` `map` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	`dirac_prod` `map_map` `Measurable.mul` `Measurable.fst` `measurable_id'` `Measurable.snd` `Measurable.prodMk` `measurable_const`
`dirac_mconv_dirac` 📖	mathematical	—	`mconv` `dirac` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	`mconv_dirac` `MeasureTheory.instSFiniteOfSigmaFinite` `dirac.instSigmaFinite` `map_dirac` `Measurable.mul_const` `MeasurableMul₂.toMeasurableMul` `measurable_id'`
`dirac_one_mconv` 📖	mathematical	—	`mconv` `dirac` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	`dirac_mconv` `one_mul` `map_id'`
`dirac_zero_conv` 📖	mathematical	—	`conv` `dirac` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	`dirac_conv` `zero_add` `map_id'`
`finite_of_finite_conv` 📖	mathematical	—	`MeasureTheory.IsFiniteMeasure` `conv`	—	`MeasureTheory.IsFiniteMeasure.measure_univ_lt_top` `isFiniteMeasure_map` `prod.instIsFiniteMeasure`
`finite_of_finite_mconv` 📖	mathematical	—	`MeasureTheory.IsFiniteMeasure` `mconv`	—	`MeasureTheory.IsFiniteMeasure.measure_univ_lt_top` `isFiniteMeasure_map` `prod.instIsFiniteMeasure`
`lintegral_conv` 📖	mathematical	`Measurable` `ENNReal` `ENNReal.measurableSpace`	`MeasureTheory.lintegral` `conv` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	`lintegral_conv_eq_lintegral_sum` `MeasureTheory.lintegral_prod` `Measurable.comp_aemeasurable'` `AEMeasurable.add` `AEMeasurable.fst` `aemeasurable_id` `AEMeasurable.snd`
`lintegral_conv_eq_lintegral_sum` 📖	mathematical	`Measurable` `ENNReal` `ENNReal.measurableSpace`	`MeasureTheory.lintegral` `conv` `Prod.instMeasurableSpace` `prod` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	`conv.eq_1` `MeasureTheory.lintegral_map` `MeasurableAdd₂.measurable_add`
`lintegral_mconv` 📖	mathematical	`Measurable` `ENNReal` `ENNReal.measurableSpace`	`MeasureTheory.lintegral` `mconv` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	`lintegral_mconv_eq_lintegral_prod` `MeasureTheory.lintegral_prod` `Measurable.comp_aemeasurable'` `AEMeasurable.mul` `AEMeasurable.fst` `aemeasurable_id` `AEMeasurable.snd`
`lintegral_mconv_eq_lintegral_prod` 📖	mathematical	`Measurable` `ENNReal` `ENNReal.measurableSpace`	`MeasureTheory.lintegral` `mconv` `Prod.instMeasurableSpace` `prod` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	`mconv.eq_1` `MeasureTheory.lintegral_map` `MeasurableMul₂.measurable_mul`
`map_conv_addMonoidHom` 📖	mathematical	`Measurable` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidHom.instFunLike`	`map` `conv`	—	`map_map` `Measurable.add` `Measurable.fst` `measurable_id'` `Measurable.snd` `map_add` `AddMonoidHomClass.toAddHomClass` `AddMonoidHom.instAddMonoidHomClass` `Measurable.prodMap` `map_prod_map`
`map_conv_continuousLinearMap` 📖	mathematical	—	`map` `DFunLike.coe` `ContinuousLinearMap` `Real` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `ContinuousLinearMap.funLike` `conv` `AddCommMonoid.toAddMonoid`	—	`DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `ContinuousLinearMap.continuousSemilinearMapClass` `map_conv_addMonoidHom` `AddMonoidHom.coe_coe` `Continuous.measurable` `ContinuousLinearMap.continuous`
`map_mconv_monoidHom` 📖	mathematical	`Measurable` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MonoidHom.instFunLike`	`map` `mconv`	—	`map_map` `Measurable.mul` `Measurable.fst` `measurable_id'` `Measurable.snd` `map_mul` `MonoidHomClass.toMulHomClass` `MonoidHom.instMonoidHomClass` `Measurable.prodMap` `map_prod_map`
`mconv_absolutelyContinuous` 📖	mathematical	`AbsolutelyContinuous`	`mconv`	—	`MeasureTheory.lintegral_indicator_one` `lintegral_mconv` `Measurable.indicator` `measurable_one` `MeasurableSet.preimage` `Measurable.const_mul` `MeasurableMul₂.toMeasurableMul` `measurable_id'` `map_apply` `IsMulLeftInvariant.map_mul_left_eq_self` `MeasureTheory.lintegral_const` `MulZeroClass.zero_mul`
`mconv_add` 📖	mathematical	—	`mconv` `MeasureTheory.Measure` `instAdd`	—	`prod_add` `map_add` `Measurable.mul` `Measurable.fst` `measurable_id'` `Measurable.snd`
`mconv_assoc` 📖	mathematical	—	`mconv`	—	`ext_of_lintegral` `lintegral_mconv` `Measurable.lintegral_prod_left` `Measurable.fun_comp` `Measurable.mul` `Measurable.snd` `measurable_id'` `Measurable.fst` `sfinite_mconv_of_sfinite` `MeasureTheory.lintegral_congr` `Measurable.const_mul` `MeasurableMul₂.toMeasurableMul` `mul_assoc`
`mconv_comm` 📖	mathematical	—	`mconv` `CommMonoid.toMonoid`	—	`prod_swap` `map_map` `Measurable.mul` `Measurable.fst` `measurable_id'` `Measurable.snd` `measurable_swap` `mul_comm`
`mconv_dirac` 📖	mathematical	—	`mconv` `dirac` `map` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	`prod_dirac` `map_map` `Measurable.mul` `Measurable.fst` `measurable_id'` `Measurable.snd` `Measurable.prodMk` `measurable_const`
`mconv_dirac_one` 📖	mathematical	—	`mconv` `dirac` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	`mconv_dirac` `mul_one` `map_id'`
`mconv_smul_left` 📖	mathematical	—	`mconv` `ENNReal` `MeasureTheory.Measure` `instSMul` `Algebra.toSMul` `ENNReal.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `IsScalarTower.right`	—	`IsScalarTower.right` `map_smul` `prod_smul_left`
`mconv_zero` 📖	mathematical	—	`mconv` `MeasureTheory.Measure` `instZero`	—	`prod_zero` `map_zero`
`probabilitymeasure_of_probabilitymeasures_conv` 📖	mathematical	—	`MeasureTheory.IsProbabilityMeasure` `conv`	—	`isProbabilityMeasure_map` `prod.instIsProbabilityMeasure` `AEMeasurable.add` `AEMeasurable.fst` `aemeasurable_id` `AEMeasurable.snd`
`probabilitymeasure_of_probabilitymeasures_mconv` 📖	mathematical	—	`MeasureTheory.IsProbabilityMeasure` `mconv`	—	`isProbabilityMeasure_map` `prod.instIsProbabilityMeasure` `AEMeasurable.mul` `AEMeasurable.fst` `aemeasurable_id` `AEMeasurable.snd`
`sfinite_conv_of_sfinite` 📖	mathematical	—	`MeasureTheory.SFinite` `conv`	—	`instSFiniteMap` `prod.instSFinite`
`sfinite_mconv_of_sfinite` 📖	mathematical	—	`MeasureTheory.SFinite` `mconv`	—	`instSFiniteMap` `prod.instSFinite`
`zero_conv` 📖	mathematical	—	`conv` `MeasureTheory.Measure` `instZero`	—	`zero_prod` `map_zero`
`zero_mconv` 📖	mathematical	—	`mconv` `MeasureTheory.Measure` `instZero`	—	`zero_prod` `map_zero`

---

← Back to Index