Dirac measures and their pushforwards

Mathlib's MeasureTheory.Measure.map_dirac' computes (Measure.dirac x).map T = Measure.dirac (T x) for a measurable T. A Dirac measure leaves a map no room to be modified on a null set: its only null sets avoid x, so a Measure.dirac x-a.e. measurable map already agrees at x with the measurable representative it is a.e. equal to. The pushforward formula therefore holds under that weaker hypothesis, which is the one a.e.-measurable interfaces such as ProbabilityTheory.HasLaw provide.

Main results

• Measure.map_dirac_of_aemeasurable — the Dirac pushforward formula for a map that is only a.e. measurable.
• Measure.dirac_eq_dirac_of_inseparable — inseparable points have equal Borel Dirac measures.

@[simp]

theorem Measure.map_dirac_of_aemeasurable {X : Type u_1} {Y : Type u_2} [MeasurableSpace X] [MeasurableSpace Y] {T : X → Y} {x : X} (hT : AEMeasurable T (MeasureTheory.Measure.dirac x)) : MeasureTheory.Measure.map T (MeasureTheory.Measure.dirac x) = MeasureTheory.Measure.dirac (T x)

A Dirac measure leaves a map no room to be modified on a null set: pushing Measure.dirac x forward along a Measure.dirac x-a.e. measurable map is evaluating that map at x.

theorem Measure.dirac_eq_dirac_of_inseparable {X : Type u_1} [MeasurableSpace X] [TopologicalSpace X] [BorelSpace X] {x y : X} (hxy : Inseparable x y) : MeasureTheory.Measure.dirac x = MeasureTheory.Measure.dirac y

Dirac measures at topologically inseparable points agree: Borel measurable sets cannot separate the points.