Measurability of Product Measure Kernels

This file contains technical lemmas about measurability of product measure kernels. These lemmas support the de Finetti theorem proof machinery but are general-purpose results about measure theory on product spaces.

Main results

• measurable_prod_ennreal: Products of measurable ENNReal functions are measurable
• rectangles_isPiSystem: Measurable rectangles form a π-system
• rectangles_generate_pi_sigma: The product σ-algebra equals the σ-algebra generated by rectangles
• measurable_measure_pi: Measurability of product measure kernels ω ↦ ∏ᵢ ν ω
• aemeasurable_measure_pi: AE-measurability version (implies measurable version)

Implementation notes

These lemmas were extracted from CommonEnding.lean to break circular dependencies between ConditionallyIID.lean and CommonEnding.lean.

The key technique is π-system induction: proving measurability on rectangles (a π-system) and extending to all measurable sets via the π-λ theorem.

References

• Kallenberg (2005), Probabilistic Symmetries and Invariance Principles

Preliminary lemmas

theorem measurable_prod_ennreal {ι : Type u_3} [Fintype ι] {Ω : Type u_4} [MeasurableSpace Ω] (f : ι → Ω → ENNReal) (hf : ∀ (i : ι), Measurable (f i)) : Measurable fun (ω : Ω) => ∏ i : ι, f i ω

The product of finitely many measurable ENNReal-valued functions is measurable.

This is a wrapper around Finset.measurable_prod specialized to ENNReal.

theorem univ_pi_eq_setOf_forall {ι : Type u_3} {α : Type u_4} (B : ι → Set α) : Set.univ.pi B = {x : ι → α | ∀ (i : ι), x i ∈ B i}

Rewrite Set.univ.pi B as a setOf comprehension.

This is a convenience lemma for working with measurable rectangles in product spaces. The two forms are definitionally equal but different proof strategies prefer different forms:

• Set.univ.pi B is convenient for applying Measure.pi_pi
• {x | ∀ i, x i ∈ B i} is convenient for membership reasoning

π-system structure of rectangles

theorem rectangles_isPiSystem {m : ℕ} {α : Type u_3} [MeasurableSpace α] : IsPiSystem {S : Set (Fin m → α) | ∃ (B : Fin m → Set α), (∀ (i : Fin m), MeasurableSet (B i)) ∧ S = {x : Fin m → α | ∀ (i : Fin m), x i ∈ B i}}

Measurable rectangles form a π-system for the product σ-algebra.

A rectangle in (Fin m → α) is a set of the form {x | ∀ i, x i ∈ B i} where each B i is measurable. The collection of such rectangles is closed under finite intersections.

theorem rectangles_generate_pi_sigma {m : ℕ} {α : Type u_3} [MeasurableSpace α] : inferInstance = MeasurableSpace.generateFrom {S : Set (Fin m → α) | ∃ (B : Fin m → Set α), (∀ (i : Fin m), MeasurableSet (B i)) ∧ S = {x : Fin m → α | ∀ (i : Fin m), x i ∈ B i}}

The product σ-algebra on (Fin m → α) is generated by measurable rectangles.

This is a fundamental result in product measure theory: the σ-algebra on a finite product equals the σ-algebra generated by measurable rectangles.

Proof strategy:

• The product σ-algebra is the smallest σ-algebra making all projections measurable
• A set is in this σ-algebra iff it's in the σ-algebra generated by cylinder sets
• Cylinder sets are finite intersections of preimages of projections
• These are exactly the rectangles

In mathlib, this follows from generateFrom_pi which establishes the equivalence between the product σ-algebra and the σ-algebra generated by rectangles.

Measurability of product measure kernels

theorem measurable_measure_pi {Ω : Type u_3} {α : Type u_4} [MeasurableSpace Ω] [MeasurableSpace α] {m : ℕ} (ν : Ω → MeasureTheory.Measure α) (hν_prob : ∀ (ω : Ω), MeasureTheory.IsProbabilityMeasure (ν ω)) (hν_meas : ∀ (s : Set α), MeasurableSet s → Measurable fun (ω : Ω) => (ν ω) s) : Measurable fun (ω : Ω) => MeasureTheory.Measure.pi fun (x : Fin m) => ν ω

The product measure kernel ω ↦ Measure.pi (fun _ => ν ω) is measurable.

Given a measurable family of probability measures ν : Ω → Measure α, the product kernel ω ↦ ∏ᵢ ν ω (where i ranges over Fin m) is measurable as a measure-valued map.

Proof strategy: Use π-system induction on rectangles:

1. Rectangles generate the product σ-algebra (rectangles_generate_pi_sigma)
2. Rectangles form a π-system (rectangles_isPiSystem)
3. On rectangles, the product measure of {x | ∀ i, x i ∈ B i} equals ∏ᵢ ν ω (B i), which is measurable in ω by measurable_prod_ennreal
4. By the π-λ theorem (Measurable.measure_of_isPiSystem_of_isProbabilityMeasure), measurability on the generating π-system extends to all measurable sets

This is a key lemma for proving the ConditionallyIID property in de Finetti's theorem.

Mathematical content: This shows that finite products of probability kernels yield measurable kernels, which is essential for disintegration theory and conditional independence.

theorem aemeasurable_measure_pi {Ω : Type u_3} {α : Type u_4} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {m : ℕ} (ν : Ω → MeasureTheory.Measure α) (hν_prob : ∀ (ω : Ω), MeasureTheory.IsProbabilityMeasure (ν ω)) (hν_meas : ∀ (s : Set α), MeasurableSet s → Measurable fun (ω : Ω) => (ν ω) s) : AEMeasurable (fun (ω : Ω) => MeasureTheory.Measure.pi fun (x : Fin m) => ν ω) μ

AE-measurable version of measurable_measure_pi.

This is the version originally proved in CommonEnding.lean. The measurable version measurable_measure_pi is stronger and generally more useful, but this AE version is kept for compatibility.

Note: The hypothesis only requires measurability for measurable sets, matching what Kernel.measurable_coe provides. This is the standard requirement in measure theory.

Triple product rectangles

These lemmas support σ-algebra arguments on triple products of the form (Fin r → α) × α × (Fin k → α), which arise in the contractable triple pushforward lemma.

def TripleRectangles (r k : ℕ) (α : Type u_3) [MeasurableSpace α] : Set (Set ((Fin r → α) × α × (Fin k → α)))

Definition of triple rectangles: sets of the form (pi A) × B × (pi C).

Equations

• One or more equations did not get rendered due to their size.

theorem tripleRectangles_isPiSystem {r k : ℕ} {α : Type u_3} [MeasurableSpace α] : IsPiSystem (TripleRectangles r k α)

Triple rectangles form a π-system.

The intersection of two triple rectangles is another triple rectangle, obtained by intersecting each component.

theorem tripleRectangles_generate {r k : ℕ} {α : Type u_3} [MeasurableSpace α] : inferInstance = MeasurableSpace.generateFrom (TripleRectangles r k α)

The product σ-algebra on (Fin r → α) × α × (Fin k → α) is generated by triple rectangles.

This is a key structural lemma for π-λ induction on triple products. It shows that to prove equality of measures on the triple product, it suffices to prove equality on triple rectangles (provided one shows they form a π-system).