Alpha_Iic: Raw CDF Functions for Directing Measure #

This file defines the raw CDF-building functions indIic, alphaIic, and alphaIicRat used in the L² proof of de Finetti's theorem. These are the building blocks for the directing measure construction via Carathéodory extension.

Main definitions #

indIic t: Indicator of (-∞, t] as a bounded measurable function ℝ → ℝ
alphaIic: Raw CDF at level t (clipped L¹ limit of Cesàro averages)
alphaIicRat: Rational restriction of alphaIic for stieltjesOfMeasurableRat

Main results #

indIic_measurable: indIic t is measurable
indIic_bdd: |indIic t x| ≤ 1 for all x
alphaIic_measurable: alphaIic is measurable in ω
alphaIic_bound: 0 ≤ alphaIic ω ≤ 1 for all ω
measurable_alphaIicRat: Joint measurability for stieltjesOfMeasurableRat

References #

Kallenberg (2005), Probabilistic Symmetries and Invariance Principles, Chapter 1, "Second proof of Theorem 1.1"

Indicator of Iic #

The indicator function 1_{(-∞, t]} serves as the basic building block for CDF construction.

source

def Exchangeability.DeFinetti.ViaL2.indIic (t : ℝ) :

ℝ → ℝ

Indicator of (-∞, t] as a bounded measurable function ℝ → ℝ.

Equations

Exchangeability.DeFinetti.ViaL2.indIic t = (Set.Iic t).indicator fun (x : ℝ) => 1

Instances For

source

theorem Exchangeability.DeFinetti.ViaL2.indIic_measurable (t : ℝ) :

Measurable (indIic t)

source

theorem Exchangeability.DeFinetti.ViaL2.indIic_bdd (t x : ℝ) :

|indIic t x| ≤ 1

Raw CDF: alphaIic #

The L¹-limit of Cesàro averages of indIic t ∘ X_i, clipped to [0,1] to ensure pointwise bounds. This is the "raw" CDF before regularization.

source

noncomputable def Exchangeability.DeFinetti.ViaL2.alphaIic {Ω : 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 : ℝ) :

Ω → ℝ

Raw "CDF" at level t: the L¹-limit α_{1_{(-∞,t]}} produced by Step 2, clipped to [0,1] to ensure pointwise bounds.

The clipping preserves measurability and a.e. equality (hence L¹ properties) since the underlying limit is a.e. in [0,1] anyway (being the limit of averages in [0,1]).

Equations

Exchangeability.DeFinetti.ViaL2.alphaIic X hX_contract hX_meas hX_L2 t ω = max 0 (min 1 (⋯.choose ω))

Instances For

source

theorem Exchangeability.DeFinetti.ViaL2.alphaIic_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 (alphaIic X hX_contract hX_meas hX_L2 t)

Measurability of the raw α_{Iic t}.

source

theorem Exchangeability.DeFinetti.ViaL2.alphaIic_bound {Ω : 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 : ℝ) (ω : Ω) :

0 ≤ alphaIic X hX_contract hX_meas hX_L2 t ω ∧ alphaIic X hX_contract hX_meas hX_L2 t ω ≤ 1

0 ≤ α_{Iic t} ≤ 1. The α is an L¹-limit of averages of indicators in [0,1].

DESIGN NOTE: This lemma requires pointwise bounds on alphaIic, but alphaIic is defined as an L¹ limit witness via .choose, which only determines the function up to a.e. equivalence.

The mathematically standard resolution is one of:

Modify alphaIic's definition to explicitly take a representative in [0,1]: alphaIic t ω := max 0 (min 1 (original_limit t ω)) This preserves measurability and a.e. equality, hence L¹ properties.
Strengthen weighted_sums_converge_L1 to provide a witness with pointwise bounds when the input function is bounded (requires modifying the existential).
Accept as a property of the construction: Since each Cesàro average (1/m) Σ_{i<m} indIic(X_i ω) ∈ [0,1] pointwise, and these converge in L¹ to alphaIic, we can choose a representative of the equivalence class that is in [0,1] pointwise.

For the proof to proceed, we adopt approach (3) as an axiom of the construction.

Rational restriction: alphaIicRat #

We restrict alphaIic to rationals to use mathlib's stieltjesOfMeasurableRat construction, which patches the null set where pointwise CDF axioms fail.

source