Directing Measure Construction

From conditional expectations on indicators, we build a measurable family of probability measures ν : Ω → Measure α.

The construction uses the standard Borel machinery: for each ω, define ν ω to be the unique probability measure satisfying ν ω B = E[1_{X₀∈B} | 𝒯_X](ω) for all measurable B.

This requires StandardBorelSpace assumption on α to ensure existence.

Main definitions

• directingMeasure X hX ω - The directing measure at ω

Main results

• directingMeasure_isProb - Each directing measure is a probability measure
• directingMeasure_measurable_eval - Directing measure is measurable in ω
• directingMeasure_X0_marginal - ν ω B = E1_{X₀∈B} | tail a.e.
• conditional_law_eq_directingMeasure - All X_n have directing measure as conditional law

Directing measure construction

noncomputable def Exchangeability.DeFinetti.ViaMartingale.directingMeasure {Ω : Type u_1} [MeasurableSpace Ω] [StandardBorelSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {α : Type u_2} [MeasurableSpace α] [StandardBorelSpace α] [Nonempty α] (X : ℕ → Ω → α) (_hX : ∀ (n : ℕ), Measurable (X n)) (ω : Ω) : MeasureTheory.Measure α

Directing measure: conditional distribution of X₀ given the tail σ-algebra.

Constructed using condExpKernel API: for each ω, evaluate the conditional expectation kernel at ω to get a measure on Ω, then push forward along X₀.

Concretely: directingMeasure ω = (condExpKernel μ (tailSigma X) ω).map (X 0)

Equations

• Exchangeability.DeFinetti.ViaMartingale.directingMeasure X _hX ω = MeasureTheory.Measure.map (X 0) ((ProbabilityTheory.condExpKernel μ (Exchangeability.DeFinetti.ViaMartingale.tailSigma X)) ω)

theorem Exchangeability.DeFinetti.ViaMartingale.directingMeasure_measurable_eval {Ω : Type u_1} [MeasurableSpace Ω] [StandardBorelSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {α : Type u_2} [MeasurableSpace α] [StandardBorelSpace α] [Nonempty α] (X : ℕ → Ω → α) (hX : ∀ (n : ℕ), Measurable (X n)) (B : Set α) : MeasurableSet B → Measurable fun (ω : Ω) => (directingMeasure X hX ω) B

directingMeasure evaluates measurably on measurable sets.

Uses: Kernel.measurable_coe and Measure.map_apply.

theorem Exchangeability.DeFinetti.ViaMartingale.directingMeasure_isProb {Ω : Type u_1} [MeasurableSpace Ω] [StandardBorelSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {α : Type u_2} [MeasurableSpace α] [StandardBorelSpace α] [Nonempty α] (X : ℕ → Ω → α) (hX : ∀ (n : ℕ), Measurable (X n)) (ω : Ω) : MeasureTheory.IsProbabilityMeasure (directingMeasure X hX ω)

The directing measure is (pointwise) a probability measure.

Uses: isProbability_condExpKernel and map preserves probability.

theorem Exchangeability.DeFinetti.ViaMartingale.directingMeasure_X0_marginal {Ω : Type u_1} [MeasurableSpace Ω] [StandardBorelSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {α : Type u_2} [MeasurableSpace α] [StandardBorelSpace α] [Nonempty α] (X : ℕ → Ω → α) (hX : ∀ (n : ℕ), Measurable (X n)) (B : Set α) (hB : MeasurableSet B) : (fun (ω : Ω) => ((directingMeasure X hX ω) B).toReal) =ᵐ[μ] μ[(B.indicator fun (x : α) => 1) ∘ X 0|tailSigma X]

X₀-marginal identity: the conditional expectation of the indicator of X 0 ∈ B given the tail equals the directing measure of B (toReal).

Uses: condExp_ae_eq_integral_condExpKernel and integral_indicator_one.

Conditional law equality

theorem Exchangeability.DeFinetti.ViaMartingale.conditional_law_eq_of_X0_marginal {Ω : Type u_1} [MeasurableSpace Ω] [StandardBorelSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {α : Type u_2} [MeasurableSpace α] [StandardBorelSpace α] [Nonempty α] (X : ℕ → Ω → α) (hX : Contractable μ X) (hX_meas : ∀ (n : ℕ), Measurable (X n)) (ν : Ω → MeasureTheory.Measure α) (hν : ∀ (B : Set α), MeasurableSet B → (fun (ω : Ω) => ((ν ω) B).toReal) =ᵐ[μ] μ[(B.indicator fun (x : α) => 1) ∘ X 0|tailSigma X]) (n : ℕ) (B : Set α) (hB : MeasurableSet B) : (fun (ω : Ω) => ((ν ω) B).toReal) =ᵐ[μ] μ[(B.indicator fun (x : α) => 1) ∘ X n|tailSigma X]

General form: All X_n have the same conditional law ν. This follows from extreme_members_equal_on_tail.

theorem Exchangeability.DeFinetti.ViaMartingale.conditional_law_eq_directingMeasure {Ω : Type u_1} [MeasurableSpace Ω] [StandardBorelSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {α : Type u_2} [MeasurableSpace α] [StandardBorelSpace α] [Nonempty α] (X : ℕ → Ω → α) (hX : Contractable μ X) (hX_meas : ∀ (n : ℕ), Measurable (X n)) (n : ℕ) (B : Set α) (hB : MeasurableSet B) : (fun (ω : Ω) => ((directingMeasure X hX_meas ω) B).toReal) =ᵐ[μ] μ[(B.indicator fun (x : α) => 1) ∘ X n|tailSigma X]

All coordinates share the directing measure as their conditional law.

This is the key "common ending" result: the directing measure ν constructed from the tail σ-algebra satisfies the marginal identity for all coordinates, not just X₀.