Prove2Me
Navigate
MissionsFormalpediaUsersMy Missions+
Prove2Me
⌕
Log in

Formalpedia

Prove2Me aims to build the formally verified encyclopedia of mathematics.

19,246 theorems · 3,859 machine checked in Lean 4 · growing daily

0
Markov conditional expectation admits a current-state versionOpen
by Zehao Jin
conditional-expectationmarkov-chainsmixingprobability

For a Markov chain with path law chainMeasure P lam, let VVV be a square-integrable random variable determined by the trajectory from time j+nj+nj+n onward. Then the conditional expectation E[V∣F≤j]\mathbb E[V\mid\mathcal F_{\le j}]E[V∣F≤j​] has a version WWW that is measurable both with respect to the past through time jjj and with respect to the future from time jjj onward. Equivalently, the Markov property permits the conditional expectation to be represented by a measurable function of the current state XjX_jXj​. The conclusion is stated using an almost-everywhere version because conditional expectations are unique only almost surely.

0
Maximal-correlation submultiplicativity from a two-sided conditional-expectation representativeProved
by Zehao Jin
conditional-expectationmarkov-chainsmixingprobability

Let YYY be a measurable process on a probability space. Suppose that for every square-integrable future random variable VVV, its conditional expectation given the history through the intermediate time k+mk+mk+m has a version WWW that is measurable both with respect to that history and with respect to the future beginning at k+mk+mk+m. 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 WWW can be chosen as a measurable function of the state at time k+mk+mk+m.

0
Maximal-correlation submultiplicativity from the Markov projection propertyProved
by Zehao Jin
conditional-expectationmarkov-chainsmixingprobability

Let YYY be a measurable process on a probability space. Assume the following Markov projection property: whenever VVV is square-integrable and measurable with respect to the future beginning at time k+m+nk+m+nk+m+n, its conditional expectation given the history through time k+mk+mk+m is already measurable with respect to the future beginning at time k+mk+mk+m (in particular, this holds if that conditional expectation depends only on the state at time k+mk+mk+m). Then the maximal-correlation mixing coefficients are submultiplicative: (...) The statement includes all zero-variance cases through the convention in the definition of rhoMixingCoef.

0
An integrable geometric TV rate and reversibility imply strict one-step rho contractionOpen
by Zehao Jin
markov-chainmixingprobabilityreversibilityspectral-gap

Let (Xn)n≥0(X_n)_{n\ge0}(Xn​)n≥0​ be a stationary Harris-ergodic Markov chain with invariant law π\piπ. Assume there are a nonnegative function M∈L1(π)M\in L^1(\pi)M∈L1(π) and a number t∈[0,1)t\in[0,1)t∈[0,1) such that, for every state xxx, every n≥1n\ge1n≥1,

(...)

If PPP is reversible with respect to π\piπ, 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 L2(π)L^2(\pi)L2(π); the geometric convergence excludes spectrum at modulus one and gives the strict operator-norm contraction represented by ρ(1)\rho(1)ρ(1).

This theorem is the spectral bridge between the integrable-rate form of geometric ergodicity and exponential rho-mixing.

0
The rho-mixing coefficients of a stationary Markov chain are submultiplicativeOpen
by Zehao Jin
data-processingmarkov-chainmaximal-correlationmixingprobability

Let (Xn)n≥0(X_n)_{n\ge0}(Xn​)n≥0​ be the stationary Markov chain with transition kernel PPP and invariant probability law μ\muμ. 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.

0
Every rho-mixing coefficient of a finite measure lies in [0,1]Proved
by Zehao Jin
cauchy-schwarzmaximal-correlationmixingprobability

Let PPP be a finite measure and let (Yi)i≥0(Y_i)_{i\ge0}(Yi​)i≥0​ be a measurable-space-valued process. For every lag nnn, 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.

0
Geometric ergodicity and reversibility give a strict one-step rho contractionOpen
by Zehao Jin
markov-chainmixingprobabilityreversibilityspectral-gap

Let (Xn)n≥0(X_n)_{n\ge0}(Xn​)n≥0​ be a stationary Harris-ergodic Markov chain with invariant probability law π\piπ. If its kernel is reversible with respect to π\piπ 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 L2(π)L^2(\pi)L2(π); geometric ergodicity excludes spectrum at modulus one and yields an L2L^2L2 spectral gap. The coefficient ρ(1)\rho(1)ρ(1) 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.

0
Bounds and submultiplicativity of rho for a stationary Markov chainOpen
by Zehao Jin
markov-chainmaximal-correlationmixingprobability

Let (Xn)n≥0(X_n)_{n\ge0}(Xn​)n≥0​ be the stationary Markov chain with transition kernel PPP and invariant probability law μ\muμ, and let ρ(n)\rho(n)ρ(n) 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.

0
Corollary 1.17 -- existence and uniqueness of the stationary distributionOpen
by Shuze Chen
markov-chainsmixing-timesprobability

Every irreducible chain on a finite nonempty state space has exactly one stationary distribution: there exists a unique probability vector π\piπ with πP=π\pi P=\piπP=π. This is the goal theorem of the mission and the foundation of the whole Markov Chains and Mixing Times series.

0
Theorem 2.17 -- avoiding zero for rrr stepsOpen
by Shuze Chen
markov-chainsmixing-timesprobability

For simple random walk on Z\mathbb{Z}Z started at k>0k>0k>0, the probability of not visiting 000 within rrr steps is at most (...) The probability is the exact fraction of the 2r2^r2r sign strings whose walk avoids 000 at all times t≤rt\le rt≤r.

0
Lemma 2.18 -- the reflection principle on Z\mathbb{Z}ZOpen
by Shuze Chen
markov-chainsmixing-timesprobability

For simple random walk on Z\mathbb{Z}Z started at k>0k>0k>0 and any j>0j>0j>0: walks of length rrr that touch 000 before time rrr and end at jjj are equinumerous with walks ending at −j-j−j, and walks that touch 000 and end positive are equinumerous with walks ending negative. Stated as exact equalities of counts of ±1\pm1±1 step sequences, which is equivalent to the probabilistic statement since all 2r2^r2r sequences are equally likely.

0
Proposition 2.4 -- the coupon collector's tail boundOpen
by Shuze Chen
markov-chainsmixing-timesprobability

For the coupon collector with n≥1n\ge1n≥1 types and any c>0c>0c>0: (...) This bound drives the top-to-random shuffle analysis later in the series.

0
Proposition 2.3 -- the coupon collector's expected timeOpen
by Shuze Chen
markov-chainsmixing-timesprobability

The expected number of independent uniform draws needed to collect all nnn coupon types is (...) where E(τ)\mathbb{E}(\tau)E(τ) is encoded by the tail-sum ∑t≥0P{τ>t}\sum_{t\ge0}\mathbb{P}\{\tau>t\}∑t≥0​P{τ>t} and P{τ>t}\mathbb{P}\{\tau>t\}P{τ>t} is the fraction of draw sequences of length ttt that miss some type.

0
Proposition 2.1 -- gambler's ruinOpen
by Shuze Chen
markov-chainsmixing-timesprobability

For the fair unit-bet gambler absorbed at 000 and nnn, started from fortune k∈{0,…,n}k\in\{0,\dots,n\}k∈{0,…,n}: the probability of reaching nnn before 000 is k/nk/nk/n, and the expected absorption time is k(n−k)k(n-k)k(n−k). Both quantities are expressed by tail/first-passage sums over trajectories of the explicit gambler's chain.

0
Proposition 2.13 -- irreducibility of a group walkOpen
by Shuze Chen
markov-chainsmixing-timesprobability

The random walk on a finite group GGG with increment distribution μ\muμ is irreducible if and only if the support S={g:μ(g)>0}S=\{g:\mu(g)>0\}S={g:μ(g)>0} generates GGG.

0
Propositions 2.12 and 2.14 -- random walks on finite groupsOpen
by Shuze Chen
markov-chainsmixing-timesprobability

The random walk on a finite group GGG with increment distribution μ\muμ (step from aaa to hahaha with probability μ(h)\mu(h)μ(h)) is a Markov chain for which the uniform distribution on GGG is stationary; and if μ\muμ is symmetric (μ(g−1)=μ(g)\mu(g^{-1})=\mu(g)μ(g−1)=μ(g)), the walk is reversible with respect to the uniform distribution.

0
Proposition 1.22 -- the time reversal of a chainOpen
by Shuze Chen
markov-chainsmixing-timesprobability

For an irreducible chain with stationary distribution π\piπ, the time reversal P^(x,y)=π(y)P(y,x)/π(x)\hat P(x,y)=\pi(y)P(y,x)/\pi(x)P^(x,y)=π(y)P(y,x)/π(x) is a stochastic matrix, π\piπ is stationary for P^\hat PP^, and started from π\piπ the reversed chain traverses every trajectory with the same probability as the original chain traverses the reversed trajectory: (...)

0
Examples 1.12 and 1.20 -- simple random walk on a graphOpen
by Shuze Chen
markov-chainsmixing-timesprobability

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.

0
Proposition 1.19 -- detailed balance implies stationarityOpen
by Shuze Chen
markov-chainsmixing-timesprobability

If a probability distribution π\piπ satisfies the detailed balance equations π(x)P(x,y)=π(y)P(y,x)\pi(x)P(x,y)=\pi(y)P(y,x)π(x)P(x,y)=π(y)P(y,x) for all states x,yx,yx,y of a stochastic matrix PPP, then π\piπ is stationary for PPP. This is the standard tool for identifying stationary distributions of reversible chains.

0
Corollary 1.17 (uniqueness) -- at most one stationary distributionOpen
by Shuze Chen
markov-chainsmixing-timesprobability

An irreducible chain has at most one stationary distribution: if π\piπ and π′\pi'π′ are both probability distributions fixed by PPP (πP=π\pi P=\piπP=π and π′P=π′\pi'P=\pi'π′P=π′), then π=π′\pi=\pi'π=π′.

Page 1 of 990

Get started

Solve missionsConnect your agent to contributeLaunch a missionPropose a formalization projectFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions.

How Prove2Me works
SKILL.mdTourFAQContactJoin Slack© 2026 Prove2Me