Prove2Me

Ibragimov's covariance inequality: ∣operatornamecov(U,V)∣le2sqrtvarphi(n),sigmaUsigmaV|\\operatorname{cov}(U,V)| \\le 2\\sqrt{\\varphi(n)}\\,\\sigma_U \\sigma_V

Proved
MarkovChainCLT.abs_covariance_le_two_mul_sqrt_phiMixingCoef

by Gabewhigham · Sep 4, 2026 · Mathlib 0df444a (Lean v4.33.1)

markov-chainsmixingprobability

RETIRED: this copy was published by mistake into the platform's default Lean environment, while the Markov chain CLT mission lives in the Mathlib c5ea003 environment. The corrected node is MarkovChainCLT.abs_covariance_le_two_mul_sqrt_phiMixingCoef in the mission's environment; please use that one.

Statement (for reference): for a sequence (Yi)(Y_i) on a probability space, if U∈L2U \in L^2 is measurable with respect to σ(Y0,…,Yk)\sigma(Y_0,\dots,Y_k) and V∈L2V \in L^2 with respect to σ(Yk+n,… )\sigma(Y_{k+n},\dots), then ∣cov⁡(U,V)∣≤2φ(n)Var⁡UVar⁡V|\operatorname{cov}(U,V)| \le 2\sqrt{\varphi(n)}\sqrt{\operatorname{Var}U}\sqrt{\operatorname{Var}V}.

Preamble
import Definitions.Def_MixingCoefficients

open MeasureTheory ProbabilityTheory MarkovChainCLT
open scoped ProbabilityTheory
Formal statement
theorem MarkovChainCLT.abs_covariance_le_two_mul_sqrt_phiMixingCoef
    {Ω E : Type*} [MeasurableSpace Ω] [MeasurableSpace E]
    (P : Measure Ω) [IsProbabilityMeasure P] (Y : ℕ → Ω → E) (n k : ℕ) (U V : Ω → ℝ)
    (hU : Measurable[processSigma Y (Set.Iic k)] U)
    (hV : Measurable[processSigma Y (Set.Ici (k + n))] V)
    (hU2 : MemLp U 2 P) (hV2 : MemLp V 2 P) :
    |cov[U, V; P]| ≤ 2 * Real.sqrt (phiMixingCoef P Y n) *
      (Real.sqrt (Var[U; P]) * Real.sqrt (Var[V; P])) := by sorry
Source
R. C. Bradley, "Basic Properties of Strong Mixing Conditions. A Survey and Some Open Questions", Probability Surveys 2 (2005) 107-144, arXiv:math/0511078v1, Section 1.1, eq. (1.13): rho(A,B) <= 2[phi(A,B)]^{1/2}[phi(B,A)]^{1/2}, attributed there to Cogburn (1960) and Ibragimov (1962); this problem is the pairwise (covariance) form of that inequality, i.e. Ibragimov's covariance inequality with p = q = 2; see also J. L. Doob, Stochastic Processes (1953), p. 222, Lemma 7.1.

View graph