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

• cylinderFunction: A function on path space depending only on finitely many coordinates
• productCylinder: Product of functions evaluated at different coordinates
• productCylinderLp: Lp representative for bounded product cylinders
• shiftedCylinder: Cylinder function composed with shift^n

Main Results

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

def cylinderFunction {α : Type u_1} {m : ℕ} (φ : (Fin m → α) → ℝ) : (ℕ → α) → ℝ

Cylinder function: a function on path space depending only on finitely many coordinates. For simplicity, we take the first m coordinates.

Equations

• cylinderFunction φ ω = φ fun (k : Fin m) => ω ↑k

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 productCylinder_eq_cylinder {α : Type u_1} {m : ℕ} (fs : Fin m → α → ℝ) : productCylinder fs = cylinderFunction fun (coords : Fin m → α) => ∏ k : Fin m, fs k (coords k)

theorem measurable_cylinderFunction {α : Type u_1} [MeasurableSpace α] {m : ℕ} {φ : (Fin m → α) → ℝ} (_hφ : Measurable φ) : Measurable (cylinderFunction φ)

Measurability of cylinder functions.

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 ω

def shiftedCylinder {α : Type u_1} (n : ℕ) (F : (ℕ → α) → ℝ) : (ℕ → α) → ℝ

The shifted cylinder function: F ∘ shift^n.

Equations

• shiftedCylinder n F ω = F (Exchangeability.PathSpace.shift^[n] ω)