Per-level mixing estimate for a weighted indicator

Proved

MarkovChainCLT.alphaPair_indicator_bound

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

markov-chainsmixingprobability

Per-level mixing estimate: a weighted event-vs-expectation gap.

Let $(\Omega, \mathcal H, P)$ be a probability space and let $\mathcal A, \mathcal B$ be sub- $\sigma$ -algebras of $\mathcal H$ . Take an event $C \in \mathcal A$ and a random variable $V$ that is $\mathcal B$ -measurable, non-negative and bounded by $T$ . Then

\left| \int V \, \mathbf{1}_{C} \, dP - P(C) \int V \, dP \right| \;\le\; T \cdot \alpha(\mathcal A, \mathcal B),

where $\alpha(\mathcal A, \mathcal B)$ is the pair-level strong mixing coefficient alphaPair.

Why this is the right level of generality. Writing $W(s)=\int V\,\mathbf{1}_{\{V \ge s\}}\,dP$ does not help on its own; the estimate above is the level-set statement from which the bounded covariance inequality $|E[UV]-E[U]E[V]| \le S T\alpha$ for $0\le U\le S$ , $0\le V\le T$ follows by integrating in $s$ (Tonelli), and hence the Ibragimov-type decay estimate for unbounded variables via truncation.

Proof method. Layer-cake (tail formula) applied to the two bounded non-negative measurable functions $V\mathbf{1}_{C}$ and $V$ on the same interval $(0,T]$ , followed by a single combination of the resulting integrals over $(0,T]$ ; the level sets satisfy

\{V\mathbf{1}_{C} \ge s\} = C \cap \{V \ge s\} \qquad (s > 0),

so each level contributes at most $\alpha(\mathcal A,\mathcal B)$ by the definition of alphaPair, and the $s$ -integral of that constant over $(0,T]$ is exactly $T\cdot\alpha$ .

Formalization note. The sub- $\sigma$ -algebra inclusions $\mathcal A,\mathcal B \le \mathcal H$ are explicit hypotheses: without them the level sets of $V$ need not be measurable for $P$ , and the layer-cake identity fails. The bound is stated pointwise (not merely a.e.) so that no completion of the measure is needed; the constant $T$ multiplies $\alpha$ linearly, which is what the downstream truncation argument requires.

Preamble

import Definitions.Def_AlphaPair

open MeasureTheory ProbabilityTheory MarkovChainCLT

Formal statement

theorem MarkovChainCLT.alphaPair_indicator_bound {Ω : Type*} [hΩ : MeasurableSpace Ω]
    {P : Measure Ω} [hP : IsProbabilityMeasure P]
    (A B : MeasurableSpace Ω) (hA : A ≤ hΩ) (hB : B ≤ hΩ)
    (C : Set Ω) (hC : @MeasurableSet Ω A C)
    (V : Ω → ℝ) (hVm : Measurable[B] V) {T : ℝ} (hT : 0 ≤ T)
    (hVnn : ∀ ω, 0 ≤ V ω) (hVb : ∀ ω, V ω ≤ T) :
    |(∫ ω, V ω * Set.indicator C (fun _ => (1 : ℝ)) ω ∂P) -
      (P C).toReal * (∫ ω, V ω ∂P)| ≤
      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 (covariance bounds via level sets, attributed to R. L. Ibragimov 1962); the layer-cake reduction is standard, cf. W. Rudin, Real and Complex Analysis, 3rd ed., Theorem 11.5.

View graph