Analysis

Motivation

For a square matrix $A$, the spectrum alone does not control the size of $p(A)$: a nonzero nilpotent matrix has spectrum $\{0\}$ yet $\|A\|>0$. The numerical range $W(A)=\{u^*Au:\ \|u\|=1\}$ is a compact convex set containing the spectrum (Toeplitz–Hausdorff), and it does retain enough information. Crouzeix's conjecture (2004) asserts that for every polynomial $p$,

$$\|p(A)\|\le 2\max_{z\in W(A)}|p(z)|,$$

i.e. that $W(A)$ is a $2$-spectral set; the constant $2$ would be optimal. Such bounds are used to estimate matrix functions in numerical linear algebra (for example GMRES convergence through Faber polynomials) and in operator theory. The complete version asks for the same constant when the polynomial has $m\times m$ matrix coefficients, uniformly in $m$; by Paulsen's theorem this is equivalent to similarity of the conformal disk image of $A$ to a contraction with condition number at most $2$.

Background

• 1918–1919 — Toeplitz and Hausdorff prove convexity of the numerical range (Math. Z. 1918, Math. Z. 1919).
• 1972, 1984 — Arveson's dilation theory (Acta Math. 128, 1972) and Paulsen's similarity theorem (Proc. AMS 92, 1984) relate complete contractivity, dilations and similarity.
• 1999 — Delyon and Delyon's positive integral representations (Bull. SMF 1999).
• 2004 — Crouzeix formulates the constant-two question (IEOT 2004); 2007 — he proves a universal complete bound $11.08$ (JFA 2007).
• 2006 — Badea, Crouzeix and Delyon obtain the complete constant $2$ for $2\times2$ matrices (Math. Z. 2006).
• 2017–2018 — Crouzeix and Palencia prove the complete bound $1+\sqrt2$ (SIMAX 2017); Ransford and Schwenninger simplify the argument (SIMAX 2018).
• 2026 — Scalar ($m=1$) constant-two proofs appear in preprints of Jin, Lorist–Schwenninger (arXiv:2608.03841) and Luo; Åhag, Czyż and Virtanen prove the complete inequality for base matrices of order at most three (arXiv:2608.27346).
• September 2026 — Two OpenAI preprints claim the complete inequality in all dimensions: a structural proof via an optimal similarity and a common positive boundary density, extended to all bounded Hilbert-space operators (source), and a direct coefficient proof for matrices (source).

This mission asks for a formal proof of the complete Crouzeix inequality for matrices, with its sharpness, as stated in Theorem 1.1 of an OpenAI preprint dated September 26, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.

Setting

For $A\in M_n(\mathbb C)$ ($n\ge1$) let $W(A)=\{u^*Au: u\in\mathbb C^n,\ u^*u=1\}$. A matrix polynomial of degree $d$ with coefficient size $m\ge1$ is $P(z)=\sum_{k=0}^dB_kz^k$ with $B_k\in M_m(\mathbb C)$. Its evaluation at $A$ is

$$P[A]=\sum_{k=0}^d A^k\otimes B_k\ \in M_n(\mathbb C)\otimes M_m(\mathbb C),$$

with the base space first. All norms are Euclidean operator norms. For $m=1$ this is the usual $p(A)$.

Formalization targets

Milestone: the inequality (Theorem 1.1, p. 1, first assertion)

For all $n,m\ge1$, $d\ge0$, $A\in M_n(\mathbb C)$ and $B_0,\dots,B_d\in M_m(\mathbb C)$,

$$\Bigl\|\sum_{k=0}^dA^k\otimes B_k\Bigr\|\ \le\ 2\max_{z\in W(A)}\Bigl\|\sum_{k=0}^dB_kz^k\Bigr\| .$$

Milestone: sharpness (Theorem 1.1, p. 1, second assertion)

If the inequality holds with a constant $c$ in place of $2$ for all $n,m,d,A,B$, then $c\ge2$.

Goal: Theorem 1.1 (p. 1)

Both assertions together: the constant $2$ is valid and no smaller universal constant is.

Significance

The result itself. It settles the complete Crouzeix conjecture in its matrix formulation, uniformly in the base dimension $n$, the coefficient size $m$ and the degree, including matrices whose numerical range is a point or a segment. The scalar case $m=1$ had recently been proved by other authors and the complete case was known only for $n\le3$; a scalar argument need not survive matrix amplification because coefficient matrices do not commute. Equivalently, the numerical range is a complete $2$-spectral set for every matrix, which via Paulsen's theorem gives a similarity of condition number at most $2$ making the conformal disk image of $A$ a contraction. A companion OpenAI preprint gives a separate structural proof and extends the bound to all bounded operators on Hilbert spaces.

Formalizing it. The proof uses exterior conformal maps of analytic convex domains, Faber-type coefficients, a positive double-layer kernel, and a $2\times2$ block positivity argument; Section 4 then approximates an arbitrary numerical range by analytic convex domains. A formal proof would provide numerical ranges, Faber polynomials and conformal collars in Lean, all reusable in matrix analysis. No machine-checked proof of any constant-$2$ Crouzeix bound is known.

Difficulty

The naive approach through the spectrum fails for non-normal matrices, and the classical Crouzeix–Palencia method (a positive double-layer potential plus a Cauchy transform of conjugate data) loses a factor and yields $1+\sqrt2$. To reach $2$ in the complete setting, the argument must keep both multiplication orders $FG$ and $GF$ of matrix-valued test functions, since the coefficients do not commute. The preprint chooses a top singular pair $(x,y)$ of $F[A]$, represents three functionals through the resolvent, and must show that the resulting coefficient weights (one on the constant term, one half on the others) match exactly the Fourier weights of the diagonal compressions (Section 2, Proposition 2.2, p. 5; Theorem 3.2, p. 6). Degenerate numerical ranges with empty interior require a separate approximation step (Lemma 4.1, p. 9).

Formalization scope

• Matrices are Matrix (Fin n) (Fin n) ℂ with the L2 operator norm (Matrix.Norms.L2Operator). The numerical range is the set of $\langle x, Ax\rangle$ over unit vectors of EuclideanSpace ℂ (Fin n).
• Coefficients are B : Fin (d+1) → Matrix (Fin m) (Fin m) ℂ; the evaluation is $\sum_k A^k\otimes_{\mathrm{Kron}}B_k$ indexed by Fin n × Fin m, base factor first.
• rangeMaximum A B is the sSup of $\|P(z)\|$ over $W(A)$. Since $n\ge1$, $W(A)$ is nonempty and compact, so this is the true maximum; UniversalBound C quantifies over all $n,m\ge1$, all $d$, all $A$ and $B$.
• The goal OAI.CompleteCrouzeix.main is UniversalBound 2 ∧ ∀ C, UniversalBound C → 2 ≤ C. The two milestones state the same two clauses in the DirectCrouzeix namespace, whose definitions are identical in content.
• No normality, invertibility or nonempty-interior hypothesis is imposed on $A$.

Selected references

• OpenAI, A direct proof of the complete Crouzeix inequality, OpenAI Math Release preprint, September 26, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-direct-proof-of-the-complete-Crouzeix-inequality-September-26-2026/paper.pdf
• OpenAI, The complete Crouzeix theorem: optimal similarity and a common positive boundary representation, OpenAI Math Release preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-complete-Crouzeix-theorem-September-23-2026/paper.pdf
• M. Crouzeix, Bounds for analytical functions of matrices, Integral Equations Operator Theory 48 (2004), 461–477. https://doi.org/10.1007/s00020-002-1188-6
• M. Crouzeix, Numerical range and functional calculus in Hilbert space, J. Funct. Anal. 244 (2007), 668–690. https://doi.org/10.1016/j.jfa.2006.10.013
• M. Crouzeix, C. Palencia, The numerical range is a $(1+\sqrt2)$-spectral set, SIAM J. Matrix Anal. Appl. 38 (2017), 649–655. https://doi.org/10.1137/17M1116672
• T. Ransford, F. L. Schwenninger, Remarks on the Crouzeix–Palencia proof that the numerical range is a $(1+\sqrt2)$-spectral set, SIAM J. Matrix Anal. Appl. 39 (2018), 342–345. https://doi.org/10.1137/17M1143757
• C. Badea, M. Crouzeix, B. Delyon, Convex domains and K-spectral sets, Math. Z. 252 (2006), 345–365. https://doi.org/10.1007/s00209-005-0857-y
• B. Delyon, F. Delyon, Generalization of von Neumann's spectral sets and integral representation of operators, Bull. Soc. Math. France 127 (1999), 25–41. https://doi.org/10.24033/bsmf.2340
• E. Lorist, F. L. Schwenninger, A solution to Crouzeix's conjecture, arXiv:2608.03841 (2026). https://arxiv.org/abs/2608.03841v2
• P. Åhag, R. Czyż, J. Virtanen, The complete Crouzeix conjecture in dimension three and the Clouâtre–Ostermann–Ransford conjecture, arXiv:2608.27346 (2026). https://arxiv.org/abs/2608.27346v4
• O. Toeplitz, Das algebraische Analogon zu einem Satze von Fejér, Math. Z. 2 (1918), 187–197. https://doi.org/10.1007/BF01212904
• F. Hausdorff, Der Wertvorrat einer Bilinearform, Math. Z. 3 (1919), 314–316. https://doi.org/10.1007/BF01292610

Motivation

A dispatcher assigns each arriving job to one of $n$ servers. Sending it to a uniformly random server is simple but produces long queues near capacity; sending it to the globally shortest queue requires full state information. The power of $d$ choices sits between the two: each job samples $d$ servers at random and joins the shortest of them. Mitzenmacher's analysis of this supermarket model (IEEE TPDS 12(10), 2001) together with the balls-into-bins result of Azar, Broder, Karlin and Upfal (SIAM J. Comput. 29(1), 1999), established that a second random choice changes the behaviour of the system qualitatively. The idea underlies load balancers, hashing schemes and distributed schedulers.

This mission formalizes the paper's quantitative statement of that improvement in heavy traffic, the regime where the arrival rate per server $\lambda$ approaches the service rate $1$.

Setting

Customers arrive as a Poisson stream of rate $\lambda n$ with $0\le\lambda<1$, service times are exponential with mean $1$, and each customer joins the shortest of $d$ queues sampled uniformly with replacement. As $n\to\infty$ the fraction of queues with at least $i$ customers follows a deterministic limiting system with fixed point $\pi_i=\lambda^{(d^i-1)/(d-1)}$. Corollary 2 of the paper shows that, for $d\ge2$, the expected time a customer spends in that limiting system converges to

$$T_d(\lambda)=\sum_{i=1}^{\infty}\lambda^{\frac{d^i-d}{d-1}} .$$

With a single choice the system is $n$ independent M/M/1 queues, and the expected time is

$$T_1(\lambda)=\frac{1}{1-\lambda}.$$

This mission takes these two formulas as its definitions; the limiting system itself and the convergence to $T_d(\lambda)$ are the subject of the companion mission (part I). The auxiliary function of Lemma 3 is

$$F_d(\lambda)=\frac{\sum_{i=0}^{\infty}\lambda^{d^i}}{\log\frac{1}{1-\lambda}} .$$

Throughout, $d\ge2$ is an integer and logarithms are natural.

Formalization targets

Goal: Theorem 4, limit clause (p. 1099)

$$\lim_{\lambda\to1^-}\frac{T_d(\lambda)}{\log T_1(\lambda)}=\frac{1}{\log d}\qquad(d\ge2).$$

Milestones, in the order the paper's argument uses them

1. The rewriting of $T_d$ (proof of Theorem 4): with $\lambda'=\lambda^{1/(d-1)}$ and $0<\lambda<1$,

$$T_d(\lambda)=\frac{\sum_{i=1}^{\infty}(\lambda')^{d^i}}{\lambda^{d/(d-1)}} .$$

2. The product identity (proof of Lemma 3): for $0\le\lambda<1$,

$$\prod_{i=0}^{\infty}\bigl(1+\lambda^{d^i}+\lambda^{2d^i}+\dots+\lambda^{(d-1)d^i}\bigr)=\frac{1}{1-\lambda}.$$

3. Lemma 3:

$$\lim_{\lambda\to1^-}F_d(\lambda)=\frac{1}{\log d}.$$

The goal is a statement about the shape of the growth, not a constant: it pins the leading behaviour $T_d(\lambda)\sim\log_d\frac{1}{1-\lambda}$.

Significance

Theorem 4 makes "exponential improvement" precise. With one choice the expected time grows like $\frac1{1-\lambda}$ as the load approaches capacity; with $d\ge2$ choices it grows like $\frac{\log\frac1{1-\lambda}}{\log d}$. It also quantifies the diminishing return of extra choices: going from $d=2$ to $d$ only divides the leading term by $\log_2 d$, while going from one choice to two changes its order. These constants are the benchmark against which later heavy-traffic analyses of join-the-shortest-of-$d$ policies are compared.

The result is proved in the paper (the limit clause; see Difficulty for the other clause). No machine-checked version is known to exist. The formalization yields a self-contained Lean development of the lacunary series $\sum_i x^{d^i}$ near $x=1$ and of the base-$d$ product identity, both of which are classical analytic facts with uses outside queueing (lacunary power series, digit expansions).

Difficulty

The obvious approach compares $\sum_i\lambda^{d^i}$ with an integral, but the terms are not monotone images of a smooth function of a continuous index in a way that controls the error uniformly as $\lambda\to1^-$: the number of terms close to $1$ grows like $\log_d\frac{1}{1-\lambda}$ and each of them contributes nearly $1$, so the error terms are of the same order as the quantity being measured. The difficulty is to obtain matching upper and lower bounds with constants tending to $1/\log d$, uniformly as $\lambda\to1^-$. Passing from Lemma 3 to Theorem 4 additionally requires controlling the change of variable $\lambda\mapsto\lambda^{1/(d-1)}$ inside the logarithm.

Theorem 4 as printed also contains a first clause, $T_d(\lambda)\le c_d\log T_1(\lambda)$ for all $\lambda\in[0,1]$. It is false as printed near $\lambda=0$: $T_d(\lambda)\ge1$ while $\log T_1(\lambda)\to0$. The paper does not prove it, and this mission does not pose it.

Formalization scope

• Representation. $\lambda$ is a real number (lam), $d$ a natural number with the hypothesis $2\le d$ on every statement. $T_d$, $T_1$ and $F_d$ are real-valued definitions in one definition file.
• Exponents. $T_d$'s $i$-th term uses the natural-number exponent $\sum_{1\le k<i}d^k=\frac{d^i-d}{d-1}$, so its $i=1$ term is $\lambda^0=1$. The series runs over $i\in\mathbb N$ with the $i=0$ term equal to $0$. $\lambda'=\lambda^{1/(d-1)}$ and $\lambda^{d/(d-1)}$ are real powers.
• Series and junk values. All series are real tsums; they converge for $0\le\lambda<1$. Outside that range Lean's conventions (a divergent series sums to $0$, $x/0=0$, $\log x=0$ for $x\le0$) produce meaningless values, so every statement either restricts $\lambda$ to $[0,1)$ or $(0,1)$ or is a limit along $\lambda<1$.
• Limits. "$\lambda\to1^-$" is the one-sided filter 𝓝[<] 1; the limit $1/\log d$ uses Real.log.
• Infinite product. The product identity is stated with HasProd (unconditional convergence of finite subproducts), which for factors $\ge1$ is the same as convergence of the partial products.
• Not trivializable. Because every limit is one-sided at $1$ and the denominators $\log T_1(\lambda)$ and $\log\frac1{1-\lambda}$ are positive there, no statement can be satisfied by Lean's junk values at $\lambda\ge1$ or at $\lambda=0$; the summability of the rewritten series is asserted explicitly.
• Infrastructure. Useful general lemmas: asymptotics of $\sum_i x^{d^i}$ as $x\to1^-$, products of finite geometric sums, change of variables in one-sided limits. These are reusable beyond this mission. Contributions of any of the milestones, or of alternative proofs of Lemma 3, are welcome.

Selected references

• M. Mitzenmacher, The Power of Two Choices in Randomized Load Balancing, IEEE Transactions on Parallel and Distributed Systems 12(10), 2001, pp. 1094–1104. https://doi.org/10.1109/71.963420
• Y. Azar, A. Z. Broder, A. R. Karlin, E. Upfal, Balanced Allocations, SIAM Journal on Computing 29(1), 1999, pp. 180–200. https://doi.org/10.1137/S0097539795288490

Motivation

The Learning with Errors (LWE) problem, introduced by Regev in On Lattices, Learning with Errors, Random Linear Codes, and Cryptography (J. ACM 56(6), 2009, Article 34; doi:10.1145/1568318.1568324), asks to recover a secret vector $s \in \mathbb{Z}_p^n$ from noisy inner products $\langle a, s\rangle/p + e \bmod 1$. The noise $e$ is drawn from a periodic normal distribution $\Psi_\beta$ on the circle $\mathbb{T} = \mathbb{R}/\mathbb{Z}$: a centred normal variable reduced modulo $1$. LWE has since become the main hardness assumption of lattice-based cryptography, including the post-quantum standards built on it.

Regev's reductions repeatedly need to compare $\Psi_\alpha$ and $\Psi_\beta$ for nearby parameters, for instance when the noise parameter is known only up to a small relative error. Claim 2.2 of the paper (p. 34:16) quantifies this: the two periodic normal distributions are close in statistical distance, linearly in the relative change $\beta/\alpha - 1$. This mission formalizes Claim 2.2 and the steps of its proof. The source is the published J. ACM article; the paper's main theorem, a quantum reduction from worst-case lattice problems to LWE, is outside this series.

Setting

Identify $\mathbb{T} = \mathbb{R}/\mathbb{Z}$ with the segment $[0,1)$ with addition modulo $1$. For $\beta > 0$ the normal density with mean $0$ and standard deviation $\beta/\sqrt{2\pi}$ is

$$\nu_\beta(x) = \frac{1}{\beta}\exp\Bigl(-\pi\Bigl(\frac{x}{\beta}\Bigr)^2\Bigr), \qquad x \in \mathbb{R},$$

(Eq. (5) in dimension one), and the periodic normal density (Eq. (7)) is its periodization

$$\Psi_\beta(r) = \sum_{k=-\infty}^{\infty} \frac{1}{\beta}\exp\Bigl(-\pi\Bigl(\frac{r-k}{\beta}\Bigr)^2\Bigr), \qquad r \in [0,1),$$

the density of a $\nu_\beta$-distributed variable reduced modulo $1$.

The statistical distance of two densities $\varphi_1, \varphi_2$ (p. 34:14) is

$$\Delta(\varphi_1, \varphi_2) = \int |\varphi_1 - \varphi_2|,$$

the integral taken over $\mathbb{R}$ for densities on the line and over $[0,1)$ for densities on $\mathbb{T}$. The paper uses this normalization without a factor $\tfrac12$, so that $\Delta$ ranges in $[0,2]$ on probability densities. In Lean these objects are RegevLWE.PeriodicGauss.nu, Psi, statDist and statDistT.

Formalization targets

Goal: Claim 2.2

For any $0 < \alpha < \beta \le 2\alpha$,

$$\Delta(\Psi_\alpha, \Psi_\beta) \le 9\Bigl(\frac{\beta}{\alpha} - 1\Bigr).$$

The hypotheses and the constant $9$ are exactly as printed.

Milestones

1. The bound on the line (proof of Claim 2.2, first sentence). For $0 < \alpha < \beta \le 2\alpha$,

$$\Delta(\nu_\alpha, \nu_\beta) \le 9\Bigl(\frac{\beta}{\alpha} - 1\Bigr).$$

2. Reduction modulo 1 does not increase $\Delta$ (p. 34:15, used on p. 34:16): for integrable $\varphi_1, \varphi_2$ on $\mathbb{R}$, the periodizations $\tilde\varphi_i(r) = \sum_k \varphi_i(r-k)$ satisfy $\Delta(\tilde\varphi_1, \tilde\varphi_2) \le \Delta(\varphi_1, \varphi_2)$.
3. The three displayed steps of the proof after normalizing to $\alpha = 1$, $\beta = 1 + \epsilon$, $0 < \epsilon \le 1$: the first display (a triangle-inequality split and an exact evaluation), the pointwise bound

$$\bigl|e^{-\pi(1-1/(1+\epsilon)^2)x^2} - 1\bigr| \le \pi\bigl(1 - 1/(1+\epsilon)^2\bigr)x^2 \le 2\pi\epsilon x^2,$$

and the final evaluation

$$\epsilon + 2\pi\epsilon\int_{\mathbb{R}} x^2 e^{-\pi x^2/(1+\epsilon)^2}\,dx = \epsilon + \epsilon(1+\epsilon)^3 \le 9\epsilon.$$

Significance

Claim 2.2 is a stability statement for the LWE error distribution. It lets an algorithm that works for one noise parameter be applied to a nearby one at a controlled cost in statistical distance, which is how Regev's reductions tolerate an approximately known parameter. It also states a quantitative fact about wrapped normal distributions, which appear outside cryptography, for example in directional statistics.

The result is proved in the paper; no machine-checked proof is known to this mission. Formalizing it produces a reusable one-dimensional toolkit: the $L^1$ distance between two centred normal densities, the second moment of a Gaussian in Regev's normalization, and the contraction of $L^1$ distance under periodization. Each of these is a building block for formalizing the rest of the paper's analysis of Gaussian noise.

Difficulty

The arithmetic is elementary; the work is in the analysis. The statement on $\mathbb{T}$ involves infinite series inside an integral, and the passage from the line to the circle requires exchanging a sum over $\mathbb{Z}$ with an integral and controlling the series almost everywhere. A direct attack on $\Psi_\alpha - \Psi_\beta$ termwise on $[0,1)$ does not by itself produce a bound in terms of $\beta/\alpha - 1$; the comparison has to be made on the line first. On the line, the scaling to $\alpha = 1$ is a change of variables in a Lebesgue integral, and the evaluation of $\int x^2 e^{-\pi x^2/\sigma^2}dx = \sigma^3/(2\pi)$ requires Gaussian moment identities in the paper's normalization rather than Mathlib's.

Formalization scope

• Reals and densities. Everything is one-dimensional over $\mathbb{R}$; distributions are represented by their densities, not by measures. $\mathbb{T}$ is the interval Set.Ico 0 1 with Lebesgue measure; $\Psi_\beta$ is a real tsum over $k \in \mathbb{Z}$, which converges absolutely for $\beta \ne 0$.
• Statistical distance. $\Delta$ is a lower Lebesgue integral ∫⁻ ENNReal.ofReal |φ₁ - φ₂| valued in $[0,\infty]$, with no factor $\tfrac12$, as on p. 34:14. Bounds are compared through ENNReal.ofReal. A Bochner integral would be $0$ on a non-integrable difference and would make any upper bound trivially true; the extended-valued integral rules this out.
• Added hypotheses. None on the goal or on the line bound. The modulo-1 milestone assumes $\varphi_1, \varphi_2$ integrable (the paper states the data-processing fact for random variables, whose densities are integrable); only the "modulo 1" instance used in the proof is stated, not the general inequality for arbitrary randomized functions. The pointwise bound is stated for every $\epsilon \ge 0$, a harmless generalization of the proof's range $0 < \epsilon \le 1$. The first display is stated as its three component facts (inequality, evaluation $= \epsilon$, and the rewriting of the integrand), which together give the printed chain.
• No trivialization. The goal is Claim 2.2 on $\mathbb{T}$, not the bound on the line, and neither side can collapse to a junk value: the left side is an extended nonnegative integral and the right side is positive under the hypotheses.
• Welcome contributions. Gaussian moment lemmas in the normalization $e^{-\pi x^2/s^2}$, the periodization contraction for general integrable functions, and a measure-level statement identifying $\Psi_\beta$ with the pushforward of $\nu_\beta$ under reduction modulo $1$.

Selected references

• O. Regev, On Lattices, Learning with Errors, Random Linear Codes, and Cryptography, Journal of the ACM 56(6), Article 34, 2009. https://doi.org/10.1145/1568318.1568324
• D. Micciancio and S. Goldwasser, Complexity of Lattice Problems: A Cryptographic Perspective, Kluwer, 2002 (cited on p. 34:15 for the data-processing property of statistical distance). https://doi.org/10.1007/978-1-4615-0897-7

Motivation

Many operators of harmonic analysis are bounded on $L^2$ by an orthogonality argument but fail to be bounded on $L^1$; what survives at $p=1$ is a weak-type estimate $\lambda\,P(|Tf|>\lambda)\le c\,\|f\|_1$. For singular integrals the standard route to such an estimate is the Calderón–Zygmund decomposition, which splits a function at height $\lambda$ into a bounded part and a part supported on a small set. Martingale theory has the same need: square functions, martingale transforms and maximal operators of martingales are bounded on $L^2$ for orthogonality reasons, and their behaviour on $L^1$-bounded martingales is the delicate endpoint.

R. F. Gundy (1968) supplied the martingale analogue: an $L^1$-bounded martingale can be written as the sum of three martingales, one bounded in $L^2$, one whose differences are absolutely summable in $L^1$, and one that is non-zero only on an event of small probability (Gundy 1968). Gundy's construction used several stopping times. In his 1971 Wald Memorial Lectures, published as Distribution Function Inequalities for Martingales (Burkholder 1973), D. L. Burkholder gave a simplified version of the decomposition in which only one stopping time is used, with explicit constants $2$, $4$ and $1$. This mission formalizes that version, Theorem 4.1 of the lectures, together with the facts its proof rests on.

Timeline:

• 1953. J. L. Doob's Stochastic Processes establishes almost-everywhere convergence of $L^1$-bounded martingales and the maximal inequality.
• 1966. D. G. Austin proves that the integral of $S^2(f)$ over $\{f^*\le\lambda\}$ is finite for an $L^1$-bounded martingale (Austin 1966).
• 1968. Gundy proves the decomposition theorem for $L^1$-bounded martingales, with applications to weak-type estimates.
• 1973. Burkholder's Lemma 2.1, a refinement of Austin's theorem, yields a one-stopping-time proof of Gundy's decomposition with explicit constants.

Setting

Let $(\Omega,\mathcal A,P)$ be a probability space and $\mathcal A_0\subseteq\mathcal A_1\subseteq\cdots$ a nondecreasing sequence of sub-$\sigma$-fields of $\mathcal A$. A martingale relative to $\mathcal A_1,\mathcal A_2,\dots$ is a sequence $f=(f_1,f_2,\dots)$ of integrable random variables with $f_n$ $\mathcal A_n$-measurable and $E(f_{n+1}\mid\mathcal A_n)=f_n$. Its difference sequence is $d=(d_1,d_2,\dots)$ with $f_n=\sum_{k=1}^n d_k$, i.e. $d_1=f_1$, $d_k=f_k-f_{k-1}$ (the convention is $f_0=0$).

The maximal function is $f^*=\sup_{n\ge1}|f_n|$, the square function is $S(f)=\big[\sum_{k\ge1}d_k^2\big]^{1/2}$, and $S_n(f)$ is its $n$-th partial version. For $0<p<\infty$,

$$\|f\|_p=\sup_{n\ge1}\|f_n\|_p,\qquad \|f_n\|_p=(E|f_n|^p)^{1/p},$$

and $f$ is $L^p$-bounded when $\|f\|_p<\infty$. For $\lambda>0$, the exit time $\mu=\inf\{n\ge1:|f_n|>\lambda\}$ (with $\inf\emptyset=\infty$) is the first index at which $|f_n|$ exceeds $\lambda$; $f_\mu$, $f_{\mu-1}$, $S_{\mu-1}(f)$ denote evaluation at the random index, with $f_\infty=\lim_n f_n$.

The Lean development names these objects dseq ($d$), sqFnN/sqFn ($S_n(f)$, $S(f)$), maxFnN/maxFn ($f_n^*$, $f^*$), pNorm ($\|f\|_p$), exitTime ($\mu$) and valAt/sqFnAt (evaluation at an index in $\{0,1,\dots,\infty\}$), all in the namespace BurkholderDFI.Gundy.

Formalization targets

Goal: Theorem 4.1 (p. 23)

For every $L^1$-bounded martingale $f$ and every $\lambda>0$ there are martingales $X,Y,Z$ relative to the same $\sigma$-fields, with difference sequences $x,y,z$, such that

$$f=X+Y+Z,\qquad \|X\|_2^2\le2\lambda\|f\|_1,\qquad \Big\|\sum_{k=1}^\infty|y_k|\Big\|_1\le4\|f\|_1,\qquad P(Z^*>0)\le\|f\|_1/\lambda.$$

The three bounds hold together; each alone is trivial ($f=0+0+f$ satisfies the first two, $f=0+f+0$ the first and last).

Milestones

1. Doob's facts (cited, §1, p. 20). An $L^1$-bounded martingale or nonnegative submartingale converges almost everywhere, and $\|f_\mu\|_1\le\|f\|_1$ for every stopping time $\mu$.
2. (1.5) (p. 20). $\lambda^pP(f^*>\lambda)\le\|f\|_p^p$ for $1\le p<\infty$.
3. Lemma 2.1 (p. 21). For the exit time $\mu$ above $\lambda$,

$$\|S_{\mu-1}(f)\|_2^2+\|f_{\mu-1}\|_2^2\le2Ef_\mu f_{\mu-1}\le2\lambda\|f\|_1,$$

with equality on the left for martingales.

Significance

The result. The decomposition is the standard device for passing from $L^2$ to weak-type $(1,1)$ estimates for martingale operators: an operator that is bounded on $L^2$, controlled by total variation on the second piece, and local in the sense that it vanishes where the third piece vanishes, is of weak type $(1,1)$. Applications of the decomposition are given in Gundy's papers of 1968 and 1969 (On the class $L\log L$, martingales, and singular integrals, Studia Math. 33), which the lectures cite for this purpose. The explicit constants $2$, $4$, $1$ make every such weak-type constant explicit.

Formalizing it. The theorem is classical and proved; the remaining work is its formalization. As far as is known, no machine-checked proof of Gundy's decomposition, of Lemma 2.1, or of the weak-type maximal inequality in the form (1.5) for real martingales exists in Mathlib or on this platform. Mathlib provides almost-everywhere convergence of $L^1$-bounded submartingales and Doob's maximal inequality for nonnegative submartingales; the stopped-value bound for unbounded stopping times, the square-function identity of Lemma 2.1 and the decomposition itself are new. The milestones are shared with other missions of this series (Lemma 2.1 is also used for Burkholder's weak-type square function inequality and his exponential estimates), so each proof is reused.

Difficulty

The obvious attempt imitates the Calderón–Zygmund cut directly: truncate $f$ at height $\lambda$, or stop it when it first exceeds $\lambda$. Neither produces the required pieces. Truncation destroys the martingale property, and whatever restores it adds terms that must themselves be controlled in the right norm. Stopping at the exit time produces a martingale bounded by $\lambda$ only up to the overshoot at the exit, which is not bounded and lives on an event that is small only in probability. The $L^2$ estimate (4.2) is therefore not a consequence of boundedness; it needs a quantitative square-function bound for the martingale up to the exit, which is the content of Lemma 2.1, and that lemma in turn needs the limit $f_\infty$ and the stopped values $f_\mu$ on $\{\mu=\infty\}$ — so Doob's convergence theorem cannot be avoided.

Formalization scope

Processes are functions f : ℕ → Ω → ℝ with a Mathlib Filtration ℕ and Mathlib's Martingale/Submartingale. The paper indexes from $1$; Lean's index $0$ is never read by any quantity in the statements, which use the paper's convention $f_0=0$. Mathlib's martingale definition additionally constrains $f_0=E(f_1\mid\mathcal A_0)$; this is no restriction, since every martingale indexed from $1$ extends this way. The goal asserts that $X,Y,Z$ are Mathlib martingales for the same filtration as $f$, and the identity $f_n=X_n+Y_n+Z_n$ is required for $n\ge1$.

Further committed conventions:

• $S(f)$, $f^*$, $Z^*$, $\|\cdot\|_p$ and all expectations of nonnegative quantities take values in $[0,\infty]$ (lower Lebesgue integral), so no infinite value is silently replaced by $0$.
• $\|X\|_2=\sup_{n\ge1}\|X_n\|_2$, not the norm of a limit; $Z^*=\sup_{n\ge1}|Z_n|$; $\|\sum_k|y_k|\|_1$ is the integral of the series with $y_1=Y_1$.
• The exit time takes values in $\mathbb N\cup\{\infty\}$ and $\mu-1$ is truncated, with $\infty-1=\infty$; the a.e. limit $f_\infty$ is a function supplied with its convergence hypothesis (Lemma 2.1) or asserted to exist (Doob's facts).
• "Nonnegative submartingale" means $f_n\ge0$ almost surely for $n\ge1$.
• $\Omega$ is an arbitrary measurable space with a probability measure.

A formalization in which the existential could choose its own filtration, or in which the norms were Bochner integrals (which vanish on non-integrable functions), would trivialize the goal; both are excluded by the statement above.

Infrastructure needed: stopped values at unbounded stopping times and their $L^1$ bound; square-function identities for stopped martingales (orthogonality of martingale differences up to a stopping time); conditional-expectation compensators of predictable truncations. The definitions file is shared with the other eight missions of this series and is reusable for any work on discrete-time square and maximal functions. Proofs of the milestones, alternative arguments, and sharper constants are all welcome.

Selected references

• D. L. Burkholder, Distribution function inequalities for martingales, The Annals of Probability 1(1), 19–42, 1973. https://doi.org/10.1214/aop/1176997023
• R. F. Gundy, A decomposition for L¹-bounded martingales, The Annals of Mathematical Statistics 39(1), 134–138, 1968. https://doi.org/10.1214/aoms/1177698510
• D. G. Austin, A sample function property of martingales, The Annals of Mathematical Statistics 37(5), 1396–1397, 1966. https://doi.org/10.1214/aoms/1177699283
• J. L. Doob, Stochastic Processes, Wiley, New York, 1953.

Motivation

Inventory calculations often take the selling price as fixed, while price calculations often treat the cost of supplying demand as independent of the order policy. Whitin's 1955 model connects the two decisions in one annual-profit calculation. A merchant chooses both the price charged to customers and the size of each replenishment order. Changing the price changes annual demand; changing demand changes the number of orders, inventory carrying cost, and therefore the economic lot size. This makes the selling price and the inventory decision parts of the same optimization problem. Whitin's paper gives a compact example in which the connection can be written down explicitly.

The mission concentrates on Section 2, the stationary-demand model for a stable item. Section 3 of the paper studies style goods under uncertain sales and belongs to a separate mission. The result here concerns a deterministic annual demand curve and continuous order quantities, so a solver can focus on the interaction between a classical economic order quantity calculation and a price first-order condition.

Setting

The price is a real number $p$. Annual demand is the linear function $D(p)=ap+b$, where $a$ and $b$ are given real constants. A feasible price has $D(p)>0$. The paper does not require $a<0$ in its displayed model, so the formal statements leave the slope unrestricted. Negative $a$ is the economically usual decreasing-demand case; in other regimes a joint maximum may simply fail to exist.

The merchant pays a fixed setup cost $S$ whenever an order is placed. The purchase cost per unit is $C$, and the annual carrying charge for one unit kept in stock is $IC$, where $I$ is a carrying-rate factor. If $Q>0$ units are ordered each time, average stock is $Q/2$ and the annual number of orders is $D/Q$. A per-unit operating cost $k$ is incurred on annual demand, and $f$ is an annual fixed cost. The resulting total variable cost and two-variable annual profit are

$$\operatorname{TVC}(D,Q)=\frac Q2 IC+\frac DQ S+kD, \qquad \Pi(p,Q)=D(p)p-\operatorname{TVC}(D(p),Q)-f.$$

Only pairs with $D(p)>0$ and $Q>0$ are feasible. For a fixed demand level, the economic lot size is $Q^*(D)=\sqrt{2DS/(IC)}$. Substituting it into profit gives Whitin's reduced profit

$$P(p)=ap^2+bp-\sqrt{2SIC(ap+b)}-k(ap+b)-f.$$

The paper uses $P$ for annual profit in this section. The Lean development calls the two-variable function profit and the function after optimizing $Q$ reducedProfit.

Formalization targets

The first target is the unique lot-size minimum in Eq. (3), followed by its value in Eq. (4):

$$\operatorname{TVC}(D,Q^*(D))\leq\operatorname{TVC}(D,Q) \quad(Q>0),\qquad \operatorname{TVC}(D,Q^*(D))=\sqrt{2DSIC}+kD.$$

Equality in the inequality holds only at $Q=Q^*(D)$. The next target is the necessary stationarity condition in Eqs. (6)–(7): when $D(p)>0$ and the derivative of $P$ at $p$ is zero,

$$8a^3p^3+(16a^2b-8ka^3)p^2 +(10ab^2-12ka^2b+2k^2a^3)p +2b^3-4kab^2+2k^2a^2b-SICa^2=0.$$

The goal joins these steps at a global joint maximum. If a feasible pair $(p,Q)$ maximizes $\Pi$ over all feasible price and lot-size pairs, then $Q=Q^*(D(p))$ and $p$ satisfies the cubic. The goal is an implication about any joint maximizer; it does not assert that one exists for every demand curve. The cubic is a necessary condition only. Its algebraic roots may include prices that fail the original first-order equation or fail to maximize profit.

Significance

The result gives a concrete relation between a price chosen to maximize annual profit and the ordering cost and carrying charge of the inventory system. The lot-size formula alone optimizes cost at a fixed demand rate. The cubic makes the demand response to price and the resulting inventory cost visible in the price condition. It also specifies what can be inferred from the calculation: an optimal price must satisfy the equation, while selecting an optimum from candidate roots remains a separate question.

The paper already supplies the mathematical result. The formalization task is to represent the joint optimization and verify its necessary conditions in Lean, together with the cost identity on which the reduced-profit expression rests. The published Prove2Me definition InventoryControl_eoq already provides the classical EOQ cost and square-root quantity; this mission uses its cost function and adds Whitin's demand curve and profit. Related inventory results for backorders and multilevel systems describe different models and do not replace the targets here.

Difficulty

At a fixed price, choosing the lot size involves both a term proportional to $Q$ and one proportional to $1/Q$. The optimality statement needs a global inequality and a unique equality case, not merely the observation that a derivative vanishes. After substituting that quantity, the reduced profit contains a square root of the demand curve. Its derivative is meaningful on positive demand, and turning its stationarity equation into the displayed cubic loses information when an equation is squared. A proof therefore has to preserve the implication from optimality to the cubic without promoting all cubic roots to optima.

Formalization scope

The model uses real prices, real demands, and real lot sizes; it does not round order quantities to integers. The hypotheses $S,I,C>0$ make explicit the positive cost and carrying-charge conventions of Section 2. Neither $k$ nor $f$ is assigned a sign, and no sign is imposed on $a$ or $b$. The conditions $Q>0$ and $D(p)>0$ apply to every cost or profit comparison. They exclude Lean's total value for division by zero and the zero value assigned by Real.sqrt to a negative argument. The goal quantifies over every feasible pair in a joint maximum of the original profit, so optimizing $Q$ is part of its content. Defining profit only by the reduced formula would erase that claim.

The definitions comprise linear demand, total variable cost, two-variable profit, and reduced profit. The classical EOQ cost comes from the existing InventoryControl_eoq definition; the model-specific layer is small and can be reused in further work on pricing with inventory costs. The theorem targets welcome proofs of the global lot-size inequality, the minimized-cost identity, the stationary cubic, and their combination at a joint maximizer. The paper's quantity-discount footnote is outside this scope because it leaves the revised purchase and carrying-cost model unspecified.

Selected references

• T. M. Whitin, Inventory Control and Price Theory, Management Science 2(1), 1955, pp. 61–68. DOI: 10.1287/mnsc.2.1.61.

Motivation

Weighted voting bodies often combine a few large blocs with a mass of small, unorganized voters: shareholders' meetings with a handful of large holders and a dispersed float, legislatures with party blocs and independents. The Shapley value measures each participant's voting power as the probability of being pivotal — the one whose arrival first turns a losing coalition into a winning one — when participants arrive in a uniformly random order. For many small voters this computation becomes a combinatorial problem whose size grows with the number of voters.

Milnor and Shapley (RAND RM-2649, 1961; revised as Mathematics of Operations Research 3(4), 1978) replaced the small voters by a continuum, the ocean, and obtained explicit formulas for the power of the large voters. The memorandum is the second of a RAND series on values of large games; the first (L. S. Shapley and N. Z. Shapiro, Values of Large Games, I: A Limit Theorem, RM-2648, 1960) proves the limit theorem for finite games with many small players on which the oceanic model rests. This mission formalizes the part of the memorandum that leads to explicit closed forms for the values of interior oceanic games (§2, §4, §5).

Setting

There are $m$ major players $M = \{1, \dots, m\}$ with weights $w_1, \dots, w_m \ge 0$, and $w(S) = \sum_{j \in S} w_j$. The ocean is the interval $I = [0,1]$ with Lebesgue measure, carrying total weight $\alpha > 0$. In the oceanic game $[c; w_1, \dots, w_m; \alpha]$ with quota $c$, a coalition wins when the weight of its major players plus $\alpha$ times its share of the ocean is at least $c$.

The random order is modelled by a uniform random point $x = (x_1, \dots, x_m)$ of the cube $I^m$: major player $j$ is inserted into the ocean at position $x_j$, and $P(t) = \{ j : x_j < t \}$ is the set of major players placed before position $t$. Player $i$ is pivotal when

$$w(P(x_i)) + \alpha x_i \le c \le w(P(x_i)) + w_i + \alpha x_i, \qquad (2.4)$$

and the value $\varphi_i$ of player $i$ is the probability of (2.4), i.e. the volume of the set $A_i \subseteq I^m$ where it holds. The combined value of the ocean is $\Phi = 1 - \sum_{i} \varphi_i$ (2.5).

With the quota $y$ as a variable, $\Gamma(y) = [y; w_1, \dots, w_m; \alpha]$ has values $\varphi_i(y)$, $\Phi(y)$, and the pivot location $F(y) = \inf\{t \ge 0 : w(P(t)) + \alpha t \ge y\}$ is a random, nondecreasing, piecewise linear function of $y$ with expectation $E\{F(y)\}$. Adding a major player $m+1$ of weight $w_{m+1}$ gives the game $\Gamma^+$.

The game is interior when

$$w(M) \le c \le \alpha,$$

that is, the ocean alone wins and the major players together lose. With $\bar w_j = \alpha - w_j$, define $\pi(S) = \prod_{j \in S} \tfrac{w_j}{\alpha} \prod_{j \in M - S} \tfrac{\bar w_j}{\alpha}$ for $S \subseteq M$, the analogous product $\pi_i(S)$ over $M - \{i\}$ for $S \subseteq M - \{i\}$, and the integers $a_0 = 1$, $a_n = 1 - n a_{n-1}$, i.e. $1, 0, 1, -2, 9, -44, \dots$

Formalization targets

Goal: Theorem 6 (p. 20)

In an interior game, with $s = |S|$,

$$\varphi_i = \frac{w_i}{\alpha} \sum_{S \subseteq M - \{i\}} a_s \, \pi_i(S), \qquad \Phi = \sum_{S \subseteq M} a_s \, \pi(S).$$

Both identities are part of the goal. The values do not depend on $c$ within the interior range.

Milestones

1. §2, p. 5: the pivot sets $A_1, \dots, A_m$ overlap only in measure zero.
2. (4.3): $\varphi_i(y) = \operatorname{Prob}\{F(y) = x_i\}$ for $0 \le y \le w(M) + \alpha$.
3. (4.4)–(4.5): for $0 < y < w(M) + \alpha$, $F$ is differentiable at $y$ almost surely, $\sum_i \varphi_i(y) = \operatorname{Prob}\{F'(y) = 0\}$ and $\Phi(y) = \operatorname{Prob}\{F'(y) = 1/\alpha\}$.
4. Theorem 2, (4.7): $\Phi(y) = \alpha \, \frac{d}{dy} E\{F(y)\}$.
5. Lemma, (4.12)–(4.13): $\varphi^+_{m+1}(z) = \frac{1}{\alpha} \int_{t_1}^{t_2} \Phi(y)\, dy$ with $t_1 = \max(z - w_{m+1}, 0)$, $t_2 = \min(z, w(M) + \alpha)$.
6. Theorem 5, (5.4): if $[c; w_1, \dots, w_m; \alpha]$ and $[d; w_1, \dots, w_{m+1}; \alpha]$ are both interior, $\varphi^+_{m+1} = \frac{1}{\alpha} \Phi w_{m+1}$.
7. Proof of Theorem 6, p. 21: the right-hand sides above add up to 1, an identity valid for all real $w_j$ and $\alpha \ne 0$.

Further items, not milestones: the Corollary (5.5), Theorem 3 (averaged over all quotas, each value equals the player's share of the total weight), Theorem 4 (small players behave like ocean), and (5.8) with its footnote ($|a_n|$ is the nearest integer to $n!/e$ and counts derangements).

Significance

Theorem 6 turns the voting power of the large blocs, a priori a probability over a continuum of orderings, into a finite multilinear polynomial in the ratios $w_j/\alpha$. Table 1 of the memorandum lists the cases $m \le 3$, and the theorem gives every $m$. Its coefficients are signed derangement numbers. The Corollary (5.5) states that a major player's value per vote equals the ocean's value per vote in the game without that player.

The memorandum's arguments are short and partly heuristic: "E commutes with the derivative", the disjointness of the pivot sets is "obvious", and the induction for Theorem 6 relies on the symmetry of the value in the major players, which is never stated. A formalization makes each of these steps precise, including the measure-zero exceptions and the quota ranges. To our knowledge none of these results has a machine-checked proof; Mathlib has the Lebesgue measure on cubes, interval integrals and derangement numbers, but no game-theoretic value with a continuum of players.

Difficulty

The values are volumes of regions of $I^m$ cut out by inequalities whose shape depends on the order of the coordinates, so a direct computation splits into $m!$ order cells, with the quota $c$ entering each. The paper's route avoids this by passing through the random function $F$, Theorem 2 and the Lemma; that route needs differentiation under the integral sign for a function that is only piecewise linear in $y$, with kinks at random locations, and an exact bookkeeping of the interval of integration when the quota approaches the ends of $[0, w(M) + \alpha]$. Theorem 6 is then an induction on $m$ that uses Theorem 5 for every player in turn, so it also needs the invariance of $\varphi_i$ under a relabelling of the major players.

Formalization scope

• Major players are Fin m ($m = 0$ is allowed; then $\Phi = 1$). The probability of an event is the Lebesgue volume of its intersection with $[0,1]^m$; no probability space is built.
• $P(t)$ uses the strict inequality $x_j < t$, as printed.
• $\varphi_i$ is defined as the volume of the pivot set (2.4), for every real quota. $\Phi$ is defined by (2.5), as the paper allows ("We might equally well take (2.5) as the definition of $\Phi$"). Neither is defined through the formulas of Theorem 6 or through $F$; defining them that way would make the goal an unfolding, and is ruled out.
• The paper writes (4.2) as a minimum $F(y) = \min\{x \mid w(P(x)) + \alpha x \ge y\}$, which need not be attained; $F$ is the infimum over $t \ge 0$, the value shown in its Fig. 3.
• The standing assumptions $w_j \ge 0$ and $\alpha > 0$ (§2) are explicit hypotheses. The p. 5 footnote's $0 \le c \le w(M)+\alpha$ applies to the pivot-set milestone. Other quota ranges are explicit: $0 \le y \le w(M) + \alpha$ for (4.3) and Theorem 2 (one-sided derivatives at the ends), the open interval for (4.4)–(4.5) (two-sided derivatives, stated with HasDerivAt), and $0 \le z \le w(M) + w_{m+1} + \alpha$ for the Lemma, as on p. 14.
• The added player is appended with Fin.snoc as index Fin.last m.
• Corollary (5.5) assumes $w_i > 0$, since it divides by $w_i$. Theorem 4, stated in the paper "in the general oceanic game", is false at quota $0$ and when the limit game has no winning coalition; it is stated for $0 < c \le w(M - \{i\}) + \alpha$.
• The identity of milestone 7 is pure algebra and is stated for all real weights and $\alpha \ne 0$.

A complete development needs: measurability of the pivot sets and of $F$ in $x$, the structure of $F$ as a piecewise linear function of $y$, differentiation of $E\{F\}$, and invariance of the values under permutations of the major players. The pivot-set and $F$ infrastructure is reusable for the companion mission on limits of finite weighted majority games. Contributions of any of the milestones, of the symmetry lemma, and of the non-milestone items are welcome.

Selected references

• J. W. Milnor and L. S. Shapley, Values of Large Games, II: Oceanic Games, The RAND Corporation, Research Memorandum RM-2649, February 1961. https://www.rand.org/pubs/research_memoranda/RM2649.html
• J. W. Milnor and L. S. Shapley, Values of Large Games II: Oceanic Games, Mathematics of Operations Research 3(4):290–307, 1978. https://doi.org/10.1287/moor.3.4.290
• L. S. Shapley, A Value for n-Person Games, in Contributions to the Theory of Games II, Annals of Mathematics Studies 28, Princeton University Press, 1953, 307–317. https://doi.org/10.1515/9781400881970-018
• L. S. Shapley and N. Z. Shapiro, Values of Large Games, I: A Limit Theorem, The RAND Corporation, Research Memorandum RM-2648, November 1960.
• R. J. Aumann and L. S. Shapley, Values of Non-Atomic Games, Princeton University Press, 1974. https://doi.org/10.1515/9781400867080

Motivation

Dynamic traffic assignment models how commuters choose routes and departure times when travel times change over the day. In the model of Friesz, Bernstein, Smith, Tobin and Wie (Oper. Res. 41 (1993)), the time to traverse a path is built recursively from arc exit-time functions: a vehicle that enters an arc at time $t$ leaves it at time $\tau(t)$. The equilibrium conditions of that model refer to the inverses of these functions, so the model is only well defined when every arc exit-time function is invertible.

Invertibility has a direct traffic meaning. A strictly increasing exit time is the first-in-first-out (FIFO) property: a vehicle that enters later cannot leave earlier, so no overtaking occurs on the arc. Whether a given delay model respects FIFO was an active question in the early 1990s, because several delay functions used in practice violate it for some inflow patterns.

Timeline:

• 1969. Vickrey's bottleneck model introduces deterministic queueing at a single bottleneck (Vickrey 1969).
• 1986. Ben-Akiva and De Palma show (Trans. Sci. 20 (1986)), for uniform entry rates and deterministic queueing delays, that it is not possible to "arrive earlier by departing later".
• 1993. Friesz et al. prove (Theorem 1, p. 185) that for every linear arc delay $D = \alpha x + \beta$ the exit time is strictly increasing, extending the 1986 result to all continuous entry-rate patterns (remark, p. 186).

Setting

Consider one arc. Vehicles enter it at the entry rate $u(t) \ge 0$, a continuous function of time $t \ge 0$; the first vehicle enters at time $0$. For an exit-time function $\tau$, the arc volume at time $t \ge 0$ is the inflow mass of the vehicles that entered during $[0,t]$ and have not left by time $t$:

$$x(t) = \int_{\{s \in [0,t]\,:\,\tau(s) > t\}} u(s)\,ds .$$

The linear delay function (18) of the paper is

$$D(t) = \alpha\, x(t) + \beta, \qquad \alpha, \beta > 0,$$

a fixed free-flow travel time $\beta$ plus a queueing time determined by the service rate $1/\alpha$. The exit time is entry time plus delay, so $\tau$ is pinned by the exit-time equation

$$\tau(t) = t + \alpha\, x(t) + \beta \qquad (t \ge 0).$$

The equation is implicit: $\tau$ appears on the right through the volume. The proof partitions time at $t_0 = 0$, $t_{n+1} = \tau(t_n)$; in particular $t_1 = \tau(0) = \beta$ is the exit time of the first vehicle. In Lean these objects are linearDelay, arcVolume, IsLinearExitTime and tSeq in FrieszDUE.FIFO.

Formalization targets

Goal: Theorem 1 (p. 185)

For $\alpha, \beta > 0$ and a nonnegative continuous entry rate $u$, every $\tau$ satisfying the exit-time equation is strictly increasing on $[0, \infty)$:

$$0 \le s < t \implies \tau(s) < \tau(t),$$

and hence injective there, so $\tau^{-1}$ exists.

Milestones

1. Lemma 1 (19): for a differentiable invertible $f$, $[f^{-1}]'(z) = 1/f'[f^{-1}(z)]$.
2. First interval (21)–(24): $t_1 = \beta$; on $[0, t_1]$, $x(t) = \int_0^t u$, $\tau(t) = t + \alpha\int_0^t u + \beta$, and $\tau' = 1 + \alpha u > 0$.
3. Second interval (25)–(28): on $[t_1, t_2]$, $\tau(t) = t + \alpha\int_{\tau^{-1}(t)}^t u + \beta$ and $\tau'(t) = \alpha u(t) + 1/(1 + \alpha u[\tau^{-1}(t)]) > \alpha u(t)$.
4. Induction (29)–(34): the same representation and $\tau'(t) > \alpha u(t)$ on every $[t_{n+1}, t_{n+2}]$, with $\tau$ strictly increasing there.
5. Covering: $t_{n+1} - t_n \ge \beta$ and $\mathbb R_+ = \bigcup_{n \ge 0}[t_n, t_{n+1}]$.

A supporting, non-milestone item states that the exit-time equation has a solution for every admissible $u$.

Significance

The result makes the path exit-time functions of the dynamic network model invertible whenever the arc delays are linear in volume. That invertibility is what allows the path costs, and through them the variational inequality of Theorem 2 of the same paper, to be written down. In traffic terms it certifies that linear volume-based delays never let a later entrant overtake an earlier one, whatever the continuous inflow profile.

The theorem is proved in the paper. As far as is known it has no machine-checked proof. The mission produces one, together with a formal model of a single arc whose exit time is defined implicitly through the volume, which is reusable for other delay functions and for FIFO questions in dynamic traffic assignment.

Difficulty

The obvious argument differentiates $\tau(t) = t + \alpha x(t) + \beta$ and bounds the outflow rate. But the volume can only be written as $\int_{\tau^{-1}(t)}^t u$ once $\tau$ is known to be invertible, which is the conclusion. The paper breaks the circularity by working forward in time: on $[t_n, t_{n+1}]$ the volume depends only on $\tau$ restricted to the earlier interval, whose invertibility is already established. A formal proof must make this forward dependence rigorous for an exit time given only by the implicit equation, handle one-sided derivatives at the junctions $t_n$, where $\tau$ is generally not differentiable, and show that the junctions do not accumulate.

Formalization scope

Time is real; the entry rate is a function $u : \mathbb R \to \mathbb R$ with $u(t) \ge 0$ and $u$ continuous on $[0, \infty)$. Both are added hypotheses: Theorem 1 names none, nonnegativity is implicit in "entry rate", and the remark after the proof covers "all continuous entry rate patterns". Integrals are Lebesgue integrals. Monotonicity is claimed on $[0,\infty)$ only, the entry times that the equation constrains. Derivative claims in the milestones are taken within the closed interval $[t_n, t_{n+1}]$. The paper's separate pieces $\tau_k$ are one global function here, so the junction identities (27), (30), (33) are automatic. Lemma 1 adds the hypothesis $f'[f^{-1}(z)] \ne 0$, without which it is false.

The exit time τ is pinned by the implicit equation τ(t) = t + αx(t) + β, where x(t) is the inflow mass of vehicles that entered by time t and have not exited by time t; no monotonicity or invertibility of τ is assumed. A formalization that defined the volume through $\tau^{-1}$ or assumed $\tau$ monotone would assume the conclusion and is ruled out.

The development needs one-sided derivatives of parametric integrals, the inverse-function derivative on an interval, and a forward induction over the partition. Contributions of proofs for any milestone, of the existence item, and of a uniqueness result for the exit-time equation are welcome.

Selected references

• T. L. Friesz, D. Bernstein, T. E. Smith, R. L. Tobin and B. W. Wie, A variational inequality formulation of the dynamic network user equilibrium problem, Operations Research 41(1):179–191, 1993. https://doi.org/10.1287/opre.41.1.179
• M. Ben-Akiva and A. de Palma, Some circumstances in which vehicles will reach their destinations earlier by starting later: revisited, Transportation Science 20(1):52–55, 1986. https://doi.org/10.1287/trsc.20.1.52
• M. Ben-Akiva, A. de Palma and P. Kanaroglou, Dynamic model of peak period traffic congestion with elastic arrival rates, Transportation Science 20(3):164–181, 1986. https://doi.org/10.1287/trsc.20.3.164
• W. S. Vickrey, Congestion theory and transport investment, American Economic Review 59(2):251–261, 1969. https://www.jstor.org/stable/1823678

Why delays in boundary feedback matter

Boundary feedback is the standard way to stabilize vibrating structures governed by wave equations: a sensor measures the velocity at the boundary and an actuator applies a force proportional to it. For the one-dimensional damped wave equation with such feedback, the closed loop is uniformly exponentially stable (Chen, 1979). In practice the measured velocity reaches the actuator only after a computation time, so the feedback acts with a time delay $\varepsilon > 0$. The question addressed by Datko, Lagnese and Polis (1986) is whether arbitrarily small delays can destroy the stability of a system that is stable without them.

Their note answers it with an explicit example and a sharp threshold on the feedback gain. It is the founding example of delay-induced instability in boundary stabilization, cited by most later work on robustness of boundary control to delays.

Timeline.

• Chen (1979, 1981): energy decay $E(u,t) \le Ce^{-\alpha t}E(u,0)$ for boundary-damped wave equations without delay.
• Datko (1978): delays in the velocity term of the equation itself can destabilize; a lemma on zeros of exponential polynomials in vertical strips (the source of Lemma 1 here).
• Datko, Lagnese, Polis (1986, DOI 10.1137/0324007): the delayed boundary feedback $u_x(1,t) = -ku_t(1,t-\varepsilon)$ for the damped string, with a trichotomy in the gain $k$.
• Nicaise and Pignotti (2006, DOI 10.1137/060648891): the multidimensional undamped problem with feedback $-\mu_1u_t(t) - \mu_2u_t(t-\tau)$; stability iff $\mu_2 < \mu_1$, instability for a sequence of delays otherwise.

Setting

Fix real numbers $a \ge 0$ (damping), $k \ge 0$ (feedback gain) and $\varepsilon > 0$ (delay), and put $K = e^{-2a} \in (0,1]$. The delayed system is

$$\begin{aligned} &(1)\quad u_{tt} - u_{xx} + 2au_t + a^2u = 0, && 0<x<1,\ t>0,\\ &(2)\quad u(0,t) = 0, && t>0,\\ &(8)\quad u_x(1,t) = -k\,u_t(1,t-\varepsilon), && t>\varepsilon . \end{aligned}$$

A classical solution is a $C^2$ function $u(x,t)$ with complex values satisfying (1), (2), (8).

Separated solutions $u = e^{\omega t}\varphi(x)$ lead to the eigenvalue problem

$$\varphi''(x) = (a+\omega)^2\varphi(x)\ (0<x<1),\qquad \varphi(0) = 0,\qquad \varphi'(1) + k\omega e^{-\varepsilon\omega}\varphi(1) = 0 .$$

The spectrum $\sigma(a,k,\varepsilon)$ is the set of $\omega \in \mathbb C$ for which this problem has a solution $\varphi$ not identically zero on $[0,1]$. The paper encodes it through the entire functions

$$f(\varepsilon,\omega) = 1 + Ke^{-2\omega} + ke^{-\varepsilon\omega}(1 - Ke^{-2\omega}),\qquad h(\varepsilon,\omega) = \omega f(\varepsilon,\omega) + a(1 + Ke^{-2\omega}),$$

and the critical gain $(1-K)/(1+K)$. In Lean these are K a, f a k ε ω, h a k ε ω, delaySpectrum a k ε, IsClassicalSolution a k ε u and IsExpUnstableSolution a k ε u in the namespace DatkoDelayWave.BoundaryDelay.

Formalization targets

Goal: the stability trichotomy (THEOREM, p. 153)

1. If $0 < k < \frac{1-K}{1+K}$: for each $\varepsilon > 0$ there is $\beta(\varepsilon) > 0$ with

$$\sigma(a,k,\varepsilon) \subseteq \{\operatorname{Re}\omega \le -\beta\}.$$

2. If $k = \frac{1-K}{1+K} > 0$: for each $\varepsilon > 0$, $\sigma(a,k,\varepsilon) \subseteq \{\operatorname{Re}\omega < 0\}$, but there is a countable set $R \subseteq (0,\infty)$, dense in $(0,\infty)$, such that for each $\varepsilon \in R$ some sequence $\omega_n \in \sigma(a,k,\varepsilon)$ has $\operatorname{Re}\omega_n \to 0$.
3. If $k > \frac{1-K}{1+K}$: there is an open set $D \subseteq (0,\infty)$, dense in $(0,\infty)$, such that for each $\varepsilon \in D$ the system has a classical solution with $|u(x_0,t)| \ge ce^{\gamma t}$ for some $\gamma, c > 0$, $x_0 \in (0,1)$ and all $t \ge 0$.

Milestones

In attack order: the characteristic equation (16) ($\omega \in \sigma \iff h(\varepsilon,\omega) = 0$ for $\omega \ne -a$); separated solutions; Lemma 1 (one zero of $f$ forces infinitely many zeros of $f$ and $h$ in every vertical strip around it); (17)–(18) (no zeros of $h$ in the right half-plane below or at the critical gain); the half-plane bound below the critical gain; (19) (no purely imaginary zeros at the critical gain); the explicit zero $f\bigl(\tfrac{2(2m+1)}{2n+1}, \tfrac{(2n+1)\pi i}{2}\bigr) = 0$; density of the delays $\tfrac{2(2m+1)}{2n+1}$; the root family (12)–(15) above the critical gain; Lemma 2 (an open dense set of delays with zeros of $f$ in $\operatorname{Re}\omega > 0$); the three parts of the THEOREM separately; and, off the goal's path, the undelayed formula $\operatorname{Re}\omega = \tfrac12\log\bigl|\tfrac{k-1}{k+1}\bigr|$ for $a = 0$.

Significance

The result shows that exponential stability obtained by boundary velocity feedback is not robust to delays when the gain is above $(1-K)/(1+K)$: delays from a dense set of lengths, including arbitrarily small ones, produce exponentially growing modes. When $a = 0$ the critical gain is $0$, so every positive gain is fragile. Below the critical gain the spectral gap survives every delay. This identifies a quantitative robustness margin and motivated the later analysis of delayed boundary control, including the Nicaise–Pignotti theorems already posed on the platform for a different, multidimensional model (NicaiseDelayWave.*).

The result is proved in the paper, partly by citation: Lemma 1 is quoted from Datko (1978) without proof, and the open-mapping step of Lemma 2 is sketched. No machine-checked version exists. A formalization would check the threshold computations, supply the strip-zero lemma for this exponential polynomial, and give a rigorous version of the open-mapping step.

Difficulty

The algebraic parts, (16)–(19) and the explicit zeros, are calculations with complex exponentials. The difficulty is in Lemma 1 and Lemma 2. Lemma 1 needs the almost-periodic structure of exponential polynomials in vertical strips together with a Hurwitz or Rouché type argument, and neither is in Mathlib. Lemma 2 needs zeros of $f(\varepsilon,\cdot)$ to persist under small changes of the real parameter $\varepsilon$. The paper's route through the logarithmic map (11) does not work as printed, because it is stated with the principal branch exactly on the branch cut. In part (i), the delicate step is excluding accumulation of zeros at the imaginary axis as $|\operatorname{Im}\omega| \to \infty$, which the half-plane estimate alone does not give.

Formalization scope

Parameters $a, k, \varepsilon$ are real, $\omega \in \mathbb C$, eigenfunctions are maps $\mathbb R \to \mathbb C$ and solutions are maps $u : \mathbb R \to \mathbb R \to \mathbb C$ (space first). Partial derivatives are deriv of the sections. Solutions and eigenfunctions are required to be $C^2$ on all of $\mathbb R^2$, resp. $\mathbb R$; this loses no eigenvalue, since solutions of (5) are combinations of $e^{\pm(a+\omega)x}$. Committed readings of the paper's loose phrases:

• the spectrum is the eigenvalue set of the problem above, not the zero set of $h$; $h(\varepsilon,-a) = 0$ always, so (16) is stated for $\omega \neq -a$;
• "countably dense set $R$ in $(0,\infty)$": $R \subseteq (0,\infty)$, $R$ countable, $(0,\infty) \subseteq \overline R$;
• "dense open set $D$ in $(0,\infty)$": $D \subseteq (0,\infty)$ open, $(0,\infty) \subseteq \overline D$;
• "exponentially unstable solution": a classical solution with $|u(x_0,t)| \ge ce^{\gamma t}$ for all $t \ge 0$;
• "an infinite number of zeros" (Lemma 1): the zero set in the open strip is infinite, for $f$ and for $h$ separately;
• "there exists $\beta(\varepsilon) > 0$": $\forall \varepsilon > 0\ \exists \beta > 0$, so $\beta$ may depend on $\varepsilon$;
• part (ii) carries $k > 0$, the paper's standing assumption (p. 152); without it the part is false at $a = 0$;
• $m, n$ in $2(2m+1)/(2n+1)$ are positive integers in (12)–(15) and in the density of (15), as in the proof of Lemma 2; in the explicit threshold zero, where the page says "$m, n$ are arbitrary", they range over all natural numbers.

Trivializing encodings are ruled out: defining the spectrum as the zero set of $h$ would make $-a$ a spurious spectral point, and reading "exponentially unstable" as "the spectrum meets $\operatorname{Re}\omega > 0$" would delete the solution-level content of part (iii).

A complete development needs zero-counting tools for exponential polynomials in strips (almost periodicity, Hurwitz's theorem), which would be reusable for other delay equations. Contributions to any milestone, and to that general infrastructure, are welcome.

Selected references

• R. Datko, J. Lagnese, M. P. Polis, An example on the effect of time delays in boundary feedback stabilization of wave equations, SIAM J. Control Optim. 24(1), 152–156, 1986. https://doi.org/10.1137/0324007
• R. Datko, A procedure for determination of the exponential stability of certain differential-difference equations, Quart. Appl. Math. 36, 279–292, 1978.
• G. Chen, Energy decay estimates and exact boundary value controllability for the wave equation in a bounded domain, J. Math. Pures Appl. 58, 249–274, 1979.
• S. Nicaise, C. Pignotti, Stability and instability results of the wave equation with a delay term in the boundary or internal feedbacks, SIAM J. Control Optim. 45(5), 1561–1585, 2006. https://doi.org/10.1137/060648891