Formalpedia
Prove2Me aims to build the formally verified encyclopedia of mathematics.
19,246 theorems · 3,859 machine checked in Lean 4 · growing daily
For a Markov chain with path law chainMeasure P lam, let be a square-integrable random variable determined by the trajectory from time onward. Then the conditional expectation has a version that is measurable both with respect to the past through time and with respect to the future from time onward. Equivalently, the Markov property permits the conditional expectation to be represented by a measurable function of the current state . The conclusion is stated using an almost-everywhere version because conditional expectations are unique only almost surely.
Let be a measurable process on a probability space. Suppose that for every square-integrable future random variable , its conditional expectation given the history through the intermediate time has a version that is measurable both with respect to that history and with respect to the future beginning at . Then the maximal-correlation coefficients satisfy (...) This version-based formulation is insensitive to the almost-everywhere choice of conditional-expectation representative and is the form naturally supplied by the Markov property, where can be chosen as a measurable function of the state at time .
Let be a measurable process on a probability space. Assume the following Markov projection property: whenever is square-integrable and measurable with respect to the future beginning at time , its conditional expectation given the history through time is already measurable with respect to the future beginning at time (in particular, this holds if that conditional expectation depends only on the state at time ). Then the maximal-correlation mixing coefficients are submultiplicative: (...) The statement includes all zero-variance cases through the convention in the definition of rhoMixingCoef.
Let be a stationary Harris-ergodic Markov chain with invariant law . Assume there are a nonnegative function and a number such that, for every state , every ,
(...)
If is reversible with respect to , then the one-step maximal-correlation coefficient is strictly less than one:
(...)
The integrable pointwise bound first yields exponential absolute regularity under the stationary law. Reversibility identifies the centered Markov operator with a self-adjoint contraction on ; the geometric convergence excludes spectrum at modulus one and gives the strict operator-norm contraction represented by .
This theorem is the spectral bridge between the integrable-rate form of geometric ergodicity and exponential rho-mixing.
Let be the stationary Markov chain with transition kernel and invariant probability law . Its maximal-correlation mixing coefficients obey
(...)
This is the multiplicative data-processing inequality for maximal correlation. The Markov property makes the past and the remote future conditionally independent through an intermediate state, so correlation across two consecutive time gaps contracts by at most the product of the two individual contraction factors.
Formalization Note The zero-lag endpoint is included together with the positive-lag formula and uses the standard range property of maximal correlation.
Let be a finite measure and let be a measurable-space-valued process. For every lag , its maximal-correlation mixing coefficient satisfies
(...)
The result remains valid for a finite, not necessarily normalized, measure because the coefficient is a supremum of normalized covariances and Cauchy--Schwarz bounds every candidate by one. Zero variances are handled by the convention that division by zero in the real numbers gives zero.
This theorem supplies the order bounds needed whenever rho coefficients are treated as a real-valued decay sequence.
Let be a stationary Harris-ergodic Markov chain with invariant probability law . If its kernel is reversible with respect to and the chain is geometrically ergodic in total variation, then its one-step maximal-correlation coefficient is strictly contractive:
(...)
This is the spectral core of the reversible geometric-ergodicity theorem. Reversibility makes the Markov operator self-adjoint on centered ; geometric ergodicity excludes spectrum at modulus one and yields an spectral gap. The coefficient is the corresponding centered operator norm. Combined with the Markov product inequality, this single-lag contraction yields exponential rho-mixing.
Formalization Note HarrisErgodic supplies invariance and pointwise total-variation convergence, while GeometricallyErgodic supplies a common geometric rate with state-dependent prefactor.
Let be the stationary Markov chain with transition kernel and invariant probability law , and let be its maximal-correlation mixing coefficient. Then
(...)
The range bound is the Cauchy--Schwarz bound for correlation. The product inequality is the maximal-correlation data-processing inequality applied through the intermediate Markov state. It is the structural fact that turns any strict contraction at one lag into an exponential mixing rate.
Formalization Note The coefficient is defined from the past and future coordinate sigma-fields of the one-sided stationary path measure. The zero-lag cases are included; they are the endpoint extension of the positive-lag formula using the same range bound.
Every irreducible chain on a finite nonempty state space has exactly one stationary distribution: there exists a unique probability vector with . This is the goal theorem of the mission and the foundation of the whole Markov Chains and Mixing Times series.
For simple random walk on started at , the probability of not visiting within steps is at most (...) The probability is the exact fraction of the sign strings whose walk avoids at all times .
For simple random walk on started at and any : walks of length that touch before time and end at are equinumerous with walks ending at , and walks that touch and end positive are equinumerous with walks ending negative. Stated as exact equalities of counts of step sequences, which is equivalent to the probabilistic statement since all sequences are equally likely.
For the coupon collector with types and any : (...) This bound drives the top-to-random shuffle analysis later in the series.
The expected number of independent uniform draws needed to collect all coupon types is (...) where is encoded by the tail-sum and is the fraction of draw sequences of length that miss some type.
For the fair unit-bet gambler absorbed at and , started from fortune : the probability of reaching before is , and the expected absorption time is . Both quantities are expressed by tail/first-passage sums over trajectories of the explicit gambler's chain.
The random walk on a finite group with increment distribution is irreducible if and only if the support generates .
The random walk on a finite group with increment distribution (step from to with probability ) is a Markov chain for which the uniform distribution on is stationary; and if is symmetric (), the walk is reversible with respect to the uniform distribution.
For an irreducible chain with stationary distribution , the time reversal is a stochastic matrix, is stationary for , and started from the reversed chain traverses every trajectory with the same probability as the original chain traverses the reversed trajectory: (...)
On a finite graph with no isolated vertices, simple random walk (move to a uniformly chosen neighbour) is a Markov chain; the distribution (...) satisfies detailed balance with it, and is therefore its stationary distribution.
If a probability distribution satisfies the detailed balance equations for all states of a stochastic matrix , then is stationary for . This is the standard tool for identifying stationary distributions of reversible chains.
An irreducible chain has at most one stationary distribution: if and are both probability distributions fixed by ( and ), then .