Cesàro L¹ Convergence: cesaro_to_condexp_L1 #
L¹ version of cesaro_to_condexp_L2 (from CesaroConvergence/L2.lean), derived
by L² → L¹ on a probability space (Cauchy–Schwarz). This is the convergence form
consumed by AlphaConvergence.lean.
Main results #
cesaro_to_condexp_L1: L¹ convergence of block Cesàro averages to the tail conditional expectation
References #
- Kallenberg (2005), Probabilistic Symmetries and Invariance Principles, Chapter 1, "Second proof of Theorem 1.1"
theorem
Exchangeability.DeFinetti.ViaL2.cesaro_to_condexp_L1
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure μ]
{X : ℕ → Ω → ℝ}
(hX_contract : Contractable μ X)
(hX_meas : ∀ (i : ℕ), Measurable (X i))
(f : ℝ → ℝ)
(hf_meas : Measurable f)
(hf_bdd : ∀ (x : ℝ), |f x| ≤ 1)
(ε : ℝ)
: