Ionescu–Tulcea covariance inequality (pair mixing coefficient)

⚠️ Retired — specification defect

The Lean statement below does not encode the problem shown on this page, so its Disproved status carries no information about that problem. Do not import this node or use it as a dependency.

This is the Ionescu–Tulcea covariance inequality (also attributed to Ibragimov), stated uniformly for two sub-$\sigma$-algebras of a probability space and phrased through the pair mixing coefficient $\alpha(\mathcal A,\mathcal B)$.

Let $(\Omega,\mathcal F,P)$ be a probability space and let $\mathcal A,\mathcal B$ be $\sigma$-subalgebras of $\mathcal F$. Their pair mixing coefficient is

$$\alpha(\mathcal A,\mathcal B)=\sup\{\lvert P(C\cap D)-P(C)P(D)\rvert:\ C\in\mathcal A,\ D\in\mathcal B\}.$$

Fix an exponent margin $\delta>0$ and moment caps $M_x,M_y\ge 0$. Then there is a constant $C\ge 0$, depending only on the law through these bounds (not on the particular sub-$\sigma$-algebras), such that for every pair of $\sigma$-subalgebras $\mathcal A,\mathcal B$ and all real random variables $X,Y$ with $X$ measurable w.r.t. $\mathcal A$ and $Y$ measurable w.r.t. $\mathcal B$, satisfying

$$\mathbb E[X]=\mathbb E[Y]=0,\qquad \mathbb E[|X|^{2+\delta}]\le M_x,\qquad \mathbb E[|Y|^{2+\delta}]\le M_y,$$

one has the covariance bound

$$\bigl|\mathbb E[XY]\bigr|\ \le\ C\cdot \alpha(\mathcal A,\mathcal B)^{\delta/(2+\delta)}.$$

This is the workhorse inequality behind mixing-based central limit theorems: it converts a decay-of-dependence assumption (the $\alpha$ coefficient of separated $\sigma$-algebras) into a quantitative bound on the covariance of two weakly-dependent, centered random variables. It is the single analytic input used to control the lagged covariances in the Markov chain CLT.

Formalization Note The pair mixing coefficient $\alpha(\mathcal A,\mathcal B)$ is the platform definition MarkovChainCLT.alphaPair, a supremum over events of the two sub-$\sigma$-algebras; $X,Y$ are measurable for $\mathcal A,\mathcal B$ via Measurable[A]/Measurable[B]; moments are expressed as integrals of $|X|^{2+\delta}$ against $P$, and the constant $C$ is chosen before the sub-$\sigma$-algebras so that it is independent of them.

Why this node was retired

The posted statement is

theorem MarkovChainCLT.cov_bound_of_alphaPair {Ω : Type*} [hΩ : MeasurableSpace Ω]
    (P : Measure Ω) [IsProbabilityMeasure P] (δ : ℝ) (hδ : 0 < δ) (Mx My : ℝ) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ (A B : MeasurableSpace Ω) (X Y : Ω → ℝ),
      Measurable[A] X → Measurable[B] Y →
      (∫ ω, X ω ∂P = 0) → (∫ ω, Y ω ∂P = 0) →
      Integrable (fun ω => |X ω| ^ (2 + δ)) P → (∫ ω, |X ω| ^ (2 + δ) ∂P ≤ Mx) →
      Integrable (fun ω => |Y ω| ^ (2 + δ)) P → (∫ ω, |Y ω| ^ (2 + δ) ∂P ≤ My) →
      |∫ ω, X ω * Y ω ∂P| ≤ C * @alphaPair Ω hΩ P A B ^ (δ / (2 + δ)) := by sorry

A and B are arbitrary measurable structures, not sub-sigma-algebras of the ambient probability space; X,Y can be measurable only for those finer structures and not P-a.e. measurable. Their Bochner integrals then become zero by convention.

The recorded counterexample refutes the statement as encoded. It says nothing about the problem shown above, which is a different proposition.

Proposed corrected statement

With ambient sigma-algebra mΩ, add A≤mΩ and B≤mΩ, and take X measurable from A and Y measurable from B (or explicitly ambient AEMeasurable versions with a precise completed-subalgebra formulation). Retain p>2/moment hypotheses and centering; define α from measurable events of these genuine sub-sigma-algebras.

Diagnosis and correction from the public Prove2Me statement audit (wamlat/prove2me-errors). The correction is natural-language mathematics and is not Lean-verified — it is a specification for a corrected node, not a drop-in replacement. No corrected replacement node exists yet.

import Definitions.Def_AlphaPair
open MeasureTheory ProbabilityTheory MarkovChainCLT

theorem MarkovChainCLT.cov_bound_of_alphaPair {Ω : Type*} [hΩ : MeasurableSpace Ω]
    (P : Measure Ω) [IsProbabilityMeasure P] (δ : ℝ) (hδ : 0 < δ) (Mx My : ℝ) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ (A B : MeasurableSpace Ω) (X Y : Ω → ℝ),
      Measurable[A] X → Measurable[B] Y →
      (∫ ω, X ω ∂P = 0) → (∫ ω, Y ω ∂P = 0) →
      Integrable (fun ω => |X ω| ^ (2 + δ)) P → (∫ ω, |X ω| ^ (2 + δ) ∂P ≤ Mx) →
      Integrable (fun ω => |Y ω| ^ (2 + δ)) P → (∫ ω, |Y ω| ^ (2 + δ) ∂P ≤ My) →
      |∫ ω, X ω * Y ω ∂P| ≤ C * @alphaPair Ω hΩ P A B ^ (δ / (2 + δ)) := by sorry