Markov Chain

Motivation

Centralized matching markets (kidney exchange, ride hailing, freight and labor platforms) repeatedly decide which waiting participants to match now and which to hold for a better opportunity later. Matching early collects value sooner; waiting lets the platform see more arrivals and avoid matches that later turn out to be wasteful. A natural yardstick is the best set of matches that could have been made with hindsight from all arrivals up to a given time, and the question is how far an online policy, which cannot see the future, must fall behind that yardstick.

Kerimov, Ashlagi and Gurvich (SSRN 3824407, September 2022; Management Science 2023, doi:10.1287/mnsc.2021.01215) answer this for multi-way matching networks with patient agents. They identify a single parameter of the fluid relaxation, the general position gap $\epsilon$, and show that the regret against the hindsight benchmark can be kept at order $\epsilon^{-1}$ at all times, and that no policy does better in order on non-trivial networks. This mission formalizes the upper bound. The paper places itself next to constant-regret results for online packing (Bumpensanti and Wang 2020; Vera and Banerjee 2021), where resolving a linear program at each arrival achieves bounded regret.

Setting

There are $n$ agent types and $d$ matches. Match $m$ is a set $\mathcal A(m)$ of at least two types, every type belongs to some match, and the matching matrix $M\in\{0,1\}^{n\times d}$ has $M_{im}=1$ iff $i\in\mathcal A(m)$. Performing match $m$ uses one agent of each type in $\mathcal A(m)$ and earns $r_m>0$. Time is discrete; at each time $t=1,2,\dots$ one agent arrives, of type $i$ with probability $\lambda_i>0$, $\sum_i\lambda_i=1$, independently over time. $A^t_i$ counts the type-$i$ arrivals by time $t$.

A matching policy records $D^t_m$, the number of times match $m$ has been performed by time $t$. It is admissible when it is non-anticipative and only matches agents present: $MD^t\le A^t$. The pre-match queue is $Q^t=A^t-MD^{t-1}$, the value collected is $\mathcal R^{D,t}=\mathbb E[r\cdot D^t]$, and the hindsight benchmark is

$$\mathcal R^{*,t}=\mathbb E\big[\max\{r\cdot y: My\le A^t,\ y\in\mathbb Z^d_{\ge0}\}\big].$$

The static-planning problem is the linear program

$$\text{(SPP)}\qquad \max\ r\cdot z\quad\text{s.t.}\quad Mz+s=\lambda,\ z\ge0,\ s\ge0.$$

For an optimal $(z^*,s^*)$ let $\mathcal M_+=\{m:z^*_m>0\}$ (active matches), $\mathcal M_0$ the rest (redundant matches), $\mathcal Q_+=\{j:s^*_j>0\}$ (under-demanded types) and $\mathcal Q_0$ the rest (over-demanded types). The network satisfies general position (GP) if (SPP) has a unique optimal solution and it is non-degenerate, $|\mathcal M_+|+|\mathcal Q_+|=n$. The general position gap is the smallest positive basic value,

$$\epsilon=\min_{m\in\mathcal M_+}z^*_m\ \wedge\ \min_{j\in\mathcal Q_+}s^*_j .$$

The exhaustive resolving policy with inter-action delay $\tau$ acts only at the epochs $t_k=k\tau$. There it performs an optimal solution of the integer program $\max\{r\cdot z: Mz\le Q^{t_k},\ z\in\mathbb Z^d_{\ge0}\}$ with the redundant matches removed, and then discards the leftover agents of the under-demanded types.

Formalization targets

Goal: Theorem 3.1 (Upper bound), p. 14

There are constants $\kappa,\Gamma>0$ depending only on $n,d,M,r$ such that, under GP, the exhaustive resolving policy with $\tau=\lceil\kappa\epsilon^{-1}\rceil$ (any tie-breaking) is admissible and

$$\mathcal R^{*,t}-\mathcal R^{D,t}\le\Gamma\,\epsilon^{-1}\qquad\text{for all }t\ge1 .$$

The constants are not fixed, so the goal survives any improvement of them.

Milestones

1. §2, p. 8: $\mathcal R^{*,t}=\max_{D}\mathcal R^{D,t}$, attained by the ultimate batching policy.
2. §4.2, (4), p. 20: under GP the optimal basis $\mathcal B$ is invertible, $(z^*_{\mathcal M_+},s^*_{\mathcal Q_+})=\mathcal B^{-1}\lambda$, and the entries of $\mathcal B^{-1}$ are bounded by a constant of the topology.
3. §4.2, p. 20: $\theta=\sum_{m\in\mathcal M_+}r_my^m$ is the optimal dual of (SPP), $\theta\ge0$, and $\theta_i>0$ on $\mathcal Q_0$.
4. Lemma 4.1, p. 19 (optimality test): a policy without redundant matches whose over-demanded queues have mean $O(\epsilon^{-1})$ has regret $O(\epsilon^{-1})$.
5. Lemma 4.2, p. 21: a Foster–Lyapunov drift condition bounds stationary means (Glynn and Zeevi 2008).
6. (11), p. 23: $\mathbb E_\pi[h^*(Q^0)]=O(\epsilon^{-1})$ for the stationary law of the epoch chain.
7. App. D, p. 49: $\mathbb E_{\mathbf 0}[h^*(Q^{t_k})]=O(\epsilon^{-1})$ for all $k\ge1$.

Here $h^*(u)$ is the $\theta$-weighted leftover in $\mathcal Q_0$ after an optimal integer matching of $u$ (display (7)).

Significance

The upper bound says that, under GP, hindsight-optimal performance up to an additive constant is achievable at every time simultaneously, not just at a known horizon. Long-run average optimality and near-optimality under discounting follow (Remark 2.1). The bound also quantifies the cost of acting often: the delay $\tau$ and the regret both scale with $\epsilon^{-1}$, so networks close to degeneracy force batching. Combined with the paper's lower bound, $\epsilon^{-1}$ is the right order on non-trivial networks.

The result has a printed proof (§4, Appendices B and D) but no machine-checked one. Several intermediate statements of the printed proof do not hold as stated and are not posed here. The goal and the stated displays (11) and App. D are posed as the paper states them, so a formal proof requires a correct argument for the uniform-in-$\lambda$ bound on the over-demanded queues. Lemma 4.1, the basis and duality facts and Lemma 4.2 are self-contained and checkable on their own.

Difficulty

The obvious approach compares the policy's realized matches with the fluid optimum $t\,z^*$ and controls the deviation with concentration bounds. That gives errors of order $\sqrt t$, not a constant. The constant comes from showing that the over-demanded queues stay of order $\epsilon^{-1}$ uniformly in time and in $\lambda$. Between epochs these queues behave like a multidimensional reflected random walk whose drift toward zero is only of order $\epsilon\tau$, while its fluctuations over an epoch are of order $\sqrt\tau$. The delay $\tau\asymp\epsilon^{-1}$ balances the two, but the queue state enters through the integer program (3), whose solution changes discontinuously with the queues, and the quantities that measure the drift are signed combinations of arrival counts, to which the usual one-sided concentration bounds for nonnegative sums do not apply. On top of this every constant must be independent of $\lambda$.

Formalization scope

• Types are Fin n and matches Fin d (0-based); the topology with its two standing assumptions ($|\mathcal A(m)|\ge2$, every type in a match) is a structure, and $\lambda>0$ with $\sum\lambda_i=1$ and $r>0$ are hypotheses.
• Time is $\mathbb N$; "for all $t>0$" is $t\ge1$. The arrival at time $s+1$ is the $s$-th entry of a path $\omega:\mathbb N\to$ Fin n. Expectations at horizon $t$ are finite sums over the first $t$ arrivals weighted by $\prod\lambda_{\omega_s}$, so no expectation is a default value.
• Admissible policies are non-anticipative cumulative counts with $MD^t\le A^t$ and no rejections. The resolving policy's removal of under-demanded leftovers acts on its own virtual queue, which agrees with the actual queue on $\mathcal Q_0$; its matches are feasible without removals, so it is admissible.
• (3) is solved with the redundant matches set to zero, and statements quantify over every tie-breaking selection. A selection exists (a sanity file exhibits one), so these statements are not vacuous.
• GP is a hypothesis on an explicit pair $(z^*,s^*)$; $\epsilon$ is the minimum of the positive basic values. The basis inverse is never a matrix-inverse function: statements assert the existence of a two-sided inverse.
• $h^*$ is defined in the form $\min\{\sum_{\mathcal Q_0}\theta_is_i: Mz+s=u,\ z_{\mathcal M_0}=0\}$, equivalent to (7) under the paper's reduction $\mathcal M_0=\emptyset$; $\theta$ is any solution of the complementary-slackness system, which is unique under GP.
• Every $O(\cdot)$ is an explicit constant, quantified after the topology and $r$ and before $\lambda$. Placing it after $\lambda$ would turn the theorem into a per-instance boundedness statement and is ruled out.
• A trivializing formalization (some unspecified policy, a $\tau$ independent of $\epsilon$, or GP replaced by an unsatisfiable condition) is ruled out: the policy is constructed, $\tau=\lceil\kappa/\epsilon\rceil$, and a sanity file proves GP for the Figure 1 network with $\epsilon=1/5$.
• Not posed: the lower bound of Theorem 3.1, Proposition 4.1 (8)–(9), Lemmas B.1–B.2, Proposition B.1 and displays (21)–(22), which do not hold as printed; Theorem 5.2 and §6.

Contributions welcome: proofs of the LP facts (milestones 2–3) and Lemma 4.1, a Mathlib-ready proof of Lemma 4.2, and any correct argument for the epoch bounds.

Selected references

• S. Kerimov, I. Ashlagi, I. Gurvich, Dynamic Matching: Characterizing and Achieving Constant Regret, SSRN 3824407 (version of Sep 14, 2022); Management Science, 2023. https://ssrn.com/abstract=3824407, https://doi.org/10.1287/mnsc.2021.01215
• P. W. Glynn, A. Zeevi, Bounding stationary expectations of Markov processes, in Markov Processes and Related Topics, IMS Collections 4, 2008. https://doi.org/10.1214/074921708000000381
• P. Bumpensanti, H. Wang, A re-solving heuristic with uniformly bounded loss for network revenue management, Management Science 66, 2020. https://doi.org/10.1287/mnsc.2019.3365
• D. Bertsimas, J. N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997.

Motivation

Sampling from a Gibbs distribution $\pi_U\propto e^{-U}\,d\lambda_d$ on $\mathbb R^d$ is a basic task in Bayesian statistics, statistical physics and machine learning. A standard approach simulates the Langevin diffusion $dX_t=-\nabla U(X_t)\,dt+\sqrt2\,dB_t$, whose invariant distribution is $\pi_U$, through its Euler scheme, and averages a test function $f$ along one long trajectory. The discretization introduces a bias of the order of the step size, so a single-step-size average with accuracy $\varepsilon$ costs more than $\varepsilon^{-2}$ steps. Dalalyan (arXiv:1412.7392) and Durmus–Moulines (arXiv:1605.01559) quantified this for strongly log-concave targets; for occupation measures of the Euler scheme the best previous bound was of order $d\varepsilon^{-4}$ (Durmus–Moulines, Bernoulli 2019, denoted [DM19] in the paper).

Egéa and Panloup (arXiv:2109.07753, Math. Oper. Res., 2025) combine Giles's multilevel Monte Carlo idea (Oper. Res. 2008) with pathwise averages. Each level is one long trajectory, not many independent samples. This mission formalizes their result for a uniformly strongly contractive, twice differentiable drift. In that case the multilevel occupation measure reaches accuracy $\varepsilon$ at a cost of order $d\varepsilon^{-2}$, the order of an unbiased Monte Carlo method.

Setting

Let $b:\mathbb R^d\to\mathbb R^d$ be $L$-Lipschitz and satisfy Assumption $(\mathbf C_\alpha)$: $\langle b(y)-b(x),y-x\rangle\le-\alpha|x-y|^2$ for all $x,y$, with $\alpha\in(0,L\wedge1]$. Let $\sigma>0$. The additive diffusion is $X^x_t=x+\int_0^tb(X^x_s)\,ds+\sigma B_t$, driven by a standard $d$-dimensional Brownian motion $B$. Let $\pi$ be its invariant distribution. Its Euler scheme with step $\gamma$ is $\bar X^{\gamma,x}_0=x$, $\bar X^{\gamma,x}_{(n+1)\gamma}=\bar X^{\gamma,x}_{n\gamma}+\gamma b(\bar X^{\gamma,x}_{n\gamma})+\sigma(B_{(n+1)\gamma}-B_{n\gamma})$, with invariant distribution $\pi^\gamma$. Write $\underline s_\eta=\eta\lfloor s/\eta\rfloor$ and $[f]_1$ for the Lipschitz constant of $f$.

Given a first step $\gamma_0$, steps $\gamma_r=\gamma_02^{-r}$, horizons $T_0>\dots>T_R$, a warm start $\tau$, and independent Brownian motions $B^{(0)},\dots,B^{(R)}$, the multilevel occupation measure (7) is

$$\mathcal Y(f)=\frac1{T_0-\tau}\int_\tau^{T_0}f(\bar X^{\gamma_0}_{\underline s_{\gamma_0}})ds+\sum_{r=1}^R\frac1{T_r-\tau}\int_\tau^{T_r}\big(f(\bar X^{\gamma_r}_{\underline s_{\gamma_{r-1}}})-f(\bar X^{\gamma_{r-1}}_{\underline s_{\gamma_{r-1}}})\big)ds,$$

where both schemes of level $r$ start at $x_0$ and are driven by $B^{(r)}$. Its cost is $\mathcal C(\mathcal Y)=T_0/\gamma_0+\sum_{r=1}^R(T_r/\gamma_r+T_r/\gamma_{r-1})$.

When $b$ is $\mathcal C^2$ with bounded derivatives, set $\|\nabla b\|_{2,\infty}=\sup_x\|\nabla b(x)\|_F$ (Frobenius norm of the Jacobian) and $\|\Delta b\|^2_{2,\infty}=\sup_x\sum_i|\Delta b_i(x)|^2$. The constant (19) is

$$\Upsilon_2^2=\max\Big(1,\ \frac{|b(x_0)|^2}{\alpha^2}+\frac{\sigma\sqrt\alpha}{L^3}\|\nabla b\|_{2,\infty}|b(x_0)|+\frac{\sigma^4}{L^4}\|\Delta b\|^2_{2,\infty}+\frac{\sigma^2\alpha\sqrt d}{L^3}\|\nabla b\|_{2,\infty}+\frac{\sigma^2d}{\alpha}\Big).$$

Formalization targets

Goal: Theorem 2.3

Take $\gamma_0\in(0,\frac\alpha{2L^2}\wedge\frac12]$, $R_\varepsilon=\lceil\log_2(\Upsilon_2/\varepsilon)\rceil$, $T_r=\Upsilon_2^2\log(\gamma_0^{-1})\alpha^{-1}\varepsilon^{-2}2^{-3r/2}$ and $\tau=\alpha^{-1}|\log\varepsilon|+(2\alpha)^{-1}\log\Upsilon_2$. There is a universal constant $\mathfrak C_1$ such that for every $\varepsilon\in(0,1)$ with $\sqrt2\log(\Upsilon_2\varepsilon^{-2})\le\log(\gamma_0^{-1})(\Upsilon_2/\varepsilon)^{1/2}$,

$$\|\mathcal Y(f)-\pi(f)\|_2\le\mathfrak C_1[f]_1\varepsilon,\qquad\mathcal C(\mathcal Y)\le\frac{\frac12+\sqrt2}{\sqrt2-1}\,\frac{\Upsilon_2^2\log(\gamma_0^{-1})}{\gamma_0\alpha}\,\varepsilon^{-2}.$$

The constant $\mathfrak C_1$ is the same for all $d$, $b$, $\sigma$, $f$, $x_0$, $\gamma_0$ and $\varepsilon$.

Companion: (22)

Under $\alpha/L^2\le1$, $\sigma^2\alpha^{-1}d\ge1$ and dimension-free bounds on $|b(x_0)|$, $\|\nabla b\|_{2,\infty}$ and $\|\Delta b\|_{2,\infty}$, the choice $\gamma_0=\alpha/(2L^2)$, $\tilde\Upsilon_2^2=\sigma^2\alpha^{-1}d$ gives $\mathcal C(\mathcal Y)\le\frac{2\sqrt2+1}{\sqrt2-1}\frac{\sigma^2L^2}{\alpha^3}\log\frac{2L^2}{\alpha}\,d\varepsilon^{-2}$.

Milestones

The milestones follow the paper's proof in order:

• Lemma 5.1 (i), (iii): stability of the scheme and the assumptions $(\mathbf H_1)$, $(\mathbf H_4)$.
• Lemma 5.2 (ii): a one-step error of order $\gamma^3$.
• Proposition 5.1 (ii), (iii): a uniform-in-time strong error $\beta_2(x)\gamma^2$ and $(\mathbf H_2)$ with $\mathfrak a=2$.
• Proposition 5.2: $\mathcal W_1(\pi,\pi^\gamma)\le\sqrt{\beta_2(x^\star)}\gamma$.
• Proposition 2.2: $(\mathbf H_2)$–$(\mathbf H_4)$ with constants controlled by $\Upsilon_2$.
• Remark 4.1: the paper's general complexity theorem, with constants known up to universal factors.

Significance

The result. Theorem 2.3 gives an explicit algorithm whose cost to reach $L^2$ accuracy $\varepsilon$ on $\pi(f)$ is of order $\varepsilon^{-2}$, uniformly over Lipschitz $f$. Under (22) the cost is $O(d\varepsilon^{-2})$. Apart from constants depending on $\alpha$ and $L$, this is the complexity of a Monte Carlo method without bias, an improvement over the $d\varepsilon^{-4}$ known for single-level occupation measures. Corollary 2.2 of the paper applies it to Gibbs distributions with a $\mathcal C^3$ potential.

Formalizing it. The theorem is proved in the paper. A machine-checked version needs a formal multilevel estimator over infinite horizons, uniform-in-time strong error bounds for the Euler scheme, and an application of Itô's formula to $b(y+\sigma B_t)$, none of which exists in Lean. Formalizing also checks the paper's constants. For instance, the printed exponential rate in the $\mathcal W_2$ contraction behind $(\mathbf H_1)$ is $\alpha$, while its proof gives $\alpha/2$, and the milestone states $\alpha/2$. No part of this result has been machine-checked.

Difficulty

Two steps resist a direct approach. First, the order-one strong error (Lemma 5.2(ii), Proposition 5.1(ii)). Bounding the one-step error by the Lipschitz constant alone gives order $\gamma^2$ per step, hence order $\gamma^{1/2}$ globally; this is Lemma 5.2(i) and the $\mathfrak a=1$ regime, with an extra $\log^3\varepsilon$ in the cost. The gain to $\gamma^3$ needs the second-order structure of $b$ along the Brownian path, through a martingale term and the Laplacian of $b$. Second, the error must be controlled uniformly over infinite horizons. Every estimate has to combine the contraction $(\mathbf C_\alpha)$ with the step-size restriction $\gamma\le\alpha/(2L^2)$; a Gronwall argument on a finite horizon gives constants that grow with time.

For the goal itself, the cost bound (21) is arithmetic once the parameters are fixed. The content is the error bound with a constant that is universal, not merely independent of $\varepsilon$.

Formalization scope

• $\mathbb R^d$ is the published EthierKurtz.SDEState d, and Brownian motions are the published EthierKurtz.IsStandardBrownian.
• The diffusion is a pathwise solution of $X_t=x+\int_0^tb(X_s)ds+\sigma W_t$ with continuous paths. No stochastic integral appears in any statement.
• $\pi$ is a probability measure invariant for the diffusion's transition laws. $\pi^\gamma$ is any probability invariant for the Euler step $x\mapsto x+\gamma b(x)+\sigma\sqrt\gamma Z$, with $Z$ standard Gaussian.
• $\|\cdot\|_2$ is eLpNorm · 2 P, valued in $[0,\infty]$. The schemes are evaluated at grid times, except in $(\mathbf H_4)$ and (47), which use the continuous-time scheme.
• $\mathcal C^2$ with bounded partial derivatives is ContDiff ℝ 2 b plus a uniform bound on the first and second Fréchet derivatives.
• $\|\nabla b\|_{2,\infty}$ and $\|\Delta b\|^2_{2,\infty}$ follow pp. 31–32, which correct the misplaced squares of (18).
• "$\lesssim_{uc}$" is an existential constant quantified before every datum.
• The $\varepsilon_0$ of Theorem 2.3 is read as membership in its defining set.
• The cost formula is used for every $T_r$.
• Added hypotheses: $\sigma>0$ wherever the page leaves it implicit; $\mathcal C^2$ regularity in Lemma 5.2(ii) and Propositions 5.1–5.2; $\gamma<1$ in Proposition 5.2; $d\ge1$ in Proposition 5.1(iii); $\alpha\le1$ in Proposition 2.2.

The goal does not assume $(\mathbf H_1)$–$(\mathbf H_4)$, Proposition 2.2 or any variance or bias estimate. It assumes only $(\mathbf C_\alpha)$, Lipschitz and $\mathcal C^2$ regularity of $b$, $\sigma>0$, invariance of $\pi$ and the parameter choices. Those results appear only as milestones.

Contributions that would be reusable elsewhere: uniform-in-time moment and strong-error bounds for Euler schemes of contractive SDEs, Itô's formula for a $\mathcal C^2$ function of Brownian motion, and the general multilevel complexity theorem (Remark 4.1). Proofs of the milestones are welcome independently.

Selected references

• M. Egéa, F. Panloup, Multilevel-Langevin pathwise average for Gibbs approximation, Math. Oper. Res., 2025; arXiv:2109.07753v2. https://arxiv.org/abs/2109.07753
• M. B. Giles, Multilevel Monte Carlo path simulation, Oper. Res. 56(3), 2008. https://doi.org/10.1287/opre.1070.0496
• A. Durmus, É. Moulines, High-dimensional Bayesian inference via the unadjusted Langevin algorithm, Bernoulli 25(4A), 2019. https://doi.org/10.3150/18-BEJ1073
• A. S. Dalalyan, Theoretical guarantees for approximate sampling from smooth and log-concave densities, J. R. Stat. Soc. B 79(3), 2017. https://arxiv.org/abs/1412.7392
• A. Durmus, É. Moulines, Nonasymptotic convergence analysis for the unadjusted Langevin algorithm, Ann. Appl. Probab. 27(3), 2017. https://arxiv.org/abs/1507.05021

Opinions on large directed social networks

Linear models of opinion formation go back to DeGroot (DeGroot 1974), in which every individual repeatedly replaces their opinion by a weighted average of the opinions of the people they listen to, and to Friedkin and Johnsen (Friedkin–Johnsen 1990), who added a persistent internal opinion. Fraiman, Lin and Olvera-Cravioto (arXiv:2209.00969v2, Mathematics of Operations Research, 2025) add a random external (media) signal whose law may depend on the individual's attributes, which models selective exposure, and ask what the opinions look like on a large random social network. The answer is the behaviour of a typical individual, a uniformly chosen vertex: its stationary opinion converges in law to the opinion of the root of the network's local weak limit, and the empirical distribution of all stationary opinions converges to the same law. Questions such as consensus or polarization are then questions about one limiting random variable, independent of the particular realization of the network.

This mission formalizes that main result (Theorem 2) together with the fixed-graph stationarity theorem it rests on (Theorem 1).

Setting

A vertex-weighted directed graph on a vertex set $V$ gives each vertex $i$ an in-degree $d_i^-$, an ordered list of inbound neighbours $\ell(i,1),\dots,\ell(i,d_i^-)$ and weights $c(i,r)\in[0,1]$ with $\sum_r c(i,r)=c$ whenever $d_i^->0$. The parameters satisfy $c\in[0,1)$, $d\in(0,1]$, $c+d\le1$. The opinions $R_i^{(k)}\in[-1,1]$ evolve by recursion (1),

$$R_i^{(k+1)}=\sum_{r=1}^{d_i^-}c(i,r)\,R^{(k)}_{\ell(i,r)}+W_i^{(k)}+(1-c-d)R_i^{(k)},\qquad k\ge0,$$

where the external signals $W_i^{(k)}$ are independent, i.i.d. in time given the vertex mark, and bounded by $|W_i^{(k)}|\le d+c-\sum_rc(i,r)$. With the operator $\Delta f(i)=\sum_rc(i,r)f(\ell(i,r))+(1-c-d)f(i)$ this reads $R^{(k+1)}=\Delta R^{(k)}+W^{(k)}$. The stationary vector is $R=\sum_{r\ge0}\Delta^rW^{(r)}$.

The full mark of a vertex is $\mathbf X_i=(\mathbf A_i,Q_i,S_i,D_i^-,C(i,1),C(i,2),\dots)$: a generic attribute, an internal opinion, a stubbornness label, the in-degree and the weights. Marks are compared by the metric

$$\rho(\mathbf x,\tilde{\mathbf x})=\rho'(\mathbf a,\tilde{\mathbf a})+|q-\tilde q|+|s-\tilde s|+|d^--\tilde d^-|+\sum_j|c_j\mathbb 1(d^-\ge j)-\tilde c_j\mathbb 1(\tilde d^-\ge j)|.$$

A random graph sequence $G(V_n,E_n;\mathscr A_n)$ has vertex set $V_n=\{1,\dots,n\}$ and attributes $\mathscr A_n=\{\mathbf Y_i=(\mathbf A_i,Q_i,S_i)\}$; edges and weights are random given the attributes. The conditional expectation $E_n[\cdot]=E[\cdot\mid\mathscr A_n]$ conditions on the attributes only. The in-component of depth $k$ of a vertex $v$ is the set of vertices with a directed path of length at most $k$ to $v$. The sequence admits a strong coupling (Definition 4) with a rooted marked graph $\mathcal G(\boldsymbol{\mathcal X})$ if, for two independent uniform vertices $I_n,J_n$, every depth $k\ge1$ and every $\epsilon>0$, there are two independent copies of $\mathcal G(\boldsymbol{\mathcal X})$ whose depth-$k$ root in-components are, with conditional probability tending to one in probability, isomorphic to those of $I_n$ and $J_n$, with all marks $\epsilon$-close in $\rho$ and the two in-components of $I_n$ and $J_n$ disjoint. The Wasserstein distance is $d_1(\mu,\nu)=\inf\{E|X-Y|:X\sim\mu,Y\sim\nu\}$.

Formalization targets

Goal: Theorem 2

Assume a strong coupling, $d>0$, and a signal kernel $\nu(\mathbf x)$ with $d_1(\nu(\mathbf x),\nu(\tilde{\mathbf x}))\le K\rho(\mathbf x,\tilde{\mathbf x})$. Then there are laws $L_k$ of $(\mathcal R^{(0)},\dots,\mathcal R^{(k)})$ and $L^*$ of $\mathcal R^*$, not depending on $n$, with

$$\max_{0\le r\le k}E\bigl[|R^{(r)}_{I_n}-\mathcal R^{(r)}|\bigm|\mathscr A_n\bigr]\xrightarrow{P}0,\qquad \frac1n\sum_{i=1}^nf(R_i^{(k)})\xrightarrow{P}E f(\mathcal R^{(k)}),$$ $$E\bigl[|R_{I_n}-\mathcal R^*|\bigm|\mathscr A_n\bigr]\xrightarrow{P}0,\qquad \frac1n\sum_{i=1}^nf(R_i)\xrightarrow{P}E f(\mathcal R^*),$$

for every continuous $f$ on $[-1,1]$, and $\mathcal R^{(k)}\Rightarrow\mathcal R^*$ geometrically fast:

$$d_1\bigl(\mathrm{law}\,\mathcal R^{(k)},\mathrm{law}\,\mathcal R^*\bigr)\le(1-d)^k\Bigl(\frac2d+2\Bigr).$$

Milestones

1. $\|\Delta\|_\infty\le1-d$ (proof of Theorem 1, p. 22).
2. Theorem 1 (p. 5): on a fixed locally finite graph, $R^{(k)}\Rightarrow R$ at a geometric rate, with a limit that does not depend on $R^{(0)}$.
3. Theorem 2(1) (p. 8): the fixed-time statement.

A supporting statement of the proposal, not a milestone, is the tail bound $\|R-B^{(k)}\|_\infty\le2\sum_{r>k}(1-d)^r$ for $B^{(k)}=\sum_{r\le k}\Delta^rW^{(r)}$ (proof of Theorem 2, p. 28).

Significance

Theorem 2 reduces the stationary opinion distribution of a large network to a single random variable $\mathcal R^*$ attached to the local limit. When the limit is a marked Galton–Watson tree, $\mathcal R^*$ has an explicit series representation whose mean and variance are computed in closed form later in the paper (the other two missions of this series), and these formulas are what explain consensus and polarization. Strong couplings exist ([Olvera-Cravioto 2022], cited on p. 8 of the paper) for Erdős–Rényi graphs, the Chung–Lu and Norros–Reittu models, the configuration model, stochastic block models and preferential attachment graphs, so the theorem applies to most random graph models used for social networks.

The result is proved in the paper; nothing in it has been formalized. On Prove2Me this is the first statement of a strong coupling, a form of local weak convergence for directed marked graphs, and of a stochastic recursion on a random graph. The definitions of in-components, the coupling event and the strong coupling are reusable for any local-limit statement about directed random graphs, and the contraction and time-reversal milestones are reusable for linear stochastic recursions.

Difficulty

The fixed-graph part is a contraction argument, but the coupled object is not the opinion process itself: $R^{(k)}$ does not converge almost surely, and only its time reversal $B^{(k)}$ does. The main difficulty is Theorem 2. A local limit controls one neighbourhood at a time, while the empirical averages need two uniformly chosen vertices to be asymptotically independent, which a one-vertex limit statement does not give. The errors in weights, signals and initial opinions enter at every vertex of a depth-$k$ neighbourhood, and the statements condition only on the attributes, with edges and weights integrated out. The stationary statement then requires an interchange of $n\to\infty$ and $k\to\infty$ that is uniform in $n$.

Formalization scope

All random objects of the $m$-th model live on one probability space, and the $m$-th graph has $m+1$ vertices (the paper's $G_{m+1}$), so a uniform vertex always exists. Signals are written $W_i^{(k)}=\zeta(\mathbf X_i,U_i^{(k)})$ and initial opinions $R_i^{(0)}=\varphi(\mathbf X_i,V_i)$ with i.i.d. uniforms independent of the graph: this quantile representation is equivalent in law to the paper's conditionally i.i.d. signals. Neighbour indices are 0-based. The conditional quantities given $\mathscr A_n$ are regular conditional distributions given the attribute vector, and "random variables whose distribution does not depend on $\mathscr A_n$" are encoded by fixed limit laws, with the paper's $E[|\cdot|\mid\mathscr A_n]\to0$ read as $d_1$ convergence in probability of the conditional laws, which is equivalent. Theorem 1 is stated on countably many vertices, with its geometric rate given as an explicit bound for 1-Lipschitz test functions of finitely many coordinates.

Disclosed choices: the strong coupling is stated on the given space with measurable events inside the coupling events (the event "an isomorphism exists" need not be measurable), with isomorphisms that preserve the order of inbound neighbours (which the proof uses), and through its second bullet, which implies the first. The paper's conditional independence of weight vectors given $\mathscr A_n$ is not imposed. The strong coupling also requires the depth-$k$ in-components of $I_n$ and $J_n$ to be disjoint on the coupling event: the proof of Theorem 7 uses this, and without it Definition 4 admits a graph whose vertices all listen to a single hub, whose shared signals keep $\frac1n\sum_if(R_i^{(k)})$ random. The page puts no condition on $R^{(0)}$ beyond conditional independence of the signals, but Theorem 2(1) at time $0$ is false then (take $R^{(0)}\equiv(-1)^n$); the statement assumes a $d_1$-Lipschitz initial kernel with the same $K$, which covers the paper's own simulations. The geometric rate uses the constant of the proof.

Trivializing readings are excluded: every tsum is absolutely summable under the hypotheses, conditional laws are regular conditional distributions of measurable random variables, the averages have no division by zero, and the limit laws are forced onto $[-1,1]$ by the convergence, so no integral defaults to $0$. Theorem 7 of the paper (the two-vertex coupling) is not a milestone. Contributions of proofs of any milestone, and of general lemmas on regular conditional distributions and Wasserstein couplings, are welcome.

Selected references

• N. Fraiman, T.-C. Lin and M. Olvera-Cravioto, Opinion dynamics on directed complex networks, Mathematics of Operations Research, 2025; preprint arXiv:2209.00969v2, 2024. https://arxiv.org/abs/2209.00969v2
• M. H. DeGroot, Reaching a consensus, Journal of the American Statistical Association 69 (1974), 118–121. https://doi.org/10.1080/01621459.1974.10480137
• N. E. Friedkin and E. C. Johnsen, Social influence and opinions, Journal of Mathematical Sociology 15 (1990), 193–206. https://doi.org/10.1080/0022250X.1990.9990069
• M. Olvera-Cravioto, Strong couplings for static locally tree-like random graphs, Journal of Applied Probability 59(4) (2022), 1261–1285 (reference [33] of the paper, where the random graph models admitting strong couplings are listed).

Motivation

Sampling from a Gibbs distribution $\pi_U \propto e^{-U}\,d\lambda_d$ on $\mathbb R^d$, or computing integrals $\pi(f)$ against it, is a basic task of Bayesian statistics, statistical physics and stochastic optimization. A standard route is to simulate a diffusion whose invariant law is the target, for instance the overdamped Langevin equation $dX_t = -\nabla U(X_t)\,dt + \sqrt2\,dB_t$, discretize it with the Euler scheme, and average a function along one long trajectory. Discretization introduces a bias of order of the step size, and the long-time average introduces a variance that decays like the inverse of the horizon, so reaching root-mean-square accuracy $\varepsilon$ with a single Euler scheme costs more than $\varepsilon^{-2}$ steps.

Egéa and Panloup (arXiv:2109.07753, Mathematics of Operations Research, 2025) adapt Giles's multilevel Monte Carlo idea (Giles 2008) to this infinite-horizon setting: they combine a coarse pathwise average with corrections between coupled Euler schemes of successively halved steps, run over decreasing horizons. Their general complexity theorem (Theorem 2.1) is stated under four abstract assumptions (H₁)–(H₄). This mission formalizes the first concrete instance the paper gives: an additive diffusion with a strongly contractive drift, where the assumptions are verified with explicit dependence on the dimension and the cost is of order $\varepsilon^{-2}\log^3(\varepsilon^{-1})$.

Setting

Let $|\cdot|$ and $\langle\cdot,\cdot\rangle$ be the Euclidean norm and inner product on $\mathbb R^d$. Let $b:\mathbb R^d\to\mathbb R^d$ be $L$-Lipschitz and satisfy the contractivity assumption $(\mathbf C_\alpha)$:

$$\langle b(y)-b(x),y-x\rangle\le-\alpha|x-y|^2\qquad(x,y\in\mathbb R^d),$$

with $0<\alpha\le L$. For $b=-\nabla U$ this is uniform strong convexity of $U$. Let $\sigma>0$ and let $W$ be a standard $d$-dimensional Brownian motion. The additive diffusion started at $x$ is $X^x_t = x+\int_0^t b(X^x_s)\,ds+\sigma W_t$; a probability $\pi$ is invariant for it if $\int\mathbb P(X^x_t\in A)\,\pi(dx)=\pi(A)$ for all $t$ and Borel $A$.

The Euler scheme with step $\gamma>0$ is $\bar X^{\gamma,x}_0=x$, $\bar X^{\gamma,x}_{(n+1)\gamma}=\bar X^{\gamma,x}_{n\gamma}+\gamma b(\bar X^{\gamma,x}_{n\gamma})+\sigma(W_{(n+1)\gamma}-W_{n\gamma})$, extended to continuous time by $\bar X_t=x+\int_0^t b(\bar X_{\underline s})\,ds+\sigma W_t$, $\underline s=\gamma\lfloor s/\gamma\rfloor$. A probability $\pi^\gamma$ invariant for one step of the scheme is its invariant distribution.

The multilevel occupation measure with start $x_0$, coarse step $\gamma_0$, levels $r=0,\dots,R$, steps $\gamma_r=\gamma_02^{-r}$, horizons $T_r$ and warm-start time $\tau$ is

$$\mathcal Y(f)=\frac1{T_0-\tau}\int_\tau^{T_0}f(\bar X^{\gamma_0}_{\underline s_{\gamma_0}})\,ds+\sum_{r=1}^R\frac1{T_r-\tau}\int_\tau^{T_r}\big(f(\bar X^{\gamma_r}_{\underline s_{\gamma_{r-1}}})-f(\bar X^{\gamma_{r-1}}_{\underline s_{\gamma_{r-1}}})\big)\,ds,$$

where level $r$ uses its own Brownian motion $B^{(r)}$, independent across levels, and both schemes of a level share it. Its cost is $\mathcal C(\mathcal Y)=T_0/\gamma_0+\sum_{r=1}^R(T_r/\gamma_r+T_r/\gamma_{r-1})$, the number of simulated Euler steps. Write $[f]_1$ for the Lipschitz constant of $f$ and

$$\Upsilon_1^2=1\vee\big(\alpha^{-2}|b(x_0)|^2+\alpha^{-1}\sigma^2d\big).$$

Formalization targets

Goal: Theorem 2.2

There is a universal constant $\mathfrak C_1$ such that, for $\alpha\in(0,L\wedge1]$, $\gamma_0\in(0,\frac\alpha{2L^2}\wedge\frac12]$, the parameters

$$r_0=\Upsilon_1,\quad R_\varepsilon=\lceil2\log_2(r_0\varepsilon^{-1})\rceil,\quad T_r=\frac{\Upsilon_1^2\log(\gamma_0^{-1})}{\alpha}\varepsilon^{-2}R_\varepsilon^22^{-r},\quad \tau=\frac2\alpha|\log\varepsilon|+\frac1\alpha\log\Upsilon_1,$$

and every $\varepsilon\in(0,1)$ with $2\log(\Upsilon_1\varepsilon^{-2})\le\log(\gamma_0^{-1})R_\varepsilon^2$,

$$\|\mathcal Y(f)-\pi(f)\|_2\le\mathfrak C_1[f]_1\varepsilon,\qquad\mathcal C(\mathcal Y)\le\frac{5\log(\gamma_0^{-1})}{2\alpha\gamma_0}\Upsilon_1^2\varepsilon^{-2}\lceil\log_2(\Upsilon_1^2\varepsilon^{-2})\rceil^3.$$

The constant $\mathfrak C_1$ does not depend on $d$, $b$, $\sigma$, $f$, $x_0$ or $\varepsilon$; all dependence on the problem sits in the explicit cost.

Milestones

1. Lemma 5.1 (i)–(iii): uniform second-moment bound (47), existence and uniqueness of $\pi^\gamma$, the $L^2$ contraction $\mathbb E|\bar X^{\gamma,x}_t-\bar X^{\gamma,y}_t|^2\le|x-y|^2e^{-\alpha t}$, the bound $\mathcal W_2(\delta_x,\pi^\gamma)\le c_1(x)$, and from these (H₁) and (H₄).
2. Lemma 5.2 (i): the one-step error between diffusion and Euler step.
3. Proposition 5.1 (i) and (iii) with $\mathfrak a=1$: $\|X^x_{n\gamma}-\bar X^{\gamma,x}_{n\gamma}\|_2^2\le\beta_1(x)\gamma$ uniformly in $n$, hence (H₂).
4. Proposition 5.2 with $\mathfrak a=1$, $\delta=\frac12$: $\mathcal W_1(\pi,\pi^\gamma)\le\sqrt{\beta_1(x^\star)\gamma}$, hence (H₃).
5. Proposition 2.1: all four assumptions with $\max(\alpha c_2^2/L^2,\alpha c_3^2/L^2,c_4^2)\lesssim\Upsilon_1^2$.
6. Remark 4.1: Theorem 2.1 (ii) for the additive scheme when the constants are known up to universal factors.
7. Theorem 2.2 (15): the refinement with $\tilde\Upsilon_1^2=\sigma^2\alpha^{-1}d$ and $\gamma_0=\alpha/(2L^2)$.

Significance

The goal gives a complexity of order $\varepsilon^{-2}\log^3(\varepsilon^{-1})$ for approximating $\pi(f)$ by a pathwise average of Euler schemes, within a logarithmic factor of the $\varepsilon^{-2}$ of an unbiased Monte Carlo method, with constants explicit in $d$, $\alpha$, $L$, $\sigma$. When $|b(x_0)|\lesssim\sqrt d$, the cost is of order $d\varepsilon^{-2}(\log^3d+\log^3\varepsilon)$. The intermediate results (uniform-in-time strong error of the Euler scheme, Wasserstein bias of its invariant law, step-independent contraction) are standard tools of Langevin Monte Carlo and are reusable on their own.

The results are proved in the paper; none of them is machine-checked. A formal proof would certify both the abstract multilevel argument as instantiated here and the explicit constants. The formal statements also pin three printed slips: the ceiling in (14) (cube of the ceiling, not ceiling of the cube), the first line of (12) (the function $c_1$ of Lemma 5.1 (ii)), and the factor in (15).

Difficulty

The obvious argument controls bias and variance separately for each level. The bias of a pathwise average involves the long-time behaviour of the scheme, and the variance of a correcting level involves the $L^2$ distance between two coupled schemes over an unbounded horizon: both require estimates uniform in time, which fail for a merely Lipschitz drift (the strong error of the Euler scheme grows exponentially on finite horizons). Contractivity is what makes the strong error $O(\sqrt\gamma)$ uniformly in $n$, and the delicate point is to obtain this with constants that do not degrade with $d$ or with the step. The complexity bound then requires balancing $R_\varepsilon$, the horizons and the warm start so that the long-time bias, the discretization bias and the variances all sit at level $\varepsilon$, with a universal constant.

Formalization scope

$\mathbb R^d$ is EuclideanSpace ℝ (Fin d) (published EthierKurtz.SDEState); Brownian motions are published EthierKurtz.IsStandardBrownian, one per level, mutually independent as path-valued variables. The diffusion is a pathwise solution of the integral equation with continuous paths; no Itô integral is needed because the noise is additive. Invariance of $\pi$ and $\pi^\gamma$ is stated through transition probabilities. $L^2$ norms are eLpNorm … 2 in $[0,\infty]$, so an infinite moment is never read as zero. $\mathcal W_1$ is used in its Kantorovich–Rubinstein form, $\mathcal W_2(\delta_x,\cdot)$ as an explicit integral, and the clause $\mathcal W_2(\mathcal L(\bar X_{\underline t}),\pi^\gamma)\le\mathcal W_2(\delta_x,\pi^\gamma)e^{-\alpha\underline t}$ as the existence of a coupling with that quadratic cost (Mathlib has no Wasserstein distance; optimal couplings exist, so the forms agree). (H₁)–(H₃) are stated at grid times, (H₄) over all $t\ge0$. "$\lesssim_{uc}$" is an existential constant quantified before every datum.

Standing assumptions carried as hypotheses: $b$ $L$-Lipschitz, $(\mathbf C_\alpha)$, $0<\alpha\le L$ (and $\alpha\le1$ where the paper requires it), $\sigma>0$. Added and disclosed: the §5.1 hypotheses in Lemma 5.2, $\gamma<1$ in Proposition 5.2 (needed by Proposition 5.1), integrability of $f$ under $\pi$, existence of $\pi^\gamma$ and $\tilde c_4>0$ in Remark 4.1. The goal's $\varepsilon_0$ (a maximum of a set that need not be an interval) is replaced by the inequality defining it.

The goal assumes only the contractive setting, the diffusion's invariance of $\pi$ and the parameter choices; it does not assume (H₁)–(H₄), a bias or a variance bound, which appear only as milestones, so it cannot be discharged by restating its hypotheses.

A complete development needs: second-moment and Grönwall estimates for the Euler scheme and the diffusion, existence and uniqueness of invariant laws of Feller chains under a Lyapunov condition, independence and variance decompositions for the multilevel estimator, and the abstract Theorem 2.1. The Gaussian-increment and Wasserstein tools are reusable well beyond this mission. Proofs of any milestone, and a Mathlib-style $\mathcal W_2$ for general laws, are welcome.

Selected references

• M. Egéa, F. Panloup, Multilevel-Langevin pathwise average for Gibbs approximation, Mathematics of Operations Research, 2025; preprint arXiv:2109.07753v2, 2024. https://arxiv.org/abs/2109.07753
• M. B. Giles, Multilevel Monte Carlo path simulation, Operations Research 56(3), 2008. https://doi.org/10.1287/opre.1070.0496
• A. S. Dalalyan, Theoretical guarantees for approximate sampling from smooth and log-concave densities, J. R. Stat. Soc. B 79(3), 2017. https://doi.org/10.1111/rssb.12183
• A. Durmus, É. Moulines, Nonasymptotic convergence analysis for the unadjusted Langevin algorithm, Ann. Appl. Probab. 27(3), 2017. https://doi.org/10.1214/16-AAP1238