Operations Research Probability Stochastic Systems·Captain: mikedeng1

Elements of Queueing Theory II: The Loynes Stability Theorem and CouplingTextbook

The Loynes Stability Theorem and Coupling

Background

Chapter 1 of Baccelli and Brémaud's Elements of Queueing Theory builds a calculus for stationary queues. Chapter 2 asks the prior question: when is there a stationary queue at all?

The G/G/1/∞ queue is one server at unit rate, infinite waiting room, fed by a stationary marked point process {(T_n, σ_n)} — arrival epochs and required service times. Its workload W(t), the service still owed by the server, obeys Lindley's equation between arrivals:

W(t) = (W(T_n−) + σ_n − (t − T_n))⁺,    t ∈ [T_n, T_{n+1}).                          (2.1.6)

Nothing in that equation says a solution exists on the whole line, let alone a stationary one. The answer is a sharp criterion in the traffic intensity ρ = λE⁰_A[σ_0].

The goal

Theorem 2.1.1 (p.80), which the book calls "the fundamental result of stability". Under ρ < 1 there is a unique finite workload process on all of ℝ, compatible with the flow, and it is given explicitly by the Loynes supremum

W(0) = sup_{n ≤ 0} ( T_n + Σ_{i=n}^{0} σ_i )⁺ ,                                      (2.1.12)

with W(T_n−) = 0 for infinitely many negative and infinitely many positive n (2.1.13). If ρ > 1 there is no finite stationary workload process at all.

Each half earns its place. The supremum is what "the Loynes construction" means: look back from the origin, take the work brought by customers n, …, 0 less the time −T_n since elapsed, and maximise over how far back you look. The ρ > 1 half is what turns ρ < 1 from a sufficient condition into a criterion. The critical case ρ = 1 is an explicit non-result in the book — there "may or may not" be a stationary workload — and is deliberately absent from the statement.

The route, and what it produces on the way

§2.2 proves the theorem by Loynes' monotone scheme on the Palm space, and two of its steps are worth stating in their own right.

Lemma 2.2.1 (p.87) is the uniqueness engine: a non-negative, a.s. finite Z with Z − Z∘θ ∈ L¹(P⁰) has E⁰[Z − Z∘θ] = 0. Applied to the difference of two stationary solutions, it forces that difference to be invariant, and ergodicity then forces it to be zero.

Theorem 2.2.1 (p.90) runs the argument backwards. Its section is titled "Queueing Proof of the Ergodic Theorem", and it is exactly that: the queueing construction yields the pointwise ergodic theorem, in the ratio form

lim_n ( Σ_{i=0}^n σ∘θ^{-i} ) / ( Σ_{i=0}^n τ∘θ^{-i} ) = E⁰[σ]/E⁰[τ],    P⁰-a.s.

Mathlib has the mean (von Neumann) ergodic theorem and no pointwise one, so this is absent substrate rather than a restatement.

Three extensions

The multiserver queue (§2.3). With s servers and the least-loaded-server rule, the state is the ordered workload vector obeying the Kiefer–Wolfowitz recurrence, and the criterion becomes E⁰[σ] < s E⁰[τ] (Theorem 2.3.1, p.93). Here uniqueness fails: p.94 exhibits a two-point space with a whole interval of stationary solutions. What survives is that the solution set is bracketed — M_∞ is minimal, and V^∞_∞ is the largest finite solution (Theorem 2.3.2, p.95).

Coupling (§2.4). Theorem 2.4.1 (p.99) is what "reaches the stationary regime" means: if a sequence couples with a θ-compatible one, then the law of its whole shifted trajectory converges in variation to the stationary trajectory's. The proof is one inequality, |P̃_{X,k} − P̃_{Z,k}| ≤ P(N > k), and the finiteness of the coupling time.

The fluid queue (§2.7). Theorem 2.7.1 (p.131) replaces customers by two θ_t-compatible random measures, the arrivals A and the service capacity C, and recovers the Loynes supremum W(t) = sup_{u ≤ t}(A_{u,t} − C_{u,t}) under λ < µ — as the minimal solution, the book claiming no uniqueness here.

Formalization scope

ρ = λE⁰_A[σ_0] takes values in [0, ∞], so an input with E⁰_A[σ_0] = ∞ has ρ = ∞ and falls under the non-existence half rather than being read as ρ = 0.
The explicit formulas are carried: the Loynes supremum (2.1.12) with the boundedness of its set as a conclusion, the construction points (2.1.13), the ratio limit E⁰[σ]/E⁰[τ] of Theorem 2.2.1, the threshold s E⁰[τ] of Theorem 2.3.1, and the fluid supremum (2.7.7).
Identities between random variables hold almost surely, as in the book: the workload equations, (2.1.12)–(2.1.13), (2.7.7), and the solutions of (2.3.2). A statement "for every sample point" would be false, because on a null invariant set of sample paths no finite solution exists.
Uniqueness in Theorem 2.1.1 is among measurable, θ_t-compatible workload processes; maximality in Theorem 2.3.2 is among measurable finite solutions; the coupling time of Theorem 2.4.1 is a random variable. A formalization that dropped the explicit supremum, or the ρ > 1 half, would trivialize the goal and is ruled out.

What this mission provides

None of it is on the platform or in Mathlib. The nearest platform item, single_server_queueing_convergence_of_subcritical, presupposes a stationary workload and proves two-time finite-dimensional convergence to it; Theorem 2.1.1 constructs that workload, proves it unique, gives it in closed form, and adds the non-existence half. Different conclusion, different generality, different Mathlib revision.

13 thms2 active usersReviewed

Analysis Operations Research Probability+1·Captain: mikedeng1

Elements of Queueing Theory Ib: Ergodicity and Stochastic IntensityTextbook

Ergodicity and Stochastic Intensity

Background

Chapter 1 of Baccelli and Brémaud's Elements of Queueing Theory has two halves. The first builds Palm calculus from the Matthes definition of P⁰_N and reaches the Swiss army formula. This mission is the second: §§1.6, 1.8 and 1.9, which supply the two things the rest of the book runs on.

Ergodic theory, quoted

§1.6 states, in its own words, "the ergodic theory results to be used later in this book". Five of them, and the book proves none: Birkhoff's pointwise ergodic theorem in discrete (Theorem 1.6.1) and continuous time (Theorem 1.6.4), Kingman's sub-additive ergodic theorem (Theorem 1.6.2), and the extremal characterizations of ergodicity in both settings (Theorems 1.6.3 and 1.6.5) — ergodicity is exactly the impossibility of splitting an invariant probability into two distinct ones.

They are quoted, but they are not decoration. Kingman's theorem is what produces the asymptotic growth rates of Theorem 2.11.2 and the constant γ(c) on which the saturation rule rests. Birkhoff's theorem is what makes the time average in PASTA's (3.3.2) a well-defined object, and what the fluid Loynes theorem invokes for lim_{u→−∞}(A_{u,0} − C_{u,0}) = −∞.

None of the three analytic ones exists in Mathlib. Analysis/InnerProductSpace/MeanErgodic is the mean (von Neumann, L²) theorem, not almost-everywhere convergence, and there is no sub-additive ergodic theorem at all. The platform has neither.

Predictability, and why PASTA can be stated

§1.8 introduces the stochastic intensity: a point process N admits the (P, F_t)-intensity {λ(t)} when E[N(a,b] 1_A] = E[(∫_a^b λ(t)dt) 1_A] for A ∈ F_a. Around it sits the notion of a predictable process — one measurable with respect to the strict past.

Theorem 1.8.1 is the structural fact that makes predictability usable. For the internal history of a marked point process, every predictable process has the concrete form

Z(t, ω) = v(t, θ_t ω),    v(t, ·) F_{0−}-measurable.                                   (1.8.1)

That is why mission IV can take this form as PASTA's hypothesis rather than constructing a predictable σ-field: Theorem 1.8.1 says nothing is lost.

The goal

Theorem 1.8.2 (p.61), §1.8.4, Watanabe's characterization of Poisson processes. For a history F_t = F_t^N ∨ G and a G-measurable, locally integrable {λ(t)}, if N admits the F_t-intensity {λ(t)} then N is a G-conditional Poisson process:

E[ e^{iuN(a,b]} | G ∨ F^N_a ] = exp{ (e^{iu} − 1) ∫_a^b λ(t) dt } .                    (1.8.12)

A stochastic intensity that carries no information beyond G forces the process to be Poisson conditionally on G, with the compensator as the parameter — and the conditional characteristic function is the exact Poisson one, not an approximation. With G trivial and λ constant this is the ordinary Poisson process, which is the equivalence Remark 3.3.1 of Chapter 3 invokes to explain the name PASTA. The book: "This result plays a role in queueing theory, especially for proving that some streams in a queueing network are or are not Poissonian."

Palm probability meets stochastic intensity

§1.9 asks whether the stochastic intensity is the same under P and under P⁰_N — whether the two probabilities describe the same dynamics. Theorem 1.9.1 says yes, on ℝ₊: the same process {λ(t)} serves both.

Theorem 1.9.2 is Papangelou's theorem, and it is the deepest statement of the section: N admits a stochastic intensity if and only if P⁰_N ≪ P on F_{0−}, and then λ(t) = (μ ∘ θ_t)λ with μ the Radon–Nikodým derivative. A dynamic property and a static one turn out to be the same thing.

Theorem 1.9.3 is Mecke's characterization: N is Poisson exactly when P ≡ P⁰_N on F_{0−}. The view from a point of the process and the view from a deterministic instant agree on the strict past precisely when the process has no memory. It follows in one line from the two theorems before it.

What this mission provides

Four of the five missions in this series import the Chapter 1 substrate; this one adds the two pieces they need from its second half — ergodic theory and the stochastic intensity. Nothing here is on the platform, and Mathlib has filtrations and adapted processes but no predictability in this form, no stochastic intensity, no pointwise ergodic theorem and no Kingman.

Formalization scope

Every result is stated in the book's strength, with the book's standing definitions as binders. A discrete flow is a bijective, measurable, P⁰-preserving map (p.46); a continuous flow is jointly measurable in (t, ω) (p.3, clause (a)). A history compatible with the flow satisfies θ_t F_s = F_{s−t} (p.57), and an F_t-intensity is a non-negative, measurable, locally integrable, adapted process (p.58). The limits of Theorems 1.6.1, 1.6.2 and 1.6.4 are asserted to exist; Kingman's constant h̄ lies in ℝ ∪ {−∞} and is identified with inf_n (1/n) E⁰[h_n], the means being extended reals so that E⁰[h_n] = −∞ is not read as 0. Theorems 1.6.3, 1.6.5, 1.9.2 and 1.9.3 are equivalences, and Theorem 1.9.2 carries the closed form λ(t) = (μ ∘ θ_t)λ with μ = dP⁰_N/dP on F_{0−}. The goal's conclusion is the exact conditional characteristic function (1.8.12); a formalization that only asserted some conditional Poisson law, or conditioned on G alone, would not be this theorem.

13 thms2 active usersReviewed

Algorithmic Game Theory Mechanism Design Operations Research·Captain: mikedeng1

Strategyproof Approximation of the Minimax on Networks 2: No Strategyproof Randomized Mechanism Beats 2 - o(1) on TreesResearch Paper

Motivation

A public facility (a fire station, a hospital, a server) is to be placed on a road network, and the people it serves report their own locations. When the planner wants to minimise the distance to the farthest user (the minimax or egalitarian objective, in the sense of Rawls), each user has an incentive to misreport so as to pull the facility towards themselves. Mechanism design without money asks which location rules make truthful reporting a dominant strategy, and how much of the optimal objective such rules must give up. Procaccia and Tennenholtz (EC 2009) introduced this approximation viewpoint for points on a line; Schummer and Vohra (J. Econom. Theory 2002) characterised the strategyproof deterministic rules on networks.

Alon, Feldman, Procaccia and Tennenholtz (Math. Oper. Res. 2010) study the minimax on general networks. Choosing a fixed agent's location (dictatorship) is strategyproof and loses at most a factor 2 on any network. On a circle they give a randomized strategyproof mechanism with ratio $3/2$ . On trees a simple randomized mechanism achieves $2-2/(n+2)$ . This mission is about their matching negative result: on trees, no strategyproof randomized mechanism does better than $2-o(1)$ .

Setting

A network $G$ is a metric space whose points are the vertices of a graph and every point inside its edges; the distance $d(a,b)$ is the length of the shortest path. There are $n$ agents; a location profile is $x=(x_1,\dots,x_n)\in G^n$ . A randomized mechanism $f$ maps each profile to a probability distribution $f(x)$ over $G$ , the location of the facility. An agent at $a$ bears the cost $\operatorname{cost}(P,a)=\mathbb E_{y\sim P}[d(a,y)]$ , and the maximum cost of $P$ for the profile $x$ is

\operatorname{mc}(P,x)=\mathbb E_{y\sim P}\Big[\max_{i} d(x_i,y)\Big].

The mechanism is strategyproof (SP) if no agent can lower its own cost by reporting another point: for all $x$ , $i$ and $x_i'\in G$ , $\operatorname{cost}(f(x),x_i)\le\operatorname{cost}(f(x_i',x_{-i}),x_i)$ . The benchmark is the best deterministic location, $\mathrm{OPT}(x)=\min_{z\in G}\operatorname{mc}(\delta_z,x)$ .

The network of the theorem is the tree $G(m,k)$ : an edge of length $1$ joins two roots $l^0$ and $r^0$ ; below each root hangs a complete $m$ -ary tree of depth $k$ whose edges from level $d$ to level $d+1$ have length $2^d$ . The profiles used are the paper's $x^0,x^1,\dots,x^k$ : $x^0$ puts $n/2$ agents on each root, and $x^{d+1}$ moves the $n/(2m^d)$ agents at a chosen left vertex $l^d$ on level $d$ to its $m$ children, equally.

Formalization targets

Goal: Theorem 4.1 with its explicit constant

For $m\ge2$ , $k\ge1$ , $n\ge1$ with $2m^k\mid n$ , and every SP randomized mechanism $f$ on $G(m,k)$ for $n$ agents, there is a profile $x$ with $\mathrm{OPT}(x)>0$ and

\operatorname{mc}(f(x),x)\ \ge\ \Big(2-\frac1{2^k}-\frac4m\Big)\,\mathrm{OPT}(x).

The paper states the bound as $2-O(1/2^{\sqrt{\log n}})$ ; the displayed form is what its proof establishes (p. 526), and $k=\Theta(\sqrt{\log n})$ , $m=\Theta(n^{1/k})$ turn it into the $O(\cdot)$ form.

Milestones

Strategyproofness preserves $\mathbb E[d(f(x^1),l^0)]\ge 1/2$ when the agents leave $l^0$ (p. 524).
For every point $y$ with $d(y,l^0)\ge1/2$ : $\sum_{j=1}^m d(y,l^1_j)\ge(3m-2)/2$ (p. 525).
Lemma B.1: some left vertex $l^k$ on level $k$ has $\mathbb E[d(f(x^k),l^k)]\ge\frac{2^{k+1}-1}{2}-\frac{2^{k+1}-(k+2)}{m}$ (p. 525).
The expected maximum cost $\operatorname{mc}(f(x^k),x^k)$ is at least the same bound (p. 526).
Under $x^k$ the deterministic facility at $l^{k-1}$ has maximum cost exactly $2^{k-1}$ (p. 526).

Significance

The result. Dictatorship already achieves ratio $2$ on every network, and on trees the best known SP mechanism improves this only to $2-2/(n+2)$ . Theorem 4.1 shows that this is essentially optimal: randomization, which buys a factor $3/2$ on the circle, buys almost nothing on trees once the tree is allowed to branch widely. It separates two natural network classes by their strategyproof approximability, and the paper notes that trees of bounded branching factor escape the construction, which leaves that class as the open case.

Formalizing it. The result is proved in the paper and has no machine-checked proof. The mission produces a checked lower bound for all SP randomized mechanisms on a continuous network, quantified over arbitrary probability measures and arbitrary deviations, together with a reusable model of facility location with strategic agents on a metric network and an explicit construction of a weighted metric tree.

Difficulty

The bound holds against every mechanism, so no mechanism is analysed: the only handle on $f$ is the SP inequality, applied along a chain of unilateral deviations whose length is the number of agents moved. The chain must be organised so that the bound on one expected distance survives each level of the tree, and the pointwise geometric inequality on the tree must be turned into a bound on expectations under an arbitrary distribution that may put mass inside edges. The final comparison needs the exact optimum of a specific profile and exact arithmetic on the resulting ratio. Restricting the facility to vertices, or assuming the mechanism is anonymous or continuous, would change the class of mechanisms and is not allowed.

Formalization scope

The network is HardTree m k, the tree $G(m,k)$ realised isometrically inside $\ell^1$ (one coordinate per edge), with the subspace metric (equal to shortest-path length on the embedded tree) and the Borel σ-algebra. Edge interiors are points of the space. Vertices are vertex s w for a side s and a word w over Fin m.
Agents are Fin n; a mechanism is any function (Fin n → HardTree m k) → ProbabilityMeasure (HardTree m k); strategyproofness quantifies over every profile, agent and point of the tree. No measurability, anonymity or continuity of $f$ is assumed. cost and mc are Bochner integrals of bounded continuous functions; $\mathrm{OPT}$ is optMc, an infimum over all points.
Explicit constant: the paper's $2-O(1/2^{\sqrt{\log n}})$ is stated as $2-1/2^k-4/m$ on $G(m,k)$ , the bound its proof yields on p. 526. The asymptotic form in $n$ is not stated: the paper assumes $2m^k\mid n$ "for ease of exposition" and does not treat the leftover agents for general $n$ , so the divisibility is a hypothesis.
The paper's "without loss of generality $\mathbb E[d(f(x^0),l^0)]\ge1/2$ " is a hypothesis of milestones 1, 3 and 4 only; the goal covers both cases.
A trivializing reading is ruled out: the goal requires $\mathrm{OPT}(x)>0$ , so a profile with all agents at one point (where both sides vanish) is not a witness.
A complete development needs basic facts about the $\ell^1$ tree metric (distances along paths, compactness), integrals of bounded continuous functions against probability measures, and the arithmetic of the bound. The model file and the tree construction are reusable for other facility-location results on trees.

Selected references

N. Alon, M. Feldman, A. D. Procaccia, M. Tennenholtz, Strategyproof Approximation of the Minimax on Networks, Mathematics of Operations Research 35(3):513–526, 2010. https://doi.org/10.1287/moor.1100.0457
A. D. Procaccia, M. Tennenholtz, Approximate Mechanism Design without Money, Proc. 10th ACM Conference on Electronic Commerce, 177–186, 2009. https://doi.org/10.1145/1566374.1566401
J. Schummer, R. V. Vohra, Strategy-proof Location on a Network, Journal of Economic Theory 104(2):405–428, 2002. https://doi.org/10.1006/jeth.2001.2807
N. Alon, M. Feldman, A. D. Procaccia, M. Tennenholtz, Strategyproof Approximation Mechanisms for Location on Networks, 2009. https://arxiv.org/abs/0907.2049

9 thms2 active usersReviewed

Algorithmic Game Theory Mechanism Design Operations Research·Captain: mikedeng1

Strategyproof Approximation of the Minimax on Networks 1: A Strategyproof 3/2-Approximation Mechanism on the CircleResearch Paper

Motivation

A facility — a fire station, a server, a meeting point — must be placed on a network, and every user of the network reports where they are. When the planner cares about the worst-off user, the objective is the minimax: minimize the largest distance from the facility to a user. The reports are private information, so a user may misreport a location to pull the facility towards itself. Approximate mechanism design without money, proposed by Procaccia and Tennenholtz (2009), asks how close to optimal a mechanism can stay when no user ever benefits from lying.

On a line the picture is complete. A deterministic strategyproof mechanism cannot beat ratio 2 for the minimax, and a randomized one cannot beat 3/2. The left-right-middle (LRM) mechanism attains 3/2 (Procaccia and Tennenholtz, 2009). Networks with cycles are harder: the extreme agents that LRM needs do not exist on a circle. Alon, Feldman, Procaccia and Tennenholtz (2010) give a randomized strategyproof mechanism on the circle whose ratio is again 3/2, which is best possible. They also show that on trees no randomized strategyproof mechanism does much better than dictatorship. This mission formalizes the circle result, Theorem 3.1 of that paper.

Setting

The circle $G$ has circumference one and carries the arc-length distance $d(a,b)\in[0,1/2]$ . There are $n$ agents; agent $i$ has a location $x_i\in G$ , and $x=(x_1,\dots,x_n)\in G^n$ is the location profile. A randomized mechanism maps each profile to a probability distribution $P$ over $G$ , the location of the facility. Agent $i$ 's cost and the maximum cost of $P$ are

\operatorname{cost}(P,x_i)=\mathbb{E}_{y\sim P}[d(x_i,y)],\qquad \operatorname{mc}(P,x)=\mathbb{E}_{y\sim P}\Big[\max_{i} d(x_i,y)\Big].

A mechanism $f$ is strategyproof if for every profile $x$ , every agent $i$ and every misreport $x_i'$ , $\operatorname{cost}(f(x),x_i)\le\operatorname{cost}(f(x_i',x_{-i}),x_i)$ . It is a $\rho$ -approximation for the minimax if $\operatorname{mc}(f(x),x)\le\rho\cdot\min_{z\in G}\operatorname{mc}(\delta_z,x)$ for every $x$ .

The agents are on one semicircle if a closed arc of length $1/2$ contains all of them. The antipodal point of $a$ is $\hat a=a+1/2$ . Mechanism 3.1 works as follows:

if the agents are on one semicircle, it treats that arc as an interval and runs LRM ( $\operatorname{lrm}(x)$ ): with probability $1/4$ it returns the leftmost agent, with probability $1/4$ the rightmost agent, and with probability $1/2$ the midpoint between them;
otherwise it runs the random center (RC) mechanism ( $\operatorname{rc}(x)$ ): the antipodal points $\hat x_1,\dots,\hat x_n$ cut the circle into arcs, and RC returns the centre of each arc with probability equal to the arc's length.

In Lean the circle is AddCircle (1 : ℝ), a profile is x : Fin n → AddCircle (1 : ℝ), the deviated profile is Function.update x i x', and the definitions are cost, mc, IsStrategyproof, IsApproximation, OnSemicircle, lrm, rc and mech31 in the namespace StrategyproofMinimax.Circle.

Formalization targets

Goal: Theorem 3.1

\texttt{IsStrategyproof}\ \texttt{mech31}\ \wedge\ \texttt{IsApproximation}\ \tfrac32\ \texttt{mech31},

that is, for all $n$ , $x\in G^n$ , $i$ and $x_i'\in G$ ,

\operatorname{cost}(\operatorname{mech31}(x),x_i)\le\operatorname{cost}(\operatorname{mech31}(x_i',x_{-i}),x_i) \quad\text{and}\quad \operatorname{mc}(\operatorname{mech31}(x),x)\le\tfrac32\min_{z\in G}\operatorname{mc}(\delta_z,x).

The constant $3/2$ is the paper's own and is optimal.

Milestones (Appendix A)

Lemma A.1: the approximation half, $\operatorname{mc}(\operatorname{mech31}(x),x)\le\frac32\,\mathrm{OPT}(x)$ .
Lemma A.2 (semicircle to semicircle): if $x$ and $x'=(x_i',x_{-i})$ are both on one semicircle, $\operatorname{cost}(\operatorname{lrm}(x),x_i)\le\operatorname{cost}(\operatorname{lrm}(x'),x_i)$ .
Lemma A.3: for $x,y\in[0,1]\subset\mathbb{R}$ , $|x-\tfrac12|\le y\,|x-\tfrac y2|+(1-y)\,|x-\tfrac{y+1}2|$ .
Lemma A.5: if $x$ is not on one semicircle, $\operatorname{cost}(\operatorname{rc}(x),x_i)\le\frac14$ .
Lemma A.6 (not semicircle to semicircle): $\operatorname{cost}(\operatorname{rc}(x),x_i)\le\operatorname{cost}(\operatorname{lrm}(x'),x_i)$ .
Lemma A.7: if $x$ is not on one semicircle and $y\in G$ , $\operatorname{cost}(\operatorname{rc}(x\cup\{y\}),y)\le\operatorname{cost}(\operatorname{rc}(x),y)$ .
Lemma A.8 (semicircle to not semicircle): $\operatorname{cost}(\operatorname{lrm}(x),x_i)\le\operatorname{cost}(\operatorname{rc}(x'),x_i)$ .
Lemma A.9 (not semicircle to not semicircle): $\operatorname{cost}(\operatorname{rc}(x),x_i)\le\operatorname{cost}(\operatorname{rc}(x'),x_i)$ .

The four deviation lemmas A.2, A.6, A.8 and A.9 together are the strategyproofness half of the goal.

Significance

The theorem closes the randomized minimax question on the circle: the ratio 3/2 matches the lower bound that already holds on a line, so cycles cost nothing once randomization is allowed. This contrasts with the tree result of the same paper, where no randomized strategyproof mechanism beats $2-o(1)$ . Mechanism 3.1 is also an example of something that is not true in general: combining two strategyproof mechanisms by a case split on the profile usually breaks strategyproofness at the boundary between the cases, and here it does not. Any characterization of randomized strategyproof mechanisms on networks, an open problem the paper raises, has to account for such hybrids.

The result is proved on paper, in the paper's Appendix A. It has no machine-checked proof. A formalization also produces reusable pieces: facility-location mechanisms and their costs on a metric space, LRM on an interval, and cost computations for finitely supported distributions on AddCircle.

Difficulty

A deviation can move the profile across the boundary between the two regimes: from one semicircle to not one semicircle, or back. Strategyproofness of LRM and RC separately therefore does not give strategyproofness of the hybrid; the four regime-crossing cases need separate arguments, which compare an LRM cost with an RC cost directly. RC's outcome depends on every agent's antipodal point, so a single deviation removes one cut point and inserts another; its effect on the deviator's cost has to be controlled across the whole partition. Even the semicircle-to-semicircle case is not inherited from the line: the deviation can change which semicircle is used, and with it which agents are extreme. On the formal side, every cost is an integral against a finitely supported measure on AddCircle, and the case analysis runs through arc-length distances that wrap around.

Formalization scope

The circle is normalized to circumference one, as in the paper's Appendix A. Rescaling the circle scales all costs by the same factor, so strategyproofness and the ratio are unaffected.
Distributions are Measure (AddCircle 1). lrm, rc and mech31 are explicit finite sums of Dirac masses whose weights sum to one. cost and mc are Bochner integrals of continuous bounded functions against these finite measures, so they are always the true expectations.
"On one semicircle" is ∃ c, ∀ i, ‖x i - c‖ ≤ 1/4: a closed arc, so agents spread over exactly a half circle are on one semicircle.
RC is defined in the paper's own equivalent form (p. 517): the centre of each arc between adjacent antipodal points, with probability equal to the arc's length. It is defined for every profile, and depends only on the set of locations. $x\cup\{y\}$ is Fin.snoc x y.
When the agents occupy exactly one antipodal pair $\{p,\hat p\}$ , two closed semicircles cover them and LRM's midpoint depends on the choice. The paper leaves this open. lrm fixes it: it uses the semicircle centred at $x_j-1/4$ for the least index $j$ for which this centre covers all agents.
The approximation is multiplicative, $\operatorname{mc}\le\frac32\cdot\mathrm{OPT}$ , never a quotient: $\mathrm{OPT}$ is $0$ when all agents coincide. Statements hold for every $n$ , including the trivial $n=0$ .
The statements are not trivialized by a junk value: the mechanisms are genuine probability distributions, no integral can silently default to $0$ , the optimum is an infimum of a continuous function over the compact circle, and the deviation $x_i'$ ranges over the whole circle, not over moves that stay in the same regime.
Lemma A.4 of the paper (a telescoping identity used inside Lemma A.5) is not a milestone.

Contributions welcome: API for integrals against finite sums of Dirac masses on AddCircle, lifting of arcs of length at most $1/2$ to intervals of $\mathbb{R}$ , and LRM strategyproofness on an interval.

Selected references

N. Alon, M. Feldman, A. D. Procaccia, M. Tennenholtz, Strategyproof Approximation of the Minimax on Networks, Mathematics of Operations Research 35(3):513–526, 2010. https://doi.org/10.1287/moor.1100.0457
A. D. Procaccia, M. Tennenholtz, Approximate Mechanism Design without Money, Proc. 10th ACM Conference on Electronic Commerce (EC), 177–186, 2009. https://doi.org/10.1145/1566374.1566409
J. Schummer, R. V. Vohra, Strategy-proof Location on a Network, Journal of Economic Theory 102(2):405–428, 2002. https://doi.org/10.1006/jeth.2001.2821

13 thms2 active usersReviewed

Dynamical Systems Geometry & Topology·Captain: Lucas

Building Anosov flows on 3-manifolds (Béguin–Bonatti–Yu)Research Paper

Motivation

Anosov flows are the model of uniformly hyperbolic, chaotic continuous-time dynamics: a nonsingular vector field $X$ on a closed manifold $M$ is Anosov when the tangent bundle splits as $TM=E^s\oplus\mathbb RX\oplus E^u$ , with $E^s$ uniformly contracted and $E^u$ uniformly expanded by the derivative of the flow. They are structurally stable, so one can hope to classify them up to topological equivalence. In dimension three this classification is far from complete: it is not known which closed 3-manifolds carry Anosov flows, nor how many inequivalent Anosov flows a given manifold can carry.

The classical examples — suspensions of hyperbolic toral automorphisms and geodesic flows of hyperbolic surfaces — are rigid (Plante; Ghys). Non-algebraic examples were built by Franks–Williams (a nontransitive Anosov flow, 1980), Handel–Thurston, Goodman, Fried, Bonatti–Langevin, Fenley, Barbot and others. Several of these examples glue together neighbourhoods of hyperbolic sets along their boundaries. Béguin, Bonatti and Yu (Geom. Topol. 21 (2017)) turned this into a general theory, and used it to answer questions of Katok and of Barbot–Fenley.

Setting

A plug $(U,X)$ is a compact 3-manifold $U$ with boundary and a nonsingular C¹ vector field $X$ transverse to $\partial U$ . The boundary splits into the entrance boundary $\partial^{in}U$ (where $X$ points inwards) and the exit boundary $\partial^{out}U$ . The maximal invariant set $\Lambda$ consists of the points whose orbit stays in $U$ for all times. The plug is hyperbolic if $\Lambda$ is a hyperbolic set with one-dimensional strong stable and strong unstable bundles. The entrance lamination $L^s_X=W^s(\Lambda)\cap\partial^{in}U$ and the exit lamination $L^u_X=W^u(\Lambda)\cap\partial^{out}U$ are one-dimensional laminations of the boundary surfaces. The plug has filling MS laminations when every component of $\partial^{in}U\setminus L^s_X$ (and of $\partial^{out}U\setminus L^u_X$ ) is a strip: a disc whose accessible boundary consists of two leaves asymptotic to each other at both ends.

A diffeomorphism $\varphi:\partial^{out}U\to\partial^{in}U$ is a strongly transverse gluing map if $\varphi_*(L^u_X)$ and $L^s_X$ are transverse and cut $\partial^{in}U$ into squares with sides alternately on leaves of the two laminations. Gluing then gives a closed manifold $U/\varphi$ with an induced vector field $Z$ . Two triples $(U,X,\varphi)$ and $(U,Y,\psi)$ are strongly isotopic if they are joined by a continuous path of such data.

Formalization targets

Goal: the gluing theorem (Theorem 1.5)

\begin{gathered}(U,X)\ \text{hyperbolic plug with filling MS laminations},\ \Lambda\ \text{without attractors or repellers},\ \varphi\ \text{strongly transverse}\\ \Longrightarrow\ \exists\,(Y,\psi)\ \text{strongly isotopic to}\ (X,\varphi)\ \text{with the field induced by } Y \text{ on } U/\psi\ \text{Anosov}.\end{gathered}

Milestones

Proposition 1.1: gluing two hyperbolic plugs along transverse laminations gives a hyperbolic plug. Proposition 1.3: strongly transverse gluing preserves filling MS laminations.
Lemma 3.27 (self-gluing case): the glued manifold $U/\varphi$ exists as a closed smooth manifold with an induced vector field.
Proposition 1.6: if the graph of basic pieces is strongly connected, the Anosov flow of Theorem 1.5 is transitive.
Theorem 1.8: every transitive Anosov flow on a closed 3-manifold is a factor of a transitive Anosov flow on another closed 3-manifold, restricted to a compact invariant set.
Theorem 1.9: some closed orientable 3-manifold carries both a transitive and a nontransitive Anosov flow.
Theorem 1.10 and Corollary 1.11: every MS foliation of a closed orientable surface is the entrance foliation of a transitive attracting hyperbolic plug; in particular incoherent transitive hyperbolic attractors exist.
Theorem 1.12: every hyperbolic plug with filling MS laminations embeds, up to topological equivalence, in an Anosov flow on a closed orientable 3-manifold, which can be taken transitive when $\Lambda$ has no attractors or repellers.
Theorem 1.13: for every $n\ge1$ some closed orientable 3-manifold carries $n$ pairwise inequivalent transitive Anosov flows.
Theorem 1.15: some transitive Anosov flow admits infinitely many pairwise nonisotopic transverse tori.

Significance

Theorem 1.5 lets one build Anosov flows on closed 3-manifolds by gluing hyperbolic plugs. Proposition 1.6 gives a combinatorial criterion for the result to be transitive. Together they answer a question of Katok (Theorem 1.9) and questions of Barbot and Fenley on manifolds with several hyperbolic JSJ pieces supporting transitive Anosov flows (Theorem 1.13). They also show that transitive Anosov flows admit no fully canonical decomposition into finitely many transverse tori (Theorem 1.15). The results are proved in the source paper. None of them is formalized, and Mathlib has no theory of hyperbolic sets for flows, stable manifolds or laminations. A formal proof therefore needs a substantial amount of reusable smooth dynamics.

Difficulty

The glued vector field is generally not hyperbolic: perturbing the gluing map can create solid tori of parallel periodic orbits. The difficulty is to choose the gluing map (and the vector field within its topological equivalence class) so that cone fields on $\partial^{in}U$ are mapped into themselves by the return map. The return map is the composition of the crossing map of the plug with the gluing map. Contraction and expansion must therefore be controlled simultaneously along two transverse invariant foliations. The paper achieves this after reducing to plugs with an affine Markov partition. The naive approach — fixing $\varphi$ and trying to verify hyperbolicity — fails in general (Question 1.4 of the paper remains open).

Formalization scope

Manifolds are modelled on the half-space EuclideanHalfSpace 3 with a $C^\infty$ structure; closed manifolds are compact, Hausdorff and BoundarylessManifold, and connected where the paper's statements concern a single manifold. Orientability is given by an atlas with positive Jacobians.
Vector fields are C¹ sections; flows are encoded by integral curves, so that partial flows on manifolds with boundary make sense; flowMap X t x is $x$ when the orbit is undefined.
Hyperbolicity is quantified over a continuous Riemannian metric, invariant line fields and constants $C,\lambda>0$ ; continuity of the splitting is not imposed (it is automatic).
Filling MS laminations are encoded through the strip condition (Lemma 3.21); leaves of $L^s$ are path components of intersections of weak stable manifolds with $\partial^{in}U$ .
The glued manifold $U/\varphi$ is not a quotient type: statements quantify over every closed smooth 3-manifold $N$ with a surjective C¹ immersion $q:U\to N$ realising the identification. Lemma 3.27 (a milestone) guarantees such $N$ exists, so these statements are not vacuous. The induced field is not required to be C¹ and "Anosov" there means hyperbolicity of the whole manifold.
Useful reusable infrastructure: flows of C¹ vector fields on compact manifolds (with boundary), stable manifold theory, the λ-lemma, laminations and foliations of surfaces, and gluing of manifolds along boundary components.

Selected references

F. Béguin, C. Bonatti, B. Yu, Building Anosov flows on 3-manifolds, Geom. Topol. 21 (2017) 1837–1930. https://doi.org/10.2140/gt.2017.21.1837

59 thms2 active usersReviewed

Completed

Convex Optimization Linear Optimization Operations Research+1·Captain: mikedeng1

Linear Programming: Foundations and Extensions V: Convergence Rates of the Path-Following MethodTextbook

Motivation

Interior-point methods are, together with the simplex method, the standard algorithms for linear programming, and the primal–dual path-following method is the form in which they are implemented in most solvers. Unlike the simplex method, it is a one-phase method: it can start from any point whose primal and dual variables are strictly positive, feasible or not, and drives infeasibility and complementarity to zero simultaneously. The question every user of such a method eventually asks is how fast these three measures of non-optimality decrease.

Chapter 18 of R. J. Vanderbei, Linear Programming: Foundations and Extensions (4th ed., Springer 2014, DOI 10.1007/978-1-4614-7630-6) defines the method from scratch (Fig. 18.1, p. 273) and proves a rate statement, Theorem 18.1 (pp. 277–279): as long as the step lengths stay bounded below and the iterates stay bounded, the primal and dual infeasibilities decay geometrically, and so does the complementarity, at a slower rate. This mission formalizes that theorem and the one-step identities and estimates it is built from. It is the fifth mission of a series on the book; the missions are independent of each other.

Setting

Let $A$ be a real $m \times n$ matrix, $b \in \mathbb{R}^m$ , $c \in \mathbb{R}^n$ . The primal problem is to maximize $c^Tx$ subject to $Ax + w = b$ , $x, w \ge 0$ ; the dual is to minimize $b^Ty$ subject to $A^Ty - z = c$ , $y, z \ge 0$ . A primal–dual point is a quadruple $(x, w, y, z)$ with $x, z \in \mathbb{R}^n$ , $w, y \in \mathbb{R}^m$ ; it is strictly positive, $(x, w, y, z) > 0$ , if every component is. Write $X, W, Y, Z$ for the diagonal matrices of $x, w, y, z$ and $e$ for the all-ones vector. The norms are $\|v\|_1 = \sum_j |v_j|$ and $\|v\|_\infty = \max_j |v_j|$ .

At a point $(x, w, y, z)$ the three measures of progress are the primal infeasibility $\rho = b - Ax - w$ , the dual infeasibility $\sigma = c - A^Ty + z$ , and the complementarity $\gamma = z^Tx + y^Tw$ . Fix parameters $0 < \delta < 1$ and $0 < r < 1$ . One iteration of the method, from a strictly positive point, sets $\mu = \delta\gamma/(n+m)$ , takes any solution $(\Delta x, \Delta w, \Delta y, \Delta z)$ of the Newton system

A\Delta x + \Delta w = \rho, \quad A^T\Delta y - \Delta z = \sigma, \quad Z\Delta x + X\Delta z = \mu e - XZe, \quad W\Delta y + Y\Delta w = \mu e - YWe,

computes the step length

\theta = r\left(\max_{i,j}\left\{\left|\tfrac{\Delta x_j}{x_j}\right|, \left|\tfrac{\Delta w_i}{w_i}\right|, \left|\tfrac{\Delta y_i}{y_i}\right|, \left|\tfrac{\Delta z_j}{z_j}\right|\right\}\right)^{-1} \wedge 1 \qquad (18.7)

(with $\theta = 1$ when all ratios vanish), and moves to $(x + \theta\Delta x, w + \theta\Delta w, y + \theta\Delta y, z + \theta\Delta z)$ . This is Fig. 18.1 with the shorter step (18.7) the book adopts for its analysis. Along a sequence of iterates, superscripts $^{(k)}$ denote the quantities at the $k$ -th iterate, and $\theta^{(k)}$ is the step length computed there.

Formalization targets

Goal: Theorem 18.1 with the explicit constant

If $t > 0$ , $M$ is real, and for all $k \le K$ one has $\theta^{(k)} \ge t$ , $\|x^{(k)}\|_\infty \le M$ , $\|y^{(k)}\|_\infty \le M$ , then for all $k \le K$ , with $\tilde t = t(1-\delta)$ ,

\|\rho^{(k)}\|_1 \le (1-t)^k\|\rho^{(0)}\|_1, \qquad \|\sigma^{(k)}\|_1 \le (1-t)^k\|\sigma^{(0)}\|_1, \qquad \gamma^{(k)} \le (1-\tilde t)^k \left(\gamma^{(0)} + \frac{M(\|\rho^{(0)}\|_1 + \|\sigma^{(0)}\|_1)}{\delta t}\right).

Milestones

The one-step identities for the infeasibilities, $\tilde\rho = (1-\theta)\rho$ (18.8) and $\tilde\sigma = (1-\theta)\sigma$ (18.9); the one-step complementarity estimate

\tilde\gamma \le (1 - (1-\delta)\theta)\gamma + M\|\rho\|_1 + M\|\sigma\|_1 \qquad (18.10)

under $\|x\|_\infty, \|y\|_\infty \le M$ ; and the recursion $\gamma^{(k)} \le (1-\tilde t)\gamma^{(k-1)} + M(1-t)^{k-1}(\|\rho^{(0)}\|_1 + \|\sigma^{(0)}\|_1)$ (18.11). Two unnumbered statements complete the picture: every iteration has $0 < \theta \le 1$ and keeps the point strictly positive, and at any strictly positive point the duality gap satisfies $|b^Ty - c^Tx| \le \gamma + \|\sigma\|_1\|x\|_\infty + \|\rho\|_1\|y\|_\infty$ (§18.5.3).

Significance

Theorem 18.1 separates the convergence question for the path-following method into two parts: a rate statement that holds whenever steps stay long and iterates stay bounded, and the remaining question of when those two conditions hold. It also explains an effect seen in practice: the infeasibilities fall by the factor $1 - t$ per iteration while the complementarity, and hence (by the duality-gap estimate) the gap $b^Ty - c^Tx$ , falls only by $1 - \tilde t$ . The book stresses that the result is partial, because it does not show that the step lengths remain bounded away from zero; that requires modifications of the method and of the starting point that the book does not carry out.

All statements here are proved in the book. The mission's contribution is a machine-checked version, with the constant of the complementarity bound made explicit. Neither Mathlib nor the platform contains a formal proof of this theorem or a formalization of the infeasible-start primal–dual iteration it concerns; the platform's existing path-following result concerns a different, feasible-start short-step method in equality form.

Difficulty

The infeasibility identities are linear and follow from the first two Newton equations. The complementarity is where the Newton system linearizes a bilinear equation, so the new complementarity contains a second-order term $\theta^2(\Delta y^T\rho - \sigma^T\Delta x)$ that has no sign. Bounding it requires relating the size of the step $\theta\Delta$ to the size of the current iterate through the specific form of the step-length rule (18.7); the rule (18.6) of Fig. 18.1, with signed ratios, does not give such a bound. The multi-step estimate then couples two geometric sequences with different rates, and keeping the constant independent of the horizon $K$ is what makes the statement non-trivial.

Formalization scope

Vectors are Fin n → ℝ and Fin m → ℝ, $A$ is a Matrix (Fin m) (Fin n) ℝ, and points and step directions are a structure PDPoint m n with fields x w y z. The sup-norm is ⨆ j, |v j| (the maximum; 0 for an empty vector). The step length is written with the explicit case $\theta = 1$ when all ratios vanish, since Lean's r / 0 = 0 would otherwise give $\theta = 0$ . An iteration is a relation between the current point, a step direction and the next point: the current point is strictly positive, the direction is some solution of the Newton system (uniqueness, which the book asserts under a full-rank assumption, is not assumed), and the next point is current $+\ \theta \cdot$ direction. The hypotheses $0 < \delta < 1$ , $0 < r < 1$ (pp. 272–273) are stated in every theorem; $M$ is an arbitrary real number and $K$ a natural number. As in the book, the hypotheses of Theorem 18.1 range over $k \le K$ , so the iteration from index $K$ is part of the data.

Explicit constants. The book's Theorem 18.1 asserts only "there exists a constant $\bar M < \infty$ ". Because $K$ is fixed, that existential is satisfied trivially by $\max_{k \le K}\gamma^{(k)}/(1-\tilde t)^k$ , and a statement with $\exists \bar M$ would be empty. The goal therefore uses the constant the book's proof establishes (p. 279, last display): $\bar M = \gamma^{(0)} + M(\|\rho^{(0)}\|_1 + \|\sigma^{(0)}\|_1)/(\delta t)$ . Eq. (18.11) is stated with the book's $\tilde M = M(\|\rho^{(0)}\|_1 + \|\sigma^{(0)}\|_1)$ written out.

The formalization needs only finite sums, dot products and matrix–vector products from Mathlib; the definitions of the iteration are reusable for other analyses of the same method (Chapters 19–22 of the book). Contributions are welcome for each milestone separately.

Selected references

R. J. Vanderbei, Linear Programming: Foundations and Extensions, 4th ed., International Series in Operations Research & Management Science 196, Springer, 2014, Chapter 18, pp. 269–283. https://doi.org/10.1007/978-1-4614-7630-6
S. J. Wright, Primal-Dual Interior-Point Methods, SIAM, 1997. https://doi.org/10.1137/1.9781611971453

14 thms2 active usersReviewed

Completed

Combinatorics Graph Theory Linear Optimization+2·Captain: mikedeng1

Linear Programming: Foundations and Extensions III: Network Flows, the Integrality Theorem and König's TheoremTextbook

Motivation

Minimum-cost network flow problems are the largest special class of linear programs met in practice: transportation, distribution, assignment, communication and electric networks, facility location and financial planning all reduce to moving material along the arcs of a directed network from supply nodes to demand nodes at least cost. Chapter 14 of R. J. Vanderbei's Linear Programming: Foundations and Extensions (4th ed., Springer 2014, DOI 10.1007/978-1-4614-7630-6) develops the network simplex method, and closes with two structural facts that explain why this class is special: simplex bases are spanning trees of the network, and a network problem with integer supplies has integer basic solutions. Vanderbei then uses integrality to prove a classical theorem of combinatorics, König's theorem on regular bipartite graphs. Chapter 15, §5 treats the maximum-flow problem on the same objects and proves the Max-Flow Min-Cut Theorem.

The combinatorial results are older than linear programming. D. König proved in 1916 that every regular bipartite graph has a perfect matching (Math. Ann. 77). The Max-Flow Min-Cut Theorem is due to Ford and Fulkerson (1956, Canad. J. Math. 8) and, independently, Elias, Feinstein and Shannon (1956). The integrality of network bases is the total unimodularity of incidence matrices, known since the 1950s (Hoffman and Kruskal, 1956).

Setting

A network $(N,A)$ has a finite set $N$ of $m$ nodes and a set of directed arcs $A\subseteq\{(i,j): i,j\in N,\ i\ne j\}$ . Node $i$ carries a supply $b_i$ (negative values are demands) with $\sum_i b_i=0$ , and arc $(i,j)$ carries a cost $c_{ij}$ . The flow $x_{ij}$ on arc $(i,j)$ is the decision variable. The node–arc incidence matrix $A$ has in the column of $(i,j)$ an entry $+1$ in row $j$ , $-1$ in row $i$ , and $0$ elsewhere. The network flow problem (14.1) is

\text{minimize } c^{T}x\quad\text{subject to}\quad Ax=-b,\ x\ge 0 .

A flow satisfying $Ax=-b$ is balanced; a balanced flow with $x\ge0$ is feasible. Paths ignore arc directions; the network is connected if every two nodes are joined by a path, which is assumed throughout Chapter 14. A spanning tree is a set of arcs that, on all of $N$ and without directions, is connected and has no cycle. Fixing a root node $r$ and deleting its row gives the matrix $\tilde A$ . A set $T$ of arcs is a basis if its columns form an invertible square submatrix of $\tilde A$ , and a basic feasible solution is a feasible flow vanishing off some basis.

For maximum flow, a source $s$ , a sink $t$ and finite upper bounds $u_{ij}$ are given; all $b_i=0$ and an extra arc $(t,s)$ of infinite capacity is added. A feasible flow satisfies $0\le x_{ij}\le u_{ij}$ , $x_{ts}\ge0$ and flow balance. A cut is a node set $C$ with $s\in C$ , $t\notin C$ , and its capacity is $\kappa(C)=\sum_{(i,j)\in A,\ i\in C,\ j\notin C}u_{ij}$ .

Formalization targets

Goal: König's Theorem (Theorem 14.3, p. 216)

If $n$ girls and $n$ boys are such that every girl knows exactly $k\ge1$ boys and every boy knows exactly $k$ girls (knowing being symmetric), then there is a bijection $\sigma$ from girls to boys with

\text{girl } i \text{ knows boy } \sigma(i)\qquad\text{for all } i .

Milestones

Theorem 14.1 (p. 205): for a connected network, a set $T$ of arcs indexes a basis of $\tilde A$ if and only if $T$ is a spanning tree.
Theorem 14.2, Integrality Theorem (p. 216): with integer supplies, every basic feasible solution is integral,

x_{ij}\in\mathbb Z\qquad\text{for all }(i,j)\in A .

Eq. (15.8) (p. 234): $x_{ts}\le\kappa(C)$ for every feasible flow and every cut.
Theorem 15.1, Max-Flow Min-Cut (p. 234):

\max\{x_{ts}\}=\min_C \kappa(C),

both extrema attained.

The goal is independent of the network definitions in its statement; the milestones are the book's route to it (14.1, 14.2) and the chapter's other duality theorem on the same objects (15.8, 15.1).

Significance

König's theorem is the base case of matching theory: it gives perfect matchings in regular bipartite graphs, hence edge colourings of bipartite graphs with $\Delta$ colours, and via Birkhoff–von Neumann-type arguments the decomposition of doubly stochastic matrices. The Integrality Theorem is the reason assignment, transportation and shortest-path problems can be solved as linear programs without an integrality constraint. Theorem 14.1 is the correspondence the network simplex method is built on. Max-Flow Min-Cut is the prototype of combinatorial min–max theorems.

All four theorems are classical and proved. This mission adds machine-checked versions in the book's own formulation: the incidence matrix with Vanderbei's sign convention $Ax=-b$ , bases as square submatrices of $\tilde A$ with a chosen root, and maximum flow as a circulation through an added return arc. The platform already has network integrality, a tree-solution characterisation and max-flow min-cut in the Bertsimas–Tsitsiklis formulation and a Keller–Trotter max-flow statement; none is stated in this form, and Mathlib has Hall's marriage theorem but no regular-bipartite corollary.

Difficulty

The combinatorial content is small; the difficulty is in the passage between matrices and graphs. Theorem 14.1 needs both directions: the book shows that a spanning tree gives a triangularisable, hence invertible, submatrix and leaves the converse (independent columns form a spanning tree) as an exercise, which requires showing that any cycle, including a pair of antiparallel arcs, yields a linearly dependent set of columns and that $m-1$ acyclic arcs span. The book's proof of König's theorem applies the Integrality Theorem to the girl–boy network, which need not be connected, while Chapter 14 assumes connectedness throughout: the statement of 14.2 does not apply to it verbatim. The step "a feasible problem has a basic optimal solution" is also used and is not stated in the chapter.

Formalization scope

Nodes are a Fintype with decidable equality; arcs are a Finset (N × N), so parallel arcs are excluded as in the book, and IsNetwork excludes loops. Flows are real functions on ordered pairs; only their values on arcs matter.
"Connected" is preconnectedness of the undirected simple graph of the arcs; a spanning tree is an arc set whose undirected graph is a tree and in which no two arcs join the same pair of nodes.
A basis is $m-1$ linearly independent columns of the $(m-1)$ -row matrix $\tilde A$ , the same as an invertible square submatrix. The root $r$ is arbitrary, as in the book ("say, the last one").
Integer data means integer supplies; costs do not enter Theorem 14.2, since a basic optimal solution is a basic feasible solution.
In König's theorem both sides are Fin n, knowing is one relation between girls and boys, and $k\ge1$ is a hypothesis: the book's proof divides by $k$ , and for $k=0<n$ the claim is false. No connectedness is assumed.
For maximum flow, the return arc $(t,s)$ is a separate variable; $s\ne t$ and $u_{ij}\ge0$ are hypotheses that the book leaves implicit. Maximum and minimum are stated with attainment.
No statement involves a constant the book leaves implicit.

A formalization of the goal as a matching of size $n$ in some larger graph, or with the degree conditions on one side only, would be a different theorem; the conclusion is a bijection between exactly the $n$ girls and the $n$ boys using only acquainted pairs.

Useful infrastructure, reusable beyond this mission: the incidence matrix and its total unimodularity, the undirected graph of an arc set. Proofs of König's theorem through Hall's theorem (Mathlib Finset.all_card_le_biUnion_card_iff_exists_injective) are welcome alongside the book's route.

Selected references

R. J. Vanderbei, Linear Programming: Foundations and Extensions, 4th ed., Springer, 2014. DOI 10.1007/978-1-4614-7630-6
D. König, Über Graphen und ihre Anwendung auf Determinantentheorie und Mengenlehre, Math. Ann. 77 (1916), 453–465. DOI 10.1007/BF01456961
L. R. Ford and D. R. Fulkerson, Maximal flow through a network, Canad. J. Math. 8 (1956), 399–404. DOI 10.4153/CJM-1956-045-5
A. J. Hoffman and J. B. Kruskal, Integral boundary points of convex polyhedra, in Linear Inequalities and Related Systems, Ann. of Math. Studies 38, Princeton University Press, 1956, 223–246.

7 thms2 active usersReviewed

Completed

Markov Chain Operations Research Probability+1·Captain: mikedeng1

Stochastic Dynamic Programming and the Control of Queueing Systems XIV: Conforming Approximating Sequences for Markov ChainsTextbook

Motivation

Countable-state Markov chains are the standard model of queues with unbounded buffers, but any numerical computation of their long-run behaviour works on a finite state space. The usual remedy is truncation: restrict the chain to a finite set $S_N$ and redistribute the probability of leaving $S_N$ back into it. Whether the steady state probabilities and average costs of the truncated chains converge to those of the original chain depends on how that probability is redistributed. Gibson and Seneta studied this question for the stationary distributions of chains without costs (Gibson and Seneta, J. Appl. Prob., 1987). Sennott extended it to chains with costs and expected first passage costs (Sennott, Adv. Appl. Prob. 29, 1997; ZOR Math. Meth. Oper. Res. 45, 1997), and used it as the basis of the approximating sequence method for average-cost Markov decision chains (Sennott, 1999, Chapter 8). This mission covers Appendix C, Sections C.4–C.5 of the 1999 book, the Markov-chain results that the book's average-cost approximation theorems use.

Setting

A Markov chain with costs $\Gamma$ on a denumerable state space $S$ has transition probabilities $P_{ij}$ with $\sum_jP_{ij}=1$ and a finite nonnegative cost $C(i)$ at each state. For a set $G\subseteq S$ and a start $i$ , $T_{iG}\ge 1$ is the first passage time to $G$ . The taboo probability ${}_GP^{(t)}_{ik}$ is the probability of moving from $i$ to $k$ in $t$ steps with no intermediate state in $G$ . The expected visits ${}_Gu_{ik}$ count the visits to $k$ at times $0\le t<T_{iG}$ . The mean first passage time is $m_{iG}=E[T_{iG}]$ , infinite when $G$ is missed with positive probability. The first passage cost is $c_{iG}=E\big[\sum_{t<T_{iG}}C(X_t)\big]$ . A state $i$ is positive recurrent when $m_{ii}<\infty$ , and the steady state probability is $\pi_i=m_{ii}^{-1}$ . On a positive recurrent class $R$ the average cost is $J_R=\sum_{j\in R}\pi_jC(j)$ . The chain is $z$ standard when $m_{iz}<\infty$ and $c_{iz}<\infty$ for every $i$ . Such a chain has one positive recurrent class $R\ni z$ with $J_R<\infty$ , and every other state is transient.

An approximating sequence (AS) $(\Gamma_N)_{N\ge N_0}$ consists of increasing nonempty finite sets $S_N$ with $\bigcup_NS_N=S$ and, for each $N$ , a chain $\Gamma_N$ on $S_N$ with the same costs and transition probabilities $P_{ij}(N)\to P_{ij}$ . The quantities of $\Gamma_N$ are written $m_{iG}(N)$ , $c_{iG}(N)$ , $\pi_i(N)$ and $J(i)(N)$ . An AS is conforming (for a $z$ standard $\Gamma$ ) if, for large $N$ , $\Gamma_N$ is unichain with $z$ in its positive recurrent class, and $m_{iz}(N)\to m_{iz}$ and $c_{iz}(N)\to c_{iz}$ for all $i$ . It is conforming on $R$ if $\pi_i(N)\to\pi_i$ and $J(i)(N)\to J_R$ on $R$ .

An augmentation type approximating sequence (ATAS) keeps the original probabilities inside $S_N$ and redistributes the probability of each excluded target $r\notin S_N$ according to an augmentation distribution $q_\cdot(i,r,N)$ on $S_N$ :

P_{ij}(N)=P_{ij}+\sum_{r\in S-S_N}P_{ir}\,q_j(i,r,N),\qquad j\in S_N.

It sends excess probability to $G$ if every $q_\cdot(i,r,N)$ is concentrated on $G$ .

Formalization targets

Goal: Proposition C.5.2

For a $z$ standard chain $\Gamma$ and a finite nonempty $G\subseteq S$ ,

\text{every ATAS that sends excess probability to } G \text{ is conforming},

and if $G\subseteq R$ it is also conforming on $R$ . No rate of convergence and no constants are involved, and $G$ need not contain $z$ .

Milestones

Proposition C.4.2: for fixed $t$ , $\lim_N{}_GP^{(t)}_{ik}(N)={}_GP^{(t)}_{ik}$ ; also $\liminf_N{}_Gu_{ik}(N)\ge{}_Gu_{ik}$ and $\liminf_Nm_{iG}(N)\ge m_{iG}$ .
Proposition C.4.3: $\pi_i(N)\to0$ off the positive recurrent states, and along subsequences $\pi_i(N_s)\to b\pi_i$ on a class, with $0\le b\le1$ .
Proposition C.4.5: $\liminf_Nc_{iG}(N)\ge c_{iG}$ .
Proposition C.4.6: on a positive recurrent class, convergence of $\pi$ , of $m_{zz}$ and of all $m_{iG}$ are equivalent. Given these, convergence of $J(i)$ , of $c_{zz}$ and of all $c_{iG}$ are equivalent.
Proposition C.4.9: conformity implies $\pi_i(N)\to\pi_i$ for all $i$ , and that the constant average costs $J(N)$ of $\Gamma_N$ converge to $J_R$ .

Further results

Proposition C.5.3: an ATAS is conforming when, for $N\ge N^*$ , the augmentation distributions satisfy $\sum_{j\ne z}q_j(i,r,N)m_{jz}\le m_{rz}$ and $\sum_{j\ne z}q_j(i,r,N)c_{jz}\le c_{rz}$ .
Corollary C.5.4: for a $0$ standard chain on $\{0,1,2,\dots\}$ with an upper Hessenberg transition matrix, truncated to $S_N=\{0,\dots,N\}$ with the excess sent to $N$ , the ATAS is conforming.

Significance

The result. Conformity is the hypothesis under which the book's approximating sequence method works for average-cost queueing control (Chapter 8). The method computes optimal policies for finite truncations and passes to the limit. That argument needs the first passage times and costs to a distinguished state to converge along the chains induced by fixed policies. Propositions C.5.2 and C.5.3 turn this analytic requirement into conditions on the truncation scheme that can be checked in practice: send the overflow to a fixed finite set, or to states from which reaching $z$ is no more expensive. Examples C.4.4 and C.4.7 of the book show that an arbitrary approximating sequence can fail. The limit of the steady state probabilities can be a strict multiple $b\pi$ with $b<1$ . First passage costs can converge to the wrong value even when the steady state probabilities converge.

Formalizing it. The results are proved in the book, some in abbreviated form ("the proof for the costs is similar and is omitted"). The Prove2Me library had no statement on truncation or augmentation of countable Markov chains when this mission was drafted (September 2026). A formalization supplies the omitted cost arguments, makes the passage between $\liminf$ bounds and limits in $[0,\infty]$ explicit, and produces a reusable library of first passage quantities for countable chains.

Difficulty

The lower bounds of Propositions C.4.2 and C.4.5 are the routine part. The difficulty is the matching upper bound: in $\Gamma_N$ , a first passage that leaves $S_N$ is restarted elsewhere, which can lengthen it without bound. Taking limits termwise in the first passage equation $m_{iz}(N)=1+\sum_{j\ne z}P_{ij}(N)m_{jz}(N)$ fails, because no dominating function is available and mass can escape to infinity. Example C.4.4 exhibits exactly this. Unichain structure is also not automatic: $\Gamma_N$ may have several recurrent classes, or a recurrent class not containing $z$ , and ruling this out is part of the conclusion rather than an assumption.

Formalization scope

The Lean development works in SennottDP.ChainASM. A chain is a structure MC S with P : S → S → ℝ≥0∞, ∑' j, P i j = 1 and C : S → ℝ≥0. Theorems assume [Countable S] [Infinite S], matching the book's denumerable state space. Taboo probabilities, expected visits, $m_{iG}$ , $c_{iG}$ , $\pi_j=(m_{jj})^{-1}$ and $J_R=\sum_{j\in R}\pi_jC(j)$ are defined as sums in $[0,\infty]$ . $m_{iG}=\sum_{t\ge0}P(T_{iG}>t)$ is infinite whenever $G$ is missed with positive probability. The average cost $J(i)$ is the $\limsup$ of the Cesàro cost averages.

An AS is a structure carrying $N_0$ , the finite sets $S_N$ (as Finset S) and $P_{ij}(N)$ . $\Gamma_N$ is built as an MC on the subtype of $S_N$ , and a set $G$ is read in $\Gamma_N$ as $G\cap S_N$ . Quantities of $\Gamma_N$ are lifted to functions of $N$ and of states of $S$ with the value $0$ where they are undefined ( $N<N_0$ or a state outside $S_N$ ). For fixed states this affects finitely many $N$ , and all statements are limits, $\liminf$ s or eventual equalities. All convergence is in $[0,\infty]$ . The conformity predicate includes the standing assumption that $\Gamma$ is $z$ standard. The positive recurrent class $R$ of a $z$ standard chain is the communicating class of $z$ .

A trivializing formalization is excluded: the AS of Example C.4.4, whose positive recurrent class $\{N\}$ excludes $z=0$ , is not conforming under these definitions. The ATAS predicate requires the augmentation distributions to be probability distributions and to reproduce $P_{ij}(N)$ exactly by (C.27).

A complete development needs first passage decompositions for countable chains, the renewal-reward identity $J_R=c_{zz}/m_{zz}$ , and dominated and Fatou-type limit theorems for sums (the book's Appendix A). The first passage library and the lifted-quantity conventions can be reused by the average-cost approximation chapters. Contributions of intermediate lemmas are welcome, especially the finite-state unichain facts of Section C.3 and the identities of Propositions C.1.4 and C.2.2.

Proposition C.5.5 (lower Hessenberg chains, from Gibson and Seneta) is stated in the book without proof and without naming the distinguished state, and is not included.

Selected references

L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley, 1999, Appendix C, Sections C.4–C.5. https://doi.org/10.1002/9780470317037
L. I. Sennott, "The computation of average optimal policies in denumerable state Markov decision chains", Advances in Applied Probability 29 (1997) 114–137 (cited in the book as Sennott 1997a).
L. I. Sennott, "On computing average cost optimal policies with application to routing to parallel queues", ZOR Mathematical Methods of Operations Research 45 (1997) 45–62 (cited in the book as Sennott 1997b).
D. Gibson and E. Seneta, "Augmented truncations of infinite stochastic matrices", Journal of Applied Probability (1987).

10 thms2 active usersReviewed

Completed

Algorithmic Game Theory Combinatorics Operations Research·Captain: mikedeng1

Theory of Games and Economic Behavior VI: Splitting Sets and the Decomposition Partition of a GameTextbook

Motivation

Chapter IX of von Neumann and Morgenstern's Theory of Games and Economic Behavior asks when a game played by many participants is really several separate games played side by side. The authors' motivation (41.1) is methodological: the general theory of the $n$ -person game becomes unmanageable as $n$ grows, and one way to gain insight into large games is to isolate classes of games that can be analysed exactly. The first such class consists of games whose players fall into groups that have no dealings with each other — the book's example is the internal economies of two countries whose connections are disregarded (41.2.4). Such a game is the composition of its constituents, and the question of the chapter is how to recognise a composite game from its characteristic function alone and how far a given game can be decomposed.

The answer (§43) is a structure theorem. The groups of players that can be split off form a Boolean algebra of sets; its atoms, the minimal splitting sets, form a partition of the set of players, the decomposition partition $\Pi_\Gamma$ ; and every splitting set is a union of blocks of $\Pi_\Gamma$ . The book remarks (41.3.3) that the splitting condition (41:7) is exactly Carathéodory's criterion of measurability, transported from measures to characteristic functions. The mission formalizes §43, together with the criterion (42:G) of §42 on which it rests.

Setting

Let $I$ be a finite set of players. A characteristic function is a real number $v(S)$ for every subset $S \subseteq I$ (every coalition, including the empty set $\ominus$ and $I$ ). Write $-S = I - S$ . From 42.4.1 on the book works in the domain of constant-sum games, whose characteristic functions are, by (42:D), exactly the functions satisfying

\text{(42:6:a)}\ v(\ominus) = 0,\qquad \text{(42:6:b)}\ v(S) + v(-S) = v(I),\qquad \text{(42:6:c)}\ v(S) + v(T) \leqq v(S \cup T)\ \text{ if } S \cap T = \ominus .

For $J \subseteq I$ with complement $K = I - J$ , the game is decomposable with respect to $J$ and $K$ if there are constant-sum games $\Delta$ on the players $J$ and $\mathrm H$ on the players $K$ with $v(R) = v_\Delta(R \cap J) + v_{\mathrm H}(R \cap K)$ for all $R \subseteq I$ — formula (41:3). The $J$ -constituent $\Delta$ is the game on $J$ with $v_\Delta(S) = v(S)$ for $S \subseteq J$ (41:4).

A splitting set (43.1) is a $J \subseteq I$ satisfying (41:6),

v(S \cup T) = v(S) + v(T) \quad \text{for } S \subseteq J,\ T \subseteq I - J .

The game is indecomposable if $\ominus$ and $I$ are its only splitting sets (43.3.1). A minimal splitting set is a splitting set $J \neq \ominus$ none of whose proper subsets $J' \neq \ominus$ is splitting (43.3.2), and $\Pi_\Gamma$ is the system of all minimal splitting sets. The game is inessential (42:F) if it is strategically equivalent to the zero game, i.e. $v(S) + \sum_{k \in S} \alpha^0_k = 0$ for all $S$ , for some reals $\alpha^0_k$ (the transformation (42:5)).

Formalization targets

Goal: (43:F), (43:G), (43:H)

For every $v$ satisfying (42:6:a)–(42:6:c):

J_1 \neq J_2 \in \Pi_\Gamma \Rightarrow J_1 \cap J_2 = \ominus, \qquad \bigcup_{J \in \Pi_\Gamma} J = I, \qquad K \text{ splitting} \iff K = J_1 \cup \dots \cup J_p,\ J_i \in \Pi_\Gamma .

The goal combines the partition property and the characterization of all splitting sets; it is the book's own summary of §43.3 and does not presuppose that $\Pi_\Gamma$ is a partition.

Milestones

In attack order: the criterion (42:G) (decomposability $\iff$ (41:6) $\iff$ (41:7)); the closure properties (43:A) (complements), (43:B) ( $\ominus$ , $I$ ), (43:C) (intersections and unions); (43:D) (splitting sets of a constituent) and (43:E) (a constituent is indecomposable iff its set is minimal); (43:F), (43:G) separately; (43:I) (a minimal splitting set is disjoint from, or inside, any splitting set); the restatement (43:H*) ( $K$ splits iff every block of $\Pi_\Gamma$ lies inside or outside $K$ ); and the two extreme cases (43:J) ( $\Pi_\Gamma$ = all singletons iff the game is inessential) and (43:K) ( $\Pi_\Gamma = \{I\}$ iff the game is indecomposable).

Significance

The decomposition partition is canonical: every constant-sum game splits uniquely into indecomposable constituents, and (43:E) identifies them as the constituents on the blocks of $\Pi_\Gamma$ . The two extreme cases (43:J), (43:K) show that inessentiality and indecomposability are opposite ends of one scale. Chapter IX uses this structure in §§44–47, where solutions of decomposable games are related to solutions of their constituents ((46:A)–(46:I)); a formal decomposition partition is the prerequisite for that later work, and a candidate follow-up mission.

The results are classical and proved in the book. The mission's contribution is a machine-checked version: a formal definition layer for splitting sets of a set function on a finite set, the Boolean-algebra closure, and the atomic decomposition. The combinatorial core — that the sets satisfying a Carathéodory-type additivity condition form a Boolean algebra of a finite set, whose atoms partition it — is reusable outside game theory (for instance for finitely additive decompositions of set functions). No machine-checked version of these results is known to exist; they are formalized here for the first time as far as a search of the platform shows.

Difficulty

The individual steps are elementary, but the obvious argument for the key closure property (43:C) fails: to show that $J' \cup J''$ is splitting one cannot simply add the identities (41:6) for $J'$ and for $J''$ , since a pair $S \subseteq J' \cup J''$ , $T \subseteq I - (J' \cup J'')$ is not of the form those identities control, and $J' \cap J''$ may be nonempty — the book's footnote on p. 354 singles out overlapping splitting sets as the case its proof is really about. Likewise (43:D) is not a tautology: that a set self-contained within a self-contained set is self-contained in the whole game has to be proved (footnote 1, p. 355). Formally, the main work is bookkeeping of set identities and the passage between subsets of $J$ (players of the constituent) and subsets of $I$ .

Formalization scope

Players. The set of players $I$ is an arbitrary finite type ι with decidable equality (the book's $I = (1, \dots, n)$ ; in Chapter IX players are also named $1', \dots, k', 1'', \dots, l''$ ). Coalitions are Finset ι, $-S$ and $I - J$ are the complement Sᶜ in $I$ , and $v$ is a function Finset ι → ℝ.
Standing hypotheses. Every theorem assumes (42:6:a)–(42:6:c) (the structure IsConstantSum), the chapter's domain from 42.5.3 on ("in the remainder of this chapter we will continue to consider constant-sum games", p. 353). $v(I)$ is arbitrary: the statements are not restricted to zero-sum games, which would be a weaker special case. (43:K) additionally assumes $I$ nonempty ([Nonempty ι], the book's $n \geqq 1$ ); every other statement holds without it. (43:E) assumes $J \neq \ominus$ , since the book's constituent is a game and has at least one player.
Characteristic functions only. Games are represented by their characteristic functions, as the book does throughout §§42–43 by (42:D). Decomposability quantifies over constant-sum characteristic functions $v_\Delta$ , $v_{\mathrm H}$ on the subtypes ↥J, ↥Jᶜ; the $J$ -constituent is $v$ restricted to subsets of ↥J. Sums of sets are unions; "disjunct" is Disjoint.
Π_Γ. decompositionPartition v is the set of minimal splitting sets; that it is a partition is proved, not assumed. An aggregate of minimal splitting sets is a finite family A, its sum A.sup id; the empty aggregate gives $\ominus$ .
No trivialization. A definition of splitting sets that quantified over $T \subseteq I$ instead of $T \subseteq I - J$ , or complements taken in an ambient type larger than $I$ , would change the theorems; here the complement is in the finite type of players itself. With $I$ empty all statements except (43:K) hold trivially, and (43:K) carries the nonemptiness hypothesis.
Contributions welcome. Proofs of the milestones in the listed order; general Mathlib-style lemmas on Boolean subalgebras of Finset ι and their atoms, which would shorten (43:F)–(43:H).

Selected references

J. von Neumann and O. Morgenstern, Theory of Games and Economic Behavior, 60th-anniversary edition, Princeton University Press, 2007 (page-for-page reprint of the 3rd edition, 1953), Chapter IX, §§41–43, pp. 339–357. https://doi.org/10.1515/9781400829460
C. Carathéodory, Vorlesungen über reelle Funktionen, Teubner, Leipzig–Berlin, 1918, Chapter V (the measurability criterion to which (41:7) corresponds, cited by the book on p. 343).

16 thms2 active usersReviewed

Completed

Convex Optimization Information Theory Linear algebra+2·Captain: naimengye

Decoding by Linear Programming: Exact Recovery by ℓ1 Minimization under the Restricted Isometry ConditionResearch Paper

Motivation

Consider the classical error-correcting problem. An input vector $f \in \mathbb{R}^n$ (the plaintext) is encoded as $Af \in \mathbb{R}^m$ by a coding matrix $A$ with $m > n$ , and an unknown, arbitrary vector of errors $e$ corrupts the result, so that only $y = Af + e$ is observed. Can $f$ be recovered exactly, and by an algorithm whose running time is polynomial in $m$ ? Candès and Tao (2005) answer both questions at once: if a matrix $F$ annihilating $A$ satisfies a restricted orthonormality condition, then $f$ is the unique solution of the convex program $\min_g \|y - Ag\|_{\ell^1}$ , which is a linear program, whenever at most $S$ entries of $y$ are corrupted, whatever their positions and values. Read for the matrix $F$ alone, the same theorem says that $\ell^1$ minimization (basis pursuit) returns the sparsest solution of an underdetermined linear system. That statement is the mathematical core of compressed sensing, and the restricted isometry constants introduced in this paper became the standard tool of the field.

Timeline. Donoho and Huo (2001), followed by Elad–Bruckstein, Donoho–Elad and Gribonval–Nielsen, proved the equivalence of $\ell^0$ and $\ell^1$ minimization for matrices formed by concatenating two orthonormal bases, for sparsity of order $\sqrt{m}$ , through incoherence. Candès, Romberg and Tao (2004) and Candès and Tao (2004) obtained recovery with overwhelming probability for random matrices at sparsity of order $m/\log m$ . Donoho (2004) showed for Gaussian matrices that a constant, unspecified fraction $\rho m$ of nonzero entries can be tolerated. The present paper (December 2004, published 2005) gives a deterministic sufficient condition, $\delta_S + \theta_{S,S} + \theta_{S,2S} < 1$ , valid for every matrix, and specializes it to Gaussian matrices with explicit numerical values of the tolerable fraction. Later work, for instance Candès (2008) with the condition $\delta_{2S} < \sqrt{2} - 1$ , sharpened the sufficient condition; those later results are not part of this mission.

Setting

Let $F$ be a real $p \times m$ matrix with columns $v_1, \dots, v_m \in \mathbb{R}^p$ , and let $H$ be the linear span of these columns. For an index set $T \subseteq \{1,\dots,m\}$ and real coefficients $c = (c_j)_{j \in T}$ , write $F_T c = \sum_{j \in T} c_j v_j$ . A vector $c \in \mathbb{R}^m$ is supported on $T$ when $c_j = 0$ for all $j \notin T$ ; with this convention $F_T c$ is just the product $Fc$ . Norms are the Euclidean norm $\|c\| = (\sum_j c_j^2)^{1/2}$ and the $\ell^1$ norm $\|c\|_{\ell^1} = \sum_j |c_j|$ .

Definition 1.1. For an integer $S$ , the $S$ -restricted isometry constant $\delta_S$ is the smallest quantity such that

(1 - \delta_S)\|c\|^2 \le \|F_T c\|^2 \le (1 + \delta_S)\|c\|^2

for all $T$ of cardinality at most $S$ and all real coefficients $(c_j)_{j \in T}$ . The $S, S'$ -restricted orthogonality constant $\theta_{S,S'}$ is the smallest quantity such that

|\langle F_T c, F_{T'} c' \rangle| \le \theta_{S,S'} \, \|c\| \, \|c'\|

for all disjoint $T, T'$ with $|T| \le S$ and $|T'| \le S'$ . The paper writes $\theta_S$ for $\theta_{S,S}$ . These numbers measure how far the columns of $F$ are from an orthonormal system when only linear combinations of at most $S$ columns are considered.

The two optimization problems are

(P_1)\quad \min_{d \in \mathbb{R}^m} \|d\|_{\ell^1} \ \text{ subject to } \ Fd = f, \qquad\qquad (P_1')\quad \min_{g \in \mathbb{R}^n} \|y - Ag\|_{\ell^1}.

A vector is the unique minimizer of one of these problems when it is feasible and every other feasible vector has a strictly larger objective value.

Formalization targets

Goal: Theorem 1.5 (decoding by linear programming)

Let $A$ be a real $m \times n$ matrix of full rank with $m > n$ , and $F$ a real $p \times m$ matrix with $FA = 0$ . Let $S \ge 1$ satisfy

\delta_S(F) + \theta_{S,S}(F) + \theta_{S,2S}(F) < 1 . \tag{1.10}

If $y = Af + e$ where $e$ is supported on a set of size at most $S$ , then $f$ is the unique minimizer of $(P_1')$ .

Core: Theorem 1.4 (exact recovery by $\ell^1$ minimization)

Let $S \ge 1$ satisfy (1.10) for $F$ , and let $c$ be supported on a set $T$ with $|T| \le S$ . Then $c$ is the unique minimizer of $(P_1)$ with $f := Fc$ .

Theorem 1.5 is the companion of Theorem 1.4 for the decoding problem, and the mission's milestones are the four lemmas the paper proves on the way: Lemma 1.2 (the $\delta$ numbers control the $\theta$ numbers), Lemma 1.3 (uniqueness of sparse representations under $\delta_{2S} < 1$ ), and the two dual sparse reconstruction properties, Lemma 2.1 ( $\ell^2$ version) and Lemma 2.2 ( $\ell^\infty$ version).

Significance

The result. The guarantee is deterministic and uniform: one condition on $F$ , checkable in principle from the matrix alone, ensures that a single linear program recovers every sufficiently sparse vector, with no probability of failure. In the decoding reading, a fixed fraction of the ciphertext can be corrupted arbitrarily and the plaintext is still recovered exactly by convex optimization. The paper shows in its Section 3 that Gaussian matrices satisfy (1.10) with overwhelming probability at explicit values of $S/m$ , and in Section 5 that the same hypothesis yields near-optimal recovery of compressible signals from few measurements; both are consequences of the deterministic core formalized here.

Formalizing it. The theorems are proved in the paper, and no machine-checked proof of them exists. Prove2Me holds a formalization of a different restricted-isometry sufficient condition taken from a textbook (HighDimProb.SparseRecovery.rip_implies_exact_recovery); it uses a different definition of the isometry constant and a different hypothesis, so nothing there can be reused as is. This mission produces the definitions of $\delta_S$ and $\theta_{S,S'}$ exactly as in Definition 1.1, the dual-certificate lemmas, and the two theorems, in a form that later missions on compressed sensing can import. The probabilistic Theorem 1.6, Lemma 3.1 and Corollary 1.7, and the compressible-signal Theorem 5.1, are not targets: see the scope section for why.

Difficulty

The whole proof rests on a dual certificate: a vector $w \in H$ with $\langle w, v_j \rangle = \operatorname{sgn}(c_j)$ for $j \in T$ and $|\langle w, v_j \rangle| < 1$ for $j \notin T$ . Given such a $w$ , the argument of Section 2.2 is a short chain of inequalities. The first idea every newcomer has is $w = F_T (F_T^* F_T)^{-1} \operatorname{sgn}(c)$ ; this interpolates the signs on $T$ and, by restricted orthogonality, its inner products off $T$ are small in an $\ell^2$ sense, but not in the $\ell^\infty$ sense required. That is exactly Lemma 2.1: the $\ell^\infty$ bound holds only outside an exceptional set of at most $S'$ indices. Lemma 2.2 removes the exceptional set by an infinite alternating iteration, prescribing values on the previous exceptional set while keeping the values on $T$ fixed, and summing a geometrically convergent series.

Two points deserve attention from solvers. First, the paper's proof of Lemma 2.2 prescribes values on sets of size up to $2S$ ( $T_0 \cup T_n$ ) at each step, while the per-step factors it quotes, $\theta_{S,2S}/(1-\delta_S)$ , are what Lemma 2.1 gives for a set of size $S$ ; a proof of the printed constant in (2.4) has to account for this, and the hypothesis of Theorem 1.4 leaves room for a proof with slightly worse per-step factors. Second, Lemma 2.1 is printed with $\theta_S$ in its $\ell^2$ bound on the exceptional set, while the inequality (2.3) its proof establishes gives $\theta_{S,S'}$ ; the mission states the lemma with $\theta_{S,S'}$ , which coincides with the printed form in the case $S' = S$ used by Lemma 2.2.

Formalization scope

Matrices are Matrix (Fin p) (Fin m) ℝ; a coefficient vector on $T$ is a vector in Fin m → ℝ supported on the finite set $T$ , and $F_T c$ is F.mulVec c. The Euclidean and $\ell^1$ norms and the inner product are explicit finite sums, so every statement can be checked by hand against the paper. $H$ is the span of the columns.

The constants $\delta_S$ and $\theta_{S,S'}$ are the infimum of the set of nonnegative $\delta$ (resp. $\theta$ ) satisfying the defining inequalities for all admissible sets and coefficients. This set is nonempty, closed and bounded below, so the infimum is attained and is the paper's smallest quantity; on the paper's domain the smallest such quantity is nonnegative, so the extra clause only fixes a harmless value in degenerate cases such as $S = 0$ . The definitions are total in $S, S'$ , and each theorem carries the paper's domain conditions ( $S \ge 1$ , and $2S \le m$ , $3S \le m$ or $S + S' \le m$ as needed) as explicit hypotheses. The hypotheses are satisfiable, since a matrix with orthonormal columns has $\delta_S = \theta_{S,S'} = 0$ , so none of the statements is vacuous.

"Unique minimizer" is a strict inequality against every competitor. "Full rank" for the $m \times n$ matrix $A$ with $m > n$ is injectivity of $g \mapsto Ag$ ; both are standing assumptions of the paper's Section 1.1 and appear as hypotheses of Theorem 1.5. In Lemma 2.1, "a constant $K > 0$ depending only on $\delta_S$ " is a positive function of the real number $\delta_S$ , quantified before all other data.

Out of scope, with the reason for each: Theorem 1.6 refers to a threshold $r^*(p,m)$ "given in Section 3.5", which the paper does not contain, and to "overwhelming probability" with unspecified constants; Lemma 3.1 is proved only for $m$ and $p$ "large enough", with an unspecified threshold and an $o(1)$ term quoted from the literature; Corollary 1.7 rests on Theorem 1.6; Theorem 5.1 has an unspecified constant $C$ and is explicitly not proved in the paper. A future mission can add these once precise statements are fixed.

Contributions that are welcome: proofs of the four milestone lemmas and of the two theorems; reusable lemmas on the attainment and monotonicity of the constants, on the Gram matrix $F_T^* F_T$ and its inverse under $\delta_S < 1$ , and on the duality inequality of Section 2.2. Statements that weaken the hypotheses (for instance to $\delta_{2S} < \sqrt{2} - 1$ ) belong to a separate mission.

Selected references

E. J. Candès and T. Tao, Decoding by linear programming, IEEE Trans. Inform. Theory 51 (12), 2005, 4203–4215. https://doi.org/10.1109/TIT.2005.858979 (arXiv: https://arxiv.org/abs/math/0502327)
E. J. Candès, J. Romberg and T. Tao, Robust uncertainty principles: exact signal reconstruction from highly incomplete frequency information, IEEE Trans. Inform. Theory 52 (2), 2006. https://arxiv.org/abs/math/0409186
E. J. Candès and T. Tao, Near optimal signal recovery from random projections: universal encoding strategies?, IEEE Trans. Inform. Theory 52 (12), 2006. https://arxiv.org/abs/math/0410542
D. L. Donoho and X. Huo, Uncertainty principles and ideal atomic decomposition, IEEE Trans. Inform. Theory 47, 2001, 2845–2862. https://doi.org/10.1109/18.959265
S. S. Chen, D. L. Donoho and M. A. Saunders, Atomic decomposition by basis pursuit, SIAM J. Sci. Comput. 20, 1999, 33–61. https://doi.org/10.1137/S1064827596304010
E. J. Candès, The restricted isometry property and its implications for compressed sensing, C. R. Acad. Sci. Paris, Ser. I 346, 2008, 589–592. https://doi.org/10.1016/j.crma.2008.03.014

9 thms2 active usersReviewed

Completed

Dynamic Programming Dynamical Systems Optimization·Captain: Lucas

Lindgren 2022: Dynamic-Programming Price Adjustment and Lyapunov StabilityResearch Paper

Motivation

In a Walrasian pure exchange economy, agents trade a fixed stock of $l$ commodities, and a price vector $p\in\mathbb R^l$ is a general equilibrium when aggregate excess demand vanishes. Existence of equilibrium (Arrow–Debreu, 1954) says nothing about how prices reach it. The classical tâtonnement model of Samuelson (1947), $dp_i/ds = c_i Z_i(p)$ , is not derived from any optimization principle, and Scarf (1960) gave economies in which it is not globally stable; see also Smale's survey Dynamics in General Equilibrium Theory (JSTOR 1817235) and the chaotic tâtonnement examples of Bala–Majumdar (JSTOR 25054664).

Lindgren (doi:10.3390/analytics1010003) proposes instead that the economy as a whole chooses a price path by dynamic programming: it minimizes a running cost combining a quadratic transaction cost for price changes and the agents' aggregate minimal expenditure. From the resulting Hamilton–Jacobi–Bellman (HJB) equation the paper derives an evolution equation for the price velocity and a condition under which the value function acts as a Lyapunov function: the equilibrium is approached when price adjustments are large enough. This mission formalizes those derivations.

Setting

There are $l$ commodities and $n$ agents. Prices are vectors $p=(p_1,\dots,p_l)\in\mathbb R^l$ , and the paper's implicit summation $x^iy_i=\sum_{i=1}^l x_iy_i$ is written $\langle x,y\rangle$ . Agent $j$ has an expenditure function $e_j(p)$ (minimal cost of reaching a fixed utility level), and the market weighs agents with constants $\lambda_j>0$ ; the aggregate expenditure is

E(p)=\lambda^je_j(p)=\sum_{j=1}^n\lambda_je_j(p).

The economy controls the price velocity $v=dp/ds$ and minimizes the cost functional (eq. (7))

\int_t^T\Big(\tfrac12 m\langle v,v\rangle+E(p)\Big)\,ds,\qquad m>0,

whose value function is $J(t,p)$ . The Hamiltonian (eq. (8)) is

H(v)=\tfrac12 m\langle v,v\rangle+E(p)+\langle\nabla J,v\rangle ,

the optimal policy (eq. (9)) is $v=-\tfrac1m\nabla J$ , and the HJB equation (eq. (10)) reads

\frac{\partial J}{\partial t}=\frac1{2m}\langle\nabla J,\nabla J\rangle-E(p).

Here $\nabla$ always denotes the gradient with respect to prices. Shephard's lemma identifies the Hicksian demand of agent $j$ with $h^j=\nabla e_j$ . For the stability analysis the paper runs time forward, which reverses the sign of the HJB equation: $\partial J/\partial s=-\frac1{2m}\langle\nabla J,\nabla J\rangle+E(p)$ .

Formalization targets

Goal — Lyapunov stability condition (Section 3)

If $J$ is $C^1$ and solves the time-reversed HJB equation, and the price path follows the optimal policy $\dot p(s)=v(s)=-\frac1m\nabla J(s,p(s))$ , then on any interval $[t,T]$ on which

E(p(s))<\tfrac32\,m\,\langle v(s),v(s)\rangle,

the function $s\mapsto J(s,p(s))$ is strictly decreasing; if moreover $J(T,p(T))=0$ , it is strictly positive on $[t,T)$ .

Milestones

Eq. (4): under the normalization $\langle p,p\rangle=1$ , $\langle p,\dot p\rangle=0$ .
Eq. (9): for $m>0$ , $v$ minimizes $H$ if and only if $mv=-\nabla J$ .
Eq. (10): the HJB equation $-\partial_tJ=\min_vH$ takes the explicit form above.
Eq. (12): for a $C^2$ solution of (10), $v=-\frac1m\nabla J$ satisfies

m\frac{\partial v_i}{\partial t}+\tfrac12 m\,\nabla_i\langle v,v\rangle=\nabla_iE .

Eq. (14): with Shephard's lemma, the right-hand side becomes $\sum_j\lambda_jh^j_i$ .
Eq. (19): along the optimal path, $\dfrac{dJ}{ds}=E(p)-\tfrac32 m\langle v,v\rangle$ .

Significance

The paper's contribution is the claim that price dynamics derived from an optimization principle are nonlinear and only conditionally stable, with stability requiring sufficiently fast price changes; the author connects this to volatility clustering in financial time series. The derivations in the paper are formal calculations with the regularity of $J$ left implicit. Formalizing them pins down exactly which smoothness assumptions each step needs (for instance, eq. (12) uses equality of mixed partial derivatives, hence a $C^2$ value function), and which facts are imported from outside (the HJB equation itself, Shephard's lemma). The resulting statements are reusable calculus facts about HJB equations with quadratic control cost.

Difficulty

Each step is a short computation on paper; the formal difficulty is in the calculus infrastructure: partial derivatives of functions on $\mathbb R\times\mathbb R^l$ , symmetry of second derivatives, the chain rule along a curve, and turning a pointwise negative derivative into strict monotonicity on a closed interval. The HJB equation is taken as a hypothesis on $J$ rather than derived from the definition of the value function, because the paper asserts it without proof and a rigorous derivation would require viscosity-solution theory.

Formalization scope

All declarations live in the namespace LindgrenPriceDynamics. Prices are functions Fin l → ℝ; partial derivatives are Fréchet derivatives applied to standard basis vectors, and time derivatives are one-variable derivatives in the time argument. The value function is a function J : ℝ → (Fin l → ℝ) → ℝ whose joint regularity is stated for the uncurried map on ℝ × (Fin l → ℝ). The standing assumption $m>0$ is kept; positivity of $\lambda_j$ and $e_j$ is not needed by any stated conclusion and is not imposed. Prices are not restricted to the positive orthant. The goal's large-velocity hypothesis is satisfiable (e.g. $l=1$ , $J=ap^2+cs$ , $E=2a^2p^2/m+c$ with small $c>0$ on a bounded interval), so the goal is not vacuous.

Selected references

J. Lindgren, General Equilibrium with Price Adjustments — A Dynamic Programming Approach, Analytics 1 (2022) 27–34. https://doi.org/10.3390/analytics1010003
S. Smale, Dynamics in General Equilibrium Theory, American Economic Review 66 (1976) 288–294. https://www.jstor.org/stable/1817235
H. Scarf, Some Examples of Global Instability of the Competitive Equilibrium, International Economic Review 1 (1960) 157–172.
A. Mas-Colell, M. Whinston, J. Green, Microeconomic Theory, Oxford University Press, 1995.
V. Bala, M. Majumdar, Chaotic Tatonnement, Economic Theory 2 (1992) 437–445. https://www.jstor.org/stable/25054664

8 thms2 active usersReviewed

Algebra Analysis·Captain: Lucas

Smale's Mean Value ConjectureOpen Problem

Motivation

The mean value problem, also called Smale's mean value conjecture, was posed by Stephen Smale in 1981 in his study of the complexity of root-finding algorithms for polynomials (Smale 1981). For a real differentiable function the mean value theorem produces, between two points, a point where the derivative equals a difference quotient. For a complex polynomial no such point need exist on a segment, and Smale asked for a substitute in which the special point is a critical point of the polynomial (a zero of its derivative). Estimates of this kind control how far Newton-type iterations can move, which is where Smale's original interest came from. The problem appears in lists of unsolved problems in mathematics, including Smale's own list of problems for the next century.

Timeline

1981 — Smale poses the problem and proves the inequality below with constant $K = 4$ (Smale 1981). The example $P(z) = z^d - dz$ shows that the constant cannot be smaller than $\frac{d-1}{d}$ in degree $d$ , so no constant below $1$ works in all degrees.
1989 — Tischler proves the inequality with the optimal constant $K = \frac{d-1}{d}$ when all roots of $P$ are real, and when all roots of $P$ have the same absolute value (Tischler 1989).
2007 — Conte, Fujikawa and Lakic prove $K \le 4\frac{d-1}{d+1}$ (Conte–Fujikawa–Lakic 2007). Crane proves $K < 4 - \frac{2.263}{\sqrt d}$ for $d \ge 8$ (Crane 2007).
2009 — Dubinin and Sugawa prove the reverse (dual) inequality with constant $\frac{1}{d\,4^d}$ (Dubinin–Sugawa 2009); optimizing this lower bound is the dual mean value problem (Ng–Zhang 2016).

No absolute constant $K < 4$ is known that works in every degree.

Setting

Let $P$ be a polynomial with complex coefficients of degree $d \ge 2$ , and write $P'$ for its derivative. A critical point of $P$ is a complex number $c$ with $P'(c) = 0$ ; since $d \ge 2$ , $P'$ is a nonconstant polynomial of degree $d-1$ , so $P$ has at least one and at most $d-1$ distinct critical points. Fix a complex number $z$ that is not a critical point, $P'(z) \ne 0$ . For every critical point $c$ we then have $c \ne z$ , and the difference quotient

\frac{P(z) - P(c)}{z - c}

is well defined. The question is how small this quotient can be made, relative to $|P'(z)|$ , by choosing the critical point $c$ well.

Formalization targets

Goal: Smale's mean value conjecture ( $K = 1$ )

For every complex polynomial $P$ of degree $d \ge 2$ and every $z \in \mathbb C$ with $P'(z) \ne 0$ there is a critical point $c$ of $P$ with

\left| \frac{P(z) - P(c)}{z - c} \right| \le |P'(z)|.

Stronger: the optimal constant

The same with $|P'(z)|$ replaced by $\frac{d-1}{d}\,|P'(z)|$ ; the example $z^d - dz$ shows this constant cannot be lowered.

Known results (milestones)

Smale's inequality with $K = 4$ .
The extremal example $P(z) = z^d - dz$ at $z = 0$ , where every critical point gives exactly $\frac{d-1}{d}|P'(0)|$ , and its consequence that no constant $K < 1$ works in all degrees.
Tischler's optimal inequality for polynomials with only real roots, and for polynomials whose roots all have the same absolute value.
The Conte–Fujikawa–Lakic bound $K \le 4\frac{d-1}{d+1}$ .
Crane's bound $K < 4 - \frac{2.263}{\sqrt d}$ for $d \ge 8$ .
The Dubinin–Sugawa dual inequality $\left|\frac{P(z)-P(c)}{z-c}\right| \ge \frac{|P'(z)|}{d\,4^d}$ for some critical point $c$ .

Significance

The result itself. A positive answer gives a sharp, degree-independent mean value inequality for complex polynomials: for every non-critical point, some critical value is reachable along a chord whose slope is at most the local derivative. Bounds of this type feed into the analysis of Newton's method and of path-following root finders, and into the study of how critical values of a polynomial are distributed relative to its values. The conjecture is part of a family of open extremal problems on the geometry of critical points, alongside Sendov's conjecture.

Formalizing it. The goal and the optimal-constant form are open. The milestones are published theorems, none of which is known to have a machine-checked proof. Formalizing Smale's $K = 4$ bound and Tischler's special cases would put the classical tools of the subject (critical points of polynomials, univalent function estimates, root location) on a formal footing that later attempts can reuse.

Difficulty

The obvious strategies control the quotient through one critical point at a time: for instance, bounding $|P(z) - P(c)|$ by integrating $P'$ along the segment from $c$ to $z$ . Such estimates lose a constant factor that depends on how the critical points are spread out, and the known uniform arguments all pass through distortion theorems for univalent functions, whose constants lead to $K$ close to $4$ . Reaching $K = 1$ requires using all critical points simultaneously, and no argument doing this in every degree is known. The equality case $z^d - dz$ , in which every critical point is equally bad, shows that any successful argument must be sharp for polynomials with maximally symmetric critical configurations.

Formalization scope

Polynomials are elements of ℂ[X] (Mathlib's Polynomial ℂ); the degree is natDegree, the derivative is Polynomial.derivative, evaluation is Polynomial.eval, and the roots of $P$ are the multiset P.roots (counted with multiplicity). A critical point is a c : ℂ with P.derivative.eval c = 0. The absolute value is the norm ‖·‖ on ℂ, and the constants $\frac{d-1}{d}$ and $4\frac{d-1}{d+1}$ are computed in ℝ from the cast of natDegree.

Every statement assumes $P'(z) \ne 0$ . This is the standard normalization and is essential in Lean: division by zero returns $0$ , so without it the choice $c = z$ would make the inequality trivially true whenever $z$ is itself a critical point. With the hypothesis, every critical point $c$ differs from $z$ and the quotient is a genuine difference quotient.

Crane's bound is stated as the existence, for each degree $d \ge 8$ , of a constant strictly below $4 - \frac{2.263}{\sqrt d}$ that works for all polynomials of degree exactly $d$ ; this is equivalent to the best constant in degree $d$ being strictly below that value.

A complete development needs basic facts on critical points of complex polynomials (existence, the Gauss–Lucas theorem), and, for the classical bounds, results from the theory of univalent functions such as the Koebe quarter theorem and coefficient estimates. These are reusable well beyond this mission. Contributions of any milestone, of supporting lemmas, and of partial results in fixed small degree are welcome.

Selected references

S. Smale, The fundamental theorem of algebra and complexity theory, Bull. Amer. Math. Soc. (N.S.) 4 (1981), 1–36. https://doi.org/10.1090/S0273-0979-1981-14858-8
D. Tischler, Critical points and values of complex polynomials, J. Complexity 5 (1989), 438–456. https://doi.org/10.1016/0885-064X(89)90019-8
A. Conte, E. Fujikawa, N. Lakic, Smale's mean value conjecture and the coefficients of univalent functions, Proc. Amer. Math. Soc. 135 (2007), 3295–3300. https://doi.org/10.1090/S0002-9939-07-08861-2
E. Crane, A bound for Smale's mean value conjecture for complex polynomials, Bull. London Math. Soc. 39 (2007), 781–791. https://doi.org/10.1112/blms/bdm063
V. Dubinin, T. Sugawa, Dual mean value problem for complex polynomials, Proc. Japan Acad. Ser. A 85 (2009), 135–137. https://arxiv.org/abs/0906.4605
T.-W. Ng, Y. Zhang, Smale's mean value conjecture for finite Blaschke products, J. Anal. 24 (2016), 331–345. https://arxiv.org/abs/1609.00170
Wikipedia, Mean value problem. https://en.wikipedia.org/w/index.php?title=Mean_value_problem&oldid=1374678764

10 thms2 active usersReviewed

Completed

Group Theory·Captain: dbenbenn

Monod: groups of piecewise projective homeomorphisms are non-amenable without free subgroupsResearch Paper

This mission formalizes N. Monod, Groups of piecewise projective homeomorphisms, Proceedings of the National Academy of Sciences 110 (2013) 4524–4527, doi:10.1073/pnas.1218426110: the groups $H(A)$ of piecewise projective homeomorphisms of the line are non-amenable and have no free subgroups whenever $A \neq \mathbf{Z}$ .

Motivation

The paper opens with the Banach–Tarski paradox and von Neumann's notion of amenability: "Tarski readily proved that amenability is the only obstruction to paradoxical decompositions. However, the known paradoxes relied more prosaically on the existence of non-abelian free subgroups. Therefore, the main open problem in the subject remained for half a century to find non-amenable groups without free subgroups" (p. 1). That problem, the so-called von Neumann conjecture, was answered by Ol'shanskii around 1980, with Tarski monsters. Monod's groups give "straightforward torsion-free counter-examples", "so simple that many additional properties can be established" (p. 1).

Monod's groups are close relatives of Thompson's groups: Thurston's model identifies Thompson's group $F$ with piecewise $\mathrm{PSL}_2(\mathbf{Z})$ maps of the line with rational breakpoints (p. 2). Whether $F$ is amenable is a notorious open problem, and whether $H(\mathbf{Z})$ is amenable is Monod's Problem 12 (p. 2).

Timeline

1914–1929. Hausdorff's paradox (1914); Banach–Tarski (1924); von Neumann introduces amenable groups (1929); Tarski characterizes amenability by the absence of paradoxical decompositions.
1950s. Day's classes; the question whether every non-amenable group contains a free subgroup of rank two becomes attached to von Neumann's name.
c. 1965–1975. Thompson's groups $F$ , $T$ , $V$ ; Thurston's piecewise projective models of $F$ and $T$ .
1979–1982. Ol'shanskii proves Tarski monsters non-amenable; Adyan does the same for free Burnside groups.
1985. Brin–Squier: groups of piecewise linear homeomorphisms of the line have no free subgroups.
2003. Ol'shanskii–Sapir: finitely presented non-amenable groups without free subgroups.
2013. Monod: the piecewise projective groups $H(A)$ (this paper).
2016. Lodha–Moore: a finitely presented subgroup of Monod's group, non-amenable and without free subgroups.

Setting

The projective line $\mathbf{P}^1$ is OnePoint ℝ, on which $\mathrm{SL}_2(A)$ acts through $\mathrm{GL}_2(\mathbf{R})$ by Möbius transformations (mob, using Mathlib's action on OnePoint). For a subring $A$ of $\mathbf{R}$ (A : Subring ℝ; $\mathbf{Z}$ is ⊥, $\mathbf{R}$ is ⊤), P A is $P_A$ , the set of fixed points of hyperbolic elements (trace of absolute value greater than $2$ ).

A homeomorphism of $\mathbf{P}^1$ is piecewise in $\mathrm{PSL}_2(A)$ with breakpoints in $E$ (IsPiecewiseProjOn A E f) when, off some finite subset of $E$ , it agrees near every point with a Möbius transformation from $\mathrm{SL}_2(A)$ . Monod's $G$ (Gpp) is the group generated by the homeomorphisms piecewise in $\mathrm{PSL}_2(\mathbf{R})$ , with breakpoints anywhere, and $H$ (Hpp) is its stabilizer of $\infty$ (fixInf). For a subring $A$ , $G(A)$ (G A) is the subgroup of $G$ generated by its elements that are piecewise in $\mathrm{PSL}_2(A)$ with breakpoints in $P_A$ (IsPiecewiseProj A), and $H(A)$ (H A) is its stabilizer of $\infty$ ; $H(\mathbf{Z})$ is H ⊥. GRat is the subgroup of $G$ generated by its elements piecewise in $\mathrm{PSL}_2(\mathbf{Z})$ with breakpoints in $\mathbf{Q} \cup \{\infty\}$ , and HRat its stabilizer of $\infty$ : the rational-breakpoint variants of $G(\mathbf{Z})$ and $H(\mathbf{Z})$ (p. 2).

Amenability is Garrido.IsAmenable (a finitely additive left-invariant probability measure on all subsets), and "no non-abelian free subgroup" is Chou.NoFreeSubgroupOfRankTwo; both are published definitions, in the bundles Garrido_Amenability and Chou_Classes. Co-amenable subgroups (IsCoamenable), inner amenability (IsInnerAmenable) and pointwise stabilizers (fixSubgroup), all on p. 3, are defined in the bundle in the same style.

A relation $R \subseteq X \times X$ is amenable for a measure $\mu$ (IsAmenableRel μ R, p. 2) when it has a left invariant mean in the sense of Connes–Feldman–Weiss: a positive, unital map from bounded measurable functions on $R$ to functions on $X$ , linear up to $\mu$ -null sets and invariant under the partial transformations of $R$ . volP1 is the Lebesgue measure class on $\mathbf{P}^1$ .

Target

The goal is Theorem 1, "The group $H(A)$ is non-amenable if $A \neq \mathbf{Z}$ " (p. 1), introduced as "the main result of this article". The proof (p. 2) passes to a countable dense subring $A'$ of $A$ , compares the orbits of $H(A')$ and $\mathrm{PSL}_2(A')$ on $\mathbf{P}^1 \setminus \{\infty\}$ (Proposition 9), and concludes from two facts about measured equivalence relations: the orbit relation of an amenable group's action is amenable, and, by a theorem of Carrière and Ghys, the orbit relation of $\mathrm{PSL}_2(A')$ on $\mathbf{P}^1$ is not.

The milestones are, in the paper's order: $G(A)$ consists exactly of the elements of $G$ piecewise in $\mathrm{PSL}_2(A)$ with breakpoints in $P_A$ ; $H = H(\mathbf{R})$ ; $H$ preserves orientation, is left-orderable and torsion-free; Proposition 9; the countable dense subring; the orbit relation of a measurable action of an amenable group is amenable; the orbit relation of $\mathrm{PSL}_2(A)$ on $\mathbf{P}^1$ is not amenable (Carrière–Ghys, external); Lemma 13 and Theorem 14 leading to Theorem 2 ( $H$ has no free subgroups); Corollary 3; Proposition 6 (bi-orderability); Lemma 16, Proposition 7 (co-amenability of pointwise stabilizers), Proposition 15 and Proposition 5 (inner amenability); and Thurston's identification of the rational-breakpoint variants of $H(\mathbf{Z})$ and $G(\mathbf{Z})$ with $F$ and $T$ .

Significance

The result. Theorem 1 and Theorem 2 together make $H(A)$ , for instance $A = \mathbf{Z}[\sqrt 2]$ , a torsion-free counterexample to the von Neumann conjecture, with finitely generated examples (Corollary 3). The groups are concrete enough to carry many further properties (Propositions 5–7).

Formalizing it. Nothing on amenability of groups of homeomorphisms of the line, or on measured equivalence relations, is in Mathlib. Amenability and Følner's theorem are on this platform from Garrido I, the Banach–Tarski paradox from Garrido II, Brin–Squier's theorem from its own mission, and Thompson's $F$ and $T$ (CannonFloydParry, CannonFloydParry_T) from the Cannon–Floyd–Parry missions.

Difficulty

The algebraic half, Theorem 2 and Propositions 5–9, follows Brin–Squier and elementary dynamics on the circle. The analytic half is the passage through measured equivalence relations in the proof of Theorem 1. The mission defines amenability of a relation as Connes–Feldman–Weiss do, by an invariant mean valued in $L^\infty$ , which is the form under which an amenable group's orbit relation is amenable without extra set-theoretic hypotheses. The step taken from the literature, that the orbit relation of $\mathrm{PSL}_2(A)$ on $\mathbf{P}^1$ is not amenable for $A$ countable and dense, rests on Carrière–Ghys's theorem and on Zimmer's theory of amenable actions (Adams–Elliott–Giordano). The milestone is proved (Monod.not_isAmenableRel_mob) by an elementary route that needs neither: a ping-pong argument in $\mathrm{SL}_2(A)$ that contradicts an invariant mean directly.

What is left out

The second sentence of Proposition 6 (no non-trivial homomorphism from a Kazhdan group) and Proposition 8 (actions on CAT(0) spaces): property (T) and CAT(0) spaces are not in Mathlib.
Proposition 4 ( $L^2$ -Betti numbers), the remarks on group laws, on the Dixmier problem and on bounded cohomology.
Remarks 10 and 11, which discuss alternative proofs of the step taken from Carrière–Ghys.

Formalization scope

$\mathbf{P}^1$ is OnePoint ℝ and $\mathrm{PSL}_2(A)$ acts through Matrix.SpecialLinearGroup (Fin 2) A; since $-1$ acts trivially the orbits are those of $\mathrm{PSL}_2(A)$ .
"Piecewise with finitely many pieces, each an interval" is stated locally: off a finite set of breakpoints, $f$ agrees near each point with one Möbius transformation. Pieces then extend over arcs because two Möbius maps agreeing near a point agree everywhere.
The groups are subgroups of the homeomorphism group of OnePoint ℝ, each defined as the subgroup generated by the maps the paper describes; the milestones state that $G(A)$ is exactly its set of such maps and that $G = G(\mathbf{R})$ .
An amenable measured equivalence relation (p. 2) is one with a left invariant mean in the sense of Connes–Feldman–Weiss (an operator from $L^\infty$ of the relation to $L^\infty(X, \mu)$ , their Definition 6), as in Schmidt, whom the paper cites. The paper describes it as a measurable assignment of means on the orbits, the motivating form in Connes–Feldman–Weiss; for that form, "an amenable group's action produces an amenable relation" is known only assuming CH. $\mathbf{P}^1$ carries its Borel σ-algebra and the Lebesgue measure class (volP1).
"Metabelian" is the vanishing of the second derived subgroup, and "contains a free abelian group of rank two" is an injective homomorphism from $\mathbf{Z}^2$ .
Reused platform items, which solutions may import: the amenability and free-subgroup definitions (Garrido, Chou), Brin–Squier's Theorem 3.1, and Thompson's $F$ and $T$ (Cannon–Floyd–Parry).

Selected references

N. Monod, Groups of piecewise projective homeomorphisms, Proc. Natl. Acad. Sci. USA 110 (2013) 4524–4527. doi:10.1073/pnas.1218426110
Y. Carrière, É. Ghys, Relations d'équivalence moyennables sur les groupes de Lie, C. R. Acad. Sci. Paris Sér. I Math. 300 (1985) 677–680 (no DOI).
A. Connes, J. Feldman, B. Weiss, An amenable equivalence relation is generated by a single transformation, Ergodic Theory Dynam. Systems 1 (1981) 431–450. doi:10.1017/S014338570000136X
K. Schmidt, Algebraic ideas in ergodic theory, CBMS Regional Conference Series in Mathematics 76, AMS (1990) (a book; no DOI).
M. G. Brin, C. C. Squier, Groups of piecewise linear homeomorphisms of the real line, Invent. Math. 79 (1985) 485–498. doi:10.1007/BF01388519

25 thms2 active usersReviewed

Completed

Group Theory·Captain: dbenbenn

Is Thompson's group F amenable? (Geoghegan's conjecture)Open Problem

This mission formalizes Geoghegan's conjecture that Thompson's group $F$ is not amenable, in the form stated by Cannon, Floyd and Parry, Introductory notes on Richard Thompson's groups, L'Enseignement Math. (2) 42 (1996), §4, p. 227 (doi:10.5169/seals-87877), together with the landmark results of the literature on the question.

Motivation

A discrete group is amenable when it carries a finitely additive, translation-invariant probability measure on all of its subsets. Groups containing a non-abelian free subgroup are not amenable, and the question whether every non-amenable group contains one (the von Neumann problem) made Thompson's group $F$ the first natural candidate for a counterexample: it contains no non-abelian free subgroup, and it is not elementary amenable. Geoghegan conjectured in 1979 that $F$ is not amenable; several announced solutions in each direction did not survive. In 2026 OpenAI released a proof that $F$ is not amenable, with a Lean formalization; adapted to this mission's definitions, it is the solution of the goal.

Timeline.

1965: Richard Thompson defines the groups $F$ , $T$ and $V$ (Cannon–Floyd–Parry, p. 215).
1979: Geoghegan conjectures that $F$ contains no non-abelian free subgroup and is not amenable (Cannon–Floyd–Parry, p. 227).
1985: Brin and Squier prove that $F$ contains no non-abelian free subgroup (doi:10.1007/BF01388519).
1996: Cannon, Floyd and Parry prove, using Chou's work on elementary amenable groups, that $F$ is not elementary amenable (Theorem 4.10).
2009–2014: announced proofs of amenability (Shavgulidze, 2009; Moore, 2012) and of non-amenability (Akhmedov, 2009; Beklaryan, 2011; Wajnryb–Witowicz, 2014) are withdrawn by their authors or found to contain serious errors.
2013: Moore proves that if $F$ is amenable, its Følner sets grow at least like a tower of exponentials (doi:10.4171/GGD/201).
2013: Monod introduces the groups $H(A)$ of piecewise-projective homeomorphisms of the line, proves that they have no non-abelian free subgroup and are not amenable for every subring $A \ne \mathbf Z$ of $\mathbf R$ , and asks whether $H(\mathbf Z)$ is amenable (Problem 12) (doi:10.1073/pnas.1218426110).
2015: Juschenko, Matte Bon, Monod and de la Salle introduce extensive amenability of group actions, and prove that a subgroup of Monod's group of piecewise-projective homeomorphisms of the line is amenable if and only if its action on the line is extensively amenable (Theorem 6.4; arXiv 2015; published 2018, doi:10.1017/etds.2016.32).
2017: Kaimanovich proves that random walks on $F$ with finitely supported, strictly non-degenerate step distributions have non-trivial Poisson boundary (doi:10.1017/9781316576571.013).
2019: Chornyi shows that $F$ is amenable if and only if its action on the dyadic rationals in $(0,1)$ is extensively amenable (arXiv:1907.01440).
2019: Kim, Koberda and Lodha show that large powers of two homeomorphisms of the line with overlapping supports generate a copy of $F$ (doi:10.24033/asens.2397).
2021: Stankov records, from Kim–Koberda–Lodha, that $H(\mathbf Z)$ contains a copy of $F$ , so that amenability of $H(\mathbf Z)$ would imply amenability of $F$ (doi:10.1017/etds.2019.76).
2023: Monod shows that the Thompson group $H_{\mathbf Q}(\mathbf Z) \cong F$ is not co-amenable in the group $H_{\mathbf Q}(\mathbf Q)$ (doi:10.4171/ggd/883).
2023: Guba's survey records that "the famous problem about amenability of $F$ remains open" (doi:10.46298/jgcc.2023.15.1.11315).
2026: OpenAI proves that $F$ is not amenable: a Lipschitz self-map of the Hilbert ball with no approximate fixed point (Benyamini–Sternfeld), composed with a recursive colouring of dyadic partitions that $F$ transports exactly, gives a uniform lower bound on the Følner ratios of $F$ . The proof comes with a Lean formalization (Thompson's group F is nonamenable, September 23, 2026, github.com/openai/math).

Setting

Let UI be the unit interval $[0,1]$ . Thompson's group $F$ (CannonFloydParry.F) is the group, under composition, of the order-preserving homeomorphisms of $[0,1]$ that are piecewise linear with finitely many breakpoints, every breakpoint a dyadic rational $k/2^n$ and every slope a power of $2$ . It is generated by two elements and finitely presented (Cannon–Floyd–Parry, Corollary 2.6 and Theorem 3.4).

A mean on a set $S$ is a function $m$ from the subsets of $S$ to $[0,\infty]$ with $m(\emptyset) = 0$ , $m(A \cup B) = m(A) + m(B)$ for disjoint $A, B$ , and $m(S) = 1$ . A group $G$ is amenable (Garrido.IsAmenable G) when it carries a mean with $m(gA) = m(A)$ for all $g \in G$ and $A \subseteq G$ , where $gA = \{ga : a \in A\}$ . This is equivalent to the definition Cannon, Floyd and Parry give on p. 227, whose means take values in $[0,1]$ .

The milestones use four further notions, defined precisely in the definitions item and in their own statements:

A finite set $A \subseteq G$ is $\varepsilon$ -Følner for a finite $\Gamma \subseteq G$ when $\sum_{\gamma\in\Gamma}|\gamma A \mathbin{\triangle} A| < \varepsilon|A|$ ; by Følner's criterion, $G$ is amenable exactly when it has such sets for every $\varepsilon > 0$ .
A finitely supported probability measure $\mu$ on $G$ drives a random walk; $\mu$ is strictly non-degenerate when its support generates $G$ as a semigroup, and the walk is Liouville when every bounded $\mu$ -harmonic function, $f(g) = \sum_h \mu(h) f(gh)$ , is constant.
An action of $G$ on a set $X$ is extensively amenable when the finite subsets of $X$ carry a $G$ -invariant mean that, for each finite $E_0 \subseteq X$ , gives full weight to the finite sets containing $E_0$ .
For a subring $A$ of $\mathbf R$ , Monod's group $H(A)$ consists of the homeomorphisms of the real line that are piecewise projective, $x \mapsto (ax+b)/(cx+d)$ with $\left(\begin{smallmatrix} a & b \\ c & d \end{smallmatrix}\right) \in \mathrm{SL}_2(A)$ , with finitely many breakpoints, each a fixed point of a hyperbolic element of $\mathrm{SL}_2(A)$ . $H_B(A)$ allows breakpoints in a set $B$ instead; $H_{\mathbf Q}(\mathbf Z)$ is isomorphic to $F$ (Thurston). A subgroup $K$ of $J$ is co-amenable when $J/K$ carries a $J$ -invariant mean.

Formalization targets

Goal: Geoghegan's conjecture

\neg\,\mathrm{IsAmenable}(F).

The question was open until 2026. OpenAI's proof of the conjecture (see the timeline), transferred to CannonFloydParry.F and Garrido.IsAmenable, proves this statement.

Landmarks

The milestones are results from the literature, stated as their sources state them: $F$ has no non-abelian free subgroup (Cannon–Floyd–Parry, Corollary 4.9) and is not elementary amenable (Theorem 4.10), and Følner's criterion, all three already proved and linked as references; Moore's tower lower bound on Følner sets of $F$ ; Kaimanovich's theorem that random walks on $F$ with finitely supported strictly non-degenerate steps are not Liouville; Chornyi's reformulation of amenability of $F$ as extensive amenability of its action on the dyadic rationals; Stankov's embedding of $F$ into Monod's $H(\mathbf Z)$ ; Monod's theorem that $H_{\mathbf Q}(\mathbf Z) \cong F$ is not co-amenable in $H_{\mathbf Q}(\mathbf Q)$ ; and the theorem of Juschenko, Matte Bon, Monod and de la Salle that a subgroup of Monod's group of piecewise-projective homeomorphisms of the line is amenable if and only if its action on the line is extensively amenable.

A second open statement

Monod's Problem 12 asks whether $H(\mathbf Z)$ is amenable; it is stated as ¬ Garrido.IsAmenable (Monod.H ⊥), where ⊥ is the smallest subring of $\mathbf R$ , namely $\mathbf Z$ ; this is parallel to the goal. Through Stankov's embedding, the proof of the goal proves it. By the theorem of Juschenko, Matte Bon, Monod and de la Salle, it is equivalent to the statement that the action of $H(\mathbf Z)$ on the line is not extensively amenable; that theorem is proved on this platform, through the germ-groupoid theorem of Juschenko, Nekrashevych and de la Salle (GermGroupoid.isAmenable_of_isExtensivelyAmenableOn), and for the subgroups of $H(\mathbf Z)$ also in a sharper form, with extensive amenability on the set of possible breakpoints only (the breakpoint criterion).

Significance

The result. A proof of the conjecture would make $F$ a finitely presented, torsion-free, non-amenable group with no non-abelian free subgroup, with a concrete description as a group of homeomorphisms of the interval. A disproof would make $F$ an amenable group that is not elementary amenable, and by Moore's theorem one whose Følner sets are at least tower-sized.

Formalizing it. Corollary 4.9 and Theorem 4.10 of Cannon–Floyd–Parry are formalized and proved on this platform and enter as references. Chornyi's corollary is proved here; its "if" direction is proved directly, by establishing the case that Chornyi applies of the Juschenko–Matte Bon–Monod–de la Salle criterion. Moore's theorem is formalized and published together with the lemmas of its proof, and the milestone here has a solution that reduces it to that statement. Kaimanovich's theorem, Stankov's embedding, Monod's 2023 theorem and the theorem of Juschenko, Matte Bon, Monod and de la Salle are proved here as well, the last through the germ-groupoid theorem of Juschenko, Nekrashevych and de la Salle (GermGroupoid.isAmenable_of_isExtensivelyAmenableOn). The definitions of Følner sets, harmonic functions on groups and extensive amenability are reusable beyond this mission.

Difficulty

The obstructions to amenability that settle the question for most groups are absent here: $F$ has no non-abelian free subgroup, and its elementary structure is well understood. In the other direction, the usual constructions of invariant means fail: by Moore's theorem any Følner set of $F$ is at least tower-sized, so no explicit search can exhibit one, and by Kaimanovich's theorem the finitely supported random walks on $F$ are not Liouville, so the random-walk route to amenability through a trivial Poisson boundary is closed.

Formalization scope

Lean representation and conventions.

$F$ is a subgroup of the order isomorphisms of UI; $H(A)$ and $H_B(A)$ are subgroups of the homeomorphisms of OnePoint ℝ. Groups of maps multiply by composition, $(fg)(x) = f(g(x))$ ; statements from sources that write the product in the other order are restated for this convention, with the equivalence explained in their natural-language statements.
Means take values in $[0,\infty]$ ; total mass $1$ and finite additivity keep every value in $[0,1]$ .
Extensive amenability is stated for an action on $[0,1]$ relative to the set of dyadic rationals in $(0,1)$ ; the statement of Chornyi's corollary includes that $F$ maps this set to itself.
The goal cannot be satisfied vacuously: amenability is a single existential statement about means on $F$ , and $F$ is a fixed, nontrivial, finitely generated group.

What is left out.

The Poisson boundary is not formalized: "Liouville" is Kaimanovich's equivalent reformulation through bounded harmonic functions on $\operatorname{sgr}\mu$ (p. 8).
The "in particular" clause of Moore's Theorem 1.1, on the Følner function, is not stated separately; with Følner's criterion it follows from the stated bound.
The withdrawn and disputed proofs in the timeline are not formalized.

What a development needs. Thompson's group $F$ and its dyadic action (Cannon–Floyd–Parry §4), its tree diagrams and presentations, and amenability, Følner's criterion and the closure properties of amenable groups (Garrido I) are published and proved on this platform, as are Monod's groups and the isomorphism $H_{\mathbf Q}(\mathbf Z) \cong F$ (Monod.contDiff_and_exists_mulEquiv_HRat_F). Mathlib has Følner filters for measurable groups and Schreier graphs of quivers, but no random walks on groups; the proofs of the landmarks here supply what they need, and the germ-groupoid theorem of Juschenko, Nekrashevych and de la Salle (GermGroupoid.isAmenable_of_isExtensivelyAmenableOn) is reusable beyond this mission. Reductions of the goal or of Problem 12 to new, sharper statements are welcome, as is a disproof of either.

Selected references

J. W. Cannon, W. J. Floyd, W. R. Parry, Introductory notes on Richard Thompson's groups, L'Enseignement Math. (2) 42 (1996) 215–256. doi:10.5169/seals-87877
M. G. Brin, C. C. Squier, Groups of piecewise linear homeomorphisms of the real line, Invent. Math. 79 (1985) 485–498. doi:10.1007/BF01388519
J. T. Moore, Fast growth in the Følner function for Thompson's group F, Groups Geom. Dyn. 7 (2013) 633–651. doi:10.4171/GGD/201
V. A. Kaimanovich, Thompson's group F is not Liouville, in Groups, Graphs and Random Walks, LMS Lecture Note Ser. 436 (2017) 300–342. doi:10.1017/9781316576571.013
N. Monod, Groups of piecewise projective homeomorphisms, Proc. Natl. Acad. Sci. USA 110 (2013) 4524–4527. doi:10.1073/pnas.1218426110
K. Juschenko, N. Matte Bon, N. Monod, M. de la Salle, Extensive amenability and an application to interval exchanges, Ergodic Theory Dynam. Systems 38 (2018) 195–219. doi:10.1017/etds.2016.32
M. Chornyi, Superharmonic functions on the Lamplighter graph of Thompson's group F, preprint (2019). arXiv:1907.01440
V. Guba, Amenability problem for Thompson's group F: state of the art, J. Groups Complex. Cryptol. 15 (2023), no. 1. doi:10.46298/jgcc.2023.15.1.11315
S.-h. Kim, T. Koberda, Y. Lodha, Chain groups of homeomorphisms of the interval, Ann. Sci. Éc. Norm. Supér. (4) 52 (2019) 797–820. doi:10.24033/asens.2397
B. Stankov, Non-triviality of the Poisson boundary of random walks on the group H(ℤ) of Monod, Ergodic Theory Dynam. Systems 41 (2021) 1160–1189. doi:10.1017/etds.2019.76
OpenAI, Thompson's group F is nonamenable, OpenAI Math Release preprint (September 23, 2026). github.com/openai/math
N. Monod, Some comments on piecewise-projective groups of the line, Groups Geom. Dyn. 19 (2025) 459–476. doi:10.4171/ggd/883

61 thms2 active usersReviewed

Differential Geometry Dynamical Systems·Captain: Lucas

Pugh's Closing LemmaResearch Paper

Motivation

A periodic point of a map $f\colon M\to M$ is a point $x$ with $f^n(x)=x$ for some $n\ge 1$ . A nonwandering point is a much weaker form of recurrence: every neighbourhood $U$ of $x$ eventually returns to meet itself, $f^n(U)\cap U\ne\emptyset$ for some $n\ge 1$ . Every periodic point is nonwandering, but a nonwandering point need not be periodic, and the orbit of such a point may never come back to $x$ exactly.

Pugh's closing lemma asserts that this gap can be closed by an arbitrarily small change of the system: if $x$ is nonwandering for a $C^1$ diffeomorphism $f$ of a compact manifold, then some diffeomorphism $g$ , as close to $f$ as desired in the $C^1$ topology, has $x$ as a periodic point (Wikipedia, "Pugh's closing lemma"). The result was proved by C. C. Pugh in 1967 (Pugh 1967), in the same paper as the General Density Theorem: for a $C^1$ -generic diffeomorphism the periodic points are dense in the nonwandering set. The source article describes the lemma as establishing a close relationship between chaotic and periodic behaviour and notes that it underlies some autonomous convergence theorems. The article also points to Smale's problems as related material.

Setting

Let $M$ be a compact smooth manifold of dimension $d$ , Hausdorff and without boundary. Write $\mathrm{Diff}^1(M)$ for the set of $C^1$ diffeomorphisms $g\colon M\to M$ : bijections such that $g$ and $g^{-1}$ are continuously differentiable. For $g\in\mathrm{Diff}^1(M)$ , $Tg\colon TM\to TM$ denotes its tangent map on the tangent bundle.

The $C^1$ topology on $\mathrm{Diff}^1(M)$ is the coarsest topology for which $g\mapsto Tg$ is continuous, where the space $C(TM,TM)$ of continuous self-maps of $TM$ carries the compact-open topology. Two diffeomorphisms are $C^1$ -close when they, and their derivatives, are uniformly close.

For a map $h\colon X\to X$ of a topological space:

$x$ is nonwandering if for every neighbourhood $U$ of $x$ there is $n\ge 1$ with $h^n(U)\cap U\ne\emptyset$ ; the nonwandering set is $\Omega(h)$ ;
$\mathrm{Per}(h)=\{x : \exists\, n\ge 1,\ h^n(x)=x\}$ is the set of periodic points.

Formalization targets

Goal: Pugh's closing lemma

For every $f\in\mathrm{Diff}^1(M)$ and every $x\in\Omega(f)$ ,

\forall\ \mathcal U \text{ a } C^1\text{-neighbourhood of } f,\quad \exists\, g\in\mathcal U,\ \ x\in\mathrm{Per}(g).

Milestones

$\mathrm{Per}(f)\subseteq\Omega(f)$ for any map $f$ .
$\Omega(f)$ is closed for any map $f$ .
$f(\Omega(f))=\Omega(f)$ for a homeomorphism $f$ .
$\Omega(f)\ne\emptyset$ for any map of a nonempty compact space.
General Density Theorem (Pugh 1967): there is a residual set $\mathcal G\subseteq\mathrm{Diff}^1(M)$ with

\overline{\mathrm{Per}(g)}=\Omega(g)\qquad (g\in\mathcal G).

Milestones 1–4 are elementary background facts that are not stated in the source article; milestone 5 is the second theorem named in the title of the source's reference.

Significance

The result. The closing lemma turns a topological recurrence property into periodicity after a $C^1$ -small perturbation. Combined with genericity arguments it gives the General Density Theorem, so that for generic $C^1$ diffeomorphisms the whole nonwandering set is the closure of the periodic orbits. It is one of the basic perturbation tools of $C^1$ generic dynamics.

Formalizing it. The theorem is classical and proved in the literature. The drafter is not aware of a machine-checked proof. A formalization needs the $C^1$ topology on diffeomorphism groups, local perturbation lemmas in charts and the combinatorics of the closing argument. None of these is currently available in Mathlib as far as the drafter knows.

Difficulty

The first idea is to take the returning piece of orbit near $x$ and push it back to $x$ with a small local perturbation. This fails in the $C^1$ topology. Moving a point by distance $\delta$ with a bump supported in a ball of radius $r$ costs $C^1$ size about $\delta/r$ , and the return may happen at a distance comparable to the size of the only available ball. The perturbation then fails to be $C^1$ -small. The derivative $Df^n$ along the return can also distort any fixed neighbourhood shape without bound. Controlling this distortion is the central difficulty.

Formalization scope

$\mathrm{Diff}^1(M)$ and its $C^1$ topology come from the published definition file BCWCentralizer_Basic. $\mathrm{Diff}^1(M)$ is M ≃ₘ^1⟮𝓡 d, 𝓡 d⟯ M, and the topology is induced by $g\mapsto Tg$ into C(TangentBundle, TangentBundle) with the compact-open topology. On a compact manifold this is the usual $C^1$ topology.
"Compact smooth manifold": a Hausdorff compact space with a $C^\infty$ atlas modelled on $\mathbb R^d$ , so without boundary. $d$ is arbitrary.
"Arbitrarily close" means that every neighbourhood of $f$ in the $C^1$ topology contains a suitable $g$ . "Periodic" requires a period $n\ge 1$ . Allowing $n=0$ would make every point periodic and the statement trivial.
The perturbation $g$ is only required to be a $C^1$ diffeomorphism, matching $\mathrm{Diff}^1(M)$ in the source.
The nonwandering notion is the definition item PughClosingLemma_nonwandering, shared by all statements. It is reusable for any topological dynamics mission.

Welcome contributions: a general theory of the $C^1$ topology on $\mathrm{Diff}^1(M)$ (for example, that it is Baire), local perturbation lemmas, and proofs of the milestones.

Selected references

C. C. Pugh, An Improved Closing Lemma and a General Density Theorem, American Journal of Mathematics 89 (4), 1967, 1010–1021. https://doi.org/10.2307/2373414
Wikipedia, Pugh's closing lemma, revision 1304222873. https://en.wikipedia.org/w/index.php?title=Pugh%27s_closing_lemma&oldid=1304222873
V. Araújo, M. J. Pacifico, Three-Dimensional Flows, Springer, 2010, ISBN 978-3-642-11414-4.

8 thms2 active usersReviewed

Dynamical Systems·Captain: Lucas

The C¹-generic diffeomorphism has trivial centralizer (Bonatti–Crovisier–Wilkinson)Research Paper

Motivation

Two commuting diffeomorphisms $f,g$ of a manifold $M$ share all of their dynamics: $g$ permutes the orbits of $f$ and preserves every smooth and topological invariant of $f$ . The centralizer of $f\in\mathrm{Diff}^r(M)$ ,

Z^r(f)=\{g\in\mathrm{Diff}^r(M): fg=gf\},

always contains the cyclic group $\langle f\rangle=\{f^n:n\in\mathbb Z\}$ , and $f$ has trivial centralizer when $Z^r(f)=\langle f\rangle$ . S. Smale asked whether diffeomorphisms with trivial centralizer are dense, residual, or even open and dense in $\mathrm{Diff}^r(M)$ (one of Smale's problems for the 21st century).

Timeline: Kopell (1970) answered the question for $r\ge2$ on the circle; Palis–Yoccoz, Fisher and Burslem obtained results under hyperbolicity or partial hyperbolicity assumptions; Togawa treated generic Axiom A diffeomorphisms in the $C^1$ topology; Bonatti–Crovisier–Vago–Wilkinson showed that trivial-centralizer diffeomorphisms do not contain an open dense set in $\mathrm{Diff}^1(M)$ ; and Bonatti–Crovisier–Wilkinson (this paper, arXiv:0804.1416) proved residuality in $\mathrm{Diff}^1(M)$ for every compact manifold.

Setting

$M$ is a closed (compact, boundaryless), connected smooth manifold of dimension $d$ . $\mathrm{Diff}^1(M)$ is the space of $C^1$ diffeomorphisms of $M$ with the $C^1$ topology; a subset is residual if it contains a countable intersection of open dense sets.

Formalization targets

Goal (Main Theorem, p. 3)

There is a residual subset $\mathcal R\subset\mathrm{Diff}^1(M)$ such that for every $f\in\mathcal R$ and every $g\in\mathrm{Diff}^1(M)$ with $fg=gf$ , one has $g=f^n$ for some $n\in\mathbb Z$ .

Milestones

Following Section 2 of the paper: the classical upper-semicontinuity lemma used for Proposition 2.5, the wandering part of Theorem A (unbounded distortion is $C^1$ -generic), Proposition 2.5 (density of trivial Lipschitz centralizers implies residuality) and Theorem 2.3 (residuality of trivial Lipschitz centralizers when $\dim M\ge2$ ).

Significance

The theorem answers the second (and hence the first) part of Smale's question in the $C^1$ topology, and exhibits a precise link between dynamical properties of $f$ (large derivative and unbounded distortion) and the algebraic structure of $f$ inside the group $\mathrm{Diff}^1(M)$ . The result is proved in the literature; it has not been formalized.

Difficulty

The density of trivial centralizers comes from perturbation results (Theorems A and B) that change the derivative without changing the topological dynamics (tidy perturbations in topological towers). Density alone does not give residuality, since the set of diffeomorphisms with the large derivative property is not residual (Appendix); the passage from dense to residual needs the Lipschitz centralizer and a semicontinuity argument.

Formalization scope

$M$ is a charted space over $\mathbb R^d$ with a $C^\infty$ atlas, Hausdorff, compact and connected; $\mathrm{Diff}^1(M)$ is Mathlib's type of $C^1$ diffeomorphisms. The $C^1$ topology is encoded as the topology induced by $f\mapsto Tf$ into the compact-open topology on continuous self-maps of the tangent bundle $TM$ . Powers $f^n$ , $n\in\mathbb Z$ , are taken in the permutation group of $M$ . Bi-Lipschitz homeomorphisms are defined chart-locally (equivalent on a compact manifold to bi-Lipschitz for a Riemannian distance). Jacobians $|\det Df^n|$ are computed with respect to an arbitrary continuous Riemannian metric; the unbounded-distortion property does not depend on this choice.

Contributions welcome: the $C^1$ topology API (Baire property, continuity of composition), the Kupka–Smale and closing-lemma genericity results, and the perturbation machinery of Sections 3–7.

Selected references

C. Bonatti, S. Crovisier, A. Wilkinson, The $C^1$ generic diffeomorphism has trivial centralizer, Publ. Math. IHÉS 109 (2009); arXiv:0804.1416. https://arxiv.org/abs/0804.1416
S. Smale, Mathematical problems for the next century, Math. Intelligencer 20 (1998).
N. Kopell, Commuting diffeomorphisms, Proc. Sympos. Pure Math. 14 (1970).

7 thms2 active usersReviewed

Algebraic Geometry Dynamical Systems·Captain: Lucas

Albouy–Kaloshin: Finiteness of Planar Five-Body Central ConfigurationsResearch Paper

Motivation

A central configuration of the Newtonian $n$ -body problem is a placement of $n$ point masses in which the gravitational acceleration of every body points toward the centre of mass and is proportional to its distance from it. Central configurations generate the only explicitly known solutions of the $n$ -body problem (the homographic, or self-similar, motions), they are the possible limiting shapes of total collisions, and they organise the topology of the integral manifolds. Counting them is therefore a basic question of celestial mechanics.

Timeline.

Euler (1767) and Lagrange (1772) found all central configurations of three bodies: three collinear ones and the equilateral triangle.
Moulton (1910) showed there are exactly $n!/2$ collinear central configurations for any positive masses.
Chazy (1918) postulated that all central configurations are nondegenerate, which would imply finiteness; Wintner (1941) stated finiteness as a conjecture.
Palmore (1975) gave a degenerate example, refuting Chazy's postulate but not finiteness.
Smale (1998) listed finiteness of relative equilibria for every choice of positive masses as the 6th of his problems for the 21st century.
Hampton and Moeckel (2006) proved finiteness for $n = 4$ , using heavy computer algebra (BKK theory).
Albouy and Kaloshin (2012) gave a new proof for $n = 4$ that avoids heavy computation, and proved finiteness for $n = 5$ except possibly for masses in a codimension-2 algebraic subset of the mass space. The case $n \ge 6$ , and the $n = 5$ case for the excluded masses, remain open.

Setting

Fix $n$ bodies with masses $m_1,\dots,m_n$ ; body $k$ sits at $(x_k,y_k)\in\mathbb R^2$ . Write $x_{kl}=x_l-x_k$ , $y_{kl}=y_l-y_k$ and $r_{kl}=\sqrt{x_{kl}^2+y_{kl}^2}$ . A configuration with all $r_{kl}>0$ is a central configuration (normalised so that the proportionality constant is $1$ ) when, for every $k$ ,

\begin{pmatrix}x_k\\ y_k\end{pmatrix}=\sum_{l\ne k} m_l\, r_{kl}^{-3}\begin{pmatrix}x_k-x_l\\ y_k-y_l\end{pmatrix}.

These equations are invariant under rotations of the plane; imposing $y_{12}=0$ removes this freedom, and a solution with this normalisation is a positive normalized central configuration (Definition 1 of the paper; Lean: PosNormalizedCC n m).

The proof works in the complex domain. Introducing unknowns $\delta_{kl}$ (inverse distances) with $\delta_{kl}^2(x_{kl}^2+y_{kl}^2)=1$ turns the equations into the polynomial system (4) on $\mathbb C^{2n}\times\mathbb C^{n(n-1)/2}$ :

x_k=\sum_{l\ne k} m_l\,\delta_{kl}^3\,(x_k-x_l),\qquad y_k=\sum_{l\ne k} m_l\,\delta_{kl}^3\,(y_k-y_l),\qquad y_{12}=0 .

A complex solution is a normalized central configuration (Lean: NormalizedCC n m), a real one if all $x_k,y_k$ are real (Lean: RealNormalizedCC n m). The potential is $U=\sum_{k<l}m_km_l\delta_{kl}$ (Lean: potential n m).

Formalization targets

Goal — Theorem 2 (planar five bodies)

There is a closed algebraic subset $A\subset\mathbb R^5$ of codimension at least $2$ such that for all masses $m\in(\mathbb R_{>0})^5\setminus A$ ,

\#\{\text{positive normalized central configurations of the planar 5-body problem with masses } m\}<\infty .

The exceptional set is not made explicit; only its existence and dimension bound are asserted.

Stronger — Theorem 6

The same statement with all complex solutions of system (4) in place of the positive real ones.

Four bodies — Theorems 1, 3, 4, 5

For $n=4$ and every positive masses: finitely many positive (Theorem 1, Hampton–Moeckel) and even real (Theorem 5) normalized central configurations; finitely many complex ones unless the masses satisfy explicit polynomial relations (Theorem 3) or are all equal (Theorem 4).

Tools — Lemmas 1 and 2 and an explicit example

Lemma 1 (a polynomial image of an affine variety is finite or cofinite), Lemma 2 (the potential takes finitely many values on the solution set), and the explicit mass vector $(1,2,3,4,5)$ .

Significance

The result. Theorem 2 is the first finiteness result for planar central configurations of five bodies, settling Smale's 6th problem for $n=5$ for generic masses; before it, no single 5-tuple of positive masses was known to have finitely many planar central configurations. Its four-body part gives a short proof of the Hampton–Moeckel theorem, including the real (not necessarily positive) solutions.

Formalizing it. The results are proved on paper; none of them is formalized. A formal development requires affine elimination theory (Chevalley's theorem on constructible images in the form of Lemma 1), a Sard-type argument on algebraic sets (Lemma 2), and the singular-sequence analysis of Sections 3–9, which is a long case analysis of limiting diagrams together with polynomial eliminations done by computer algebra in the paper.

Difficulty

Finiteness is not a local statement: nondegeneracy fails in general (Palmore), so no implicit-function argument applies, and a continuum of solutions would have to be excluded globally. In the complex domain continua genuinely exist for some masses (Roberts' continuum with a negative mass; its sign-modified version with positive masses solves system (4)), so any proof must use the positivity of the masses in an essential way, and the exceptional mass set of Theorem 2 cannot simply be dropped with the present method.

Formalization scope

Bodies are indexed by Fin n; the paper's bodies $1$ and $2$ are the indices 0 and 1, so the normalisation reads y 1 - y 0 = 0.
Masses are real (and hypothesised positive) in all main theorems; in the definition of NormalizedCC they are complex, as in Section 2 of the paper. Lemma 2 carries the paper's standing hypothesis that no nonempty subset of bodies has total mass zero (NoZeroSubMass).
A point of system (4) is a triple (x, y, δ); δ is a full n × n array constrained to be symmetric with zero diagonal, so it carries exactly the $n(n-1)/2$ unknowns $\delta_{kl}$ , $k<l$ . Finiteness of the solution set is unaffected by this encoding.
"Closed algebraic subset of codimension 2 of the mass space" is encoded as the real zero locus massZeroLocus I of an ideal I of $\mathbb R[m_1,\dots,m_5]$ with ringKrullDim (ℝ[m] ⧸ I) ≤ 3. Taking $I=0$ is impossible (the quotient has dimension $5$ ), so the goal is not trivialised by an exceptional set equal to the whole mass space.
Finiteness is Set.Finite of the solution set.

Useful reusable infrastructure: finite-or-cofinite images of polynomial maps on affine varieties, and basic facts on central configurations (centre of mass, the identity $I=U$ ).

Selected references

A. Albouy, V. Kaloshin, Finiteness of central configurations of five bodies in the plane, Annals of Mathematics 176 (2012), 535–588. https://doi.org/10.4007/annals.2012.176.1.10
M. Hampton, R. Moeckel, Finiteness of relative equilibria of the four-body problem, Inventiones Mathematicae 163 (2006), 289–312. https://doi.org/10.1007/s00222-005-0461-0
S. Smale, Mathematical problems for the next century, The Mathematical Intelligencer 20 (1998), 7–15. https://doi.org/10.1007/BF03025291

10 thms2 active usersReviewed

Completed

Discrete Geometry Mathematical Physics·Captain: Lucas

Thomson Problem: Seven Electrons and the Known Exact SolutionsOpen Problem

Motivation

The Thomson problem asks for the configuration of $N$ electrons, constrained to the surface of the unit sphere and repelling each other according to Coulomb's law, that minimises the total electrostatic potential energy. J. J. Thomson posed it in 1904 in connection with his "plum pudding" atomic model. The same energy-minimisation question reappears in the arrangement of protein subunits in spherical virus shells, in colloidosomes, in fullerene patterns and in multi-electron bubbles, and it is a special case ( $s=1$ ) of the Riesz $s$ -energy problem on the sphere; the logarithmic variant is Smale's 7th problem.

Despite its elementary statement, the minimum is rigorously known only for a handful of values of $N$ .

Timeline of exact solutions (as reported in the source).

$N=1,2$ : trivial; for $N=2$ the optimum is an antipodal pair with $U=1/2$ .
$N=3$ : equilateral triangle on a great circle — L. Föppl (1912).
$N=4$ : regular tetrahedron (listed in the source without a citation).
$N=6$ : regular octahedron — V. A. Yudin (1992).
$N=12$ : regular icosahedron — N. N. Andreev (1996).
$N=5$ : triangular bipyramid — R. Schwartz (2013), computer-assisted.
$N=7$ : pentagonal bipyramid — long observed numerically; in September 2026 an exact, Lean-kernel-checked proof was claimed (H. Tran, Vals AI).
$N=8$ and $N=20$ : numerically, the optimum is not the cube, resp. the dodecahedron.

Setting

A configuration of $N$ points is a map $x:\{0,\dots,N-1\}\to\mathbb R^3$ . It is admissible if every point lies on the unit sphere, $\|x_i\|=1$ , and the points are pairwise distinct. In units with $e=1$ and $k_e=1$ its Coulomb energy is

U(x)=\sum_{0\le i<j\le N-1}\frac{1}{\|x_i-x_j\|}.

An admissible $x$ is an energy minimiser (solves the Thomson problem for $N$ ) if $U(x)\le U(y)$ for every admissible $N$ -point configuration $y$ .

Explicit candidate configurations are fixed in the definitions file: the antipodal pair ( $N=2$ ), an equatorial equilateral triangle ( $N=3$ ), the regular tetrahedron ( $N=4$ ), the triangular bipyramid ( $N=5$ ), the regular octahedron ( $N=6$ ), the pentagonal bipyramid ( $N=7$ : the two poles plus a regular pentagon $(\cos\tfrac{2\pi k}5,\sin\tfrac{2\pi k}5,0)$ on the equator) and the regular icosahedron ( $N=12$ ).

Formalization targets

Goal: $N=7$

\text{the pentagonal bipyramid is an energy minimiser for } N=7 .

This asserts admissibility of the seven points and the inequality $U(P_7)\le U(y)$ against every admissible seven-point configuration $y$ . It fixes no numerical value of the minimum and does not assert uniqueness.

Milestones: the other known exact solutions

N=1:\ U\equiv 0;\qquad N=2:\ \text{antipodal pair optimal},\ U=\tfrac12;

N=3,4,5,6,12:\ \text{triangle, tetrahedron, triangular bipyramid, octahedron, icosahedron are energy minimisers.}

Significance

The result. Among the values of $N$ listed in the source, $N=7$ is the smallest one whose optimum was, until the 2026 claim, supported only by numerical computation; the cases $N\le 6$ and $N=12$ were settled earlier. Settling $N=7$ extends the short list of rigorously known Thomson minimisers.

Formalizing it. The $N=7$ result reported in the source is recent and described there as a claimed Lean-kernel-checked proof; a formalization on this platform against a public, reviewed statement would corroborate it independently. For the milestones, the source attributes the $N=3,5,6,12$ cases to published proofs (Föppl 1912, Schwartz 2013, Yudin 1992, Andreev 1996); the source does not describe machine-checked proofs of these, and each is a self-contained formalization target.

Difficulty

The energy is a non-convex function on the configuration space $(S^2)^N$ with many critical points, so numerical minimisation — which is how most entries of the source's table of smallest known energies were obtained — does not certify global optimality. The $N=5$ case, the most recent classical entry before $N=7$ , was resolved only with a computer-assisted proof (Schwartz 2013).

Formalization scope

Points live in EuclideanSpace ℝ (Fin 3); configurations are functions Fin N → EuclideanSpace ℝ (Fin 3). Admissibility requires unit norm and injectivity (distinct points), matching the source's " $N$ distinct points". The energy sums $1/\mathrm{dist}(x_i,x_j)$ over $i<j$ ; Lean's $1/0=0$ convention is harmless because coincident points are excluded by admissibility. The candidate configurations are fixed in one particular orientation; since the energy is invariant under orthogonal maps and relabelling, this is no loss of generality. The statement " $x$ is an energy minimiser" includes admissibility of $x$ itself, so the goal cannot be satisfied by a degenerate candidate.

Reusable infrastructure welcome: energy invariance under isometries and permutations, existence of minimisers by compactness, linear-programming (Delsarte–Yudin) bounds on the sphere, and interval-arithmetic tooling for certified numerical bounds.

Selected references

Wikipedia, Thomson problem (source of this mission). https://en.wikipedia.org/wiki/Thomson_problem
J. J. Thomson, On the Structure of the Atom…, Philosophical Magazine 7 (1904), 237–265.
L. Föppl, Stabile Anordnungen von Elektronen im Atom, J. Reine Angew. Math. 141 (1912), 251–301. https://doi.org/10.1515/crll.1912.141.251
V. A. Yudin, The minimum of potential energy of a system of point charges, Discrete Math. Appl. 3 (1993), 75–81. https://doi.org/10.1515/dma.1993.3.1.75
N. N. Andreev, An extremal property of the icosahedron, East J. Approx. 2 (1996), 459–462.
R. Schwartz, The five-electron case of Thomson's problem, Experimental Mathematics 22 (2013), 157–186. https://arxiv.org/abs/1001.3702
S. Smale, Mathematical Problems for the Next Century, Math. Intelligencer 20 (1998), 7–15. https://doi.org/10.1007/bf03025291
Vals AI, A Lean Proof of the Thomson Problem for Seven Electrons (2026). https://www.vals.ai/blogs/thomson-n7-lean-proof

32 thms2 active usersReviewed

Completed

Functional Analysis·Captain: savarin

Sharp diagonal Hlawka constants: formalize the supplied proof at cutoff 90Research Paper

The Hlawka inequality for Schatten $p$ -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. The question is how large a comparison constant is needed to make this inequality hold.

This mission extends the best possible constant for complex diagonal matrices from $p\ge256$ to every real $p\ge90$ . The result is proved in Lean. The constant and its formula are unchanged from the foundation mission: the largest comparison constant required by the cyclic family of three $3\times3$ diagonal matrices. For each exponent, it works for every triple of diagonal matrices, whatever their size, and no smaller constant does.

The mission started from a supplied pen-and-paper proof. Lowering the cutoff took more than replacing 256 with 90: several estimates in the original argument had to be strengthened. The research note proves the bound for real entries first, then transfers it to complex entries and shows that the constant cannot be improved. The goal theorem below gives the exact formula and statement.

This is the second step of the sharp diagonal Hlawka campaign, and it reuses the foundation's definitions and supporting results. The campaign invites further improvements below 90, keeping the same formula.

The broader question of optimal constants for Schatten norms appears in Audenaert and Kittaneh’s Problem 7. Extending the sharp diagonal constant to general matrices is a separate challenge.

References

K. M. R. Audenaert and F. Kittaneh, Problems and Conjectures in Matrix and Operator Inequalities, arXiv preprint, 2012, §8.2, Problem 7. arXiv:1201.5232
Ezzeri Esa, Hlawka–Schatten inequalities: sharp diagonal construction, Lean source repository, 2026, revision 79aa498bfcf7b22bd91d771fb32ec278e2d4704b. Source library
Ezzeri Esa and project contributors, The cyclic bound for every real p ≥ 90, research note with appendices and exact certificates, 2026. Research note

Established results on Prove2Me

61 thms2 active usersReviewed

Convex Optimization Operations Research Optimization+1·Captain: mikedeng1

Introduction to the Scenario Approach III: The Risks of the Empirical Costs Follow an Ordered Dirichlet DistributionTextbook

Motivation

A scenario program replaces an uncertain optimization problem by its worst case over finitely many sampled instances. In its simplest form it reads

\min_{\nu\in\mathbb R^{d-1}}\Big[\max_{i=1,\dots,N}\ell(\nu,\delta_i)\Big],

where $\ell(\nu,\delta)$ is the cost of a decision $\nu$ when the uncertain parameter takes the value $\delta$ , and $\delta_1,\dots,\delta_N$ are independent draws from an unknown probability $\mathbb P$ . The classical guarantee of the scenario approach (Campi and Garatti, 2008) bounds the probability that a new instance produces a cost above the optimal value $\ell^*$ , and it does so without any knowledge of $\mathbb P$ .

That guarantee concerns a single number, $\ell^*$ . Two scenario programs with the same $N$ and the same optimal value can look very different at the solution: in one, most sampled costs lie just below $\ell^*$ ; in the other, they are widely scattered. The costs that do not determine the solution still carry information about how the cost of the chosen decision is distributed on future instances. Carè, Garatti and Campi (2015) showed that this information can be extracted with the same distribution-free character as the classical result, which is the subject of this mission. It is Chapter 8, §8.1 ("Probability box") of Campi and Garatti, Introduction to the Scenario Approach (SIAM/MOS 2018), the third mission of the series formalizing that book.

Timeline:

2008: Campi and Garatti prove that the violation of the scenario solution is dominated by a beta distribution $B(d,N-d+1)$ , with equality for fully supported problems (doi:10.1137/07069821X).
2015: Carè, Garatti and Campi prove that the risks of all empirical costs from index $d$ on have a joint ordered Dirichlet law (doi:10.1137/130928546).
2018: the book states the result as Theorem 8.4 and draws the probability box from it.

Setting

Let $\Delta$ be a measurable space with a probability $\mathbb P$ , and $\ell:\mathbb R^{d-1}\times\Delta\to\mathbb R$ a cost that is convex in $\nu$ for every $\delta$ (a standing assumption of the book). For a sample $(\delta_1,\dots,\delta_N)$ of independent draws from $\mathbb P$ , let $\nu^*$ be the solution of the program above and $\ell^*=\max_i\ell(\nu^*,\delta_i)$ its optimal value.

Empirical costs (Definition 8.1). Sort the costs of the solution on the sampled scenarios in decreasing order, $\ell^*_1\ge\ell^*_2\ge\dots\ge\ell^*_N$ ; so $\ell^*_1=\ell^*$ .

Risk (Definition 8.2). For a decision $\nu$ and a level $\ell$ , $R(\nu,\ell)=\mathbb P\{\delta:\ell(\nu,\delta)>\ell\}$ . The risk of the $k$ -th empirical cost is $R_k=R(\nu^*,\ell^*_k)$ , and $R_1\le R_2\le\dots\le R_N$ .

Nondegeneracy (Definition 8.3). For every $N\ge d$ , with probability $1$ , $\ell^*_d\ne\ell^*_{d+1}\ne\dots\ne\ell^*_N$ . Costs with index below $d$ are excluded because several scenarios typically attain the maximum at $\nu^*$ .

Support constraints and full support (Definitions 5.1 and 5.4). In epigraph form, $\min t$ subject to $t\ge\ell(\nu,\delta_i)$ , the constraint of scenario $i$ is a support constraint if removing it lowers the optimal value; the problem is fully supported if for every $m\ge d$ the program with $m$ scenarios has exactly $d$ support constraints with probability $1$ .

The ordered Dirichlet distribution with parameters $(d,1,\dots,1)$ is the law on $\{0\le\alpha_d\le\dots\le\alpha_N\le1\}$ with density $\frac{N!}{(d-1)!}\alpha_d^{d-1}$ .

Formalization targets

Goal: Theorem 8.4

Under nondegeneracy, for $N\ge d$ and all $\varepsilon_d,\dots,\varepsilon_N$ ,

\mathbb P^N\{R_d\le\varepsilon_d,\dots,R_N\le\varepsilon_N\}=\frac{N!}{(d-1)!}\int_0^{\varepsilon_d}\alpha_d^{d-1}\int_0^{\varepsilon_{d+1}}\!\!\cdots\int_0^{\varepsilon_N}\mathbf 1_{\{0\le\alpha_d\le\dots\le\alpha_N\le1\}}\,\mathrm d\alpha_N\cdots\mathrm d\alpha_d .

This is an identity of joint distribution functions, not a bound, and it does not depend on $\ell$ or $\mathbb P$ .

Milestones

Theorem 3.7 for the min-max program: $\mathbb P^N\{R(\nu^*,\ell^*)>\varepsilon\}\le\sum_{i=0}^{d-1}\binom Ni\varepsilon^i(1-\varepsilon)^{N-i}$ for $\varepsilon\in[0,1]$ .
Fully supported problems: $\ell^*=\ell^*_d$ with probability $1$ .
Marginal of $R_d$ (a corollary of the goal): $\mathbb P^N\{R_d\le\varepsilon\}=1-\sum_{i=0}^{d-1}\binom Ni\varepsilon^i(1-\varepsilon)^{N-i}$ , the beta law $B(d,N-d+1)$ .

Significance

The result. The theorem controls the whole distribution function of the cost $\ell(\nu^*,\delta)$ of the scenario solution on a new instance, not just one quantile of it. Discarding the extreme tails of the laws of $R_d,\dots,R_N$ yields, with a prescribed confidence $1-\beta$ , a region (the book's "probability box", Figure 8.2) that contains the entire cumulative distribution function of $\ell(\nu^*,\delta)$ , computed from the sample alone. The first marginal recovers the classical Theorem 3.7, since $\ell^*\ge\ell^*_d$ makes the risk of $\ell^*$ at most $R_d$ .

Formalizing it. The theorem is proved in Carè, Garatti and Campi (2015); the book states it and gives no proof. No machine-checked version of the scenario approach, of its generalization theorem, or of ordered Dirichlet laws of risks is known to exist. A formalization would produce a checked proof of the distribution-free identity together with the combinatorial and measure-theoretic infrastructure (order statistics of sampled costs, laws of random risks) that the rest of scenario theory reuses. The milestones separate the classical beta bound, which is also the goal of the first mission of this series, from the new exact joint law.

Difficulty

The obvious attempt treats $R_d,\dots,R_N$ as the order statistics of the uniform variables $1-F(\ell(\nu^*,\delta_i))$ . That works only for $d=1$ , when the decision space is a point and the costs are independent. For $d\ge2$ the decision $\nu^*$ is itself a function of the whole sample, so the sampled costs at $\nu^*$ are neither independent nor identically distributed, and the $d$ -th cost is tied to the scenarios that determine the solution. The factor $\alpha_d^{d-1}$ and the constant $N!/(d-1)!$ encode exactly this dependence. Any argument must account for which scenarios are active at $\nu^*$ without assuming full support, since the theorem holds whether or not $\ell^*=\ell^*_d$ .

Formalization scope

The decision space is EuclideanSpace ℝ (Fin n) and the book's $d$ is $n+1$ ; the sample is ω : Fin N → Δ with law Measure.pi (fun _ => P). Empirical costs are read from Tuple.sort with $k$ counted from $1$ ; risks are real numbers (P {δ | c < ℓ ν δ}).toReal. The right-hand side of the goal is a Lebesgue integral over the box $\prod_k[0,\varepsilon_k]$ intersected with the ordered simplex, stated for all real $\varepsilon_k$ . The solution map $\omega\mapsto\nu^*$ is a hypothesis-constrained function, never an arbitrary map.

Implicit hypotheses of the book pinned down in the binders:

$\ell(\cdot,\delta)$ is convex for every $\delta$ (p. 6).
Existence and uniqueness of the solution of the program for every sample size $m\ge1$ and every sample; the book's Assumption 3.6 says "every $m$ ", but the program with no scenario has no solution.
Nondegeneracy for every sample size $m\ge d$ , not only for the $N$ of the theorem, as Definition 8.3 is written.
Joint measurability of $(\nu,\delta)\mapsto\ell(\nu,\delta)$ and measurability of the solution map (measurability is glossed over in the book, p. 6 footnote 1 and p. 33).
$N\ge d$ , and $\varepsilon\in[0,1]$ in the binomial-form statements.

A statement in which the solution is an arbitrary measurable map, or in which the nondegeneracy or existence hypothesis is unsatisfiable, would make the goal vacuous; the hypotheses here are met, for example, by $\ell(\nu,\delta)=\|\nu-\delta\|^2$ with a continuous law on $\mathbb R^{n}$ , and for $d=1$ by any cost independent of $\nu$ with an atomless law.

A complete development needs: the scenario approach generalization theorem (reusable across this series), laws of order statistics of i.i.d. uniform variables, and the combinatorics of support sets of convex min-max programs. Proofs of the milestones, of the $d=1$ case of the goal, and of auxiliary facts about kthLargest are all welcome.

Selected references

M. C. Campi, S. Garatti, Introduction to the Scenario Approach, MOS-SIAM Series on Optimization 26, SIAM, 2018. doi:10.1137/1.9781611975444
A. Carè, S. Garatti, M. C. Campi, Scenario min-max optimization and the risk of empirical costs, SIAM J. Optim. 25(4):2061–2080, 2015. doi:10.1137/130928546
M. C. Campi, S. Garatti, The exact feasibility of randomized solutions of uncertain convex programs, SIAM J. Optim. 19:1211–1230, 2008. doi:10.1137/07069821X

10 thms2 active usersReviewed

Numerical Analysis Probability Stochastic Systems·Captain: mikedeng1

Euler Approximations with Varying Coefficients III: Uniform Lq-Convergence with Order 1/2Research Paper

Motivation

Stochastic differential equations whose coefficients grow faster than linearly (for instance stochastic volatility models such as the 3/2-model) cannot be simulated with the classical explicit Euler–Maruyama scheme: Hutzenthaler, Jentzen and Kloeden showed that its moments diverge when the drift or diffusion grows superlinearly (Proc. R. Soc. A, 2011). Implicit schemes avoid the divergence but require solving a nonlinear equation at every step. Tamed Euler schemes keep the scheme explicit and damp the coefficients by a factor depending on the step size.

2012: Hutzenthaler, Jentzen and Kloeden introduce a tamed Euler scheme for SDEs with superlinearly growing drift (Ann. Appl. Probab. 22, 2012).
2013: Sabanis extends the taming analysis for superlinearly growing drift (Electron. Commun. Probab. 18, no. 10, 2013, MR3070913).
2015: Hutzenthaler and Jentzen survey explicit schemes for non-globally Lipschitz coefficients (Mem. Amer. Math. Soc. 236, no. 1112, 2015); for the 3/2-model their results give $\mathcal L^p$ -convergence without rate only for $p<1/2$ , as Sabanis (2016, p. 2) notes.
2016: Sabanis (Ann. Appl. Probab. 26(4), 2016, arXiv:1308.1796v4) treats schemes with varying coefficients $b_n,\sigma_n$ , covering superlinearly growing diffusion coefficients, and proves $\mathcal L^p$ convergence (Theorem 1), the $\mathcal L^p$ rate 1/2 (Theorem 2) and the uniform $\mathcal L^q$ rate 1/2 (Theorem 3). A motivating example is the $d$ -dimensional analogue of the 3/2-model of stochastic volatility, $dX=\lambda X(\mu-|X|)\,dt+\xi|X|^{3/2}\,dW$ , used for pricing VIX options.

Theorem 3 is the target here; Theorems 1 and 2 are the targets of companion missions.

Setting

Fix a filtered probability space $(\Omega,\{\mathcal F_t\}_{t\ge0},\mathcal F,P)$ satisfying the usual conditions, a $d_1$ -dimensional Wiener martingale $W$ , a horizon $T>0$ , and exponents $p_0,p_1\ge2$ . For $x\in\mathbb R^d$ , $|x|$ is the Euclidean norm; for a $d\times d_1$ matrix $A$ , $|A|$ is the Hilbert–Schmidt norm; $xy$ is the scalar product. The coefficients are Borel functions $b:[0,\infty)\times\mathbb R^d\to\mathbb R^d$ and $\sigma:[0,\infty)\times\mathbb R^d\to\mathbb R^{d\times d_1}$ , and the SDE is

dX(t)=b(t,X(t))\,dt+\sigma(t,X(t))\,dW(t),\qquad t\in[0,T],\qquad(2.1)

with an $\mathcal F_0$ -measurable initial value $X(0)$ . With $\kappa_n(t)=\lfloor nt\rfloor/n$ , the scheme (2.2) is

dX_n(t)=b_n(t,X_n(\kappa_n(t)))\,dt+\sigma_n(t,X_n(\kappa_n(t)))\,dW(t),\qquad X_n(0)=X(0),

and in this mission $b_n,\sigma_n$ are the tamed coefficients of Model 2 with $\alpha=1/2$ :

b_n(t,x)=\frac{b(t,x)}{1+n^{-1/2}|x|^l},\qquad \sigma_n(t,x)=\frac{\sigma(t,x)}{1+n^{-1/2}|x|^l}.

The conditions used are: A-2, local boundedness of $b$ on balls; A-4, the coercivity bound $2xb(t,x)+(p_0-1)|\sigma(t,x)|^2\le K(1+|x|^2)$ ; A-5, $\mathbb E|X(0)|^{p_0}<\infty$ ; and A-6, the global monotonicity

2(x-y)(b(t,x)-b(t,y))+(p_1-1)|\sigma(t,x)-\sigma(t,y)|^2\le L|x-y|^2

together with the polynomial Lipschitz bound $|b(t,x)-b(t,y)|\le L(1+|x|^l+|y|^l)|x-y|$ , with $l,L>0$ . The $\mathfrak p$ -condition asks $l\le\frac{p_0-2}{4}$ and a moment exponent $p$ with $0<p<p_1$ and $p\le\frac{p_0}{2l+1}$ .

Formalization targets

Goal: Theorem 3 (p. 6)

Under A-2, A-4–A-6 and the $\mathfrak p$ -condition, for every $0<q<p$ there is $C$ independent of $n$ with

\mathbb E\Big[\sup_{0\le t\le T}|X(t)-X_n(t)|^q\Big]\le Cn^{-q/2},\qquad n\ge1.\qquad(2.14)

The supremum is inside the expectation, which distinguishes it from Theorem 2.

Milestones

Lemma 2 (p. 8): the moments of $X$ and of $X_n$ up to order $p_0$ are bounded on $[0,T]$ uniformly in $n$ (for general coefficients $b_n,\sigma_n$ under A-1–A-5, B-2, B-3).
Lemma 5 (p. 19): the Gyöngy–Krylov maximal inequality. If nonnegative continuous adapted $f,g$ satisfy $\mathbb E[f_\tau\mathbb 1_{\{g_0\le c\}}]\le\mathbb E[g_\tau\mathbb 1_{\{g_0\le c\}}]$ for all $c>0$ and stopping times $\tau\le T$ , then

\mathbb E\Big[\sup_{t\le\tau}f_t^\gamma\Big]\le\frac{2-\gamma}{1-\gamma}\,\mathbb E\Big[\sup_{t\le\tau}g_t^\gamma\Big],\qquad\gamma\in(0,1).

Lemma 4 (p. 16): $\sup_{0\le t\le T}\mathbb E|X_n(t)-X_n(\kappa_n(t))|^p\le Cn^{-p/2}$ .
Lemma 3 (p. 15): the taming errors $\mathbb E\int_0^T|b-b_n|^p(s,X_n(\kappa_n(s)))\,ds$ and the analogue for $\sigma$ are $\le Cn^{-\alpha p}$ .

Significance

Theorem 3 gives the optimal strong rate 1/2 for an explicit scheme, uniformly over the time interval, for SDEs whose diffusion coefficient may grow superlinearly. Uniform-in-time error bounds are what pathwise functionals need (running maxima, barrier options, hitting times), and via Borel–Cantelli they give the almost-sure rate of Corollary 1 in the paper. Lemma 5 is a general-purpose tool: a domination inequality of Lenglart type, used throughout stochastic analysis to pass from bounds at stopping times to bounds on running suprema.

The results are proved in the paper; to our knowledge none of them has been formalized. Formalizing them would produce the first machine-checked convergence rate of a numerical scheme for SDEs, and a Lean proof of a Lenglart-type inequality, which Mathlib does not currently contain.

Difficulty

The error $X-X_n$ is controlled by the monotonicity condition A-6, which is one-sided: it bounds $2(x-y)(b(t,x)-b(t,y))$ from above but gives no Lipschitz bound on $b$ or $\sigma$ with a constant independent of $|x|,|y|$ . The first idea, estimating $\mathbb E\sup_t|X-X_n|^p$ directly by applying the Burkholder–Davis–Gundy inequality to the martingale part of the error equation, therefore does not close: it produces terms of the same order as the quantity being estimated, weighted by polynomial factors in $|X|$ and $|X_n|$ , and the argument that gives Theorem 2 controls $\mathbb E|X(t)-X_n(t)|^p$ only for fixed $t$ . Passing from fixed times to the supremum is what forces the loss from $p$ to $q<p$ in Theorem 3, and it is where Lemma 5 enters. On the formal side, the Itô integral against Brownian motion, Itô's formula for functions of multidimensional Itô processes and the Burkholder–Davis–Gundy inequality are not in Mathlib.

Formalization scope

Processes are indexed by $t\in[0,\infty)$ (ℝ≥0) with values in EuclideanSpace ℝ (Fin d); diffusion values live in EuclideanSpace ℝ (Fin d × Fin d₁), whose norm is the Hilbert–Schmidt norm. The stochastic integral is the Ethier–Kurtz platform relation EthierKurtz.HasBrownianItoIntegral, applied coordinatewise, with integrands cut off after $T$ . Solutions are hypotheses: the theorems apply to any solution $X$ of (2.1) and any family $(X_n)_{n\ge1}$ of solutions of (2.2) on one probability space with one $W$ and one $X(0)$ ; existence is not claimed. Processes are required to be adapted to the filtration augmented by null sets (weaker than a complete filtration), the filtration is right-continuous, and nothing is required after $T$ . Expectations and suprema are computed in $[0,\infty]$ , so no statement holds through an integral defaulting to $0$ . Constants $C$ depend on everything except $n$ (and, in Theorem 3, may depend on $q$ ); only $n\ge1$ is used, and $q>0$ , $p>0$ follow the paper's $\mathcal L^p$ convention.

Two hypotheses are added to the printed statements, both because the printed proofs need them:

$p_1>2$ in Theorem 3. The proof applies Itô's formula for $p\ge2$ ; an admissible $p<2$ is handled through $p'=2$ , which satisfies the $\mathfrak p$ -condition exactly when $p_1>2$ .
B-3 in Lemma 4. The proof uses moment bounds uniform in $n$ (Lemma 2), which need B-3. Model 2 satisfies B-3.

Lemma 2 drops the dependence clause $C=C(p,T,K,\mathbb E|X(0)|^p)$ and asserts only finiteness. Lemma 5 assumes neither that $g$ is nondecreasing nor anything beyond the printed hypotheses.

A trivializing formalization is ruled out: the supremum sits inside a Lebesgue integral in $[0,\infty]$ , so the goal cannot hold because of a junk value, and the hypotheses are satisfiable (zero coefficients, constant solutions), which a sorry-free check confirms.

Needed infrastructure: Itô's formula for multidimensional Itô processes, the Burkholder–Davis–Gundy inequality (for Lemma 4), Gronwall's inequality in integral form, and stopping-time localisation for continuous adapted processes. Contributions to any of these are welcome, and all are reusable far beyond this mission. Lemma 5 is independent of the SDE part and can be attacked first.

Selected references

S. Sabanis, Euler approximations with varying coefficients: the case of superlinearly growing diffusion coefficients, Ann. Appl. Probab. 26(4), 2083–2105, 2016. https://doi.org/10.1214/15-AAP1140 — arXiv:1308.1796v4, https://arxiv.org/abs/1308.1796v4
M. Hutzenthaler, A. Jentzen, P. E. Kloeden, Strong and weak divergence in finite time of Euler's method for stochastic differential equations with non-globally Lipschitz continuous coefficients, Proc. R. Soc. A 467, 1563–1576, 2011. https://doi.org/10.1098/rspa.2010.0348
M. Hutzenthaler, A. Jentzen, P. E. Kloeden, Strong convergence of an explicit numerical method for SDEs with nonglobally Lipschitz continuous coefficients, Ann. Appl. Probab. 22(4), 1611–1641, 2012. https://doi.org/10.1214/11-AAP803
M. Hutzenthaler, A. Jentzen, Numerical approximations of stochastic differential equations with non-globally Lipschitz continuous coefficients, Mem. Amer. Math. Soc. 236, no. 1112, 2015 (reference [5] of the paper).
S. Sabanis, A note on tamed Euler approximations, Electron. Commun. Probab. 18, no. 10, 2013. MR3070913
I. Gyöngy, N. V. Krylov, On the rate of convergence of splitting-up approximations for SPDEs, in Stochastic Inequalities and Applications, Progr. Probab. 56, 301–321, Birkhäuser, 2003 (cited by the paper for Lemma 5). MR2073438
N. V. Krylov, Introduction to the Theory of Diffusion Processes, Transl. Math. Monographs 142, AMS, 1995 (cited by the paper for Lemma 5). MR1311478

14 thms2 active usersReviewed

Completed

Markov Chain Probability Statistics·Captain: mikedeng1

A Note on Metropolis–Hastings Kernels for General State Spaces III: The Maximal Kernel of a Mixture Proposal Dominates the Mixture of Maximal Kernels Off the DiagonalResearch Paper

Motivation

A Markov chain Monte Carlo sampler is often assembled from simpler parts. A practitioner who has several proposal mechanisms $Q_1, Q_2, \dots$ for a Metropolis–Hastings sampler can combine them in two ways. Either each $Q_i$ drives its own Metropolis–Hastings kernel $P_i$ and the sampler picks kernel $P_i$ with probability $\beta_i$ at each step, or the mixture $Q = \sum_i \beta_i Q_i$ is used as a single proposal inside one Metropolis–Hastings kernel. Both samplers leave the target $\pi$ invariant, so the choice is about efficiency.

Section 4 of Tierney (1998) settles the comparison: when both samplers use the maximal acceptance probability, the second never does worse in terms of asymptotic variances of sample-path averages. The statement that carries this is Proposition 5, an ordering of kernels in Peskun's off-diagonal order; the variance comparison then follows from Theorem 4 of the same paper, the general-state-space extension of Peskun (1973).

Timeline. Peskun (1973) introduced off-diagonal domination for finite state spaces and showed that the Metropolis–Hastings acceptance probability is maximal in that order. A version of Proposition 5 for discrete chains appears in the appendix of Tierney (1991) and in the rejoinder of Besag, Green, Higdon and Mengersen (1995). Tierney (1998) states and proves it for general state spaces, using the measure-theoretic description of Metropolis–Hastings kernels from §2 of the same paper.

Setting

Let $(E, \mathcal E)$ be a measurable space and $\pi$ a probability measure on it, the target. A proposal kernel $Q(x, dy)$ is a Markov kernel on $E$ . Given a measurable acceptance probability $\alpha : E \times E \to [0,1]$ , the Metropolis–Hastings kernel is

P(x, dy) = Q(x, dy)\,\alpha(x, y) + \delta_x(dy) \int \bigl(1 - \alpha(x, u)\bigr)\, Q(x, du),

where $\delta_x$ is the point mass at $x$ (mhKernel Q α).

Put $\mu(dx, dy) = \pi(dx) Q(x, dy)$ and $\mu^T(dx, dy) = \mu(dy, dx)$ . With $\nu = \mu + \mu^T$ and $h = d\mu/d\nu$ (canonDensity), let

R = \{(x, y) : h(x, y) > 0,\ h(y, x) > 0\},\qquad r(x, y) = h(x, y)/h(y, x) \text{ on } R,\quad r = 1 \text{ on } R^c

(canonR, canonRatio). The set $R$ is symmetric, $\mu$ and $\mu^T$ are mutually absolutely continuous on $R$ and mutually singular off it (Proposition 1 of the paper). The Metropolis–Hastings acceptance probability is

\alpha_{MH}(x, y) = \min\{1, r(y, x)\} \text{ if } (x, y) \in R, \qquad \alpha_{MH}(x, y) = 0 \text{ otherwise}

(alphaMH π Q), and the kernel with $\alpha = \alpha_{MH}$ is the maximal Metropolis–Hastings kernel for $Q$ (maxMHKernel π Q).

For kernels $P_1, P_2$ on $E$ , $P_1$ dominates $P_2$ off the diagonal, $P_1 \succeq P_2$ (OffDiagDominates π P₁ P₂), if for $\pi$ -almost every $x$ , $P_1(x, A \setminus \{x\}) \ge P_2(x, A \setminus \{x\})$ for all $A \in \mathcal E$ . For a countable family of kernels $K_i$ and weights $\beta_i \ge 0$ , the mixture $\sum_i \beta_i K_i$ is the kernel $x \mapsto \sum_i \beta_i K_i(x, \cdot)$ (mixKernel β K).

Formalization targets

Goal: Proposition 5

Let $Q_i$ be a finite or countable family of proposal kernels and $\beta_i \ge 0$ with $\sum_i \beta_i = 1$ . Let $P_i$ be the maximal Metropolis–Hastings kernel for $Q_i$ and $P$ the maximal Metropolis–Hastings kernel for $Q = \sum_i \beta_i Q_i$ . Then

P \succeq \sum_i \beta_i P_i .

Both sides use maximal kernels: $P$ uses $\alpha_{MH}$ of the mixture proposal, each $P_i$ its own $\alpha^{(i)}_{MH}$ , and the same weights $\beta_i$ form both mixtures.

Milestones

The construction in the proof of Proposition 1 (p. 2) yields a set $R$ and ratio $r$ with the properties of Proposition 1 for $\mu = \pi \otimes Q$ .
$\alpha_{MH}$ satisfies conditions (i) and (ii) of Theorem 2 (p. 3): $\alpha_{MH} = 0$ $\mu$ -a.e. on $R^c$ , and $\alpha_{MH}(x, y) r(x, y) = \alpha_{MH}(y, x)$ $\mu$ -a.e. on $R$ .
The maximal kernel satisfies detailed balance, $\pi(dx) P(x, dy) = \pi(dy) P(y, dx)$ .
For any symmetric $\sigma$ -finite $\nu$ dominating $\mu$ , with $h = d\mu/d\nu$ :

\pi(dx) Q(x, dy)\, \alpha_{MH}(x, y) = \min\{h(y, x), h(x, y)\}\, \nu(dx, dy).

As measures on $E \times E$ :

\pi(dx) Q(x, dy)\, \alpha_{MH}(x, y) \ge \sum_i \beta_i\, \pi(dx) Q_i(x, dy)\, \alpha^{(i)}_{MH}(x, y).

A companion item states the maximality of $\alpha_{MH}$ (§3, p. 7): every measurable acceptance probability $\alpha$ whose kernel is reversible satisfies $\alpha \le \alpha_{MH}$ $\mu$ -a.e., so the maximal kernel dominates every reversible Metropolis–Hastings kernel with the same proposal.

Significance

The result. Proposition 5, combined with Theorem 4 of the paper (off-diagonal domination orders asymptotic variances of reversible kernels), shows that for every function $f$ with finite variance the asymptotic variance of $\frac1n \sum_{k} f(X_k)$ under the mixture-proposal sampler is at most that under the mixture of samplers. Per-iteration cost can be higher for the mixture proposal, since $\alpha_{MH}$ then needs the densities of all components; Proposition 5 isolates the statistical side of that trade-off. The maximality companion states the fact behind the name "maximal kernel": $\alpha_{MH}$ is the largest acceptance probability that keeps a Metropolis–Hastings kernel reversible.

Formalizing it. The paper's proof is a computation of about six lines with Radon–Nikodym densities. A formal version must make explicit what the computation leaves implicit: that $\alpha_{MH}$ , defined from one dominating measure, has the same density form for every symmetric dominating measure; that the measure inequality on $E \times E$ passes to the kernel-level statement with one null set for all $A$ ; and that the mixture proposal and the mixture of kernels are handled as countable sums of kernels. As of September 2026 neither Mathlib nor this platform has a machine-checked version of Proposition 5, of the maximality of $\alpha_{MH}$ , or of reversibility of the Metropolis–Hastings kernel on a general state space; only finite-state Metropolis chains have been formalized on the platform.

Difficulty

The obvious argument works pointwise with densities: write every kernel as a density against a common reference measure and compare $\min\{\cdot, \cdot\}$ of sums with sums of minima. On a general state space there is no common reference measure given in advance, and $\alpha_{MH}$ is only defined up to $\mu$ -null sets, through a Radon–Nikodym derivative with respect to $\mu + \mu^T$ , a measure that differs for $Q$ and for each $Q_i$ . The step that needs care is relating these different versions: the densities $h_i$ of the $\mu_i$ against a common symmetric $\nu$ , the density of $\mu = \sum_i \beta_i \mu_i$ , and the transpose densities $h(y, x)$ , which are densities of $\mu^T$ only because $\nu$ is symmetric.

The second difficulty is the passage from measures to kernels. The inequality between measures on $E \times E$ gives, for each fixed $A$ , the kernel inequality for $\pi$ -almost every $x$ , with a null set that depends on $A$ . The order $\succeq$ requires one null set for all $A$ , and the diagonal must be removed, which needs the diagonal to be measurable.

Formalization scope

The formalization is in Lean 4 with Mathlib, in the namespace TierneyMH.Mixture. The state space is a type E with a σ-algebra; π is a probability measure; proposal kernels are Markov kernels Kernel E E. Acceptance probabilities and densities take values in $[0, \infty]$ (ℝ≥0∞); a general $\alpha$ is assumed measurable with $\alpha \le 1$ . $\mu$ is π ⊗ₘ Q, $\mu^T$ its image under Prod.swap, detailed balance is Kernel.IsReversible. Mixtures are indexed by a countable type ("a sequence", which includes finite families), with weights in ℝ≥0 and HasSum β 1.

Added hypotheses, both labelled in the statements: singletons are measurable (implicit in the paper's $A \setminus \{x\}$ and $\delta_x$ ), on the goal and the maximality companion; and, on the goal only, the σ-algebra of $E$ is countably generated. The second is an addition to the paper: it is what makes the exceptional null set in $\succeq$ uniform over $A$ in the passage from the measure inequality to the kernels. It is not assumed in the measure-level milestones.

$\alpha_{MH}$ is one fixed version, built from Mathlib's rnDeriv exactly as in the proof of Proposition 1 (with $\nu = \mu + \mu^T$ , not an arbitrary dominating measure), and all statements are insensitive to the version. The ratio $r$ is set to 1 on the null subset of $R$ where $h$ is infinite, so that $0 < r < \infty$ and $r(x, y) = 1/r(y, x)$ hold everywhere, as Proposition 1 asks.

Trivializations ruled out: $\alpha_{MH}$ is the indicator of $R$ times $\min\{1, r(y, x)\}$ , never an arbitrary acceptance function or a single $\alpha$ shared by all components; $\succeq$ compares $A \setminus \{x\}$ , not $A$ (on $A$ the rejection masses differ and the comparison is false); and the conclusion is about the Metropolis–Hastings kernels themselves, not about the measure identity alone. All hypotheses are satisfiable, for instance on $E$ = Bool with $\pi$ uniform, two proposals $Q_1 = \pi$ and $Q_2 = \delta_x$ and weights $(1/2, 1/2)$ .

Needed infrastructure, reusable for other Metropolis–Hastings results: Radon–Nikodym calculus for product measures and their transposes, countable sums of kernels, and a monotone-class argument over a countable generating family. The Metropolis–Hastings kernel, $R$ , $r$ and off-diagonal domination are defined identically in the companion missions I (detailed balance, Theorem 2) and II (Peskun ordering, Theorem 4) of this series. Proofs of milestones in any order, and proofs of the goal from the milestones, are welcome.

Selected references

L. Tierney, A Note on Metropolis–Hastings Kernels for General State Spaces, The Annals of Applied Probability 8(1), 1998, 1–9. https://doi.org/10.1214/aoap/1027961031
P. H. Peskun, Optimum Monte Carlo sampling using Markov chains, Biometrika 60(3), 1973, 607–612. https://doi.org/10.1093/biomet/60.3.607
J. Besag, P. Green, D. Higdon, K. Mengersen, Bayesian computation and stochastic systems (with discussion), Statistical Science 10(1), 1995, 3–66. https://doi.org/10.1214/ss/1177010123
W. K. Hastings, Monte Carlo sampling methods using Markov chains and their applications, Biometrika 57(1), 1970, 97–109. https://doi.org/10.1093/biomet/57.1.97
N. Metropolis, A. W. Rosenbluth, M. N. Rosenbluth, A. H. Teller, E. Teller, Equations of state calculations by fast computing machines, J. Chemical Physics 21, 1953, 1087–1091. https://doi.org/10.1063/1.1699114

16 thms2 active usersReviewed

Completed

Number Theory Probability Quantum Information+1·Captain: mikedeng1

Polynomial-Time Algorithms for Prime Factorization and Discrete Logarithms on a Quantum Computer 4: The Discrete Logarithm Circuit Gives a Good Output with Probability at Least 1/480Research Paper

Motivation

The discrete logarithm problem modulo a prime asks, given a prime $p$ , a generator $g$ of the multiplicative group modulo $p$ , and a nonzero residue $x$ , for the exponent $r$ with $g^r\equiv x \pmod p$ . Its presumed classical hardness underlies Diffie–Hellman key exchange, ElGamal encryption and the Digital Signature Algorithm. The best classical algorithm known when Shor wrote, Gordon's adaptation of the number field sieve, runs in time $\exp(O((\log p)^{1/3}(\log\log p)^{2/3}))$ .

In §6 of Polynomial-Time Algorithms for Prime Factorization and Discrete Logarithms on a Quantum Computer (SIAM J. Comput. 26(5), 1997; doi:10.1137/S0097539795293172, arXiv:quant-ph/9508027), Shor gave a quantum algorithm that uses two modular exponentiations and two quantum Fourier transforms and outputs, with constant probability, a pair from which $r$ can be computed. The quantitative core of that analysis is a single number: the circuit produces a "good" output with probability at least $1/480$ . This mission formalizes that bound and the three estimates it is assembled from.

Setting

Let $p$ be a prime and $g$ a generator of $(\mathbb Z/p\mathbb Z)^\times$ , so that $1,g,\dots,g^{p-2}$ are all the nonzero residues. Fix the unknown $r$ with $0\le r<p-1$ and put $x=g^r$ . Let $q=2^l$ be the power of $2$ with $p<q<2p$ .

The Fourier matrix $A_q$ is the $q\times q$ matrix with entries $(A_q)_{a,c}=q^{-1/2}\exp(2\pi i\,ac/q)$ for $0\le a,c<q$ (§4, eq. (4.1)). Rows index input basis vectors and columns output basis vectors.

The algorithm uses three registers: two holding numbers $0\le a,b<q$ and one holding a nonzero residue modulo $p$ . It starts from the state

\frac{1}{p-1}\sum_{a=0}^{p-2}\sum_{b=0}^{p-2}|a,b,g^ax^{-b}\ (\mathrm{mod}\ p)\rangle \qquad (6.1)

(preFourierState), applies $A_q$ to each of the first two registers (finalState), and measures all three registers. The probability of observing $|c,d,y\rangle$ is the squared modulus of its amplitude (outcomeProb).

For integers $z$ and $q>0$ , the symmetric residue $\{z\}_q$ is the residue of $z$ modulo $q$ in $(-q/2,q/2]$ (symmRes). Put

T=rc+d-\frac{r}{p-1}\{c(p-1)\}_q .

An observed state $|c,d,y\rangle$ is good (IsGood) when

|\{T\}_q|\le\tfrac12 \quad (6.10) \qquad\text{and}\qquad |\{c(p-1)\}_q|\le q/12 \quad (6.11).

Goodness depends only on $(c,d)$ .

Formalization targets

Goal: a good output with probability at least $1/480$ (§6, p. 1504)

\sum_{\substack{0\le c,d<q\\ (c,d)\ \text{good}}}\ \sum_{y\in(\mathbb Z/p)^\times}\Pr[c,d,y]\ \ge\ \frac1{480}.

The constant is the one the page carries forward. The goal fixes no threshold on $p$ : it is stated for every prime $p$ that admits a power of two strictly between $p$ and $2p$ .

Milestones

The output distribution, eq. (6.4). For $0\le k<p-1$ ,

\Pr[c,d,g^k]=\left|\frac{1}{(p-1)q}\sum_{\substack{0\le a,b\le p-2\\ a-rb\equiv k\ (p-1)}}\exp\Bigl(\frac{2\pi i}{q}(ac+bd)\Bigr)\right|^2 .

Each good state is likely, eq. (6.17). If $(c,d)$ is good, then $\Pr[c,d,y]\ge 1/(20q^2)$ for every $y$ .
Many good pairs (p. 1504). At least $q/12$ pairs $(c,d)$ are good.
Each good $c$ is likely (p. 1504). If $(c,d)$ is good for some $d$ , then $\sum_{d',y}\Pr[c,d',y]\ge(p-1)/(20q^2)\ge1/(40q)$ .

Significance

The result. The bound $1/480$ is what turns the circuit into an algorithm. Repeating the circuit $O(1)$ times in expectation yields a good output, and from a good pair $(c,d)$ one reads off an equation that determines $r$ modulo divisors of $p-1$ (§6, eqs. (6.18)–(6.20)). Together with the quantum Fourier transform circuit and reversible modular exponentiation, this places the discrete logarithm modulo a prime in quantum polynomial time. Every later analysis of quantum attacks on discrete-logarithm cryptography starts from this success probability or a sharpened version of it.

Formalizing it. The result has been proved since 1994–1997 and is textbook material; it is not open. As far as is known, no machine-checked proof of Shor's discrete-logarithm analysis exists. The paper's proof of eq. (6.17) replaces a sum by an integral with an error term $O(W/(pq))$ whose constant is not given, yet states $1/(20q^2)$ for every prime. A formal proof must therefore either control that error explicitly or find another argument, and so settles a point the paper leaves informal. Numerically, the smallest value of $q^2\Pr[c,d,y]$ over good states is about $0.49$ for all primes $p<90$ , so the unconditional claim is not in doubt for small $p$ . The page also contains two small slips, recorded under Formalization scope; a complete development pins down exactly what is true.

Difficulty

The exponential sum (6.4) runs over pairs $(a,b)$ satisfying a congruence modulo $p-1$ , while the phases are taken modulo $q$ . The two moduli are unrelated: $q$ is a power of two and $p-1$ is arbitrary. Eliminating $a$ through the congruence introduces a floor function $\lfloor(br+k)/(p-1)\rfloor$ , and the resulting phase is not linear in $b$ . The obvious estimate treats the sum as a geometric series in $b$ and bounds it by its first-order phase; this fails because the floor term perturbs every phase by an amount of size up to $|\{c(p-1)\}_q|$ . Condition (6.11) only keeps this perturbation within $\pi/6$ of the main phase; it does not remove it. The per-state bound must survive this perturbation uniformly in $p$ , $r$ and $k$ , including small primes where the paper's integral approximation gives no explicit control.

The count of good pairs needs a separate argument about how often a multiple $c(p-1)$ lies within $q/12$ of a multiple of $q$ when $\gcd(p-1,q)$ is large.

Formalization scope

States are functions Fin q × Fin q × (ZMod p)ˣ → ℂ. The first two registers range over $\{0,\dots,q-1\}$ ; the third over the units modulo $p$ .
Matrix convention. Following §2, rows are inputs, so the amplitude of $|c,d,y\rangle$ after the transforms is $\sum_{a,b}\psi(a,b,y)(A_q)_{a,c}(A_q)_{b,d}$ . finalState is defined this way from (6.1) and $A_q$ . It is not typed in as the closed form (6.3) or (6.4). A formalization that defined the final state by (6.4) directly would make milestone 1 trivial, and is ruled out.
Probability of a basis state is the squared norm of its amplitude, with no normalization hypothesis.
Parameters. $p$ is prime (Fact p.Prime). The generator is encoded as orderOf g = p - 1. $r<p-1$ is a parameter, with $x=g^r$ . $q$ is given by q = 2 ^ l together with $p<q<2p$ . No large- $p$ threshold is added anywhere.
Arithmetic. $x^{-b}$ is x⁻¹ ^ b in the unit group. $p-1$ is computed in $\mathbb Z$ and $\mathbb R$ inside $T$ and the congruences, and as natural-number subtraction only where $p\ge2$ makes it exact. $T$ is real.
Condition (6.10) is stated as "some integer $j$ has $|T-jq|\le\frac12$ ". Because $q\ge4$ , this is equivalent to the page's form with $j$ the closest integer to $T/q$ .
Not formalized. The preparation of (6.1) by testing and restarting is not formalized; the state (6.1) is taken as displayed. The printed test "whether the number is less than $p$ " should read $p-1$ , as the sums in (6.1) show. Also out of scope: the recovery of $r$ (eqs. (6.18)–(6.20)), the repetition count " $480t$ ", and all running-time claims.
Printed slips.
- The page asserts that for each $c$ there is exactly one $d$ satisfying (6.10). At a tie $\{T\}_q=\pm\frac12$ there can be two such $d$ . Milestone 3 states only the count, which needs at least one.
- The page's intermediate bound "at least $p/(240q)$ " should be $(p-1)/(240q)$ . The conclusion $1/480$ is unaffected, since $q$ and $2p$ are both even and so $q\le 2(p-1)$ . Only $1/480$ is stated.

Needed infrastructure: finite exponential sums and their modulus, the symmetric residue and its basic properties, and counting multiples in residue classes of $\mathbb Z/q$ . The exponential-sum estimates of milestones 1 and 2 are reusable in the order-finding analysis of §5 of the same paper. Proofs of any milestone, of the normalization $\sum\Pr=1$ , and of auxiliary lemmas about symmRes are welcome.

Selected references

P. W. Shor, Polynomial-Time Algorithms for Prime Factorization and Discrete Logarithms on a Quantum Computer, SIAM J. Comput. 26(5):1484–1509, 1997. https://doi.org/10.1137/S0097539795293172 (preprint: https://arxiv.org/abs/quant-ph/9508027)
D. M. Gordon, Discrete logarithms in GF(p) using the number field sieve, SIAM J. Discrete Math. 6(1):124–138, 1993. https://doi.org/10.1137/0406010
W. Diffie and M. E. Hellman, New directions in cryptography, IEEE Trans. Inform. Theory 22(6):644–654, 1976. https://doi.org/10.1109/TIT.1976.1055638
M. A. Nielsen and I. L. Chuang, Quantum Computation and Quantum Information, Cambridge University Press, 2000. https://doi.org/10.1017/CBO9780511976667

11 thms2 active usersReviewed

Analysis Control Theory Partial Differential Equations·Captain: mikedeng1

Stability and Instability Results of the Wave Equation with a Delay Term in the Boundary or Internal Feedbacks IV: Arbitrarily Small Destabilizing Delays for Internal DampingResearch Paper

Motivation

Feedback laws in engineering are applied with a lag: sensors, actuators and communication channels introduce a time delay $\tau$ between the measurement of a state and the control that reacts to it. For finite-dimensional systems small delays are usually harmless. For distributed systems such as the wave equation they need not be: Datko, Lagnese and Polis (SIAM J. Control Optim. 24, 1986) and Datko (SIAM J. Control Optim. 26, 1988) showed, for one-dimensional examples, that an arbitrarily small delay in a stabilizing feedback can destroy stability. The question matters to anyone who designs boundary or internal controllers for vibrating structures and wants to know whether a stabilizing law is robust to delay.

Nicaise and Pignotti (SIAM J. Control Optim. 45 (2006)) study the wave equation on a bounded domain of $\mathbb R^n$ with a damping term that combines an instantaneous and a delayed velocity feedback, with coefficients $\mu_1$ and $\mu_2$ . They show that the system is exponentially stable when $\mu_2 < \mu_1$ (Theorems 1.1 and 1.3), and that when $\mu_2 \ge \mu_1$ stability can fail (Theorems 1.2 and 1.4). This mission is Theorem 1.4, the internal-damping instability result, in the case the paper proves.

1986–1988: Datko, Lagnese and Polis; Datko — destabilization by small delays in one-dimensional boundary-damped wave equations.
2006: Nicaise and Pignotti — the multi-dimensional dichotomy $\mu_2 < \mu_1$ (stability) versus $\mu_2 \ge \mu_1$ (instability for some delays), for boundary and internal feedback.

Setting

Let $n \ge 1$ and let $\Omega \subset \mathbb R^n$ be a bounded open set with boundary $\Gamma$ of class $C^2$ , split as $\Gamma = \Gamma_D \cup \Gamma_N$ with $\overline{\Gamma_D} \cap \overline{\Gamma_N} = \emptyset$ and $\Gamma_D \neq \emptyset$ . Write $\nu$ for the outer unit normal and $\partial u/\partial\nu$ for the normal derivative. Let $\mu_1 > 0$ , $\mu_2 > 0$ and let $\tau > 0$ be the delay. With damping coefficient $a \equiv 1$ the problem is

u_{tt}(x,t) - \Delta u(x,t) + \mu_1 u_t(x,t) + \mu_2 u_t(x,t-\tau) = 0 \quad \text{in } \Omega \times (0,\infty),

u = 0 \ \text{ on } \Gamma_D \times (0,\infty), \qquad \frac{\partial u}{\partial\nu} = 0 \ \text{ on } \Gamma_N \times (0,\infty),

with initial data $u(\cdot,0) = u_0$ , $u_t(\cdot,0) = u_1$ and a history $u_t = g_0$ on $\Omega \times (-\tau, 0)$ . The standard energy of a solution is

\mathcal E(t) = \frac12 \int_\Omega \big\{ |u_t(x,t)|^2 + |\nabla u(x,t)|^2 \big\}\,dx .

The condition $\mu_2 < \mu_1$ is the paper's assumption (1.8). The paper's problem (1.12)–(1.16) carries a general coefficient $a \in L^\infty(\Omega)$ with $a \ge 0$ and $a > a_0 > 0$ near $\Gamma_N$ ; $a \equiv 1$ is one such coefficient.

Formalization targets

Goal: Theorem 1.4 for $a \equiv 1$

If (1.8) fails, i.e. $0 < \mu_1 \le \mu_2$ , then

\forall \varepsilon > 0\ \exists \tau \in (0,\varepsilon)\ \exists u \text{ solving the problem with delay } \tau:\ \ \mathcal E(t) \not\to 0 \ (t \to \infty),

and the same holds with " $\tau \in (0,\varepsilon)$ " replaced by " $\tau > M$ ", for every $M$ . The goal asserts only non-decay, not a rate of growth or the value of the energy, so it survives any sharpening of the examples.

Milestones

(5.21)–(5.23): if $\varphi$ is an eigenfunction of the mixed Dirichlet–Neumann Laplacian, $\Delta\varphi = -\Lambda^2\varphi$ , and $\lambda \in \mathbb C$ solves $\lambda^2 + (\mu_1 + \mu_2 e^{-\lambda\tau})\lambda = -\Lambda^2$ , then $e^{\lambda t}\varphi(x)$ is a solution.
(5.24)–(5.25): with $\lambda = \alpha + i\beta$ and $\beta\tau = (2l+1)\pi$ , that equation is equivalent to $\alpha^2 + \beta^2 = \Lambda^2$ , $\mu_2 e^{-\alpha\tau} = 2\alpha + \mu_1$ .
Case (a), $\mu_1 = \mu_2$ : the system forces $\alpha = 0$ and $\beta^2 = \Lambda^2$ .
Case (b), $\mu_2 > \mu_1$ , (5.26)–(5.27): for every $\Lambda > 0$ and $l$ there is $\alpha \in (0, (\mu_2-\mu_1)/2)$ with $\tau(\alpha) = \alpha^{-1}\ln(\mu_2/(\mu_1+2\alpha)) > 0$ solving the system.
Energy of separated solutions (p. 1584): $\mathcal E(t) = e^{2\,\mathrm{Re}(\lambda)t}\,\mathcal E(0)$ with $\mathcal E(0) > 0$ .
Delay bounds (p. 1585, corrected): $(2l+1)\pi/\Lambda < \tau < (2l+1)\pi/\sqrt{\Lambda^2 - (\mu_2-\mu_1)^2/4}$ , the second when $\Lambda^2 > (\mu_2-\mu_1)^2/4$ .

Significance

The result shows that the stability threshold $\mu_2 < \mu_1$ of Theorem 1.3 is sharp in the sense that matters for design: at or beyond the threshold there is no delay margin, since delays as small as desired already produce solutions whose energy does not decay. Together with Theorem 1.3 it gives a complete dichotomy in the coefficients $(\mu_1,\mu_2)$ for the internally damped wave equation with delay, in any dimension, and it identifies the mechanism (roots of the characteristic equation on or to the right of the imaginary axis) that later work on delayed stabilization has had to avoid.

The result is proved in the paper; to the best of current knowledge it has not been machine-checked. The mission's product is a formal proof of the $a \equiv 1$ case together with its algebraic core: the reduction of the transcendental characteristic equation, the analysis of both cases, and the two-sided bounds on the delays. The spectral input it needs, an unbounded sequence of eigenvalues of the mixed Dirichlet–Neumann Laplacian with regular eigenfunctions, is reusable well beyond this paper.

Difficulty

The scalar part is elementary. The difficulty is the spectral input. The small delays come from $\tau_{n,l} \approx (2l+1)\pi/\Lambda_n$ with $\Lambda_n \to \infty$ , so the proof needs infinitely many eigenvalues $\Lambda_n^2 \to \infty$ of the Laplacian with mixed Dirichlet–Neumann conditions on a $C^2$ domain, with eigenfunctions that are $C^2$ inside and $C^1$ up to the boundary. This requires compactness of the embedding $H^1_{\Gamma_D}(\Omega) \hookrightarrow L^2(\Omega)$ , the spectral theorem for compact self-adjoint operators, and elliptic regularity for a mixed problem, none of which is available in Mathlib for domains in $\mathbb R^n$ . A single eigenpair gives only the large delays (letting $l \to \infty$ ); it does not give the small ones.

A second point: the paper's own bound $(2l+1)^2\pi^2/\tau_{n,l}^2 \le \Lambda_n^2$ bounds $\tau_{n,l}$ only from below, so it does not by itself give $\tau_{n,l} \to 0$ ; the upper bound of milestone 6 is needed.

Formalization scope

Space: $\mathbb R^n$ is EuclideanSpace ℝ (Fin n) with $n \ge 1$ . The $C^2$ boundary is given by a global $C^2$ defining function $\psi$ ( $\Omega = \{\psi < 0\}$ , $\partial\Omega = \{\psi = 0\}$ , $\nabla\psi \ne 0$ on $\partial\Omega$ ); $\nu = \nabla\psi/|\nabla\psi|$ ; the surface measure is pinned by the Gauss–Green formula for all $C^1$ fields.
Solutions are complex valued functions $u(x,t)$ defined for all $t \in \mathbb R$ , $C^2$ on $\Omega \times \mathbb R$ and $C^1$ on $\overline\Omega \times \mathbb R$ ; the equation and boundary conditions hold for $t > 0$ ; initial data and history are the traces of $u$ . The Neumann condition uses the derivative within $\overline\Omega$ . $|\nabla u|^2$ is the sum of the squared moduli of the partial derivatives.
Corrected scope: Theorem 1.4 is printed for a general $a$ satisfying (1.17)–(1.18); §5.2 proves it only for $a \equiv 1$ , which is what is stated.
Corrected slips: (5.22) prints $\Delta\varphi = -\mu^2\varphi$ for $-\Lambda^2\varphi$ ; p. 1584 prints $e^{\alpha+i\beta}\varphi(x)$ for $e^{(\alpha+i\beta)t}\varphi(x)$ ; the p. 1585 bound is supplemented by the upper bound of milestone 6. Milestone texts are quoted verbatim, including the slips.
The standing hypotheses (1.6)–(1.7) and the constant $\xi$ of (1.10) are not used by §5.2 and are omitted, which strengthens the statements.
A trivializing formalization is ruled out: the goal's conclusion $\mathcal E \not\to 0$ excludes $u \equiv 0$ , the energy integrand is continuous on the compact $\overline\Omega$ so the integral is genuine, and the normal derivative is taken within $\overline\Omega$ so the Neumann condition is not satisfied by a junk value.
No statement assumes the existence of eigenvalues; supplying the spectral theory of the mixed Laplacian is part of the goal. Contributions welcome: the spectral theorem for the mixed Dirichlet–Neumann Laplacian on a bounded $C^2$ domain, boundary regularity of its eigenfunctions, and the energy identity for separated solutions.

Selected references

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
R. Datko, Not all feedback stabilized hyperbolic systems are robust with respect to small time delays in their feedbacks, SIAM J. Control Optim. 26:697–713, 1988.
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:152–156, 1986.
P. Grisvard, Elliptic Problems in Nonsmooth Domains, Pitman, 1985 (regularity of mixed boundary value problems).

11 thms2 active usersReviewed

Analysis Control Theory Partial Differential Equations·Captain: mikedeng1

Stability and Instability Results of the Wave Equation with a Delay Term in the Boundary or Internal Feedbacks III: Destabilizing Delays for Boundary FeedbackResearch Paper

Motivation

Boundary feedback stabilization of the wave equation asks whether a damping term placed on part of the boundary drives the energy of every solution to zero. Without delay the answer is classical: the feedback $\partial u/\partial\nu = -\mu_1 u_t$ on a part $\Gamma_N$ of the boundary gives exponential energy decay under geometric conditions (Chen, Lagnese, Lasiecka–Triggiani, Komornik–Zuazua). In practice a feedback is applied with a lag, and a small lag can destroy stability. Datko, Lagnese and Polis (doi:10.1137/0324007) and Datko (doi:10.1137/0326040) showed, in one space dimension, that a purely delayed boundary feedback destabilizes the system for arbitrarily small delays.

Nicaise and Pignotti (doi:10.1137/060648891) study a feedback made of an instantaneous part and a delayed part, with weights $\mu_1$ and $\mu_2$ , in any space dimension. Their Theorem 1.1 gives exponential decay when $\mu_2 < \mu_1$ . This mission formalizes the converse, Theorem 1.2: when $\mu_2 \ge \mu_1$ , some delays admit solutions whose energy does not decay at all.

Timeline.

1986: Datko, Lagnese and Polis, a one-dimensional wave equation whose delayed boundary feedback is unstable.
1988: Datko, instability under arbitrarily small delays for a class of hyperbolic systems.
2006: Xu, Yung and Li (doi:10.1051/cocv:2006021), one space dimension, by spectral analysis: stability for $\mu_2 < \mu_1$ , instability for $\mu_2 > \mu_1$ , possible instabilities for $\mu_1 = \mu_2$ .
2006: Nicaise and Pignotti, the same dichotomy in any dimension $n$ , with explicit destabilizing delays built from eigenfunctions (§5.1).

Setting

Let $n \ge 1$ and let $\Omega \subset \mathbb R^n$ be a bounded open set with boundary $\Gamma$ of class $C^2$ . The boundary is split as $\Gamma = \Gamma_D \cup \Gamma_N$ , with $\overline{\Gamma_D} \cap \overline{\Gamma_N} = \emptyset$ and $\Gamma_D \neq \emptyset$ . Write $\nu$ for the outer unit normal and $d\Gamma$ for the surface measure. Together these data form a mixed domain (MixedDomain n in Lean).

Fix $\mu_1, \mu_2 > 0$ and a delay $\tau > 0$ . The problem (1.1)–(1.3) is

\begin{cases} u_{tt}(x,t) - \Delta u(x,t) = 0 & \text{in } \Omega \times (0,+\infty),\\ u(x,t) = 0 & \text{on } \Gamma_D \times (0,+\infty),\\ \dfrac{\partial u}{\partial\nu}(x,t) = -\mu_1 u_t(x,t) - \mu_2 u_t(x,t-\tau) & \text{on } \Gamma_N \times (0,+\infty), \end{cases}

with initial data $u(\cdot,0)$ , $u_t(\cdot,0)$ and a history $u_t$ on $\Gamma_N \times (-\tau,0)$ (1.4)–(1.5). The standard energy of a solution is (3.7)

\mathcal E(t) = \frac12\int_\Omega \big(|u_t(x,t)|^2 + |\nabla u(x,t)|^2\big)\,dx .

Condition (1.8) of the paper is $\mu_2 < \mu_1$ . This mission concerns the complementary case $\mu_2 \ge \mu_1$ .

For real functions $w$ on $\Omega$ , (5.11) defines $q_0(w) = \int_{\Gamma_N} |w|^2\,d\Gamma$ and $q_1(w) = \int_\Omega |\nabla w|^2\,dx$ .

Formalization targets

Goal: Theorem 1.2 (p. 1563)

If $\mu_2 \ge \mu_1$ , there exist delays $0 < \tau_0 < \tau_1 < \cdots$ and, for each $k$ , a classical solution $u_k$ of (1.1)–(1.3) with delay $\tau_k$ and a constant $c_k > 0$ such that

\mathcal E_k(t) = c_k \qquad \text{for all } t \ge 0 .

The statement fixes no formula for the delays and no value of the energy. It asserts only the existence of infinitely many delays for which the energy does not decay.

Milestones

(5.1)–(5.2), pp. 1579–1580. If $\lambda \in \mathbb C$ and $\varphi$ solves $-\Delta\varphi + \lambda^2\varphi = 0$ in $\Omega$ , $\varphi = 0$ on $\Gamma_D$ and $\partial\varphi/\partial\nu = -(\mu_1 + \mu_2 e^{-\lambda\tau})\lambda\varphi$ on $\Gamma_N$ , then $u = e^{\lambda t}\varphi$ solves (1.1)–(1.3).
(5.5)–(5.7), pp. 1580 and 1582. For $b > 0$ , $l \in \mathbb N$ and $b\tau = \arccos(-\mu_1/\mu_2) + 2l\pi$ :

\cos(b\tau) = -\mu_1/\mu_2,\qquad \mu_2\sin(b\tau) = \sqrt{\mu_2^2-\mu_1^2},\qquad (\mu_1 + \mu_2e^{-ib\tau})\,ib = b\sqrt{\mu_2^2-\mu_1^2}.

Case (a), $\mu_1 = \mu_2$ , p. 1581. For a normalized mixed Dirichlet–Neumann eigenfunction $\varphi$ with $-\Delta\varphi = b^2\varphi$ and $\tau = (2l+1)\pi/b$ , the function $u = e^{ibt}\varphi$ is a solution and

\int_\Omega(|\nabla u|^2 + |u_t|^2)\,dx = 2b^2 \quad (t \ge 0).

Case (b), $\mu_2 > \mu_1$ , pp. 1581–1582. A normalized minimizer $\varphi$ of $s\,q_0(w) + \sqrt{s^2q_0(w)^2 + 4q_1(w)}$ , where $s = \sqrt{\mu_2^2-\mu_1^2}$ , solves the variational problem (5.7) with $2b$ equal to the minimum value.

Significance

The result. Theorem 1.2 shows that the threshold $\mu_2 < \mu_1$ of Theorem 1.1 is sharp in the following sense: once the delayed weight reaches the instantaneous one, no geometric assumption restores asymptotic stability for every delay. Together, Theorems 1.1 and 1.2 separate robust from non-robust boundary feedbacks by a single inequality between the two gains. The explicit delays of case (a), $\tau_{n,l} = (2l+1)\pi/b_n$ , become arbitrarily small or large. So even an arbitrarily short lag in an equally weighted feedback can remove decay.

The formalization. The paper proves the result. It has not been formalized, and Mathlib has no wave equation on domains, no mixed eigenvalue problems and no Sobolev spaces on domains. This mission produces:

a machine-checked statement of the instability half of the paper's dichotomy;
the reduction to a spectral problem as separate, checkable steps;
a precise record of what the paper leaves implicit. In case (b) the existence of the minimizer is assumed ("if the minimum … is attained"), and in case (a) the existence of Dirichlet–Neumann eigenfunctions is quoted.

Difficulty

Milestones 1 and 2 are calculus and trigonometry. The difficulty sits in producing $\varphi$ . The goal needs a nonzero function $\varphi$ that is $C^2$ in $\Omega$ and $C^1$ up to the boundary and solves an eigenvalue problem with mixed Dirichlet and Neumann (case (a)) or Dirichlet and Robin-type (case (b)) boundary conditions. Existence requires compactness of $H^1_{\Gamma_D}(\Omega) \hookrightarrow L^2(\Omega)$ and of the trace into $L^2(\Gamma_N)$ , followed by elliptic regularity up to a $C^2$ boundary. None of these is in Mathlib.

A shortcut does not work: in case (b) the frequency $b$ enters the boundary condition, so $\varphi$ is not an eigenfunction of a fixed self-adjoint operator. The page instead minimizes a non-quadratic functional, and its first-variation computation (5.18)–(5.19) needs care: the functional is not 2-homogeneous, so the normalization by $1 + \varepsilon^2\|v\|^2$ does not literally give $g(\varepsilon) \ge g(0)$ , although the first-order condition is right.

Taking real parts does not give a real-valued solution with constant energy: in case (b) the energy of $\cos(bt)\varphi$ oscillates.

Formalization scope

Solutions are complex-valued, $u : \mathbb R^n \times \mathbb R \to \mathbb C$ , as the page's $e^{\lambda t}\varphi$ with $\lambda \in \mathbb C$ are. $|u_t|^2$ and $|\nabla u|^2 = \sum_i |\partial_i u|^2$ are squared moduli.
Classical solutions. A solution is $C^2$ on $\Omega \times \mathbb R$ and $C^1$ on $\overline\Omega \times \mathbb R$ . It solves the equations for $t > 0$ , and its values at $t \le 0$ are the initial data and history. The normal derivative is the derivative within $\overline\Omega$ applied to $\nu$ . $C^2$ regularity up to the boundary is not required, because eigenfunctions of mixed problems generally lack it.
The domain. The $C^2$ boundary is given by a global defining function $\psi$ with $\Omega = \{\psi < 0\}$ . The surface measure is pinned down by the Gauss–Green formula for all $C^1$ vector fields, which determines it uniquely.
Dropped hypotheses. The geometric hypotheses (1.6)–(1.7) and the parameter $\xi$ of (1.10) are not used in §5.1 and are omitted. This strengthens the statements.
Sobolev spaces. $H^1_{\Gamma_D}(\Omega)$ is replaced in milestone 4 by the class of real functions that are $C^2$ in $\Omega$ , $C^1$ on $\overline\Omega$ and zero on $\Gamma_D$ , both as the minimization class and as the test class.
Non-triviality. The goal requires the constant energy to be positive and the delays to be strictly increasing. Without positivity, the zero solution would satisfy "constant energy". Without strict monotonicity, one delay repeated would count as a sequence.

A complete development needs the following:

Green's first identity on $C^2$ domains for functions that are $C^1$ up to the boundary;
existence and regularity of eigenfunctions of the Laplacian with mixed boundary conditions;
in case (b), existence of the minimizer (Rellich compactness and the trace theorem).

These pieces are reusable well beyond this mission. Contributions of any of them, or of an alternative route to a $\varphi$ with the required properties, are welcome.

Selected references

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
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:152–156, 1986. https://doi.org/10.1137/0324007
R. Datko, Not all feedback stabilized hyperbolic systems are robust with respect to small time delays in their feedbacks, SIAM J. Control Optim. 26:697–713, 1988. https://doi.org/10.1137/0326040
G. Q. Xu, S. P. Yung, L. K. Li, Stabilization of wave systems with input delay in the boundary control, ESAIM Control Optim. Calc. Var. 12:770–785, 2006. https://doi.org/10.1051/cocv:2006021

8 thms2 active usersReviewed

All missions

Elements of Queueing Theory II: The Loynes Stability Theorem and CouplingTextbook

The Loynes Stability Theorem and Coupling

Background

The goal

The route, and what it produces on the way

Three extensions

Formalization scope

What this mission provides

Elements of Queueing Theory Ib: Ergodicity and Stochastic IntensityTextbook

Ergodicity and Stochastic Intensity

Background

Ergodic theory, quoted

Predictability, and why PASTA can be stated

The goal

Palm probability meets stochastic intensity

What this mission provides

Formalization scope

Strategyproof Approximation of the Minimax on Networks 2: No Strategyproof Randomized Mechanism Beats 2 - o(1) on TreesResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 4.1 with its explicit constant

Milestones

Significance

Difficulty

Formalization scope

Selected references

Strategyproof Approximation of the Minimax on Networks 1: A Strategyproof 3/2-Approximation Mechanism on the CircleResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 3.1

Milestones (Appendix A)

Significance

Difficulty

Formalization scope

Selected references

Building Anosov flows on 3-manifolds (Béguin–Bonatti–Yu)Research Paper

Motivation

Setting

Formalization targets

Goal: the gluing theorem (Theorem 1.5)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Linear Programming: Foundations and Extensions V: Convergence Rates of the Path-Following MethodTextbook

Motivation

Setting

Formalization targets

Goal: Theorem 18.1 with the explicit constant

Milestones

Significance

Difficulty

Formalization scope

Selected references

Linear Programming: Foundations and Extensions III: Network Flows, the Integrality Theorem and König's TheoremTextbook

Motivation

Setting

Formalization targets

Goal: König's Theorem (Theorem 14.3, p. 216)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Stochastic Dynamic Programming and the Control of Queueing Systems XIV: Conforming Approximating Sequences for Markov ChainsTextbook

Motivation

Setting

Formalization targets

Goal: Proposition C.5.2

Milestones

Further results

Significance

Difficulty

Formalization scope

Selected references

Theory of Games and Economic Behavior VI: Splitting Sets and the Decomposition Partition of a GameTextbook

Core: Theorem 1.4 (exact recovery by $\ell^1$ minimization)

Goal: Smale's mean value conjecture ( $K = 1$ )