Additional L² helpers

Technical lemmas supporting the L² proof of de Finetti's theorem.

Contents

• CDF/Stieltjes constructions used by MainConvergence.lean

CDF construction via stieltjesOfMeasurableRat

Wraps mathlib's measurable-rational-CDF infrastructure to give CDFs with the right boundary behavior at ±∞ for every ω (not just a.e.).

theorem Exchangeability.DeFinetti.ViaL2.cdf_from_alpha_limits {Ω : Type u_3} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (X : ℕ → Ω → ℝ) (hX_contract : Contractable μ X) (hX_meas : ∀ (i : ℕ), Measurable (X i)) (hX_L2 : ∀ (i : ℕ), MeasureTheory.MemLp (X i) 2 μ) (ω : Ω) : Filter.Tendsto (cdf_from_alpha X hX_contract hX_meas hX_L2 ω) Filter.atBot (nhds 0) ∧ Filter.Tendsto (cdf_from_alpha X hX_contract hX_meas hX_L2 ω) Filter.atTop (nhds 1)

CDF limits at ±∞: F(t) → 0 as t → -∞ and F(t) → 1 as t → +∞.

This is now trivial because cdf_from_alpha is defined via stieltjesOfMeasurableRat, which guarantees these limits for ALL ω (not just a.e.) by construction.

The stieltjesOfMeasurableRat construction automatically patches the null set where the raw L¹ limit alphaIic would fail to have proper CDF limits.

theorem Exchangeability.DeFinetti.ViaL2.directing_measure_eval_Iic_measurable {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (X : ℕ → Ω → ℝ) (hX_contract : Contractable μ X) (hX_meas : ∀ (i : ℕ), Measurable (X i)) (hX_L2 : ∀ (i : ℕ), MeasureTheory.MemLp (X i) 2 μ) (t : ℝ) : Measurable fun (ω : Ω) => (directing_measure X hX_contract hX_meas hX_L2 ω) (Set.Iic t)

For each fixed t, ω ↦ ν(ω)((-∞,t]) is measurable. This is the base case for the π-λ theorem.

theorem Exchangeability.DeFinetti.ViaL2.directing_measure_measurable {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (X : ℕ → Ω → ℝ) (hX_contract : Contractable μ X) (hX_meas : ∀ (i : ℕ), Measurable (X i)) (hX_L2 : ∀ (i : ℕ), MeasureTheory.MemLp (X i) 2 μ) (s : Set ℝ) (hs : MeasurableSet s) : Measurable fun (ω : Ω) => (directing_measure X hX_contract hX_meas hX_L2 ω) s

For each measurable set s, the map ω ↦ ν(ω)(s) is measurable.

This is the key measurability property needed for conditional_iid_from_directing_measure. Uses monotone class theorem (π-λ theorem) - prove for intervals, extend to all Borel sets.

theorem Exchangeability.DeFinetti.ViaL2.directing_measure_bridge {Ω : Type u_1} [MeasurableSpace Ω] [StandardBorelSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (X : ℕ → Ω → ℝ) (hX_contract : Contractable μ X) (hX_meas : ∀ (i : ℕ), Measurable (X i)) (hX_L2 : ∀ (i : ℕ), MeasureTheory.MemLp (X i) 2 μ) {m : ℕ} (k : Fin m → ℕ) (hk : Function.Injective k) (B : Fin m → Set ℝ) (hB : ∀ (i : Fin m), MeasurableSet (B i)) : ∫⁻ (ω : Ω), ∏ i : Fin m, ENNReal.ofReal ((B i).indicator (fun (x : ℝ) => 1) (X (k i) ω)) ∂μ = ∫⁻ (ω : Ω), ∏ i : Fin m, (directing_measure X hX_contract hX_meas hX_L2 ω) (B i) ∂μ

The bridge property: E[∏ᵢ 𝟙_{Bᵢ}(X_{k(i)})] = E[∏ᵢ ν(·)(Bᵢ)].

This is the key property needed for conditional_iid_from_directing_measure. Uses indicator_product_bridge from BridgeProperty.lean, establishing that the directing measure satisfies hν_law via shift invariance of conditional expectations.

theorem Exchangeability.DeFinetti.ViaL2.directing_measure_satisfies_requirements {Ω : Type u_1} [MeasurableSpace Ω] [StandardBorelSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (X : ℕ → Ω → ℝ) (hX_meas : ∀ (i : ℕ), Measurable (X i)) (hX_contract : Contractable μ X) (hX_L2 : ∀ (i : ℕ), MeasureTheory.MemLp (X i) 2 μ) : ∃ (ν : Ω → MeasureTheory.Measure ℝ), (∀ (ω : Ω), MeasureTheory.IsProbabilityMeasure (ν ω)) ∧ (∀ (s : Set ℝ), MeasurableSet s → Measurable fun (ω : Ω) => (ν ω) s) ∧ ∀ {m : ℕ} (k : Fin m → ℕ), Function.Injective k → ∀ (B : Fin m → Set ℝ), (∀ (i : Fin m), MeasurableSet (B i)) → ∫⁻ (ω : Ω), ∏ i : Fin m, ENNReal.ofReal ((B i).indicator (fun (x : ℝ) => 1) (X (k i) ω)) ∂μ = ∫⁻ (ω : Ω), ∏ i : Fin m, (ν ω) (B i) ∂μ

Main packaging theorem for L² proof.

This theorem packages all the directing measure properties needed by CommonEnding.conditional_iid_from_directing_measure:

1. ν is a probability measure for all ω
2. ω ↦ ν(ω)(s) is measurable for all measurable sets s
3. The bridge property: E[∏ᵢ 1_{Bᵢ}(X_{k(i)})] = E[∏ᵢ ν(·)(Bᵢ)]

This enables the final step of the L² proof of de Finetti's theorem.