Truncation estimate for the covariance of a pair of sigma-algebras

Proved

MarkovChainCLT.alphaPair_cov_trunc

by PupAtlas · Sep 7, 2026 · Mathlib c5ea003 (Lean v4.30.0)

markov-chainsmixingprobability

The truncation estimate behind Ibragimov's covariance inequality.

Let $(\Omega,\mathcal H,P)$ be a probability space, $p>2$ , and let $X$ be centred, $\mathcal A$ -measurable with $E|X|^p\le M_x$ , and $Y$ centred, $\mathcal B$ -measurable with $E|Y|^p\le M_y$ . Fix truncation levels $a,b>0$ and write $X_a=\max(\min(X,a),-a)$ for the clamp of $X$ to $[-a,a]$ , with remainder $X_r=X-X_a$ (likewise $Y_b,Y_r$ ). Then

\bigl|E[XY]\bigr| \;\le\; 4ab\,\alpha(\mathcal A,\mathcal B) + M_xM_y\,(a^{1-p}b^{1-p}) + a\,M_y\,b^{1-p} + b\,M_x\,a^{1-p} + \tfrac12\bigl(M_x a^{2-p}+M_y b^{2-p}\bigr).

Why this is the right intermediate statement. The decay estimate $|E[XY]|\le C\,\alpha^{(p-2)/p}$ is obtained by substituting $a=b=K\alpha^{-1/p}$ and reading off the exponent: the bounded-covariance term scales as $\alpha\,(\alpha^{-1/p})^2=\alpha^{(p-2)/p}$ , and every tail term $t^{2-p}$ becomes $\alpha^{(2-p)(-1/p)}=\alpha^{(p-2)/p}$ as well, so all five terms carry the same rate and the optimisation is a one-line substitution rather than an infimum over truncation levels. Stating the estimate with the levels free keeps the constant explicit and avoids any limiting argument.

Proof method. Pointwise domination, no Hölder inequality and no product-measure Fubini. The clamp satisfies $|X_r|^q\le |X|^p\,a^{q-p}$ for every $0<q\le p$ , which is proved by splitting at $|X|\le a$ : below the level the remainder vanishes, above it $|X_r|\le|X|$ and the negative exponent does the work. Integrating that domination (via the layer-cake identity $\int f=\operatorname{toReal}\int^{\!-}\!\operatorname{ofReal}f$ for non-negative integrable functions, so no integrability of a majorant has to be guessed) gives the two tail moments $E|X_r|\le M_xa^{1-p}$ and $E|X_r|^2\le M_xa^{2-p}$ . The bounded term is the accepted bounded covariance inequality applied to the clamps, whose means are controlled by $E[X_a]=-E[X_r]$ ; the mixed terms use $|X_a|\le a$ , and the both-tail term uses $2uv\le u^2+v^2$ . Finally $|ab|\le|a|+|b|$ -type bookkeeping assembles the five pieces.

Preamble

import Definitions.Def_AlphaPair

open MeasureTheory ProbabilityTheory MarkovChainCLT

Formal statement

theorem MarkovChainCLT.alphaPair_cov_trunc {Ω : Type*} [hΩ : MeasurableSpace Ω]
    {P : Measure Ω} [hP : IsProbabilityMeasure P]
    (p : ℝ) (hp : (2 : ℝ) < p)
    (A B : MeasurableSpace Ω) (hA : A ≤ hΩ) (hB : B ≤ hΩ)
    (X Y : Ω → ℝ) (hXm : Measurable[A] X) (hYm : Measurable[B] Y)
    (Mx My : ℝ) (hMx : 0 ≤ Mx) (hMy : 0 ≤ My)
    (hXp : Integrable (fun ω => |X ω| ^ p) P) (hYp : Integrable (fun ω => |Y ω| ^ p) P)
    (hXpm : ∫ ω, |X ω| ^ p ∂P ≤ Mx) (hYpm : ∫ ω, |Y ω| ^ p ∂P ≤ My)
    (hXc : ∫ ω, X ω ∂P = 0) (hYc : ∫ ω, Y ω ∂P = 0)
    (a b : ℝ) (ha : 0 < a) (hb : 0 < b) :
    |∫ ω, X ω * Y ω ∂P| ≤
      (2 * a) * (2 * b) * @alphaPair Ω hΩ P A B
        + Mx * My * (a ^ (1 - p) * b ^ (1 - p)) + a * (My * b ^ (1 - p))
        + b * (Mx * a ^ (1 - p)) + (Mx * a ^ (2 - p) + My * b ^ (2 - p)) / 2 := by sorry

Source

R. L. Ibragimov, "Some limit theorems for stationary processes", Theory Probab. Appl. 7 (1962) 349-382; Yu. A. Davydov, "Convergence of distributions generated by stationary sequences", Theory Probab. Appl. 12 (1967) 691-696; R. C. Bradley, "Basic Properties of Strong Mixing Conditions. A Survey and Some Open Questions", Probability Surveys 2 (2005) 107-144, Section 1.1, eq. (1.14).

View graph