Ibragimov's covariance inequality, with $C$ depending only on $p, M_x, M_y$

Ibragimov's covariance inequality with the constant where it belongs.

Let $(\Omega,\mathcal H,P)$ be a probability space, $p>2$, and $M_x,M_y\ge 0$. Then there is a constant $C\ge 0$ depending only on $p$, $M_x$, $M_y$ such that for every pair of sub-$\sigma$-algebras $\mathcal A,\mathcal B\le\mathcal H$ and every pair of random variables $X\in L^p$ that is $\mathcal A$-measurable and $Y\in L^p$ that is $\mathcal B$-measurable, both centred and with $E|X|^p\le M_x$, $E|Y|^p\le M_y$,

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

Why this statement and not the existing one. MarkovChainCLT.alphaPair_cov_of_subSigmaAlgebra (ab3a517b-0838-4157-8f6f-0cb85785e627) states the same inequality, but binds C after A, B, X and Y. That makes it vacuous whenever $\alpha>0$: since $p>2$ the exponent is positive, so $\alpha^{(p-2)/p}>0$ and one takes $C=|E[XY]|/\alpha^{(p-2)/p}$. Only the case $\alpha=0$ — that is, independence — carries any content there, and that case is elementary. I proved it in that form; the Lean build reports the moment hypotheses as unused variables, which is the statement admitting as much. Moving the binder outwards is the whole repair, and it is the same class of defect, one binder further out, that retired MarkovChainCLT.alphaPair_cov_uniform.

Second repair: MemLp. The original also passes the moment bounds as ∫ ω, |X ω| ^ p ∂P ≤ Mx. In Lean the Bochner integral of a non-integrable function is 0, so that inequality is satisfied vacuously by any X whose $p$-th power is not integrable — it is not a moment hypothesis at all, and neither is ∫ ω, X ω ∂P = 0 a centring hypothesis. Adding MemLp X (ENNReal.ofReal p) P restores the intended meaning and is needed by any real proof.

Proof sketch (Ibragimov / Davydov). Truncate at level $T$: write $X = X\mathbf 1_{|X|\le T} + X\mathbf 1_{|X|>T}$ and likewise for $Y$. The bounded parts are handled by the event-level bound already on the platform (MarkovChainCLT.alphaPair_bounded_cov, 10d46f2a-cf7c-4b78-87b0-e8b558a3b001, and the indicator estimate alphaPair_indicator_bound, 60e33dfa-2508-4f60-8888-af3cf8a5e86f), giving $\le 4T^2\alpha$. The tails are handled by Hölder against the $L^p$ bound: $E|X\mathbf 1_{|X|>T}| \le M_x^{1/p}\,P(|X|>T)^{1-1/p} \le M_x T^{-(p-1)}$ by Markov. Optimising $T$ in $T^2\alpha + \text{tail}(T)$ produces the exponent $(p-2)/p$ and a constant built only from $p$, $M_x$, $M_y$. The truncated variables stay $\mathcal A$- and $\mathcal B$-measurable, which is exactly why the sub-$\sigma$-algebra hypotheses hA, hB are needed and why the retired uniform version was false.

Role. This is the covariance estimate underlying the Markov-chain CLT through the blocking/mixing route (Jones, On the Markov chain central limit theorem, Probability Surveys 1 (2004) 299–320, §3–4): applied to lag-$k$ pairs of summands it turns a moment bound into summable correlations. The uniformity of $C$ across lags is the entire point — a per-pair constant gives nothing when summing over $k$.