Centered Variable Infrastructure for L² Proofs

This file provides infrastructure for working with centered random variables in the context of exchangeable/contractable sequences. The key result is that centering preserves the uniform covariance structure needed for L² convergence proofs.

Main results

• centered_uniform_covariance: Centered variables from a contractable sequence have uniform variance and covariance structure
• centered_variable_bounded: Centered variables from bounded functions are bounded
• correlation_coefficient_bounded: Correlation coefficient is bounded by 1 via Cauchy-Schwarz

References

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

theorem Exchangeability.Probability.CenteredVariables.centered_uniform_covariance {Ω : 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) (m : ℝ) (hm_def : m = ∫ (ω : Ω), f (X 0 ω) ∂μ) (Z : ℕ → Ω → ℝ) (hZ_def : ∀ (i : ℕ) (ω : Ω), Z i ω = f (X i ω) - m) : (∀ (i : ℕ), Measurable (Z i)) ∧ Contractable μ Z ∧ (∀ (i : ℕ), ∫ (ω : Ω), Z i ω ^ 2 ∂μ = ∫ (ω : Ω), Z 0 ω ^ 2 ∂μ) ∧ (∀ (i : ℕ), ∫ (ω : Ω), Z i ω ∂μ = 0) ∧ ∀ (i j : ℕ), i ≠ j → ∫ (ω : Ω), Z i ω * Z j ω ∂μ = ∫ (ω : Ω), Z 0 ω * Z 1 ω ∂μ

Helper lemma: Uniform covariance structure of centered variables.

Given contractable sequence X and function f, the centered variables Z_i = f(X_i) - m have uniform covariance structure:

• Z is contractable
• Uniform variance: E[Z_i²] = E[Z_0²] for all i
• Zero mean: E[Z_i] = 0 for all i
• Uniform covariance: E[Z_i Z_j] = E[Z_0 Z_1] for all i ≠ j

This is the key infrastructure for applying l2_contractability_bound.

theorem Exchangeability.Probability.CenteredVariables.centered_variable_bounded {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ℕ → Ω → ℝ} (hX_meas : ∀ (i : ℕ), Measurable (X i)) (f : ℝ → ℝ) (hf_meas : Measurable f) (hf_bdd : ∀ (x : ℝ), |f x| ≤ 1) (m : ℝ) (hm_def : m = ∫ (ω : Ω), f (X 0 ω) ∂μ) (Z : ℕ → Ω → ℝ) (hZ_def : ∀ (i : ℕ) (ω : Ω), Z i ω = f (X i ω) - m) (i : ℕ) (ω : Ω) : |Z i ω| ≤ 2

Helper lemma: Centered variables Z = f(X) - m are bounded by 2.

When |f| ≤ 1 and m = E[f(X_0)], then |Z i ω| = |f(X i ω) - m| ≤ 2.

theorem Exchangeability.Probability.CenteredVariables.correlation_coefficient_bounded {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (Z : ℕ → Ω → ℝ) (hZ_meas : ∀ (i : ℕ), Measurable (Z i)) (M : ℝ) (hZ_bdd : ∀ (i : ℕ) (ω : Ω), |Z i ω| ≤ M) (σSq : ℝ) (hσ_pos : σSq > 0) (h_σSq_def : σSq = ∫ (ω : Ω), Z 0 ω ^ 2 ∂μ) (covZ : ℝ) (h_covZ_def : covZ = ∫ (ω : Ω), Z 0 ω * Z 1 ω ∂μ) (ρ : ℝ) (h_ρ_def : ρ = covZ / σSq) (hZ_var_uniform : ∀ (i : ℕ), ∫ (ω : Ω), Z i ω ^ 2 ∂μ = ∫ (ω : Ω), Z 0 ω ^ 2 ∂μ) : -1 ≤ ρ ∧ ρ ≤ 1

Helper lemma: Correlation coefficient is bounded by 1 via Cauchy-Schwarz.

Given variables Z with uniform variance σSq > 0 and bound |Z i ω| ≤ M, proves |ρ| ≤ 1 where ρ = cov(Z_0,Z_1)/σSq.