Cylinder Functions for de Finetti's Theorem

This file defines cylinder functions on infinite path spaces and proves their measurability and boundedness properties.

Main Definitions

• productCylinder: Product of functions evaluated at different coordinates
• productCylinderLp: Lp representative for bounded product cylinders

Main Results

• measurable_productCylinder: Product cylinders are measurable
• productCylinder_bounded: Product cylinders are bounded
• productCylinder_memLp: Product cylinders are in L²

def productCylinder {α : Type u_1} {m : ℕ} (fs : Fin m → α → ℝ) : (ℕ → α) → ℝ

Product cylinder: ∏_{k < m} fₖ(ω k).

Equations

• productCylinder fs ω = ∏ k : Fin m, fs k (ω ↑k)

theorem measurable_productCylinder {α : Type u_1} [MeasurableSpace α] {m : ℕ} {fs : Fin m → α → ℝ} (hmeas : ∀ (k : Fin m), Measurable (fs k)) : Measurable (productCylinder fs)

Measurability of product cylinders.

theorem productCylinder_bounded {α : Type u_1} {m : ℕ} {fs : Fin m → α → ℝ} (hbd : ∀ (k : Fin m), ∃ (C : ℝ), ∀ (x : α), |fs k x| ≤ C) : ∃ (C : ℝ), ∀ (ω : ℕ → α), |productCylinder fs ω| ≤ C

Boundedness of product cylinders.

theorem productCylinder_memLp {α : Type u_1} [MeasurableSpace α] {m : ℕ} (fs : Fin m → α → ℝ) (hmeas : ∀ (k : Fin m), Measurable (fs k)) (hbd : ∀ (k : Fin m), ∃ (C : ℝ), ∀ (x : α), |fs k x| ≤ C) {μ : MeasureTheory.Measure (ℕ → α)} [MeasureTheory.IsProbabilityMeasure μ] : MeasureTheory.MemLp (productCylinder fs) 2 μ

Membership of product cylinders in L².

noncomputable def productCylinderLp {α : Type u_1} [MeasurableSpace α] {m : ℕ} (fs : Fin m → α → ℝ) (hmeas : ∀ (k : Fin m), Measurable (fs k)) (hbd : ∀ (k : Fin m), ∃ (C : ℝ), ∀ (x : α), |fs k x| ≤ C) {μ : MeasureTheory.Measure (ℕ → α)} [MeasureTheory.IsProbabilityMeasure μ] : ↥(MeasureTheory.Lp ℝ 2 μ)

Lp representative associated to a bounded product cylinder.

Equations

• productCylinderLp fs hmeas hbd = MeasureTheory.MemLp.toLp (productCylinder fs) ⋯

theorem productCylinderLp_ae_eq {α : Type u_1} [MeasurableSpace α] {m : ℕ} (fs : Fin m → α → ℝ) (hmeas : ∀ (k : Fin m), Measurable (fs k)) (hbd : ∀ (k : Fin m), ∃ (C : ℝ), ∀ (x : α), |fs k x| ≤ C) {μ : MeasureTheory.Measure (ℕ → α)} [MeasureTheory.IsProbabilityMeasure μ] : ∀ᵐ (ω : ℕ → α) ∂μ, ↑↑(productCylinderLp fs hmeas hbd) ω = productCylinder fs ω