Ibragimov's covariance inequality for a pair of $\sigma$-algebras

⚠️ 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.

Ibragimov's covariance inequality for a pair of $\sigma$-algebras (uniform form).

Let $(\Omega, \mathcal F, P)$ be a probability space, let $p > 2$, and let $M_x, M_y$ be moment caps. Then there is a constant $C \ge 0$, depending only on $p$, $M_x$ and $M_y$, such that for any pair of sub-$\sigma$-algebras $\mathcal A, \mathcal B$ and any centered random variables $X, Y$ with $X$ $\mathcal A$-measurable, $Y$ $\mathcal B$-measurable, and

the covariance obeys the power-decay estimate

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).

Formalization Note. The exponent $(p-2)/p$ is the classical Ibragimov rate: it is what makes the estimate summable when applied along a chain at lag $n$, and it turns into $\delta/(2+\delta)$ at $p = 2 + \delta$. The constant is deliberately left existential - only its independence of the pair $(\mathcal A, \mathcal B)$ and of the centered variables matters downstream. Proofs of this form (e.g. via dyadic truncation combined with Hölder at the endpoint pair $(p/(p-1), p)$, or via decreasing rearrangements) must control the bounded-versus-tail split uniformly; no $L^{\infty}$ bound on $X$ or $Y$ is available or admissible.

Why this node was retired

The posted statement is

theorem MarkovChainCLT.alphaPair_cov_uniform {Ω : Type*} [hΩ : MeasurableSpace Ω]
    (P : Measure Ω) [hP : IsProbabilityMeasure P] (p : ℝ) (hp : 2 < p) (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 ω| ^ p) P → Integrable (fun ω => |Y ω| ^ p) P →
      (∫ ω, |X ω| ^ p ∂P ≤ Mx) → (∫ ω, |Y ω| ^ p ∂P ≤ My) →
      |∫ ω, X ω * Y ω ∂P| ≤ C * @alphaPair Ω hΩ P A B ^ ((p - 2) / p) := 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.