Bounded covariance inequality for a pair of sigma-algebras

Proved

MarkovChainCLT.alphaPair_bounded_cov

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

markov-chainsmixingprobability

Bounded covariance inequality for two sub- $\sigma$ -algebras.

Let $(\Omega, \mathcal H, P)$ be a probability space and let $\mathcal A, \mathcal B \le \mathcal H$ be sub- $\sigma$ -algebras. Take random variables $U, V$ with $U$ $\mathcal A$ -measurable, $V$ $\mathcal B$ -measurable, and non-negative variables bounded by deterministic caps $0 \le U \le S$ , $0 \le V \le T$ . Then their covariance satisfies

\bigl| E[UV] - E[U]\,E[V] \bigr| \;\le\; S\,T\cdot \alpha(\mathcal A, \mathcal B),

where $\alpha(\mathcal A,\mathcal B)=\sup\{\,|P(C\cap D)-P(C)P(D)|: C\in\mathcal A,\ D\in\mathcal B\,\}$ is the pair-level strong mixing coefficient (alphaPair), and $E[\cdot]=\int(\cdot)\,dP$ .

Role. This is the bounded case of Ibragimov's covariance inequality and the exact intermediate step needed for the decay estimate $|E[XY]| \le C\,\alpha^{(p-2)/p}$ : applying it to the truncated variables $U = (X - E[X])\,\mathbf 1_{\{|X| \le s\}}$ and optimizing the truncation level against the tail terms produced by Hölder's inequality gives Ibragimov's rate. The bilinear dependence on the caps ( $S \cdot T$ , not $S + T$ ) is what makes that optimization close.

Proof method. Layer-cake (tail formula) applied to $U$ with respect to two measures - $P$ itself, and the finite measure $V\cdot P$ with density $V$ - followed by a level-by-level bound. At level $t$ one has $E[V\,\mathbf 1_{\{U \ge t\}}] - P\{U \ge t\}\,E[V]$ , whose absolute value is at most $T\,\alpha(\mathcal A,\mathcal B)$ by the per-level mixing estimate; integrating that constant bound over $t \in (0,S]$ produces $S\,T\,\alpha$ . No Fubini theorem on the product space is required.

Preamble

import Definitions.Def_AlphaPair

open MeasureTheory ProbabilityTheory MarkovChainCLT

Formal statement

theorem MarkovChainCLT.alphaPair_bounded_cov {Ω : Type*} [hΩ : MeasurableSpace Ω]
    {P : Measure Ω} [hP : IsProbabilityMeasure P]
    (A B : MeasurableSpace Ω) (hA : A ≤ hΩ) (hB : B ≤ hΩ)
    (U V : Ω → ℝ) (hUm : Measurable[A] U)
    (hVm : Measurable[B] V) (S T : ℝ) (hS : 0 ≤ S) (hT : 0 ≤ T)
    (hUnn : ∀ ω, 0 ≤ U ω) (hUb : ∀ ω, U ω ≤ S)
    (hVnn : ∀ ω, 0 ≤ V ω) (hVb : ∀ ω, V ω ≤ T) :
    |(∫ ω, U ω * V ω ∂P) - (∫ ω, U ω ∂P) * (∫ ω, V ω ∂P)| ≤
      S * T * @alphaPair Ω hΩ P A B := 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/0511078, Section 1.1, eq. (1.14) (Ibragimov's covariance inequality, R. L. Ibragimov 1962); the bounded case with the

S\cdot T

dependence is proved e.g. via the layer-cake/level-set argument of W. Rudin, Real and Complex Analysis, 3rd ed., Theorem 11.5.

View graph