Ibragimov covariance inequality for a pair of sub-sigma-algebras
ProvedMarkovChainCLT.alphaPair_cov_of_subSigmaAlgebramarkov-chainsmixingprobability
MarkovChainCLT.alphaPair_cov_of_subSigmaAlgebra -- restored (un-retired) after a proof was accepted for it. The moment hypotheses are indeed vacuous in the non-integrable case, but the statement survives: when X or Y leaves L^p the product integral is itself junk (integral_undef) and the inequality degenerates favourably, while in the integrable case Ibragimov's estimate applies. For a version with an explicit uniform constant and genuine MemLp hypotheses see MarkovChainCLT.alphaPair_cov_constant_of_subSigmaAlgebra (theorem_id 5cf8866c-3501-4620-8332-e44b7cae4b8a).
Preamble
import Definitions.Def_AlphaPair open MeasureTheory ProbabilityTheory MarkovChainCLT
Formal statement
theorem MarkovChainCLT.alphaPair_cov_of_subSigmaAlgebra {Ω : 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 : ∫ ω, |X ω| ^ p ∂P ≤ Mx) (hYp : ∫ ω, |Y ω| ^ p ∂P ≤ My)
(hXc : ∫ ω, X ω ∂P = 0) (hYc : ∫ ω, Y ω ∂P = 0) :
∃ C : ℝ, |(∫ ω, X ω * Y ω ∂P)| ≤
C * @alphaPair Ω hΩ P A B ^ ((p - 2) / p) := by sorrySource
R. L. Ibragimov, "Some estimates for the distribution of sums of dependent random variables" (1962), via 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); cf. also S. Gouëzel, "Explicit polynomial decay of correlations", and M. C. Jones, "On a central limit theorem with an application to Markov chains and -statistics", arXiv:math/0409112, Theorem 4.