Measurable coding of probability measures

The Giry measurable space on ProbabilityMeasure α is generated by evaluation on measurable sets, but it is not currently available as a standard Borel space. When α is countably generated, probability measures nevertheless admit a canonical measurable injective code into a countable product of ℝ≥0∞: evaluate on the countable set algebra generated by Mathlib's chosen countableGeneratingSet α.

This code lets probability arguments use a standard Borel target without imposing a topology on α. Its coordinates generate the Giry measurable space, so every measurable function of a probability measure into a nonempty standard Borel space factors measurably through the code. Injectivity follows from uniqueness of finite measures on a generating set algebra.

Main definitions and results

• TauCeti.MeasureTheory.ProbabilityMeasureCodeIndex -- the countable generating set algebra;
• TauCeti.MeasureTheory.probabilityMeasureCode -- evaluation on every member of that algebra;
• TauCeti.MeasureTheory.measurable_probabilityMeasureCode -- measurability of the code;
• TauCeti.MeasureTheory.measurableSpace_probabilityMeasure_eq_comap_probabilityMeasureCode -- the Giry measurable space is induced by the code;
• Measurable.exists_eq_measurable_comp_probabilityMeasureCode -- measurable factorization through the code;
• TauCeti.MeasureTheory.probabilityMeasureCode_injective -- the code determines the measure.

@[reducible, inline]

abbrev TauCeti.MeasureTheory.ProbabilityMeasureCodeIndex (α : Type u_2) [MeasurableSpace α] [MeasurableSpace.CountablyGenerated α] : Type u_2

The countable index type used to code a probability measure: the set algebra generated by Mathlib's chosen countable generating family for the measurable space.

Equations

• TauCeti.MeasureTheory.ProbabilityMeasureCodeIndex α = { s : Set α // s ∈ MeasureTheory.generateSetAlgebra (MeasurableSpace.countableGeneratingSet α) }

instance TauCeti.MeasureTheory.instCountableProbabilityMeasureCodeIndex {α : Type u_1} [MeasurableSpace α] [MeasurableSpace.CountablyGenerated α] : Countable (ProbabilityMeasureCodeIndex α)

def TauCeti.MeasureTheory.probabilityMeasureCode {α : Type u_1} [MeasurableSpace α] [MeasurableSpace.CountablyGenerated α] (P : MeasureTheory.ProbabilityMeasure α) : ProbabilityMeasureCodeIndex α → ENNReal

The measurable evaluation code of a probability measure on a countably generated space.

Equations

• TauCeti.MeasureTheory.probabilityMeasureCode P s = ↑P ↑s

@[simp]

theorem TauCeti.MeasureTheory.probabilityMeasureCode_apply {α : Type u_1} [MeasurableSpace α] [MeasurableSpace.CountablyGenerated α] (P : MeasureTheory.ProbabilityMeasure α) (s : ProbabilityMeasureCodeIndex α) : probabilityMeasureCode P s = ↑P ↑s

Evaluation of the probability-measure code.

theorem TauCeti.MeasureTheory.measurableSet_probabilityMeasureCodeIndex {α : Type u_1} [MeasurableSpace α] [MeasurableSpace.CountablyGenerated α] (s : ProbabilityMeasureCodeIndex α) : MeasurableSet ↑s

Every member of the coding set algebra is measurable.

theorem TauCeti.MeasureTheory.measurable_probabilityMeasureCode {α : Type u_1} [MeasurableSpace α] [MeasurableSpace.CountablyGenerated α] : Measurable probabilityMeasureCode

The evaluation code is measurable into its countable product space.

theorem TauCeti.MeasureTheory.measurableSpace_probabilityMeasure_eq_comap_probabilityMeasureCode {α : Type u_1} [MeasurableSpace α] [MeasurableSpace.CountablyGenerated α] : inferInstance = MeasurableSpace.comap probabilityMeasureCode inferInstance

The Giry measurable space on probability measures over a countably generated space is the pullback of the product measurable space along the canonical evaluation code.

theorem Measurable.exists_eq_measurable_comp_probabilityMeasureCode {α : Type u_1} [MeasurableSpace α] [MeasurableSpace.CountablyGenerated α] {γ : Type u_2} [MeasurableSpace γ] [StandardBorelSpace γ] [Nonempty γ] {F : MeasureTheory.ProbabilityMeasure α → γ} (hF : Measurable F) : ∃ (G : (TauCeti.MeasureTheory.ProbabilityMeasureCodeIndex α → ENNReal) → γ), Measurable G ∧ F = G ∘ TauCeti.MeasureTheory.probabilityMeasureCode

A measurable function of a probability measure into a nonempty standard Borel space factors measurably through its canonical code. The extension away from codes of actual probability measures is not specified.

theorem TauCeti.MeasureTheory.probabilityMeasureCode_injective {α : Type u_1} [MeasurableSpace α] [MeasurableSpace.CountablyGenerated α] : Function.Injective probabilityMeasureCode

The evaluation code determines a probability measure on a countably generated space.