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
• indProd_mul - Product formula for indProd

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

Product of indicators for finite cylinders

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.

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

indProd is strongly measurable when coordinates and sets are measurable.

theorem Exchangeability.DeFinetti.ViaMartingale.indProd_nonneg_le_one {Ω : Type u_1} {α : Type u_2} (X : ℕ → Ω → α) (r : ℕ) (C : Fin r → Set α) (ω : Ω) : 0 ≤ indProd X r C ω ∧ indProd X r C ω ≤ 1

indProd takes values in [0,1].

@[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.

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

indProd on the universal sets is identically 1.

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

indProd is measurable when coordinates are measurable.

theorem Exchangeability.DeFinetti.ViaMartingale.indProd_mul {Ω : Type u_1} {α : Type u_2} (X : ℕ → Ω → α) {r : ℕ} {C D : Fin r → Set α} (ω : Ω) : indProd X r C ω * indProd X r D ω = indProd X r (fun (i : Fin r) => C i ∩ D i) ω

indProd product equals multiplication of indProds.

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

indProd on intersection via firstRCylinder.