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.

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.norm_indicator_one_le {α : Type u_1} (S : Set α) (x : α) : ‖S.indicator (fun (x : α) => 1) x‖ ≤ 1

Conditional Distribution Uniqueness

Conditional Independence from Distributional Equality