BlockAverages — Long vs. tail L² bound

l2_bound_long_vs_tail: the second L² Cauchy bound, comparing a long window average to a tail-shifted average. Together with l2_bound_two_windows_uniform (BlockAverages/TwoWindows.lean) this drives the Cauchy property of block averages used in CesaroConvergence/Cauchy.lean.

Also exposes get_covariance_constant, the helper that packages the covariance structure of f ∘ X into a single shared bound Cf passed to both l2_bound_two_windows_uniform and this file's main lemma.

theorem Exchangeability.DeFinetti.ViaL2.get_covariance_constant {Ω : 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 : ∃ (M : ℝ), ∀ (x : ℝ), |f x| ≤ M) : ∃ (Cf : ℝ) (mf : ℝ) (σSqf : ℝ) (ρf : ℝ), Cf = 2 * σSqf * (1 - ρf) ∧ 0 ≤ Cf ∧ (∀ (n : ℕ), ∫ (ω : Ω), f (X n ω) ∂μ = mf) ∧ (∀ (n : ℕ), ∫ (ω : Ω), (f (X n ω) - mf) ^ 2 ∂μ = σSqf) ∧ (∀ (n m : ℕ), n ≠ m → ∫ (ω : Ω), (f (X n ω) - mf) * (f (X m ω) - mf) ∂μ = σSqf * ρf) ∧ 0 ≤ σSqf ∧ -1 ≤ ρf ∧ ρf ≤ 1

Compute the L² contractability constant for f ∘ X.

This helper extracts the common covariance structure computation needed by both l2_bound_two_windows_uniform and l2_bound_long_vs_tail.

Returns Cf = 2σ²(1-ρ) where (mf, σ², ρ) is the covariance structure of f ∘ X obtained from contractable_covariance_structure.

Design rationale: Computing the covariance structure once and passing it to both bound lemmas ensures they use the same constant, avoiding the need to prove equality of opaque existential witnesses.

theorem Exchangeability.DeFinetti.ViaL2.l2_bound_long_vs_tail {Ω : 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 : ℕ) (hk : 0 < k) (hkm : k ≤ m) : ∫ (ω : Ω), (1 / ↑m * ∑ i : Fin m, f (X (n + ↑i + 1) ω) - 1 / ↑k * ∑ i : Fin k, f (X (n + (m - k) + ↑i + 1) ω)) ^ 2 ∂μ ≤ Cf / ↑k