BlockAverages — Two-window L² bound #
l2_bound_two_windows_uniform: L² distance between block averages over two
windows of the same length is bounded by a uniform constant. Uses the
covariance structure from BlockAverages/Covariance.lean.
theorem
Exchangeability.DeFinetti.ViaL2.l2_bound_two_windows_uniform
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure μ]
(X : ℕ → Ω → ℝ)
(hX_meas : ∀ (i : ℕ), Measurable (X i))
(f : ℝ → ℝ)
(hf_meas : Measurable f)
(hf_bdd : ∃ (M : ℝ), ∀ (x : ℝ), |f x| ≤ M)
(Cf mf σSqf ρf : ℝ)
(hCf_def : Cf = 2 * σSqf * (1 - ρf))
(hmean : ∀ (n : ℕ), ∫ (ω : Ω), f (X n ω) ∂μ = mf)
(hvar : ∀ (n : ℕ), ∫ (ω : Ω), (f (X n ω) - mf) ^ 2 ∂μ = σSqf)
(hcov : ∀ (n m : ℕ), n ≠ m → ∫ (ω : Ω), (f (X n ω) - mf) * (f (X m ω) - mf) ∂μ = σSqf * ρf)
(hσSq_nonneg : 0 ≤ σSqf)
(hρ_bd : -1 ≤ ρf ∧ ρf ≤ 1)
(n m k : ℕ)
: