Mathlib Map

Theorems · Theorem · abstract harmonic analysis

MeasureTheory.Measure.conv_dirac

∀ {M : Type u_1} [inst : AddMonoid M] [inst_1 : MeasurableSpace M] [MeasurableAdd₂ M] (μ : MeasureTheory.Measure M)
  [MeasureTheory.SFinite μ] (x : M),
  μ.conv (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
AddMonoidMeasurableSpaceMeasurableAdd₂MeasureTheory.SFinite
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

MeasureTheory.Measure.conv_dirac_zero · cited by 0Measure.conv_dirac_zeroMeasureTheory.Measure.dirac_conv_dirac · cited by 0Measure.dirac_conv_diracMeasurableSpace · cited by 13106MeasurableSpaceMeasureTheory.Measure · cited by 10939MeasureTheory.MeasureAddMonoid · cited by 2864AddMonoidMeasureTheory.Measure.map · cited by 858Measure.mapMeasureTheory.SFinite · cited by 449MeasureTheory.SFiniteMeasureTheory.Measure.dirac · cited by 210Measure.diracmeasurable_const · cited by 156measurable_constMeasurableAdd₂ · cited by 155MeasurableAdd₂measurable_id' · cited by 145measurable_id'Measurable.prodMk · cited by 115Measurable.prodMkMeasureTheory.Measure.map_map · cited by 67Measure.map_mapMeasurable.fst · cited by 51Measurable.fstMeasurable.snd · cited by 51Measurable.sndMeasureTheory.Measure.conv · cited by 41Measure.convMeasurable.fun_add · cited by 11Measurable.fun_addMeasure.conv_diracCITED BYCITES

Cites16

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by2

Results whose statement or proof uses this declaration.