Theorems · Theorem · abstract harmonic analysis

MeasureTheory.Measure.mconv_dirac

∀ {M : Type u_1} [inst : Monoid M] [inst_1 : MeasurableSpace M] [MeasurableMul₂ M] (μ : MeasureTheory.Measure M)
  [MeasureTheory.SFinite μ] (x : M),
  μ.mconv (MeasureTheory.Measure.dirac x) = MeasureTheory.Measure.map (fun y => y * x) μ

Defined in: Mathlib.MeasureTheory.Group.Convolution
Cited by: 2 results in Mathlib
Foundations: Depth 223 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Monoid MeasurableSpace MeasurableMul₂ MeasureTheory.SFinite

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites16

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.mapstatement and proof · cited by 858
MeasureTheory.SFinitestatement and proof · cited by 449
MeasureTheory.Measure.diracstatement · cited by 210
measurable_constproof · cited by 156
measurable_id'proof · cited by 145
MeasurableMul₂statement and proof · cited by 139
Measurable.prodMkproof · cited by 115
MeasureTheory.Measure.map_mapproof · cited by 67
Measurable.fstproof · cited by 51

Cited by2

Results whose statement or proof uses this declaration.

MeasureTheory.Measure.dirac_mconv_diracproof · cited by 0
MeasureTheory.Measure.mconv_dirac_oneproof · cited by 0