Theorems · Definition · abstract harmonic analysis
MeasureTheory.Measure.mconv
{M : Type u_1} →
[Monoid M] → [inst : MeasurableSpace M] → MeasureTheory.Measure M → MeasureTheory.Measure M → MeasureTheory.Measure MMultiplicative convolution of measures.
- Defined in
- Mathlib.MeasureTheory.Group.Convolution
- Cited by
- 31 results in Mathlib
- Foundations
- Depth 214 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- MonoidMeasurableSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- MeasurableSpacestatement and proof · cited by 13,106
- MeasureTheory.Measurestatement and proof · cited by 10,939
- Monoidstatement and proof · cited by 3,887
- MeasureTheory.Measure.mapproof · cited by 858
- MeasureTheory.Measure.prodproof · cited by 353
Cited by31
Results whose statement or proof uses this declaration.
- ProbabilityTheory.IndepFun.map_mul_eq_map_mconv_map₀'statement and proof · cited by 5
- MeasureTheory.Measure.mconv_absolutelyContinuousstatement · cited by 3
- MeasureTheory.mconv_eq_withDensity_mlconvolution_rnDerivstatement and proof · cited by 3
- MeasureTheory.Measure.mconv_diracstatement · cited by 2
- ProbabilityTheory.IndepFun.map_mul_eq_map_mconv_map₀statement · cited by 2
- MeasureTheory.Measure.lintegral_mconvstatement · cited by 2
- MeasureTheory.Measure.lintegral_mconv_eq_lintegral_prodstatement · cited by 2
- MeasureTheory.HaveLebesgueDecomposition.mconvstatement and proof · cited by 2
- MeasureTheory.rnDeriv_mconv'statement and proof · cited by 1
- MeasureTheory.mconv_withDensity_eq_mlconvolutionstatement · cited by 1
- MeasureTheory.mconv_withDensity_eq_mlconvolution₀statement · cited by 1
- ProbabilityTheory.IndepFun.hasLaw_mulstatement and proof · cited by 1