Local Infrastructure Lemmas for ViaMartingale

This file contains helper lemmas that unblock the martingale approach proof by providing targeted results that should eventually be contributed to mathlib. Each is marked with its intended mathlib home.

Main sections

• PiFiniteProjections - σ-algebra structure of infinite product spaces
• ProbabilityMeasureHelpers - Integrability and bounds on probability spaces
• CondDistribUniqueness - Conditional distribution uniqueness under factorization
• ConditionalIndependence - Conditional independence projection lemmas

These lemmas are extracted from ViaMartingale.lean to enable modular imports.

Pi-system and Finite Projections

theorem Exchangeability.DeFinetti.ViaMartingale.measurableSpace_pi_nat_le_iSup_fin {α : Type u_1} [MeasurableSpace α] : inferInstance ≤ ⨆ (k : ℕ), MeasurableSpace.comap (fun (f : ℕ → α) (i : Fin k) => f ↑i) inferInstance

The σ-algebra on ℕ → α is contained in the supremum of σ-algebras pulled back by finite-coordinate projections. This is the ≤ direction we need for filtration arguments.

Probability Measure Helpers

theorem Exchangeability.DeFinetti.ViaMartingale.integrable_of_bounded_on_prob {α : Type u_1} [MeasurableSpace α] {ν : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure ν] {h : α → ℝ} (hmeas : Measurable h) {C : ℝ} (hB : ∀ᵐ (x : α) ∂ν, ‖h x‖ ≤ C) : MeasureTheory.Integrable h ν

[Mathlib candidate:MeasureTheory.Integral.Bochner]

On a probability space, a bounded measurable function is integrable.

This is a standard fact: if ‖f‖ ≤ C a.e. on a probability measure, then ∫ ‖f‖ ≤ C·μ(univ) = C < ∞, so f is integrable.

Proof strategy: Use mathlib's Integrable.of_mem_Icc for functions bounded in an interval.

theorem Exchangeability.DeFinetti.ViaMartingale.ae_norm_condExp_le_of_bound {Ω : Type u_1} {m m₀ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {f : Ω → ℝ} {C : ℝ} (hC0 : 0 ≤ C) (hbound : ∀ᵐ (ω : Ω) ∂μ, |f ω| ≤ C) : ∀ᵐ (ω : Ω) ∂μ, |μ[f|m] ω| ≤ C

If |f| ≤ C a.e., then |E[f | m]| ≤ C a.e.

This is essentially MeasureTheory.ae_bdd_condExp_of_ae_bdd from mathlib, re-exported here for convenience with a slightly different signature.

Mathlib already proves this result for ℝ≥0 bounds.

theorem Exchangeability.DeFinetti.ViaMartingale.norm_indicator_one_le {α : Type u_1} (S : Set α) (x : α) : ‖S.indicator (fun (x : α) => 1) x‖ ≤ 1

Indicator functions Set.indicator S (1 : _ → ℝ) are bounded by 1 in norm.

Conditional Distribution Uniqueness

theorem Exchangeability.DeFinetti.ViaMartingale.condDistrib_factor_indicator_agree {Ω : Type u_1} {α : Type u_2} {β : Type u_3} [MeasurableSpace Ω] [StandardBorelSpace Ω] [MeasurableSpace α] [StandardBorelSpace α] [Nonempty α] [MeasurableSpace β] [Nonempty β] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (ξ : Ω → α) (η ζ : Ω → β) (_hξ : Measurable ξ) (_hη : Measurable η) (hζ : Measurable ζ) (_h_law : MeasureTheory.Measure.map (fun (ω : Ω) => (ξ ω, η ω)) μ = MeasureTheory.Measure.map (fun (ω : Ω) => (ξ ω, ζ ω)) μ) (h_le : MeasurableSpace.comap η inferInstance ≤ MeasurableSpace.comap ζ inferInstance) {B : Set α} (_hB : MeasurableSet B) : μ[μ[(B.indicator fun (x : α) => 1) ∘ ξ|MeasurableSpace.comap ζ inferInstance]|MeasurableSpace.comap η inferInstance] =ᵐ[μ] μ[(B.indicator fun (x : α) => 1) ∘ ξ|MeasurableSpace.comap η inferInstance]

[Mathlib candidate:Probability.Kernel.CondDistrib]

Indicator version of conditional distribution uniqueness under factorization.

If the joint laws (ξ, η) and (ξ, ζ) agree, and η factors through ζ (i.e., η = g ∘ ζ for some measurable g), then the conditional expectations of indicator functions agree almost everywhere.

This is a special case of the general uniqueness of regular conditional distributions. The full version (for all bounded measurable functions, not just indicators) should be contributed to mathlib as condDistrib_unique_of_pair_law_and_factor.

Proof strategy:

1. Use condExp_ae_eq_integral_condDistrib to express both sides as kernel integrals
2. From h_law and h_factor, show the conditional distributions agree a.e.
3. Conclude by transitivity of a.e. equality

This leverages the uniqueness of regular conditional distributions on standard Borel spaces: if two probability kernels disintegrate the same joint measure, they agree a.e.

Conditional Independence from Distributional Equality

theorem Exchangeability.DeFinetti.ViaMartingale.condExp_projection_of_condIndep {Ω : Type u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_4} [MeasurableSpace Ω] [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (Y : Ω → α) (Z : Ω → β) (W : Ω → γ) (hY : Measurable Y) (hZ : Measurable Z) (hW : Measurable W) (h_indep : CondIndep μ Y Z W) {B : Set α} (hB : MeasurableSet B) : μ[(B.indicator fun (x : α) => 1) ∘ Y|MeasurableSpace.comap (fun (ω : Ω) => (Z ω, W ω)) inferInstance] =ᵐ[μ] μ[(B.indicator fun (x : α) => 1) ∘ Y|MeasurableSpace.comap W inferInstance]

[Mathlib candidate:Probability.Independence.Conditional]

Conditional expectation projection property: If Y and Z are conditionally independent given W, then conditioning on (Z, W) gives the same result as conditioning on W alone for functions of Y.

Mathematical statement: If Y ⊥⊥_W Z, then E[f(Y) | σ(Z, W)] = E[f(Y) | σ(W)] a.e.

Proof strategy:

1. Use conditional independence definition for indicators
2. Extend to simple functions, then to L¹ functions
3. Apply uniqueness of conditional expectation

theorem Exchangeability.DeFinetti.ViaMartingale.pair_law_ZW_of_triple_law {Ω : Type u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_4} [MeasurableSpace Ω] [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] {μ : MeasureTheory.Measure Ω} (Y : Ω → α) (Z : Ω → β) (W W' : Ω → γ) (hY : Measurable Y) (hZ : Measurable Z) (hW : Measurable W) (hW' : Measurable W') (h_triple : MeasureTheory.Measure.map (fun (ω : Ω) => (Y ω, Z ω, W ω)) μ = MeasureTheory.Measure.map (fun (ω : Ω) => (Y ω, Z ω, W' ω)) μ) : MeasureTheory.Measure.map (fun (ω : Ω) => (Z ω, W ω)) μ = MeasureTheory.Measure.map (fun (ω : Ω) => (Z ω, W' ω)) μ

Helper: Pair law (Z,W) equality from triple law. The marginal distribution (Z,W) coincides with (Z,W') when (Y,Z,W) =^d (Y,Z,W').

theorem Exchangeability.DeFinetti.ViaMartingale.pair_law_YW_of_triple_law {Ω : Type u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_4} [MeasurableSpace Ω] [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] {μ : MeasureTheory.Measure Ω} (Y : Ω → α) (Z : Ω → β) (W W' : Ω → γ) (hY : Measurable Y) (hZ : Measurable Z) (hW : Measurable W) (hW' : Measurable W') (h_triple : MeasureTheory.Measure.map (fun (ω : Ω) => (Y ω, Z ω, W ω)) μ = MeasureTheory.Measure.map (fun (ω : Ω) => (Y ω, Z ω, W' ω)) μ) : MeasureTheory.Measure.map (fun (ω : Ω) => (Y ω, W ω)) μ = MeasureTheory.Measure.map (fun (ω : Ω) => (Y ω, W' ω)) μ

Helper: Pair law (Y,W) equality from triple law. The marginal distribution (Y,W) coincides with (Y,W') when (Y,Z,W) =^d (Y,Z,W').