Bridge Property: Product Formula for Indicators

This file provides the bridge property used by CommonEnding to complete the de Finetti proof. It converts the measure equality from ViaMartingale's finite_product_formula to the integral equality form needed by CommonEnding.complete_from_directing_measure.

Main results

• indicator_product_bridge_strictMono: Bridge property for strictly monotone selections
• indicator_product_bridge: Bridge property for injective selections (main result)

Architecture

This is shared infrastructure used by both:

• ViaL2: via MoreL2Helpers.directing_measure_bridge
• ViaMartingale: directly via finite_product_formula

The proof uses:

1. ViaMartingale's finite_product_formula for the measure equality
2. Conversion from measure equality to integral equality on rectangles
3. Extension from strictly monotone to injective via permutation

References

• Kallenberg (2005), Probabilistic Symmetries and Invariance Principles, Theorem 1.1 (pages 26-28)

Converting measure equality to integral equality

theorem Exchangeability.DeFinetti.measure_eq_implies_lintegral_prod_eq {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (ν : Ω → MeasureTheory.Measure α) [∀ (ω : Ω), MeasureTheory.IsProbabilityMeasure (ν ω)] (hν_meas : ∀ (B : Set α), MeasurableSet B → Measurable fun (ω : Ω) => (ν ω) B) (X : ℕ → Ω → α) (hX_meas : ∀ (n : ℕ), Measurable (X n)) {m : ℕ} (k : Fin m → ℕ) (h_measure_eq : MeasureTheory.Measure.map (fun (ω : Ω) (i : Fin m) => X (k i) ω) μ = μ.bind fun (ω : Ω) => MeasureTheory.Measure.pi fun (x : Fin m) => ν ω) (B : Fin m → Set α) (hB : ∀ (i : Fin m), MeasurableSet (B i)) : ∫⁻ (ω : Ω), ∏ i : Fin m, ENNReal.ofReal ((B i).indicator (fun (x : α) => 1) (X (k i) ω)) ∂μ = ∫⁻ (ω : Ω), ∏ i : Fin m, (ν ω) (B i) ∂μ

Convert measure equality on rectangles to integral equality for products of indicators.

This is the key bridge between ViaMartingale's measure-theoretic formulation and CommonEnding's integral formulation.

Given Measure.map (fun ω => fun i => X (k i) ω) μ = μ.bind (fun ω => Measure.pi ν), applying both sides to the rectangle ∏ᵢ Bᵢ and using:

• LHS: μ (preimage) = ∫⁻ ∏ᵢ 1_{Bᵢ}(X (k i) ω) ∂μ
• RHS: ∫⁻ (Measure.pi ν)(rectangle) ∂μ = ∫⁻ ∏ᵢ ν ω (Bᵢ) ∂μ

gives the desired integral equality.

theorem Exchangeability.DeFinetti.indicator_product_bridge_strictMono {Ω : Type u_1} [MeasurableSpace Ω] [StandardBorelSpace Ω] {α : Type u_3} [MeasurableSpace α] [StandardBorelSpace α] [Nonempty α] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (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|ViaMartingale.tailSigma X]) {m : ℕ} (k : Fin m → ℕ) (hk : StrictMono k) (B : Fin m → Set α) (hB : ∀ (i : Fin m), MeasurableSet (B i)) : ∫⁻ (ω : Ω), ∏ i : Fin m, ENNReal.ofReal ((B i).indicator (fun (x : α) => 1) (X (k i) ω)) ∂μ = ∫⁻ (ω : Ω), ∏ i : Fin m, (ν ω) (B i) ∂μ

Bridge property for strictly monotone selections.

This converts ViaMartingale's finite_product_formula to the integral form.

theorem Exchangeability.DeFinetti.indicator_product_bridge {Ω : Type u_1} [MeasurableSpace Ω] [StandardBorelSpace Ω] {α : Type u_3} [MeasurableSpace α] [StandardBorelSpace α] [Nonempty α] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (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|ViaMartingale.tailSigma X]) {m : ℕ} (k : Fin m → ℕ) (hk : Function.Injective k) (B : Fin m → Set α) (hB : ∀ (i : Fin m), MeasurableSet (B i)) : ∫⁻ (ω : Ω), ∏ i : Fin m, ENNReal.ofReal ((B i).indicator (fun (x : α) => 1) (X (k i) ω)) ∂μ = ∫⁻ (ω : Ω), ∏ i : Fin m, (ν ω) (B i) ∂μ

Bridge property for injective selections.

For any injective k : Fin m → ℕ, the integral of the product of indicators equals the integral of the product of directing measure evaluations.

This is the main result used by CommonEnding.complete_from_directing_measure.