Finite measures

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

On a finite measurable space, a probability measure is the sum of its singleton masses.

Main results

• MeasureTheory.FiniteMeasure.instMeasurableSingletonClass
• MeasureTheory.ProbabilityMeasure.instMeasurableSingletonClass
• MeasureTheory.Measure.sum_singleton_eq_one

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 α] [MeasurableSingletonClass (FiniteMeasure α)] : MeasurableSingletonClass (ProbabilityMeasure α)

Singletons are measurable in the space of probability measures whenever they are measurable in the space of finite measures, as they are when the σ-algebra on α is countably generated (FiniteMeasure.instMeasurableSingletonClass).

theorem MeasureTheory.Measure.sum_singleton_eq_one {κ : Type u_2} [Fintype κ] [MeasurableSpace κ] [MeasurableSingletonClass κ] (ν : Measure κ) [IsProbabilityMeasure ν] : ∑ k : κ, ν {k} = 1

The singleton masses of a probability measure on a finite measurable space sum to one.