Block Cesàro Average Definition

This file defines block Cesàro averages used in Kallenberg's L² approach to de Finetti's theorem.

Main definitions

• blockAvg f X m n ω: The block average (1/n) ∑{k=0}^{n-1} f(X{m+k}(ω))

Main results

• blockAvg_measurable: Block averages are measurable
• blockAvg_abs_le_one: Block averages of bounded functions are bounded

References

• Kallenberg (2005), Probabilistic Symmetries and Invariance Principles, Chapter 1

noncomputable def Exchangeability.DeFinetti.ViaL2.blockAvg {Ω : Type u_1} {α : Type u_2} (f : α → ℝ) (X : ℕ → Ω → α) (m n : ℕ) (ω : Ω) : ℝ

Block Cesàro average of a function along a sequence.

For a function f : α → ℝ and sequence X : ℕ → Ω → α, the block average starting at index m with length n is:

A_{m,n}(ω) := (1/n) ∑{k=0}^{n-1} f(X{m+k}(ω))

This is the building block for Kallenberg's L² convergence proof.

Equations

• Exchangeability.DeFinetti.ViaL2.blockAvg f X m n ω = (↑n)⁻¹ * ∑ k ∈ Finset.range n, f (X (m + k) ω)

theorem Exchangeability.DeFinetti.ViaL2.blockAvg_measurable {Ω : Type u_3} {α : Type u_4} [MeasurableSpace Ω] [MeasurableSpace α] (f : α → ℝ) (X : ℕ → Ω → α) (hf : Measurable f) (hX : ∀ (i : ℕ), Measurable (X i)) (m n : ℕ) : Measurable fun (ω : Ω) => blockAvg f X m n ω

theorem Exchangeability.DeFinetti.ViaL2.blockAvg_abs_le_one {Ω : Type u_3} {α : Type u_4} [MeasurableSpace Ω] (f : α → ℝ) (X : ℕ → Ω → α) (hf_bdd : ∀ (x : α), |f x| ≤ 1) (m n : ℕ) (ω : Ω) : |blockAvg f X m n ω| ≤ 1

theorem Exchangeability.DeFinetti.ViaL2.blockAvg_memLp_two_of_abs_le_one {Ω : Type u_3} {α : Type u_4} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (f : α → ℝ) (X : ℕ → Ω → α) (hf_meas : Measurable f) (hX_meas : ∀ (i : ℕ), Measurable (X i)) (hf_bdd : ∀ (x : α), |f x| ≤ 1) (m n : ℕ) : MeasureTheory.MemLp (blockAvg f X m n) 2 μ

blockAvg f X m n is in L²(μ) whenever f is bounded by 1, on any probability space. Combines blockAvg_measurable + blockAvg_abs_le_one + MemLp.of_bound.