Motivation

Many estimation problems ask for a low-rank matrix from far fewer linear measurements than it has entries: matrix completion, quantum state tomography, recovery of positions from partial distances. The rank minimization problem $\min \operatorname{rank}(X)$ subject to $\mathcal S(X) = \mathcal M$ is NP-hard, so one solves a tractable surrogate instead, either the nuclear-norm minimization $\min \|X\|_*$ subject to $\mathcal S(X) = \mathcal M$ or an iterative scheme such as the iteratively reweighted least squares algorithm IRLS-M of Fornasier, Rauhut and Ward (arXiv:1010.2471).

Guarantees for these surrogates rest on conditions on the measurement map. Two are standard. The restricted isometry property (RIP) asks that $\mathcal S$ nearly preserve the Frobenius norm of every low-rank matrix; it holds with high probability for many random maps, and it is what one can verify in practice. The null space property asks that no nonzero matrix in the kernel of $\mathcal S$ be concentrated on few singular directions; it is what the recovery proofs actually use. This mission formalizes the bridge between them in the paper's form: a small restricted isometry constant implies the strong rank null space property (SRNSP) that drives the convergence analysis of IRLS-M.

Timeline.

• 2005: Candès and Tao introduce restricted isometry constants for sparse vectors and prove exact recovery by $\ell_1$ minimization under a condition on them (IEEE Trans. Inf. Theory).
• 2008: Candès shows that $\delta_{2s} < \sqrt 2 - 1$ suffices in the vector case (C. R. Math.).
• 2010: Recht, Fazel and Parrilo define the rank restricted isometry property and prove that nuclear-norm minimization recovers every rank-$r$ matrix when $\delta_{5r}$ is small enough (SIAM Review).
• 2011: Candès and Plan prove the matrix analogue of the $\sqrt 2 - 1$ threshold and the orthogonality estimate quoted here as Lemma 6.9 (IEEE Trans. Inf. Theory).
• 2011: Fornasier, Rauhut and Ward prove Proposition 6.8, the target of this mission: $\delta_{4k} < \sqrt 2 - 1$ implies the SRNSP of order $k$.

Setting

Fix integers $n, p, m$. A measurement map is a linear map $\mathcal S : \mathbb R^{n\times p} \to \mathbb R^m$; it is given by $m$ matrices $A_1,\dots,A_m$ through $\mathcal S(X)_\ell = \langle A_\ell, X\rangle$, where $\langle X, Y\rangle = \operatorname{Tr}(XY^{\top}) = \sum_{i,j} X_{ij}Y_{ij}$. The Frobenius norm is $\|X\|_F = \langle X, X\rangle^{1/2}$, the nuclear norm $\|X\|_*$ is the sum of the singular values of $X$, and $\|\mathcal S(X)\|_{\ell_2^m}$ is the Euclidean norm of the vector $\mathcal S(X)$. A matrix is $k$-rank if its rank is at most $k$.

The restricted isometry constant $\delta_k = \delta_k(\mathcal S)$ (Definition 1.1) is the smallest $\delta \ge 0$ such that

$$(1 - \delta)\|X\|_F^2 \le \|\mathcal S(X)\|_{\ell_2^m}^2 \le (1+\delta)\|X\|_F^2 \qquad \text{for all $k$-rank } X .$$

The map $\mathcal S$ has the strong rank null space property of order $k$ with constant $\eta \in (0,1)$ (Definition 6.4) if for every $X \in \ker \mathcal S \setminus\{0\}$ and every decomposition $X = X_1 + X_2$ with $X_1$ $k$-rank, there is another decomposition $X = H_1 + H_2$ with $\operatorname{rank} H_1 \le 2k$, $\langle H_1, H_2\rangle = 0$, $X_1H_2^{\top} = 0$, $X_1^{\top}H_2 = 0$, and

$$\|H_1\|_* \le \eta\,\|H_2\|_* .$$

In Lean these are IRLSM.RIP.ripConst A k, IRLSM.RIP.SRNSP A k η and IRLSM.RIP.measSq A X $= \|\mathcal S(X)\|^2_{\ell_2^m}$, built on the published module HighDimStat_MatrixRank_Core (traceInner, frobeniusNorm, nuclearNorm, observationOp).

Formalization targets

Goal: Proposition 6.8

If $\delta_{4k} > 0$ and

$$\delta_{4k} < \sqrt 2 - 1,$$

then $\mathcal S$ satisfies the SRNSP of order $k$ with constant

$$\eta = \sqrt 2\,\frac{\delta_{4k}}{1 - \delta_{3k}} \in (0,1).$$

The constant $\eta$ is the paper's explicit one; the goal asserts the full property for every kernel element and every decomposition, including $\eta \in (0,1)$.

Milestones

1. Lemma 6.9 (Candès–Plan): for $\langle X, Y\rangle = 0$ and $\operatorname{rank}X + \operatorname{rank}Y \le k$, $|\langle \mathcal S(X), \mathcal S(Y)\rangle| \le \delta_k \|X\|_F\|Y\|_F$.
2. Lemma 6.10 (Recht–Fazel–Parrilo): $XZ^{\top} = 0$ and $X^{\top}Z = 0$ imply $\|X + Z\|_* = \|X\|_* + \|Z\|_*$.
3. The block decomposition of the proof: relative to an SVD $X_1 = U(\begin{smallmatrix}\Sigma & 0\\ 0 & 0\end{smallmatrix})V^{\top}$, the matrices $H_0$ and $H_c$ obtained by zeroing blocks of $U^{\top}XV$ satisfy $X = H_0 + H_c$, $\operatorname{rank}H_0 \le 2k$, $X_1H_c^{\top} = 0$, $X_1^{\top}H_c = 0$, $\langle H_0, H_c\rangle = 0$.
4. $\|H\|_* \le \sqrt r\,\|H\|_F$ for $\operatorname{rank}H \le r$, and $\|H\|_F \le \|H + K\|_F$ for $\langle H, K\rangle = 0$.
5. The shelling bound: for a nonincreasing nonnegative sequence cut into blocks of length $\ell$, each block's $\ell_2$ norm is at most $\ell^{-1/2}$ times the $\ell_1$ norm of the previous block.
6. Monotonicity $\delta_k \le \delta_{k'}$ for $k \le k'$, and $\eta \in (0,1)$ under $0 < \delta_{4k} < \sqrt2 - 1$.

Significance

The result. Proposition 6.8 is the step that turns a verifiable, probabilistically typical hypothesis (a small rank restricted isometry constant, which Gaussian and many other random maps satisfy once $m$ is of order $k\max(n,p)$) into the deterministic null-space hypothesis under which the paper proves that IRLS-M converges to the nuclear-norm minimizer and recovers every $k$-rank matrix exactly (Theorem 6.11, Proposition 2.1). Through Lemma 6.6 and Corollary 6.7 of the same paper, the SRNSP also gives stable recovery by nuclear-norm minimization, with error controlled by the best $k$-rank approximation error in the nuclear norm.

Formalizing it. The result is proved on paper; it has no machine-checked proof that we know of. A complete development supplies the rank restricted isometry constant as a usable object (its monotonicity, its polarization estimate Lemma 6.9), the nuclear norm's additivity on orthogonal pieces, its comparison with the Frobenius norm, and the block-splitting of the singular value decomposition. These tools are reusable across low-rank recovery. The sibling mission of this series, IRLS-M Converges to the Nuclear-Norm Minimizer Under the Strong Rank Null Space Property, takes the SRNSP as its hypothesis; together the two give Proposition 2.1 of the paper.

Difficulty

The obvious argument would bound $\|H_1\|_*$ directly by the restricted isometry inequality, but that inequality controls only Frobenius norms of low-rank matrices, while the kernel element $X$ has full rank in general and the property is stated in nuclear norms. The restricted isometry hypothesis therefore cannot be applied to $X$, or to $H_2$, as a whole, and the constant $\eta$ depends on how the high-rank part is handled. In Lean, the singular value decomposition of a rectangular matrix and the behaviour of singular values under block operations are the main missing infrastructure: Mathlib has the spectral theorem for Hermitian matrices but little on singular values of rectangular matrices.

Formalization scope

• Real matrices Matrix (Fin n) (Fin p) ℝ; the paper treats real and complex matrices indifferently. $X^*$ is $X^{\top}$ and $\langle\cdot,\cdot\rangle$ is traceInner.
• Measurement map by matrices: $\mathcal S(X)_\ell = \langle A_\ell, X\rangle$ (observationOp); $\|\mathcal S(X)\|^2_{\ell_2^m}$ is a sum of squares, not Mathlib's sup norm on Fin m → ℝ.
• The squared RIP constant of Definition 1.1, defined as the infimum of the admissible $\delta \ge 0$ (attained, never a junk value), for every $k \in \mathbb N$; the page's range $1 \le k \le n$ is dropped because the goal uses $\delta_{4k}$ with $4k$ possibly larger than $n$. The unsquared constant $(1-\delta)\|X\|_F \le \|\mathcal S(X)\| \le (1+\delta)\|X\|_F$ used by other formalizations is a different quantity and is not used.
• Positivity $\delta_{4k} > 0$ is a hypothesis of the goal: it is Definition 1.1's own "$\delta_k > 0$", and without it $\eta = 0 \notin (0,1)$.
• No n ≤ p assumption: the proof does not use it.
• The block decomposition milestone states the page's explicit construction, with a general (not necessarily diagonal) top-left block, and without the unused hypothesis $X \in \ker\mathcal S$.
• The shelling bound is stated in its vector form for every block; the page writes "for $j \ge 2$" but display (6.7) uses it for every $j \ge 1$.

A formalization that proved only $\eta < 1$, or only the existence of some decomposition without the bound $\|H_1\|_* \le \eta\|H_2\|_*$, or that defined $\delta_k$ as any admissible constant rather than the smallest one, would not be this mission's goal.

Welcome contributions: singular value decomposition for rectangular real matrices in the Core encoding, singular values of block-diagonal and orthogonally-equivalent matrices, and proofs of the milestones in any order.

Selected references

• M. Fornasier, H. Rauhut, R. Ward, Low-rank matrix recovery via iteratively reweighted least squares minimization, SIAM J. Optim. 21(4), 2011; read as arXiv:1010.2471v4. https://arxiv.org/abs/1010.2471
• E. J. Candès, Y. Plan, Tight oracle inequalities for low-rank matrix recovery from a minimal number of noisy random measurements, IEEE Trans. Inf. Theory 57(4), 2011. https://doi.org/10.1109/TIT.2011.2111771
• B. Recht, M. Fazel, P. A. Parrilo, Guaranteed minimum-rank solutions of linear matrix equations via nuclear norm minimization, SIAM Review 52(3), 2010. https://doi.org/10.1137/070697835
• E. J. Candès, T. Tao, Decoding by linear programming, IEEE Trans. Inf. Theory 51(12), 2005. https://doi.org/10.1109/TIT.2005.858979
• E. J. Candès, The restricted isometry property and its implications for compressed sensing, C. R. Math. Acad. Sci. Paris 346, 2008. https://doi.org/10.1016/j.crma.2008.03.014

Motivation

In a road or communication network, traffic is routed by many independent users, each choosing a route that is fastest for itself given the congestion caused by everyone else. The resulting Nash flow (also called a Wardrop equilibrium, after Wardrop 1952) need not minimize the total delay experienced by all users: Braess's paradox shows that adding a road can make everyone slower. Network designers, transport economists and the designers of Internet congestion-control protocols therefore ask how much total delay is lost to selfish routing, compared with a centrally optimized routing of the same traffic.

Roughgarden and Tardos (J. ACM 2002) gave the first general answers. For linear latency functions they showed that the loss is at most a factor $4/3$. For general latency functions they showed that no such factor exists, and proved instead a bicriteria bound: selfish routing is never worse than optimal routing of twice the traffic. This mission formalizes that bicriteria bound (§3 of the paper) together with its variants for an arbitrary traffic increase (Theorem 3.2) and for approximate equilibria (§5.1).

Timeline:

• 1952: Wardrop states the equilibrium principle for traffic networks.
• 1968: Braess exhibits a network where adding an edge increases the equilibrium delay of every user.
• 2000–2002: Roughgarden and Tardos prove the $4/3$ bound for linear latencies and the bicriteria bound of Theorem 3.1 for all continuous nondecreasing latencies (conference version FOCS 2000, journal version 2002).

Setting

A network has edges $e$ and routes $P$; route $P$ is a set of edges. There are $k$ commodities $i = 1,\dots,k$; commodity $i$ is served by a set of routes $\mathcal P_i$ and has a rate $r_i > 0$, the amount of traffic it must send. A flow assigns an amount $f_P \ge 0$ to each route; it is feasible for the rates $r$ if $\sum_{P \in \mathcal P_i} f_P = r_i$ for every $i$. The flow on edge $e$ is $f_e = \sum_{P \ni e} f_P$.

Each edge has a latency function $\ell_e$, nonnegative, continuous and nondecreasing on $[0,\infty)$: the delay of one unit of traffic crossing $e$ when the edge carries $f_e$. The latency of a route is $\ell_P(f) = \sum_{e \in P} \ell_e(f_e)$, and the cost of a flow is the total delay

$$C(f) = \sum_P \ell_P(f)\, f_P = \sum_e \ell_e(f_e)\, f_e .$$

A feasible flow $f$ is at Nash equilibrium (Definition 2.1) if no amount $\delta > 0$ of the flow on a route $P_1 \in \mathcal P_i$, moved to another route $P_2 \in \mathcal P_i$, would find a latency on $P_2$ smaller than the latency it had on $P_1$. Lemma 2.2 shows this is equivalent to the Wardrop condition: every route carrying flow has minimum latency among the routes of its commodity. Definition 5.1 relaxes the equilibrium by a factor $1 + \epsilon$.

In the Lean development: pathLatency A ℓ x r is $\ell_P(f)$, cost A ℓ x is $C(f)$, IsNashFlow A s ℓ rate x is Definition 2.1, IsApproxNashFlow A s ℓ rate ε x is Definition 5.1, and barLatency is the auxiliary latency $\bar\ell$ of the proof of Theorem 3.1. Edge flows and feasibility are the published KellyStochasticNetworks.linkFlow and wardropFeasible.

Formalization targets

Goal: Theorem 3.1

If $f$ is a Nash flow for the rates $r$ and $f^*$ is any flow feasible for the rates $2r$, then

$$C(f) \le C(f^*).$$

The comparison is with every flow of twice the rates, not only an optimal one.

Milestones

The edge form of the cost (§2.1), Lemma 2.2 (Nash $\Leftrightarrow$ Wardrop), Lemma 2.3 ($C(f) = \sum_i L_i(f) r_i$ for the common latency $L_i(f)$ of the flow-carrying routes of commodity $i$), and the two displayed inequalities of the proof of Theorem 3.1:

$$\sum_e \bar\ell_e(f^*_e) f^*_e - C(f^*) \le C(f), \qquad \sum_P \bar\ell_P(f^*) f^*_P \ge 2C(f).$$

Stronger and related statements

Theorem 3.2: for $\gamma > 0$ and $f^*$ feasible for $(1+\gamma) r$,

$$C(f) \le \tfrac{1}{\gamma}\, C(f^*).$$

Lemma 5.2 (the approximate analogue of Lemma 2.2) and Theorem 5.3: for $0 < \epsilon < 1$, an $\epsilon$-approximate Nash flow $f$ and $f^*$ feasible for $2r$,

$$C(f) \le \frac{1+\epsilon}{1-\epsilon}\, C(f^*).$$

Significance

The price of anarchy, the ratio of the cost of a Nash flow to the minimum cost, is unbounded for general latencies: with two parallel links of latencies $1$ and $x^p$, the ratio tends to infinity as $p$ grows. Theorem 3.1 shows that the inefficiency of selfish routing can nevertheless always be offset by doubling capacity, in the sense that the optimal cost of twice the traffic is at least the Nash cost. Theorem 3.2 quantifies the trade-off for any traffic increase and is essentially tight. These results were among the first quantitative bounds of the price-of-anarchy programme and are a standard part of algorithmic game theory courses.

All statements here are proved in the paper (Theorem 5.3 with its proof omitted there as a close copy of Theorem 3.1). To our knowledge none has a machine-checked proof. This mission produces Lean proofs of Theorem 3.1, its supporting lemmas and its two variants, on top of the published Wardrop-equilibrium definitions of Kelly and Yudovina's chapter on road traffic; existence of a Wardrop equilibrium is already proved on the platform (KellyStochasticNetworks.wardrop_equilibrium_exists), so the goal's hypothesis is satisfiable.

Difficulty

The obvious comparison of $f$ with $f^*$ route by route fails: $f^*$ can place its traffic on edges whose latency is much lower than the Nash latencies, and nothing in the latency functions bounds how much lower, since they are only continuous and nondecreasing. A naive bound on the ratio $C(f)/C(f^*)$ is ruled out by the $x^p$ example above, so any proof must use the doubled rates essentially. In the Lean development, the passage from Definition 2.1 (a statement about perturbed flows) to the Wardrop condition needs a limit $\delta \to 0$ through continuity on $[0,\infty)$, and the cost manipulations need exchanges of finite double sums over routes and edges.

Formalization scope

• Routes, not graphs. Routes are arbitrary columns of a $0/1$ edge–route incidence matrix A, each assigned a commodity by s. The paper's family of simple $s_i$–$t_i$ paths is one instance; the statements therefore hold for every route family (a disclosed generalization; the proofs use no graph structure). Two copies of one edge set serving two commodities are two routes.
• Latencies are assumed nonnegative, nondecreasing and continuous on $[0,\infty)$ only. Continuity replaces the paper's differentiability, as licensed by footnote 3 (p. 7) and by §3 (p. 11).
• Rates are positive reals $r_i > 0$. The number of commodities may be $0$, the paper's $k = 0$, where all statements hold trivially.
• Definition 2.1 is formalized with $P_1 \ne P_2$ and $0 < \delta \le f_{P_1}$. The page writes $\delta \in [0, f_{P_1}]$ and does not exclude $P_1 = P_2$; read literally, $\delta = 0$ would force every route of a commodity, used or not, to have the same latency (contradicting Lemma 2.2), and $P_1 = P_2$ would make Nash flows fail to exist for strictly increasing latencies. Definition 5.1 follows the same convention.
• No ratios. Bounds are stated as $C(f) \le c\, C(f^*)$ for every feasible $f^*$, never as a quotient of costs, so a zero optimal cost cannot make a statement trivial. The constants $1/\gamma$ and $(1+\epsilon)/(1-\epsilon)$ carry $\gamma > 0$ and $0 < \epsilon < 1$.
• Feasibility for $2r$ is wardropFeasible s (fun i => 2 * rate i); for $(1+\gamma) r$ it is wardropFeasible s (fun i => (1 + γ) * rate i). Replacing $2r$ by $r$ would make the goal false (Pigou's example), and comparing only with an optimal $f^*$ would weaken it.
• $\bar\ell$ is a function of the Nash flow's edge flows, not a free parameter.

Needed infrastructure: finite double-sum exchanges, a one-sided limit argument for continuous functions on $[0,\infty)$, and bookkeeping of the perturbed flow $\tilde f$. The lemmas relating Definition 2.1 to the Wardrop condition are reusable by every later result on nonatomic routing games, including the other missions of this series. Contributions of proofs of any milestone are welcome.

Selected references

• T. Roughgarden and É. Tardos, How Bad is Selfish Routing?, Journal of the ACM 49(2), 236–259, 2002. https://doi.org/10.1145/506147.506153
• J. G. Wardrop, Some Theoretical Aspects of Road Traffic Research, Proceedings of the Institution of Civil Engineers 1(3), 325–378, 1952. https://doi.org/10.1680/ipeds.1952.11259
• D. Braess, A. Nagurney and T. Wakolbinger, On a Paradox of Traffic Planning (translation of Braess 1968), Transportation Science 39(4), 446–450, 2005. https://doi.org/10.1287/trsc.1050.0127
• F. Kelly and E. Yudovina, Stochastic Networks, Cambridge University Press, 2014, Chapter 4. https://doi.org/10.1017/CBO9781107284722

Why abandonment matters in call centers

Telephone call centers are among the largest employers of service labour, and their staffing decisions are made with queueing models. The classical model is the Erlang-C queue $M/M/N$: Poisson arrivals, $N$ agents, exponential service, infinitely patient callers. Real callers hang up. Garnett, Mandelbaum and Reiman (M&SOM 2002) argued that a model ignoring abandonment is misleading exactly in the regime where large call centers operate, near full utilization: the Erlang-C queue is unstable when the offered load exceeds the number of agents, while a real center simply loses the excess callers. They advocated the Erlang-A queue $M/M/N+M$, in which each caller also has an exponential patience, and developed its many-server asymptotics.

The first of their asymptotic results, Theorem 1 of the paper, settles the most basic performance measure, the fraction of callers who abandon, to first order as the center grows. Its proof combines a utilization argument with two monotonicity properties proved by Bhattacharya and Ephremides (1991) and an asymptotic expansion of Erlang's loss formula due to Jagerman (1974).

The Erlang-A queue

Callers arrive as a Poisson process of rate $\lambda>0$. There are $N\ge1$ statistically identical agents, each serving one caller at a time with exponentially distributed service times of rate $\mu>0$. The waiting room is unlimited and is served in order of arrival. Each caller carries a patience, an exponential random variable of rate $\theta>0$ independent of everything else; a caller whose wait in queue reaches his patience abandons and does not return.

The number of callers in the system, $Q$, is a birth–death process with birth rate $\lambda$ in every state and death rate

$$\mu_k=\min(k,N)\,\mu+(k-N)^+\,\theta$$

in state $k$. Its stationary distribution (Appendix B of the paper, with infinite buffer) is

$$\pi_k=\frac{(\lambda/\mu)^k}{k!}\,\pi_0\ (0\le k\le N),\qquad \pi_k=\prod_{j=N+1}^{k}\frac{\lambda}{N\mu+(j-N)\theta}\cdot\frac{(\lambda/\mu)^N}{N!}\,\pi_0\ (k>N),$$

with $\pi_0$ normalizing. The abandonment probability $P_N\{Ab\}$ is the probability that a caller arriving in steady state abandons. An arrival finding $N+n$ callers in the system abandons with probability $(n+1)\theta/(N\mu+(n+1)\theta)$, so

$$P_N\{Ab\}=\sum_{n\ge0}\pi_{N+n}\,\frac{(n+1)\theta}{N\mu+(n+1)\theta}.$$

The blocking probability $P_N\{Bl\}$ of the loss system $M/M/N/N$ with the same rates is Erlang's formula $E(\lambda/\mu,N)=\dfrac{(\lambda/\mu)^N/N!}{\sum_{j=0}^{N}(\lambda/\mu)^j/j!}$.

The asymptotic regime. The $N$-th system has $N$ agents, arrival rate $\lambda_N$, service rate $\mu$ independent of $N$, and patience rate $\theta_N$. As in §4 of the paper, $\lambda_N\to\infty$ and $\theta_N\to\theta\in(0,\infty)$. The traffic intensity is $\rho_N=\lambda_N/(N\mu)$.

Formalization targets

Goal: Theorem 1 (p. 215)

If $\rho_N\to\rho_\infty$ for some $0\le\rho_\infty\le\infty$, then

$$\lim_{N\to\infty}P_N\{Ab\}=\begin{cases}0,&0\le\rho_\infty\le1,\\ 1-1/\rho_\infty,&\rho_\infty>1,\end{cases}$$

with $1-1/\infty=1$. The limit does not depend on $\theta$.

Milestones

1. The explicit $\pi$ is the unique steady state of the Erlang-A birth–death process (Appendix B).
2. Equation (2): $\theta\,E[\#\text{ waiting}]=\lambda P\{Ab\}$.
3. Utilization below one: $\lambda_N(1-P_N\{Ab\})<N\mu$.
4. Property (ii): $P_N\{Ab\}$ is increasing in $\theta$.
5. $P_N\{Ab\}\to P_N\{Bl\}$ as $\theta\to\infty$.
6. $P_N\{Ab\}\le P_N\{Bl\}$ for every $0<\theta<\infty$.
7. Erlang's formula is increasing in the offered load (published and proved: KellyStochasticNetworks.erlang_strictMono).
8. Jagerman's expansion (10) of $P_N\{Bl\}$ for $\lambda_N=N\mu\rho_\infty$, $\rho_\infty>1$, as an asymptotic equivalence.
9. If $\lambda_N=N\mu\rho_\infty+o(N)$ with $\rho_\infty>1$, then $P_N\{Bl\}\to1-1/\rho_\infty$ and $\limsup_N P_N\{Ab\}\le 1-1/\rho_\infty$.
10. Property (i): $P_N\{Ab\}$ is increasing in $\lambda$.

Significance

Theorem 1 is the law-of-large-numbers description of an overloaded or critically loaded many-server queue with abandonment. It says that an overloaded center sheds exactly its excess load, $\lambda_N-N\mu$, to abandonment, and that a critically loaded center ($\rho_\infty=1$) already has vanishing abandonment. This is what directs attention to the Halfin–Whitt (quality-and-efficiency-driven) regime $\sqrt N(1-\rho_N)\to\beta$, where the paper's later results (Theorems 2 and 4) refine the picture to order $1/\sqrt N$. It is also the fluid-scale input of later work on staffing with abandonment.

The theorem has been proved in the paper; to our knowledge none of the statements above has a machine-checked proof. The mission produces a formal model of the Erlang-A queue with its stationary law, a verified bridge between the Erlang-A and Erlang-B (loss) systems, and a formal limit theorem for Erlang's loss formula under linear load, each reusable in other many-server problems.

Difficulty

The heuristic is immediate: utilization is at most one, so $\lambda_N(1-P_N\{Ab\})\le N\mu$ gives the lower bound $1-1/\rho_N$. The upper bound is the substance. A direct estimate of the series defining $P_N\{Ab\}$ involves $\theta$-dependent products whose asymptotics are not elementary, and the result must hold uniformly over patience rates $\theta_N$ that are only known to be positive. Two further obstacles remain: the monotonicity of $P_N\{Ab\}$ in $\theta$ and in $\lambda$ is a stochastic-ordering property of the birth–death process, not a term-by-term inequality between the series, and any comparison with the loss system needs the asymptotics of Erlang's formula under a load that is linear in $N$ only up to $o(N)$. Nothing is assumed about how $\rho_N$ approaches its limit, so the critical case $\rho_\infty=1$ cannot be read off from either side.

Formalization scope

• Model. All objects live in the namespace ErlangA.Abandonment. The death rates, the unnormalized weights $w_k$, $\pi_k=w_k/\sum_j w_j$ (a tsum) and $P_N\{Ab\}$ are explicit definitions of the parameters $N\in\mathbb N$ and $\lambda,\mu,\theta\in\mathbb R$; $P_N\{Bl\}$ is the published KellyStochasticNetworks.erlang (λ/μ) N.
• Steady state. "Stationary" means a probability distribution on $\{0,1,2,\dots\}$ solving the global balance equations (the published QueueingFundamentals.BirthDeath.IsSteadyState). The time limit $\lim_t P\{Q(t)=n\}$ is not formalized. The buffer is infinite.
• Abandonment probability. $P_N\{Ab\}$ is defined by the arrival-sees-time-average form above; the balance form $(\theta/\lambda)\sum_k(k-N)^+\pi_k$ is milestone 2. It is a probability per arriving caller, not the abandonment rate and not the probability that someone is waiting.
• Sequences. $N$ is both the index and the number of agents; hypotheses on the $N$-th system are imposed for $N\ge1$. $\mu>0$ is fixed.
• Limits. $\rho_\infty\in[0,\infty]$ is an extended nonnegative real and $\rho_N\to\rho_\infty$ is convergence in $[0,\infty]$; $1-1/\rho_\infty$ is evaluated there, giving $1$ at $\rho_\infty=\infty$. All limits are Filter.Tendsto along $N\to\infty$; "$\sim$" is Asymptotics.IsEquivalent; $\limsup\le c$ is "for every $\varepsilon>0$, eventually $\le c+\varepsilon$".
• Monotonicity. "Increasing" in properties (i) and (ii) is read as nondecreasing, in one parameter at a time with the others fixed.
• Ruling out trivial readings. Because $\pi$ is a quotient by a tsum, a divergent normalizing series would make $\pi\equiv0$ and $P_N\{Ab\}=0$, which would make the underloaded case of the goal vacuous; milestone 1 asserts that $\pi$ is a genuine probability distribution for every $N\ge1$ and $\lambda,\mu,\theta>0$, and the goal is stated for exactly these parameters.
• Welcome contributions. Stochastic-ordering arguments for birth–death processes (for properties (i) and (ii)), asymptotics of Erlang's loss formula (Jagerman's expansion, or a direct proof of the linear-load limit), and summation identities for the stationary law.

Selected references

• O. Garnett, A. Mandelbaum, M. Reiman, Designing a Call Center with Impatient Customers, Manufacturing & Service Operations Management 4(3):208–227, 2002. https://doi.org/10.1287/msom.4.3.208.7753
• P. P. Bhattacharya, A. Ephremides, Stochastic monotonicity properties of multiserver queues with impatient customers, Journal of Applied Probability 28(3):673–682, 1991. https://doi.org/10.2307/3214500
• D. L. Jagerman, Some properties of the Erlang loss function, Bell System Technical Journal 53(3):525–551, 1974. https://doi.org/10.1002/j.1538-7305.1974.tb02756.x
• S. Halfin, W. Whitt, Heavy-traffic limits for queues with many exponential servers, Operations Research 29(3):567–588, 1981. https://doi.org/10.1287/opre.29.3.567

Motivation

AdaBoost (Freund and Schapire, 1997) combines many weak classifiers $f_m(x) \in \{-1, 1\}$ into a weighted vote $\operatorname{sign}\big(\sum_m c_m f_m(x)\big)$. At each round it fits a classifier to a reweighted training sample, sets $c_m = \log((1 - \mathrm{err}_m)/\mathrm{err}_m)$ from the weighted error $\mathrm{err}_m$, and multiplies the weights of the misclassified points by $e^{c_m}$. The algorithm was introduced as a procedure for boosting the accuracy of weak learners in the PAC sense, and its good test performance was at first not explained by any statistical model.

Friedman, Hastie and Tibshirani (Ann. Statist. 28 (2000) 337–407) recast boosting as stagewise fitting of an additive model by minimizing the exponential criterion $J(F) = E(e^{-yF(x)})$. Their Lemma 1 shows that $J$ is minimized at half the log-odds, so an additive $F$ fitted this way estimates a logistic regression model. Result 1 of that paper, the subject of this mission, shows that Discrete AdaBoost is exactly such a fitting procedure: in its population version, each round is a Newton-like step on $J$ followed by an exact line search, and the resulting reweighting is AdaBoost's. This view underlies gradient boosting, LogitBoost and the loss-function analysis of boosting in later work.

Setting

Let $X$ be a measurable space of features and let $\nu$ be a probability law of the pair $(x, y)$ on $X \times \{-1, 1\}$. The conditional law of $y$ given $x$ is the disintegration $\nu(\cdot \mid x)$, and $E(\cdot \mid x)$ is the integral against it. A current estimate is a measurable $F : X \to \mathbb R$, and the exponential criterion is

$$J(F) = E\big(e^{-yF(x)}\big) \in [0, \infty].$$

With weight $w(x, y) = e^{-yF(x)}$, the weighted conditional expectation and the weighted expectation are

$$E_w[g(x, y) \mid x] = \frac{E[w(x, y) g(x, y) \mid x]}{E[w(x, y) \mid x]}, \qquad E_w[g(x, y)] = \frac{E[w(x, y) g(x, y)]}{E[w(x, y)]}.$$

A classifier is a measurable $f : X \to \{-1, 1\}$; its weighted error is $\mathrm{err} = E_w[1_{[y \neq f(x)]}]$. The paper's candidate update is $F \leftarrow F + cf$ with

$$f(x) = \begin{cases} 1, & E_w(y \mid x) > 0, \\ -1, & \text{otherwise}, \end{cases} \qquad (18) \qquad\qquad c = \frac12 \log\frac{1 - \mathrm{err}}{\mathrm{err}}. \qquad (20)$$

Algorithm 1 (p. 338) uses $c_m = \log((1 - \mathrm{err})/\mathrm{err}) = 2c$ and the update $w \leftarrow w \exp(c_m 1_{[y \neq f(x)]})$ followed by renormalization.

Formalization targets

Goal: Result 1 (p. 346)

For $F$ measurable with $J(F) < \infty$:

1. for every $c > 0$ and every $x$, the classifier (18) minimizes the quadratic approximation $E_w(1 - ycs + c^2/2 \mid x)$ over $s \in \{-1, 1\}$;
2. for every classifier $f$ with $0 < \mathrm{err} < 1$, the coefficient $c$ of (20) satisfies

$$J(F + cf) \le J(F + c'f) \qquad \text{for all } c' \in \mathbb R;$$

3. for every classifier $f$, every $x$ and $y$,

$$e^{-yF(x)} e^{-cf(x)y} = e^{-c} \cdot e^{-yF(x)} \exp\Big(\log\frac{1 - \mathrm{err}}{\mathrm{err}}\, 1_{[y \neq f(x)]}\Big),$$

so the population reweighting coincides with Algorithm 1's after renormalization.

Milestones

• the second-order expansion of $E_w(e^{-cys} \mid x)$ in $c$ (proof of Result 1, p. 346);
• (17)–(18): for $c > 0$, (16) is maximization of $E_w[yf(x)]$, solved by (18) (p. 347);
• (19): $-E_w[yf(x)] = E_w[(y - f(x))^2]/2 - 1$ (p. 347);
• (20): $c = \frac12\log((1-\mathrm{err})/\mathrm{err})$ is the unique minimizer of $E_w e^{-cyf(x)}$ (p. 347);
• $-yf(x) = 2 \times 1_{[y \neq f(x)]} - 1$ and the weight identity (p. 347);
• Corollary 2 (p. 348), referenced from the platform in its sample form;
• (21)–(22): the first-order condition of the line search (p. 348).

Significance

The result. Result 1 turns AdaBoost from a combinatorial reweighting scheme into an optimization method with a known objective. It identifies the population quantity the algorithm estimates (via Lemma 1, half the log-odds), explains the specific constant $\log((1-\mathrm{err})/\mathrm{err})$ as an exact line search, explains why the weights of misclassified points are inflated by $(1-\mathrm{err})/\mathrm{err}$, and shows that a weak learner worse than chance is used with reversed sign. It is the template for the other population results of the paper (Real AdaBoost, LogitBoost, Gentle AdaBoost) and for later functional-gradient views of boosting.

Formalizing it. The result is proved on paper; it has not been machine-checked. The paper's argument is stated informally ("≈", "arg min", "Newton-like"); this mission fixes each claim as a precise statement about measures on $X \times \{-1, 1\}$. The sample version of Corollary 2 is already proved on the platform (UnderstandingML.adaboost_reweighted_error) and is reused; everything else is new.

Difficulty

Each step is elementary on its own; the work is in carrying the population statements through measure theory. The weighted expectations are ratios of integrals that are meaningful only under integrability of $e^{-yF(x)}$, and the line-search claim compares $J(F + c'f)$ for all real $c'$, all of which must be shown finite before they can be compared as real numbers. The pointwise claim (16)–(18) uses the conditional law of $y$ given $x$, which exists only as a disintegration kernel; passing from it to the unconditional (17) requires the disintegration identity and measurability of (18) in $x$. The tempting shortcut of treating $J(F + cf)$ as its quadratic approximation does not prove the line-search claim: (20) is the exact minimizer of $J$, not of the approximation.

Formalization scope

Labels are Booleans, with $y = 1$ for true and $y = -1$ for false. $J$ is a lower Lebesgue integral in $[0, \infty]$ and is compared there; $E_w$ and $E_w(\cdot \mid x)$ are ratios of Bochner integrals, the conditional one against ν.condKernel x. Disclosed additions, each needed for the page's formulas to be defined: $F$ and $f$ measurable, $J(F) < \infty$, and $0 < \mathrm{err} < 1$ wherever $\log((1-\mathrm{err})/\mathrm{err})$ is used. No condition $\mathrm{err} < 1/2$ is imposed. Ties $E_w(y \mid x) = 0$ go to $-1$, as printed. The "≈" of the expansion is read as "second-order Taylor polynomial in $c$", and derivatives are stated with HasDerivAt.

Trivializing formalizations are excluded: $J$ is not defined by a conditional formula or as a Bochner integral (which would return $0$ on non-integrable weights and make every step optimal), the logarithm is never applied outside its domain, and the class of $f$ stays $\{-1, 1\}$-valued (over real-valued $f$ the Newton step is Gentle AdaBoost's, a different result).

Everything is in the namespace AddLogReg.Discrete, with one definitions file (Setting) holding $J$, $E_w$, the classifier (18), $\mathrm{err}$ and the coefficient (20). Reusable pieces are lemmas on disintegrations of laws on $X \times \mathrm{Bool}$ and on weighted expectations. Proofs of any milestone are welcome independently.

Selected references

• J. Friedman, T. Hastie and R. Tibshirani, Additive logistic regression: a statistical view of boosting, Ann. Statist. 28(2):337–407, 2000. https://doi.org/10.1214/aos/1016218223
• Y. Freund and R. E. Schapire, A decision-theoretic generalization of on-line learning and an application to boosting, J. Comput. System Sci. 55(1):119–139, 1997. https://doi.org/10.1006/jcss.1997.1504
• R. E. Schapire and Y. Singer, Improved boosting algorithms using confidence-rated predictions, Machine Learning 37:297–336, 1999. https://doi.org/10.1023/A:1007614523901

Motivation

Retailers accept large volumes of returned merchandise, and a common default is the full refund: a buyer who is unhappy with a product brings it back and gets the whole price back. Many consumers only learn how much they value a product after they have it at home — clothes that do not fit, a gadget that does not suit the buyer's needs. A returns policy therefore plays two roles at once. It raises the buyer's willingness to pay before purchase, and after purchase it decides which units stay with consumers and which go back to the seller to be salvaged.

Xuanming Su's paper Consumer Returns Policies and Supply Chain Performance (SSRN 1020451; published in Manufacturing & Service Operations Management 11(4), 2009, doi:10.1287/msom.1080.0240) puts this effect into a newsvendor model with random demand. The earlier literature it builds on, notably Che (1996) and Davis, Gerstner and Hagerty (1995), asked whether a seller should offer full refunds or no returns at all. Su's model makes the refund amount a separate decision variable. The answer it gives is closed-form and sharp: the optimal refund equals the salvage value. This mission formalizes Sections 3–4 of the paper: the single-seller model, the full-refund benchmark, and the optimal partial refund.

Setting

A seller stocks a quantity $q \ge 0$ before a selling season at unit cost $c$. Unsold and returned units are salvaged at value $s$. Market demand is a nonnegative random variable $X$ with law $D$, distribution function $F$ and $\bar F = 1 - F$. Each consumer who buys learns a valuation $V$ after purchase. Valuations are i.i.d. with law $\nu$ and finite mean $\mu = EV$, and the standing assumption is $\mu > c > s \ge 0$.

The seller chooses a price $p$, a quantity $q$ and a refund $r$. Once a consumer has bought, they keep the product if $V \ge r$ and return it otherwise. The keep and return probabilities are

$$\bar G(r) = \mathbb P(V \ge r), \qquad G(r) = \mathbb P(V < r).$$

Before purchase a consumer's expected utility from buying is $E\max(V, r)$, so this is the reservation price. Every consumer buys if $p \le E\max(V, r)$ and nobody buys otherwise (the demand rule (6)). With $E\min(X, q)$ the expected sales of a stock $q$, the seller's expected profit (7)–(8) is

$$\Pi(p,q,r) = \big[(p-s)\bar G(r) + (p-r)G(r)\big]\,E\min(X,q) - (c-s)q \quad\text{if } p \le E\max(V,r),$$

and $-(c-s)q$ otherwise. Two special cases serve as benchmarks. Under full refunds ($r = p$) every consumer buys and the profit is $\Pi_{\text{full}}(p,q) = (p-s)\bar G(p)E\min(X,q) - (c-s)q$, from (1)–(2). Under no returns the price is $\mu$ and the profit is $\Pi_{\text{no}}(q) = (\mu - s)E\min(X,q) - (c-s)q$, from (3). Social welfare (12)–(13) is the sum of consumer surplus and seller profit, $SW(p,q,r) = \int_{[r,\infty)}(v-s)\,d\nu(v)\cdot E\min(X,q) - (c-s)q$, again subject to the demand rule.

Formalization targets

Goal: Proposition 2 (p. 11)

With $p^* = E\max(V,s)$, $r^* = s$ and any $q^*$ satisfying

$$\bar F(q^*) = \frac{c-s}{E\max(V,s) - s},$$

the triple $(p^*, q^*, r^*)$ maximizes $\Pi$ over all prices, all refunds and all quantities $q \ge 0$:

$$\Pi(p,q,r) \le \Pi(p^*, q^*, r^*).$$

Milestones

1. The reservation price splits as $E\max(V,r) = rG(r) + \int_{[r,\infty)} v\,d\nu$, which is the step (28)→(29) of the proof (p. 26).
2. At $p = E\max(V,r)$ the per-unit margin $(p-s)\bar G(r) + (p-r)G(r)$ equals $\int_{[r,\infty)}(v-s)\,d\nu$, displays (27)–(30), p. 26.
3. This integral is maximized at $r = s$ (p. 26).
4. Hence $(E\max(V,s), s)$ maximizes the margin subject to $p \le E\max(V,r)$, the first step of the proof (p. 26).
5. The newsvendor critical fractile, a reference to a proved platform theorem (p. 26).
6. Proposition 1(i) (p. 9): under full refunds, $p^* \in \arg\max_p (p-s)\bar G(p)$ with $\bar F(q^*) = (c-s)/((p^*-s)\bar G(p^*))$ is optimal.
7. Proposition 1(ii) at $s = 0$ (p. 26): with nonnegative valuations, no returns beats every full-refund policy.
8. Corollary 1 (p. 12): the inequality $(p-s)\bar G(p) \le E\max(V,s) - s$ (p. 26), and its consequence that partial refunds earn at least the full-refund profit and, for strictly increasing $F$, stock at least as much.
9. Corollary 2 (p. 13): the triple of Proposition 2 also maximizes social welfare.

Significance

The result separates two things that a full refund ties together: the price and the refund. Setting $r = s$ sends every unit back to its more valuable use. Consumers who value the product above its salvage value keep it, and the rest return it to be salvaged. The price $E\max(V,s)$ then extracts the whole expected surplus. Consequences follow directly. Partial refunds dominate both full refunds and no returns (Corollary 1). They raise the stocking quantity, which benefits an upstream manufacturer paid per unit ordered. With valuation uncertainty resolved only after purchase, the monopoly outcome is welfare-maximizing (Corollary 2). Section 5 of the paper, formalized in the companion mission, uses Proposition 2's triple as the first-best target that supply chain contracts must implement.

The results are proved on paper with short arguments in Appendix A of the paper. None of them has a machine-checked proof. The mission's contribution is a formal model of consumer returns with the demand rule built in, plus checked versions of Propositions 1–2 and Corollaries 1–2 for general valuation laws (with atoms), not only densities.

Difficulty

The paper's proof treats the problem as separable: first maximize the margin over $(p, r)$, then solve a newsvendor problem in $q$. Two steps that are routine on paper need care. First, the margin bound must hold over the whole constrained region $p \le E\max(V, r)$, including refunds above the price and negative prices. It rests on comparing $\int_{[r,\infty)}(v-s)\,d\nu$ with $\int_{[s,\infty)}(v-s)\,d\nu$, which needs the closed half-line convention to hold up at atoms of $\nu$. Second, the newsvendor step must be done for a demand law that may have atoms, where $\bar F$ has no inverse. Without the demand rule the problem is not separable at all: formula (8) alone is unbounded in $p$. Without nonnegativity of demand and quantity it is unbounded in the other direction.

Formalization scope

Lean represents all prices, refunds, costs, quantities and profits as real numbers. The valuation law is a probability measure ν on ℝ with integrable identity, so a density is not required. The demand law is a probability measure D on ℝ with D (Set.Iio 0) = 0. $\bar G(r)$ is (ν (Set.Ici r)).toReal and $G(r)$ is (ν (Set.Iio r)).toReal, following the page's tie rule (keep iff $V \ge r$). $E\min(X,q)$ is SupplyChainTheory.expSales D q from the published module SupplyChainTheory_contracts, and $\bar F$ is 1 - ProbabilityTheory.cdf D. Printed page numbers equal PDF page numbers throughout the source.

Committed conventions and readings:

• Demand rule inside the objectives. Profit and welfare are zero-demand cash flows when $p > E\max(V,r)$.
• Nonnegativity. Stocking quantities range over $q \ge 0$ and demand is nonnegative. Both are the page's words ("stocking quantity", "a mass of infinitesimal consumers"), and without them the profit is unbounded.
• Salvage value. $0 \le s$, as on p. 26.
• Optimality, not uniqueness. Every optimum is stated as optimality of the page's closed-form triple. Uniqueness fails when $\nu$ has gaps: if $\nu$ puts no mass on $[s, r)$, the refund $r$ is optimal too.
• No continuity of $F$ for the goal. The goal assumes no continuity of $F$. Existence of $q^*$ is not claimed.
• Corollary 1, quantity part. The quantity comparison assumes $F$ strictly increasing on $[0,\infty)$, which the proof's $\bar F^{-1}$ presumes. Without it the statement is false.
• Proposition 1(ii) at $s = 0$. This case assumes nonnegative valuations. The "sufficiently low" form of Proposition 1(ii) is not formalized.

A trivializing formalization is ruled out: $p^*$ and $r^*$ are the explicit values $E\max(V,s)$ and $s$, not an argmax chosen by Classical.choose. The maximization ranges over all $(p, r)$ and all $q \ge 0$, not a set restricted to $r = s$. The returned-units cash flow $(p - r + s)G(r)$ appears in the profit.

The newsvendor step reuses the proved platform theorem SupplyChainTheory.chain_optimal_fractile. The other pieces needed are elementary lemmas on integrals over half-lines and the concavity of $q \mapsto E\min(X,q)$. They are reusable for any newsvendor-type model. Proofs of any milestone, and a general-law newsvendor optimality lemma that does not need a continuous $F$, are welcome.

Selected references

• X. Su, Consumer Returns Policies and Supply Chain Performance, SSRN working paper 1020451, version of August 2008. https://ssrn.com/abstract=1020451 — published in Manufacturing & Service Operations Management 11(4), 2009. https://doi.org/10.1287/msom.1080.0240
• Y.-K. Che, Customer Return Policies for Experience Goods, Journal of Industrial Economics 44(1), 1996. https://doi.org/10.2307/2950560
• S. Davis, E. Gerstner, M. Hagerty, Money Back Guarantees in Retailing: Matching Products to Consumer Tastes, Journal of Retailing 71(1), 1995. https://doi.org/10.1016/0022-4359(95)90010-1

Motivation

The log-Sobolev constant $\alpha$ of a finite Markov chain controls how fast the chain forgets its starting point in relative entropy and in $\ell^2$, and it gives sharper mixing-time bounds than the spectral gap $\lambda$ when the stationary distribution has very small atoms. Diaconis and Saloff-Coste (Ann. Appl. Probab. 6 (1996)) made this constant a standard tool for finite chains. A practical obstacle runs through their paper: $\alpha$ is defined by a nonlinear variational problem, and exact values are known for very few chains. Lower bounds on $\alpha$ for a complicated chain are usually obtained by comparison with a simple chain whose constant is known exactly.

The Appendix of that paper computes such a reference value. For the chain that forgets its state in one step, $K(x,y)=\pi(y)$, it determines $\alpha$ in closed form for every positive $\pi$, and with it the log-Sobolev constant of every chain on two points and of the random walk on the complete graph.

Timeline. Rothaus's work on log-Sobolev inequalities (references [38–40] of the paper) studied the constant through its minimizers, the approach the Appendix follows. Diaconis and Saloff-Coste (1996) give the formula $\alpha=(1-2\pi_*)/\log(1/\pi_*-1)$, and note that Higuchi and Yoshida independently found the asymmetric two-point value.

Setting

Let $\mathcal X$ be a finite set and $K$ a Markov kernel on it: $K(x,y)\ge0$ and $\sum_y K(x,y)=1$. Let $\pi$ be an invariant probability, $\sum_x\pi(x)K(x,y)=\pi(y)$, with $\pi(x)>0$ for every $x$. Functions on $\mathcal X$ are real. Write $Kf(x)=\sum_yK(x,y)f(y)$, $\langle f,g\rangle=\sum_x f(x)g(x)\pi(x)$, $\|f\|_2^2=\langle f,f\rangle$, $E_\pi f=\sum_x f(x)\pi(x)$ and $\mathrm{Var}_\pi(f)=\|f-E_\pi f\|_2^2$.

The Dirichlet form is $\mathcal E(f,g)=\langle (I-K)f,g\rangle$. The entropy functional is

$$\mathcal L(f)=\sum_{x\in\mathcal X}|f(x)|^2\log\frac{|f(x)|^2}{\|f\|_2^2}\,\pi(x),$$

which is nonnegative and vanishes exactly when $|f|$ is constant. The spectral gap and the log-Sobolev constant are

$$\lambda=\inf\Big\{\frac{\mathcal E(f,f)}{\mathrm{Var}_\pi(f)}:\mathrm{Var}_\pi(f)\ne0\Big\},\qquad \alpha=\inf\Big\{\frac{\mathcal E(f,f)}{\mathcal L(f)}:\mathcal L(f)\ne0\Big\}.$$

Equivalently, $1/\alpha$ is the best constant $C$ in $\mathcal L(f)\le C\,\mathcal E(f,f)$.

The chain of the mission is $K(x,y)=\pi(y)$: at each step it draws a fresh point from $\pi$, ignoring its current state. Its invariant measure is $\pi$, and $\pi_*=\min_{\mathcal X}\pi$ is its smallest atom. In Lean the objects are dirichlet, entL, gap, logSobolev, indepChain and piMin in the namespace LogSobolevMC.TwoPoint.

Formalization targets

Goal: Theorem A.1

For a positive probability $\pi$ on $\mathcal X$ with $\pi_*<1/2$, the chain $K(x,y)=\pi(y)$ has

$$\alpha=\frac{1-2\pi_*}{\log(1/\pi_*-1)},$$

and in particular, for $\pi\equiv1/|\mathcal X|$ with $|\mathcal X|\ge3$, $\alpha=(1-2/|\mathcal X|)/\log(|\mathcal X|-1)$. The goal is an equality, so it contains both a log-Sobolev inequality with this constant and the existence of functions that make it sharp.

Milestones

1. Lemma 3.1: $2\alpha\le\lambda$ for every chain.
2. $\mathcal E(|f|,|f|)\le\mathcal E(f,f)$ (proof of Theorem A.1).
3. Either $\alpha=\lambda/2$, or the infimum is attained at a nonconstant nonnegative function (proof of Theorem A.1).
4. (A.3): a positive minimizer $u$ of a reversible chain satisfies $2u\log u-2u\log\|u\|_2-\alpha^{-1}(I-K)u=0$.
5. (A.1): the explicit pair $a=\log[(1-\theta)/\theta]/(1-2\theta)$, $s=(1-2\theta)/(2\theta(1-\theta))$ solves the two-equation system of the proof of Theorem A.2.
6. Theorem A.2: the two-point chain with both rows $(\theta,1-\theta)$, $0<\theta\le1/2$, has $\alpha(\theta)=(1-2\theta)/\log[(1-\theta)/\theta]$, with the limit value $1/2$ at $\theta=1/2$.

Consequences

Corollary A.3 (every two-point chain), Corollary A.4 ($\alpha(K)\ge(1-2\pi_*)\lambda(K)/\log[1/\pi_*-1]$ for every finite chain) and Corollary A.5 (the complete graph, $\alpha=(|\mathcal X|-2)/((|\mathcal X|-1)\log(|\mathcal X|-1))$, and $\alpha=1/(2\log2)$ on $\mathbb Z_3$).

Significance

The result. Theorem A.1 is one of the few exact log-Sobolev constants known for a whole family of chains. Since this chain has $\lambda=1$, the formula shows that $\alpha$ can be smaller than $\lambda/2$ by a factor of order $\log(1/\pi_*)$, which answers the question on p. 715 of how far $2\alpha$ and $\lambda$ can be apart. Corollary A.4 turns this into a general tool: any spectral gap bound gives a log-Sobolev bound, losing only a factor $\log(1/\pi_*-1)/(1-2\pi_*)$. Corollary A.3 settles every chain on two points, and Corollary A.5 gives the complete graph, a frequent reference chain for comparison arguments.

Formalizing it. These results are proved in the paper. To our knowledge none of them, nor the log-Sobolev constant of a finite Markov chain itself, has a machine-checked formalization. The mission produces the definitions of $\mathcal E$, $\mathcal L$, $\lambda$ and $\alpha$ for finite chains, and exact values that later comparison arguments can cite.

Difficulty

The upper bound $\alpha\le(1-2\pi_*)/\log(1/\pi_*-1)$ needs only a good test function. The lower bound is the hard part: it is a statement about every function on $\mathcal X$, and $\mathcal L$ is neither quadratic nor convex. The obvious route, comparing with the spectral gap, loses exactly the logarithmic factor the theorem is about. Reducing to two-valued functions requires the infimum to be attained and analysed through its minimizers. The two-point problem that remains is a one-parameter inequality $l(s)\le a\,e(s)$ on an interval. The authors describe its solution as a calculus exercise that depended on numerical guessing, and it has removable singularities at $\theta=1/2$.

Formalization scope

$\mathcal X$ is a Fintype with decidable equality. $K$ is a Matrix V V ℝ and $\pi$ a function V → ℝ. Stochasticity, invariance, distributions and reversibility are the published MarkovMixing predicates (IsStochastic, IsStationary, IsDist, DetailedBalance) from mm_basic, and $\mathrm{Var}_\pi$ is MarkovMixing.distVar from mm_lower. Positivity of $\pi$ is a hypothesis throughout, as in §2.1. The infima $\lambda$ and $\alpha$ are Lean sInfs over exactly the sets of (2.4) and (3.1). $\mathcal E$ is the bilinear form $\langle (I-K)f,g\rangle$. $\lambda$ is the variational gap, not the eigenvalue-based MarkovMixing.spectralGap, which agrees with it only for reversible chains.

Disclosed additions, all at removable singularities of the printed formulas: $\pi_*<1/2$ in Theorem A.1 (and $|\mathcal X|\ge3$ in its uniform case); the explicit limit value $1/2$ at $\theta=1/2$ in Theorem A.2; strict $\pi(0)<\pi(1)$ in Corollary A.3; and $|\mathcal X|\ge3$ in Corollary A.5. In (A.3), reversibility, positivity of $u$ and $\alpha>0$ are added. Irreducibility is not assumed anywhere.

Trivializing formalizations are ruled out. A closed form evaluated at $0/0$ would be Lean's value $0$, so each such case is excluded or replaced by its limit. Real.log of a nonpositive number and an sInf over an empty or unbounded set do not occur under the stated hypotheses. Dropping the positivity or invariance of $\pi$, or replacing $\lambda$ by the eigenvalue gap, would change the statements. Stating the goal for two points only, or assuming the minimizer is two-valued, would state a step of the proof.

Contributions welcome: the general facts $\mathcal L\ge0$, $\mathcal E(f,f)=\tfrac12\sum_{x,y}(f(x)-f(y))^2K(x,y)\pi(x)$ and the existence of minimizers are reusable for every log-Sobolev development on finite spaces. The two-point calculus of Theorem A.2 is self-contained real analysis.

Selected references

• P. Diaconis and L. Saloff-Coste, Logarithmic Sobolev inequalities for finite Markov chains, Ann. Appl. Probab. 6(3):695–750, 1996. https://doi.org/10.1214/aoap/1034968224
• D. A. Levin, Y. Peres and E. L. Wilmer, Markov Chains and Mixing Times, AMS, 2009 (source of the MarkovMixing definitions used here). https://doi.org/10.1090/mbk/058