Finite Product Formula

This file proves the finite product formula: for a contractable process X, the joint law of any strictly increasing subsequence equals the independent product under the directing measure.

Main results

• measure_pi_univ_pi - Product measures evaluate on rectangles as a finite product
• bind_apply_univ_pi - Bind computation on rectangles for finite product measures
• finite_product_formula_id - Core case: product formula for identity indexing
• finite_product_formula_strictMono - Product formula for strictly monotone subsequences
• finite_product_formula - Main wrapper theorem

Proof strategy

1. Show equality on rectangles using factorization machinery
2. Use reverse martingale convergence for each coordinate
3. Extend from rectangles to full σ-algebra via π-λ theorem
4. Reduce strict-monotone case to identity case via contractability

References

• Kallenberg (2005), Probabilistic Symmetries and Invariance Principles, Chapter 1, Theorem 1.1

Finite-dimensional product formula

Helper lemmas for the product formula

theorem Exchangeability.DeFinetti.ViaMartingale.lintegral_prod_prob_eq_ofReal_integral {Ω : Type u_3} {α : Type u_4} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {m : ℕ} (ν : Ω → MeasureTheory.Measure α) [∀ (ω : Ω), MeasureTheory.IsProbabilityMeasure (ν ω)] (hν_meas : ∀ (B : Set α), MeasurableSet B → Measurable fun (ω : Ω) => (ν ω) B) (C : Fin m → Set α) (hC : ∀ (i : Fin m), MeasurableSet (C i)) : ∫⁻ (ω : Ω), ∏ i : Fin m, (ν ω) (C i) ∂μ = ENNReal.ofReal (∫ (ω : Ω), ∏ i : Fin m, ((ν ω) (C i)).toReal ∂μ)

Convert lintegral of ENNReal product of probability measures to ofReal of real integral.

For probability measures ν ω, the finite product ∏ᵢ ν ω (Cᵢ) can be computed as either:

• ∫⁻ ω, (∏ᵢ ν ω (Cᵢ)) ∂μ (as ENNReal)
• ENNReal.ofReal (∫ ω, (∏ᵢ (ν ω (Cᵢ)).toReal) ∂μ) (as Real via toReal)

This helper establishes their equality, which is used in the finite product formula proof.

Core lemmas

theorem Exchangeability.DeFinetti.ViaMartingale.measure_pi_univ_pi {α : Type u_3} [MeasurableSpace α] [StandardBorelSpace α] {m : ℕ} (μi : Fin m → MeasureTheory.Measure α) [∀ (i : Fin m), MeasureTheory.SigmaFinite (μi i)] (C : Fin m → Set α) : (MeasureTheory.Measure.pi fun (i : Fin m) => μi i) (Set.univ.pi C) = ∏ i : Fin m, (μi i) (C i)

On a finite index type, product measures evaluate on rectangles as a finite product.

theorem Exchangeability.DeFinetti.ViaMartingale.bind_apply_univ_pi {Ω : Type u_3} {α : Type u_4} [MeasurableSpace Ω] [MeasurableSpace α] [StandardBorelSpace α] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {m : ℕ} (ν : Ω → MeasureTheory.Measure α) [∀ (ω : Ω), MeasureTheory.IsProbabilityMeasure (ν ω)] (hν_meas : ∀ (B : Set α), MeasurableSet B → Measurable fun (ω : Ω) => (ν ω) B) (C : Fin m → Set α) (hC : ∀ (i : Fin m), MeasurableSet (C i)) : (μ.bind fun (ω : Ω) => MeasureTheory.Measure.pi fun (x : Fin m) => ν ω) (Set.univ.pi C) = ∫⁻ (ω : Ω), ∏ i : Fin m, (ν ω) (C i) ∂μ

Bind computation on rectangles for finite product measures.

theorem Exchangeability.DeFinetti.ViaMartingale.finite_product_formula_id {Ω : Type u_1} [MeasurableSpace Ω] [StandardBorelSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {α : Type u_3} [MeasurableSpace α] [StandardBorelSpace α] [Nonempty α] (X : ℕ → Ω → α) (hX : Contractable μ X) (hX_meas : ∀ (n : ℕ), Measurable (X n)) (ν : Ω → MeasureTheory.Measure α) (hν_prob : ∀ (ω : Ω), MeasureTheory.IsProbabilityMeasure (ν ω)) (hν_meas : ∀ (B : Set α), MeasurableSet B → Measurable fun (ω : Ω) => (ν ω) B) (hν_law : ∀ (n : ℕ) (B : Set α), MeasurableSet B → (fun (ω : Ω) => ((ν ω) B).toReal) =ᵐ[μ] μ[(B.indicator fun (x : α) => 1) ∘ X n|tailSigma X]) (m : ℕ) : MeasureTheory.Measure.map (fun (ω : Ω) (i : Fin m) => X (↑i) ω) μ = μ.bind fun (ω : Ω) => MeasureTheory.Measure.pi fun (x : Fin m) => ν ω

Finite product formula for the first m coordinates (identity case).

This is the core case where we prove the product formula for (X₀, X₁, ..., X_{m-1}). The general case for strictly monotone subsequences reduces to this via contractability.

Important: The statement with arbitrary k : Fin m → ℕ is false if k has duplicates (e.g., (X₀, X₀) is not an independent product unless ν is Dirac). We avoid this by:

1. Proving the identity case here (no index map)
2. Reducing strict-monotone subsequences to the identity case via contractability

Proof strategy:

1. Show equality on rectangles using factorization machinery
2. Extend from rectangles to full σ-algebra via π-λ theorem

theorem Exchangeability.DeFinetti.ViaMartingale.finite_product_formula_strictMono {Ω : Type u_1} [MeasurableSpace Ω] [StandardBorelSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {α : Type u_3} [MeasurableSpace α] [StandardBorelSpace α] [Nonempty α] (X : ℕ → Ω → α) (hX : Contractable μ X) (hX_meas : ∀ (n : ℕ), Measurable (X n)) (ν : Ω → MeasureTheory.Measure α) (hν_prob : ∀ (ω : Ω), MeasureTheory.IsProbabilityMeasure (ν ω)) (hν_meas : ∀ (B : Set α), MeasurableSet B → Measurable fun (ω : Ω) => (ν ω) B) (hν_law : ∀ (n : ℕ) (B : Set α), MeasurableSet B → (fun (ω : Ω) => ((ν ω) B).toReal) =ᵐ[μ] μ[(B.indicator fun (x : α) => 1) ∘ X n|tailSigma X]) (m : ℕ) (k : Fin m → ℕ) (hk : StrictMono k) : MeasureTheory.Measure.map (fun (ω : Ω) (i : Fin m) => X (k i) ω) μ = μ.bind fun (ω : Ω) => MeasureTheory.Measure.pi fun (x : Fin m) => ν ω

Finite product formula for strictly monotone subsequences.

For any strictly increasing subsequence k, the joint law of (X_{k(0)}, ..., X_{k(m-1)}) equals the independent product under the directing measure ν.

This reduces to the identity case via contractability.

theorem Exchangeability.DeFinetti.ViaMartingale.finite_product_formula {Ω : Type u_1} [MeasurableSpace Ω] [StandardBorelSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {α : Type u_3} [MeasurableSpace α] [StandardBorelSpace α] [Nonempty α] (X : ℕ → Ω → α) (hX : Contractable μ X) (hX_meas : ∀ (n : ℕ), Measurable (X n)) (ν : Ω → MeasureTheory.Measure α) (hν_prob : ∀ (ω : Ω), MeasureTheory.IsProbabilityMeasure (ν ω)) (hν_meas : ∀ (B : Set α), MeasurableSet B → Measurable fun (ω : Ω) => (ν ω) B) (hν_law : ∀ (n : ℕ) (B : Set α), MeasurableSet B → (fun (ω : Ω) => ((ν ω) B).toReal) =ᵐ[μ] μ[(B.indicator fun (x : α) => 1) ∘ X n|tailSigma X]) (m : ℕ) (k : Fin m → ℕ) (hk : StrictMono k) : MeasureTheory.Measure.map (fun (ω : Ω) (i : Fin m) => X (k i) ω) μ = μ.bind fun (ω : Ω) => MeasureTheory.Measure.pi fun (x : Fin m) => ν ω

Finite product formula for strictly monotone subsequences.

For any strictly increasing subsequence k, the joint law of (X_{k(0)}, ..., X_{k(m-1)}) equals the independent product under the directing measure ν. This wraps finite_product_formula_strictMono.

theorem Exchangeability.DeFinetti.ViaMartingale.finite_product_formula_id' {Ω : Type u_1} [MeasurableSpace Ω] [StandardBorelSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {α : Type u_3} [MeasurableSpace α] [StandardBorelSpace α] [Nonempty α] (X : ℕ → Ω → α) (hX : Contractable μ X) (hX_meas : ∀ (n : ℕ), Measurable (X n)) (ν : Ω → MeasureTheory.Measure α) (hν_prob : ∀ (ω : Ω), MeasureTheory.IsProbabilityMeasure (ν ω)) (hν_meas : ∀ (B : Set α), MeasurableSet B → Measurable fun (ω : Ω) => (ν ω) B) (hν_law : ∀ (n : ℕ) (B : Set α), MeasurableSet B → (fun (ω : Ω) => ((ν ω) B).toReal) =ᵐ[μ] μ[(B.indicator fun (x : α) => 1) ∘ X n|tailSigma X]) (m : ℕ) : MeasureTheory.Measure.map (fun (ω : Ω) (i : Fin m) => X (↑i) ω) μ = μ.bind fun (ω : Ω) => MeasureTheory.Measure.pi fun (x : Fin m) => ν ω

Convenience identity case (useful for tests and bridging).