Markov Chain

Motivation

An agent whose preferences change over time cannot simply optimize once: a plan that is optimal today may be abandoned tomorrow by the agent's own "future selves". This is time inconsistency, and its standard source is non-exponential discounting, studied since Strotz (1955). The usual response, going back to Strotz and made rigorous in continuous time by Ekeland and Lazrak (2006), is to look for an equilibrium strategy: a strategy from which no future self wants to deviate. In continuous time "no incentive to deviate" is encoded through a first-order condition, which Huang and Zhou call a weak equilibrium.

Björk, Khapko and Murgoci (2017, Remark 3.5) observed that this first-order condition need not express the absence of an incentive to deviate: it only says that a derivative vanishes or is nonnegative, and a stationary point need not be a maximum. Huang and Zhou (Math. Oper. Res. 46(2), 2021; read here as arXiv:1809.09243v3) introduce a strong equilibrium, which requires the agent's payoff to be no better after any short deviation, and study the two notions for continuous-time Markov chains with controlled generators. This mission formalizes their main example (Example 4.3): a concrete two-state model in which a weak equilibrium fails to be strong, so that an agent in one state strictly gains from deviating on every short interval.

Setting

The state space is $S=\{1,\dots,N\}$. A generator is a matrix $Q\in\mathbb R^{N\times N}$ whose $i$-th row $Q_i$ lies in $E_i=\{q: q_j\ge0\ (j\ne i),\ q_i=-\sum_{j\ne i}q_j\}$. Admissible rows form sets $D_i\subseteq E_i$, and the control space is $\mathcal Q=\{Q: Q_i\in D_i\ \forall i\}$. A payoff function $f(t,i,q)$ gives the payment rate at time difference $t$ in state $i$ when row $q$ is in force. The expected payoff of using $Q$ from state $i$ is

$$F(i,Q)=\mathbb E_{i,Q}\Big[\int_0^\infty f(t,X_t,Q_{X_t})\,dt\Big]=\int_0^\infty\sum_j (e^{tQ})_{ij}\,f(t,j,Q_j)\,dt .$$

The concatenation $Q\otimes_\varepsilon Q^*$ uses $Q$ on $[0,\varepsilon]$ and $Q^*$ afterwards. A generator $Q^*\in\mathcal Q$ is a weak equilibrium if $\liminf_{\varepsilon\downarrow0}[F(i,Q^*)-F(i,Q\otimes_\varepsilon Q^*)]/\varepsilon\ge0$ for all $i\in S$, $Q\in\mathcal Q$, and a strong equilibrium if for all $i,Q$ there is $\varepsilon>0$ with $F(i,Q^*)\ge F(i,Q\otimes_{\varepsilon'}Q^*)$ for every $\varepsilon'\in(0,\varepsilon]$.

The paper's first-order and second-order quantities are

$$\Gamma^{Q^*}(Q_i)=f(0,i,Q_i)+Q_i\cdot F(Q^*),\qquad \Lambda^{Q^*}(i,Q)=f_t(0,i,Q_i)+Q_i\cdot\big(2G(Q^*)+\Gamma^{Q^*}(Q)\big),$$

with $G$ the payoff computed with the time derivative $f_t$ in place of $f$.

In the two-state model of §4, $S=\{1,2\}$, $D_i=E_i$, every generator is $Q\sim(a,b)=\begin{bmatrix}-a&a\\ b&-b\end{bmatrix}$ with $a,b\ge0$, and $f(t,1,(-a,a))=\delta(t)g_1(a)$, $f(t,2,(b,-b))=\delta(t)g_2(b)$ with the pseudo-exponential discount $\delta(t)=\lambda e^{-\rho t}+(1-\lambda)e^{-\rho't}$. Example 4.3 takes $\lambda=\tfrac12$, $\rho=1$, $\rho'=2$, $g_1(a)=-a^2$, and $g_2(b)=\tfrac{193}{144}+\tfrac56b$ for $b<\tfrac7{12}$, $g_2(b)=2-(1-b)^2$ for $b\ge\tfrac7{12}$.

Formalization targets

Goal: Example 4.3

$$Q^*\sim\Big(\frac5{12},\frac7{12}\Big)\ \text{is a weak equilibrium and not a strong equilibrium.}$$

The statement is fully explicit and has no hypotheses.

Milestones

1. (4.3)–(4.4): closed forms of $F_1-F_2$ and $G_1-G_2$ for $Q\sim(a,b)$ under pseudo-exponential discounting.
2. (4.5), (4.6), (4.8): $\Gamma^{Q^*}(Q_1)$, $\Gamma^{Q^*}(Q_2)$ and $\Lambda^{Q^*}(2,Q)$ in the two-state model.
3. Theorem 3.1: under (2.3) and (3.3), $Q^*$ is weak iff $\Gamma^{Q^*}(Q^*_i)\ge\Gamma^{Q^*}(Q_i)$ for all $(i,Q)$.
4. (4.11): at $Q^*$, $\Gamma_1$ is maximized uniquely at $a^*$ and $\operatorname{arg\,max}_{b\ge0}\Gamma_2(b)=[0,7/12]$.
5. Proposition 3.3: the second-order test on the set $R$ of equality cases.
6. (4.12): $\Lambda_2(a^*,b)=-b/12-579/288$ on $[0,7/12]$, so $\Lambda_2(a^*,b^*)<\Lambda_2(a^*,b)$ for $b\in[0,7/12)$.

Further statements

Remark 4.1: for $Q\sim(5/12,b)$, $b\in[0,7/12)$, $F(2,Q^*)<F(2,Q\otimes_\varepsilon Q^*)$ for all small $\varepsilon>0$. And (4.13): the equation $\tfrac56\le2a=\tfrac12(\tfrac1{1+a}+\tfrac1{2+a})(a^2+\tfrac{193}{144})$ has a unique solution $\bar a\ge0$, and $\bar Q^*\sim(\bar a,0)$ is a strong equilibrium.

Significance

The example shows that the weak equilibrium concept, the standard one in the time-inconsistency literature since Ekeland and Lazrak, admits strategies that an agent would abandon: Remark 4.1 exhibits a deviation that strictly increases the payoff on every short interval. Together with (4.13), it shows that in one and the same model a weak-but-not-strong equilibrium and a strong equilibrium coexist, so the choice of equilibrium concept changes which strategies are predicted. The example is the paper's justification for introducing strong equilibria.

The result is proved in the paper, through the first-order characterization (Theorem 3.1), the second-order test (Proposition 3.3, resting on the second-order expansion Lemma 3.2) and explicit computations in the two-state model. None of it has been machine-checked. A formal proof would provide checked versions of Theorem 3.1 and Proposition 3.3 for finite-state chains, reusable for any other example, and an independent check of the arithmetic of Example 4.3, where the source contains at least one misprinted formula.

Difficulty

Both conjuncts of the goal concern the small-$\varepsilon$ behaviour of $F(2,Q\otimes_\varepsilon Q^*)$, an integral of products of matrix exponentials. Weakness reduces to a first-order comparison by Theorem 3.1, but its proof needs the expansion (3.6) with an $o(\varepsilon)$ remainder controlled uniformly enough to pass under the integral over $[0,\infty)$. Failure of strong equilibrium cannot be read off the first-order term: at $b^*=7/12$ the maximizer of $\Gamma_2$ is not unique, every $b\in[0,7/12)$ ties at first order, and the decision moves to the second-order coefficient $\Lambda$ of Lemma 3.2, whose derivation needs a second-order expansion of the concatenated payoff. The regularity hypotheses of Lemma 3.2 and of (3.3) must also be verified for the example's discount function.

Formalization scope

States are Fin N; the paper's state $k$ is index $k-1$, so in the two-state model state 1 is 0 : Fin 2 and state 2 is 1 : Fin 2. Expectations are written through the transition matrices $e^{tQ}$ (NormedSpace.exp (t • Q)) and Fubini, exactly as the paper computes on p. 23; no Markov process is constructed. Payoffs are Bochner integrals over $(0,\infty)$. The weak-equilibrium condition is written as "for every $\eta>0$, eventually as $\varepsilon\downarrow0$ the quotient is $\ge-\eta$", which is $\liminf\ge0$ without a real-valued liminf. The norm in (2.3) is the sup norm, equivalent to the paper's Euclidean norm because (2.3) quantifies over every $c>0$.

Standing assumptions: $D_i\subseteq E_i$, continuity of $f$ in $t$ (2.2) and the integrability condition (2.3). Theorem 3.1 adds the shift bound (3.3)–(3.5); Proposition 3.3 assumes the conditions of Lemma 3.2, with the derivative $f_t$ tied to $f$. The closed forms (4.3)–(4.4) assume $\rho,\rho'>0$ (the page allows $\rho,\rho'\ge0$, but with a zero rate the payoff integral diverges); the algebraic identities (4.5)–(4.8) keep the page's $\rho,\rho'\ge0$; Example 4.3 has $\rho=1$, $\rho'=2$. Statement (4.11) gives $\Gamma_2(b)=g_2(b)-\tfrac56b$ and the argmax; the page's case formula for $b\ge7/12$ contains a misprint and is not used.

No trivializing reading is available: the goal has no hypotheses, $F$ is built from $e^{tQ}$ and the concatenation uses $Q$ before and $Q^*$ after $\varepsilon$, so neither conjunct holds by a junk value. Integrability of every payoff follows from (2.3) and is never assumed.

Theorem 3.1 and the second-order package are also drafted in the companion mission on existence of equilibria; they are restated here in the sub-namespace StrongWeakEq.TwoState. The goal needs the verification of (2.3), (3.3) and the Lemma 3.2 conditions for the example (convexity of $\delta$ gives (3.15)), the closed forms of $e^{tQ}$ for two-state generators, and the expansions of the paper. Contributions of proofs of the general results (Theorem 3.1, Proposition 3.3) are welcome independently of the example.

Selected references

• Y.-J. Huang and Z. Zhou, Strong and Weak Equilibria for Time-Inconsistent Stochastic Control in Continuous Time, Math. Oper. Res. 46(2), 2021; arXiv:1809.09243v3. https://arxiv.org/abs/1809.09243, https://doi.org/10.1287/moor.2020.1066
• I. Ekeland and A. Lazrak, Being serious about non-commitment: subgame perfect equilibrium in continuous time, 2006. https://arxiv.org/abs/math/0604264
• T. Björk, M. Khapko and A. Murgoci, On time-inconsistent stochastic control in continuous time, Finance Stoch. 21 (2017), pp. 331–360.
• R. H. Strotz, Myopia and inconsistency in dynamic utility maximization, Rev. Econ. Stud. 23 (1955), pp. 165–180.

Motivation

A decision maker is time-inconsistent when the plan that is optimal today stops being optimal tomorrow. The standard source is non-exponential discounting: a reward $t$ units of time ahead is weighted by $\delta(t)$, and unless $\delta$ is exponential the relative weight of two future dates changes as time passes. Hyperbolic and pseudo-exponential discount functions, which fit experimental and group-decision data better than exponential ones, all have this property. For such an agent "optimal control" is not a meaningful target, and the literature instead looks for equilibrium policies: plans that no current self wants to deviate from, given that all future selves follow the plan.

In discrete time the definition is unambiguous: a policy is an equilibrium if deviating at the current step alone does not help. In continuous time there is no "current step", and the usual definition, due to Ekeland and Lazrak (2006), compares the payoff of the plan with that of a deviation on a short interval $[0,\varepsilon]$ through a first-order condition as $\varepsilon\downarrow0$. Huang and Zhou (arXiv:1809.09243, Math. Oper. Res. 2021) call this a weak equilibrium, introduce a strong equilibrium that requires the deviation to be unprofitable for every small $\varepsilon$, and study both for a controlled finite-state Markov chain.

A natural question is whether continuous-time equilibria are the limits of the discrete-time ones as the time step shrinks. This mission formalizes the paper's answer (§5.1): limits of discrete equilibria are always weak equilibria. The paper's Example 5.1 shows they need not be strong.

Setting

The state space is $S=\{1,\dots,N\}$. A continuous-time Markov chain on $S$ is controlled through its generator $Q=(q_{ij})$: in state $i$ the row $Q_i$ is chosen from an admissible set $D_i\subseteq E_i=\{q: q_j\ge0\ (j\ne i),\ q_i=-\sum_{j\ne i}q_j\}$, and the control space is $\mathcal Q=\{Q: Q_i\in D_i\ \forall i\}$. A payoff function $f(t,i,q)$ gives the reward at time-distance $t$ from now, in state $i$, under row $q$. The standing assumptions are continuity of $t\mapsto f(t,i,q)$ on $[0,\infty)$ and, for each $c>0$, integrability over $[0,\infty)$ of $\sup_{i,\,q\in D_i,\,\|q\|\le c}|f(t,i,q)|$ (condition (2.3)). The expected payoff from state $i$ is

$$F(i,Q)=\mathbb E_{i,Q}\Big[\int_0^\infty f(t,X_t,Q_{X_t})\,dt\Big]=\int_0^\infty\sum_j(e^{tQ})_{ij}f(t,j,Q_j)\,dt,$$

and $F(Q)=(F(1,Q),\dots,F(N,Q))$. With $Q\otimes_\varepsilon Q^*$ the generator that uses $Q$ on $[0,\varepsilon]$ and $Q^*$ afterwards, $Q^*\in\mathcal Q$ is a weak equilibrium if $\liminf_{\varepsilon\downarrow0}\big(F(i,Q^*)-F(i,Q\otimes_\varepsilon Q^*)\big)/\varepsilon\ge0$ for all $i$ and $Q\in\mathcal Q$. The first-order quantity is $\Gamma^{Q^*}(q)=f(0,i,q)+q\cdot F(Q^*)$.

Discretization. Fix a mesh $\delta_n>0$. A transition matrix $u$ (rows in the probability simplex $\mathfrak P$) has generator $Q^{u,n}=(u-I)/\delta_n$, the admissible matrices are $\mathcal A^n=\{u: Q^{u,n}\in\mathcal Q\}$, and the discrete payoff is $\kappa^n(k,i,\alpha)=f\big(k\delta_n,i,(\alpha-e_i)/\delta_n\big)\,\delta_n$. The discrete value is $V^n(i,u)=\mathbb E_{i,u}\big[\sum_{k\ge0}\kappa^n(k,X_k,u_{X_k})\big]$, and $u^n\in\mathcal A^n$ is a discrete equilibrium if $V^n(i,u^n)\ge V^n(i,u\otimes_1u^n)$ for all $i$ and $u\in\mathcal A^n$, where $u\otimes_1u^n$ uses $u$ at time $0$ and $u^n$ afterwards. The continuation values are $H^n_i(u^n)=\mathbb E_{i,u^n}\big[\sum_{k\ge0}\kappa^n(k+1,X_k,u^n_{X_k})\big]$. Theorem 5.2 additionally assumes (5.8): for some $T>0$, $t\mapsto|f(t,i,q)|$ is nonincreasing on $[T,\infty)$.

Formalization targets

Goal: Theorem 5.2

Let $\delta_n\downarrow0$, let $u^n$ be an equilibrium of the problem with mesh $\delta_n$, $Q^n=Q^{u^n,n}$, and suppose $f(\cdot,i,\cdot)$ is continuous on $[0,\infty)\times D_i$. If $Q^{n_k}\to Q^*\in\mathcal Q$ along a subsequence, then

$$\Gamma^{Q^*}(Q^*_i)\ge\Gamma^{Q^*}(Q_i)\quad\text{for all }(i,Q)\in S\times\mathcal Q,\qquad\text{and } Q^* \text{ is a weak equilibrium.}$$

Milestones

1. (5.12): an equilibrium $u^n$ satisfies $\kappa^n(0,i,u^n_i)+H^n(u^n)\cdot u^n_i\ge\kappa^n(0,i,u_i)+H^n(u^n)\cdot u_i$ for all $u\in\mathcal A^n$.
2. Generator form (proof of Theorem 5.2): dividing by $\delta_n$, the same inequality reads $f(0,i,Q^n_i)+H\cdot Q^n_i\ge f(0,i,Q^{u,n}_i)+H\cdot Q^{u,n}_i$.
3. Continuity of $Q\mapsto F(Q)$ on $\mathcal Q$ (proof of Theorem 3.3).
4. Lemma 5.1: $H^{n_k}_i(u^{n_k})\to F(i,Q^*)$ along the subsequence.

Significance

The theorem justifies the weak-equilibrium notion from discrete time: whatever a time-inconsistent agent does on a fine time grid, the continuous-time limit satisfies the first-order condition (3.10). Combined with the paper's discrete existence result (Theorem 5.1) and compactness of $\mathcal Q$, it yields weak equilibria by approximation (Remark 5.3). It also locates the gap between the two notions: the limit is weak but in general not strong.

The result is proved in the paper; nothing about it is open. No part of it has a machine-checked proof. A formal development adds a checked Euler-scheme comparison between $(I+\delta Q)^k$ and $e^{k\delta Q}$ for generator matrices, a dominated passage to the limit for Riemann sums of the payoff, and continuity of the payoff in the generator, each reusable for other finite-state continuous-time control problems.

Difficulty

The obvious argument is to divide the discrete one-step inequality (5.12) by $\delta_n$ and let $n\to\infty$. Its algebraic part is immediate. The difficulty is the convergence of the discrete continuation values $H^n(u^n)$, which are infinite sums along a discrete chain with transition matrix $u^n$, to the continuous payoff $F(Q^*)$, an integral along the continuous chain with generator $Q^*$. Three errors must be controlled at once: the discrete chain against the chain sampled from $e^{tQ^n}$ (the difference of $k$-th powers grows with $k\approx M/\delta_n$), the Riemann sum against the integral (needs uniform continuity of $f$ jointly in $t$ and $q$), and $F(Q^n)$ against $F(Q^*)$. The tail of the infinite sums is not controlled by (2.3) alone: integrability of a majorant does not make its samples on a grid summable, which is why (5.8) is assumed. A second subtlety concerns the last step: the paper passes from (3.10) to the weak-equilibrium property through Theorem 3.1, which assumes a condition (3.3) that Theorem 5.2 does not. The conclusion is still true without (3.3), but no numbered statement of the paper provides that step.

Formalization scope

• States are Fin N; rows are Fin N → ℝ with the sup norm, generators and transition matrices are Matrix (Fin N) (Fin N) ℝ with the product topology.
• Expectations are written through marginals: $F(i,Q)=\int_0^\infty\sum_j(e^{tQ})_{ij}f(t,j,Q_j)\,dt$ (Bochner integral) and $H^n_i(u)=\sum_k\sum_j(u^k)_{ij}\kappa^n(k+1,j,u_j)$ (tsum). No Markov process is constructed.
• The weak-equilibrium liminf is encoded as "for every $\eta>0$, eventually as $\varepsilon\downarrow0$ the quotient is $\ge-\eta$".
• "$f(\cdot,i,\cdot)$ is continuous" is joint continuity on $[0,\infty)\times D_i$; (5.8) is required for $q\in D_i$; $\delta_n\downarrow0$ is positivity, monotonicity and convergence to $0$; the subsequence is a strictly increasing $\varphi:\mathbb N\to\mathbb N$.
• Not assumed: integrability of $F$, summability of $H^n$ or (5.2) for $\kappa^n$ (they follow from (2.3) and (5.8)), compactness of $D_i$, and condition (3.3).
• The equilibria $u^n$, the generators $Q^n=(u^n-I)/\delta_n$ and the subsequence are part of the goal's data. A version that only assumes "$Q^n\to Q^*$" for arbitrary $Q^n\in\mathcal Q$ would be false and is ruled out.
• The continuity milestone is proved in the paper for compact $D_i$; it is stated here without compactness, since only convergent sequences in $\mathcal Q$ matter.
• Needed infrastructure: bounds on $\|(I+\delta Q)^k-e^{k\delta Q}\|$ for generator matrices, stochasticity of $e^{tQ}$ for generator $Q$, dominated convergence for the payoff integral and for the discrete series. Contributions of these general lemmas are welcome.

Selected references

• Y.-J. Huang and Z. Zhou, Strong and Weak Equilibria for Time-Inconsistent Stochastic Control in Continuous Time, Math. Oper. Res. 46(2), 2021; read as arXiv:1809.09243v3. https://arxiv.org/abs/1809.09243 , https://doi.org/10.1287/moor.2020.1066
• I. Ekeland and A. Lazrak, Being serious about non-commitment: subgame perfect equilibrium in continuous time, tech. rep., University of British Columbia, 2006. http://arxiv.org/abs/math/0604264
• S. N. Ethier and T. G. Kurtz, Markov Processes: Characterization and Convergence, Wiley, 1986. https://doi.org/10.1002/9780470316658

Motivation

Nonlinear filtering asks for the conditional law of an unobserved Markov process given noisy partial observations of it. It is the computational core of data assimilation in weather forecasting, oceanography and geophysics, of target tracking, and of inference in large networked systems. The standard numerical method, the particle filter, replaces the conditional law by a cloud of $N$ weighted samples. Its error is well understood in fixed dimension, but in practice it degrades exponentially in the dimension of the state: the number of particles needed for a fixed accuracy grows exponentially with the number of variables. This phenomenon, the curse of dimensionality of particle filters, has been documented empirically and analysed by Bickel, Li and Bengtsson and by Snyder et al. (Bickel–Li–Bengtsson 2008; Snyder et al. 2008), and it is a main obstacle to their use in high-dimensional data assimilation.

Rebeschini and van Handel (arXiv:1301.6585v2, Ann. Appl. Probab. 25(5), 2015) gave the first rigorous proof that a local variant of the particle filter, the block particle filter, has an approximation error that does not depend on the model dimension, for models with local interactions above a mixing threshold. The result is the standard theoretical reference for localization in sequential Monte Carlo.

Setting

Let $G=(V,E)$ be a finite graph with graph distance $d$, and fix a neighbourhood size $r\ge1$. The $r$-neighbourhood of a vertex is $N(v)=\{v':d(v,v')\le r\}$, and the $r$-inner boundary of $J\subseteq V$ is $\partial J=\{v\in J:N(v)\not\subseteq J\}$. Each vertex carries a Polish state space $\mathbb X^v$ with a reference measure $\psi^v$, and an observation space $\mathbb Y^v$; write $\mathbb X=\prod_v\mathbb X^v$ and $\psi=\bigotimes_v\psi^v$.

The hidden process $(X_n)_{n\ge0}$ is a Markov chain on $\mathbb X$ with transition density $p(x,z)=\prod_{v}p^v(x,z^v)$ with respect to $\psi$, where each $p^v(x,z^v)$ depends on $x$ only through $x^{N(v)}$ (locality). The observation $Y_n$ has density $g(x,y)=\prod_v g^v(x^v,y^v)$ given $X_n=x$. For a fixed observation sequence, the filter is the recursion

$$\pi_0=\delta_x,\qquad \pi_n=\mathsf C_n\mathsf P\pi_{n-1},$$

where $\mathsf P$ applies the transition kernel and $\mathsf C_n$ reweights by $g(\cdot,Y_n)$ and renormalizes (the Bayes formula).

A partition $\mathcal K$ of $V$ into blocks defines the blocking operator $\mathsf B\rho=\bigotimes_{K\in\mathcal K}\mathsf B^K\rho$, which replaces a measure by the product of its block marginals. The block particle filter with $N$ particles is

$$\hat\pi_n=\mathsf C_n\mathsf B\mathsf S^N\mathsf P\hat\pi_{n-1},$$

where $\mathsf S^N$ replaces a measure by the empirical measure of $N$ i.i.d. samples from it. The local quantities are $|\mathcal K|_\infty=\max_K\operatorname{card}K$, $\Delta=\max_v\operatorname{card}N(v)$, and $\Delta_{\mathcal K}=\max_K\operatorname{card}\{K':d(K,K')\le r\}$. The error is measured locally:

$$|||\rho-\rho'|||_J=\sup_{f\in\mathbb X^J,\,|f|\le1}\mathbf E\big[|\rho(f)-\rho'(f)|^2\big]^{1/2},$$

where $\mathbb X^J$ is the class of measurable functions depending only on the coordinates in $J$.

Formalization targets

Goal: Theorem 2.1

There is $0<\varepsilon_0<1$ depending only on $(\Delta,\Delta_{\mathcal K})$ such that, if $\varepsilon_0<\varepsilon<1$, $0<\kappa<1$, $\varepsilon\le p^v\le\varepsilon^{-1}$ and $\kappa\le g^v\le\kappa^{-1}$, then for all $n\ge0$, $x\in\mathbb X$, $K\in\mathcal K$, $J\subseteq K$,

$$|||\pi^x_n-\hat\pi^x_n|||_J\le\alpha\operatorname{card}J\Big[e^{-\beta_1d(J,\partial K)}+\frac{e^{\beta_2|\mathcal K|_\infty}}{\sqrt N}\Big],$$

with $0<\alpha,\beta_1,\beta_2<\infty$ depending only on $(\varepsilon,\kappa,r,\Delta,\Delta_{\mathcal K})$. The goal states the constants existentially, as the paper does, so that it survives any improvement of them.

Milestones

The proof splits the error through the block filter $\tilde\pi_n=\mathsf C_n\mathsf B\mathsf P\tilde\pi_{n-1}$:

1. elementary lemmas: Lemma 4.1 (minorization), Lemma 4.2 (reweighting), Lemma 4.3 (weighted Neumann series);
2. Theorem 3.1, the Dobrushin comparison theorem;
3. Theorem 4.14, the bias term $\|\pi^x_n-\tilde\pi^x_n\|_J\le\frac{8e^{-\beta}}{1-e^{-\beta}}(1-\varepsilon^{2\Delta})\operatorname{card}J\,e^{-\beta d(J,\partial K)}$;
4. Proposition 4.17, stability of the block filter from product initial laws;
5. Lemma 4.19, Lemma 4.20 (products of empirical measures) and Proposition 4.22, the one-step sampling errors;
6. Theorem 4.23, the variance term $|||\tilde\pi^x_n-\hat\pi^x_n|||_J\le\operatorname{card}J\,\frac{64\Delta_{\mathcal K}e^\beta}{1-e^{-\beta}}\frac{\varepsilon^{-4|\mathcal K|_\infty}\kappa^{-4|\mathcal K|_\infty\Delta_{\mathcal K}}}{\sqrt N}$.

Theorems 4.14 and 4.23 together give Theorem 2.1 by the triangle inequality.

Significance

The theorem shows that the error of a local particle filter can be controlled by quantities that are local in the graph: neither the assumptions nor the bound depend on the time horizon or on $\operatorname{card}V$. On a square lattice, choosing blocks of side length of order $\log N$ balances the two terms and gives a local error, at most locations, that tends to zero as $N\to\infty$ uniformly in time and in the lattice size (the paper's Corollary 2.5, which is not part of this mission): the number of particles needed for a given local accuracy does not grow with the dimension. The result identifies decay of correlations of the filter, established through the Dobrushin comparison theorem, as the mechanism that makes localization work, and it underlies later work on local particle filters and their spatial bias.

The result is proved on paper. No part of it is formalized, and the formal library has no nonlinear filter, no particle filter and no Dobrushin comparison theorem. The mission produces machine-checked statements of the main theorem and of the intermediate results of its proof, with explicit constants for the two halves; proofs of any milestone, or of the goal from Theorems 4.14 and 4.23, are the remaining work.

Difficulty

The obvious argument fails in two places. First, the standard particle filter error bound is uniform in time only through filter stability, and its constants are exponential in the dimension, because the reweighting step compares likelihoods over all of $V$ at once. Localizing the sampling (blocking) removes this, but introduces a bias at block boundaries that must not accumulate over time. Controlling that bias requires showing that the filter has decay of correlations uniformly in time, which is a statement about conditional distributions of a high-dimensional measure, not about its marginals. Second, the sampling error must be propagated through the block filter dynamics in a norm strong enough to compose: the weak $|||\cdot|||$ norm does not contract under the block filter, which is why the paper measures one-step errors in total variation after one further step of dynamics.

Formalization scope

The Lean development is in the namespace LocalPF.Block. Committed conventions:

• the graph distance takes values in $\mathbb N\cup\{\infty\}$, and $e^{-\beta d}=0$ for $d=\infty$; the partition is a surjective block label map;
• the filter, block filter and block particle filter are defined by their recursions for a fixed observation sequence, and every statement holds for every observation sequence (Remark 2.4); the reference measure of the observations is omitted;
• the block particle filter is represented by the law of its particle array at each step, built with the Giry monad bind, and the step-$n$ estimate as a function of that array;
• total variation norms $\|\cdot\|$, $\|\cdot\|_J$ are suprema in $[0,\infty]$; $|||\cdot|||_J\le B$ is stated as $\mathbf E[|\rho(f)-\rho'(f)|^2]\le B^2$ for every test function, with lower Lebesgue integrals;
• $r\ge1$ and $N\ge1$; reference measures are $\sigma$-finite.

Added or changed hypotheses, each disclosed in the item: strict positivity and integrability of $g^v$ in Theorem 4.14 and Proposition 4.17 (the paper assumes no bounds on $g$ there; without them the Bayes formula is undefined); explicit bounds $0<a\le\Lambda\le b$ in Lemma 4.2, whose $|||\cdot|||$ clause is stated for Giry-measurable random probability measures; $\varepsilon<1$ in Theorem 4.23, excluding only the case where the paper's bound is $+\infty$; Lemma 4.19 and Proposition 4.22 are stated for every deterministic probability measure in place of the random previous estimate, which is stronger.

The statement admits no trivializing reading: the constants of Theorem 2.1 are quantified before the graph and the model, so they cannot depend on $\operatorname{card}V$; the goal and Theorem 4.23 assert that the particle-array law is a probability measure, so a zero law cannot make the expectation vanish; test functions are measurable and bounded, so the integrals are not junk values; $N\ge1$ excludes division by $\sqrt0$; and the correction step's normalizer is positive and finite under the stated hypotheses.

Needed infrastructure: product measures over finite index sets and their marginals, the Giry monad and measurability of the maps it composes, conditional distributions on products of Polish spaces, and matrix Neumann series. The Dobrushin comparison theorem and the V-statistic bound (Lemma 4.20) are reusable beyond filtering. Proofs of any milestone are welcome, and so are formal statements of the remaining results of §4 (Propositions 4.4, 4.8, 4.9, Corollary 4.13).

Selected references

• P. Rebeschini and R. van Handel, Can local particle filters beat the curse of dimensionality?, Ann. Appl. Probab. 25(5), 2809–2866, 2015. arXiv:1301.6585, doi:10.1214/14-AAP1061
• P. Bickel, B. Li and T. Bengtsson, Sharp failure rates for the bootstrap particle filter in high dimensions, IMS Collections 3, 318–329, 2008. doi:10.1214/074921708000000228
• C. Snyder, T. Bengtsson, P. Bickel and J. Anderson, Obstacles to high-dimensional particle filtering, Monthly Weather Review 136(12), 4629–4640, 2008. doi:10.1175/2008MWR2529.1
• H.-O. Georgii, Gibbs Measures and Phase Transitions, de Gruyter, 2nd ed., 2011 (Theorem 8.20, the Dobrushin comparison theorem). doi:10.1515/9783110250329

Motivation

High-dimensional expanders are simplicial complexes whose local structure forces global mixing. Random walks on their $k$-dimensional faces, the high order random walks, are used to analyse sampling algorithms: the bases-exchange walk on the bases of a matroid is such a walk, and its spectral analysis by Anari, Liu, Oveis Gharan and Vinzant (arXiv:1811.01816) settled the Mihail–Vazirani conjecture on counting matroid bases. Agreement tests and PCP constructions use the same walks (Dinur–Kaufman, FOCS 2017).

Most of these applications use only the second eigenvalue of the walk. Kaufman and Oppenheim (arXiv:1707.02799v3) observe that this eigenvalue cannot be very small, because of natural obstructions such as cochains pulled up from lower dimensions, and ask instead for the whole spectrum and the structure of the eigenvectors. For complexes whose links have both small second eigenvalue and bounded-below smallest eigenvalue (two-sided local spectral expanders), they show that the spectrum of the walk on $k$-faces clusters around $k+1$ explicit values, each cluster corresponding to cochains built from a lower dimension.

Timeline. Garland (1973, doi:10.2307/1970833) introduced the localization method relating global cohomology to spectra of links. Kaufman and Mass (ITCS 2017, arXiv:1604.02947) defined high order random walks and bounded their second eigenvalue. Oppenheim (Discrete Comput. Geom. 2018, arXiv:1709.04431) developed the local spectral expansion framework and its trickle-down theorem. Kaufman and Oppenheim gave the decomposition theorems this mission formalizes; arXiv v3 (2021) corrects an error of the published version. Alev and Lau (arXiv:2001.02827) later improved the one-sided bounds.

Setting

Let $X$ be a pure $n$-dimensional finite simplicial complex on a vertex set $V$: a finite family of finite subsets of $V$, closed under subsets, in which every face lies in a face with $n+1$ vertices. $X(k)$ is the set of faces with $k+1$ vertices, and $X(-1)=\{\emptyset\}$. A weight is a function $m:X\to(0,\infty)$ with $m(\tau)=\sum_{\sigma\in X(k+1),\,\tau\subseteq\sigma}m(\sigma)$ for $\tau\in X(k)$, $k\le n-1$.

A $k$-cochain is a function $\phi:X(k)\to\mathbb R$; the space $C^k(X)$ carries the inner product $\langle\phi,\psi\rangle=\sum_{\sigma\in X(k)}m(\sigma)\phi(\sigma)\psi(\sigma)$. $C^k_0(X)$ is the subspace of cochains orthogonal to the constants.

• The signless differential $d_k:C^k\to C^{k+1}$ is $d_k\phi(\sigma)=\sum_{\tau\subset\sigma,\,\tau\in X(k)}\phi(\tau)$, and $d_k^*$ is its adjoint.
• The upper random walk $M^+_k$ on $X(k)$ stays at $\tau$ with probability $\frac1{k+2}$ and moves to $\tau'$ with probability $\frac{m(\tau\cup\tau')}{(k+2)m(\tau)}$ when $\tau\cup\tau'\in X(k+1)$; equivalently $d_k^*d_k=(k+2)M^+_k$.
• The link of $\tau$ is $X_\tau=\{\eta:\ \eta\cap\tau=\emptyset,\ \tau\cup\eta\in X\}$ with weight $m_\tau(\eta)=m(\tau\cup\eta)$. On its vertices, $(M')^+_{\tau,0}$ is the non-lazy walk; $\mu_\tau$ and $\nu_\tau$ are its second largest and smallest eigenvalues.
• $X$ is a two-sided $\lambda$-local spectral expander if $-\lambda\le\nu_\tau$ and $\mu_\tau\le\lambda$ for every face $\tau$ of dimension $-1,\dots,n-2$.

For $0\le k\le n-1$ the paper defines subspaces of $C^k_0(X)$: $V^0_0=C^0_0$; for $k\ge1$, $V^j_k=d_{k-1}\cdots d_j(C^j_0)$ for $j<k$ and $V^k_k=\ker d^*_{k-1}$; and $U^0_k=V^0_k$, $U^j_k=V^j_k\cap(V^{j-1}_k)^\perp$ for $0<j<k$, $U^k_k=V^k_k$. With $\varepsilon_0=\lambda$ and $\varepsilon_k=2k(1+2k\sqrt k)\varepsilon_{k-1}+(k+1)\lambda$, $P_{U}$ denotes the weighted orthogonal projection onto $U$.

Formalization targets

Goal: Theorem 5.9 (p. 22)

If $\varepsilon_k\le\frac{1}{2(1+2(k+1)\sqrt{k+1})}$ for $0\le k\le n-2$ and $\varepsilon_{n-1}<\frac1{2\sqrt n}$, then for $0\le k\le n-1$

$$\operatorname{Spec}(M^+_k)\subseteq\{1\}\cup\bigcup_{j=0}^{k}\Big[\tfrac{k+1-j}{k+2}-\tfrac{\sqrt{k+1}}{k+2}\varepsilon_k,\ \tfrac{k+1-j}{k+2}+\tfrac{\sqrt{k+1}}{k+2}\varepsilon_k\Big],$$

and an eigenvector $\phi\in C^k_0$ whose eigenvalue lies in the $j$-th interval satisfies $\|\phi-P_{U^j_k}\phi\|\le\frac{\sqrt{k+1}\varepsilon_k}{1-\sqrt{k+1}\varepsilon_k}\|\phi\|$.

Milestones

• the localization identities (Lemma 3.6, Corollary 3.7, Propositions 4.1, 4.2) and the two-sided bound of Lemma 4.3;
• Lemma 5.1 and the orthogonal decomposition $C^k_0(X)=U^k_k\oplus\cdots\oplus U^0_k$ (§5.3);
• Theorem 5.6: $\|d^*_kd_kP_{U^j_k}\phi-(k+1-j)P_{U^j_k}\phi\|\le\varepsilon_k\|P_{U^j_k}\phi\|$;
• Corollary 5.8: the same for $M^+_k$, with $\frac{k+1-j}{k+2}$ and $\frac{\varepsilon_k}{k+2}$.

Significance

The result. Theorem 5.9 describes the spectrum of $M^+_k$, not only its second eigenvalue. The eigenvalue $\frac{k+1-j}{k+2}$ is the one carried by cochains pulled up from dimension $j$, so it explains which cochains are shrunk slowly by the walk and which quickly. It is the two-sided counterpart of the paper's one-sided mixing bound (Theorem 5.4, the subject of the first mission in this series). It gives approximate eigenspaces explicitly, which a mixing-time analysis or an agreement-test analysis can use in place of a bound on a single eigenvalue.

Formalizing it. No machine-checked development of simplicial-complex random walks, Garland's method, or local spectral expansion is known to exist; Mathlib has simplicial complexes in a geometric sense but no weighted cochain calculus. The mission produces the cochain calculus of §2–§4 together with the spectral statements of §5.3. The statements are those of the arXiv v3 preprint. They are published results but have not been formalized.

Difficulty

The obvious route would show that the spaces $U^j_k$ are exact eigenspaces. That holds for the complete complex but not in general: $d^*d$ maps $U^j_k$ only approximately into itself, and the error has to be controlled through every lower dimension at once. Theorem 5.6 is an induction on $k$ in which the error $\varepsilon_{k-1}$ of dimension $k-1$ enters dimension $k$ multiplied by norms of $d^*_{k-1}d_{k-1}$ and its square root. Controlling these factors on the correct subspaces, rather than on all of $C^{k-1}$, is the delicate step: $d^*_{k-1}d_{k-1}=(k+1)M^+_{k-1}$ has norm $k+1$ on $C^{k-1}(X)$, attained on the constants, and the bound needed is on the complement of the constants. Passing from Corollary 5.8 to the spectral statement of Theorem 5.9 needs the intervals to be disjoint and the eigenvector to be split along the orthogonal decomposition.

Formalization scope

• Encoding. Faces are Finset V and $X$ is a Finset (Finset V); faces are indexed by their number of vertices (cells X (k + 1) is $X(k)$). Cochains are functions Finset V → ℝ, and every operator vanishes off $X$.
• Supports. Subspaces, eigenvectors and orthogonal complements consist of functions supported on $X(k)$ (Supp X (k + 1)). Without this, a function living off the faces would have norm $0$, would be an eigenvector with eigenvalue $0$, and would make the spectral statement false; a formalization without supports is ruled out for this reason.
• Weights and adjoints. The weight is strictly positive on faces. $d^*$ is defined by its explicit formula, and Lemma 3.6 states that this formula is the adjoint.
• Expansion. The eigenvalue conditions on links are stated in Rayleigh form on the weighted complement of the constants, $|\langle(M')^+_{\tau,0}g,g\rangle|\le\lambda\|g\|^2$; this encodes $-\lambda\le\nu_\tau$ and $\mu_\tau\le\lambda$ and needs no connectivity. Definition 1.2 is followed where Definition 4.4 misprints the two-sided clause.
• Projections. $P_U\phi$ is characterised relationally (IsWProj: $u\in U$ and $\phi-u\perp U$) instead of by an operator. On these finite-dimensional subspaces it exists and is unique.
• Indices and constants. $\varepsilon_k$ is eps lam k, with the recursion shifted by one index. $k$ is quantified inside each conclusion, and $\varepsilon_{n-1}$ is written without natural subtraction. The statements follow the printed constants of arXiv v3.

A complete development needs finite-dimensional weighted inner-product spaces of cochains, Garland localization, Courant–Fischer for self-adjoint operators on these spaces, and orthogonal projections onto images of iterated differentials. The cochain calculus and the localization identities are reusable for any weighted simplicial complex, and the first mission of this series needs the same objects. Proofs of the localization identities, of the decomposition, and of any milestone are welcome, as are proofs of the results with weaker hypotheses.

Selected references

• T. Kaufman, I. Oppenheim, High Order Random Walks: Beyond Spectral Gap, arXiv:1707.02799v3, 2021. https://arxiv.org/abs/1707.02799
• H. Garland, p-adic curvature and the cohomology of discrete subgroups of p-adic groups, Annals of Mathematics 97, 1973. https://doi.org/10.2307/1970833
• T. Kaufman, D. Mass, High dimensional random walks and colorful expansion, ITCS 2017. https://arxiv.org/abs/1604.02947
• I. Oppenheim, Local spectral expansion approach to high dimensional expanders Part I: Descent of spectral gaps, Discrete & Computational Geometry 59, 2018. https://arxiv.org/abs/1709.04431
• N. Anari, K. Liu, S. Oveis Gharan, C. Vinzant, Log-concave polynomials II: high-dimensional walks and an FPRAS for counting bases of a matroid, STOC 2019. https://arxiv.org/abs/1811.01816
• V. L. Alev, L. C. Lau, Improved analysis of higher order random walks and applications, STOC 2020. https://arxiv.org/abs/2001.02827

Motivation

A high dimensional expander is a simplicial complex whose local structure forces global expansion. The high order random walks on such a complex move from a $k$-face to a $k$-face through a common $(k+1)$-face. They were studied for their connection to agreement tests in probabilistically checkable proofs (Dinur–Kaufman 2017; Kaufman–Mass 2017), and they later became a tool for sampling. Anari, Liu, Oveis Gharan and Vinzant (arXiv:1811.01816) used the mixing bound of this mission to prove the Mihail–Vazirani conjecture: the bases-exchange walk of every matroid mixes rapidly.

Timeline:

• 1973. Garland (Ann. of Math. 97) shows that spectral gaps in the links of a complex control its cohomology. Inner products are localized to links; this is now called Garland's method.
• 2017. Kaufman and Mass (arXiv:1604.02947) bound the second eigenvalue of the high order walks on complexes with well-expanding links. Dinur and Kaufman obtain the optimal bound under a two-sided spectral gap in the links, as Kaufman–Oppenheim explain.
• 2018. Oppenheim (Discrete Comput. Geom. 59) shows how spectral gaps descend from top-dimensional links to lower ones ("trickling down").
• 2017–2021. Kaufman and Oppenheim (arXiv:1707.02799v3) obtain the optimal mixing bound under a one-sided gap only: negative eigenvalues of the links do not matter. This is the target of this mission.

Setting

Let $V$ be a type of vertices. A pure $n$-dimensional finite simplicial complex $X$ is a finite family of finite subsets of $V$ that is closed under subsets, has faces of at most $n+1$ elements, and has every face contained in a face of exactly $n+1$ elements. A face with $k+1$ elements is a $k$-face; $X(k)$ is the set of $k$-faces, and $X(-1)=\{\emptyset\}$.

A weight function is a map $m$ from the faces of $X$ to $(0,\infty)$ that is balanced: for $-1\le k\le n-1$ and $\tau\in X(k)$,

$$m(\tau)=\sum_{\sigma\in X(k+1),\ \tau\subseteq\sigma}m(\sigma).$$

A $k$-cochain is a function $\phi:X(k)\to\mathbb R$. The cochains carry the inner product $\langle\phi,\psi\rangle=\sum_{\sigma\in X(k)}m(\sigma)\phi(\sigma)\psi(\sigma)$ and the norm $\|\cdot\|$. The cochains orthogonal to the constants form $C^k_0(X,\mathbb R)=\{\phi:\sum_{\sigma\in X(k)}m(\sigma)\phi(\sigma)=0\}$.

The upper random walk $M^+_k$ acts on $k$-cochains by

$$M^+_k\phi(\tau)=\frac{1}{k+2}\,\phi(\tau)+\sum_{\tau'\in X(k),\ \tau\cup\tau'\in X(k+1)}\frac{m(\tau\cup\tau')}{(k+2)\,m(\tau)}\,\phi(\tau').$$

It stays put with probability $1/(k+2)$, and otherwise moves to a neighbouring $k$-face with probability proportional to the weight of their union.

The link of a face $\tau$ is $X_\tau=\{\eta\in X:\eta\cap\tau=\emptyset,\ \tau\cup\eta\in X\}$, weighted by $m_\tau(\eta)=m(\tau\cup\eta)$. On the vertices of $X_\tau$, the non-lazy upper walk $(M')^+_{\tau,0}=2M^+_{\tau,0}-I$ is the weighted random walk on the 1-skeleton of the link. Let $\mu_\tau$ be its second largest eigenvalue. $X$ is a one-sided $\lambda$-local spectral expander if $\mu_\tau\le\lambda$ for every face $\tau$ of dimension $-1,\dots,n-2$. The empty face is included, and its link is $X$ itself.

Formalization targets

Goal: Theorem 5.4 (p. 17)

Let $0\le\lambda\le1$ and let $X$ be a one-sided $\lambda$-local spectral expander. Then for every $0\le k\le n-1$ and every $\phi\in C^k_0(X,\mathbb R)$,

$$\|M^+_k\phi\|\le\Big(\frac{k+1}{k+2}+\frac{k+1}{2}\,\lambda\Big)\|\phi\|.$$

Milestones

They follow the paper's proof order:

• Lemma 3.6 and Corollary 3.7: the adjoint $d^*$ of the signless differential $d$, and the factorizations $d^*d=(k+2)M^+_k$, $dd^*=(k+1)M^-_k$.
• Proposition 4.1 (1)–(3), Garland's localization identities, and Proposition 4.2:

$$\|d\phi\|^2=\|d^*\phi\|^2+\|\phi\|^2+\sum_{\tau\in X(k-1)}\langle (M')^+_{\tau,0}(I-M^-_{\tau,0})\phi_\tau,\phi_\tau\rangle .$$

• Lemma 4.3, which bounds the link terms by $(k+1)\mu\|\phi\|^2$.
• Lemma 5.1.
• Theorem 5.2 (the Decomposition Theorem).
• Corollary 5.3, in its general and its one-sided form:

$$\|d\phi\|^2\le\sum_{j=0}^{k}\Big(k+1-j+\frac{(k+j+2)(k+1-j)}{2}\lambda\Big)\|\phi^j\|^2,\qquad \|\phi\|^2=\sum_{j=0}^k\|\phi^j\|^2.$$

Significance

The result. The coefficient $\frac{k+1}{k+2}$ is the baseline in the paper's mixing bound, and the bound is optimal up to the $O(\lambda)$ term. It needs a gap on one side only: links may have eigenvalues near $-1$. This matters in two places. The links of a matroid's independence complex are only one-sided expanders, so the matroid application needs exactly this case. And the links of Ramanujan complexes are one-sided expanders, so this bound gives optimal mixing on them; the two-sided bound of Dinur–Kaufman does not apply to them.

Formalizing it. The theorem is proved on paper; the Lean statements in this mission are proof targets. Completing the mission would give machine-checked proofs of the mixing bound, Garland's localization identities, and the Decomposition Theorem, built on definitions of weighted simplicial complexes, links, and their random walks. Lemma 4.3 and Corollary 5.3 are stated with a correction: as printed they are false when a link eigenvalue bound is negative (see Formalization scope).

Difficulty

The obvious argument fails. The tempting route bounds the second eigenvalue of $M^+_k$ directly from the link spectra, by induction on $k$. But $M^+_k$ has large eigenvalues near $\frac{k+1-j}{k+2}$ for every $j$, coming from cochains of the form $d\psi$ with $\psi$ of lower degree. A single spectral-gap estimate cannot separate these levels from one another. The paper instead splits $\phi$ into contributions from every degree $j\le k$; this is the Decomposition Theorem, and each piece is controlled separately. Formally, the main costs are:

• the double-counting behind Proposition 4.1 (Appendix A, pp. 28–29);
• a square root of a positive self-adjoint operator on a weighted finite-dimensional space (Theorem 5.2);
• the bookkeeping of degrees and links.

Formalization scope

Faces are Finset V. $X$ is a Finset (Finset V), and $X(k)$ is cells X (k + 1): faces are indexed by their number of vertices. Cochains are functions Finset V → ℝ that are read only on the relevant faces. Every operator is zero off $X$. The weight is positive on faces; the paper writes $\mathbb R^+$, and $m$ appears in denominators. Every goal-level statement carries the standing assumption of §2: $X$ is pure $n$-dimensional and $m$ is a weight. Orthogonality to the constants is always weighted by $m$ (or by $m_\tau$ in a link).

The adjoint $d^*$ is defined by its explicit formula; that it is the adjoint is Lemma 3.6. The eigenvalue condition $\mu_\tau\le\lambda$ is stated in Rayleigh form: $\langle (M')^+_{\tau,0}g,g\rangle\le\lambda\|g\|^2$ for every $g$ on the vertices of $X_\tau$ that is $m_\tau$-orthogonal to the constants. It is equivalent to the eigenvalue form even for disconnected links. A Rayleigh bound over all $g$, constants included, would be unsatisfiable for $\lambda<1$ and would make the goal vacuous; it is ruled out. The predicate quantifies over every face of dimension $-1$ to $n-2$, including $\emptyset$.

Corrections, all disclosed in the items:

• Lemma 4.3 is stated with a bound $\mu\ge\max(\mu_k,0)$. The printed version with $\mu_k<0$ fails already for the complete graph on three vertices.
• Corollary 5.3 accordingly takes $\mu_i\ge0$ and $\lambda\ge0$. Its two formal statements retain the page's assumption that every link of dimension at least one is connected, including $X$ itself.
• The proof of Theorem 5.4 ends with $(k+1)\lambda$; the statement's $\frac{k+1}{2}\lambda$ is formalized.

Welcome contributions: proofs of any milestone. Reusable lemmas on finite weighted inner products, on double counting over faces of a Finset (Finset V), and on links are useful beyond this mission; the companion mission on two-sided expanders uses the same objects.

Selected references

• T. Kaufman, I. Oppenheim, High Order Random Walks: Beyond Spectral Gap, arXiv:1707.02799v3, 2021. https://arxiv.org/abs/1707.02799
• N. Anari, K. Liu, S. Oveis Gharan, C. Vinzant, Log-concave polynomials II: High-dimensional walks and an FPRAS for counting bases of a matroid, STOC 2019. https://arxiv.org/abs/1811.01816
• H. Garland, p-adic curvature and the cohomology of discrete subgroups of p-adic groups, Ann. of Math. 97:375–423, 1973. https://doi.org/10.2307/1970781
• T. Kaufman, D. Mass, High dimensional random walks and colorful expansion, ITCS 2017. https://arxiv.org/abs/1604.02947
• I. Oppenheim, Local spectral expansion approach to high dimensional expanders Part I: Descent of spectral gaps, Discrete Comput. Geom. 59(2):293–330, 2018. https://arxiv.org/abs/1709.04431

Motivation

Bayesian inverse problems for functions — the initial condition of a PDE, a permeability field, a diffusion coefficient — lead to posterior measures $\mu$ on an infinite-dimensional Hilbert space $H$, given by a density $\exp(-\Phi)$ with respect to a Gaussian prior $\gamma$. In practice $\mu$ is sampled by Markov chain Monte Carlo on an $m$-dimensional discretisation $\mu_m$, and the question that matters is whether the sampler's convergence rate survives the limit $m\to\infty$. For the standard random-walk Metropolis algorithm it does not (mission III of this series). The preconditioned Crank–Nicolson (pCN) algorithm, whose proposal preserves $\gamma$, was introduced to avoid this (Beskos, Roberts, Stuart and Voss 2008; Cotter, Roberts, Stuart and White 2013).

Hairer, Stuart and Vollmer (2014) prove that pCN has a Wasserstein spectral gap that is uniform in the dimension. Mission I of this series covers their result for globally Lipschitz potentials $\Phi$ (Theorem 2.12). This mission covers Theorem 2.14, which needs only that $\Phi$ be locally Lipschitz, with a local Lipschitz constant growing slower than any exponential. That class contains potentials of polynomial growth, which arise for nonlinear forward maps.

Setting

$H$ is a separable real Hilbert space with a centred Gaussian measure $\gamma$, and $(e_i)_{i\ge0}$ is an orthonormal basis of eigenvectors of the covariance of $\gamma$. $P_mH$ is the span of $e_0,\dots,e_{m-1}$, and $\gamma_m$ is the image of $\gamma$ under the orthogonal projection onto $P_mH$. For a potential $\Phi:H\to\mathbb R$ the targets are

$$\mu(dx)\propto e^{-\Phi(x)}\gamma(dx),\qquad \mu_m(dx)\propto e^{-\Phi(x)}\gamma_m(dx).$$

Fix a step size $\delta\in(0,\tfrac12]$ and put $\rho=1-(1-2\delta)^{1/2}$. One pCN step from $x$ draws $\xi\sim\gamma$ and proposes $p_x=(1-2\delta)^{1/2}x+\sqrt{2\delta}\,\xi$. The proposal is accepted with probability $\alpha(x,p_x)=1\wedge\exp(\Phi(x)-\Phi(p_x))$; otherwise the chain stays at $x$. Its transition kernel is $\mathcal P$. The kernel $\mathcal P_m$ is the same algorithm on $P_mH$ with $\xi\sim\gamma_m$.

Distances between probability measures are Wasserstein lifts of a cost $c$: $c(\nu_1,\nu_2)=\inf_\pi\int c\,d\pi$ over couplings $\pi$ of $\nu_1,\nu_2$. A kernel is $d$-contracting if $d(x,y)<1$ implies $d(\mathcal P(x,\cdot),\mathcal P(y,\cdot))\le c\,d(x,y)$ for a fixed $c<1$. A set $S$ is $d$-small if $d(\mathcal P(x,\cdot),\mathcal P(y,\cdot))\le s<1$ for all $x,y\in S$.

The distance of this mission is a weighted path length (3.6). For unit-speed $C^1$ paths $\psi:[0,T]\to H$ from $x$ to $y$,

$$\bar d(x,y)=\inf_{T,\psi}\frac1\varepsilon\int_0^T e^{\eta\|\psi(t)\|}\,dt,\qquad d=1\wedge\bar d,\qquad \tilde d(x,y)=\sqrt{d(x,y)\,(1+V(x)+V(y))},$$

with $V(x)=\|x\|^i$ ($i\ge1$) or $V(x)=e^{v\|x\|}$ ($v>0$).

There are two assumptions. Assumption 2.10 says that for $\|x\|\ge R$ every proposal within distance $r(\|x\|)$ of the proposal mean $(1-\rho)x$ is accepted with probability at least $e^{\alpha_l}$, where $r(s)\le\frac\rho2 s$. Assumption 2.13 says that $e^{-\Phi}$ is $\gamma$-integrable and that $\varphi(r)=\sup_{x\ne y\in B_r(0)}|\Phi(x)-\Phi(y)|/\|x-y\|\le M_\kappa e^{\kappa r}$ for every $\kappa>0$.

Formalization targets

Goal: Theorem 2.14

Under Assumption 2.10 with $r(s)=r s^a$ ($r>0$, $a\in(\frac12,1)$) and Assumption 2.13:

1. $\mu$ and every $\mu_m$ are the unique invariant probability measures of $\mathcal P$ and $\mathcal P_m$.
2. For $\eta$ small enough and then $\varepsilon$ small enough, there is one $\tilde n$ such that for every $m$ and all probability measures $\nu_1,\nu_2$

$$\tilde d(\nu_1\mathcal P^{\tilde n},\nu_2\mathcal P^{\tilde n})\le\tfrac12\tilde d(\nu_1,\nu_2),\qquad \tilde d(\nu_1\mathcal P_m^{\tilde n},\nu_2\mathcal P_m^{\tilde n})\le\tfrac12\tilde d(\nu_1,\nu_2).$$

The essential point is that $\tilde n$ does not depend on $m$.

Milestones

• Lemma 3.5 (1)–(3): the comparison of $\bar d$ with $\|x-y\|e^{\eta(\|x\|\vee\|y\|)}/\varepsilon$, and the contraction of $\bar d$ under a common-noise pCN step,

$$\bar d(p_x,p_y)\le(1-2\delta)^{1/2}e^{\eta[-\rho(\|x\|\vee\|y\|)+\sqrt{2\delta}\|\xi\|+J]}\bar d(x,y).$$

• Lemma 3.6: $\mathcal P$ and every $\mathcal P_m$ are $d$-contracting with one constant.
• Lemma 3.7: bounded sets are $d$-small for $\mathcal P^n$ and every $\mathcal P_m^n$, with $n$ and $s$ independent of $m$.

The paper derives Theorem 2.14 from these, from Lemma 3.2 (Lyapunov functions) and from Proposition 2.6 (the weak Harris theorem of Hairer, Mattingly and Scheutzow 2011). The last two are posed in mission I of this series.

Significance

A Wasserstein spectral gap uniform in $m$ means that the number of pCN steps needed to reach a given accuracy does not grow with the discretisation level. In §4 of the paper this yields a strong law of large numbers and a central limit theorem for pCN ergodic averages, and, combined with Theorem 2.15, an $L^2_\mu$-spectral gap and mean-square error bounds, all uniform in the dimension. The locally Lipschitz case is the one that covers potentials of polynomial growth.

The result is proved in the paper. It has not been formalized. A formalization would produce a reusable weak-Harris toolkit for Markov kernels on Polish spaces, and a machine-checked account of the path-metric construction, which the paper adapts from Hairer and Majda (2010) and Hairer, Mattingly and Scheutzow (2011). It would also check the paper's proof, whose printed Lemma 3.5 (3) contains a typographical slip in the exponent; the formalized bound is the one the proof derives.

Difficulty

With $\Phi$ only locally Lipschitz, no single $\varepsilon$ makes $1\wedge\|x-y\|/\varepsilon$ contracting. The probability that exactly one of two coupled chains accepts is controlled by $|\Phi(x)-\Phi(y)|$, and far from the origin this exceeds any fixed multiple of $\|x-y\|$. The weighted path distance makes far-out points "close" only when they are very close in norm. But then even the "both accept" move can increase the distance, because the weight $e^{\eta\|\cdot\|}$ changes along the move. Showing that the shrinkage $(1-\rho)$ of the proposal mean beats this, while the Gaussian noise term stays integrable uniformly in $m$, is the content of Lemmas 3.5 and 3.6. The order of the choices ($R$, then $\eta$, then $\varepsilon$) is essential.

Formalization scope

• $H$ is a real Hilbert space that is complete, separable and Borel. $\gamma$ is Mathlib's IsGaussian with mean zero. $(e_i)$ is a HilbertBasis ℕ whose vectors are pairwise uncorrelated under the covariance bilinear form.
• $P_mH$ is a submodule. $\gamma_m$ is the pushforward under the orthogonal projection. $\mathcal P_m$ lives on the subtype $P_mH$, with $\Phi$ and $V$ restricted to it and $d$ restricted from $H$.
• $\mu$ and $\mu_m$ are Mathlib's normalised tilted measures. The goal concludes that they are probability measures.
• The Metropolis–Hastings kernel is built from Mathlib's Kernel.withDensity. Kernel powers are composition powers, and $\nu\mathcal P^n$ is Measure.bind.
• Wasserstein lifts and $\bar d$ are infima in $[0,\infty]$, so no junk zero arises from an empty or unbounded set. Unit speed is imposed on $(0,T)$, so $\bar d(x,x)=0$ through the constant path with $T=0$.
• Contraction, smallness and Lyapunov constants are explicit arguments. "Uniform in $m$" is "one constant for all $m$".
• "Small enough" is $\exists\eta_0>0\ \forall\eta\in(0,\eta_0]\ \exists\varepsilon_0>0\ \forall\varepsilon\in(0,\varepsilon_0]$.
• Several readings are disclosed. "$r\in\mathbb R$" is read as $r>0$, $i\in\mathbb N$ as $i\ge1$, and $v>0$. Assumption 2.10 is stated for $s\ge0$, the domain of $r$, and requires $r(s)>0$ for $s>0$ so that the acceptance balls are nonempty. Its infimum and the supremum $\varphi(r)$ of Assumption 2.13 are stated pointwise.
• The general form of Lemma 3.6 has a disclosed radius-floor hypothesis: $r(s)$ stays bounded away from zero for large $s$. The printed proof needs a uniform positive probability for the proposal ball; this hypothesis supplies it. Theorem 2.14's power-law radius already meets it.
• The formalization rules out trivialising readings. The tilted measure cannot be the zero measure, because the goal asserts it is a probability measure. Uniqueness is among probability measures. $V\equiv1$ is excluded. A $\tilde n$ chosen after $m$ would give a per-dimension gap, not this theorem.
• A complete development needs:
  • the weak Harris theorem (Proposition 2.6, mission I);
  • Gaussian tail bounds of Fernique type, with the dimension-monotonicity of Lemma 3.1 (mission I);
  • the Lyapunov drift Lemma 3.2 (mission I);
  • calculus of $C^1$ paths in Hilbert space;
  • synchronous couplings of Metropolis–Hastings kernels.
• The Harris and coupling layers are reusable well beyond this paper. Contributions to any of them are welcome.

Selected references

• M. Hairer, A. M. Stuart and S. J. Vollmer, Spectral gaps for a Metropolis–Hastings algorithm in infinite dimensions, arXiv:1112.1392v4 (2014), published in Ann. Appl. Probab. 24(6) (2014) 2455–2490, https://doi.org/10.1214/13-AAP982. https://arxiv.org/abs/1112.1392v4
• M. Hairer, J. C. Mattingly and M. Scheutzow, Asymptotic coupling and a general form of Harris' theorem with applications to stochastic delay equations, Probab. Theory Related Fields 149 (2011) 223–259. MR2773030, https://mathscinet.ams.org/mathscinet-getitem?mr=2773030
• M. Hairer and A. J. Majda, A simple framework to justify linear response theory, Nonlinearity 23 (2010) 909–922. MR2602020, https://mathscinet.ams.org/mathscinet-getitem?mr=2602020
• A. Beskos, G. O. Roberts, A. M. Stuart and J. Voss, MCMC methods for diffusion bridges, Stoch. Dyn. 8 (2008) 319–350. MR2444507, https://mathscinet.ams.org/mathscinet-getitem?mr=2444507
• S. L. Cotter, G. O. Roberts, A. M. Stuart and D. White, MCMC methods for functions: modifying old algorithms to make them faster, Statist. Sci. 28 (2013) 424–446. https://doi.org/10.1214/13-STS421