Dependencies

For a finite type \(A\), set \(\operatorname {avg}(f)=\sum _{a\in A}f(a)/|A|\). When \(A\) is empty this is zero, following Lean’s division convention.

A distribution consists of nonnegative real weights \(p_a\) with \(\sum _a p_a=1\). Its expectation is \(\sum _a p_a f(a)\), and an event probability is the expectation of its indicator. Such a distribution cannot exist on an empty type.

\(\mathrm{hitProb}(K,B,n)(a)=\Pr _a(\exists s\le n,\ X_s\in B)=\Pr _a(T_B\le n)\), the expectation over the first \(n\) transitions of the indicator that one of the states at the times \(0,\dots ,n\) lies in \(B\).

A family of kernels \((K_t)_{t\ge 0}\) moves the chain from time \(t\) to time \(t+1\) with \(K_t\); \(\mathrm{iterateSeq}(K,n,f)(a)\) is the expectation of \(f\) at time \(n\) from \(a\). A constant family gives the iterates of a single kernel.

A finite kernel assigns a distribution to every state. Its operator iterates compute expectations at finite times; trajectory functionals additionally record the history.

A deterministic update \(\mathrm{step}\colon S\times R\to S\) driven by a uniform round \(r\in R\) defines the kernel \(K(s)=\mathrm{law}(\mathrm{step}(s,r))\). Its \(T\)-step expectations are expectations over \(T\) i.i.d. uniform rounds.

Iterated uniform averages over two finite sets commute; in particular an outer average commutes with the trajectory expectation \(\mathrm{expList}\), which also commutes with finite sums and vanishes on the zero functional.

Let \(f\) be a zero-one survival indicator with \(Kf\le f\). Suppose for each state \(a\) there is \(n_a\) with \((K^{n_a}f)(a){\lt}1\). There are \(m{\gt}0\) and \(0\le q{\lt}1\) such that \(K^m f\le qf\).

The finite average is Mathlib’s finite expectation, \(\operatorname {avg}(f)=\mathbb {E}_{a\in A}f(a)\) (Finset.expect); both vanish on an empty type. On a nonempty type the independent product of uniform distributions on \(A\), indexed by a finite set \(I\), is the uniform distribution on \(A^I\). Hence \(\mathrm{expList}\) over \(T\) rounds is the expectation of \(F\) over \(T\) i.i.d. uniform draws, both as Mathlib’s \(\mathbb {E}_{\omega \colon \{ 0,\ldots ,T-1\} \to A}\) and under the product distribution.

For a uniform dart \(d\) of \(G\), \(\mathbb {E}F(d_1,d_2)=\sum _v\sum _{u\in N(v)}F(v,u)/(2|E|)\); reversing \(d\) preserves the law, its underlying edge is a uniform edge, and its tail is \(v\) with probability \(\deg v/(2|E|)\).

Ignoring history in a trajectory expectation recovers the iterated transition operator.

Let \(V\ge 0\) vanish on \(B\) and be at least \(V_{\min }{\gt}0\) off \(B\), with \(\mathbb {E}[V(X_{t+1})\mid X_t=x]\le \rho V(x)\) for \(x\notin B\). Then \(\Pr _a(T_B{\gt}t)\le \rho ^tV(a)/V_{\min }\).

In a round \(r\in \prod _vN(v)\) every vertex picks a neighbour. Under the uniform distribution the picks are independent and uniform: \(\mathbb {E}\prod _vf_v(r_v)=\prod _v\mathbb {E}_{u\in N(v)}f_v(u)\), and, without isolated vertices, \(\mathbb {E}g(r_v)=\mathbb {E}_{u\in N(v)}g(u)\). A uniform vertex \(v\) with a uniform round gives the sequential step “uniform vertex, uniform neighbour \(r_v\)”.

On a nonempty finite type the normalized uniform distribution agrees with the existing finite average.

Uniform averages factor over independent coordinates and are invariant under bijections of the sample space.

The recursively defined expectation over \(T\) independent draws equals the uniform average over functions \(\{ 0,\ldots ,T-1\} \to A\).

Independent coordinates have product weights. Expectations of product observables factor, and transporting weights along a function commutes with expectation.

Under these hypotheses, \(K^{nm}f\le q^n f\), and \(K^t f(a)\to 0\) for every state \(a\).

Let \(X=\sum _iX_i\) be a sum of independent \(\{ 0,1\} \)-valued trials with \(\Pr (X_i=1)=p_i\), and let \(\mu _L\le \mu =\sum _ip_i\le \mu _H\). For \(\delta {\gt}0\),

and for \(0{\lt}\delta {\lt}1\),

The trials are \(\{ 0,1\} \)-valued observables of the coordinates of an independent product of distributions, independent biased coins (counting the heads in any subset), or the coordinates of one uniform round (Mitzenmacher–Upfal, Probability and Computing, Theorems 4.4 and 4.5 with Exercise 4.7).

Let \(X=\sum _{i{\lt}n}Y_i(\omega _i)\) with independent uniform coordinates. If each \(Y_i\) is \(\{ 0,1\} \)-valued, \(\Pr (X\ge \mathbb {E}X+\lambda )\le e^{-2\lambda ^2/n}\). If \(Y_i-\mathbb {E}Y_i\le b\) and \(\sum _i\mathrm{Var}\, Y_i\le \sigma ^2\), then \(\Pr (X\ge \mathbb {E}X+\lambda )\le \exp \bigl(-\lambda ^2/(2\sigma ^2(1+b\lambda /(3\sigma ^2)))\bigr)\).

Let \(\Psi \ge 0\), and for \(t{\lt}T\) let \(c_t\ge 0\), \(\mathbb {E}[\Psi (X_{t+1})\mid X_t=x]\le \Psi (x)-c_t/\Psi (x)\) when \(\Psi (x){\gt}0\), and \(\mathbb {E}[\Psi (X_{t+1})\mid X_t=x]=0\) when \(\Psi (x)=0\). If \(\sum _{t{\lt}T}c_t\ge 4\Psi (x_0)^2\), then \(\Pr _{x_0}(\Psi (X_T)=0)\ge 1/2\).

Let \(c_1{\gt}1\) and \(c_2,c_3,c_4,c_6{\gt}0\). There is \(c_5{\gt}0\) such that for every finite chain and observable \(X\in \{ 0,\dots ,q\} \) with \(c_4\log q\le q\): if from every state below the target \(\Pr [X_{t+1}\ge \min \{ c_1X_t,q\} ]\ge 1-e^{-c_2X_t}\), and \(\Pr [X_{t+1}\ge 1]\ge c_3\) when \(X_t=0\), then \(X\) reaches \(c_4\log q\) within \(c_5\log q+\log _{c_1}(c_4\log q)\) steps with probability at least \(1-q^{-c_6}\) (equivalently within \(C\log q\) steps).

Let \(\Psi \ge 0\) with every positive value at least \(\Psi _{\min }{\gt}0\), and \(\mathbb {E}[\Psi (X_{t+1})\mid X_t=x]\le (1-\delta _t)\Psi (x)\) for all \(x\) and \(t{\lt}T\). Then \(\Pr _{x_0}(\Psi (X_T){\gt}0)\le \prod _{t{\lt}T}(1-\delta _t)\, \Psi (x_0)/\Psi _{\min }\).

Let \(\varphi \) equal \(\varphi _A\) on an event \(A\) and \(\varphi _B\) on an event \(B\), and let \(S\) be the event of lying in neither. If \(\mathbb {E}_{x_0}\varphi (X_T)=\varphi (x_0)\) and \(m\le \varphi -\varphi _B\le M\) on \(S\), then \(\varphi (x_0)-\varphi _B-(\varphi _A-\varphi _B)\Pr _{x_0}(X_T\in A)\) lies between \(m\Pr _{x_0}(X_T\in S)\) and \(M\Pr _{x_0}(X_T\in S)\). Hence, if \(\varphi _A\ne \varphi _B\), the conservation law holds for every \(T\) and \(\Pr _{x_0}(X_T\in S)\to 0\), then \(\Pr _{x_0}(X_T\in A)\to (\varphi (x_0)-\varphi _B)/(\varphi _A-\varphi _B)\); if moreover \(A\) is absorbing, this is the supremum of the finite-time probabilities.

Let \(A_1\supseteq \cdots \supseteq A_T\) be sets of states such that from \(A_i\) the chain stays in \(A_i\) with probability at least \(1-\varepsilon \) and, for \(i{\lt}T\), enters \(A_{i+1}\) with probability at least \(1-\nu \). From \(A_1\), after \(\ell T\) steps the chain is in \(A_T\) with probability at least \(1-T(\ell \varepsilon +\nu ^\ell )\).

For every functional \(F\) of \(T\) i.i.d. uniform rounds, \(\mathbb {E}F(r_T,\dots ,r_1)=\mathbb {E}F(r_1,\dots ,r_T)\). In particular the \(T\)-step expectations of a round-based process are also obtained by applying the rounds last to first.

Every stochastic kernel on a nonempty finite type has a distribution \(p\) with \(pK=p\).