Event-level strong mixing coefficient between two sub-σ-algebras

Definition

AlphaPair

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

markov-chainsmixingprobability

Let $(\\Omega, \\mathcal F, P)$ be a probability space and let $A, B$ be sub- $\\sigma$ -algebras of $\\mathcal F$ . Define the event-level strong mixing coefficient between $A$ and $B$ by

\\alpha(A,B)=\\sup\bigl\{\,|P(C\\cap D)-P(C)\\,P(D)| : C\\in A,\\ D\\in B\,\bigr\}.

This is the pair-level quantity that underlies the strong mixing coefficients $\\alpha(n)$ of a sequence of random variables (Definition 1 of Jones, On the Markov chain central limit theorem, 2004): for the past $\\sigma$ -algebra $\\mathcal F_{\\le k}$ and future $\\sigma$ -algebra $\\\\mathcal F_{\\ge k+n}$ one has $\\alpha(n)=\\sup_k \\alpha(\\mathcal F_{\\le k},\\mathcal F_{\\ge k+n})$ . It is the natural hypothesis for covariance inequalities of Ionescu–Tulcea / Ibragimov type, which bound the covariance of two random variables measurable with respect to $A$ and $B$ in terms of $\\alpha(A,B)$ and their moments.

Formalization Note The supremum is taken over a set of real numbers built from the extended-real measures via ENNReal.toReal; for a probability measure each term lies in $[0,1]$ , so the set is bounded above and the supremum is well-defined.

Definition code

import Definitions.Def_MixingCoefficients

/-!
Event-level strong mixing coefficient between two sub-σ-algebras of `Ω`.

For sub-σ-algebras `A`, `B` of a probability space `(Ω, P)`,
$$\\alpha(A,B)=\\sup\\{|P(C\\cap D)-P(C)P(D)| : C\\in A,\\ D\\in B\\}.$$
This is the pair-level quantity underlying the strong mixing coefficient
`alphaMixingCoef` of a sequence (Definition 1 of Jones 2004), and is the natural
hypothesis for covariance inequalities such as Ionescu–Tulcea's.
-/

open MeasureTheory ProbabilityTheory

namespace MarkovChainCLT

/-- The strong mixing coefficient between two sub-σ-algebras `A` and `B`. -/
noncomputable def alphaPair {Ω : Type*} [MeasurableSpace Ω]
    (P : Measure Ω) (A B : MeasurableSpace Ω) : ℝ :=
  sSup {r | ∃ C D : Set Ω, MeasurableSet[A] C ∧ MeasurableSet[B] D ∧
    r = |((P (C ∩ D)).toReal : ℝ) - (P C).toReal * (P D).toReal|}

end MarkovChainCLT

Source

G. L. Jones, "On the Markov Chain Central Limit Theorem", Probability Surveys 1 (2004) 299-320, arXiv math/0409112v2, Section 3, Definition 1

View graph