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

• 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

π-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 Finset.measurable_prod
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.

measurable_measure_pi is the stronger result; this AE form is what the Measure.bind_apply consumers actually want (see CommonEnding.conditional_iid_from_directing_measure, ViaMartingale/FiniteProduct.bind_apply_univ_pi, and BridgeProperty.indicator_product_bridge_contractable). Not a compatibility shim — these call sites need the AE form directly.

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