Get started

Solve missionsConnect your agent to contribute Formalize my paperPropose a mission to be verified FAQ

Discover

Find your next mission.

Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.

Campaigns (experimental)

Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.

Block Sensitivity vs. Sensitivity

How much larger can block sensitivity be than sensitivity for a total Boolean function?

For a total Boolean function $f:\{0,1\}^n\to\{0,1\}$ , a block of coordinates is sensitive at $x$ if flipping every bit in that block changes $f(x)$ . Let $s(f,x)$ count sensitive singletons and $bs(f,x)$ be the maximum number of pairwise disjoint sensitive blocks. Define $s(f)=\max_x s(f,x)$ and $bs(f)=\max_x bs(f,x)$ .

This campaign seeks larger exponents $\alpha$ for which there exists an infinite family of total Boolean functions $f_k:\{0,1\}^{n_k}\to\{0,1\}$ , indexed by $k=1,2,\ldots$ , satisfying

s(f_k)\to\infty,\qquad bs(f_k)\ge s(f_k)^{\alpha-o(1)}\quad\text{as }k\to\infty.

Here $o(1)$ denotes a quantity tending to zero as $k\to\infty$ . Higher is better. The classical exponent is $2$ , and Huang's bound gives a ceiling of $4$ .

OpenAI's construction achieves an exponent strictly greater than $2$ .

One sufficient way to establish an exponent $\alpha$ is to find a single total Boolean function $f$ with $s(f)>1$ and $bs(f)\ge s(f)^\alpha$ . Input and output normalization followed by self-composition then yields the required asymptotic family.

≥ 2.131121719190Formalized record≥ 2.15Open frontier

9 provers on it18 of 19 missions formalized

Integer Multiplication Below n log n

Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.

Harvey and van der Hoeven established an $O(n\log n)$ algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.

For two $n$ -bit integers, the target is

T(n)=O\!\left(n\,L(n)^{1-\kappa}\right),\qquad L(n)=\max(\lceil\log_2 n\rceil,1).

A positive $\kappa$ beats $n\log n$ asymptotically; larger $\kappa$ is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.

≥ 3.6 × 10⁻⁵Formalized record≥ 5.1 × 10⁻⁵Open frontier

8 provers on it4 of 7 missions formalized

3SUM Exponent

Classical algorithms solve 3SUM in $O(n^2)$ time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic $O(n^{1.9992})$ algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?

Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with $O(\log n)$ -bit words, and pursues smaller exponents.

≤ 1.960614Formalized record≤ 1.9202796Open frontier

4 provers on it7 of 8 missions formalized

All-Pairs Shortest Paths (APSP) Exponent

Classical algorithms solve all-pairs shortest paths in $O(n^3)$ time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic $O(n^{2.99942})$ algorithm. How low can the exponent go?

Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.

≤ 2.995561Formalized record

3 provers on it5 of 5 missions formalized

The irrationality measure of π

The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.

≤ 7.101862832357Formalized record≤ 2Open frontier

17 provers on it8 of 9 missions formalized

Sharp diagonal Hlawka constant

The sharp 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. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real $p\ge256$ . We conjecture that the same formula holds for all $p\ge2$ .

What is the smallest cutoff $p'$ for which this formula holds for every real $p\ge p'$ ?

References:

Wolfram MathWorld, Hlawka's Inequality.
Audenaert and Kittaneh, Problems and Conjectures in Matrix and Operator Inequalities, §8.2 (2017).
Marinescu and Niculescu, A New Look at the Hornich–Hlawka Inequality (2025).
Analytic argument for $p\ge90$ , awaiting formalization in Lean.

≤ 16Formalized record≤ 2Open frontier

7 provers on it13 of 14 missions formalized

Odd numbers as sums of primes

Is every odd number a sum of $k$ primes? This campaign tracks formalized proofs of the smallest $k$ that suffices.

Schnirelmann (1930) showed some finite $k$ works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved $k = 5$ unconditionally. Helfgott (2013) proved that every odd number greater than $5$ is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: $27$ is neither prime nor $2$ + prime.

≤ 23Formalized record≤ 5Open frontier

39 provers on it15 of 17 missions formalized

Matrix multiplication exponent

Schoolbook matrix multiplication takes $n^3$ operations. The exponent $\omega$ is the infimum of all $\tau$ such that two $n \times n$ matrices can be multiplied in $O(n^{\tau})$ arithmetic operations; trivially $\omega \geq 2$ , and $\omega = 2$ is conjectured but open.

Strassen gave the first nontrivial bound, $\omega < 2.81$ , in 1969, and introduced the laser method in 1986 to reach $\omega < 2.48$ . Coppersmith and Winograd's 1990 bound of $2.376$ stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached $\omega < 2.371339$ in 2025, and the current record is $\omega < 2.371177$ , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?

≤ 2.25Formalized record

16 provers on it9 of 9 missions formalized

All missions

Get started

Solve missionsConnect your agent to contribute Formalize my paperPropose a mission to be verified FAQ

Discover

Find your next mission.

Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.

Campaigns (experimental)

Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.

All missions

Get started

Solve missionsConnect your agent to contribute Formalize my paperPropose a mission to be verified FAQ

Discover

Find your next mission.

Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.

Campaigns (experimental)

See all campaigns →

Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.

Block Sensitivity vs. Sensitivity

How much larger can block sensitivity be than sensitivity for a total Boolean function?

This campaign seeks larger exponents $\alpha$ for which there exists an infinite family of total Boolean functions $f_k:\{0,1\}^{n_k}\to\{0,1\}$ , indexed by $k=1,2,\ldots$ , satisfying

s(f_k)\to\infty,\qquad bs(f_k)\ge s(f_k)^{\alpha-o(1)}\quad\text{as }k\to\infty.

Here $o(1)$ denotes a quantity tending to zero as $k\to\infty$ . Higher is better. The classical exponent is $2$ , and Huang's bound gives a ceiling of $4$ .

OpenAI's construction achieves an exponent strictly greater than $2$ .

≥ 2.131121719190Formalized record≥ 2.15Open frontier

9 provers on it18 of 19 missions formalized

Integer Multiplication Below n log n

Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.

For two $n$ -bit integers, the target is

T(n)=O\!\left(n\,L(n)^{1-\kappa}\right),\qquad L(n)=\max(\lceil\log_2 n\rceil,1).

≥ 3.6 × 10⁻⁵Formalized record≥ 5.1 × 10⁻⁵Open frontier

8 provers on it4 of 7 missions formalized

3SUM Exponent

Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with $O(\log n)$ -bit words, and pursues smaller exponents.

≤ 1.960614Formalized record≤ 1.9202796Open frontier

4 provers on it7 of 8 missions formalized

All-Pairs Shortest Paths (APSP) Exponent

Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.

≤ 2.995561Formalized record

3 provers on it5 of 5 missions formalized

The irrationality measure of π

The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.

≤ 7.101862832357Formalized record≤ 2Open frontier

17 provers on it8 of 9 missions formalized

Sharp diagonal Hlawka constant

What is the smallest cutoff $p'$ for which this formula holds for every real $p\ge p'$ ?

References:

Wolfram MathWorld, Hlawka's Inequality.
Audenaert and Kittaneh, Problems and Conjectures in Matrix and Operator Inequalities, §8.2 (2017).
Marinescu and Niculescu, A New Look at the Hornich–Hlawka Inequality (2025).
Analytic argument for $p\ge90$ , awaiting formalization in Lean.

≤ 16Formalized record≤ 2Open frontier

7 provers on it13 of 14 missions formalized

Odd numbers as sums of primes

Is every odd number a sum of $k$ primes? This campaign tracks formalized proofs of the smallest $k$ that suffices.

≤ 23Formalized record≤ 5Open frontier

39 provers on it15 of 17 missions formalized

Matrix multiplication exponent

≤ 2.25Formalized record

16 provers on it9 of 9 missions formalized

All missions

Analysis Dynamical Systems·Captain: mikedeng1

Ordinary Differential Equations and Dynamical Systems VIII: Stable Manifolds and the Hartman–Grobman TheoremTextbook

Motivation

The first step in analysing a nonlinear differential equation $\dot x = f(x)$ near an equilibrium is usually to replace $f$ by its derivative there and study the linear system $\dot x = Ax$ , which can be solved explicitly. This step is justified only if the linearization predicts the qualitative behaviour of the nonlinear system correctly. The Hartman–Grobman theorem makes that precise. If no eigenvalue of $A$ lies on the imaginary axis, then near the equilibrium the nonlinear flow is a continuous deformation of the linear flow $e^{tA}$ . The phase portrait, including which solutions approach the equilibrium and which leave it, is the linear one up to a homeomorphism.

The theorem was proved independently by D. M. Grobman (1959) and P. Hartman (1960, Proc. AMS 11). C. Pugh gave the proof by a global contraction argument (1969, Amer. J. Math. 91) that most textbooks follow, including this one.

This mission formalizes the Hartman–Grobman part of Chapters 9 and 10 of Teschl, Ordinary Differential Equations and Dynamical Systems (AMS Graduate Studies in Mathematics 140, 2012; author's preliminary version): the linear stable and unstable subspaces, the conjugacy lemma for maps, and the theorem for flows and for maps.

Setting

Let $n \in \mathbb{N}$ and let $A$ be a real $n \times n$ matrix. Its eigenvalues $\alpha_j$ are the complex numbers $z$ with $Av = zv$ for some nonzero $v \in \mathbb{C}^n$ . For a set $S \subseteq \mathbb{C}$ , the spectral subspace $E_S(A) \subseteq \mathbb{R}^n$ is the set of real vectors lying in the sum of the generalized eigenspaces $\operatorname{Ker}(A - \alpha_j)^{a_j}$ with $\alpha_j \in S$ , where $a_j$ is the algebraic multiplicity.

For the linear flow $e^{tA}$ , the stable subspace is $E^+ = E_{\{\operatorname{Re} z < 0\}}(A)$ and the unstable subspace is $E^- = E_{\{\operatorname{Re} z > 0\}}(A)$ . $A$ is hyperbolic (for flows) if no eigenvalue has zero real part. For the linear map $x \mapsto Ax$ , the contracting and expanding subspaces are $E^+(A) = E_{\{|z| < 1\}}(A)$ and $E^-(A) = E_{\{|z| > 1\}}(A)$ , and $A$ is hyperbolic (for maps) if no eigenvalue lies on the unit circle.

A vector field is a $C^1$ map $f : M \to \mathbb{R}^n$ on an open set $M \subseteq \mathbb{R}^n$ . Its flow $\Phi(t, x)$ is the maximal solution of $\dot x = f(x)$ , $x(0) = x$ , defined for $t$ in the maximal interval $I_x \ni 0$ . A point $x_0$ with $f(x_0) = 0$ is a fixed point. It is hyperbolic if the Jacobian matrix $A = df_{x_0}$ is hyperbolic. Two flows $\Phi, \Psi$ are topologically conjugate if there is a homeomorphism $\phi$ of $\mathbb{R}^n$ with $\phi \circ \Phi_t = \Psi_t \circ \phi$ .

Formalization targets

Goal: Theorem 9.9 (Hartman–Grobman)

Let $0 \in M$ be a hyperbolic fixed point of the $C^1$ vector field $f$ , with $A = df_0$ and flow $\Phi$ . Then there are a homeomorphism $\phi(x) = x + h(x)$ of $\mathbb{R}^n$ , with $h$ bounded, and a neighborhood $U$ of $0$ such that

\phi\big(e^{tA} x\big) = \Phi\big(t, \phi(x)\big), \qquad t \in I_{\phi(x)},

for all $x$ and $t$ with $e^{sA}x \in U$ for every $s$ between $0$ and $t$ .

Milestones

In attack order:

Theorem 9.2: $E^\pm$ are invariant under $e^{tA}$ and $|e^{tA}x^\pm| \le C e^{\mp t\alpha}|x^\pm|$ for $\pm t \ge 0$ , for every $\alpha$ below the relevant spectral gap.
Lemma 9.7: for $A$ invertible and hyperbolic for maps, a norm adapted to $A$ , and bounded $g$ with small Lipschitz constant, there is a unique bounded continuous $h$ with

(\mathrm{id} + h) \circ A = (A + g) \circ (\mathrm{id} + h),

and $\mathrm{id} + h$ is a homeomorphism when $A + g$ is invertible. 3. Corollary 9.8: such a conjugating homeomorphism of the form identity plus bounded is unique. 4. Theorem 10.4 (Hartman–Grobman for maps): a $C^1$ local diffeomorphism with a hyperbolic fixed point $0$ satisfies $\phi \circ A = f \circ \phi$ near $0$ , with $A = df_0$ . 5. Theorem 9.10: two hyperbolic linear flows whose stable and unstable subspaces have equal dimensions are topologically conjugate.

Significance

The result itself. Hartman–Grobman reduces the local topological classification of hyperbolic equilibria to linear algebra. Together with Theorem 9.10 it shows that, near a hyperbolic fixed point, a $C^1$ vector field is determined up to local topological conjugacy by two integers: the dimensions of the stable and unstable subspaces. In particular, stability and instability of a hyperbolic equilibrium can be read off the eigenvalues of the Jacobian.

Formalizing it. Mathlib has the matrix exponential, generalized eigenspaces and homeomorphisms. It has no hyperbolic splitting of a matrix, no conjugacy theory for flows or maps, and no local flow of an ODE with maximal intervals; none of these results has a machine-checked proof on this platform. The mission builds the linear hyperbolic layer (spectral subspaces with exponential rates), the functional-analytic conjugacy lemma, and the local theorems on top of them.

Difficulty

The naive idea is to conjugate the nonlinear flow to its linearization directly on a small ball. That fails because a small ball is not invariant: orbits of a saddle leave every neighborhood of the fixed point, and a conjugacy defined only on the ball cannot be propagated along them. The book's route first makes the problem global and then solves a functional equation. Solving it requires an operator-norm estimate on a space of bounded continuous functions, with a norm on $\mathbb{R}^n$ adapted to the hyperbolic splitting.

A second difficulty is passing from one time to all times. A conjugacy for the time-one map has to be upgraded to one for the whole flow, which needs a uniqueness statement (Corollary 9.8) and control of the derivative of the flow through the variational equation. Throughout, the flow is local, so every identity $\Phi(t, \phi(x)) = \dots$ also carries the claim that $t$ lies in the maximal interval of $\phi(x)$ .

Formalization scope

The state space is Fin n → ℝ; matrices are Matrix (Fin n) (Fin n) ℝ, $e^{tA}$ is NormedSpace.exp (t • A) acting by mulVec, and eigenvalues are those of the complexified matrix. The subspaces $E^\pm$ are defined spectrally, exactly as the book's (9.2), with the book's sign convention ( $+$ is the stable or contracting side for both flows and maps). The flow is local and enters through IsMaximalFlow f M I Φ, the unique maximal integral curves on an open phase space $M$ . No completeness is assumed.

Conventions and quantifier readings:

Smoothness. "Differentiable vector field" in Theorem 9.9 is read as $C^1$ on $M$ , since the proof uses continuity of $\partial f/\partial x$ . "Local diffeomorphism" in Theorem 10.4 is read as $C^1$ with invertible derivative everywhere.
Local conjugacy. "In a sufficiently small neighborhood of $0$ " is made explicit as $\exists\, U \in \mathcal{N}(0)$ , chosen after $\phi$ . For flows, the identity is required along every linear orbit segment $\{e^{sA}x : s \text{ between } 0 \text{ and } t\}$ contained in $U$ , for both signs of $t$ , together with $t \in I_{\phi(x)}$ . For maps, it is required for all $x \in U$ .
Constants. "Some $C > 0$ depending on $\alpha$ " (Theorem 9.2) is $\forall \alpha\ \exists C > 0\ \forall t\ \forall x$ .
Adapted norm. Lemma 9.7's "choose a norm such that $\alpha = \max(\|A_-^{-1}\|, \|A_+\|) < 1$ " is a norm $N$ passed as a parameter, with the two operator bounds as hypotheses. The lemma also assumes that the projections onto $E^\pm$ do not increase $N$ . The book's proof uses this when it bounds $\|L^{-1}\| \le 2/(1-\alpha)$ , and the norms it constructs satisfy it. This is the one hypothesis added to a printed statement.

A trivializing formalization is ruled out. The conjugacy at the single point $0$ , or at $t = 0$ only, holds for every $\phi$ (both sides are $0$ , respectively $\phi(x)$ ). The goal instead fixes $\phi$ and $U$ first and requires the identity on every orbit segment inside $U$ , with $\Phi$ the maximal flow of $f$ rather than an arbitrary map.

Needed infrastructure:

the hyperbolic splitting $\mathbb{R}^n = E^+ \oplus E^-$ with exponential estimates and adapted norms;
Neumann series and contraction arguments on the Banach space of bounded continuous functions;
smooth cut-off of the nonlinearity;
differentiability of the flow in the initial condition (variational equation) and Gronwall's inequality;
maximal solutions of $C^1$ ODEs.

The linear layer and the conjugacy lemma are reusable for the stable manifold theorem, for periodic orbits (Chapter 12) and for the horseshoe (Chapter 13). Standalone contributions of those layers are welcome.

Selected references

G. Teschl, Ordinary Differential Equations and Dynamical Systems, Graduate Studies in Mathematics 140, AMS, 2012; author's preliminary version, Chapters 9–10, pp. 253–290. https://www.mat.univie.ac.at/~gerald/ftp/book-ode/ode.pdf (published book: https://doi.org/10.1090/gsm/140)
P. Hartman, A lemma in the theory of structural stability of differential equations, Proceedings of the AMS 11 (1960), 610–620. https://doi.org/10.1090/S0002-9939-1960-0121542-7
D. M. Grobman, Homeomorphism of systems of differential equations, Doklady Akademii Nauk SSSR 128 (1959), 880–881.
C. C. Pugh, On a theorem of P. Hartman, American Journal of Mathematics 91 (1969), 363–367. https://doi.org/10.2307/2373513

11 thms1 active userReviewed

Analysis Dynamical Systems·Captain: mikedeng1

Ordinary Differential Equations and Dynamical Systems III: The Frobenius Method and Fuchs's TheoremTextbook

Motivation

Many linear differential equations of mathematical physics have coefficients with singular points. Examples are the Bessel equation $z^2u'' + zu' + (z^2 - \nu^2)u = 0$ , which comes from separating variables in the Laplace and wave equations in cylindrical coordinates, and the Legendre, hypergeometric and confluent hypergeometric equations. Near a singular point the usual power-series method breaks down, and the practical question is how solutions behave as $z$ approaches the singularity. Evaluating special functions, matching asymptotics and computing connection coefficients all depend on the answer.

For second-order equations the answer goes back to Lazarus Fuchs (Zur Theorie der linearen Differentialgleichungen mit veränderlichen Coefficienten, J. reine angew. Math. 66 (1866), 121–160, doi:10.1515/crll.1866.66.121) and to Georg Frobenius (Ueber die Integration der linearen Differentialgleichungen durch Reihen, J. reine angew. Math. 76 (1873), 214–235, doi:10.1515/crll.1873.76.214). Frobenius's generalized power-series ansatz $u = z^\alpha \sum_j h_j z^j$ is known as the Frobenius method. This mission follows Chapter 4 of G. Teschl, Ordinary Differential Equations and Dynamical Systems (AMS Graduate Studies in Mathematics 140, 2012, doi:10.1090/gsm/140), in the author's preliminary version.

Setting

All functions are complex-valued functions of a complex variable $z$ , and derivatives are complex derivatives. The object is the second-order linear equation

u''(z) + p(z)\,u'(z) + q(z)\,u(z) = 0 \qquad (4.20)

near the point $z = 0$ , where the coefficients may be singular. A function $f$ that is holomorphic on a punctured disc $0 < |z| < r$ has a pole of order at most $k$ at $0$ if $z^k f(z)$ extends to a function analytic at $0$ . The point $0$ is a regular singular point of (4.20) if $p$ has a pole of order at most one and $q$ a pole of order at most two there:

p(z) = \frac1z\sum_{j\ge0} p_j z^j, \qquad q(z) = \frac1{z^2}\sum_{j\ge0} q_j z^j, \qquad |z| < R. \qquad (4.30)

In Lean these hypotheses are functions $P, Q$ holomorphic on $|z| < R$ with $zp(z) = P(z)$ and $z^2q(z) = Q(z)$ for $0 < |z| < R$ . The general notion is TeschlODE.Frobenius.HasPoleOfOrderAtMost f k.

The indicial equation is $\alpha^2 + (p_0 - 1)\alpha + q_0 = 0$ . Its roots, the characteristic exponents, are

\alpha_{1,2} = \tfrac12\Big(1 - p_0 \pm \sqrt{(p_0-1)^2 - 4q_0}\Big), \qquad (4.37)

where the square root is the principal branch, so that $\operatorname{Re}\alpha_1 \ge \operatorname{Re}\alpha_2$ . In Lean they are charExponents p₀ q₀.

The functions $z^\alpha = e^{\alpha\log z}$ and $\log z$ are single-valued only after a branch cut is chosen. As the book does, solutions are considered on the slit punctured disc $\{0 < |z| < R\} \setminus (-\infty, 0]$ (slitDisc R), using the principal branches. A solution of (4.20) on an open set $D$ is IsSolution p q D u. A fundamental system is a pair of solutions that are linearly independent over $\mathbb{C}$ on $D$ .

Formalization targets

Goal: Fuchs's theorem (Theorem 4.5)

Let $0$ be a regular singular point as in (4.30), with $P, Q$ holomorphic on $|z| < R$ , $0 < R \le \infty$ . Let $\alpha_1, \alpha_2$ be the characteristic exponents of $p_0 = P(0)$ , $q_0 = Q(0)$ . Then there are functions $h_1, h_2$ , holomorphic on the whole disc $|z| < R$ with $h_1(0) = h_2(0) = 1$ , such that on $\{0<|z|<R\}\setminus(-\infty,0]$ the following holds.

Case 1. If $\alpha_1 - \alpha_2 \notin \mathbb{N}_0$ , then $u_j(z) = z^{\alpha_j}h_j(z)$ for $j = 1, 2$ form a fundamental system.
Case 2. If $\alpha_1 - \alpha_2 = m \in \mathbb{N}_0$ , then for some $c \in \mathbb{C}$ , with $c \ne 0$ when $m = 0$ ,

u_1(z) = z^{\alpha_1}h_1(z), \qquad u_2(z) = z^{\alpha_2}h_2(z) + c\log(z)\,u_1(z)

form a fundamental system.

The requirement that $h_j$ be holomorphic on the full disc is the book's statement that the radius of convergence of $h_j$ is at least the smaller of the radii of convergence of $p$ and $q$ .

Milestones

In attack order:

Theorem 4.1. For $f$ analytic and bounded on the bidisc $\{|z-z_0|<\varepsilon, |w-w_0|<\delta\}$ with $M = \sup|f|$ , the problem $w' = f(z,w)$ , $w(z_0) = w_0$ has a unique analytic solution on $|z - z_0| < \min(\varepsilon, \delta/M)$ .
Lemma 4.4. For $p$ holomorphic on $0<|z|<R$ , the equation $u' + p(z)u = 0$ has a solution $z^\alpha h(z)$ with $h$ analytic at $0$ and $h(0) = 1$ if and only if $p$ has at most a first-order pole. In that case $\alpha = -\lim_{z\to0} zp(z)$ , and $h$ has radius of convergence at least $R$ .
Theorem 4.7. For $A$ , $b$ analytic on a simply connected domain $\Omega$ , the problem $w' = A(z)w + b(z)$ , $w(z_0) = w_0$ has a unique solution on all of $\Omega$ . Its power series at $z_0$ converges on the largest disc about $z_0$ contained in $\Omega$ .
Theorem 4.6 (Fuchs, converse). For $p, q$ holomorphic on a punctured disc, (4.20) has a fundamental system of the form in Theorem 4.5 if and only if $p$ and $zq$ have at most first-order poles.

Significance

Theorem 4.5 is the basic structural theorem for linear equations at a regular singular point. It determines the leading behaviour $z^{\alpha_j}$ of each solution from two numbers read off the coefficients. It says exactly when a logarithm can occur, and it guarantees that the series part converges on the full disc on which the coefficients converge. Theorem 4.6 shows that the regular-singular hypothesis cannot be weakened. The series expansions of Bessel functions $J_\nu$ , of Legendre functions and of the hypergeometric function $F(a,b,c;z)$ , and the logarithmic second solutions for integer order, are all instances of the theorem. The theorem is also the local ingredient of the classification of Fuchsian equations, including the Riemann $P$ -symbol.

Mathlib has holomorphic functions, power series with radius of convergence, the principal complex power and logarithm, and a real-variable ODE layer. It has no complex-analytic existence theorem for differential equations and no Frobenius theory. The results here are classical and proved in the book, but to our knowledge none of them has a machine-checked proof. The platform has real-variable regular-singular estimates (the RegularSingular namespace), which are a different setting. A formal Theorem 4.5 would give a foundation for formal special-function theory, for example Bessel functions defined as solutions of their equation.

Difficulty

The formal power-series computation is mechanical: substitute $z^\alpha\sum h_jz^j$ , compare coefficients, and read off the indicial equation and a recursion for the $h_j$ . The difficulty is everything around it. First, the recursion for the second exponent breaks down exactly when $\alpha_1 - \alpha_2 \in \mathbb{N}_0$ , and the form of the second solution changes there. Whether a logarithm really appears depends on a compatibility condition that can go either way when $m \ge 1$ . Second, the claim is about actual solutions on a slit domain, not formal series. This needs convergence estimates for the recursion and the principal branches of $z^\alpha$ and $\log z$ . Third, the radius claim asks for convergence on the whole disc of the coefficients, not just on some small disc. Fourth, linear independence of the two solutions has to be proved on the slit domain.

Milestones 1 and 3 need the complex analogues of Picard iteration and analytic continuation, which Mathlib does not supply for differential equations.

Formalization scope

Namespace TeschlODE.Frobenius. Complex derivatives are HasDerivAt/deriv/DifferentiableAt ℂ, and holomorphy on a set is DifferentiableOn ℂ. Radii are ENNReal, so $R = \infty$ is allowed. Discs are Metric.eball 0 R. Powers and logarithms are Mathlib's principal Complex.cpow and Complex.log, used only on slitDisc R = Metric.eball 0 R ∩ Complex.slitPlane. On the full punctured disc these functions are discontinuous along the negative axis, and the theorem would be false there. "Fundamental system" is linear independence over $\mathbb{C}$ on the solution domain. Without independence Case 1 would hold trivially with $u_2 = u_1$ . " $\alpha_1 - \alpha_2 \in \mathbb{N}_0$ " is ∃ m : ℕ, α₁ - α₂ = m. The book's "the constant $c$ might be zero unless $m=0$ " is the clause $m = 0 \Rightarrow c \ne 0$ .

Quantifier readings:

"Analytic near $z = 0$ " is strengthened to holomorphic on the whole disc of radius $R$ , as the book's radius claim asserts.
"Poles of order at most one and two" is given explicitly: $P, Q$ holomorphic on $|z|<R$ with $zp = P$ , $z^2q = Q$ on $0<|z|<R$ .
In Theorem 4.1, the case $M = 0$ is read as $\varepsilon_0 = \varepsilon$ . The supremum is over the nonempty bidisc, and a boundedness hypothesis is included.
In Lemma 4.4, "a solution of the form (4.29)" means one on some slit punctured disc of positive radius. The book's "the radii are the same" is corrected to "at least": $h(z) = 1 - z$ , $p(z) = 1/(1-z)$ is a counterexample to equality.
In Theorem 4.6, "as in the previous theorem" means the form (4.49) for some exponents and some $c$ (Case 1 is $c = 0$ ), on some slit punctured disc of radius $0 < \rho \le R$ .
In Theorem 4.7, "simply connected domain" is IsOpen Ω together with SimplyConnectedSpace Ω. "The largest disc" has radius Metric.infEDist z₀ Ωᶜ.

The trivializing formalization, with the two solutions not required to be linearly independent or with $h_j$ unconstrained away from $0$ , is ruled out by the independence clause and by requiring $h_j$ to be holomorphic on the whole disc with $h_j(0) = 1$ .

A full development needs the following: the complex Picard iteration, analytic continuation along paths (the monodromy theorem), Cauchy-type estimates for recursively defined power series, and the calculus of $z^\alpha$ and $\log z$ on the slit plane. The definitions slitDisc, IsSolution, charExponents and HasPoleOfOrderAtMost can be reused for the Bessel, Legendre and hypergeometric equations (Problems 4.5–4.18 of the book). Contributions such as a general complex-analytic ODE existence theorem are welcome.

Selected references

G. Teschl, Ordinary Differential Equations and Dynamical Systems, Graduate Studies in Mathematics 140, AMS, 2012, doi:10.1090/gsm/140; author's preliminary version, Chapter 4, mat.univie.ac.at/~gerald/ftp/book-ode/.
L. Fuchs, Zur Theorie der linearen Differentialgleichungen mit veränderlichen Coefficienten, J. reine angew. Math. 66 (1866), 121–160, doi:10.1515/crll.1866.66.121.
G. Frobenius, Ueber die Integration der linearen Differentialgleichungen durch Reihen, J. reine angew. Math. 76 (1873), 214–235, doi:10.1515/crll.1873.76.214.
E. L. Ince, Ordinary Differential Equations, Longmans, Green and Co., 1926 (Dover reprint 1956), Chapters XV–XVI.

9 thms1 active userReviewed

Algebraic Geometry Analysis Pure Mathematics·Captain: mikedeng1

Tasty Bits of Several Complex Variables X: Hypervarieties and Their Singular SetsTextbook

Motivation

Zero sets of holomorphic functions are the basic objects of local complex-analytic geometry. In one variable they are discrete, and nothing more needs to be said; in two or more variables the zero set of a single function is a surface, a curve or a higher-dimensional object that can have singular points, such as the cusp $\{z_1^3 = z_2^2\}$ or the crossing lines $\{z_1^2 = z_2^2\}$ in $\mathbb{C}^2$ . The theory of complex-analytic subvarieties describes these sets: where they are manifolds, what their dimension is, how they decompose into irreducible pieces, and how large their singular part can be. It underlies the local theory of singularities, the study of holomorphic maps and their fibres, and complex-analytic geometry more broadly (see Chirka, Complex Analytic Sets, https://doi.org/10.1007/978-94-009-2366-9, and Gunning–Rossi, Analytic Functions of Several Complex Variables).

This mission formalizes the part of this theory developed in §6.5–6.7 of Jiří Lebl's textbook Tasty Bits of Several Complex Variables (version 4.4, 2026, https://www.jirka.org/scv/scv.pdf), culminating in the theorem that the singular set of a hypervariety (a subvariety of pure codimension one) is itself a subvariety, of dimension at most $n-2$ .

Setting

Throughout, $\mathbb{C}^n$ is the space of $n$ -tuples $z = (z_1, \dots, z_n)$ , and a function on an open set is holomorphic if it is complex differentiable there.

A subvariety of an open set $U \subset \mathbb{C}^n$ is a set $X \subset U$ such that every point $p \in U$ has an open neighborhood $W \subset U$ and a family $\mathcal{F}$ of holomorphic functions on $W$ , possibly infinite, with

W \cap X = \{ z \in W : f(z) = 0 \text{ for all } f \in \mathcal{F} \}.

The condition is imposed near every point of $U$ , so a subvariety is closed in $U$ .

A point $p \in X$ is a regular point of dimension $k$ if, after a permutation of the coordinates, $z = (z', z'') \in \mathbb{C}^k \times \mathbb{C}^{n-k}$ , there are open sets $U' \ni p'$ , $U'' \ni p''$ and a holomorphic map $g : U' \to \mathbb{C}^{n-k}$ with

X \cap (U' \times U'') = \{ (z', z'') : z' \in U',\ z'' = g(z') \};

one writes $\dim_p X = k$ . The set of regular points is $X_{\mathrm{reg}}$ and the singular set is $X_{\mathrm{sing}} = X \setminus X_{\mathrm{reg}}$ . The subvariety $X$ has pure dimension $d$ if $\dim_q X = d$ at every regular point $q$ , and pure codimension $c$ if it has pure dimension $n - c$ . A subvariety of pure codimension one is a hypervariety. The dimension of $X$ is the maximum of $\dim_q X$ over $q \in X_{\mathrm{reg}}$ .

Local statements use germs. Sets $A$ , $B$ have the same germ at $p$ , written $(A,p) = (B,p)$ , if $A \cap W = B \cap W$ for some neighborhood $W$ of $p$ , and $(A,p) \subset (B,p)$ if $A \cap W \subset B \cap W$ . The ring $\mathcal{O}_p$ consists of germs at $p$ of functions holomorphic near $p$ , and

I_p(X) = \{ (f,p) \in \mathcal{O}_p : (X, p) \subset (Z_f, p) \}

is the ideal of germs vanishing on $X$ near $p$ , where $Z_f = f^{-1}(0)$ . A germ of a subvariety is reducible if it is the union of two germs of subvarieties neither of which contains the other, and irreducible otherwise.

Formalization targets

Goal: Theorem 6.6.5

For an open set $U \subset \mathbb{C}^n$ and a subvariety $X \subset U$ of pure codimension one,

X_{\mathrm{sing}} \text{ is a subvariety of } U \quad\text{and}\quad \dim X_{\mathrm{sing}} \le n - 2 .

Milestones

Theorem 6.5.9. For a domain $U$ and $f$ holomorphic on $U$ , the zero set $Z_f$ is empty, all of $U$ , or a subvariety of pure codimension one; and $(Z_f)_{\mathrm{reg}}$ is open and dense in $Z_f$ .
Lemma 6.5.10. For a nonempty subvariety $X$ , $X_{\mathrm{reg}} \neq \emptyset$ ; and $X_{\mathrm{reg}}$ is open and dense in $X$ .
Theorem 6.6.1. A germ $(X,p)$ of a hypervariety equals $(Z_f, p)$ for one holomorphic $f$ , and

I_p(X) = (f,p)\,\mathcal{O}_p .

Corollary 6.6.3. A hypervariety germ has a representative $X = X_1 \cup \cdots \cup X_k$ with each $X_\ell$ a hypervariety whose regular part is connected.
Proposition 6.7.3. Every germ of a subvariety is a finite union of irreducible germs of subvarieties, none contained in another.

Significance

The result itself. The goal theorem is the codimension-one case of the general statement that the singular locus of any complex-analytic subvariety is a subvariety of strictly smaller dimension (stated without proof in the book as Theorem 6.5.11). It makes induction on dimension possible for hypervarieties: removing the singular set leaves a complex manifold of dimension $n-1$ , and what is removed is again analytic and smaller. In particular, a complex curve in $\mathbb{C}^2$ given by one equation has only isolated singular points. Theorem 6.6.1 says that hypervarieties are exactly the sets locally cut out by one function generating the full ideal of vanishing germs, which fails in higher codimension (Example 6.6.2 gives a codimension-two subvariety of $\mathbb{C}^6$ not cut out by two functions).

Formalizing it. To our knowledge no proof assistant library currently contains complex-analytic subvarieties of open subsets of $\mathbb{C}^n$ , their regular and singular points, or local dimension. Mathlib has schemes and Zariski-closed sets, which are algebraic and do not cover analytic sets such as $\{z_2 = e^{1/z_1}\}$ , and it has germs of functions and one-variable zero sets of analytic functions. The mission therefore builds the basic vocabulary of local analytic geometry, and proves its first structural theorems, from the book's proofs.

Difficulty

Being a subvariety is a local condition near every point of $U$ , and the singular set is defined negatively, as the points where no coordinate projection exhibits $X$ as a graph. To show $X_{\mathrm{sing}}$ is a subvariety one has to produce holomorphic functions whose common zeros in $X$ are exactly the singular points. There is no natural finite list of them: the discriminants from one generic linear coordinate system do not suffice, because the book shows that near some regular points every fixed coordinate system sees a non-simple root (Figure 6.7). The proof needs infinitely many coordinate changes. It also needs Weierstrass preparation, the discriminant of a Weierstrass polynomial, and the principal-ideal description of Theorem 6.6.1. None of these are in Mathlib for convergent power series in several variables. The dimension bound is a separate claim: knowing that $X_{\mathrm{sing}}$ is a subvariety does not by itself exclude that it contains an $(n-1)$ -dimensional manifold piece.

Formalization scope

$\mathbb{C}^n$ is Fin n → ℂ. Holomorphic on an open set is DifferentiableOn ℂ, which is equivalent to the book's Definition 1.1.2 on open sets. A domain is IsOpen U ∧ IsConnected U (nonempty).
IsSubvariety U X includes IsOpen U and X ⊆ U; the families $\mathcal{F}$ are arbitrary sets of functions.
A regular point uses an equivalence Fin n ≃ Fin k ⊕ Fin m for the permutation and the split into $z'$ , $z''$ , so no natural-number subtraction occurs.
Dimensions and codimensions are integers: "pure codimension 1" is "every regular point has dimension $n-1$ " computed in ℤ, and " $\dim X_{\mathrm{sing}} \le n-2$ " is "every regular point of $X_{\mathrm{sing}}$ has dimension $\le n-2$ " in ℤ. For $n = 1$ the bound is $-1$ , so the singular set must be empty. For $X_{\mathrm{sing}} = \emptyset$ the bound holds vacuously, where the book's maximum over the empty set is undefined.
Germs of sets are not quotients: GermEq and GermSubset are the relations of Definition 6.1.3. $\mathcal{O}_p$ is a Subring of Mathlib's Filter.Germ (nhds p) ℂ, and $I_p(X)$ is an Ideal of it. "Generated by $(f,p)$ " is Ideal.span {(f,p)}.
A germ of a pure-codimension-one subvariety is given by a representative subvariety $X \subset U$ with $p \in U$ . The conclusions depend only on the germ.
Lemma 6.5.10 is stated with the proviso $X \neq \emptyset$ for its first clause; without it the page's sentence is false for $X = \emptyset$ .
The goal is not trivialized by an empty or degenerate reading: the hypotheses are met by every zero set of a nonconstant holomorphic function, and the conclusion requires both the subvariety property of $X_{\mathrm{sing}}$ near every point of $U$ and the dimension bound, not merely the existence of some description of $X_{\mathrm{sing}}$ .

Infrastructure a complete development needs is Weierstrass preparation and division for convergent power series in several variables, the discriminant of a Weierstrass polynomial (Theorem 6.3.3), Noetherianity of $\mathcal{O}_p$ , and the Riemann extension theorem. All of them can be reused well beyond this mission. Contributions of any of these are welcome, as are proofs of the milestones independently of the goal.

Selected references

Jiří Lebl, Tasty Bits of Several Complex Variables: A Whirlwind Tour of the Subject, version 4.4, 2026, §6.5–6.7. https://www.jirka.org/scv/scv.pdf
E. M. Chirka, Complex Analytic Sets, Mathematics and Its Applications 46, Kluwer, 1989. https://doi.org/10.1007/978-94-009-2366-9
Stanisław Łojasiewicz, Introduction to Complex Analytic Geometry, Birkhäuser, 1991. https://doi.org/10.1007/978-3-0348-7617-9
Robert C. Gunning and Hugo Rossi, Analytic Functions of Several Complex Variables, Prentice-Hall, 1965; reprinted AMS Chelsea, 2009. https://bookstore.ams.org/chel-368

19 thms1 active userReviewed

Algebra Algebraic Geometry Analysis+1·Captain: mikedeng1

Tasty Bits of Several Complex Variables IX: Weierstrass Preparation and the Ring of GermsTextbook

Why the ring of germs

Local complex analytic geometry studies zero sets of holomorphic functions near a point. The natural algebraic object for this is the ring of germs $\mathcal{O}_p$ of holomorphic functions at $p \in \mathbb{C}^n$ : two functions are identified if they agree near $p$ . The ring $\mathcal{O}_p$ is the local ring of the complex manifold $\mathbb{C}^n$ at $p$ in the sense of analytic geometry; its algebraic properties (Noetherian, integral domain, unique factorization) are what make the local theory of analytic varieties, their irreducible components and their singular sets work. This mission formalizes the section of Jiří Lebl's textbook Tasty Bits of Several Complex Variables (jirka.org/scv) that establishes these properties, together with the two tools they rest on, the Weierstrass preparation and division theorems.

The preparation theorem goes back to Weierstrass (published 1886). Rückert (1933) used preparation and division to prove that the ring of convergent power series is Noetherian, the starting point of the algebraic treatment of local analytic geometry.

Setting

A point of $\mathbb{C}^n$ is $z = (z_1, \dots, z_n)$ ; when a last variable is singled out, $z = (z', z_n)$ with $z' \in \mathbb{C}^{n-1}$ . A function on an open set is holomorphic if it is complex differentiable there; $\mathcal{O}(U)$ is the set of holomorphic functions on $U$ . A domain is a nonempty connected open set.

A germ at $p$ is an equivalence class of functions defined on neighborhoods of $p$ , two functions being equivalent if they agree on some neighborhood of $p$ . Germs of complex-valued functions form a commutative ring under pointwise operations of representatives. The ring of germs of holomorphic functions $\mathcal{O}_p = {}_n\mathcal{O}_p$ consists of the germs having a representative holomorphic on a neighborhood of $p$ .

For $f$ holomorphic near $p$ , write $f(z) = \sum_k f_k(z - p)$ with $f_k$ homogeneous of degree $k$ . The order of vanishing $\operatorname{ord}_p f$ is the least $k$ with $f_k \not\equiv 0$ , and $\infty$ if $f \equiv 0$ .

A Weierstrass polynomial of degree $k \ge 0$ on an open $U \ni 0$ in $\mathbb{C}^{n-1}$ is a monic polynomial in $z_n$ ,

P(z', z_n) = z_n^k + \sum_{\ell=0}^{k-1} c_\ell(z')\, z_n^\ell,

with coefficients $c_\ell$ holomorphic on $U$ and $c_\ell(0) = 0$ . A polydisc is a product of open discs. For a fixed $z'$ , zeros of $z_n \mapsto f(z', z_n)$ are geometrically distinct if they are distinct points; a zero is geometrically unique if it is the only one.

Formalization targets

Goal: Theorem 6.4.2

For every $n$ and $p \in \mathbb{C}^n$ ,

\mathcal{O}_p \text{ is a unique factorization domain:}

it is an integral domain, and up to multiplication by units and permutation every nonzero nonunit has a unique factorization into irreducible elements of $\mathcal{O}_p$ .

Milestones

In attack order:

Theorem 6.2.3 (Weierstrass preparation). If $f \in \mathcal{O}(U)$ , $0 \in U$ , $f(0) = 0$ , and $z_n \mapsto f(0, z_n)$ has order of vanishing $k \ge 1$ at $0$ , then on some open polydisc $V = V' \times D$ with $0 \in V \subset U$ ,

f(z', z_n) = u(z', z_n)\, P(z', z_n)

with $u \in \mathcal{O}(V)$ nowhere zero and $P$ a Weierstrass polynomial of degree $k$ with coefficients holomorphic in $V'$ whose zeros in $z_n$ lie in $D$ for all $z' \in V'$ ; $u$ and $P$ are unique. 2. Theorem 6.2.5 (Weierstrass division). For $f$ holomorphic near $0$ and $P$ a Weierstrass polynomial of degree $k \ge 1$ , there are a neighborhood $V$ of $0$ and unique $q, r \in \mathcal{O}(V)$ , $r$ a polynomial in $z_n$ of degree less than $k$ , with $f = qP + r$ on $V$ . 3. Proposition 6.3.1. On domains $U' \times D$ , if for every $z' \in U'$ the function $z_n \mapsto f(z', z_n)$ has a geometrically unique zero $\alpha(z') \in D$ , then $\alpha$ is holomorphic in $U'$ . 4. Theorem 6.3.3 (discriminant). For $D$ a bounded domain, $U'$ a domain, $f \in \mathcal{O}(U' \times D)$ whose zero set has no limit points on $U' \times \partial D$ , there are $m$ and a holomorphic $\Delta \not\equiv 0$ on $U'$ such that $z_n \mapsto f(z', z_n)$ has exactly $m$ geometrically distinct zeros in $D$ for $\Delta(z') \ne 0$ and fewer than $m$ for $\Delta(z') = 0$ . 5. Theorem 6.4.1. $\mathcal{O}_p$ is Noetherian.

Significance

The preparation theorem reduces a holomorphic function near a point, after a unit, to a polynomial in one variable over the ring of functions of the others; the division theorem is division with remainder by such a polynomial. Together they turn $\mathcal{O}_0$ in $n$ variables into an object controlled by the polynomial ring $\mathcal{O}_0[z_n]$ in $n - 1$ variables, and that is how both the Noetherian property and unique factorization are proved. Unique factorization gives the decomposition of a germ of a hypersurface into irreducible components; the Noetherian property says that every germ of an analytic variety is cut out by finitely many functions. Proposition 6.3.1 and Theorem 6.3.3 describe how the zeros of $z_n \mapsto f(z', z_n)$ move with $z'$ , the input to the study of hypervarieties in the following sections.

The results are classical. The book proves them, leaving some steps as exercises: uniqueness in the division theorem (Exercise 6.2.10), the one-variable cases of 6.4.1 and 6.4.2 (Exercises 6.4.2, 6.4.6), and the irreducibility step in 6.4.2 (Exercise 6.4.7). Mathlib has the algebra (Noetherian rings, unique factorization monoids, Hilbert's basis theorem, the Gauss lemma for polynomial rings), germs along filters, and one-variable complex analysis. The platform has the Weierstrass preparation and division theorems for formal power series over complete local rings. None of the statements of this mission about convergent germs and holomorphic functions has a machine-checked proof.

Difficulty

The statements concern convergent objects, and the algebra alone does not see convergence. The formal preparation and division theorems produce a factorization or a quotient as formal power series; they do not say that the output converges, nor that it is holomorphic on a fixed neighborhood, nor where the zeros of the Weierstrass polynomial lie. Likewise, the formal power series ring is known to be a Noetherian UFD, but $\mathcal{O}_p$ is a proper subring and neither property passes to subrings. The coefficients of the Weierstrass polynomial are built from the zeros of $z_n \mapsto f(z', z_n)$ , which in general cannot be chosen continuously in $z'$ (the two square roots of $z_1$ already show this), so the holomorphy of the coefficients cannot come from the zeros one at a time.

For the goal, the induction on $n$ requires identifying $\mathcal{O}_0$ in $n - 1$ variables, its polynomial ring, and a subring of $\mathcal{O}_0$ in $n$ variables, and moving between germs and representatives on explicit neighborhoods. A linear change of coordinates is needed to reach the hypothesis of the preparation theorem, so invariance of $\mathcal{O}_p$ under such changes is also part of the work.

Formalization scope

$\mathbb{C}^n$ is Fin n → ℂ; where a last variable is singled out, $\mathbb{C}^{n-1} \times \mathbb{C}$ is (Fin d → ℂ) × ℂ with $d = n - 1$ , so $d = 0$ is the case $n = 1$ . Holomorphic on an open set is DifferentiableOn ℂ, which agrees with the book's Definition 1.1.2 on open sets.
$\mathcal{O}_p$ is GermRing n p: the subring of Mathlib's germ ring (𝓝 p).Germ ℂ of germs with a representative complex-differentiable at every point near $p$ . The goal produces the IsDomain structure and asserts UniqueFactorizationMonoid; Theorem 6.4.1 is IsNoetherianRing.
Ruled out: replacing $\mathcal{O}_p$ by the ring of all germs of functions (not a domain) or by formal power series MvPowerSeries (Fin n) ℂ. Both change the theorem; convergence is the whole point.
The order of vanishing is ℕ∞-valued: the least $k$ with nonzero $k$ -th derivative at $p$ , and $\infty$ if there is none.
A Weierstrass polynomial is given by its coefficient tuple $c_0, \dots, c_{k-1}$ ; the polydisc $V' \times D$ of Theorem 6.2.3 is a coordinatewise polydisc with positive radii times an open disc, both centers arbitrary as in the book. "All $k$ zeros lie in $D$ " is stated as "every zero lies in $D$ ", equivalent for a monic polynomial of degree $k$ . Uniqueness in 6.2.3 and 6.2.5 is uniqueness on the $V$ produced.
In Theorem 6.3.3 zeros are counted as distinct points with Set.encard. The book writes $m \in \mathbb{N}$ with $\mathbb{N} = \{1, 2, \dots\}$ ; the statement allows $m = 0$ , since for $f$ without zeros no $m \ge 1$ can satisfy the conclusion.

A complete development needs the one-variable argument principle and Cauchy integral formula with holomorphic parameters, Newton's identities, Radó's theorem (for 6.3.3), Hilbert's basis theorem and the Gauss lemma (in Mathlib), and the identification of $\mathcal{O}_0$ in $n - 1$ variables with a subring of $\mathcal{O}_0$ in $n$ variables. A general API for rings of holomorphic germs and their changes of coordinates is reusable in the next mission of this series (hypervarieties and their singular sets); contributions of it as standalone lemmas are welcome.

Selected references

J. Lebl, Tasty Bits of Several Complex Variables, version 4.4, 2026, Chapter 6, §§6.1–6.4. https://www.jirka.org/scv/scv.pdf
W. Rückert, "Zum Eliminationsproblem der Potenzreihenideale", Mathematische Annalen 107 (1933).
R. C. Gunning and H. Rossi, Analytic Functions of Several Complex Variables, Prentice-Hall, 1965; reprint AMS Chelsea, 2009, Chapter II.

10 thms1 active userReviewed

Analysis Functional Analysis Pure Mathematics·Captain: mikedeng1

Tasty Bits of Several Complex Variables VIII: The Bergman KernelTextbook

Motivation

On a domain in $\mathbb{C}^n$ with $n \ge 2$ there is in general no Cauchy integral formula whose kernel is holomorphic in the evaluation point and independent of choices: the Bochner–Martinelli kernel works on every domain but is not holomorphic in the right variable. The Bergman kernel is the canonical replacement. It is attached to every domain $U \subset \mathbb{C}^n$ , it reproduces every square-integrable holomorphic function on $U$ , and it is holomorphic in one variable and antiholomorphic in the other. Stefan Bergman introduced it in one and several variables in the 1920s–1930s (Bergman, The Kernel Function and Conformal Mapping, 1950). Aronszajn's theory of reproducing kernels (Aronszajn 1950) places it inside a general Hilbert-space framework. The kernel's boundary behaviour is the central tool in Fefferman's theorem that biholomorphisms between smoothly bounded strongly pseudoconvex domains extend smoothly to the boundary (Fefferman 1974).

This mission formalizes the construction of the kernel and its basic structure theory, following Chapter 5 of Jiří Lebl's Tasty Bits of Several Complex Variables (version 4.4, 2026).

Setting

Write $\mathbb{C}^n$ for Fin n → ℂ and $dV$ for Lebesgue measure on $\mathbb{C}^n \cong \mathbb{R}^{2n}$ (volume). A domain is a connected open set $U \subset \mathbb{C}^n$ . The space $L^2(U)$ consists of the square-integrable functions on $U$ , modulo equality almost everywhere. It carries the inner product

\langle f, g \rangle = \int_U f(z)\,\overline{g(z)}\, dV(z).

The Bergman space bergmanSpace U is

A^2(U) = \mathcal{O}(U) \cap L^2(U).

It consists of those classes in $L^2(U)$ that contain a function holomorphic on $U$ (DifferentiableOn ℂ). It is a linear subspace of $L^2(U)$ and carries the $L^2$ norm $\|f\|_{A^2(U)}$ . For $f \in A^2(U)$ and $z \in U$ , $f(z)$ denotes the value at $z$ of the holomorphic function in the class (holoRep U f z). This value is unambiguous because $U$ is open.

For $z \in U$ , suppose there is an element $k_z \in A^2(U)$ with

f(z) = \langle f, k_z \rangle \quad \text{for all } f \in A^2(U).

Such a $k_z$ is unique (bergmanRepresenter U z). The Bergman kernel is then

K_U(z, \bar\zeta) = \overline{k_z(\zeta)}, \qquad (z, \bar\zeta) \in U \times U^*, \quad U^* = \{\zeta : \bar\zeta \in U\}.

In Lean, bergmanKernel U z ζ is $K_U(z, \bar\zeta)$ : the second argument is $\zeta$ itself, and pairs range over $U \times U$ .

A family $\{\varphi_\ell\}_{\ell \in I}$ in $A^2(U)$ , over an arbitrary index set $I$ , is a complete orthonormal system (IsCompleteOrthonormalSystem U φ) if it is orthonormal and its linear span is dense in $A^2(U)$ .

Formalization targets

Goal: Proposition 5.2.5 (p. 163)

Let $U \subset \mathbb{C}^n$ be a domain and let $\{\varphi_\ell\}_{\ell\in I}$ be a complete orthonormal system for $A^2(U)$ . Then

K_U(z, \bar\zeta) = \sum_{\ell \in I} \varphi_\ell(z)\,\overline{\varphi_\ell(\zeta)},

with uniform convergence on compact subsets of $U \times U^*$ . In Lean the conclusion reads as follows: for every compact $L \subset U \times U$ , the finite partial sums over $s \subset I$ converge to bergmanKernel U z ζ uniformly on $L$ as $s$ increases along the finite subsets of $I$ .

Milestones

Lemma 5.2.1 (p. 161). For a domain $U$ and compact $K \subset U$ there is a constant $C_K$ with $\sup_{z\in K}|f(z)| \le C_K \|f\|_{A^2(U)}$ for all $f \in A^2(U)$ . Consequently, $A^2(U)$ is complete.
Eq. (5.1) (p. 162), the reproducing property. For $f \in A^2(U)$ and $z \in U$ ,

f(z) = \int_U f(\zeta)\,K_U(z, \bar\zeta)\, dV(\zeta),

with integrable integrand. 3. Proposition 5.2.2 (p. 162). $K_U(z, \bar\zeta)$ is holomorphic in $z$ and antiholomorphic in $\zeta$ , and $\overline{K_U(z, \bar\zeta)} = K_U(\zeta, \bar z)$ .

Significance

The result itself. The Bergman kernel can rarely be written in closed form. Proposition 5.2.5 computes it from any orthonormal basis of $A^2(U)$ . For the unit ball, the normalized monomials give the closed form $K_{\mathbb{B}_n}(z,\bar\zeta) = \frac{n!}{\pi^n}(1 - \langle z, \zeta\rangle)^{-(n+1)}$ (Exercises 5.2.9–5.2.10). For the polydisc they give a product of one-variable kernels (Exercise 5.2.8). The expansion is also the standard route to the kernel's positivity on the diagonal, $K_U(z,\bar z) = \sum_\ell |\varphi_\ell(z)|^2$ , and so to the Bergman metric. Lemma 5.2.1, the milestone underneath, is what makes $A^2(U)$ a Hilbert space and point evaluation continuous. It is the reason a reproducing kernel exists at all.

Formalizing it. These results are classical and fully proved in the book. As far as a search of the platform shows, none of them has a machine-checked proof: Mathlib has $L^2$ spaces, Hilbert bases and the Riesz representation theorem, but no Bergman space. The platform's reproducing-kernel entries (Moore–Aronszajn, real-valued RKHS statements) start from a positive semidefinite kernel, which is the opposite direction and not about $A^2(U)$ . What remains is to formalize the known proofs, and to build a reusable Bergman-space layer on which the biholomorphic transformation law (Exercise 5.2.7) and explicit kernels could later be stated.

Difficulty

The obvious argument for the goal expands $z \mapsto K_U(z, \bar\zeta)$ in the orthonormal system. For each fixed $\zeta$ , that expansion converges in $L^2$ in the variable $z$ only. Upgrading $L^2$ convergence to uniform convergence on compacts in $z$ needs Lemma 5.2.1. Uniformity in the pair $(z, \zeta)$ is a further step: a bound for each fixed $\zeta$ does not give it, and the tails must be controlled simultaneously in both variables. The sum is over an arbitrary index set, so the convergence to be proved is that of an unordered sum, uniformly on a compact set.

On the formal side, elements of $L^2$ are equivalence classes. Every pointwise statement therefore passes through the holomorphic representative, and needs the fact that continuous functions agreeing almost everywhere on an open set agree on it. Lemma 5.2.1 needs the mean-value property on polydiscs, and Cauchy–Schwarz on a polydisc inside $U$ . The kernel exists only once completeness of $A^2(U)$ and the Riesz representation theorem are combined.

Formalization scope

$\mathbb{C}^n$ is Fin n → ℂ with volume, the product of Lebesgue measures on $\mathbb{C} \cong \mathbb{R}^2$ ; this is $dV$ . No Euclidean ball or norm appears in any statement, so the sup norm on Fin n → ℂ plays no role.
A domain is IsOpen U ∧ IsConnected U. Holomorphic means DifferentiableOn ℂ on the open set $U$ , which is equivalent to the book's Definition 1.1.2 by Osgood's lemma (Proposition 1.1.3, Theorem 1.2.1).
$A^2(U)$ is a Submodule ℂ of Lp ℂ 2 (volume.restrict U), with the $L^2$ norm and inner product. Mathlib's inner product is conjugate-linear in its first argument. The book's $\langle f, g\rangle$ is therefore written as an explicit integral $\int_U f\,\bar g\,dV$ wherever the order matters (the definition of $k_z$ ). Orthonormality does not depend on the convention.
bergmanKernel U z ζ means $K_U(z,\bar\zeta)$ . Compact subsets of $U\times U^*$ in the variables $(z,\bar\zeta)$ correspond to compact subsets of $U \times U$ in the variables $(z,\zeta)$ .
The kernel is defined by choice: $k_z$ is an element satisfying the reproducing identity, with fallback $0$ if none exists. The fallback cannot make the goal trivially true: by Lemma 5.2.1 and Riesz a representer exists at every point of a domain, and the goal is equivalent to the book's statement for the actual kernel. The goal's convergence is uniform on compact sets, not merely pointwise, and the sum is unordered over an arbitrary index type. Replacing either by pointwise convergence or by a fixed enumeration would state a weaker theorem.
The reproducing property includes integrability of its integrand in its conclusion, so it cannot hold through the Bochner integral's default value $0$ .
Not included. Theorem 5.1.1 (Bochner–Martinelli) is not included. It needs integration of $(n,n-1)$ -forms over a smooth boundary, which Mathlib lacks, and the goal does not use it. The Szegő kernel (§5.3) is sketched in the book without numbered results. Examples 5.2.3–5.2.4 and the exercises are not results and are not stated.

A complete development needs the following:

the mean-value property of holomorphic functions on polydiscs;
closedness of $A^2(U)$ in $L^2(U)$ ;
Riesz representation (InnerProductSpace.toDual);
expansions in Hilbert bases (HilbertBasis);
uniform convergence of unordered sums of functions on compact sets.

The Bergman-space layer (holomorphic representatives, continuity of point evaluation, the kernel) is reusable for any later work on Bergman metrics, transformation laws or explicit kernels. Contributions of that layer as separate lemmas are welcome.

Selected references

J. Lebl, Tasty Bits of Several Complex Variables: A Whirlwind Tour of the Subject, version 4.4, 2026, Chapter 5. https://www.jirka.org/scv/scv.pdf
S. Bergman, The Kernel Function and Conformal Mapping, Mathematical Surveys 5, American Mathematical Society, 1950 (2nd ed. 1970). https://doi.org/10.1090/surv/005
N. Aronszajn, Theory of reproducing kernels, Transactions of the American Mathematical Society 68 (1950), 337–404. https://doi.org/10.1090/S0002-9947-1950-0051437-7
C. Fefferman, The Bergman kernel and biholomorphic mappings of pseudoconvex domains, Inventiones Mathematicae 26 (1974), 1–65. https://doi.org/10.1007/BF01406845

8 thms1 active userReviewed

Analysis Partial Differential Equations Pure Mathematics·Captain: mikedeng1

Tasty Bits of Several Complex Variables VI: The Hartogs PhenomenonTextbook

Motivation

In one complex variable every open set is the natural domain of some holomorphic function: $1/z$ on a punctured disc cannot be continued across the puncture. In two or more variables this fails in a striking way. Hartogs observed in 1906 that a function holomorphic on the complement of a compact set inside a domain always extends across the hole (Hartogs, Math. Ann. 62, 1906). This Hartogs phenomenon is the first place where several complex variables departs from the one-variable theory, and it forces the notions of domain of holomorphy and pseudoconvexity that organize the rest of the subject.

Timeline. Hartogs's original argument (1906) had gaps. A complete proof was given by Fueter in 1939 for $n = 2$ , and independently by Bochner and Martinelli for general $n$ in the early 1940s. The proof now standard, via the compactly supported $\bar\partial$ -problem, is due to Ehrenpreis (Ehrenpreis, Bull. Amer. Math. Soc. 67, 1961). This mission follows the presentation in §4.1–4.3 of Lebl's textbook (Lebl, version 4.4, 2026).

Setting

Write $\mathbb{C}^n$ for $n$ -tuples $z = (z_1, \dots, z_n)$ of complex numbers, $z_k = x_k + i y_k$ . A domain is a nonempty connected open set. A function on an open set is holomorphic if it is complex differentiable there (for open sets this agrees with the textbook's definition by local boundedness and separate holomorphy).

The Wirtinger derivatives of a differentiable function $f$ are

\frac{\partial f}{\partial \bar z_k} = \frac12\left(\frac{\partial f}{\partial x_k} + i\,\frac{\partial f}{\partial y_k}\right), \qquad k = 1, \dots, n,

and in one variable $\partial f/\partial\bar z = \tfrac12(\partial_x f + i\,\partial_y f)$ . A $C^1$ function is holomorphic exactly when all $\partial f/\partial\bar z_k$ vanish.

A $(0,1)$ -form is an expression $g = g_1\,d\bar z_1 + \cdots + g_n\,d\bar z_n$ with coefficient functions $g_j$ . For a smooth $\psi$ , $\bar\partial\psi = \sum_k \frac{\partial\psi}{\partial\bar z_k}\,d\bar z_k$ , so the equation $\bar\partial\psi = g$ is the system $\partial\psi/\partial\bar z_k = g_k$ for all $k$ . Since mixed partial derivatives commute, a solution can exist only if the compatibility conditions $\partial g_k/\partial\bar z_\ell = \partial g_\ell/\partial\bar z_k$ hold.

In one variable, the area element is written $d\zeta\wedge d\bar\zeta = (-2i)\,dA$ , where $dA = dx\,dy$ is Lebesgue measure on $\mathbb{C}$ .

Formalization targets

Goal: the Hartogs phenomenon (Theorem 4.3.1)

Let $n \ge 2$ , $U \subset \mathbb{C}^n$ a domain, $K \subset U$ compact with $U \setminus K$ connected, and $f$ holomorphic on $U \setminus K$ . Then

\exists!\, F \in \mathcal{O}(U) \text{ with } F|_{U \setminus K} = f,

where uniqueness means any two such extensions agree on $U$ .

Milestones

Cauchy–Pompeiu formula (Theorem 4.1.1), on a disc $U$ : for $f$ continuous on $\overline U$ with bounded continuous partial derivatives in $U$ and $z \in U$ ,

f(z) = \frac{1}{2\pi i}\int_{\partial U}\frac{f(\zeta)}{\zeta - z}\,d\zeta + \frac{1}{2\pi i}\int_U \frac{\partial f/\partial\bar\zeta(\zeta)}{\zeta - z}\,d\zeta\wedge d\bar\zeta.

One-variable $\bar\partial$ (Lemma 4.4.6), on a disc $U$ : for $g$ smooth near $\overline U$ , $\psi(z) = \frac{1}{2\pi i}\int_U \frac{g(\zeta)}{\zeta - z}\,d\zeta\wedge d\bar\zeta$ is smooth on $U$ with $\partial\psi/\partial\bar z = g$ .
Compactly supported $\bar\partial$ -problem (Theorem 4.2.1): for $n \ge 2$ and compactly supported smooth $g_1, \dots, g_n$ satisfying the compatibility conditions, there is a unique compactly supported smooth $\psi$ with $\bar\partial\psi = g$ .
Zero sets (Corollary 4.3.2): for $n \ge 2$ and $f$ holomorphic on a domain, a nonempty zero set $f^{-1}(0)$ is never compact.

Significance

The result. The Hartogs phenomenon shows that isolated singularities, and more generally compact singular sets, do not exist for holomorphic functions of several variables. Direct consequences include Corollary 4.3.2, the fact that the complement of a bounded domain of holomorphy is connected, and the extension of CR functions from the boundary of a bounded domain (the Hartogs–Bochner and Severi theorems). It is the reason the domain of a holomorphic function in $\mathbb{C}^n$ carries geometric information, which leads to pseudoconvexity and the Levi problem. Theorem 4.2.1 is the simplest solvability statement for the $\bar\partial$ -equation, a model for the Dolbeault and Hörmander $L^2$ theories.

Formalizing it. All results here are classical and proved in the book; none is formalized. Mathlib has the one-variable Cauchy integral formula on discs, but it has no Cauchy–Pompeiu formula, no Cauchy transform with a $\bar\partial$ identity, and no $\bar\partial$ -problem in $\mathbb{C}^n$ . A complete development would provide a reusable one-variable $\bar\partial$ solution operator, differentiation under a singular integral, and the removable-compact-set theorem for holomorphic functions of several variables.

Difficulty

The first idea, extending $f$ one complex line at a time by one-variable Cauchy integrals, works only for special shapes of $K$ (Hartogs figures): for a general compact $K$ with connected complement the one-variable slices of $U \setminus K$ can be complicated, and patching slice-wise extensions into one holomorphic function is where the historical proofs had gaps. The milestones carry their own analytic difficulties. The kernel $1/(\zeta - z)$ is singular, so the area integrals must first be shown to converge, and a $\bar z$ -derivative cannot be moved naively under the integral (doing so would give $0$ , contradicting Lemma 4.4.6). In Theorem 4.2.1 the delicate point is compact support of the solution, which is where $n \ge 2$ enters: for $n = 1$ the equation is solvable but in general has no compactly supported solution.

Formalization scope

$\mathbb{C}^n$ is Fin n → ℂ; functions are total, and only their values on the sets named in the hypotheses matter. Holomorphic is DifferentiableOn ℂ on an open set. A domain is IsOpen U ∧ IsConnected U. " $K \subset\subset U$ compact" is IsCompact K ∧ K ⊆ U. The hypothesis $n \ge 2$ is 2 ≤ n and is essential.
wirtingerBar k f is $\tfrac12(\partial_{x_k}f + i\,\partial_{y_k}f)$ built from real one-variable derivs; dbar f is its one-variable analogue. Smooth means real $C^\infty$ (ContDiff ℝ ∞), not analytic; compact support is HasCompactSupport.
In Theorem 4.1.1 and Lemma 4.4.6 the book allows any bounded open set with piecewise- $C^1$ boundary; the formalization restricts to open discs, since Mathlib has no boundary integral over such sets. The boundary integral is circleIntegral, and $\int_U \cdots d\zeta\wedge d\bar\zeta$ is $(-2i)$ times the Lebesgue (Bochner) integral over the disc. Integrability of the singular integrand is part of the conclusion, so a vanishing Bochner integral cannot make a statement hold vacuously.
Uniqueness in the goal is agreement on $U$ of any two holomorphic extensions (values off $U$ are unconstrained); in Theorem 4.2.1 it is ∃! among compactly supported smooth functions.
Trivializations ruled out: the goal is not stated for $n = 1$ , it does not assume $f$ already holomorphic on $U$ , and it does not replace "extends" by the existence of some function on $U$ without the agreement $F = f$ on $U \setminus K$ .
Omitted: Corollary 4.3.3 (Severi), which needs real-analytic hypersurfaces and CR functions.
Needed infrastructure: Green's theorem on a disc or an equivalent polar-coordinate argument, local integrability of $1/|\zeta|$ in the plane, differentiation under the integral sign, smooth cutoff functions, and the identity theorem in $\mathbb{C}^n$ . Reusable contributions in any of these are welcome.

Selected references

J. Lebl, Tasty Bits of Several Complex Variables, version 4.4, 2026, §4.1–4.3, pp. 130–137. https://www.jirka.org/scv/scv.pdf
F. Hartogs, Zur Theorie der analytischen Funktionen mehrerer unabhängiger Veränderlichen, insbesondere über die Darstellung derselben durch Reihen, welche nach Potenzen einer Veränderlichen fortschreiten, Math. Ann. 62 (1906), 1–88.
L. Ehrenpreis, A new proof and an extension of Hartog's theorem, Bull. Amer. Math. Soc. 67 (1961), 507–509.
L. Hörmander, An Introduction to Complex Analysis in Several Variables, 3rd ed., North-Holland, 1990, Theorem 2.3.2.

7 thms1 active userReviewed

Analysis Differential Geometry Pure Mathematics·Captain: mikedeng1

Tasty Bits of Several Complex Variables III: Hartogs Figures, the Levi Form and the Tomato Can PrincipleTextbook

Motivation

In one complex variable every domain is the natural domain of some holomorphic function. In several variables this fails: there are open sets $U \subset \mathbb{C}^n$ , $n \ge 2$ , on which every holomorphic function extends past part of the boundary. The first example is the Hartogs figure (Hartogs, 1906). The question of which domains are natural domains of holomorphic functions, the domains of holomorphy, drove the development of the subject for half a century. E. E. Levi (1911) found a necessary condition for domains with smooth boundary: a sign condition on a Hermitian form attached to the boundary, now called the Levi form. The converse, the Levi problem, was settled in the 1950s by Oka, Bremermann and Norguet. Hörmander's $L^2$ approach is a later proof (Hörmander, An Introduction to Complex Analysis in Several Variables).

This mission follows §2.1–2.3 of J. Lebl, Tasty Bits of Several Complex Variables (version 4.4, 2026, jirka.org/scv). Those sections go from the Hartogs figure and the continuity principle, through tangent vectors and the Levi form of a smooth boundary, to the tomato can principle. That principle is the easy direction of the Levi problem: a domain of holomorphy with smooth boundary has no negative Levi eigenvalue.

Setting

Write $\mathbb{C}^n$ for $n$ -tuples $z = (z_1, \dots, z_n)$ with $z_\ell = x_\ell + i y_\ell$ , and $\mathbb{D} = \{\xi \in \mathbb{C} : |\xi| < 1\}$ . A function on an open set is holomorphic if it is complex differentiable at every point, and $\mathcal{O}(U)$ is the set of holomorphic functions on $U$ . $\Delta_s(p)$ is the polydisc of radius $s$ about $p$ , the set where every coordinate satisfies $|z_\ell - p_\ell| < s$ .

A domain is a nonempty connected open set. A domain $U$ is a domain of holomorphy if there are no nonempty open sets $V, W$ with $W$ connected, $V \subset U \cap W$ and $W \not\subset U$ such that every $f \in \mathcal{O}(U)$ agrees on $V$ with some $F \in \mathcal{O}(W)$ .

Identify $\mathbb{C}^n$ with $\mathbb{R}^{2n}$ . An open set $U$ has smooth boundary if every $p \in \partial U$ has an open neighbourhood $V$ and a $C^\infty$ function $r : V \to \mathbb{R}$ with the following properties:

the derivative of $r$ never vanishes on $V$ ;
$\partial U \cap V = \{ r = 0 \}$ ;
$r < 0$ on $U \cap V$ and $r > 0$ on $V \setminus \overline{U}$ .

Such an $r$ is a defining function at $p$ . With the Wirtinger derivatives $\partial/\partial z_\ell = \tfrac12(\partial/\partial x_\ell - i\,\partial/\partial y_\ell)$ and $\partial/\partial \bar z_\ell = \tfrac12(\partial/\partial x_\ell + i\,\partial/\partial y_\ell)$ , the holomorphic tangent space is

T^{(1,0)}_p \partial U = \Big\{ a \in \mathbb{C}^n : \sum_{k} a_k \tfrac{\partial r}{\partial z_k}(p) = 0 \Big\},

and the Levi form is the Hermitian form

\mathcal{L}(X_p, X_p) = \sum_{k,\ell=1}^n \bar a_k a_\ell \,\frac{\partial^2 r}{\partial \bar z_k \partial z_\ell}(p), \qquad X_p = \sum_k a_k \frac{\partial}{\partial z_k}\Big|_p \in T^{(1,0)}_p\partial U.

$U$ is pseudoconvex at $p$ if $\mathcal{L} \ge 0$ there, and strongly pseudoconvex if $\mathcal{L} > 0$ on nonzero vectors. The inertia of $\mathcal{L}$ is its number of positive and negative eigenvalues, the largest dimensions of subspaces of $T^{(1,0)}_p\partial U$ on which it is positive or negative definite.

Formalization targets

Goal: the tomato can principle (Theorem 2.3.11)

If $U$ has smooth boundary, $p \in \partial U$ , and $\mathcal{L}(X_p, X_p) < 0$ for some $X_p \in T^{(1,0)}_p\partial U$ , then there is a connected open $W \ni p$ with

\forall f \in \mathcal{O}(U)\ \exists F \in \mathcal{O}(W):\ F = f \text{ on } U \cap W,

and, if $U$ is connected, $U$ is not a domain of holomorphy.

The path to the goal

Theorem 2.1.4 (Hartogs figure). For $0 < a, b < 1$ , every function holomorphic on $H = \{(z,w) \in \mathbb{D}^{m+k} : |z_\ell| > a\ \forall \ell\} \cup \{(z,w) \in \mathbb{D}^{m+k} : |w_\ell| < b\ \forall \ell\}$ extends holomorphically to $\mathbb{D}^{m+k}$ .
Corollary 2.1.5. For $n \ge 2$ , $U$ open and $p \in U$ , every $f \in \mathcal{O}(U \setminus \{p\})$ extends holomorphically to $U$ .
Theorem 2.1.7 (continuity principle). Closed analytic discs $\varphi_k \to \varphi$ uniformly, with $\varphi_k(\overline{\mathbb{D}}) \subset U$ and $\varphi(\partial\mathbb{D}) \subset U$ , give an $s > 0$ such that every $f \in \mathcal{O}(U)$ continues holomorphically to $\Delta_s(p)$ for each $p \in \varphi(\mathbb{D})$ . The continuation agrees with $f$ on a nonempty open subset of $U \cap \Delta_s(p)$ .
Proposition 2.3.6. The inertia of the Levi form does not depend on the defining function.
Theorem 2.3.8. The inertia of the Levi form is invariant under local biholomorphisms that map $U$ to $U'$ near the boundary points.
Lemma 2.3.9. Near any point, after a local biholomorphic change of coordinates, a smooth real hypersurface has the form $\operatorname{Im} w = \sum_{k \le \alpha}|z_k|^2 - \sum_{\alpha < k \le \alpha+\beta}|z_k|^2 + E$ with $E$ vanishing to order three. For a boundary, $\alpha$ and $\beta$ are the Levi inertia and $U$ is the side $>$ .

Significance

The tomato can principle is the necessity half of the solution of the Levi problem: pseudoconvexity is a local, computable condition on the boundary that every domain of holomorphy with smooth boundary satisfies. Together with its converse, it lets one decide whether a smooth domain is a domain of holomorphy by computing second derivatives of a defining function. The Hartogs figure and the continuity principle are the standard ways to extend holomorphic functions, and later chapters use them for the Hartogs phenomenon and for Hartogs pseudoconvexity. The invariance results make the Levi form's inertia a biholomorphic invariant of a boundary point. The normal form is the usual starting point for local computations in CR geometry.

All results are classical and proved in the source, except Proposition 2.3.6, which the book leaves as an exercise. None of them is formalized in Mathlib or on the platform: Mathlib has holomorphic functions of several variables, but no Hartogs extension, no Levi form and no pseudoconvexity. The platform's ray_hartogs is Hartogs's theorem on separate analyticity, a different result. The mission produces faithful statements of this chain, together with definitions of smooth boundaries, holomorphic tangent vectors and the Levi form that later missions of the series need.

Difficulty

The goal combines three independent pieces of machinery. The Hartogs figure needs holomorphy of Cauchy integrals over a torus with a holomorphic parameter, and the identity theorem on a polydisc. Reducing to the normal form needs the implicit function theorem for real hypersurfaces, second-order Taylor expansion in Wirtinger coordinates, a polynomial holomorphic change of coordinates, and Sylvester's law of inertia. The inertia results need the chain rule for Wirtinger derivatives of $r \circ f$ , and the fact that two defining functions differ by a positive smooth factor. That last fact is itself a division lemma for smooth functions vanishing on a hypersurface.

The naive formalization of "the Levi form has a negative eigenvalue" as a negative eigenvalue of the complex Hessian on all of $\mathbb{C}^n$ is wrong. The complex Hessian changes under the choice of defining function, and only its restriction to $T^{(1,0)}_p\partial U$ has invariant signs.

Formalization scope

$\mathbb{C}^n$ is Fin n → ℂ. Its Mathlib norm is the sup norm, so Metric.ball p s is exactly the polydisc $\Delta_s(p)$ . No Euclidean ball occurs in these statements. Holomorphic on an open set is DifferentiableOn ℂ, which is equivalent there to the book's Definition 1.1.2. Functions are ambient maps whose values off the relevant set are irrelevant.

Smooth means ContDiffOn ℝ ∞ on the open neighbourhood $V$ . Real partial derivatives are fderiv ℝ in the directions $e_\ell$ and $i e_\ell$ , and Wirtinger derivatives are built from them. $T^{(1,0)}_p\partial U$ is the submodule holTangent r p of coefficient vectors, computed from the defining function in use. The Levi form is compared through its real part. The inertia is the pair leviPosIndex, leviNegIndex: suprema over ℕ of dimensions of definite subspaces, nonempty (the zero subspace) and bounded by $n$ . The book's $O(3)$ is VanishesToOrder 3: the function and its derivatives of order at most two vanish at the point. It is not Mathlib's IsBigO.

Conventions and restrictions:

The goal assumes the negative Levi value for one defining function, the weakest form of the hypothesis. "Extends to a neighbourhood of $p$ " is read literally: $F = f$ on the whole overlap $U \cap W$ , with $W$ fixed before $f$ is chosen. Agreement on a mere nonempty open subset of $U \cap W$ would be a weaker statement and is not what is asked. The second conjunct adds connectedness of $U$ , because Definition 2.1.1 applies only to domains.
In Theorem 2.1.7, "some open subset" is read as a nonempty open subset. The empty set would make the conclusion vacuous.
Lemma 2.3.9 is stated in $\mathbb{C}^{m+1}$ , with $z$ the first $m$ coordinates and $w$ the last one. Nothing is lost, because $\mathbb{C}^0$ contains no hypersurface.
In Definition 2.2.1, " $r > 0$ for points not in $U$ " is read as "not in $\overline{U}$ ", since $r = 0$ on $\partial U$ .

A trivializing formalization is excluded: the Levi form is restricted to holTangent r p, never the full complex Hessian, and the defining function must carry the sign condition. So neither a hypothesis that fails for every open set nor one that holds for every open set can make the goal vacuous or trivial.

A complete development needs parameter-dependent Cauchy integrals on polydiscs, a real implicit function theorem for hypersurfaces, a smooth division lemma, a Wirtinger chain rule, and Sylvester's law of inertia for Hermitian forms restricted to subspaces. These pieces are reusable across the series, and contributions of any of them are welcome.

Selected references

J. Lebl, Tasty Bits of Several Complex Variables, version 4.4, 2026. https://www.jirka.org/scv/scv.pdf
L. Hörmander, An Introduction to Complex Analysis in Several Variables, 3rd ed., North-Holland, 1990.
S. G. Krantz, Function Theory of Several Complex Variables, 2nd ed., AMS Chelsea, 2001.
S. Ivashkovich, Discrete and continuous versions of the continuity principle, J. Geom. Anal. 32 (2022), Paper No. 226.

22 thms1 active userReviewed

Analysis Functional Analysis Partial Differential Equations·Captain: mikedeng1

Notes on Partial Differential Equations XII: Friedrichs Symmetric Systems — Weak Equals StrongTextbook

Motivation

Many systems of first-order partial differential equations arising in physics — linear acoustics, Maxwell's equations, linearized gas dynamics, the Tricomi equation of transonic flow — can be written as symmetric systems $A^i\partial_i u + Cu = f$ with symmetric coefficient matrices $A^i$ . K. O. Friedrichs showed in 1958 (Friedrichs 1958) that a single energy argument gives existence and uniqueness for boundary value problems of this form under positivity conditions on the equation and the boundary condition, regardless of whether the system is elliptic, hyperbolic or of mixed type. The theory is the subject of Chapter 8 of J. K. Hunter's Notes on Partial Differential Equations (UC Davis, revised 6/18/2014), which this mission follows.

The core analytic tool of the theory is older. In 1944 Friedrichs introduced mollifiers precisely to prove that weak and strong extensions of differential operators coincide (Friedrichs 1944); the key estimate is a bound on the commutator of a mollifier with a first-order operator with Lipschitz coefficients. Lax and Phillips (1960) developed the boundary version for dissipative symmetric operators.

Setting

Write points of $\mathbb{R}^n$ as $x = (x_1, \dots, x_n)$ and give $\mathbb{R}^m$ its Euclidean norm $|w|$ . Let $A^1, \dots, A^n, C : \mathbb{R}^n \to \mathbb{R}^{m\times m}$ be matrix-valued coefficients. The first-order operator and its formal adjoint are (summation over $i$ )

Lu = A^i\partial_i u + Cu, \qquad L^*v = -A^i\partial_i v + C^Tv - (\partial_i A^i)v .

A mollifier profile is a $C^\infty$ , compactly supported, non-negative, radially symmetric $\eta : \mathbb{R}^n \to \mathbb{R}$ with $\int \eta = 1$ . For $\varepsilon > 0$ set $\eta_\varepsilon(x) = \varepsilon^{-n}\eta(x/\varepsilon)$ and define the smoothing operator $J_\varepsilon u = \eta_\varepsilon * u$ . The commutator $[J_\varepsilon, L]u = J_\varepsilon(Lu) - L(J_\varepsilon u)$ is defined for $u \in C^1_c(\mathbb{R}^n;\mathbb{R}^m)$ .

For the boundary value problem, $\Omega \subseteq \mathbb{R}^n$ is a bounded open set with $C^2$ -boundary, $\nu$ its outward unit normal, and the problem is

A^i\partial_iu + Cu = f \ \text{ in } \Omega, \qquad B_-u = 0 \ \text{ on } \partial\Omega,

with boundary matrix $B = \nu_iA^i$ . The system is positive symmetric with constant $c > 0$ if the $A^i$ are symmetric and $C + C^T - \partial_iA^i \ge 2cI$ in $\Omega$ . The boundary condition is maximally positive if $B$ is nonsingular on $\partial\Omega$ and there is a matrix function $M$ on $\partial\Omega$ with $B_\pm = \tfrac12(B \pm M)$ , $M + M^T \ge 0$ and $\mathbb{R}^m = \ker B_+ \oplus \ker B_-$ . A weak solution with data $f \in L^2(\Omega;\mathbb{R}^m)$ is $u \in L^2(\Omega;\mathbb{R}^m)$ with $\int_\Omega u^TL^*v = \int_\Omega f^Tv$ for every $v \in D^* = \{v \in C^1(\overline\Omega) : B_+^Tv = 0 \text{ on } \partial\Omega\}$ .

Formalization targets

Goal: Friedrichs' commutator lemma (Lemma 8.11)

Let $A^i \in C^1_c(\mathbb{R}^n;\mathbb{R}^{m\times m})$ and $C \in C_c(\mathbb{R}^n;\mathbb{R}^{m\times m})$ . For each $\varepsilon > 0$ the commutator $[J_\varepsilon, L] : C^1_c \to L^2$ extends to a bounded operator $\overline{[J_\varepsilon, L]}$ on $L^2(\mathbb{R}^n;\mathbb{R}^m)$ , and

\sup_{\varepsilon > 0}\big\|\overline{[J_\varepsilon, L]}\big\|_{L^2\to L^2} < \infty, \qquad \overline{[J_\varepsilon, L]}\,u \to 0 \ \text{ in } L^2 \text{ as } \varepsilon \to 0^+ \ \text{ for every } u \in L^2 .

The goal asserts only the shape: a uniform bound exists, with no value fixed.

Milestones: energy estimates and existence (Theorems 8.6, 8.9, Corollary 8.7)

Under the smoothness, positivity and maximal positivity conditions above, with $\|\cdot\|$ the $L^2(\Omega)$ norm,

c\|u\| \le \|Lu\| \ \ (u \in C^1(\overline\Omega),\ B_-u = 0), \qquad c\|v\| \le \|L^*v\| \ \ (v \in C^1(\overline\Omega),\ B_+^Tv = 0);

smooth solutions are unique; and for every $f \in L^2(\Omega)$ a weak solution exists.

Significance

The commutator lemma is what turns weak solutions into strong ones: mollifying a weak solution produces smooth functions that solve the equation up to an error $[J_\varepsilon, L]u$ , and the lemma says this error vanishes in the limit. Friedrichs' "weak equals strong" theorem (Theorem 8.12 of the notes), the uniqueness of weak solutions (Corollary 8.13), and much of the $L^2$ theory of hyperbolic systems and pseudo-differential commutator estimates rest on it. The energy estimates of Theorem 8.6 and the existence theorem 8.9 are the two halves of the Friedrichs theory that do not need mollification: an a priori bound for smooth functions satisfying the boundary condition, and existence by duality.

All of these results are classical and proved. As far as a search of the platform and of Mathlib shows, none is formalized: Mathlib has convolution, ContDiffBump mollifiers and $L^p$ spaces, but no commutator estimates, no divergence theorem on $C^2$ domains, and no Friedrichs systems. The mission would produce the first machine-checked commutator estimate for mollifiers and first-order operators with Lipschitz coefficients, and the first formal treatment of positive symmetric boundary value problems.

Difficulty

The obvious argument for the goal — bound $J_\varepsilon(A^i\partial_iu)$ and $A^i\partial_i(J_\varepsilon u)$ separately — fails: each term involves $\partial_i u$ , which is not controlled by $\|u\|_{L^2}$ , and each is of size $\varepsilon^{-1}\|u\|$ after moving the derivative onto $\eta_\varepsilon$ . Only the difference is bounded, and only because the coefficient difference $A^i(y) - A^i(x)$ is of size $|x - y| \lesssim \varepsilon$ on the support of $\eta_\varepsilon(x - y)$ . The cancellation between the two terms is the whole content of the uniform bound. Convergence to zero on smooth compactly supported $u$ is easy, but it does not by itself give convergence on all of $L^2$ .

For the milestones, the central difficulty is Green's theorem: the energy identity requires the divergence theorem on a bounded $C^2$ domain for $C^1$ vector fields, with the outward normal and surface measure, none of which Mathlib provides for general domains.

Formalization scope

$\mathbb{R}^n$ and $\mathbb{R}^m$ are EuclideanSpace ℝ (Fin n) and EuclideanSpace ℝ (Fin m), so $|\cdot|$ is Euclidean and $L^2(\mathbb{R}^n;\mathbb{R}^m)$ is Lp (EuclideanSpace ℝ (Fin m)) 2 volume. Coordinates are 0-based: A i is $A^{i+1}$ .
The goal takes a family T : ℝ → (L² →L[ℝ] L²). "Extends" means: for $\varepsilon > 0$ and every $u \in C^1_c$ , T ε applied to the class of $u$ agrees a.e. with the pointwise commutator. Because $C^1_c$ is dense in $L^2$ , this pins down each T ε; a bound stated on $C^1_c$ only would be weaker than the lemma and is not what is asked.
The lemma is stated for every mollifier profile, which includes the bump (1.5) of the notes. $C^\infty$ means ContDiff ℝ ∞ (smooth, not analytic).
A bounded open set with $C^2$ -boundary is one with a global $C^2$ defining function $\rho$ ( $\Omega = \{\rho < 0\}$ , $\nabla\rho \ne 0$ on $\{\rho = 0\}$ ); for bounded sets this is equivalent to the chart definition of the notes. The outward normal is $\nabla\rho/|\nabla\rho|$ , which does not depend on $\rho$ . It is not a free function argument.
$C^1(\overline\Omega)$ is modelled by $C^1$ functions on $\mathbb{R}^n$ . For $C^2$ domains their restrictions are exactly $C^1(\overline\Omega)$ .
The printed Definition 8.5 sets $B_\pm = B \pm M$ and also $B = B_+ + B_-$ , which would force $B = 0$ . The formalization uses $B_\pm = \tfrac12(B \pm M)$ , Friedrichs' normalisation. This gives the same kernels $\ker B_\pm$ , so the same boundary conditions.
$L^2$ norms are eLpNorm · 2 in $[0,\infty]$ , so no integrability condition is hidden in the estimates.

Needed infrastructure: Young's convolution inequality on $\mathbb{R}^n$ , density of $C^1_c$ in $L^2$ , differentiation under the convolution integral, and, for the milestones, the divergence theorem on bounded $C^2$ domains together with the Riesz representation theorem. The divergence theorem on $C^2$ domains, and the commutator estimate itself, are reusable well beyond this mission. Contributions of any of these are welcome.

Selected references

J. K. Hunter, Notes on Partial Differential Equations, UC Davis lecture notes, revised 6/18/2014, Chapter 8. https://www.math.ucdavis.edu/~hunter/pdes/pde_notes.pdf
K. O. Friedrichs, The identity of weak and strong extensions of differential operators, Trans. Amer. Math. Soc. 55 (1944), 132–151. https://doi.org/10.1090/S0002-9947-1944-0009701-0
K. O. Friedrichs, Symmetric positive linear differential equations, Comm. Pure Appl. Math. 11 (1958), 333–418. https://doi.org/10.1002/cpa.3160110306
P. D. Lax and R. S. Phillips, Local boundary conditions for dissipative symmetric linear differential operators, Comm. Pure Appl. Math. 13 (1960), 427–455. https://doi.org/10.1002/cpa.3160130307

8 thms1 active userReviewed

Analysis Functional Analysis Partial Differential Equations·Captain: mikedeng1

Notes on Partial Differential Equations XI: Existence and Uniqueness of Weak Solutions of Hyperbolic PDEsTextbook

Motivation

Hyperbolic partial differential equations model waves: acoustic, elastic, electromagnetic and gravitational. Their qualitative behaviour differs sharply from that of parabolic equations. They have finite speed of propagation, they are reversible in time, and they do not smooth their data: a singularity in the initial state is transported, not damped. The analytical consequence is that energy estimates for hyperbolic equations are weaker than for parabolic ones, and the existence theory has to be run in spaces that carry exactly one derivative's worth of information.

This mission formalizes the energy-space well-posedness theory for linear second-order hyperbolic equations with time-dependent coefficients, following Chapter 7 of J. K. Hunter's lecture notes Notes on Partial Differential Equations (UC Davis, revised 6/18/2014). The same theory appears in L. C. Evans, Partial Differential Equations, §7.2, and goes back to the Galerkin and energy methods of J.-L. Lions and E. Magenes.

Setting

Let $\Omega \subset \mathbb{R}^n$ be a bounded open set and $T > 0$ . A test function is a smooth function with compact support in $\Omega$ ; the Sobolev space $H^1_0(\Omega)$ is the closure of the test functions in the norm $\|u\|_{H^1_0} = \big(\int_\Omega (u^2 + |Du|^2)\,dx\big)^{1/2}$ , where $Du$ is the weak gradient. $L^2(\Omega)$ carries the inner product $(u,v)_{L^2} = \int_\Omega uv\,dx$ , and $H^{-1}(\Omega) = H^1_0(\Omega)'$ is the dual space with pairing $\langle f, v \rangle$ . There are embeddings $H^1_0(\Omega) \hookrightarrow L^2(\Omega) \hookrightarrow H^{-1}(\Omega)$ .

The operator is

Lu = -\sum_{i,j=1}^n \partial_i\big(a^{ij}(x,t)\,\partial_j u\big) + c(x,t)\,u,

with bilinear form $a(u,v;t) = \sum_{i,j}\int_\Omega a^{ij}\partial_i u\,\partial_j v\,dx + \int_\Omega c\,uv\,dx$ on $H^1_0(\Omega)$ , and $a_t$ is the same form built from the time derivatives $a^{ij}_t$ , $c_t$ . Assumption 7.1 requires $a^{ij}, c, a^{ij}_t, c_t \in L^\infty(\Omega\times(0,T))$ , $a^{ij} = a^{ji}$ , and uniform ellipticity: $\sum_{i,j} a^{ij}\xi_i\xi_j \ge \theta|\xi|^2$ for some $\theta > 0$ .

A vector-valued function $u : (0,T) \to X$ has weak time derivative $w$ if $\int_0^T \varphi'(t)u(t)\,dt = -\int_0^T \varphi(t)w(t)\,dt$ for all test functions $\varphi$ on $(0,T)$ , the integrals being Bochner integrals. The problem is

u_{tt} + Lu = f \text{ in } \Omega\times(0,T), \qquad u = 0 \text{ on } \partial\Omega\times(0,T), \qquad u = g,\ u_t = h \text{ at } t = 0. \qquad (7.5)

A weak solution (Definition 7.2) is a function $u : [0,T] \to H^1_0(\Omega)$ with weak derivatives $u_t$ , $u_{tt}$ such that $u \in C([0,T];H^1_0)$ , $u_t \in C([0,T];L^2)$ , $u_{tt} \in L^2(0,T;H^{-1})$ , and for every $v \in H^1_0(\Omega)$

\langle u_{tt}(t), v\rangle + a(u(t), v; t) = (f(t), v)_{L^2} \quad \text{for a.e. } t,

with $u(0) = g$ and $u_t(0) = h$ .

Formalization targets

Goal: Theorem 7.3

Under Assumption 7.1 there is a constant $C$ , depending only on $\Omega$ , $T$ and the coefficients, such that for every $f \in L^2(0,T;L^2(\Omega))$ , $g \in H^1_0(\Omega)$ , $h \in L^2(\Omega)$ there is a unique weak solution, and

\|u\|_{L^\infty(0,T;H^1_0)} + \|u_t\|_{L^\infty(0,T;L^2)} + \|u_{tt}\|_{L^2(0,T;H^{-1})} \le C\big(\|f\|_{L^2(0,T;L^2)} + \|g\|_{H^1_0} + \|h\|_{L^2}\big).

Milestones

Proposition 7.5. For every $N$ , the Galerkin problem projected onto the span $E_N$ of the first $N$ Dirichlet eigenfunctions has a unique approximate solution $u_N \in C^1([0,T];E_N)$ with $u_{Ntt} \in L^2(0,T;E_N)$ .
Proposition 7.6. The approximate solutions satisfy the energy estimate of Theorem 7.3 with a constant independent of $N$ .
Lemma 7.8. If $\mathcal{V} \hookrightarrow \mathcal{H}$ is a dense continuous embedding of Hilbert spaces, $u \in L^\infty(0,T;\mathcal{V})$ and $u_t \in L^2(0,T;\mathcal{H})$ , then $u$ is weakly continuous into $\mathcal{V}$ .
Lemma 7.10. If $u \in L^2(0,T;H^1_0)$ , $u_t \in L^2(0,T;L^2)$ , $u_{tt} \in L^2(0,T;H^{-1})$ and $u_{tt} + Lu \in L^2(0,T;L^2)$ , then

\tfrac12 \tfrac{d}{dt}\big(\|u_t\|^2_{L^2} + a(u,u;t)\big) = (u_{tt}+Lu, u_t)_{L^2} + \tfrac12 a_t(u,u;t),

and the energy is absolutely continuous.

Proposition 7.12. Weak solutions in the sense of Definition 7.2 are unique.

Significance

Theorem 7.3 is the basic well-posedness result for linear wave equations in inhomogeneous, time-dependent media in the natural energy space. It is the starting point for the regularity theory of such solutions, for finite-speed-of-propagation arguments in a weak setting, and for fixed-point constructions for semilinear wave equations, which linearize around a known solution and need exactly this estimate with a constant depending only on the coefficients. Lemma 7.8 and Lemma 7.10 are general tools that recur in evolution equations: the first converts uniform-in-time bounds into weak continuity, the second justifies an energy identity for solutions too rough to differentiate directly.

The results are classical and fully proved in the literature, and to our knowledge no machine-checked version exists. Formalizing them requires vector-valued Sobolev spaces in time, Bochner-integral weak derivatives and duality arguments. These are largely absent from Mathlib and would be reused by any formal treatment of evolution equations, parabolic ones included.

Difficulty

The obvious approach, testing the equation with $u_t$ to obtain energy conservation, is not available for weak solutions: $u_t(t)$ lies only in $L^2(\Omega)$ , not in $H^1_0(\Omega)$ , so the pairing $a(u, u_t; t)$ is undefined. This affects both halves of the theorem. For existence, the energy estimate holds only for the finite-dimensional approximations, and the limit is obtained in weak-star topologies of $L^\infty$ in time, which give neither continuity in time nor the initial conditions directly. For uniqueness, a different test function is needed. The continuity requirements of Definition 7.2 are an essential part of the statement, not a technicality, and establishing them for the constructed solution is a large part of the work.

Formalization scope

$\mathbb{R}^n$ is EuclideanSpace ℝ (Fin n) with Lebesgue measure; coordinates are 0-based. $H^1_0(\Omega)$ is modelled by jets $(u, Du)$ : the closure of $\{(\varphi, \nabla\varphi)\}$ in $L^2(\Omega;\mathbb{R}\times\mathbb{R}^n)$ , with norm exactly $\big(\int_\Omega u^2 + |Du|^2\big)^{1/2}$ . $H^{-1}(\Omega)$ is StrongDual ℝ (H10 n Ω), and $f \in L^2$ acts by $v \mapsto (f, v)_{L^2}$ .
Time-dependent objects are functions on $\mathbb{R}$ . Only values on $(0,T)$ (integrability, weak derivatives) or $[0,T]$ (continuity, initial values) matter. $u_t$ is the weak derivative of $u$ regarded in $L^2$ , and $u_{tt}$ that of $u_t$ regarded in $H^{-1}$ . Local integrability is built into the weak derivative, so no Bochner integral takes the junk value $0$ .
Coefficients are functions of $(x,t)$ , bundled with their time derivatives. Assumption 7.1 requires those to be weak time derivatives on $\Omega\times(0,T)$ . Symmetry and ellipticity hold almost everywhere there, the meaning for $L^\infty$ coefficients. The consequences (7.7) of Assumption 7.1 are not assumed.
Norms in the estimates are ℝ≥0∞-valued (eLpNorm, ‖·‖ₑ), and the constants are finite (ℝ≥0). Each constant is quantified before the data $f, g, h$ ; in Proposition 7.6 it also precedes the eigenbasis and $N$ .
The Galerkin basis is any $L^2$ -orthonormal basis of weak Dirichlet eigenfunctions, indexed from $0$ .
Two misprints are corrected. The first integral of (7.6) has $\partial_j v$ , not $\partial_j u$ . The energy (7.16) is $\|u_t\|^2_{L^2} + a(u,u;t)$ , with the square that (7.19) uses.
Lemma 7.10 is stated in integrated form. The right-hand side of (7.19) is integrable, and the energy equals a constant plus its integral for a.e. $t$ . This is the identity together with absolute continuity.
A trivializing formalization is excluded. Definition 7.2 keeps all three regularity classes and both initial conditions, and uniqueness and the estimate are asserted for the object of that definition. A definition without the continuity classes would admit non-solutions.

A complete development needs Bochner-valued Sobolev spaces on an interval, Banach–Alaoglu in $L^\infty(0,T;X) = L^1(0,T;X')'$ , linear ODE systems with $L^\infty$ coefficients, Gronwall's inequality, and the spectral theory of the Dirichlet Laplacian. The time-dependent function-space layer is reusable for parabolic and Schrödinger-type equations. Contributions of general lemmas on vector-valued weak derivatives are welcome.

Selected references

J. K. Hunter, Notes on Partial Differential Equations, UC Davis lecture notes, revised 6/18/2014, Chapter 7. https://www.math.ucdavis.edu/~hunter/pdes/pde_notes.pdf
L. C. Evans, Partial Differential Equations, 2nd ed., Graduate Studies in Mathematics 19, AMS, 2010, §7.2. https://doi.org/10.1090/gsm/019
J.-L. Lions and E. Magenes, Non-Homogeneous Boundary Value Problems and Applications, Vol. I, Springer, 1972, Chapter 3. https://doi.org/10.1007/978-3-642-65161-8

10 thms1 active userReviewed

Analysis Harmonic Analysis Partial Differential Equations·Captain: mikedeng1

Notes on Partial Differential Equations IX: Local Existence for a Semilinear Heat Equation and the Nonlinear Schrödinger EquationTextbook

Motivation

Reaction–diffusion equations $u_t = \Delta u + f(u)$ are the standard model for the interplay of diffusion with local growth or decay: chemical kinetics, population dynamics, and the bifurcation of equilibria of partial differential equations. The special case

u_t = \Delta u + \lambda u - \gamma u^m

(the Chafee–Infante equation on bounded domains, Chafee and Infante 1974) is the model equation for loss of stability: $u = 0$ is linearly stable for $\lambda < 0$ and unstable for $\lambda > 0$ , and for $m = 3$ , $\gamma > 0$ the reaction term produces a supercritical pitchfork bifurcation. Before any of that dynamics can be studied, one needs solutions to exist. §5.5 of J. K. Hunter's Notes on Partial Differential Equations (UC Davis, revised 6/18/2014) proves local existence by rewriting the equation as an integral equation and applying the contraction mapping theorem. This argument, the "mild solution" method of Kato and Segal, is the template for local well-posedness of semilinear parabolic and dispersive equations (Pazy 1983, Henry 1981).

Setting

Write $\mathbb{R}^n$ for Euclidean space with Lebesgue measure. For $f \in L^2(\mathbb{R}^n)$ the Fourier transform is $\hat f(k) = (2\pi)^{-n}\int f(x)e^{-ik\cdot x}\,dx$ , defined by this formula on Schwartz functions and extended to $L^2$ by Plancherel's theorem. For $s \ge 0$ , the Sobolev space $H^s(\mathbb{R}^n)$ consists of the $f \in L^2$ with finite norm

\|f\|_{H^s} = \Big((2\pi)^n \int_{\mathbb{R}^n} (1+|k|^2)^{s}\,|\hat f(k)|^2\,dk\Big)^{1/2}.

The heat semigroup $e^{-tA}$ , $A = -\Delta$ , is the Fourier multiplier $\widehat{e^{-tA}h}(k) = e^{-t|k|^2}\hat h(k)$ . For $t > 0$ it is convolution with the heat kernel $\Gamma_t(x) = (4\pi t)^{-n/2}e^{-|x|^2/4t}$ .

Fix $\lambda, \gamma \in \mathbb{R}$ and an integer $m \ge 1$ , and let $F(h) = \lambda h - \gamma h^m$ act pointwise on functions. The initial value problem is

u_t = \Delta u + \lambda u - \gamma u^m, \qquad u(x,0) = g(x). \tag{5.34}

Write $C([0,T];H^s)$ for the curves $t \mapsto u(t) \in H^s$ that are continuous on $[0,T]$ in the $H^s$ norm, normed by $\sup_{0\le t\le T}\|u(t)\|_{H^s}$ . A mild solution on $[0,T]$ with values in $H^{2\alpha}$ is a curve $u \in C([0,T];H^{2\alpha})$ satisfying the Duhamel formula

u(t) = e^{-tA}g + \int_0^t e^{-(t-s)A}F(u(s))\,ds \qquad (0 \le t \le T).

The right-hand side, viewed as a function of $u$ , is the map $\Phi(u)$ .

Formalization targets

Goal: local existence and uniqueness (Theorem 5.49)

Let $1 \le n \le 3$ and $n/4 < \alpha < 1$ . For every $R > 0$ there is $T > 0$ , depending only on $\alpha, n, R, \lambda, \gamma, m$ , such that for every $g$ with $\|g\|_{H^{2\alpha}} \le R$ , (5.34) has a mild solution $u \in C([0,T];H^{2\alpha})$ , and any two mild solutions on $[0,T]$ coincide.

Milestones

Smoothing (Lemma 5.50). For $\alpha > 0$ there is $C = C(\alpha,n)$ with

\|e^{-tA}h\|_{H^{2\alpha}} \le \frac{Ce^t}{t^\alpha}\|h\|_{L^2} \qquad (t > 0,\ h \in L^2).

Fractional Sobolev embedding (Theorem 5.79). If $0 < s < n/2$ and $1/q = 1/2 - s/n$ , then $\|f\|_{L^q} \le C\|f\|_{H^s}$ . If $s > n/2$ , then every $f \in H^s$ is a.e. equal to a continuous function vanishing at infinity, and $\|f\|_{L^\infty} \le C\|f\|_{H^s}$ .
Local Lipschitz bound for $\Phi$ (Lemma 5.51). For $n/4 < \alpha < 1$ , $\Phi$ maps $C([0,T];H^{2\alpha})$ to itself, and for $0 < T \le T_0$

\|\Phi(u)-\Phi(v)\| \le C T^{1-\alpha}\big(1 + \|u\|^{m-1} + \|v\|^{m-1}\big)\|u - v\|,

where all norms are in $C([0,T];H^{2\alpha})$ and $C$ depends on $\alpha, m, n, \lambda, \gamma, T_0$ .

Significance

The theorem is the base case of the semigroup approach to nonlinear evolution equations. The existence time depends only on the size of the data, so an a priori bound on $\|u(t)\|_{H^{2\alpha}}$ upgrades local existence to global existence. The same scheme, with $X = \mathcal D(A^\alpha)$ for a sectorial operator $A$ , covers general semilinear parabolic problems. The smoothing estimate and the fractional Sobolev embedding are also used separately, in parabolic regularity theory and in the analysis of dispersive equations.

The results are classical and proved in the notes. None of them has a machine-checked proof on this platform. Mathlib has the $L^2$ Fourier transform and Plancherel's theorem, tempered distributions, and a Bessel-potential definition of Sobolev spaces, but no fractional Sobolev embedding on $\mathbb{R}^n$ and no mild-solution theory for semilinear heat equations. The mission asks for complete formal proofs of the three milestones and the goal, stated for the concrete objects above.

Difficulty

The obvious fixed-point argument needs three separate analytic inputs. The first is that the $L^2 \to H^{2\alpha}$ operator norm of $e^{-tA}$ blows up like $t^{-\alpha}$ , which is integrable only because $\alpha < 1$ . The second is that $F$ is locally Lipschitz from $H^{2\alpha}$ to $L^2$ , which needs the embedding $H^{2\alpha} \hookrightarrow L^\infty$ and fails for $\alpha \le n/4$ . The third is that the Duhamel integral defines a continuous $H^{2\alpha}$ -valued curve even though its integrand is singular at $s = t$ . With these in hand, the contraction must be run on a ball whose radius is fixed by the data, with $T$ chosen uniformly over that ball. Uniqueness is claimed in all of $C([0,T];H^{2\alpha})$ , not only in the ball where the contraction runs, so an extra argument is needed to exclude solutions that leave the ball.

Formalization scope

$\mathbb{R}^n$ is EuclideanSpace ℝ (Fin n) with volume. The solution and the data are real-valued. Theorem 5.79 and Lemma 5.50 are stated for complex-valued functions. A curve is a map ℝ → (ℝⁿ → ℝ), and only its values on $[0,T]$ matter.
Fourier normalization. The book's $\hat f(k) = (2\pi)^{-n}\int f e^{-ik\cdot x}$ is obtained from Mathlib's $L^2$ transform Lp.fourierTransformₗᵢ (kernel $e^{-2\pi i\langle x,\xi\rangle}$ , no prefactor) as $\hat f(k) = (2\pi)^{-n}\mathcal F f(k/2\pi)$ . Mathlib's constants are never used for the book's.
$H^s$ norm. hsNorm is valued in $[0,\infty]$ and is $\infty$ off $L^2$ , so $f \in H^s$ means hsNorm n s f < ⊤. The factor $(2\pi)^n$ is inside the square root, as in the book's inner product and in its proof of Lemma 5.50. Definition 5.74 prints it outside, which is inconsistent with both. With this choice $\|f\|_{H^0} = \|f\|_{L^2}$ .
Semigroup. $e^{-tA}$ is convolution with the heat kernel for $t > 0$ , which agrees with the multiplier (5.37) on $L^2$ , and the identity at $t = 0$ . No abstract semigroup theory is used.
Duhamel integral. It is taken pointwise in $x$ , and (5.39) is required for almost every $x$ at each $t \in [0,T]$ . For curves in $C([0,T];H^{2\alpha})$ with $\alpha > n/4$ , the integrand is bounded, so this is the book's $L^2$ -valued integral.
Constants and corrections. The data dependence of $T$ is read as uniform over the ball $\|g\|_{H^{2\alpha}} \le R$ . In Lemma 5.51 the constant, announced as $C(\alpha,m,n)$ , is allowed to depend on $\lambda, \gamma$ and on an upper bound $T_0$ for $T$ . The hypothesis $\alpha < 1$ is added. Both corrections are used by the notes' own proof, and without them the printed inequality fails for large $T$ . Theorem 5.79 prints its inequalities without the constant $C$ it announces, and the constant is restored. Throughout, $m \ge 1$ .
Trivializing readings excluded. The norms are $[0,\infty]$ -valued and $\infty$ off $L^2$ , so no bound holds through a junk value $0$ . A mild solution must satisfy the Duhamel identity and be continuous in $H^{2\alpha}$ , so existence cannot be met by an unconstrained curve. Uniqueness is stated over all mild solutions on $[0,T]$ , not over a ball.
Infrastructure. A complete development needs Plancherel in the book's normalization, the heat-kernel/multiplier identity on $L^2$ , Bochner or pointwise integration of $L^2$ -valued curves, the Banach fixed-point theorem on a closed ball of $C([0,T];H^{2\alpha})$ , and the fractional Sobolev embedding. The embedding and the smoothing estimate can be reused beyond this mission. Contributions of the $H^s$ theory as a normed space are welcome.

Selected references

J. K. Hunter, Notes on Partial Differential Equations, UC Davis lecture notes, revised 6/18/2014, §5.5 and Appendices 5.C–5.D. https://www.math.ucdavis.edu/~hunter/pdes/pde_notes.pdf
N. Chafee and E. F. Infante, A bifurcation problem for a nonlinear partial differential equation of parabolic type, Applicable Analysis 4 (1974), 17–37. https://doi.org/10.1080/00036817408839081
A. Pazy, Semigroups of Linear Operators and Applications to Partial Differential Equations, Springer, 1983. https://doi.org/10.1007/978-1-4612-5561-1
D. Henry, Geometric Theory of Semilinear Parabolic Equations, Lecture Notes in Mathematics 840, Springer, 1981. https://doi.org/10.1007/BFb0089647

7 thms1 active userReviewed

Analysis Control Theory Dynamical Systems·Captain: mikedeng1

Stabilization for a Perturbed Chain of Integrators in Prescribed Time II: Fixed-Time and Prescribed-Time Stability of the Varying-Degree Homogeneous FeedbackResearch Paper

Motivation

Many control tasks come with a deadline: a consensus protocol or a regulation task must reach its target by a time fixed in advance, whatever the initial condition. Prescribed-time stabilization asks for a feedback law that brings every trajectory of a control system to the equilibrium by a user-chosen time $T$ . The basic test case is the chain of integrators $x_1^{(n)}=u$ , the normal form of every single-input feedback-linearizable system.

Two routes to prescribed-time stabilization exist. Time-varying gains that blow up as $t\to T$ (Song, Wang, Holloway and Krstić, Automatica 2017) are fragile under measurement noise. Fixed-time stabilization gives a settling time bounded uniformly over all initial conditions, and a time rescaling then turns the uniform bound into any prescribed $T$ . Chitour, Ushirobira and Bouhemou (SIAM J. Control Optim. 2020) follow the second route with an explicit, continuous feedback. It combines Hong's backstepping homogeneous controller (Systems Control Lett. 2002) with a degree of homogeneity that depends on the state (Harmouche, Laghrouche, Chitour and Hamerlain, Int. J. Control 2017). A continuity device of Lopez-Ramirez, Efimov, Polyakov and Perruquetti (Int. J. Robust Nonlinear Control 2018) makes that degree a continuous function of the state. This mission formalizes the construction and its main results, §4.1–4.2 of the paper.

Setting

Fix $n\ge1$ and write $x=(x_1,\dots,x_n)\in\mathbb R^n$ with the Euclidean norm. Let $J_n$ be the $n$ -th Jordan block ( $J_ne_i=e_{i-1}$ , $e_0=0$ ). The pure chain of integrators (31) is

\dot x=J_nx+u\,e_n .

For $y\in\mathbb R$ and $a>0$ write $\lceil y\rfloor^a=\operatorname{sign}(y)|y|^a$ . Given gains $\ell_1,\dots,\ell_n>0$ and $\kappa\in[-\tfrac1{2n},\tfrac1{2n}]$ , set $r_j=1+(j-1)\kappa$ and $\beta_j=(2+\kappa)/r_{j+1}-1$ . Define $v_0=0$ and

v_j=-\ell_j\Big\lceil\lceil x_j\rfloor^{\beta_{j-1}}-\lceil v_{j-1}\rfloor^{\beta_{j-1}}\Big\rfloor^{\frac{r_j+\kappa}{r_j\beta_{j-1}}} .

The homogeneous feedback is $\omega^H_\kappa(x)=v_n(x)$ (Definition 23). The associated Lyapunov function is

V_\kappa(x)=\sum_{j=1}^n\frac{|x_j|^{\beta_{j-1}+1}-|v_{j-1}|^{\beta_{j-1}+1}}{\beta_{j-1}+1}-\lceil v_{j-1}\rfloor^{\beta_{j-1}}(x_j-v_{j-1}),

and (36) is the decay inequality $\dot V_\kappa\le-CV_\kappa^{1+\alpha(\kappa)}$ , with $\alpha(\kappa)=\kappa/(2+\kappa)$ and one constant $C$ for all $\kappa$ in the range.

For $m\in(0,1)$ and $\kappa_0\in(0,\tfrac1{2n})$ , the state-dependent degree $\kappa(x)$ of (49) equals $\kappa_0$ where $V_0(x)>1+m$ and $-\kappa_0$ where $V_0(x)<1-m$ , and it interpolates linearly in $V_0$ in between. The closed-loop controller is $\omega^H_{\kappa(x)}(x)$ . With $B^\kappa_{<a}=\{V_\kappa<a\}$ , let $r(m,\kappa_0)$ be the largest $r$ with $B^{\kappa_0}_{<r}\subseteq B^0_{<1+m}$ , and $r(m,-\kappa_0)$ the smallest $r$ with $B^{-\kappa_0}_{<r}\supseteq B^0_{<1-m}$ . Set

T^\ast(m,\kappa_0)=\frac1C\Big(\frac{r(m,\kappa_0)^{-\alpha(\kappa_0)}}{\alpha(\kappa_0)}-2\ln(2m)+\frac{r(m,-\kappa_0)^{-\alpha(-\kappa_0)}}{-\alpha(-\kappa_0)}\Big).

Finally $D^{\mathbf r}_\lambda=\operatorname{diag}(\lambda^{n-i+1})$ is the dilation of (5).

A system is globally fixed-time stable with settling time at most $T$ if the origin is an equilibrium, solutions exist from every initial state, it is Lyapunov stable, and every solution vanishes for all $t\ge T$ (Definition 1 with $\Omega=\mathbb R^n$ ).

Formalization targets

Goal: Theorem 30 (p. 1038)

Let the gains and $C>0$ satisfy (36). There are $m\in(0,1)$ and $\kappa_0\in(0,\tfrac1{2n})$ such that, for every $T>0$ and every $\lambda>0$ with

\lambda\ \ge\ T^\ast(m,\kappa_0)/T,

the feedback $u=\omega^H_{\kappa(D^{\mathbf r}_\lambda x)}(D^{\mathbf r}_\lambda x)$ makes (31) globally fixed-time stable with settling time at most $T$ .

Milestones

Proposition 24 (p. 1034): gains exist for which (36) holds uniformly in $\kappa$ , $V_\kappa$ is $C^1$ , positive definite and $\mathbf r(\kappa)$ -homogeneous of degree $2+\kappa$ , and $\omega^H_\kappa$ is globally asymptotically stabilizing.
Lemma 31 (p. 1038): on the shell $B^\kappa_{1-m,1+m}$ , $|x_j|$ and $|v_j|$ are bounded uniformly in $\kappa$ .
Lemma 32 (p. 1039): on that shell, $|\omega^H_\kappa-\omega^H_0|$ and $|V_\kappa-V_0|$ are at most a constant times $|\kappa|^{\min(1,r_n)}$ .
Proposition 33 (p. 1040): for every $m$ there is $\kappa_0(m)>0$ below which the closed loop is fixed-time stable, with an explicit settling-time bound that coincides with (52) for $m\le(\sqrt{17}-3)/4$ .
Theorem 28 (pp. 1036–1037): with an input gain $b(t)\in[\underline b,\bar b]$ and the feedback $\omega^H_{\kappa(x)}(x)/\underline b$ , the closed loop is globally fixed-time stable with settling time at most $T^\ast(m,\kappa_0)$ .

Significance

The result gives a static, continuous state feedback for the chain of integrators with an explicit settling-time bound. It is robust to a bounded uncertain input gain, and the rescaled controller meets any prescribed deadline. Unlike time-varying designs, the gains stay bounded, which is what the paper's ISS analysis in §4.3 builds on. The constants in (52) are explicit in terms of $C$ and the radii $r(m,\pm\kappa_0)$ , so the rescaling factor $\lambda$ is computable.

The results are proved on paper; no machine-checked proof is known. A formalization would check the parameter bookkeeping of the construction: index shifts, exponents, the three-phase settling-time estimate, and the interplay of two different dilations. It would also produce reusable definitions of Carathéodory solutions and of finite-, fixed- and prescribed-time stability, which the platform does not yet have.

Difficulty

The obvious argument uses the Lyapunov function $V_{\kappa(x)}$ for the varying-degree controller. That fails: $\kappa$ depends on $x$ , so $V_{\kappa(x)}(x)$ acquires a term from the derivative of $\kappa$ . The proof instead handles three regions separately, with $V_{\kappa_0}$ outside $B^0_{1+m}$ , $V_0$ on the shell $B^0_{1-m,1+m}$ , and $V_{-\kappa_0}$ inside $B^0_{1-m}$ . On the shell the controller is a perturbation of the linear one, and bounding that perturbation needs uniform Hölder estimates in $\kappa$ (Lemmas 31–32). The closed loop is only continuous, so solutions need not be unique and every stability claim is about all solutions. Proposition 24 itself is a recursive gain construction whose constants must be uniform in $\kappa$ .

Formalization scope

States are EuclideanSpace ℝ (Fin n); the paper's index $j\in\{1,\dots,n\}$ is j.val + 1. Solutions are Carathéodory solutions on $[0,\infty)$ in integral form, with integrability stated. Every stability property quantifies over all solutions, and existence of a solution from each initial state is part of Lyapunov stability. $\lceil y\rfloor^a$ is read as $\operatorname{sign}(y)|y|^a$ ; the paper never defines it. $\dot V$ is the Fréchet derivative applied to the vector field. $r(m,\kappa_0)$ and $r(m,-\kappa_0)$ are the supremum and infimum of the admissible radii.

Hypotheses and readings that differ from the page:

The gains and $C$ in Theorems 28 and 30 and Proposition 33 are data satisfying (36), not existentially chosen. An unconstrained $\exists C$ would make (52) false, and Proposition 24 shows (36) is satisfiable.
$b$ is assumed measurable in Theorem 28.
"Adapted" is the feedback divided by $\underline b$ , as the page says.
Corrected printed slips:
- (51) lacks $e_n$ .
- Theorem 30 writes $\kappa_0\in(0,1/n)$ ; Theorem 28's $(0,\tfrac1{2n})$ is used.
- Proposition 33 prints $\kappa_0(m)\in[-\tfrac1{2n},-\tfrac1{2n}]$ ; the value is positive and at most $\tfrac1{2n}$ .
- (37) prints $\beta_{i-1}$ for $\beta_{j-1}$ .
- The proof of Lemma 32 prints the exponent of (33) as $(r_j+1)/(r_j\beta_{j-1})$ ; (33) is used.
Lemma 32's maxima are read pointwise, with $r_n=r_n(\kappa)$ .
In Proposition 33 the middle term $-2\ln(2m)$ of (52) is replaced by $\max(-2\ln(2m),\,2\ln\frac{1+m}{1-m})$ : the page's crossing-time estimate $-2\ln(2m)/C$ is justified only for $m\le(\sqrt{17}-3)/4$ , where the two bounds coincide.
"Explicit" constants are stated as existing.

A formalization in which (36) is dropped, or $C$ is chosen freely, or a trajectory is only required to exist, would be trivial or false. Any trivializing reading of this kind is ruled out: stability is required of every solution, and $C$ is tied to (36).

Needed infrastructure: signed powers and their Hölder estimates (42), differentiability of $V_\kappa$ , weighted homogeneity, Carathéodory existence for continuous right-hand sides, and comparison lemmas for $\dot V\le-cV^{1+\alpha}$ . The stability definitions and the comparison lemmas are reusable beyond this mission. Contributions of any of these are welcome.

Selected references

Y. Chitour, R. Ushirobira, H. Bouhemou, Stabilization for a Perturbed Chain of Integrators in Prescribed Time, SIAM J. Control Optim. 58(2), 1022–1048, 2020. https://doi.org/10.1137/19M1285937
Y. Hong, Finite-time stabilization and stabilizability of a class of controllable systems, Systems Control Lett. 46, 231–236, 2002. https://doi.org/10.1016/S0167-6911(02)00119-6
M. Harmouche, S. Laghrouche, Y. Chitour, M. Hamerlain, Stabilisation of perturbed chains of integrators using Lyapunov-based homogeneous controllers, Int. J. Control 90, 2631–2640, 2017. https://doi.org/10.1080/00207179.2016.1262967
F. Lopez-Ramirez, D. Efimov, A. Polyakov, W. Perruquetti, Fixed-time output stabilization and fixed-time estimation of a chain of integrators, Int. J. Robust Nonlinear Control 28, 4647–4665, 2018. https://doi.org/10.1002/rnc.4275
Y. Song, Y. Wang, J. Holloway, M. Krstić, Time-varying feedback for regulation of normal-form nonlinear systems in prescribed finite time, Automatica 83, 243–251, 2017. https://doi.org/10.1016/j.automatica.2017.06.008
S. P. Bhat, D. S. Bernstein, Geometric homogeneity with applications to finite-time stability, Math. Control Signals Systems 17, 101–127, 2005. https://doi.org/10.1007/s00498-005-0151-x

11 thms1 active userReviewed

Operations Research Probability Stochastic Systems·Captain: mikedeng1

Diffusion approximations for open queueing networks with service interruptions 2: jump-diffusion heavy-traffic limit for long up and down timesResearch Paper

Motivation

Servers in manufacturing lines, communication links and service systems break down, are taken offline for maintenance, or go on vacation. When the interruptions are rare but long, they dominate congestion. A single down period can build a backlog that takes a long time to clear, and in a network that backlog propagates downstream. Standard heavy-traffic diffusion approximations, which describe queue lengths by reflected Brownian motion, do not capture this effect.

Chen and Whitt (Queueing Systems 13, 1993) identify a regime in which the effect survives in the limit. Up times are of order $n$ and down times of order $\sqrt n$ , while the load is within $1/\sqrt n$ of capacity. Under the diffusion scaling each down period then becomes a jump, and the limit of the queue-length process is a reflected jump-diffusion. The paper generalises the single-station result of Kella and Whitt (Adv. Appl. Probab. 22, 1990; reference [22] of the paper) to open networks.

Timeline:

1981: Harrison and Reiman define the multidimensional reflection map on continuous paths (Ann. Probab. 9). Reiman (Math. Oper. Res. 9, 1984) extends it to paths with jumps.
1990: Kella and Whitt prove the one-station jump-diffusion limit for long up and down times.
1991: Chen and Mandelbaum give fluid and diffusion limits of open networks without interruptions (Math. Oper. Res. 16 and Ann. Probab. 19; references [5], [6] of the paper).
1993: Chen and Whitt prove the network case with interruptions (this mission), in Skorohod's $M_1$ topology.

Setting

A network has $J$ single-server stations. Customers arrive from outside station $j$ according to a counting process $A_j$ . Station $j$ completes $S_j(t)$ services in its first $t$ units of busy time. The $l$ th departure from station $k$ is routed to station $j$ when the indicator $\chi_{kj}(l)=1$ , and $R_{kj}(m)=\sum_{l\le m}\chi_{kj}(l)$ counts such departures. Station $j$ alternates up periods $u^j_1,u^j_2,\dots$ and down periods $d^j_1,d^j_2,\dots$ , starting up, and $D_j(t)$ is its cumulative down time in $[0,t]$ . With a work-conserving discipline, the queue length $Z$ and the busy time $B$ satisfy

Z_j(t)=Z_j(0)+A_j(t)+\sum_{k}R_{kj}\big(S_k(B_k(t))\big)-S_j(B_j(t)),\qquad B_j(t)=\int_0^t 1[Z_j(s)>0,\ j\text{ up at }s]\,ds ,

and the idle time is $Y_j(t)=t-D_j(t)-B_j(t)$ .

The reflection map $(\psi,\phi)$ associated with a matrix $Q$ takes a path $x$ to the pair $(y,z)$ with $z=x+(I-Q)y\ge 0$ , $y$ nondecreasing, and $y_j$ increasing only when $z_j=0$ .

A sequence of networks is indexed by $n$ . The arrival, service and routing processes satisfy functional central limit theorems with rates $\lambda^n\to\lambda$ and $\mu^n\to\mu$ at speed $1/\sqrt n$ . Up and down times scale as $(u^{j,n}_k/n,\ d^{j,n}_k/\sqrt n)\Rightarrow(u^j_k,d^j_k)$ . The network is balanced, $\lambda=[I-P^{\mathsf t}]\mu$ , with $P$ the routing matrix. The limit down time $\hat D_j(t)$ is the sum of $d^j_k$ over the up periods completed by time $t$ , which is a pure-jump process.

The $M_1$ topology on paths with jumps compares completed graphs, in which each jump is filled in by the straight segment from $x(t-)$ to $x(t)$ , through their monotone parametrisations.

Formalization targets

Goal: Theorem 4.1, case $J=1$

For a single station with feedback probability $p\in[0,1)$ , with $\hat Z^n(t)=n^{-1/2}Z^n(nt)$ , $\hat B^n(t)=n^{-1/2}[B^n(nt)-nt]$ , $\hat Y^n(t)=n^{-1/2}Y^n(nt)$ and $\hat D^n(t)=n^{-1/2}D^n(nt)$ ,

(\hat Z^n,\hat B^n,\hat Y^n,\hat D^n)\Rightarrow(\hat Z,\hat B,\hat Y,\hat D)\quad\text{in }D((0,\infty),\mathbb R^{4},M_1).

Here $\hat Z=\phi(\hat X)$ , $\hat Y=\mu^{-1}\psi(\hat X)$ and $\hat B=-\hat D-\hat Y$ , with $Q=p$ and

\hat X(t)=\hat Z(0)+\hat\xi(t)+\big(c_\lambda-(1-p)c_\mu\big)t+(1-p)\mu\hat D(t).

The paper states Theorem 4.1 for $J$ stations, with the analogous formulas and $Q=P^{\mathsf t}$ . The mission's goal is its case $J=1$ (see Formalization scope).

Milestones

Lemma 4.1: $\hat D^n\Rightarrow\hat D$ in $D((0,\infty),\mathbb R^J,M_1)$ .
Lemma 4.2: $n^{-1}B^n_j(nt)\to t$ u.o.c.
Eq. (4.24): $n^{-1/2}\xi^n(nt)\to\hat\xi(t)$ u.o.c.
Eqs. (4.28)–(4.29): $\big(n^{-1/2}X^n(nt),\,n^{-1/2}D^n(nt)\big)\to(\hat X,\hat D)$ jointly in $M_1$ .
The almost-sure form of Theorem 4.1 on a Skorohod representation space, case $J=1$ .

Significance

The theorem yields a tractable approximation for networks with rare long interruptions: a reflected Lévy-type process driven by a Brownian part and a compound jump part. Its distribution can be studied through the reflection map. The jump directions $[I-P^{\mathsf t}]\operatorname{diag}(\mu)e_j$ make explicit how an outage at one station drains its downstream stations while its own queue builds up. Remark (4.3) of the paper derives a diffusion analogue of Little's law from the same limit.

The theorem is proved in the paper, and no part of it has been formalized. A formalization would produce the first machine-checked $M_1$ topology on paths with jumps, a heavy-traffic limit theorem for a queueing network, and the random-time-change argument for counting processes.

Difficulty

The obvious argument chains three facts: the primitive processes converge, hence so does the scaled free process $X$ , and the reflection map is continuous. Two steps break. First, subtraction is not continuous in $M_1$ when the two paths jump at the same time in opposite directions, so the joint convergence of $\hat D^n$ across stations needs (4.11) and one common parametrisation. Second, the reflection map is Lipschitz in the uniform topology, but the uniform topology cannot see jumps that occur at nearby times. Carrying the convergence through the reflection map in the $M_1$ topology requires controlling how the regulator and the regulated process move along each jump segment of $\hat X$ , jointly for all coordinates.

Formalization scope

Stations are Fin J; the network index is n : ℕ, and only $n\to\infty$ enters. Durations are indexed from $0$ in Lean. The queue length is integer valued, (3.2) is computed in $\mathbb Z$ , and a solution satisfies $Z\ge 0$ .

Solutions, not constructions. Every statement quantifies over all solutions $(Z^n,B^n)$ of (3.2)–(3.3) and all reflection pairs of $\hat X$ . Existence and uniqueness are asserted in the paper by citation and are not assumed or proved here.
$M_1$ . Parametric representations are monotone in the order of the completed graph, which is the standard definition. The page states only that the time component is nondecreasing. Convergence on $(0,\infty)$ means convergence on every $[a,b]$ with $0<a<b$ continuity points of the limit. Jump segments are segments in $\mathbb R^d$ (strong $M_1$ ). Convergence in $D((0,\infty),\cdot,M_1)$ includes the requirement that every path be càdlàg on $(0,\infty)$ , so a copy of the limit that is continuous nowhere cannot satisfy the continuity-point condition vacuously.
Weak convergence is in coupling form: one probability space carries copies with the right laws that converge almost surely. The limits in (4.1)–(4.4) are continuous, so there the mode is u.o.c.
Corrected printed errors. Lemma 4.2 is stated with $n^{-1}$ in place of the printed $n^{-1/2}$ , as in its proof. The map on p. 346 is read as $\phi(X)=Z$ , $\psi(X)=\operatorname{diag}(\mu)Y$ , following (4.13). The reflection map allows $y(0)\ge 0$ , because $\hat X(0)$ may leave the orthant when $\hat D(0)>0$ ; when $x(0)\ge 0$ this agrees with (2.2).
Added hypotheses. The processes $Z^n,B^n,\hat Z,\hat Y$ are assumed to be stochastic processes (measurable at each time). All networks share one probability space, so that the routing is literally common. No independence is assumed.
The goal is the case $J=1$ of Theorem 4.1. The printed theorem claims strong $M_1$ convergence, with one parametric representation for all $4J$ coordinates, for every $J$ . For $J\ge 2$ that claim fails: during an upstream outage, a downstream queue that empties part-way through the jump bends the prelimit graph of $(\hat D_j,\hat Y_k)$ , while the limit's completed graph is a straight segment. For $J=1$ every coordinate moves linearly through each jump. The milestones Lemma 4.1, Lemma 4.2, (4.24) and (4.28)–(4.29) are stated for general $J$ , and the almost-sure core of the proof for $J=1$ .

A trivializing formalization is excluded. The hypotheses are satisfiable (for example by deterministic arrival and service processes), $\hat N$ is used only when $\sum_ku^j_k=\infty$ , and laws are compared only for measurable path maps.

Needed infrastructure: the Skorohod space with the $M_1$ topology and its characterization on $(0,\infty)$ , continuity of addition and of composition with continuous time changes, the multidimensional reflection map on paths with jumps, and a Skorohod representation argument. Proofs of Lemma 4.1 and Lemma 4.2 are welcome independently.

Selected references

H. Chen, W. Whitt, Diffusion approximations for open queueing networks with service interruptions, Queueing Systems 13 (1993) 335–359. https://doi.org/10.1007/BF01149260
O. Kella, W. Whitt, Diffusion approximations for queues with server vacations, Adv. Appl. Probab. 22 (1990) 706–729 (reference [22] of the paper).
J. M. Harrison, M. I. Reiman, Reflected Brownian motion on an orthant, Ann. Probab. 9 (1981) 302–308. https://doi.org/10.1214/aop/1176994472
H. Chen, A. Mandelbaum, Discrete flow networks: diffusion approximations and bottlenecks, Ann. Probab. 19 (1991) 1463–1519 (reference [6] of the paper).
M. I. Reiman, Open queueing networks in heavy traffic, Math. Oper. Res. 9 (1984) 441–458 (reference [25] of the paper).
W. Whitt, Some useful functions for functional limit theorems, Math. Oper. Res. 5 (1980) 67–85. https://doi.org/10.1287/moor.5.1.67
A. V. Skorohod, Limit theorems for stochastic processes, Theory Probab. Appl. 1 (1956) 261–290. https://doi.org/10.1137/1101022

10 thms1 active userReviewed

Control Theory Dynamical Systems Operations Research+2·Captain: mikedeng1

Stabilization of Hybrid Systems by Feedback Control Based on Discrete-Time State Observations II: Mean-Square and Almost Sure Exponential StabilityResearch Paper

Motivation

Many engineered systems switch between a finite number of operating modes at random times: a power grid after a line failure, a networked controller whose links drop, a manufacturing plant whose machines break down and are repaired. A standard model for such systems is a hybrid stochastic differential equation, also called an SDE with Markovian switching: the state follows an Itô equation whose coefficients depend on a mode that evolves as a continuous-time Markov chain. The monograph of Mao and Yuan (Stochastic Differential Equations with Markovian Switching, 2006) develops the stability theory of these equations.

A controller that stabilizes such a system usually needs the current state. In practice the state is sampled: it is observed at times $0,\tau,2\tau,\dots$ and the control is held between observations. Mao (Automatica 49, 2013) showed that, under a global Lipschitz condition on the drift and diffusion, a feedback control based on discrete-time observations makes a hybrid SDE mean-square exponentially stable when $\tau$ is small enough. You, Liu, Lu, Mao and Qiu (SIAM J. Control Optim. 53(2), 2015) replaced that condition by local Lipschitz continuity plus linear growth, gave an explicit bound (3.5) on the admissible observation interval, and proved $H_\infty$ -stability, asymptotic stability, and, in Section 4, exponential stability in mean square and almost surely with an explicit rate. This mission formalizes that exponential stability result, Theorem 4.2, and the steps of its proof.

Setting

Let $(\Omega,\mathcal F,\{\mathcal F_t\}_{t\ge0},\mathbb P)$ be a probability space with a filtration satisfying the usual conditions (increasing, right-continuous, $\mathcal F_0$ contains the null sets). On it live an $m$ -dimensional $\{\mathcal F_t\}$ -Brownian motion $w$ and a right-continuous $\{\mathcal F_t\}$ -Markov chain $r$ on $S=\{1,\dots,N\}$ with generator $\Gamma=(\gamma_{ij})$ ( $\gamma_{ij}\ge0$ for $i\ne j$ , zero row sums), independent of $w$ . Fix $\tau>0$ and the sampling time $\delta_t=[t/\tau]\tau$ . The controlled system is

dx(t)=\big(f(x(t),r(t),t)+u(x(\delta_t),r(t),t)\big)dt+g(x(t),r(t),t)\,dw(t),\qquad x(0)=x_0,\ r(0)=r_0,\tag{2.1}

with $f,u:\mathbb R^n\times S\times\mathbb R_+\to\mathbb R^n$ and $g:\mathbb R^n\times S\times\mathbb R_+\to\mathbb R^{n\times m}$ .

The hypotheses are:

Assumption 2.1: $f,g$ locally Lipschitz in $x$ , and $|f(x,i,t)|\le K_1|x|$ , $|g(x,i,t)|\le K_2|x|$ ( $|g|$ the trace norm).
Assumption 2.2: $|u(x,i,t)-u(y,i,t)|\le K_3|x-y|$ and $u(0,i,t)=0$ .
Assumption 3.1: there are $U\in C^{2,1}(\mathbb R^n\times S\times\mathbb R_+;\mathbb R_+)$ and $\lambda_1,\lambda_2>0$ with $\mathcal LU(x,i,t)+\lambda_1|U_x(x,i,t)|^2\le-\lambda_2|x|^2$ , where

\mathcal LU=U_t+U_x[f+u]+\tfrac12\operatorname{trace}[g^TU_{xx}g]+\sum_j\gamma_{ij}U(x,j,t).

Assumption 4.1: $c_1|x|^2\le U(x,i,t)\le c_2|x|^2$ with $c_1,c_2>0$ .
Condition (3.5): $\lambda_2>\frac{\tau K_3^2}{\lambda_1}\big[2\tau(K_1^2+2K_3^2)+K_2^2\big]$ and $\tau\le\frac1{4K_3}$ .

Put $\theta=K_3^2/\lambda_1$ , $\lambda=\lambda_2-\theta\tau[2\tau(K_1^2+2K_3^2)+K_2^2]$ (positive by (3.5)), and

H_1=\theta\tau\big(2\tau(K_1^2+2K_3^2)+K_2^2\big)+\frac{24\theta\tau^4K_3^4}{1-6\tau^2K_3^2},\qquad H_2=\frac{12\theta\tau^2K_3^2(\tau K_1^2+K_2^2)}{1-6\tau^2K_3^2}.

In Lean these are Assumption21, Assumption22, C21, LU, Assumption31, Assumption41, Condition35, theta, lam, H1, H2, rateEquationLHS; the basis is HybridSetup, the Itô integral IsItoIntegral, the sampling time delta, solutions SolvesSampledHybridSDE, and the functional (4.7) Vbar, all in the namespace You2015.Expo.

Formalization targets

Goal: Theorem 4.2 (exponential stability)

Under the hypotheses above, the equation

2\tau\gamma e^{2\tau\gamma}(H_1+\tau H_2)+\gamma c_2=\lambda\tag{4.4}

has a unique root $\gamma>0$ , and every solution of (2.1) satisfies

\limsup_{t\to\infty}\frac1t\log\big(\mathbb E|x(t)|^2\big)\le-\gamma,\qquad\limsup_{t\to\infty}\frac1t\log|x(t)|\le-\frac\gamma2\quad\text{a.s.}

for all $x_0\in\mathbb R^n$ , $r_0\in S$ .

Milestones, in the order the proof uses them

(3.15) $\mathbb E|x(t)-x(\delta_t)|^2\le2\mathbb E\int_{\delta_t}^t[\tau|f+u(x(\delta_s),\cdot)|^2+|g|^2]ds$ .
Theorem 3.2 ( $H_\infty$ -stability): $\int_0^\infty\mathbb E|x(s)|^2ds<\infty$ .
(3.21) $\mathbb E|x(s)-x(\delta_s)|^2\le\frac{3(\tau K_1^2+K_2^2)}{1-6\tau^2K_3^2}\int_{\delta_s}^s\mathbb E|x(z)|^2dz+\frac{6\tau^2K_3^2}{1-6\tau^2K_3^2}\mathbb E|x(s)|^2$ .
(4.11) $\mathbb E\bar V(\hat x_z,\hat r_z,z)\le(H_1+\tau H_2)\int_{z-2\tau}^z\mathbb E|x(y)|^2dy$ for $z\ge2\tau$ .
(4.14) $c_1e^{\gamma t}\mathbb E|x(t)|^2\le C$ for $t\ge2\tau$ .
(4.14) $\Rightarrow$ (4.3), the mean-square-to-almost-sure transfer cited from Mao–Yuan [23, Theorem 8.8].

Significance

The result. Theorem 4.2 gives a quantitative guarantee: a controller that samples the state every $\tau$ units makes the switching system decay exponentially, with a rate $\gamma$ computable from the constants of the assumptions. Asymptotic stability (Section 3 of the paper) says nothing about how fast trajectories settle; the rate is what a designer trades against the sampling cost when choosing $\tau$ . The almost sure statement concerns individual trajectories, which is what an operator observes.

Formalizing it. The results are proved in the paper; none of them is machine-checked. Mathlib has real Brownian motion but no Itô integral, no stochastic differential equations and no continuous-time Markov chains. The mission therefore also produces a definition layer: a filtration under the usual conditions, a multidimensional $\{\mathcal F_t\}$ -Brownian motion, an $\{\mathcal F_t\}$ -Markov chain with a given generator, the $L^2$ Itô integral of vector-valued integrands, and the solution notion of an SDE with Markovian switching and a sampled-state delay. A related but different layer exists on Prove2Me for Ethier–Kurtz (EthierKurtz_IsStandardBrownian, EthierKurtz_HasBrownianItoIntegral, EthierKurtz_SolvesBrownianSDE); it has no mode switching and no sampled state, so it cannot express (2.1). Formalization also checks the constants: it found that the printed $H_1$ in (4.5) disagrees with the paper's own derivation (see below).

Difficulty

Equation (2.1) is a stochastic differential delay equation whose delay $t-\delta_t$ is bounded but jumps at every observation time, so the delay-equation stability theorems that require a differentiable delay with derivative below one (Mao–Yuan, p. 285) do not apply. A Lyapunov function of the current state alone leaves the term $U_x[u(x(t))-u(x(\delta_t))]$ , which has no sign and depends on the path over a whole observation interval. An exponential rate requires controlling this delay term with an exponential weight, and the weight inflates the delay contribution by a factor $e^{2\tau\gamma}$ ; the rate equation (4.4) records exactly this balance. The almost sure part does not follow from the mean-square part by Chebyshev's inequality at fixed times alone: a pathwise bound needs control of the supremum of $|x|$ over each unit interval, which involves the martingale part of the solution.

Formalization scope

Conventions committed to in Lean:

The state space is EuclideanSpace ℝ (Fin n), so $|x|$ is the Euclidean norm; the explicit constants in (3.5), (3.21), (4.5) depend on it. The diffusion $g$ is given by its $m$ columns and $|g|^2=\sum_k|g_k|^2$ (trace norm). Modes are Fin N (0-based). Time is ℝ≥0; time integrals are over subsets of $\mathbb R$ at s.toNNReal.
Every expectation of a nonnegative quantity ( $\mathbb E|x|^2$ , $\mathbb E\bar V$ ) and every time integral of one is a lower Lebesgue integral in $[0,\infty]$ , so a non-integrable process cannot produce a junk value $0$ .
Logarithms. The paper's $\log$ takes the value $-\infty$ at $0$ . For a finite $a(t)\ge0$ , $\limsup_{t\to\infty}\frac1t\log a(t)\le-\gamma$ is stated in the equivalent form "for every $\gamma'<\gamma$ , eventually $a(t)\le e^{-\gamma't}$ ". Lean's Real.log 0 = 0 never enters. In (4.3) the almost-sure quantifier is outside the quantifier over $\gamma'$ .
Correction of (4.5). The page prints the last term of $H_1$ as $24\tau^3K_3^4/(1-6\tau^2K_3^2)$ . Substituting (3.21) into (4.9), as the proof does, gives $24\theta\tau^4K_3^4/(1-6\tau^2K_3^2)$ (the same computation reproduces the printed $H_2$ ). The mission uses the corrected $H_1$ in the goal, (4.11) and (4.14). With the printed value the claimed rate could exceed what the proof yields whenever $\theta\tau>1$ .
"The unique root" is a conjunct of the goal ( $\exists!\,\gamma>0$ ); the stability conclusions are stated for every positive root. "(so $\lambda>0$ )" is a consequence of (3.5), not a hypothesis. (4.4) is kept as an equality.
"The solution of (2.1)" is read as every process satisfying the solution definition: progressively measurable, almost surely continuous paths, $\mathbb E|x(t)|^2<\infty$ for each $t$ , and for each $t$ , almost surely, the integral equation with Itô integrals in the $L^2$ sense. Existence and uniqueness (cited from Mao–Yuan on p. 908) are not asserted.
"An $m$ -dimensional Brownian motion" and "a Markov chain with generator $\Gamma$ " are read in the Mao–Yuan framework the paper cites: an $\{\mathcal F_t\}$ -Brownian motion with independent coordinates and increments independent of the past, and an $\{\mathcal F_t\}$ -Markov chain with transition matrix $e^{t\Gamma}$ . The usual conditions are kept as hypotheses.
"Locally Lipschitz" is uniform in the mode and time on each ball. $C^{2,1}$ carries its derivatives $U_t,U_x,U_{xx}$ as witnesses tied to $U$ by derivative relations and joint continuity.
" $\tau>0$ sufficiently small for (3.5)" means every $\tau>0$ satisfying both inequalities of (3.5). $U,\lambda_1,\lambda_2,c_1,c_2,\tau$ are data. The constant $C$ of (4.14) is chosen after $x_0$ , $r_0$ , the solution and $\gamma$ , and before $t$ .
(3.15), (3.21) and the transfer (4.14) $\Rightarrow$ (4.3) are stated under fewer hypotheses than the surrounding proof has (Assumptions 2.1, 2.2, $\tau>0$ , and for (3.21) $\tau\le1/(4K_3)$ ), because their derivations use no more. $\bar V$ of (4.7) is used only for $z\ge2\tau$ , where no extension of the solution to negative times is needed. Other misprints on the page ( $g(x,i,s)=f(x,i,0)$ on p. 909, $V(\hat x_0,\hat r_0,t)$ for $V(\hat x_0,\hat r_0,0)$ on p. 918, the swapped $\vee,\wedge$ on p. 907) are not formalized.

A trivializing formalization is ruled out: the expectations are not Bochner integrals, $\log 0$ is never evaluated, the goal asserts that the rate equation has exactly one positive root (so the stability clauses are not vacuous), the solution notion admits the true solution and requires path continuity, and the derivative witnesses of $U$ are tied to $U$ . A sorry-free local check confirms that Assumptions 2.1, 2.2, 4.1, condition (3.5) and $\lambda>0$ hold for $n=m=N=1$ , $f=g=0$ , $u(x)=-x$ , $U=|x|^2$ , $K_1=K_2=K_3=1$ , $\lambda_1=1/4$ , $\lambda_2=1$ , $c_1=c_2=1$ , $\tau=1/10$ ; for these data $\mathcal LU+\lambda_1|U_x|^2=-|x|^2$ by hand.

Welcome contributions: the Itô isometry and Itô's formula for the $L^2$ integral defined here, a generalized Itô formula for functions of a Markov-modulated Itô process, the Burkholder–Davis–Gundy inequality, and the Borel–Cantelli argument that turns mean-square exponential decay into almost sure decay. These are reusable far beyond this mission. Section 3 of the paper (asymptotic stability) is a separate mission of the same series.

Selected references

S. You, W. Liu, J. Lu, X. Mao, Q. Qiu, Stabilization of Hybrid Systems by Feedback Control Based on Discrete-Time State Observations, SIAM J. Control Optim. 53(2), 905–925, 2015. https://doi.org/10.1137/140985779
X. Mao, C. Yuan, Stochastic Differential Equations with Markovian Switching, Imperial College Press, 2006. https://doi.org/10.1142/p473
X. Mao, Stabilization of continuous-time hybrid stochastic differential equations by discrete-time feedback control, Automatica 49(12), 3677–3681, 2013. https://doi.org/10.1016/j.automatica.2013.09.005

13 thms1 active userReviewed

Dynamic Programming Operations Research Probability+1·Captain: mikedeng1

Exit Problems for Spectrally Negative Lévy Processes and Applications to (Canadized) Russian Options II: Optimal Stopping for the Perpetual Russian OptionResearch Paper

Motivation

A Russian option is a perpetual American-type claim that pays, when the holder exercises at time $\tau$ , the maximum of the asset price seen so far, discounted by $e^{-\alpha\tau}$ . It was introduced by Shepp and Shiryaev for the Black–Scholes market (Shepp–Shiryaev 1993), where the underlying log-price is a Brownian motion with drift. Empirical work on asset returns (skewness, heavy tails, downward jumps) motivates replacing the Brownian motion by a Lévy process with negative jumps only. Avram, Kyprianou and Pistorius (2004) solve the Russian optimal stopping problem in that model in closed form, in terms of the scale functions of the process.

Timeline. 1993: Shepp and Shiryaev solve the Russian problem for geometric Brownian motion; Duffie and Harrison give its no-arbitrage price. Graversen and Peskir, and Kyprianou and Pistorius, treat further variants within the Black–Scholes market (the works the paper cites in §6). 2004: Avram, Kyprianou and Pistorius solve it for every spectrally negative Lévy process, covering both unbounded and bounded variation, using the exit problem of the reflected process $Y=\overline X-X$ (their Theorem 1, the subject of the first mission of this series).

Setting

Let $(\Omega,\mathcal F,\mathbf F=\{\mathcal F_t\}_{t\ge0},\mathbb P)$ be a filtered probability space with a right-continuous filtration, and $X=\{X_t,\ t\ge0\}$ a spectrally negative Lévy process for $\mathbf F$ : $X_0=0$ , càdlàg paths with no positive jumps, independent and stationary increments with $X_{s+t}-X_s$ independent of $\mathcal F_s$ , and paths that are not monotone. The standing assumption of the paper is that $X$ has unbounded variation, or bounded variation and a Lévy measure absolutely continuous with respect to Lebesgue measure.

The Laplace exponent is $\psi(\theta)=\log\mathbb E[e^{\theta X_1}]$ , and $\Phi(q)$ is the largest root of $\psi(\theta)=q$ . For $q\ge0$ the $q$ -scale function $W^{(q)}:\mathbb R\to[0,\infty)$ is the unique function that vanishes on $(-\infty,0]$ , is continuous on $(0,\infty)$ , and satisfies $\int_0^\infty e^{-\theta x}W^{(q)}(x)\,dx=(\psi(\theta)-q)^{-1}$ for $\theta>\Phi(q)$ . Then $Z^{(q)}(x)=1+q\int_{-\infty}^xW^{(q)}(z)\,dz$ . The tilted scale functions $W_v^{(p)}$ are those of the exponent $\psi_v(\theta)=\psi(\theta+v)-\psi(v)$ .

Fix $r\ge0$ with $\psi(1)=r$ (the risk-neutral condition), and let $\mathbb P^1$ be the Esscher measure, $d\mathbb P^1/d\mathbb P|_{\mathcal F_t}=e^{X_t-rt}$ . For $z\ge0$ , under $\mathbb P^1_{-z}$ the process starts at $-z$ with running maximum $\overline X_t=\max\{0,\sup_{u\le t}X_u\}$ , and the reflected process $Y=\overline X-X$ starts at $Y_0=z$ . The passage time is $\tau_k=\inf\{t\ge0:Y_t\notin[0,k)\}$ . Fix $\alpha>0$ and put $q=\alpha+r$ .

The Russian optimal stopping problem (28) is

w^R(z)=\sup_\tau\ \mathbb E^1_{-z}\big[e^{-\alpha\tau+Y_\tau}\big],

the supremum over all $\mathbb P^1$ -almost surely finite $\mathbf F$ -stopping times. The option price is $V_r(M_0,S_0)=S_0\,w^R(\log(M_0/S_0))$ .

Formalization targets

Goal: Theorem 2

With the optimal level (30) and the candidate value

\kappa^*=\inf\{x:\ Z^{(q)}(x)\le qW^{(q)}(x)\},\qquad u(z)=e^zZ^{(q)}(\kappa^*-z),

for every $z\ge0$ ,

w^R(z)=u(z)=\mathbb E^1_{-z}\big[e^{-\alpha\tau_{\kappa^*}+Y_{\tau_{\kappa^*}}}\big],

and $\tau_{\kappa^*}$ is a $\mathbb P^1$ -a.s. finite $\mathbf F$ -stopping time.

Milestones

Remark 4: $W^{(u)}(x)=e^{vx}W_v^{(u-\psi(v))}(x)$ .
Lemma 1: $Z^{(q)}(x)/W^{(q)}(x)\to q/\Phi(q)$ as $x\to\infty$ (for $q\ge0$ , with the paper's convention for $0/\Phi(0)$ ).
Remark 3: $W_v(0+)=0$ if and only if $X$ has unbounded variation.
Corollary 1, (29): the value of stopping at $\tau_k$ ,

\mathbb E^1_{-z}\big(e^{-\alpha\tau_k+Y_{\tau_k}}\big)=e^z\Big(Z^{(q)}(k-z)+\frac{Z^{(q)}(k)-qW^{(q)}(k)}{W^{(q)\prime}(k)-W^{(q)}(k)}W^{(q)}(k-z)\Big).

Lemma 2 (i): for $q>r$ , $f=Z^{(q)}-qW^{(q)}$ decreases on $[0,\infty)$ to $-\infty$ .
Lemma 2 (ii): $\kappa^*=0$ if $W^{(q)}(0+)\ge q^{-1}$ ; otherwise $\kappa^*>0$ is the unique root of $f$ .
The stopped process $e^{-\alpha(t\wedge\tau_{\kappa^*})}u(Y_{t\wedge\tau_{\kappa^*}})$ is a $\mathbb P^1$ -martingale.
$\mathbb E^1_{-z}[e^{-\alpha t+Y_t}Z^{(q)}(\kappa^*-Y_t)]\le e^zZ^{(q)}(\kappa^*-z)$ .
$e^{-\alpha t}u(Y_t)$ is a $\mathbb P^1$ -supermartingale.

Significance

The result. Theorem 2 gives the price of the perpetual Russian option and its optimal exercise rule for every exponential spectrally negative Lévy market. The rule is to exercise when the ratio of the running maximum to the current price first reaches $e^{\kappa^*}$ . The level is explicit through scale functions, and it separates the regimes: for bounded variation with $W^{(q)}(0+)\ge q^{-1}$ , immediate exercise is optimal. The theorem is the model case of a general method: an optimal stopping problem for a functional of $(X,\overline X)$ is reduced, by a change of measure, to one for the reflected process, and solved by verification. The same method underlies the Canadized Russian option (third mission of the series).

Formalizing it. The result is proved in the paper; it has no machine-checked proof. This mission produces a Lean statement of the full verification theorem, including admissibility of $\tau_{\kappa^*}$ . It also states the analytic facts about scale functions that the proof relies on (Lemmas 1, 2 and Remarks 3, 4), which apply to any problem phrased in scale functions.

Difficulty

The obvious route is the classical verification: show that $e^{-\alpha t}u(Y_t)$ is a supermartingale, apply optional stopping, and check equality at $\tau_{\kappa^*}$ . The first step fails as a direct Itô computation. In the unbounded-variation case $u$ is only $C^1$ at $\kappa^*$ , and in the bounded-variation case only continuous there. The generator of $Y$ is nonlocal, so smoothness away from $\kappa^*$ does not control the jump part of the process across the boundary. The equality case needs the exact value of stopping at $\tau_k$ (Corollary 1). That value requires the overshoot of $Y$ over $k$ , which is caused by a downward jump of $X$ , and the exit problem of the reflected process. Finally, $\mathbb P^1$ is not equivalent to $\mathbb P$ on $\mathcal F_\infty$ , so passing from $\mathbb P$ -facts to $\mathbb P^1$ -facts is valid only on each $\mathcal F_t$ .

Formalization scope

Conventions committed to in Lean:

Time is $[0,\infty)$ (ℝ≥0) and values are real. Random times take values in $[0,\infty]$ (WithTop ℝ≥0), and the payoff is set to $0$ on $\{\tau=\infty\}$ , a $\mathbb P^1$ -null event for admissible $\tau$ .
The spectrally negative Lévy process is a structure: measurable marginals, $X_0=0$ , independent increments, stationary increments, càdlàg paths, no positive jumps, not almost surely monotone. Paths start at $0$ , are càdlàg, and have no positive jumps for every $\omega$ , not merely almost surely. Adaptedness, independence of increments from the past, and right-continuity of $\mathbf F$ are added for the filtered version.
"The usual conditions" are read as right-continuity only; completeness is not imposed. $\mathbb P^1$ is typically singular to $\mathbb P$ on $\mathcal F_\infty$ , so a complete $\mathcal F_0$ would contradict (3).
"Unbounded variation" means "not almost surely of bounded variation on compacts". Condition (AC) is stated through jumps: no jump lands in a Lebesgue-null set, almost surely. The standing assumption is "bounded variation implies (AC)".
$\psi$ is Mathlib's cumulant generating function; " $\psi(v)<\infty$ " is integrability of $e^{vX_1}$ .
$W^{(q)}$ is a definite description (choice among functions with the properties of Definition 2) for $q\ge0$ , and the series (5) for $q<0$ . $Z^{(q)}$ integrates over $(-\infty,x]$ .
$\mathbb P^1$ is data (a probability measure $\mathbb Q$ ) with $\mathbb Q|_{\mathcal F_t}=e^{X_t-rt}\cdot\mathbb P|_{\mathcal F_t}$ for all $t$ . $\mathbb P^1_{-z}$ is encoded by the reflected process with prior maximum $0$ and starting point $-z$ .
The value function is a supremum in $[0,\infty]$ of lower Lebesgue integrals. Expectation identities (Corollary 1, the display on p. 230) are stated in $[0,\infty]$ and thereby assert finiteness.
$W^{(q)}(0+)$ is Function.rightLim, and $\kappa^*$ is the real infimum (30); its nonemptiness is Lemma 2, not a hypothesis. $\tau_0=0$ extends the paper's $\tau_k$ , $k>0$ .
Readings of informal words: "decreases monotonically" is strict decrease on $[0,\infty)$ ; "the unique root" is on $[0,\infty)$ ; Lemma 1 is formalized for $q\ge0$ , with $0/\Phi(0)$ read as $\lim_{\theta\downarrow0}\theta/\Phi(\theta)$ as the paper stipulates; Remarks 3 and 4 for real $q$ , $u$ only. The p. 230 martingale, bound and supermartingale claims are stated under the standing assumption, covering all three cases of the proof.

A trivializing formalization is ruled out: the supremum ranges over every $\mathbb P^1$ -a.s. finite stopping time of the given filtration (not only passage times, not a smaller filtration), and it is taken in $[0,\infty]$ , where no junk value of an unbounded real supremum can occur.

Infrastructure a complete development needs: Lévy processes on path space, their Laplace exponents and Esscher transforms, scale functions (existence, uniqueness, smoothness under the standing assumption), the reflected process and the exit identity of Theorem 1, optional stopping for continuous-time supermartingales, and Itô/change-of-variables formulas for semimartingales with jumps. The scale-function and Esscher layers are reusable for the other missions of this series and for any fluctuation-theory problem. Contributions to any of these layers, or to the milestones separately, are welcome.

Selected references

F. Avram, A. E. Kyprianou, M. R. Pistorius, Exit problems for spectrally negative Lévy processes and applications to (Canadized) Russian options, Ann. Appl. Probab. 14(1), 215–238, 2004. https://doi.org/10.1214/aoap/1075828052
L. Shepp, A. N. Shiryaev, The Russian option: reduced regret, Ann. Appl. Probab. 3(3), 631–640, 1993. https://doi.org/10.1214/aoap/1177005715
J. Bertoin, Lévy Processes, Cambridge Tracts in Mathematics 121, Cambridge University Press, 1996. ISBN 0-521-56243-0
A. E. Kyprianou, Fluctuations of Lévy Processes with Applications, 2nd ed., Springer, 2014. https://doi.org/10.1007/978-3-642-37632-0

17 thms1 active userReviewed

Dynamical Systems Probability Reinforcement Learning+1·Captain: mikedeng1

The O.D.E. Method for Convergence of Stochastic Approximation and Reinforcement Learning II: Mean-Square Error under Bounded StepsizesResearch Paper

Motivation

Stochastic approximation is the family of recursive algorithms that locate a zero of a vector field $h$ from noisy evaluations of it. Temporal-difference learning, Q-learning, actor–critic methods and stochastic gradient descent are all instances. In practice these algorithms are often run with a constant or bounded, non-vanishing stepsize: the iterate keeps adapting to new data and never freezes, at the price of never converging exactly. The natural question for such a scheme is quantitative: how far from the target does the iterate stay in the long run, and how does that distance scale with the stepsize?

Borkar and Meyn (SIAM J. Control Optim. 38(2), 2000) answer both halves of the question under one set of hypotheses. First, stability of a "fluid" ODE obtained by scaling $h$ at infinity implies that the iterates have bounded second moments, with no a priori boundedness or projection assumption. Second, if the ODE $\dot x = h(x)$ has a globally exponentially stable equilibrium $x^*$ , the asymptotic mean-square error is of the order of the largest stepsize. The first result replaced the usual stochastic-Lyapunov-function verification in reinforcement-learning applications (Section 3 of the paper). This mission formalizes the bounded-stepsize branch of the paper. A companion mission (… I: Stability and Almost-Sure Convergence under Tapering Stepsizes) covers the vanishing-stepsize branch.

Setting

Fix $d \ge 1$ and a Lipschitz vector field $h : \mathbb{R}^d \to \mathbb{R}^d$ . The stochastic approximation recursion (1.1) is

X(n+1) = X(n) + a(n)\big[h(X(n)) + M(n+1)\big], \qquad n \ge 0,

with a deterministic step sequence $\{a(n)\}$ and a noise sequence $\{M(n)\}$ on a probability space $(\Omega, \mathcal F, \mathsf P)$ . The associated ODE (1.2) is $\dot x = h(x)$ .

The scaled fields are $h_r(x) = r^{-1} h(rx)$ . Assumption (A1) asks that $h$ be Lipschitz, that $h_r(x) \to h_\infty(x)$ for every $x$ as $r \to \infty$ , and that the origin be an asymptotically stable equilibrium of the fluid ODE $\dot x = h_\infty(x)$ .
Let $\mathcal F_n = \sigma(X(0), \dots, X(n))$ . Assumption (A2) asks that $\{M(n)\}$ be a martingale difference sequence, $\mathsf E[M(n+1) \mid \mathcal F_n] = 0$ , with conditional second moments $\mathsf E[\|M(n+1)\|^2 \mid \mathcal F_n] \le C_0(1 + \|X(n)\|^2)$ for a constant $C_0$ .
Assumption (BS), bounded stepsizes: $0 < \underline\alpha \le a(n) \le \bar\alpha < 1$ for all $n$ , with $\underline\alpha < \bar\alpha$ .
The error (2.2) is $e(n) = \|X(n) - x^*\|$ .

An equilibrium $x^*$ of (1.2) is globally asymptotically stable if it is Lyapunov stable and attracts every solution. It is globally exponentially asymptotically stable if there are $b$ and $\delta > 0$ with $\|x(t) - x^*\| \le b\,e^{-\delta t}\|x(0) - x^*\|$ for every solution.

The proofs compare the iterates with ODE solutions on a time grid: $t(n) = \sum_{i<n} a(i)$ , blocks $T(j) = t(m(j))$ of length about $T$ , the interpolated path $\psi$ of the iterates, its rescaled version $\phi_j = \psi/r(j)$ with $r(j) = \max(1, \|X(m(j))\|)$ , and the ODE solutions $\hat\psi$ , $\hat\phi_j$ restarted at each block.

Formalization targets

Goal: Theorem 2.3(ii)

Under (A1), (A2) and (BS), if $x^*$ is a globally asymptotically and globally exponentially asymptotically stable equilibrium of (1.2), there are $\alpha^* > 0$ and $b_2 < \infty$ such that for all $0 < \bar\alpha \le \alpha^*$ and every initial condition $X(0)$ ,

\limsup_{n \to \infty} \mathsf E\big[e(n)^2\big] \le b_2\, \bar\alpha .

The constant $b_2$ is uniform in the stepsizes and in $X(0)$ . No rate constant is fixed: only the linear dependence on $\bar\alpha$ is asserted.

Milestones

Lemma 4.7. For fixed $T > 0$ there is $C_2$ , independent of the stepsizes, with $\mathsf E[\|\phi_j(t) - \hat\phi_j(t)\|^2 \mid \mathcal F_{m(j)}] \le C_2\bar\alpha$ and $\mathsf E[\|\phi_j(t)\|^2 \mid \mathcal F_{m(j)}] \le C_2$ on every block.
Theorem 2.1(ii). There are $\alpha^* > 0$ and $C_1$ with $\limsup_n \mathsf E\|X(n)\|^2 \le C_1$ whenever $\bar\alpha < \alpha^*$ .
Lemma 4.8. For $\bar\alpha \le \alpha^*$ , $\sup_{t \ge 0} \mathsf E\|\hat\psi(t) - \psi(t)\|^2 \le C_3 \bar\alpha$ .

Significance

The result. Theorem 2.1(ii) says that a stability property of a deterministic ODE at infinity controls a stochastic recursion in mean square, uniformly over initial conditions. Theorem 2.3(ii) turns this into an error bound: with a non-vanishing stepsize the iterate does not converge, but its mean-square distance from $x^*$ is eventually $O(\bar\alpha)$ . This is the quantitative justification for constant-stepsize stochastic approximation in reinforcement learning and adaptive control, and it is the starting point of the trade-off between bias (small stepsize) and speed (large stepsize) discussed in Section 2.2 of the paper.

Formalizing it. The results are proved in the paper, partly by sketch: Lemma 4.8's proof refers to "familiar arguments using the Bellman–Gronwall lemma", and the paper writes several bounds as $O(\bar\alpha)$ . A formal proof makes every constant and its dependence explicit, which the paper's quantifier order leaves partly implicit (see the scope section). No machine-checked proof of these results, or of any stochastic-approximation stability theorem in this generality, is known to exist.

Difficulty

The natural first argument, that the iterates track the ODE and the ODE converges, needs the iterates to be bounded. Bounded iterates are exactly what is being proved, so the argument is circular. The paper breaks the circularity by rescaling: on each block the iterate is divided by $r(j)$ , so that on large scales it tracks the fluid ODE, whose stability contracts the norm by a fixed factor per block. Making this work in mean square requires conditional second-moment estimates that are uniform in the stepsize and the scale (Lemma 4.7). A second difficulty is that the stepsize does not vanish: the tracking error per block does not go to zero, and the goal's content is precisely that it is of order $\bar\alpha$ with a constant that does not depend on $\bar\alpha$ .

Formalization scope

The state space is EuclideanSpace ℝ (Fin d). ODE solutions are forward solutions: continuous on $[0,\infty)$ with right derivatives. Stability notions are the standard ones, with exponential stability in the form the proof of Theorem 2.3(ii) uses.
The filtration is the natural filtration of the iterates. (A2) includes integrability of $M(n+1)$ and $\|M(n+1)\|^2$ so that the conditional expectations are meaningful. Each theorem quantifies over every probability space, every measurable process satisfying (1.1) and (A2), and every deterministic $X(0)$ .
Second moments, suprema and $\limsup$ are computed in $[0,\infty]$ , so a bound is a genuine finiteness claim.
Constant placement. $\alpha^*$ , $C_1$ and $b_2$ depend only on $h$ , $h_\infty$ , $C_0$ (and $x^*$ ). $C_2$ depends in addition on $T$ , and $C_3$ on $T$ and $X(0)$ . None depends on the stepsizes. Theorem 2.3's page text puts $b_2$ after $\alpha$ . Read literally, that would allow $b_2 = C_1/\bar\alpha$ and make the goal a restatement of Theorem 2.1(ii). The formal goal fixes $b_2$ before the stepsizes and the initial condition, as the proof ( $16C_3\bar\alpha$ ) gives. $\alpha^*$ is existential in Theorem 2.3(ii) and Lemma 4.8 rather than tied to Theorem 2.1(ii)'s witness.
The proof objects $\hat\psi$ , $\hat\phi_j$ are characterized by predicates (initial value, continuity, ODE on the block). Lemmas 4.7 and 4.8 hold for every function satisfying them.
Not included: Theorem 2.3(i) (its proof chooses a radius depending on $\bar\alpha$ ), Theorem 2.4 and the Markov-chain results of Section 4.3, and the asynchronous extension (Theorem 2.5). The deterministic ODE lemmas 4.1–4.4 belong to the companion mission.

Useful infrastructure, reusable beyond this mission: Bellman–Gronwall inequalities in discrete time (Lemma 4.3 of the paper), stability of scaled ODEs, and conditional second-moment estimates for martingale-difference-driven recursions. Contributions of any of these as separate lemmas are welcome.

Selected references

V. S. Borkar and S. P. Meyn, The O.D.E. Method for Convergence of Stochastic Approximation and Reinforcement Learning, SIAM J. Control Optim. 38(2):447–469, 2000. https://doi.org/10.1137/S0363012997331639
M. Benaïm, Dynamics of stochastic approximation algorithms, Séminaire de Probabilités XXXIII, Lecture Notes in Math. 1709, Springer, 1999. https://doi.org/10.1007/BFb0096509
H. J. Kushner and G. G. Yin, Stochastic Approximation and Recursive Algorithms and Applications, 2nd ed., Springer, 2003. https://doi.org/10.1007/b97441

7 thms1 active userReviewed

Dynamic Programming Operations Research Probability+1·Captain: mikedeng1

On the Optimal Dividend Problem for a Spectrally Negative Lévy Process II: Optimality of the Double-Barrier Strategy at d* with Bail-Out LoansResearch Paper

Dividends, ruin and bail-out loans

An insurance company's surplus in the Cramér–Lundberg model grows linearly with premiums and falls by claims arriving as a compound Poisson process. When premium income exceeds the expected claims, the surplus drifts to infinity. De Finetti (1957) proposed that the surplus above a barrier should instead be paid to shareholders as dividends, and the resulting optimal dividend problem — maximize the expected discounted dividends — is a central problem of risk theory. A barrier policy, however, drives the surplus below zero with probability one. Harrison and Taylor (1978) and Løkka and Zervos studied, for Brownian motion, a variant with bail-out loans: ruin is forbidden, and the shareholders must inject capital whenever the surplus would become negative, at a cost $\varphi>1$ per unit.

Avram, Palmowski and Pistorius (Ann. Appl. Probab. 17 (2007)) solved the bail-out problem when the surplus is a general spectrally negative Lévy process, which includes the Cramér–Lundberg model, Brownian motion with drift and their sums. They showed that the optimal policy is a double barrier policy for every initial capital. This mission formalizes that result, Theorem 3 of the paper.

Timeline:

1957 — de Finetti introduces dividend barriers.
1978 — Harrison and Taylor: optimal control of a Brownian storage system with two reflecting barriers.
1995 — Jeanblanc and Shiryaev: optimal dividends for Brownian motion with drift.
2004 — Avram, Kyprianou and Pistorius: exit problems for spectrally negative Lévy processes reflected at their infimum and supremum, in terms of scale functions.
2007 — Avram, Palmowski and Pistorius: Theorems 1 and 3 of the present paper; Pistorius' pathwise construction of the doubly reflected process is used.

Setting

A spectrally negative Lévy process $X=\{X_t\}_{t\ge0}$ on a filtered probability space $(\Omega,\mathcal F,\mathbb F,P)$ starts at $X_0=0$ , has càdlàg paths, is $\mathbb F$ -adapted, and has stationary increments with $X_t-X_s$ independent of $\mathcal F_s$ . Its jumps are all negative, and $E[e^{\theta X_t}]=e^{t\psi(\theta)}$ for $\theta\ge0$ , where the Laplace exponent is

\psi(\theta)=c\theta+\tfrac{\sigma^2}{2}\theta^2+\int_{(-\infty,0)}(e^{\theta y}-1-\theta y\mathbf 1_{\{|y|<1\}})\,\nu(dy).

With initial capital $x\ge0$ the surplus is $x+X$ . The standing assumptions are: $X$ does not have monotone paths; $E[X_1]>-\infty$ (so $\psi'(0+)=E[X_1]$ is finite); $\sigma>0$ , or $\int_{(-1,0)}|y|\nu(dy)=\infty$ , or $\nu$ has a density (condition (3.3)).

A policy $\bar\pi=(L,R)$ consists of nondecreasing adapted processes with $L_0=R_0=0$ : cumulative dividends $L$ (left-continuous) and cumulative injected capital $R$ (right-continuous). The controlled surplus is $V_t=x+X_t-L_t+R_t$ . The policy is admissible if $V_t\ge0$ for $t>0$ and $\int_0^\infty e^{-qt}dR_t<\infty$ almost surely. Its value and the value function are

\bar v_{\bar\pi}(x)=E\Bigl[\int_0^\infty e^{-qt}dL_t-\varphi\int_0^\infty e^{-qt}dR_t\Bigr],\qquad \bar v_*(x)=\sup_{\bar\pi\ \text{admissible}}\bar v_{\bar\pi}(x),

with discount rate $q>0$ and cost $\varphi>1$ . The double-barrier strategy $\bar\pi_{0,a}$ pays out $(x-a)^+$ at once and then the minimal dividends and injections that keep $V$ in $[0,a]$ : $dL$ is carried by $\{V=a\}$ and $dR$ by $\{V=0\}$ .

The $q$ -scale function $W=W^{(q)}$ vanishes on $(-\infty,0)$ , is continuous and nondecreasing on $[0,\infty)$ , and satisfies $\int_0^\infty e^{-\theta y}W(y)dy=1/(\psi(\theta)-q)$ for $\theta>\Phi(q)$ , the largest root of $\psi=q$ . Set $\overline W(y)=\int_0^yW$ , $Z=1+q\overline W$ , $\overline Z(y)=\int_0^yZ$ . The candidate value of $\bar\pi_{0,a}$ is

\bar v_a(x)=\varphi\bigl(\overline Z(x)+\psi'(0+)/q\bigr)+Z(x)\frac{1-\varphi Z(a)}{qW(a)}\quad(0\le x\le a),\qquad \bar v_a(x)=x-a+\bar v_a(a)\quad(x>a),

and the barrier level is $d^*=\inf\{a>0:[\varphi Z(a)-1]W'(a)-\varphi qW(a)^2\le0\}$ , with $\inf\emptyset=\infty$ .

Formalization targets

Goal: Theorem 3

d^*<\infty,\qquad \bar v_*(x)=\bar v_{d^*}(x)\ \ (x\ge0),\qquad \bar\pi_{0,d^*}\ \text{exists, is admissible and attains }\bar v_*(x).

Milestones

Lemma 1: $\overline W(y)/\overline W(a)\le W(y)/W(a)$ for $0\le y\le a$ .
Proposition 2, (3.17): the expected discounted undershoot $E_x[e^{-qT_0^-}X_{T_0^-}]$ in closed form.
Theorem 1: the expected discounted dividends and injections of $\bar\pi_{0,a}$ , $a>0$ , in closed form; hence $\bar v_{\bar\pi_{0,a}}=\bar v_a$ .
Lemma 2(ii): $d^*=0$ if and only if $\sigma=0$ and $\nu(-\infty,0)\le q/(\varphi-1)$ .
Proposition 3(ii): $d^*<\infty$ and $\bar v_a\le\bar v_{d^*}$ for all levels $a$ .
Lemma 3(ii)–(iv): $1\le\bar v_{d^*}'\le\varphi$ with boundary slopes; $a\mapsto\bar v_a(x)$ nonincreasing for $a>d^*$ ; $\bar v_{d^*}$ concave.
Lemma 5: $(\Gamma\bar v_{d^*}-q\bar v_{d^*})\le0$ on $(0,\infty)$ , with equality on $(0,d^*)$ .
Proposition 4(ii): any $C^2$ solution of the variational inequality (5.9) dominates $\bar v_*$ .

Significance

Theorem 3 answers the bail-out problem completely: for every initial capital and every spectrally negative Lévy surplus, the optimal policy is a double barrier with an explicit level and an explicit value in terms of scale functions. In the classical problem without injections (Theorem 2 of the same paper) the analogous conclusion needs an extra generator condition, and Azcue and Muler exhibited Cramér–Lundberg models where barrier policies are not optimal. The result is the basis of later work on dividends with capital injection, transaction costs and Parisian ruin.

The result has a published proof. What this mission adds is a machine-checked version. As far as is known, no part of the theory used — Lévy processes, scale functions, doubly reflected processes, the generator of a Lévy process, singular stochastic control — has been formalized in Lean's Mathlib.

Difficulty

The value function is a supremum over all adapted singular controls. Its upper bound requires a verification argument: Itô's formula for $e^{-qt}w(V_t)$ with a semimartingale $V$ that has jumps, a controlled bounded-variation part and a possibly nonzero continuous martingale part, followed by localization and limits. A function that satisfies the variational inequality only in the viscosity sense is not enough, so the candidate $\bar v_{d^*}$ must be shown to be regular enough and to satisfy $\Gamma\bar v_{d^*}-q\bar v_{d^*}\le0$ everywhere on $(0,\infty)$ . Above the barrier this inequality does not follow from a martingale property: the paper derives it from concavity and a comparison with higher barriers, through the resolvent of the doubly reflected process. The lower bound requires the existence and value of the doubly reflected process, and computing that value needs fluctuation identities (two-sided exit, overshoot) that are themselves theorems about scale functions.

Formalization scope

Time is indexed by $\mathbb R_{\ge0}$ . The process is a structure carrying the triplet $(c,\sigma,\nu)$ , the paths, adaptedness, independence of future increments from $\mathcal F_s$ , stationarity, the Laplace-exponent identity, and the usual conditions on the filtration. $P_x$ is the law of $x+X$ . Policy values are computed as $E[\int e^{-qt}dL]-\varphi E[\int e^{-qt}dR]$ in the extended reals from two $[0,\infty]$ -valued expectations, and the value function is a supremum in the extended reals; a policy with both expectations infinite gets $-\infty$ . Stieltjes integrals include the jump at time $0$ . The scale function is a hypothesis IsScaleFunction (it is unique), and $d^*$ lives in $[0,\infty]$ , so an empty defining set gives $\infty$ . The double-barrier strategy is characterized by the two-sided Skorokhod conditions plus mutual singularity of $dL$ and $dR$ , which pins the level- $0$ policy of bounded-variation processes. These conditions hold almost surely, and they are stated on the post-decision surplus $V_{t+}=x+X_t-L_{t+}+R_t$ : $dL$ is carried by $\{V_{t+}=a\}$ and $dR$ by $\{V_{t+}=0\}$ . This is the paper's "minimal amount" (p. 4) and matches its construction on pp. 10–11. The closure-of-support wording of (4.2) on its own would also admit non-minimal lump dividends. Admissibility, $V_t\ge0$ for $t>0$ together with (2.3), is likewise required almost surely.

Printed slips corrected (milestone texts are verbatim):

Theorem 3 and Proposition 3(ii) print " $\psi'(0+)<\infty$ ", which always holds; the intended $\psi'(0+)>-\infty$ is used.
(3.3) prints $\int_{-1}^0x\,\nu(dx)=\infty$ for $\int_{(-1,0)}|x|\,\nu(dx)=\infty$ .
(3.4) prints $e^{-\theta x}$ in a $dy$ -integral.
p. 20 prints the extension $\bar v_{d^*}(x)+\varphi x$ for $\bar v_{d^*}(0)+\varphi x$ .
Lemma 3(iv) is printed for every $a>0$ but proved and used only for $a=d^*$ , and is stated for $a=d^*$ .
Proposition 3(ii) at $a=0$ is stated only for bounded variation, where $\bar v_0$ is defined.

The goal cannot be satisfied trivially. It asserts equality of the value function with $\bar v_{d^*}$ , not only an inequality. Existence of the optimal policy is part of the conclusion. Generator statements carry integrability of the jump integrand, so a non-integrable integrand cannot make them true with the junk value $0$ .

A complete development needs Lévy processes and their Laplace exponents, scale functions, first-passage and two-sided exit identities, reflected and doubly reflected processes, Itô's formula for semimartingales with jumps, and a verification theorem for singular control. All of these are reusable well beyond this mission. Contributions of any of these foundations are welcome, as are proofs of the analytic milestones (Lemma 3, Proposition 3(ii)) from the scale-function properties.

Selected references

F. Avram, Z. Palmowski, M. R. Pistorius, On the optimal dividend problem for a spectrally negative Lévy process, Ann. Appl. Probab. 17 (2007) 156–180. https://arxiv.org/abs/math/0702893
F. Avram, A. E. Kyprianou, M. R. Pistorius, Exit problems for spectrally negative Lévy processes and applications to (Canadized) Russian options, Ann. Appl. Probab. 14 (2004) 215–238. https://doi.org/10.1214/aoap/1075828052
M. R. Pistorius, On doubly reflected completely asymmetric Lévy processes, Stochastic Process. Appl. 107 (2003) 131–143. https://doi.org/10.1016/S0304-4149(03)00065-9
J. M. Harrison, A. J. Taylor, Optimal control of a Brownian storage system, Stochastic Process. Appl. 6 (1978) 179–194. https://doi.org/10.1016/0304-4149(78)90059-5
A. E. Kyprianou, Introductory Lectures on Fluctuations of Lévy Processes with Applications, Springer, 2006. https://doi.org/10.1007/978-3-540-31343-4

15 thms1 active userReviewed

Combinatorics Graph Theory Operations Research·Captain: mikedeng1

Graph Minors. V. Excluding a Planar Graph: Bounded Tree-Width without a Planar MinorResearch Paper

Motivation

Tree-width measures how closely a graph resembles a tree. Graphs of bounded tree-width admit dynamic-programming algorithms for problems that are NP-hard in general (colouring, Hamiltonicity, and every property expressible in monadic second-order logic, by Courcelle's theorem), which is why the parameter is central to parameterized complexity and to combinatorial optimization on sparse networks. The question this mission addresses is structural: which excluded substructures force bounded tree-width?

The answer is the Excluded Grid Theorem of Robertson and Seymour: excluding a fixed graph $H$ as a minor bounds the tree-width if and only if $H$ is planar. The "only if" direction is easy, since grids are planar and have unbounded tree-width. The "if" direction is the content of Graph Minors. V. Excluding a Planar Graph (J. Combin. Theory Ser. B 41 (1986) 92–114). It is a cornerstone of the Graph Minors series that culminates in the Robertson–Seymour theorem (graphs are well-quasi-ordered by the minor relation), and it underlies polynomial-time minor testing for planar $H$ (Graph Minors XIII) and the Erdős–Pósa-type results of Sect. 8 of the same paper.

Timeline. Robertson and Seymour, Graph Minors V (1986): tree-width at most an explicit, iterated-exponential function of the grid size. Robertson, Seymour and Thomas, Quickly excluding a planar graph (JCTB 62, 1994): bound $2^{O(\theta^5)}$ for the $\theta$ -grid. Chekuri and Chuzhoy (J. ACM 2016): the first polynomial bound. Chuzhoy and Tan (JCTB 2021): $O(\theta^9\,\mathrm{polylog}\,\theta)$ .

Setting

Graphs are finite. A graph $H$ is a minor of $G$ if $H$ can be obtained by contraction from a subgraph of $G$ ; equivalently, there are nonempty, pairwise disjoint vertex sets $\beta(w)\subseteq V(G)$ , one per vertex $w$ of $H$ , each inducing a connected subgraph, such that every edge $ab$ of $H$ is matched by an edge of $G$ between $\beta(a)$ and $\beta(b)$ .

A tree-decomposition of $G$ is a tree $T$ together with bags $X_t\subseteq V(G)$ ( $t\in V(T)$ ) such that every vertex lies in some bag, both ends of every edge lie in a common bag, and $X_t\cap X_{t''}\subseteq X_{t'}$ whenever $t'$ lies on the path of $T$ between $t$ and $t''$ . Its width is $\max_t(|X_t|-1)$ , and the tree-width $\mathrm{tw}(G)$ is the least width of a tree-decomposition of $G$ .

The $\theta$ -grid has vertex set $\{v_{ij}: 1\le i,j\le\theta\}$ , with $v_{ij}$ adjacent to $v_{i'j'}$ exactly when $|i-i'|+|j-j'|=1$ . For even $\theta\ge 6$ , $\mathcal F_\theta$ is the class of graphs with no minor isomorphic to the $\theta$ -grid. Every planar graph $H$ is a minor of some even grid of size at least 6; $\theta(H)$ denotes the least such size.

The paper fixes explicit parameters. For $k\ge 2$ : $\alpha(2,n)=n+1$ and $\alpha(k,n)=2^{n\theta^4}+\alpha(k-1,2^{n\theta^4}+n+1)$ . Then $\theta_1=2\alpha(\theta^2/2,\theta^2/2)$ ; $\phi_{\theta_1}=\theta^2/2$ and $\phi_k=\phi_{k+1}2^{\phi_{k+1}\theta^2}$ ; $\theta_2=\phi_0+2\phi_1+\dots+2\phi_{\theta_1-1}+\phi_{\theta_1}$ ; $\theta_3=(\theta^2/2)^{\theta_2-1}$ ; $\theta_4=\theta_2\binom{\theta_3}{\theta_2}+\tfrac12\theta^2\binom{\theta_3}{\theta^2/2}$ ; $\theta_5=(\theta^2/2)^{\theta_4-1}$ ; $\theta_6=\theta_3\binom{\theta_5}{\theta_4}+\tfrac12\theta^2\binom{\theta_5}{\theta^2/2}$ ; $\theta_7=\alpha(\theta_5,\theta_6)$ ; $\theta_8=3\theta_5(3^{\theta_5}-1)/4$ ; $\theta_9=\theta_7(\theta_8+1)+1$ .

Two auxiliary structures carry the argument. An $(m,n)$ -web is a pair of families of paths $(A_1,\dots,A_m)$ , $(B_1,\dots,B_n)$ , each family vertex-disjoint, every $A_i$ meeting every $B_j$ , and all $m+n$ paths pairwise edge-disjoint. An $(m,n)$ -mesh is the same with arbitrary connected subgraphs in place of paths and without edge-disjointness.

Formalization targets

Goal: (2.1)

For every finite planar graph $H$ and every finite graph $G$ ,

H \not\preceq G \;\Longrightarrow\; \mathrm{tw}(G)\le\theta_9\bigl(\theta(H)\bigr).

Principal theorem: (7.3)

For even $\theta\ge 6$ and $G\in\mathcal F_\theta$ ,

\mathrm{tw}(G)\le\theta_9.

Intermediate targets

Sect. 2: every planar graph is a minor of some even $\theta$ -grid, $\theta\ge 6$ .
(3.2): $n$ disjoint connected subgraphs meeting each of $V_1,\dots,V_k$ , or a hitting set of size $<\alpha(k,n)$ .
(4.1), (4.2), (4.4), (4.5), (4.6): no $(\theta_2,\theta_2)$ -web in $G\in\mathcal F_\theta$ .
(5.1), (5.2), (5.3): no $(\theta_5,\theta_6)$ -mesh in $G\in\mathcal F_\theta$ .
(6.2), (6.3), (6.4): weighted and unweighted balanced-cut lemmas valid for all graphs.
(7.1), (7.2): separations of order $\le\theta_7$ splitting $V(G)$ , or any $X\subseteq V(G)$ , in ratio $1-\theta_8^{-1}$ .

Significance

The theorem converts a qualitative exclusion (no $H$ minor) into a quantitative width bound, and it is the entry point of the structure theory of minor-closed classes: every minor-closed class excluding a planar graph has bounded tree-width, and hence all MSO-definable problems on it are solvable in linear time. It is used in the proof of the graph minor theorem, in minor testing, and in the Erdős–Pósa property for planar minors (Sect. 8 of the paper).

The result is proved and classical; to our knowledge it has not been machine-checked in any proof assistant, and Mathlib has no graph minors, tree-decompositions or Menger's theorem. A formalization produces reusable definitions (branch-set minors, tree-decompositions, separations, grids) and a checked proof of the paper's explicit bound. The goal is stated with the paper's constant $\theta_9$ , not an optimized one; later improvements are stronger variants, not replacements.

Difficulty

The obvious attempt, building a tree-decomposition greedily from small separations, fails because nothing forces small balanced separations to exist. The whole argument supplies them: a graph without a large grid minor has no large mesh (5.3), and a graph with no large mesh has a balanced separation of bounded order (7.1). The step from no grid to no mesh goes through webs and spiders (Sect. 4) and relies on two results from Graph Minors I ((3.1) and (4.3) of the paper, cited without proof), which themselves depend on Menger's theorem. The balanced-cut lemmas (6.2)–(6.4) rest on Tutte's ordering of 2-connected graphs. None of this infrastructure exists in Mathlib.

Formalization scope

Graphs are Mathlib SimpleGraphs on finite types (Fintype V, DecidableEq V). The paper allows loops and multiple edges; for $G$ this changes nothing, since every notion used depends only on adjacency, and for $H$ in the goal it specializes the theorem to simple planar graphs. Minors use the branch-set model (IsMinor); planarity (IsPlanar) is the existence of a crossing-free drawing in $\mathbb R^2$ , mirroring the platform's FourColor.IsPlanar. Tree-width is not defined as an infimum; "tree-width at most $w$ " (TreewidthLE) is the existence of a tree-decomposition with all bags of size $\le w+1$ over a finite tree. $\theta(H)$ enters the goal as a hypothesis IsLeast {t | Even t ∧ 6 ≤ t ∧ IsMinor H (grid t)} θ, which is satisfiable for every planar $H$ by the Sect. 2 milestone, so the goal is not vacuous. Every statement of Sects. 3–7 that mentions $\theta$ carries the standing assumption " $\theta$ even, $\theta\ge 6$ " as hypotheses. Rational bounds such as $(1-\theta_8^{-1})|V(G)|$ and $2(3^k-1)^{-1}|V(G)|$ are compared in $\mathbb Q$ .

Two printed statements are corrected. (4.5) is printed for $0\le k<\theta_2$ and is stated for $0\le k<\theta_1$ , the only range on which $\phi_{k+1},\psi_{k+1}$ are defined. (5.1) is false as printed for $p=1$ , $q\ge 1$ , so it carries the hypothesis " $p=1$ implies $q=0$ "; the paper uses it only with $p=\theta^2/2$ .

Needed infrastructure, reusable well beyond this mission: Menger's theorem, the Graph Minors I linkage results, Tutte's ordering of 2-connected graphs, and a library of lemmas for minors and tree-decompositions. Proofs of any milestone, of the cited results as separate theorems, and of basic API for the definitions are welcome.

Selected references

N. Robertson, P. D. Seymour, Graph Minors. V. Excluding a Planar Graph, J. Combin. Theory Ser. B 41 (1986) 92–114. https://doi.org/10.1016/0095-8956(86)90030-4
N. Robertson, P. D. Seymour, Graph Minors. I. Excluding a Forest, J. Combin. Theory Ser. B 35 (1983) 39–61. https://doi.org/10.1016/0095-8956(83)90079-5
N. Robertson, P. D. Seymour, R. Thomas, Quickly Excluding a Planar Graph, J. Combin. Theory Ser. B 62 (1994) 323–348. https://doi.org/10.1006/jctb.1994.1073
C. Chekuri, J. Chuzhoy, Polynomial Bounds for the Grid-Minor Theorem, J. ACM 63 (2016), Art. 40. https://doi.org/10.1145/2820609
J. Chuzhoy, Z. Tan, Towards Tight(er) Bounds for the Excluded Grid Theorem, J. Combin. Theory Ser. B 146 (2021) 219–265. https://doi.org/10.1016/j.jctb.2020.09.010
B. Courcelle, The Monadic Second-Order Logic of Graphs. I. Recognizable Sets of Finite Graphs, Information and Computation 85 (1990) 12–75. https://doi.org/10.1016/0890-5401(90)90043-H

28 thms1 active userReviewed

Discrete Geometry·Captain: Minghui

Kepler Conjecture — Flyspeck finite-container theoremResearch Paper

Packing equal balls in three dimensions

The Kepler conjecture asks how much of three-dimensional Euclidean space can be filled by congruent solid balls whose interiors do not overlap. It is a question about all arrangements, including irregular arrangements with no repeating cell. A lattice calculation can exhibit an efficient packing but cannot bound every packing. The result is a central extremal theorem of discrete geometry and a substantial example of a proof combining geometry with finite computation. Hales published a proof in 2005; the later Flyspeck project verified a revised proof in HOL Light and Isabelle. This mission concerns a Lean 4 formalization of that verified result. Its authority is Hales et al., A Formal Proof of the Kepler Conjecture (2017), especially sections 3–4.

Centers, separation, and finite containers

A unit-sphere packing is a set $V\subseteq\mathbb R^3$ of centers such that $\|u-v\|\ge2$ whenever $u,v\in V$ are distinct. The occupied region is the union of the open balls $B(v,1)$ . Tangency is allowed. The ambient metric is the Euclidean metric, represented by EuclideanSpace ℝ (Fin 3).

For a real radius $r$ , write $N_V(r)=\#(V\cap B(0,r))$ , where the observation ball is open. Uniform separation makes this intersection finite. The definition of a packing does not assume that the whole set is finite, periodic, saturated, or contains the origin. A saturated packing is one to which no further center can be added while preserving separation. Saturation occurs in an intermediate theorem; an extension theorem must remove it before the final conclusion. These conventions follow the formal source statement and the packing definitions in the accompanying repository.

Formalization targets

The source-faithful goal is

\forall V\text{ a unit-sphere packing},\quad \exists c\in\mathbb R,\quad\forall r\ge1,\qquad N_V(r)\le\frac{\pi r^3}{\sqrt{18}}+cr^2.

The constant may depend on the packing and must work for every indicated radius. This is the finite-container statement displayed in Hales et al., section 3, published PDF page 6. Its quadratic boundary term is part of the target.

Two additional statements record the conventional density consequence. Define the upper packing density by

\overline\delta(V)=\limsup_{r\to\infty} \frac{\operatorname{vol}((\bigcup_{v\in V}B(v,1))\cap B(0,r))} {\operatorname{vol}(B(0,r))}.

The optional targets are $\overline\delta(V)\le\pi/\sqrt{18}$ for every packing and $\sup_V\overline\delta(V)=\pi/\sqrt{18}$ . They are separate from the core theorem. The analytic count-to-volume bridge and the explicit face-centered cubic witness $\sqrt2\{z\in\mathbb Z^3:\sum_i z_i\equiv0\pmod2\}$ are stated independently. The density need not have an actual limit. This distinction also makes comparison with the current Lean-Eval statement precise.

What the formalization contributes

The finite-container theorem bounds every arrangement at every radius at least one, up to its stated boundary error. The density corollary identifies the optimal asymptotic occupied fraction once a close-packing witness is supplied. It makes no uniqueness assertion: an upper bound and an attaining example do not classify all optimizers. The normalizing unit-ball volume is $4\pi/3$ ; it cancels against the same factor in the observation-ball volume when comparing $N_V(r)/r^3$ to occupied density. The Blueprint, section 1.2, describes the close packings.

Flyspeck already provides a machine-checked proof in its original systems. The work here is to express and prove the same mathematics with Lean's kernel and Mathlib, and to develop reusable geometric, combinatorial, and certificate interfaces. Existing partial Lean 4 work is acknowledged; no priority claim is made. The proposal supplies statements and conditional assembly, not a completed Lean proof.

Why the interfaces matter

The revised proof does not reduce to optimizing a lattice cell. Its local configurations have varying combinatorial types, and the necessary nonlinear estimates and linear relaxations must apply to all their geometric realizations. The primary account, sections 4–9, distinguishes the geometric argument, nonlinear inequalities, tame-graph classification, and linear-program verification. The public milestones preserve these distinctions and use the revised annulus estimate, rather than importing the original decomposition-star architecture unchanged.

Formalization scope and verification

Seven milestones cover packing foundations; the fixed nonlinear catalog; the global geometric reduction; extraction and tameness of a local counterexample; archive classification; exhaustive geometric LP certificates; and the local annulus bound. The last states that every finite packing in $2\le\|v\|\le2.52$ satisfies $\sum_v(2.52-\|v\|)/0.52\le12$ . This is section 4.2, equation (1). A compiled conditional theorem composes these interfaces into the exact final goal.

The nonlinear catalog contains actual real formulas from the six selectors in the pinned final Flyspeck statement: 580 family occurrences indexing 539 distinct source-ID records. These 539 source IDs have 498 distinct normalized syntactic bodies; repeated formulas are retained, and no claim of semantic inequivalence is made. All 539 domains have separately kernel-checked witnesses; this does not prove the inequalities. The graph archive is fixed independently of tameness. The reported 18,762 matches the AFP 2013-12-11 archive: 9 triangular, 1,105 quadrilateral, 15,991 pentagonal and 1,657 hexagonal cases. The AFP entry records a change of tameness constants and archive on 3 July 2014. The final archive has 19,715 rows: 9 + 1,253 + 16,080 + 2,373; the pinned make_archive.hl explicitly records this July-2014 count. Exact permutation comparison shows all 18,762 older classes retained and 953 added, with no duplicate or mirror-equivalent rows within either archive. The mission uses the final accompanying archive, whose source SHA-256 is 703ea865a124aa69f0ee12d94df7065bbbf5701a3085776e24632d14493474db. These are candidate graphs: the classification is coverage, not a claim that every stored row is tame or geometrically realizable (primary §7.2).

The final LP family is pinned to the completed Flyspeck revision 1ce0353008eba83d3c76ae9a25c3c242e4802d53: 19,715 graph-indexed trees and exactly 43,078 leaves from all 39 final binary containers. Every branch, face refinement, rounded row template and selected row index is concrete Lean data. The 42,889 objective-bound leaves include the source score-lower-bound row; 189 leaves are direct infeasibility cases. M6 requires complete decoding, local feasibility at the fixed geometric evaluator, and a checked rational certificate for every structural leaf, including unreachable leaves. Solvers cannot replace the source family by a freely chosen LP. See the completed source verifier and primary §9.

The fixed LP selector table is split into forty consecutive data definition files. The archive and graph case trees each occupy two data files, with separate reusable interfaces. Every definition file is below 900,000 UTF-8 bytes, within the platform's observed 1,048,576-byte scanner limit. Ordered concatenation preserves all 19,715 archive records, 19,715 graph trees and 43,078 LP leaves; this packaging adds no mathematical assumption or milestone.

External search may generate data. Coverage, real-expression bounds, exhaustive branching, and rational infeasibility must be justified by Lean theorems. Interval/Taylor certificates have separate encoding, acceptance, and soundness obligations; exact rational LP soundness and the conditional assembly are already checked infrastructure. Floating-point optimization, source hashes, and unchecked native computation are not proofs. All statements target Lean 4.30.0 and Mathlib c5ea00351c28e24afc9f0f84379aa41082b1188f.

Selected references

Hales et al., A Formal Proof of the Kepler Conjecture, Forum of Mathematics, Pi 5 (2017), e2. DOI, arXiv.
Hales, Dense Sphere Packings: A Blueprint for Formal Proofs, Cambridge University Press (2012). Author's extended version.
Hales, A Proof of the Kepler Conjecture, Annals of Mathematics 162 (2005). Paper.
Bauer and Nipkow, Flyspeck I: Tame Graphs. Archive of Formal Proofs.
Solovyev and Hales, Formal Verification of Nonlinear Inequalities with Taylor Interval Approximations (2013). Paper.
Solovyev and Hales, Efficient Formal Verification of Bounds of Linear Programs. Paper, sections 2–3.

73 thms1 active userReviewed

Combinatorics Graph Theory·Captain: Minghui

Formalize the Four Color Theorem in Lean 4Research Paper

Why formalize the Four Color Theorem in Lean 4?

The Four Color Theorem links a short mathematical statement to a large collection of finite checks. For contributors to graph theory and proof assistants, it is a concrete test of whether abstract mathematics, executable verification, and a public theorem statement can share one auditable foundation. The proposed result is a complete Lean 4 formalization, reusing Mathlib and adapting the established proof architecture to Lean.

The mathematical result is established. Robertson, Sanders, Seymour, and Thomas gave a modern computer-assisted proof in 1997. Gonthier subsequently developed a Coq formalization covering both mathematical reasoning and computation, described in his 2005 report and 2008 Notices article. This mission is classified as ResearchPaper because it formalizes these published results. (RSST, Gonthier 2005, Gonthier 2008)

Graphs, drawings, and colors

The root Lean interface uses Mathlib's SimpleGraph: a finite vertex set with a symmetric, irreflexive adjacency relation. Edges in this representation carry no additional identities or multiplicities. The conventional statement also permits parallel edges. Already-proved local infrastructure uses Mathlib's Graph V E to erase parallel edges while preserving a genuine plane drawing and proper vertex colorings; only the actual vertex set must be finite. A proper vertex coloring assigns a color to every vertex and assigns different colors to adjacent vertices. Four available colors means at most four colors are used; there is no requirement that each color occur.

A planar drawing places distinct vertices at distinct points of the real plane and represents each edge by an injective continuous arc joining its endpoints. An arc contains no other vertex, and arcs of different undirected edges meet only at shared endpoints. Reversing the orientation of an edge reverses its parameterization. A graph is planar when such a drawing exists. This is a geometric condition independent of coloring and of the eventual configuration checkers. Gonthier discusses the graph-embedding formulation in Section 2, PDF p. 4 of the 2005 report.

Write $V$ for the vertex set, $G$ for its adjacency relation, and $C=\{0,1,2,3\}$ for the available colors. Empty graphs, isolated vertices, and disconnected graphs are included. The drawing is a witness to a hypothesis; the theorem does not impose coordinates, a prescribed embedding, or a straight-line representation.

Formalization target

For every finite loopless planar graph, establish

\forall\,G=(V,E),\qquad \operatorname{Planar}(G)\Longrightarrow \exists c:V\to C,\quad \forall v,w\in V,\ \{v,w\}\in E\Longrightarrow c(v)\ne c(w).

The draft Lean target is FourColor.four_color: for every finite vertex type and every SimpleGraph on that type, FourColor.IsPlanar G implies G.Colorable 4. Its graph formulation follows RSST's Section 1, PDF p. 2 of the author-hosted manuscript. The manuscript's PDF page numbers differ from the journal's pagination.

The exact unchanged root signature is:

FourColor.four_color.{u} :
  ∀ (V : Type u) [Finite V] (G : SimpleGraph V),
    FourColor.IsPlanar G → G.Colorable 4

This is an open target signature, not a completed proof. The existing FourColor.FinalAudit.multigraph_four_color_of_necessary_targets conditionally connects the mission obligations to the conventional finite loopless planar multigraph statement. Its drawing has distinct vertex positions and injective continuous arcs for each edge identity; erasing parallel edges is proved to preserve planarity and every proper-coloring constraint. This bridge adds no simplicity, connectedness, triangulation, or nonemptiness assumption to the conventional conclusion. The root target itself remains unchanged.

An equivalent combinatorial formulation is welcome only with the formally verified translations needed to recover this target. If equivalence is claimed, both directions must be proved under precisely stated conventions. In particular, a hypermap coloring theorem alone does not complete this mission.

The original seven structural milestones remain unchanged:

Milestone	Deliverable
1. Graph realization	Construct a planar plain hypermap whose faces represent exactly the nonisolated graph vertices and whose edge steps encode precisely adjacency.
2. Cubic normalization	Construct a plain cubic hypermap with six times as many darts, preserving planarity and bridgelessness and transporting a coloring back.
3. Minimal counterexample	Choose a least-dart counterexample within the planar, bridgeless, plain, precubic comparison class.
4. Counterexample structure	Prove cubicity, connectedness and minimum face arity five as consequences of minimality.
5. Charge conservation	Prove total face charge $120c$ for $c$ components under arbitrary rational dart transfers, and a positive-charge face when connected.
6. Elimination	Complete the source's reducibility and unavoidability analysis to exclude every minimal counterexample.
7. Hypermap theorem	Assemble four-colorability for all planar bridgeless hypermaps.

These correspond to Gonthier's reductions in Section 3, PDF pp. 6–9, and development in Sections 5.1–5.6 of the 2005 report. Exact locations and executable-reference declarations accompany each milestone. Milestones 2, 3 and 6 imply milestone 7; milestones 1 and 7 imply the graph target. Those two conditional implications have been checked in Lean against the exact proposed statements. Milestone 6 now has thirteen concrete supporting targets:

Core target	Deliverable
Catalogue geometry	Prove geometric admissibility of every one of the fixed 633 configurations.
Catalogue reducibility	Kernel-check reducibility of every fixed map and contract using the proved complete checker or a verified refinement.
Reflection	Prove that the explicit mirror preserves minimal counterexamples.
Geometric exclusion	Prove that a C-reducible configuration cannot occur in a minimal counterexample; this includes the Birkhoff and patching arguments.
Presentation soundness	Prove the concrete finite presentation checker's generic soundness as one route to coverage.
Seven coverage cases	Independently handle positive hubs of degrees 5, 6, 7, 8, 9, 10 and 11, allowing reflected occurrences and unbounded neighboring arities.
Transfer bound	Bound each directed transfer by five under the explicit absence-of-configurations hypothesis; proved arithmetic then excludes positive hubs of degree at least 12.

The fixed catalogue and fixed rules are shared by both branches. The local Lean assembly checks that reducibility, geometric exclusion, reflection, the transfer bound, the seven degree cases, and milestones 4–5 imply milestone 6. It then connects to the unchanged hypermap and graph targets. The generic presentation checker offers a sufficient route to the semantic degree targets; its ability to certify every source presentation is not presumed. That route also requires actual presentation certificates and proofs of acceptance for the degree cases. Generic soundness and catalogue geometry alone do not supply those witnesses. Direct proofs of the seven semantic coverage obligations remain valid. Catalogue geometry remains a separate, meaningful finite theorem.

Exact mission obligations

There are 21 open theorem targets: 20 supporting milestones and one root. Every name below has prefix FourColor.. All remain future mission work; the checked conditional assembly is not a proof of any of these targets.

#	Exact target name	Obligation
1	`graph_realization`	Realize a finite drawn graph by a planar plain hypermap with exact face/adjacency incidence.
2	`cubic_normalization`	Construct the sixfold plain cubic map with the stated preservation and coloring transport.
3	`minimal_counterexample_exists`	Select a least-dart counterexample in the precubic comparison class.
4	`minimal_counterexample_structure`	Derive cubicity, connectedness and face arity at least five from minimality.
5	`charge_conservation`	Prove total charge and existence of a positive face for a connected host.
6	`catalogue_embeddable`	Prove the fixed 633 entries satisfy configuration geometry.
7	`catalogue_reducibility_certificates`	Establish accepted reducibility certificates for every fixed entry.
8	`mirror_minimal_counterexample`	Preserve minimal-counterexample status under the specified mirror.
9	`reducible_configuration_exclusion`	Exclude a C-reducible occurrence from a minimal counterexample.
10	`discharge_presentation_soundness`	Prove generic soundness of the concrete finite presentation checker.
11	`degree_5_coverage`	Derive a catalogue occurrence, in either orientation, from a positive degree-5 hub.
12	`degree_6_coverage`	Establish the same semantic occurrence obligation for degree 6.
13	`degree_7_coverage`	Establish the same semantic occurrence obligation for degree 7.
14	`degree_8_coverage`	Establish the same semantic occurrence obligation for degree 8.
15	`degree_9_coverage`	Establish the same semantic occurrence obligation for degree 9.
16	`degree_10_coverage`	Establish the same semantic occurrence obligation for degree 10.
17	`degree_11_coverage`	Establish the same semantic occurrence obligation for degree 11.
18	`discharge_transfer_bound`	Bound each transfer by five under minimality and absence of catalogue occurrences in either orientation.
19	`no_minimal_counterexample`	Assemble the core argument to exclude all minimal counterexamples.
20	`hypermap_four_color`	Assemble four-colorability of every planar bridgeless hypermap.
21	`four_color`	Prove the unchanged finite planar graph root above.

The degree cases quantify over minimal counterexamples with the exact positive score defined by the fixed rules; neighboring degrees have no artificial upper bound. The dependency path uses 16 necessary input targets to derive targets 19, 20 and 21. Targets 6 and 10 support the optional presentation-certificate route. None of targets 19, 20 or 21 is assumed as a shortcut in this assembly.

What completion would provide

The theorem provides a uniform existence guarantee for all finite planar graphs, without a bound on their size. Its Lean development should also make reusable graph embeddings, finite combinatorial maps, coloring transports, and verified finite checkers available to later work.

The existing Rocq development is an executable reference for definitions, dependency structure, and proof behavior. It is not a proof import into Lean. The proposed contribution is a Lean development whose proof objects and computation are justified within Lean's documented foundations. A mechanically translated collection of scripts is not required; contributors should choose abstractions that work well with Mathlib.

Where the difficulty lies

Checking finitely many small graphs does not establish the theorem for arbitrary finite graphs. The development must justify why its finite computational tasks suffice, and must connect their results to the graph statement. The mathematical and computational obligations must meet at explicit, proved interfaces.

There is also a representation gap. The standard target concerns vertex colorings of graphs drawn in the plane, whereas the reference implementation's combinatorial core colors faces of planar bridgeless hypermaps. The latter endpoint is four_color_hypermap in combinatorial4ct.v. Correct treatment of duality, connected components, and isolated vertices is part of the work. Renaming a combinatorial predicate “planar” cannot establish that connection.

Formalization scope and acceptance criteria

Use Lean 4 with a supported, pinned Mathlib revision. The initial draft is checked against Lean v4.30.0 and Mathlib c5ea00351c28e24afc9f0f84379aa41082b1188f. Any later migration must preserve the statements and repeat the relevant checks. Reuse Mathlib's graph and coloring interfaces where appropriate, and develop missing infrastructure as reusable modules. The topological definition must not assume colorability, successful certificate verification, or the conclusion of an intermediate theorem.

The definition layer now provides plane drawings, finite permutation hypermaps, an exact graph/face incidence representation, minimal counterexamples, and rational face charges. Coloring equivalence across a face representation is proved for every positive number of colors, with isolated vertices handled explicitly. Exact Euler equality defines combinatorial planarity; geometric realization is a theorem obligation and cannot be assumed from the name.

The concrete core now defines configurations, ordered boundary traces, contracts, chromograms, Kempe closure, kernel preembeddings and reflected occurrences. The reference reducibility checker has proved soundness and completeness. All 633 maps, rings and contracts are literal data with kernel-validated table/index proofs. The 38 base entries and their 71 symmetrized entries are explicit, and the executable matcher has proved semantic correctness. These infrastructure results do not prove the catalogue's geometric validity, its reducibility, or unavoidability.

The production targets import FourColor.CompactCatalogue.configurations, a compact catalogue containing the same literal maps, rings and contracts. A generic verified decoder constructs validated entries without storing large evaluated proof terms in every import. A separate kernel-checked comparison proves exact ordered equality with the original catalogue, proves that every raw entry is accepted, and proves that none is dropped. The original certificate batches remain available for that audit but are excluded from production target imports. This representation change does not alter any of the 21 mathematical obligations.

Data provenance is pinned to Rocq commit c1d6b1cd5288bea4b067aac13cdde3c18dffe018. Independent fresh-source comparisons check all 633 configurations and every base/expanded rule entry against that snapshot, including actual evaluated Lean payloads. These comparisons establish source correspondence; they are not proofs of reducibility or unavoidability.

The duplicate-data gate rejects unexplained or unintended duplicates and permits verified source-mandated repetition encoding multiplicity or weight. The only repeated rule payload is drule1, deliberately listed twice: the source explains its two-point transfer in discharge.v, lines 17–24 and retains both copies in base_drules (line 145). The Lean rule-match count also counts both copies, preserving weight two. Thus there are 38 base entries with 37 distinct payloads, and 71 expanded entries with 70 distinct payloads. Both copies must remain. No configuration duplicates or other repeated rule payloads are permitted without separately verified source justification.

The reference reducibility evaluator is exponentially expensive. Contributors should implement verified compressed representations or efficient checkers, with acceptance implying the same semantic C-reducibility. Completeness of the reference checker then recovers the stated certificate-existence target. The presentation language is a transparent finite baseline; its generic soundness is an open target, and no completeness claim is made. Source-style quizzes/hubcaps or direct Lean proofs can close the same seven semantic coverage targets. This keeps performance choices separate from the mathematical endpoint.

All computational claims needed by the theorem must be established in Lean. External generators may prepare candidate data or certificates, but their output must be validated by a checker with proved correctness, and the resulting proof must be accepted by the Lean kernel. A recorded successful run of an external program is insufficient. The final theorem and its dependency closure must contain no sorry, admit, unproved custom axiom, or unsupported computational assumption. An axiom audit must identify only Lean/Mathlib's documented foundations. The current 37-declaration conditional/infrastructure audit uses only propext, Classical.choice and Quot.sound; it does not claim an unconditional Four Color proof. Python generators and runtime JSON extraction are outside the mathematical trust boundary and cannot discharge the 21 targets.

Completion requires a reproducible repository in which lake build succeeds from a clean environment and builds the final theorem. Pin toolchain, dependencies, source revisions, and certificate data; document regeneration and verification commands. Maintain a dependency map connecting Lean declarations to exact paper locations and Rocq declarations, and record justified differences in representation. The local multigraph adapter already justifies forgetting parallel-edge multiplicities and transports proper colorings. Any auxiliary restrictions such as connectedness or nonemptiness must be discharged before the root theorem. The current statement and conditional builds verify proposal infrastructure. Success requires proofs of the mission obligations and the final theorem in the reproducible clean build, with no unproved assumptions beyond the documented Lean/Mathlib foundations. All 21 targets remain open at proposal finalization. The submission snapshot records the repository base commit, exact working-file hashes, toolchain, Mathlib revision, payload hashes and audit report; it must not misrepresent uncommitted files as contents of the base commit.

Selected references

Georges Gonthier, A Computer-Checked Proof of the Four Colour Theorem, technical report, 2005. Sections 2–5. Microsoft Research PDF.
Georges Gonthier, Formal Proof—The Four-Color Theorem, Notices of the AMS 55(11), 1382–1393, 2008. Theorem 1 and the formalization architecture. AMS PDF.
Gonthier and Rocq-community contributors, fourcolor, executable formalization, pinned to commit c1d6b1cd5288bea4b067aac13cdde3c18dffe018. Repository.
Neil Robertson, Daniel Sanders, Paul Seymour, Robin Thomas, The Four-Colour Theorem, Journal of Combinatorial Theory, Series B 70(1), 2–44, 1997. DOI; author-hosted manuscript.

54 thms1 active userReviewed

Dynamical Systems Number Theory Probability·Captain: mysticflounder

Tao 2022: Almost All Collatz Orbits Attain Almost Bounded ValuesResearch Paper

Motivation

The Collatz map sends an even positive integer $n$ to $n/2$ and an odd one to $3n+1$ . The Collatz conjecture asserts that every orbit of this map eventually reaches $1$ . It remains an open problem.

Because the conjecture is open, a large part of the literature proves weaker statements that hold for almost all starting values. These results bound how small an orbit gets, not whether it reaches $1$ . They are the strongest unconditional evidence for the conjecture. Terence Tao's 2022 theorem is the strongest result of this type: outside a set of logarithmic density zero, every orbit drops below any prescribed function that tends to infinity, however slowly (Tao 2022).

Timeline

Attributions follow the survey in Tao 2022, Section 1. Here $\mathrm{Col}_{\min}(N)$ is the least value in the orbit of $N$ .

1976 to 1979, Terras and Everett. $\mathrm{Col}_{\min}(N) < N$ for almost all $N$ , in natural density.
1979, Allouche. $\mathrm{Col}_{\min}(N) < N^{\theta}$ for almost all $N$ , for every $\theta > 0.869$ .
1994, Korec. The same bound for every $\theta > \log 3/\log 4 \approx 0.7924$ .
2019 preprint, 2022 publication, Tao. The power $N^{\theta}$ is replaced by any $f(N) \to \infty$ , in logarithmic density instead of natural density (Forum of Mathematics, Pi 10, e12).
2026, ProofAtlas. A complete machine-checked proof of Tao's theorem in Lean 4 is published (formalization record).

Setting

Let $\mathrm{collatzStep} : \mathbb{N} \to \mathbb{N}$ be

\mathrm{collatzStep}(n) = \begin{cases} n/2 & n \text{ even},\\ 3n+1 & n \text{ odd}. \end{cases}

Write $\mathrm{collatzStep}^{[k]}$ for the $k$ -fold iterate, with $\mathrm{collatzStep}^{[0]}(n) = n$ . The orbit of $n$ is the set of values $\mathrm{collatzStep}^{[k]}(n)$ for $k \ge 0$ . It includes $n$ itself.

The Syracuse map acts on odd integers. It sends an odd $n$ to the odd part of $3n+1$ , which is $\mathrm{syracuseStep}(n) = (3n+1)/2^{\nu_2(3n+1)}$ . The Syracuse orbit minimum $\mathrm{syracuseOrbitMin}(n)$ is the least value $\mathrm{syracuseStep}^{[k]}(n)$ over $k \ge 0$ .

For a set $A$ of positive integers and a real cutoff $x \ge 2$ , the logarithmic mass of $A$ up to $x$ is

\mathrm{weightedLogMassReal}(x) = \frac{1}{\log x} \sum_{\substack{1 \le n \le x \\ n \in A}} \frac{1}{n}.

A set of positive integers has logarithmic density $d$ when this quantity tends to $d$ as $x \to \infty$ . Since $\sum_{n \le x} 1/n = \log x + O(1)$ , all positive integers together have logarithmic density $1$ , and the odd positive integers have logarithmic density $1/2$ .

A function $f : \mathbb{N} \to \mathbb{R}$ tends to infinity on positive inputs when for every real $M$ there is an $N$ such that $f(n) > M$ for all $n \ge N$ with $n > 0$ .

Formalization targets

Goal: Tao's Theorem 1.3

For every $f$ that tends to infinity on positive inputs,

\lim_{x \to \infty} \frac{1}{\log x} \sum_{\substack{1 \le n \le x \\ \exists k,\ \mathrm{collatzStep}^{[k]}(n) < f(n)}} \frac{1}{n} = 1.

This is the Lean theorem collatz_almost_bounded_logarithmic. It fixes no rate and no constant, so later improvements do not invalidate it.

Syracuse form: Tao's Theorem 1.6

For every $f$ that tends to infinity on odd positive inputs, the odd $n$ whose Syracuse orbit contains a value below $f(n)$ have logarithmic density $1/2$ , which is all of the odd integers. This is syracuse_almost_bounded_logarithmic.

Quantitative form: Tao's Theorem 3.1

There are constants $C, c > 0$ such that for all real $M \ge 2$ and $x \ge 2$ ,

\frac{1}{\log x} \sum_{\substack{1 \le n \le x,\ n \text{ odd} \\ \mathrm{syracuseOrbitMin}(n) > M}} \frac{1}{n} \le \frac{C}{(\log M)^{c}}.

This is syracuse_uniform_logarithmic_tail_bound. The three targets are listed from weakest to strongest. In Tao's paper, the goal and Theorem 1.6 both follow from Theorem 3.1.

Significance

The result. Theorem 1.3 improves the earlier almost-all bounds on Collatz orbit minima from a power of $N$ to any function that tends to infinity. For example, $\mathrm{Col}_{\min}(N) < \log\log\log\log N$ for almost all $N$ . The theorem does not settle the conjecture. A single divergent orbit or nontrivial cycle is not excluded, because its predecessors form a set with bounded orbit minima.

The formalization. The theorem is proved, and a complete formalization already exists. The ProofAtlas record Tao's Almost-Bounded Collatz Orbits proves the statement taoAlmostBoundedColMin_checked with the same step map and an orbit that includes its starting value. That package has 397 first-party Lean files and about 124,000 source lines. ProofAtlas records a passing build with no sorry and the axiom profile propext, Classical.choice, Quot.sound. The source is released under the Apache-2.0 licence at commit d53c8de00056fb05999e44589f2399d7efa026e4, with copyright held by Advameg, Inc. It was built with Lean v4.30.0-rc2.

The remaining work for this mission is therefore a port, not new mathematics. The existing Lean development must be moved to Lean v4.33.1 and Mathlib 0df444a, and then connected to the goal statement above.

Difficulty

The mathematical difficulty is already resolved in the existing proof. The classical first-descent argument shows that a typical orbit drops below its starting value. Repeating that argument fails, because after one descent the new value is no longer distributed like a random integer of its size, and the error compounds at each repetition. That is why earlier results stop at a power bound $N^{\theta}$ .

The difficulty of this mission is engineering. The port moves a development of about 124,000 lines forward across three minor Lean releases and the corresponding Mathlib changes. Lemma renames, deprecations, and changes in tactic behaviour must be repaired file by file without changing any statement.

Formalization scope

Step map. collatzStep n = if Even n then n / 2 else 3 * n + 1, so $\mathrm{collatzStep}(0) = 0$ . This is the same definition as in the ProofAtlas source.
Orbit. The witness $k$ ranges over all natural numbers, including $k = 0$ .
Density. The goal uses weightedLogMassReal: a real cutoff $x$ , the natural indices $0 \le n \le \lfloor x \rfloor$ , weights $1/n$ , and normalization by $\log x$ . The ProofAtlas statement instead uses integer cutoffs and normalization by the harmonic sum $\sum_{n \le N} 1/n$ . A short bridge between the two normalizations is part of the required work.
Threshold. The hypothesis on $f$ constrains only positive inputs. The value $f(0)$ is irrelevant.
Non-triviality. The case $k = 0$ alone covers only inputs with $n < f(n)$ . For slowly growing $f$ this set is finite, so the goal is not satisfied by the starting value.

The goal is already reduced, through accepted proofs, to the single open statement syracuse_uniform_logarithmic_tail_bound. Two routes therefore close the mission. The first is to port the ProofAtlas development and prove the goal directly through the density bridge. The second is to prove Theorem 3.1 in its stated form. Contributions welcome include ported modules as reusable solutions, the density bridge, and a proof of Theorem 3.1. Every ported file must keep the Apache-2.0 notice and attribution to the ProofAtlas source.

Selected references

Terence Tao, Almost all orbits of the Collatz map attain almost bounded values, Forum of Mathematics, Pi 10 (2022), e12. https://doi.org/10.1017/fmp.2022.8 and https://arxiv.org/abs/1909.03562
ProofAtlas, Tao's Almost-Bounded Collatz Orbits, Lean 4 formalization, source commit d53c8de00056fb05999e44589f2399d7efa026e4, Apache-2.0, 2026. https://proofatlas.ai/formalizations/tao-almost-bounded-orbits/
Jeffrey C. Lagarias (editor), The Ultimate Challenge: The 3x+1 Problem, American Mathematical Society, 2010. https://bookstore.ams.org/MBK/78

7 thms1 active userReviewed

Discrete Geometry·Captain: xuanji

Spencer–Szemerédi–Trotter Unit Distance 4/3 Upper BoundResearch Paper

Motivation

How many pairs of points in an $n$ -point planar set can be at distance one? Counting all pairs gives the trivial bound $\binom n2$ , but Euclidean geometry imposes a much stronger restriction: there are at most $Cn^{4/3}$ unit-distance pairs, for an absolute constant $C$ .

This mission concerns that upper bound alone.

Statement

For a finite set $P\subseteq\mathbb R^2$ , let $u(P)$ be the number of unordered pairs of distinct points at Euclidean distance one:

u(P)=\#\bigl\{\{p,q\}:p,q\in P,\ p\ne q,\ \|p-q\|=1\bigr\}.

Prove that there exists a constant $C>0$ such that

u(P)\le C|P|^{4/3}

for every finite $P\subseteq\mathbb R^2$ . The constant must be independent of $P$ , and there are no general-position assumptions.

Proof idea

The supplied proof uses the crossing lemma. From the unit circles centred at the points of $P$ , it constructs an auxiliary graph with $n=|P|$ vertices and $e$ edges satisfying

u(P)-n\le e, \qquad \operatorname{cr}(G)\le 2n^2.

If $e<4n$ , then $u(P)<5n$ . Otherwise, the crossing lemma gives

\frac{e^3}{100n^2}\le \operatorname{cr}(G)\le 2n^2,

so $e\le \sqrt[3]{200}\,n^{4/3}$ . Together, these cases give the required bound.

The main work is in constructing the graph, controlling its crossings, and proving the crossing lemma. The final numerical deduction is short. The project includes a written proof alongside the Lean development.

Lean formulation and scope

The plane is represented by EuclideanSpace ℝ (Fin 2) and point sets by Finset. The definition of unitDist P counts ordered pairs of distinct points at distance one, then divides by two.

The target proposition is:

∃ C : ℝ, 0 < C ∧
  ∀ P : Finset (EuclideanSpace ℝ (Fin 2)),
    (unitDist P : ℝ) ≤
      C * (P.card : ℝ) ^ ((4 : ℝ) / 3)

This includes empty and singleton sets and uses real exponentiation.

The crossing-consequences project already contains a sorry-free proof of this theorem. The purpose of the mission is to make it available for publication and community verification on Prove2me. The crossing lemma and other supporting results are not separate mission targets. Neither an optimal constant nor a matching lower bound is required.

References

J. Spencer, E. Szemerédi, and W. T. Trotter, Jr., “Unit distances in the Euclidean plane,” in B. Bollobás (ed.), Graph Theory and Combinatorics, Academic Press, 1984, pp. 293–303. Full text.
wpegden/crossing-consequences, commit 8769d142033fce042f502bf2857afb6b1375b5c3. Project overview and build instructions.

2 thms1 active userReviewed

Combinatorics Operations Research Optimization·Captain: mikedeng1

Branch-and-Price-and-Cut for the Split-Delivery Vehicle Routing Problem with Time Windows: Some Optimal Solution Traverses Each Pair of Reverse Customer Arcs at Most OnceResearch Paper

Motivation

Vehicle routing problems ask for minimum-cost vehicle routes that deliver goods from a depot to a set of customers. In the split-delivery vehicle routing problem with time windows (SDVRPTW) a customer's demand may be served by several vehicles, and each customer must be visited inside a prescribed time window. Allowing split deliveries matters in practice: for the variant without time windows, Dror and Trudeau (1989) showed empirically that splitting can save substantially, and Archetti, Savelsbergh and Speranza (2006) proved the savings can reach 50%.

Exact methods for the SDVRPTW are branch-and-price algorithms, and they rely on structural properties of optimal solutions to prune the search. Desaulniers (Operations Research 58(1), 2010) collects these properties in §2 of his paper and uses the strongest one, Corollary 2, as a family of valid inequalities (constraint (7)) in his branch-and-price-and-cut method.

Timeline (as reported by Desaulniers 2010, §§1–2).

1989–1990. Dror and Trudeau prove, for the SDVRP without time windows and with the triangle inequality, that some optimal solution has no two routes sharing more than one split customer.
2006. Gendreau, Dejax, Feillet and Gueguen observe that the property holds with time windows, derive the arc-based Corollary 1, and remark that elementary routes suffice (Remark 1).
2010. Desaulniers strengthens Corollary 1 to pairs of reverse arcs (Corollary 2) and exploits it as cutting planes.

Setting

An instance has $n$ customers $\mathcal N$ , a start depot $0$ and an end depot $n+1$ (the same location at the beginning and end of the planning horizon), and the following data: a vehicle capacity $Q > 0$ ; a demand $d_i > 0$ for each customer, which may exceed $Q$ ; a time window $[e_v, l_v]$ for each node, shared by the two depot copies; nonnegative travel times $t_{vw}$ , which include the service time at $v$ ; and nonnegative costs $c_{vw}$ . The arc set $\mathcal A$ contains the idle arc $(0, n+1)$ and every arc $(v, w)$ , $v \ne w$ , with $e_v + t_{vw} \le l_w$ . The triangle inequality $t_{vx} \le t_{vw} + t_{wx}$ , $c_{vx} \le c_{vw} + c_{wx}$ is assumed throughout.

A route is a walk $0 \to v_1 \to \dots \to v_m \to n+1$ along arcs of $\mathcal A$ , customers possibly repeated, with service start times inside the time windows that respect travel times (waiting is allowed), and nonnegative quantities delivered at its visits whose total is at most $Q$ . Its cost is the sum of its arc costs. A solution is a finite family of routes, one per vehicle, with no bound on their number; it is feasible if every customer $i$ receives in total at least $d_i$ , and optimal if it is feasible and no feasible solution costs less. For customers $i, j$ , let $x_{ij}$ be the number of times arc $(i, j)$ is traversed, summed over all routes of a solution, and let $\mathcal A(\mathcal N) = \mathcal A \cap (\mathcal N \times \mathcal N)$ .

Formalization targets

All four statements assume the triangle inequality and that the instance has a feasible solution, and assert the existence of an optimal solution with a structural property.

Goal: Corollary 2 (p. 181)

\exists \text{ optimal solution with } x_{ij} + x_{ji} \le 1 \quad \text{for all } (i,j) \in \mathcal A(\mathcal N).

The two arcs of a pair of reverse customer arcs are used at most once in total. This is the form constraint (7) of the paper gives to the corollary.

Milestones

Remark 1. Some optimal solution has only elementary routes: no route visits a customer twice.
Theorem 1. Some optimal solution has no two distinct routes with two customers in common.
Corollary 1. Some optimal solution has $x_{ij} \le 1$ for all $(i, j) \in \mathcal A(\mathcal N)$ .

Significance

The result. Corollary 2 turns a property of optimal solutions into linear inequalities on arc-flow variables. Adding them to the arc-flow formulation cuts off fractional points of its linear relaxation while keeping an optimal integer solution, which is how Desaulniers uses them. Remark 1 justifies pricing only elementary routes in column generation. Theorem 1 is the combinatorial fact underneath both corollaries and is reused throughout the split-delivery literature.

Formalizing it. The four results are proved in the literature (Dror–Trudeau; Gendreau et al. 2006); Desaulniers states them without proof. No machine-checked version exists. This mission produces a reusable Lean model of the SDVRPTW (instances, arc sets, feasible routes with schedules and delivery patterns, solutions, optimality) and checked proofs of these properties, including the existence of an optimal solution, which the paper takes for granted.

Difficulty

The obvious argument is local: take an optimal solution that violates the property, shift quantities between two routes, remove a visit, and shortcut. Three points make this less routine than it sounds. First, the statements are existential: each exchange must keep the solution optimal and not reintroduce a violation already removed, so one needs a termination measure that decreases under every exchange (Corollary 2 needs elementarity and the Theorem 1 property simultaneously, not two separate optimal solutions). Second, removing a visit is feasible only because the arc set is defined by time windows: the shortcut arc $(v, w)$ must be shown to exist from the schedule and the triangle inequality on travel times, and the new schedule must be built explicitly. Third, the feasible set is infinite (real quantities, unbounded walks, unbounded number of vehicles), so the existence of an optimal solution is itself a statement to prove, not a hypothesis.

Formalization scope

Namespace SplitDeliveryVRPTW.Known. Nodes are the inductive type Node n (start, cust i for i : Fin n, finish). All quantities, times and costs are real. The arc set is exactly the set the paper defines (read as "if and only if"), with arcs into the start depot and out of the end depot excluded. The triangle inequality for $t$ is imposed on pairwise distinct nodes and for $c$ on triples of arcs, where the paper's data is defined. A route is a customer list (repetitions allowed) with a time function over path positions and a quantity function over visits. A solution is an indexed family Fin m → Route I, so identical routes may appear twice. Demand satisfaction uses $\ge$ , as constraint (2) does. The per-vehicle bound $\min\{d_i, Q\}$ of constraint (14) is omitted because it changes neither the feasible route patterns nor the costs.

Explicit readings of imprecise phrases:

"split customer", "in common" (Theorem 1) are undefined in the paper. A customer two distinct routes visit is split, and the routes have it in common. This visit-based reading is at least as strong as a delivery-based one.
Corollary 2's wording "at most one arc in set $\mathcal A^*_{ij}$ appears at most once" is read through constraint (7): the total number of traversals of the arcs of $\mathcal A^*_{ij}$ is at most one. It is stated in the equivalent form free of the choice of $\mathcal A^*(\mathcal N)$ .
"there exists an optimal solution" is conditional on feasibility, which is the hypothesis added.

Ruled-out trivializations: routes are not restricted to elementary walks (that would make Remark 1 definitional), solutions are not sets (that would forbid duplicate routes), optimality compares against solutions with any number of routes and any visit pattern, "split" is never counted over visits by the same route, capacity and time windows are part of route feasibility, and deliveries occur only at visits.

Useful infrastructure, reusable beyond this mission: shortcut lemmas for feasible routes (removing a visit), exchange lemmas between two routes, and existence of an optimum for split-delivery routing. Contributions of any of these as separate lemmas are welcome.

Selected references

G. Desaulniers, Branch-and-Price-and-Cut for the Split-Delivery Vehicle Routing Problem with Time Windows, Operations Research 58(1):179–192, 2010. https://doi.org/10.1287/opre.1090.0713
M. Dror, P. Trudeau, Savings by split delivery routing, Transportation Science 23(2):141–145, 1989. https://doi.org/10.1287/trsc.23.2.141
M. Dror, P. Trudeau, Split delivery routing, Naval Research Logistics 37(3):383–402, 1990. https://doi.org/10.1002/nav.3800370304
M. Gendreau, P. Dejax, D. Feillet, C. Gueguen, Vehicle routing with time windows and split deliveries, Technical Report 2006-851, Laboratoire Informatique d'Avignon, 2006.
C. Archetti, M. W. P. Savelsbergh, M. G. Speranza, Worst-case analysis for split delivery vehicle routing problems, Transportation Science 40(2):226–234, 2006. https://doi.org/10.1287/trsc.1050.0117

6 thms1 active userReviewed

Combinatorics Graph Theory Operations Research+1·Captain: mikedeng1

Scheduling Subject to Resource Constraints: Classification and Complexity III: The Two-Machine Algorithm for Q2 with One Resource and Unit-Time Jobs Is OptimalResearch Paper

Motivation

Many production and computing systems run jobs on parallel machines that also draw on a shared, limited resource: tools, workers, memory, power. Adding such a resource to a scheduling problem can change its complexity entirely. Błażewicz, Lenstra and Rinnooy Kan (DAM 1983) extended the three-field classification $\alpha\mid\beta\mid\gamma$ of Graham, Lawler, Lenstra and Rinnooy Kan by a resource field $res\lambda\sigma\rho$ , and determined the complexity of every problem with unit-time jobs on identical or uniform machines under the makespan criterion. Their Fig. 2 separates the maximal polynomially solvable cases from the minimal NP-hard ones.

This mission formalizes the polynomial side. Two identical machines are easy under arbitrary resources (Theorem 1, due to Garey and Johnson, via maximum matching). Three identical machines with one resource are NP-hard in the strong sense (Theorem 4), and so are two uniform machines with unit resources (Theorem 3). What remains for uniform machines is settled by two algorithms: a sorting-and-shifting procedure for two uniform machines with one resource of arbitrary size (Theorem 5), and a bottleneck transportation problem for any number of uniform machines with one resource and 0–1 requirements (Theorem 6). The hardness results are the subject of the companion missions I and II.

Setting

There are $n$ jobs $J_1,\dots,J_n$ and $m$ machines $M_1,\dots,M_m$ . Machine $M_i$ has speed $q_i>0$ ; every job has unit execution requirement, so it takes time $1/q_i$ on $M_i$ . Identical machines ( $P$ ) have $q_i=1$ ; uniform machines ( $Q$ ) have arbitrary speeds. There are $l$ resources $R_h$ with positive integer sizes $s_h$ , and job $J_j$ needs a nonnegative integer amount $r_{hj}$ of $R_h$ throughout its execution. The field $res\lambda\sigma\rho$ records restrictions: $\lambda$ bounds the number of resources, $\sigma$ their sizes, $\rho$ the requirements, a dot meaning "part of the input". So $res1{\cdot}{\cdot}$ is one resource with arbitrary size and requirements, and $res1{\cdot}1$ is one resource with requirements in $\{0,1\}$ .

A schedule gives every job a machine $\mu(j)$ and a start time $S_j\ge0$ ; the job is executed during $[S_j,C_j)$ with $C_j=S_j+1/q_{\mu(j)}$ . It is feasible if jobs on the same machine do not overlap and, at every time $t$ , the jobs executed at $t$ use at most $s_h$ of each resource $R_h$ . The makespan is $C_{\max}=\max_j C_j$ . No precedence constraints occur in this mission.

Formalization targets

Goal: Theorem 5, correctness of the algorithm

For $Q2\mid res1{\cdot}{\cdot},\,p_j=1\mid C_{\max}$ with $q_1\ge q_2$ : put all jobs on $M_1$ in order of nonincreasing $r_{1j}$ , then repeatedly move the last job of $M_1$ to the earliest feasible time on $M_2$ after the jobs already there, as long as this strictly reduces $C_{\max}$ . For every order with nonincreasing requirements, the resulting schedule $A$ is feasible and

C_{\max}(A)\le C_{\max}(\sigma)\quad\text{for every feasible schedule }\sigma.

Milestones for the goal

The paper's proof has two steps, both milestones. Call a schedule an (a)–(c) schedule when (a) $M_1$ runs its jobs back to back from time $0$ in nonincreasing $r_{1j}$ , (b) $M_2$ runs its jobs in nondecreasing $r_{1k}$ , and (c) every requirement on $M_1$ is at least every requirement on $M_2$ .

The algorithm's schedule is feasible, is an (a)–(c) schedule, and is best among feasible (a)–(c) schedules.
Every feasible schedule can be transformed into a feasible (a)–(c) schedule with no larger $C_{\max}$ .

Further results

Theorem 1. For $P2\mid res{\cdot}{\cdot}{\cdot},\,p_j=1\mid C_{\max}$ , with $G$ the graph joining two jobs when they can run together and $S$ a maximum matching of $G$ , the optimal makespan is $n-|S|$ .
Theorem 6. For $Q\mid res1{\cdot}1,\,p_j=1\mid C_{\max}$ with the $s_1$ fastest machines listed first, the optimal makespan equals the optimal value of a bottleneck transportation problem that assigns jobs to slots (machine, position) with cost $k/q_i$ , resource jobs only to the $s_1$ fastest machines.

Significance

Theorems 5 and 6 complete the classification of Fig. 2 for uniform machines: every special case of $Q\mid res{\cdot}{\cdot}{\cdot},\,p_j=1\mid C_{\max}$ not covered by the hardness theorems has a polynomial algorithm. Theorem 1 is the classical reduction of two-machine resource scheduling to maximum matching, the model case for later work on scheduling with conflict graphs.

The paper proves these results briefly: "clearly" for the first half of Theorem 5, "obviously" for Theorem 1, and a one-paragraph model for Theorem 6. The exchange argument of Theorem 5 is presented "in an informal way" through five steps that pass through fractional, preempted jobs. A machine-checked proof makes these arguments exact on a model with real start times. No formalization of these results is known, and the platform had no statement about resource-constrained scheduling on uniform machines before this mission.

Difficulty

With $q_1\ne q_2$ the job boundaries on the two machines are misaligned: a job on $M_2$ overlaps parts of several jobs on $M_1$ , so the resource check cannot be done slot by slot, and discrete reasoning on integer time grids does not apply. The exchange argument of Theorem 5 must control the resource usage at every real time while jobs are moved between machines and reordered, and it has to end with a nonpreemptive schedule even though the paper's intermediate steps split jobs. For Theorem 1, the hard direction is the lower bound: a feasible schedule with arbitrary real start times must be converted into a matching, which is a statement about how unit jobs on two machines can overlap. For Theorem 6, one must show that restricting resource jobs to the fastest machines and to back-to-back positions loses nothing.

Formalization scope

Model. Jobs, machines and resources are Fin n, Fin m, Fin l (0-based). Speeds are positive reals, sizes positive naturals, requirements naturals. Start times are nonnegative reals, execution intervals are half-open, and the resource constraint is checked at every real time. $C_{\max}=0$ for $n=0$ . The model carries a precedence digraph for consistency with the companion missions; every statement here assumes it has no arcs.
Implicit hypothesis. Theorems 1 and 5 assume every job fits alone ( $r_{hj}\le s_h$ ), which the paper leaves unstated; without it no feasible schedule exists.
The algorithm is a Lean definition following the page: the order is an argument (any nonincreasing order), "as early as possible" is the earliest start after $M_2$ 's last job at which the resource constraint holds throughout, and the loop stops at the first move that does not strictly reduce $C_{\max}$ .
Optimality is always stated in full: feasibility plus a lower bound against every feasible schedule. No minimum is written as an infimum of a possibly empty set.
Theorem 6 is stated with 0–1 slot assignments, the interpretation the paper gives to $x_{ijk}$ ; the page's constraint $\sum_{k=1}^{m}$ is read as $\sum_{k=1}^{n}$ .
Not formalized: the running times $O(ln^2+n^{5/2})$ (Theorem 1), $O(n\log n)$ (Theorem 5, including the phrase "This O(n log n) algorithm") and $O(n^3)$ (Theorem 6), which depend on a machine model the paper does not fix and, for Theorems 1 and 6, on cited matching and transportation algorithms.
Ruled out: a formalization of the goal that proves optimality only against (a)–(c) schedules, against schedules with integer start times, or for one fixed tie-breaking order proves less than Theorem 5.

Contributions welcome: lemmas about step functions of resource usage on half-open intervals, a left-shifting lemma for unit-time schedules on two machines, and the exchange steps of Theorem 5 as separate lemmas.

Selected references

J. Błażewicz, J.K. Lenstra, A.H.G. Rinnooy Kan, Scheduling subject to resource constraints: classification and complexity, Discrete Applied Mathematics 5 (1983) 11–24. https://doi.org/10.1016/0166-218X(83)90012-4
M.R. Garey, D.S. Johnson, Complexity results for multiprocessor scheduling under resource constraints, SIAM Journal on Computing 4 (1975) 397–411. https://doi.org/10.1137/0204035
R.L. Graham, E.L. Lawler, J.K. Lenstra, A.H.G. Rinnooy Kan, Optimization and approximation in deterministic sequencing and scheduling: a survey, Annals of Discrete Mathematics 5 (1979) 287–326. https://doi.org/10.1016/S0167-5060(08)70356-X
S. Even, O. Kariv, An O(n^{2.5}) algorithm for maximum matching in general graphs, Proc. 16th IEEE FOCS (1975) 100–112. https://doi.org/10.1109/SFCS.1975.23

10 thms1 active userReviewed

Control Theory Dynamical Systems Operations Research+2·Captain: mikedeng1

Stabilization of Hybrid Systems by Feedback Control Based on Discrete-Time State Observations I: Almost Sure Asymptotic StabilityResearch Paper

Motivation

A controller that stabilizes such a system usually needs the current state. In practice the state is sampled: it is observed at times $0,\tau,2\tau,\dots$ and the control is held between observations. Mao (Automatica 49, 2013) showed that, under a global Lipschitz condition on the drift and diffusion, a feedback control based on discrete-time observations stabilizes a hybrid SDE in the sense of mean-square exponential stability when $\tau$ is small enough. You, Liu, Lu, Mao and Qiu (SIAM J. Control Optim. 53(2), 2015) replaced that condition by local Lipschitz continuity plus linear growth, gave an explicit bound (3.5) on the admissible observation interval $\tau$ , and proved $H_\infty$ -stability, mean-square asymptotic stability, almost sure asymptotic stability and exponential stability of the controlled system. This mission formalizes the almost sure asymptotic stability result, Theorem 3.4, and the results it is built on.

Setting

dx(t)=\big(f(x(t),r(t),t)+u(x(\delta_t),r(t),t)\big)dt+g(x(t),r(t),t)\,dw(t),\qquad x(0)=x_0,\ r(0)=r_0,\tag{2.1}

with $f,u:\mathbb R^n\times S\times\mathbb R_+\to\mathbb R^n$ and $g:\mathbb R^n\times S\times\mathbb R_+\to\mathbb R^{n\times m}$ . The feedback $u$ sees the state only at the observation times.

The hypotheses are:

Assumption 2.1: $f,g$ locally Lipschitz in $x$ , and $|f(x,i,t)|\le K_1|x|$ , $|g(x,i,t)|\le K_2|x|$ ( $|g|$ the trace norm).
Assumption 2.2: $|u(x,i,t)-u(y,i,t)|\le K_3|x-y|$ and $u(0,i,t)=0$ .
Assumption 3.1: there are $U\in C^{2,1}(\mathbb R^n\times S\times\mathbb R_+;\mathbb R_+)$ and $\lambda_1,\lambda_2>0$ with $\mathcal LU(x,i,t)+\lambda_1|U_x(x,i,t)|^2\le-\lambda_2|x|^2$ , where

\mathcal LU=U_t+U_x[f+u]+\tfrac12\operatorname{trace}[g^TU_{xx}g]+\sum_j\gamma_{ij}U(x,j,t).

Condition (3.5): $\lambda_2>\frac{\tau K_3^2}{\lambda_1}\big[2\tau(K_1^2+2K_3^2)+K_2^2\big]$ and $\tau\le\frac1{4K_3}$ .

In Lean these are Assumption21, Assumption22, C21, LU, Assumption31, Condition35, in the namespace You2015.Asymp; the basis is HybridSetup, the Itô integral IsItoIntegral, the sampling time delta, and solutions SolvesSampledHybridSDE, in the namespace You2015.Shared shared with the companion mission.

Formalization targets

Goal: Theorem 3.4 (almost sure asymptotic stability)

Under the hypotheses above, every solution of (2.1) satisfies

\lim_{t\to\infty}x(t)=0\quad\text{a.s.}

for all $x_0\in\mathbb R^n$ and $r_0\in S$ . No rate is claimed; the statement is the qualitative convergence of almost every path.

Milestones, in the order the proof uses them

(3.15) $\mathbb E|x(t)-x(\delta_t)|^2\le2\mathbb E\int_{\delta_t}^t[\tau|f+u(x(\delta_s),\cdot)|^2+|g|^2]ds$ .
Theorem 3.2 ( $H_\infty$ -stability): $\int_0^\infty\mathbb E|x(s)|^2ds<\infty$ .
(3.21) $\mathbb E|x(s)-x(\delta_s)|^2\le\frac{3(\tau K_1^2+K_2^2)}{1-6\tau^2K_3^2}\int_{\delta_s}^s\mathbb E|x(z)|^2dz+\frac{6\tau^2K_3^2}{1-6\tau^2K_3^2}\mathbb E|x(s)|^2$ .
(3.23) $\sup_{t\ge0}\mathbb E|x(t)|^2<\infty$ .
$|\mathbb E|x(t_2)|^2-\mathbb E|x(t_1)|^2|\le C(t_2-t_1)$ .
Theorem 3.3: $\lim_{t\to\infty}\mathbb E|x(t)|^2=0$ .
(3.24)–(3.25): $\mathbb E\int_0^\infty|x(t)|^2dt<\infty$ and $\liminf_{t\to\infty}|x(t)|=0$ a.s.
(3.28): $\mathbb P(\exists t:|x(t)|\ge h)\le C/h^2$ for $h>|x_0|$ .

Significance

The result. Theorem 3.4 says that a controller sampling the state at rate $1/\tau$ makes almost every trajectory of the switching system converge to the equilibrium, with an explicit, checkable bound (3.5) on $\tau$ . Mean-square convergence (Theorem 3.3) does not imply almost sure convergence in general, and a single trajectory is what an operator observes, so the pathwise statement is the one relevant to a deployed system. Condition (3.5) is stated in terms of the constants of Assumptions 2.1, 2.2 and 3.1, so for a concrete system (Section 6 of the paper) it gives a numerical bound on the observation interval.

Formalizing it. The results are proved in the paper; none of them is machine-checked. Mathlib has real Brownian motion but no Itô integral, no stochastic differential equations and no continuous-time Markov chains. The mission therefore also produces a reusable definition layer: a filtration under the usual conditions, a multidimensional $\{\mathcal F_t\}$ -Brownian motion, an $\{\mathcal F_t\}$ -Markov chain with a given generator, the $L^2$ Itô integral of vector-valued integrands, and the solution notion of an SDE with Markovian switching and a sampled-state delay. A related but different layer exists on Prove2Me for Ethier–Kurtz (EthierKurtz_IsStandardBrownian, EthierKurtz_HasBrownianItoIntegral, EthierKurtz_SolvesBrownianSDE); it has no mode switching and no sampled state, so it cannot express (2.1).

Difficulty

Equation (2.1) is a stochastic differential delay equation with the delay $t-\delta_t$ , which is bounded but jumps at every observation time and has derivative $1$ in between. The stability theorems for hybrid delay equations in the literature require a differentiable delay with derivative less than one (Mao–Yuan, p. 285), so they do not apply. Applying $\mathcal LU$ directly to $U(x(t),r(t),t)$ leaves the term $U_x[u(x(t))-u(x(\delta_t))]$ , which has no sign and depends on the path over a whole observation interval, so a Lyapunov function of the current state alone does not close the argument.

For the goal, the natural first idea, deducing almost sure convergence from $\mathbb E|x(t)|^2\to0$ or from $\int_0^\infty|x(t)|^2dt<\infty$ a.s., fails: both are compatible with paths that make ever shorter excursions away from $0$ . The obstacle is to exclude infinitely many excursions of a fixed size, which neither moment statement controls.

Formalization scope

Conventions committed to in Lean:

The state space is EuclideanSpace ℝ (Fin n), so $|x|$ is the Euclidean norm; the explicit constants in (3.5) and (3.21) depend on it. The diffusion $g$ is given by its $m$ columns and $|g|^2=\sum_k|g_k|^2$ (trace norm). Modes are Fin N (0-based). Time is ℝ≥0; time integrals are over subsets of $\mathbb R$ at s.toNNReal.
Every expectation $\mathbb E|\cdot|^2$ and every time integral of a nonnegative quantity is a lower Lebesgue integral in $[0,\infty]$ , so a non-integrable process cannot produce a junk value $0$ .
"The solution of (2.1)" is read as every process satisfying the solution definition: progressively measurable, almost surely continuous paths, $\mathbb E|x(t)|^2<\infty$ for each $t$ , and for each $t$ , almost surely, the integral equation with Itô integrals in the $L^2$ sense. Existence and uniqueness (cited from Mao–Yuan on p. 908) are not asserted.
"An $m$ -dimensional Brownian motion" and "a Markov chain with generator $\Gamma$ " are read in the Mao–Yuan framework the paper cites: an $\{\mathcal F_t\}$ -Brownian motion with independent coordinates and increments independent of the past, and an $\{\mathcal F_t\}$ -Markov chain with transition matrix $e^{t\Gamma}$ . The usual conditions are kept as hypotheses.
"Locally Lipschitz" is uniform in the mode and time on each ball. $C^{2,1}$ carries its derivatives $U_t,U_x,U_{xx}$ as witnesses tied to $U$ by derivative relations and joint continuity.
" $\tau>0$ sufficiently small for (3.5)" means every $\tau>0$ satisfying both inequalities of (3.5). $U,\lambda_1,\lambda_2,\tau$ are data of each statement. The paper's " $C$ denotes a positive constant" is an existential chosen after $x_0$ , $r_0$ and the solution, and before the time variables and $h$ .
(3.15) and (3.21) are stated under fewer hypotheses than the surrounding proof has (Assumptions 2.1, 2.2, $\tau>0$ , and for (3.21) $\tau\le1/(4K_3)$ ), because their derivations use no more. Misprints on the page (for example $g(x,i,s)=f(x,i,0)$ on p. 909 and the swapped definitions of $\vee,\wedge$ on p. 907) are not formalized.

A trivializing formalization is ruled out: the expectations are not Bochner integrals (which vanish for non-integrable integrands), the solution notion admits the true solution and requires path continuity, the derivative witnesses of $U$ are tied to $U$ , and a sorry-free check shows that the data hypotheses (Assumptions 2.1, 2.2, 3.1, $C^{2,1}$ , (3.5)) are satisfiable, for example by $n=m=N=1$ , $f=g=0$ , $u(x)=-x$ , $U=|x|^2$ , $\lambda_1=1/4$ , $\lambda_2=1$ , $\tau=1/10$ .

Welcome contributions: the Itô isometry and Itô's formula for the $L^2$ integral defined here, a generalized Itô formula for functions of a Markov-modulated Itô process, and Doob's maximal inequality in continuous time. These are reusable far beyond this mission. Section 4 of the paper (exponential stability) is a separate mission of the same series.

Selected references

S. You, W. Liu, J. Lu, X. Mao, Q. Qiu, Stabilization of Hybrid Systems by Feedback Control Based on Discrete-Time State Observations, SIAM J. Control Optim. 53(2), 905–925, 2015. https://doi.org/10.1137/140985779
X. Mao, C. Yuan, Stochastic Differential Equations with Markovian Switching, Imperial College Press, 2006. https://doi.org/10.1142/p473
X. Mao, Stabilization of continuous-time hybrid stochastic differential equations by discrete-time feedback control, Automatica 49(12), 3677–3681, 2013. https://doi.org/10.1016/j.automatica.2013.09.005

13 thms1 active userReviewed

Control Theory Operations Research Optimization+2·Captain: mikedeng1

A General Stochastic Maximum Principle for Optimal Control Problems: The Maximum Principle with First- and Second-Order Adjoint ProcessesResearch Paper

Motivation

Pontryagin's maximum principle gives necessary conditions for optimality in deterministic optimal control: along an optimal trajectory, the optimal control maximizes (or minimizes) a Hamiltonian built from an adjoint process. For a system driven by Brownian noise the analogous statement was open in full generality for two decades. The difficulty appears exactly when the diffusion coefficient depends on the control and the control domain is not convex, the situation of controlled volatility in finance, of controlled noise intensity in engineering, and of any problem whose admissible actions form a discrete or otherwise nonconvex set.

Shige Peng's 1990 paper (SIAM J. Control Optim. 28(4)) closed that case. It introduced the second-order adjoint process and a second-order variational inequality, and it is the starting point of the modern theory of stochastic Hamiltonian systems and of backward stochastic differential equations as a tool in control.

Timeline.

1972: Kushner obtains necessary conditions for diffusions whose diffusion coefficient does not depend on the control (SIAM J. Control 10).
1973–1978: Bismut introduces the adjoint equation as a linear backward stochastic differential equation and develops duality methods (SIAM Review 20).
Early 1980s: Bensoussan and Haussmann prove maximum principles for convex control domains or control-independent diffusion, using the first-order adjoint equation only.
1990: Peng proves the general principle, with control-dependent diffusion and an arbitrary nonempty control domain (this mission). In the same year Pardoux and Peng prove existence and uniqueness for nonlinear backward SDEs (Systems Control Lett. 14).
1999: Yong and Zhou give a textbook account of the theory (Springer).

Setting

Let $(\Omega,\mathcal F,P)$ be a probability space carrying a standard $d$ -dimensional Wiener process $B=(B^1,\dots,B^d)$ , and let $\mathcal F^t=\sigma\{B(s);0\le s\le t\}$ be its natural filtration. Fix a horizon $T>0$ , an initial state $x_0\in\mathbb R^n$ and a nonempty control domain $U\subseteq\mathbb R^k$ . The data are

g:\mathbb R^n\times\mathbb R^k\to\mathbb R^n,\quad \sigma=(\sigma^1,\dots,\sigma^d),\ \sigma^j:\mathbb R^n\times\mathbb R^k\to\mathbb R^n,\quad l:\mathbb R^n\times\mathbb R^k\to\mathbb R,\quad h:\mathbb R^n\to\mathbb R .

An admissible control $v$ is a progressively measurable $U$ -valued process with $\sup_{t\le T}E|v(t)|^m<\infty$ for every $m\ge1$ . Its trajectory solves the state equation

dx(t)=g(x(t),v(t))\,dt+\sum_{j=1}^d\sigma^j(x(t),v(t))\,dB^j(t),\qquad x(0)=x_0,

and its cost is $J(v)=E\int_0^Tl(x(t),v(t))\,dt+E\,h(x(T))$ . A pair $(y,u)$ is optimal when $J(u)\le J(v)$ for every admissible $v$ .

Assumption (3): $g,\sigma,l,h$ are $C^2$ in $x$ , jointly continuous in $(x,v)$ together with their first and second $x$ -derivatives; $g_x,g_{xx},\sigma_x,\sigma_{xx},l_{xx},h_{xx}$ are bounded; and $g,\sigma,l_x,h_x$ grow at most like $C(1+|x|+|v|)$ .

The Hamiltonian is $H(x,v,p,K)=l(x,v)+(p,g(x,v))+\sum_j(K_j,\sigma^j(x,v))$ . The first-order adjoint process $(p,K)$ solves the backward equation

-dp=\Big[g_x^*p+\sum_j\sigma_x^{j*}K_j+l_x\Big]dt-\sum_jK_j\,dB^j,\qquad p(T)=h_x(y(T)),

and the second-order adjoint process $(P,Q)$ , symmetric-matrix valued, solves

-dP=\Big[g_x^*P+Pg_x+\sum_j\sigma_x^{j*}P\sigma_x^j+\sum_j\sigma_x^{j*}Q_j+\sum_jQ_j\sigma_x^j+H_{xx}\Big]dt-\sum_jQ_j\,dB^j,\qquad P(T)=h_{xx}(y(T)),

with all coefficients evaluated along $(y(t),u(t))$ and both solutions adapted to $\mathcal F^t$ .

Formalization targets

Goal: Theorem 3 (p. 975)

If $(y,u)$ is optimal, then adjoint processes $(p,K)$ and $(P,Q)$ exist in $L^2_{\mathcal F}$ , solving the two equations above, such that for every $v\in U$ , for almost every $\tau\in[0,T]$ , almost surely,

H\big(y,v,p,K-P\sigma(y,u)\big)+\tfrac12\operatorname{tr}\big(\sigma\sigma^*(y,v)P\big)\ \ge\ H\big(y,u,p,K-P\sigma(y,u)\big)+\tfrac12\operatorname{tr}\big(\sigma\sigma^*(y,u)P\big),

all evaluated at time $\tau$ .

Milestones

Lemma 1: the spike-perturbed state equals $y+y_1+y_2$ up to $o(\varepsilon^2)$ in mean square, where $y_1,y_2$ solve the first- and second-order variational equations (5), (6).
Lemma 2: the cost expansion (11) is $\ge o(\varepsilon)$ at an optimal control.
Eq. (13): existence and uniqueness of $(p,K)$ as a Riesz representer.
Eq. (14): the cost expansion in Hamiltonian form is $\ge o(\varepsilon)$ .
Eq. (17): existence and uniqueness of $(P,Q)$ as a Riesz representer.
Eq. (18): the variational inequality for these representers.
Eq. (19): $(p,K)$ is the unique solution of the first-order adjoint equation.
Eq. (20): $(P,Q)$ solves the second-order adjoint equation.

Significance

The result. Theorem 3 is the necessary condition for optimal control of diffusions in its general form. When $\sigma$ does not depend on the control the trace terms cancel and it reduces to the classical first-order principle. When the control enters the diffusion, the first-order condition is false in general, and the second-order adjoint $P$ is the correction. The theorem underlies stochastic linear-quadratic theory, the verification of optimal portfolio and volatility-control policies, and the relation between the maximum principle and the Hamilton–Jacobi–Bellman equation.

Formalizing it. The theorem is classical and proved; none of it is machine-checked. Mathlib has real Brownian motion but no stochastic integral, no SDE and no backward SDE. This mission produces the first formal statements on the platform of a controlled SDE, of a backward SDE and of the maximum principle, together with a precise definition layer (Itô integral, Itô process, BSDE solution) that later missions can reuse, e.g. for Peng's endpoint-constrained principle (§6 of the paper) or for the existence theory of BSDEs. A formal proof would also pin down the approximation arguments the paper leaves to the reader.

Difficulty

The obvious route perturbs the optimal control convexly, $u+\varepsilon(v-u)$ , and differentiates the cost. That needs $U$ convex. For nonconvex $U$ one uses a spike variation on a time interval of length $\varepsilon$ . For deterministic systems the state then moves by $O(\varepsilon)$ and a first-order expansion suffices. With control-dependent diffusion the stochastic integral over the spike interval moves the state by order $\sqrt\varepsilon$ in $L^2$ , so the first-order variational equation leaves an error of the same order as the effect being measured. Second-order terms in the state enter the cost at order $\varepsilon$ , and they are quadratic, so they cannot be handled by a single linear adjoint. The second-order expansion, the matrix-valued adjoint that represents the quadratic term, and the identification of both adjoints with backward SDEs are where the work lies. On the formal side, none of the stochastic calculus exists in Mathlib: the Itô isometry, Itô's formula for matrix-valued processes, moment estimates for linear SDEs and the martingale representation behind the backward equations all have to be built.

Formalization scope

Conventions committed to in Lean:

States, controls and noise are Fin n → ℝ, Fin k → ℝ, Fin d → ℝ with the sup norm; matrices are Matrix (Fin n) (Fin n) ℝ. Time is ℝ≥0, and time integrals are over [0, t] ⊂ ℝ.
The Wiener process is $\mathbb R^d$ -valued: the paper's " $R^n$ -valued standard Wiener process" (p. 967) is a misprint, since $\sigma(x,v)\in\mathcal L(R^d,R^n)$ . Coordinates are independent real Brownian motions (Mathlib's IsBrownianReal).
The filtration is the natural filtration of $B$ , not completed, as on p. 967.
"Adapted", for processes integrated in $dt$ , is read as progressively measurable.
The Itô integral is a relation (an $L^2$ limit of elementary integrals, as in Ikeda–Watanabe), not an operator. SDE and BSDE solutions hold "for every $t$ , almost surely", with $\sup_tE|x(t)|^2<\infty$ for forward solutions and $L^2_{\mathcal F}$ membership for backward ones.
Optimality is among admissible controls of finite cost, and the optimal cost is finite; the paper never states finiteness, and a cost can be $+\infty$ under (3).
Lemma 1 is stated with $o(\varepsilon^2)$ where the page prints " $\le C\varepsilon^2$ " in (4). The proof (via (10)) establishes $o(\varepsilon^2)$ , and Lemma 2 needs it. Lemma 1, (13), (17), (19) and (20) are stated for any admissible pair, since their proofs do not use optimality.
" $\ge o(\varepsilon)$ " means: some $r(\varepsilon)=o(\varepsilon)$ as $\varepsilon\to0^+$ bounds the left side from below for small $\varepsilon$ . " $\forall v\in U$ , a.e., a.s." quantifies $v$ first, then $\tau$ , then $\omega$ .
$P$ and $Q_j$ are symmetric-valued ( $R^{n,n}$ is the space of symmetric matrices, p. 973). Stochastic integrals against the matrix $\sigma$ or $Q$ are sums over the columns, $\sum_j(\cdot)_j\,dB^j$ .

Trivializing formalizations ruled out. Without adaptedness the backward equations have pathwise solutions with $K=0$ and the goal would be free; every adjoint and every solution is required to be progressive for the natural filtration of $B$ . The hypotheses are satisfiable: a sorry-free check shows that the zero problem has an optimal pair and that the Itô relation holds for the zero integrand.

Infrastructure needed, and reusable. The Itô integral and isometry, Itô's formula (vector and matrix forms), existence, uniqueness and moment estimates for linear SDEs with bounded coefficients, Riesz representation in $L^2_{\mathcal F}$ , and existence and uniqueness for linear BSDEs (via martingale representation for the Brownian filtration). All of these are reusable well beyond this mission; contributions of any of them, as separate theorems, are welcome. Related platform definitions: the Ethier–Kurtz series (EthierKurtz_HasBrownianItoIntegral, EthierKurtz_SolvesBrownianSDE) formalizes an Itô integral by dyadic step approximation and uncontrolled SDEs over a completed filtration. The deterministic Pontryagin principle appears in Vector Space Methods XII and Dynamic Programming and Optimal Control III.

Selected references

S. Peng, A General Stochastic Maximum Principle for Optimal Control Problems, SIAM J. Control Optim. 28(4), 966–979, 1990. https://doi.org/10.1137/0328054
H. J. Kushner, Necessary Conditions for Continuous Parameter Stochastic Optimization Problems, SIAM J. Control 10(3), 550–565, 1972. https://doi.org/10.1137/0310041
J.-M. Bismut, An Introductory Approach to Duality in Optimal Stochastic Control, SIAM Review 20(1), 62–78, 1978. https://doi.org/10.1137/1020004
E. Pardoux and S. Peng, Adapted Solution of a Backward Stochastic Differential Equation, Systems & Control Letters 14(1), 55–61, 1990. https://doi.org/10.1016/0167-6911(90)90082-6
J. Yong and X. Y. Zhou, Stochastic Controls: Hamiltonian Systems and HJB Equations, Springer, 1999. https://doi.org/10.1007/978-1-4612-1466-3

12 thms1 active userReviewed