Indicator Algebra for Finite Cylinders

This file contains the indProd definition and related lemmas for working with products of indicator functions on finite cylinders.

Main definitions

• indProd X r C - Product of indicators: ∏ᵢ 𝟙_{X_i ∈ C_i}

Main results

• indProd_as_indicator - indProd equals indicator of intersection
• indProd_eq_firstRCylinder_indicator - Connection to firstRCylinder
• indProd_integrable - Integrability under finite measures

These are extracted from ViaMartingale.lean to enable modular imports.

Product of indicators for finite cylinders

noncomputable def Exchangeability.DeFinetti.ViaMartingale.indProd {Ω : Type u_1} {α : Type u_2} (X : ℕ → Ω → α) (r : ℕ) (C : Fin r → Set α) : Ω → ℝ

Product of indicator functions for a finite cylinder on the first r coordinates.

Equations

• Exchangeability.DeFinetti.ViaMartingale.indProd X r C ω = ∏ i : Fin r, (C i).indicator (fun (x : α) => 1) (X (↑i) ω)

theorem Exchangeability.DeFinetti.ViaMartingale.indProd_as_indicator {Ω : Type u_1} {α : Type u_2} (X : ℕ → Ω → α) (r : ℕ) (C : Fin r → Set α) : indProd X r C = {ω : Ω | ∀ (i : Fin r), X (↑i) ω ∈ C i}.indicator fun (x : Ω) => 1

theorem Exchangeability.DeFinetti.ViaMartingale.indProd_eq_firstRCylinder_indicator {Ω : Type u_1} {α : Type u_2} (X : ℕ → Ω → α) (r : ℕ) (C : Fin r → Set α) : indProd X r C = (PathSpace.firstRCylinder X r C).indicator fun (x : Ω) => 1

Connection between indProd and firstRCylinder: the product indicator equals the indicator of the first-r cylinder.

theorem Exchangeability.DeFinetti.ViaMartingale.indProd_integrable {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] (X : ℕ → Ω → α) (r : ℕ) (C : Fin r → Set α) (hX : ∀ (n : ℕ), Measurable (X n)) (hC : ∀ (i : Fin r), MeasurableSet (C i)) : MeasureTheory.Integrable (indProd X r C) μ

Basic integrability: indProd is an indicator of a measurable set, hence integrable under a finite measure.

@[simp]

theorem Exchangeability.DeFinetti.ViaMartingale.indProd_zero {Ω : Type u_1} {α : Type u_2} (X : ℕ → Ω → α) (C : Fin 0 → Set α) : indProd X 0 C = fun (x : Ω) => 1

indProd of zero coordinates is identically 1.