Measurable singletons in spaces of finite measures

When the underlying σ-algebra is countably generated, singletons are measurable in FiniteMeasure α and in ProbabilityMeasure α.

Main results

• MeasureTheory.FiniteMeasure.instMeasurableSingletonClass
• MeasureTheory.ProbabilityMeasure.instMeasurableSingletonClass

Implementation

The statement is really about finite measures; the probability-measure form is the subtype corollary. Countable generation is exactly what the proof consumes — StandardBorelSpace α implies it, but is stronger than needed.

A countable generating family need not be closed under intersection, so it is replaced by the set algebra it generates (MeasureTheory.generateSetAlgebra), which is still countable, is a π-system, and generates the same σ-algebra. A finite measure is then pinned down by its values there (ext_of_generate_finite, with Set.univ supplied by the algebra), so {μ} is the countable intersection of the equalizers {ν | ν s = μ s}. Each equalizer is measurable because evaluation at a fixed measurable set is.

instance MeasureTheory.FiniteMeasure.instMeasurableSingletonClass {α : Type u_1} [MeasurableSpace α] [MeasurableSpace.CountablyGenerated α] : MeasurableSingletonClass (FiniteMeasure α)

Singletons are measurable in the space of finite measures, when the σ-algebra on α is countably generated.

instance MeasureTheory.ProbabilityMeasure.instMeasurableSingletonClass {α : Type u_1} [MeasurableSpace α] [MeasurableSpace.CountablyGenerated α] : MeasurableSingletonClass (ProbabilityMeasure α)

Singletons are measurable in the space of probability measures, when the σ-algebra on α is countably generated. Pulled back from the finite-measure instance along the injective measurable map ProbabilityMeasure.toFiniteMeasure, so the argument is not repeated.