Analysis

Motivation

Quasi-Newton methods such as BFGS were designed for smooth objectives, yet in practice they are routinely and successfully applied to nonsmooth functions. Lewis and Overton (Math. Program. 141 (2013) 135–163) study why. A quasi-Newton step needs a step length along each search direction, and on a nonsmooth function the usual line searches have to decide what to do at points where the function is not differentiable. Classical inexact line searches for nonsmooth optimization (Lemaréchal 1981, Wolfe 1975, Mifflin 1977) ask an oracle for a subgradient at such points. Lewis and Overton propose a simpler rule: a trial point at which the objective is not differentiable simply fails the Wolfe test. This mission formalizes the analysis of that line search, §4 of the paper: when an acceptable step exists, when the bisection search finds one, what happens when it does not, and how many trials it takes on a convex function.

Setting

Let $\bar x$ be an iterate of an optimization algorithm and $\bar p$ a search direction. The line search objective is $h(t)=f(\bar x+t\bar p)-f(\bar x)$ for $t\ge0$. Only $h$ enters the analysis.

Assumption 4.1. The function $h$ is absolutely continuous on every bounded interval and bounded below, and

$$h(0)=0,\qquad s=\limsup_{t\downarrow0}\frac{h(t)}{t}<0 .$$

The number $s$ plays the role of the directional derivative $\nabla f(\bar x)^T\bar p$.

Armijo and Wolfe conditions. Fix constants $c_1<c_2$ in $(0,1)$. For $t>0$,

$$A(t):\ h(t)<c_1st, \qquad W(t):\ h\text{ is differentiable at }t\text{ with }h'(t)>c_2s .$$

An Armijo–Wolfe step is a $t>0$ satisfying both.

Algorithm 4.6. Start from $\alpha=0$, $\beta=+\infty$, $t=1$. At each trial: if $A(t)$ fails, set $\beta\leftarrow t$; otherwise, if $W(t)$ fails, set $\alpha\leftarrow t$; otherwise stop. Then set $t\leftarrow(\alpha+\beta)/2$ if $\beta<+\infty$, and $t\leftarrow2\alpha$ otherwise. So the search doubles until $A$ fails and then bisects the bracket $[\alpha,\beta]$. Write $(\alpha_n,\beta_n,t_n)$ for the state before trial $n=0,1,2,\dots$ (lsRun), so $t_0=1$. The search terminates if some trial passes both tests (Terminates).

Formalization targets

Goal: Theorem 4.7 (convergence)

Under Assumption 4.1 and $0<c_1<c_2<1$:

1. a trial step that passes both tests is an Armijo–Wolfe step;
2. the search terminates under the condition

$$\lim_{t\uparrow\bar t}h'(t)\ \text{exists in }[-\infty,+\infty]\ \text{ for all }\bar t>0; \tag{4.8}$$

3. if the search does not terminate, then eventually the brackets $[\alpha_n,\beta_n]$ are finite, nested, halve in length at each trial and each contains a set of nonzero measure of Armijo–Wolfe steps, and they shrink to a step $\tilde t>0$ with

$$h(\tilde t)=c_1s\tilde t\qquad\text{and}\qquad\limsup_{t\uparrow\tilde t}h'(t)\ge c_2s. \tag{4.9}$$

Milestones

• Lemma 4.4. If $A$ holds at $\alpha>0$ and fails at $\beta>\alpha$, and $h$ is absolutely continuous on $[\alpha,\beta]$, then the Armijo–Wolfe steps in $[\alpha,\beta]$ have nonzero measure.
• Theorem 4.5. Under Assumption 4.1, the Armijo–Wolfe steps have nonzero measure.
• The bracket invariant (proof of Theorem 4.7, pp. 147–148). Without termination, eventually $0<\alpha_n$, $\beta_n<\infty$, $A(\alpha_n)$ holds and $A(\beta_n)$ fails.
• Weak lower semismoothness (pp. 148–149). If $h$ is weakly lower semismooth at every $\bar t>0$ and differentiable at every trial step, the search terminates.
• Proposition 4.11 (complexity on a convex function). For convex $h$ the Armijo–Wolfe steps are the points of differentiability in an open interval $I=(b,b+a)$, and with $d=\max\{1+\lfloor\log_2b\rfloor,0\}$ the search tries a step in $I$ after between $d+1$ and $d+1+\max\{d+\lfloor\log_2(1/a)\rfloor,0\}$ trials when $d\ge1$, and at most $1+\max\{1+\lfloor\log_2(1/a)\rfloor,0\}$ trials when $d=0$.

Significance

Theorem 4.7 is the convergence guarantee for the line search used by the BFGS implementation analysed in the rest of the paper. It isolates the only failure mode: a derivative that oscillates as $t$ increases to a limit point, which condition (4.8) excludes. The paper notes that (4.8) holds for every semi-algebraic $h$, so the search terminates on the functions met in practice. The same line search is the one whose trial sequence produces the binary-expansion behaviour of the secant method in §5. Theorem 4.5 shows that an acceptable step exists on a set of positive measure, which is why a sampling line search is not defeated by the null set of nondifferentiable points. Proposition 4.11 bounds the work per line search on convex functions.

All statements are proved in the paper. None has been formalized; there is no line search for nonsmooth functions on Prove2Me or in Mathlib. A formalization checks the measure-theoretic argument (absolute continuity and the fundamental theorem of calculus for Lebesgue integrals), the bookkeeping of the bisection, and the complexity count, where the printed upper bound turns out to be false for $b<1$.

Difficulty

The obvious proof of termination fails: on a nonsmooth function the bisection can land on a kink at every trial, and the paper's §4.2 constructs a convex $h$ where it does. Termination therefore cannot follow from Assumption 4.1 alone, and both the existence of acceptable steps and the convergence of the brackets have to be argued through measure: Lemma 4.4 needs the fundamental theorem of calculus for absolutely continuous functions and a supremum argument over almost-everywhere inequalities. The non-termination analysis has to combine the bracket invariant with Lemma 4.4 on every late bracket and with a limit argument for (4.9). The complexity bound needs a careful count of doubling and bisection trials, including the regime $b<1$ where no doubling occurs.

Formalization scope

The objective is h : ℝ → ℝ; only its values on $[0,\infty)$ enter. Lebesgue measure is volume with values in $[0,\infty]$, and "nonzero measure" is volume S ≠ 0. Limits superior and inferior are computed in EReal. The upper bound $\beta$ is in WithTop ℝ, with $\top=+\infty$. Stopping freezes the state of lsRun. Mathlib's deriv is $0$ at nondifferentiable points, so the Wolfe condition, condition (4.8) and (4.9) all state differentiability explicitly.

Deviations from the page, each disclosed in the item's Formalization Note:

• Lemma 4.4 adds the standing $0<c_1<c_2<1$ and $s<0$, which its statement omits and its proof uses.
• Condition (4.8) is read as differentiability on a left neighbourhood of $\bar t$ plus existence of the limit, as the proof on p. 148 uses it.
• (4.9) takes the $\limsup$ over points of differentiability left of $\tilde t$; an empty such set would give $-\infty$, so the bound is not vacuous.
• Weak lower semismoothness restricts the paper's subgradient sequences to derivatives at points of differentiability (no Clarke subdifferential in Mathlib). This weakens the hypothesis and strengthens the theorem; the paper's argument proves it unchanged.
• Proposition 4.11. The printed upper bound is false for $b<1$: for $s=-1$, $c_1=0.6$, $c_2=0.9$ and the convex piecewise linear $h$ with slopes $-1$ on $[0,\frac12]$ and $-0.2$ on $[\frac12,10]$, the interval is $I=(\frac12,1)$, the bound is $2$, and the search needs $3$ trials. The bound for $d=0$ is replaced by $1+\max\{1+\lfloor\log_2(1/a)\rfloor,0\}$. The case $a=+\infty$ cannot occur under Assumption 4.1, and a trial at a kink inside $(b,b+a)$ counts as reaching $I$.

Algorithm 4.6 is encoded as the literal state machine; a definition of the search as "some Armijo–Wolfe step" or as an arbitrary nested sequence of brackets would make the goal trivial and is ruled out. The Wolfe condition includes differentiability; without it every kink would pass, since $0>c_2s$.

A complete development needs absolute continuity (AbsolutelyContinuousOnInterval, with almost-everywhere differentiability and the fundamental theorem of calculus, both in Mathlib), the mean value theorem, and facts about one-sided derivatives of convex functions. Lemma 4.4 and the bracket invariant are reusable for other bracketing line searches. Contributions of the milestones in order, of proofs of the definitions' basic properties (all trial steps are positive, the brackets are monotone), and of the §4.2 non-termination example are welcome.

Selected references

• A. S. Lewis, M. L. Overton, Nonsmooth optimization via quasi-Newton methods, Math. Program. Ser. A 141 (2013) 135–163. https://doi.org/10.1007/s10107-012-0514-2
• C. Lemaréchal, A view of line-searches, in: Optimization and Optimal Control, Lecture Notes in Control and Information Sciences 30, Springer, Berlin, 1981, pp. 59–78 (reference [26] of the paper).
• P. Wolfe, A method of conjugate subgradients for minimizing nondifferentiable functions, Math. Programming Study 3 (1975) 145–173 (reference [51] of the paper).
• R. Mifflin, An algorithm for constrained optimization with semismooth functions, Math. Oper. Res. 2 (1977) 191–207. https://doi.org/10.1287/moor.2.2.191

Why the geometry of a minimum needs a parameter convention

A trained neural network is used through its predictions, while its parameters are the coordinates in which training takes place. Distinct parameter vectors can describe exactly the same prediction function. A proposed explanation of generalization based on the shape of the parameter-space loss therefore needs to account for these equivalences. This mission concerns Hessian sharpness: the spectral norm of the matrix of second derivatives of the loss at a minimum. The question is whether that number is intrinsic to the predictor or can change without changing any prediction.

Dinh, Pascanu, Bengio, and Bengio establish that, for a one-hidden-layer rectified network, every sufficiently differentiable critical minimum with nonzero Hessian has equivalent parameterizations of arbitrarily large Hessian sharpness. The formalization target is their Section 4.2, Theorem 4, PDF pp. 5–6. The goal theorem and both supporting milestones now have accepted Lean proofs on Prove2Me. This public research-paper mission is complete.

The immediate historical sequence is:

• 2016–2017: Keskar and collaborators reported numerical evidence relating large-batch training, sharp minima, and a generalization gap. This is empirical context, not an assumption or a theorem to be proved in this mission. ICLR 2017 paper.
• March 2017: Dinh and collaborators released a mathematical analysis of parameter symmetries and several flatness measures. The fixed source for this mission is their May 2017 revision, arXiv version 2, which determines the theorem numbering and PDF page citations. Version history.

Networks, losses, and reciprocal layer scaling

Fix positive integers $d$ and $h$, the input dimension and hidden width. Let $W\in\mathbb R^{d\times h}$ and $v\in\mathbb R^h$ be the network's weights. For an input $x\in\mathbb R^d$, define

$$f_{W,v}(x)=\sum_{j=1}^h \max\!\left(\sum_{i=1}^d x_iW_{ij},0\right)v_j.$$

This is a bias-free network with one hidden layer, rectified activation, and a scalar linear output. Its parameter vector $\theta=(W,v)$ has $n=dh+h$ coordinates and the Euclidean norm. A function-based loss is a real-valued functional $\ell$ of the entire prediction function, giving $L(\theta)=\ell(f_\theta)$. The Hessian targets assume $L$ is continuous. These conventions come from Sections 2–3, PDF pp. 2–4, Definition 3.

Two parameters are observationally equivalent if their predictions agree on every input. For a positive real number $\alpha$, the layer scaling is

$$T_\alpha(W,v)=(\alpha W,\alpha^{-1}v).$$

The definition rescales the incoming and outgoing weights in opposite ways. It is the transformation in Section 3, Definition 5, PDF p. 4.

Write $DL(\theta)$ for the first Fréchet derivative and $H_L(\theta)=D(DL)(\theta)$ for the second derivative. The local differentiability condition requires $L$ to be differentiable throughout a neighborhood of $\theta$, with $DL$ differentiable at $\theta$. This states the regularity needed for the paper's Hessian notation explicitly, without requiring global smoothness or continuous second derivatives. A critical local minimum satisfies $DL(\theta)=0$ and has no smaller loss in some neighborhood; it may belong to a continuum of minima.

Symmetry, derivative transformation, and the goal theorem

The first milestone formalizes the scaling consequence of positive ReLU homogeneity in Theorem 1 and Definition 5, PDF p. 4:

$$f_{T_\alpha\theta}=f_\theta,\qquad L(T_\alpha\theta)=L(\theta),$$

and $T_\alpha\theta$ is a local minimum precisely when $\theta$ is. These statements hold for every parameter and every $\alpha>0$; the milestone itself requires no loss regularity.

The second milestone is Theorem 3, Section 4.2, PDF p. 5. At every point satisfying the stated local differentiability condition,

$$DL(T_\alpha\theta)[u]=DL(\theta)[T_{\alpha^{-1}}u],$$ $$H_L(T_\alpha\theta)[u,w] =H_L(\theta)[T_{\alpha^{-1}}u,T_{\alpha^{-1}}w]$$

for all parameter directions $u,w$. The same regularity holds at the rescaled point. This is the coordinate-free form of the paper's gradient formula and Hessian congruence with $D_\alpha=\operatorname{diag}(\alpha^{-1}I_{dh},\alpha I_h)$.

The goal is Theorem 4. If $\theta$ is a critical local minimum with the stated differentiability and $H_L(\theta)\ne0$, then

$$\forall M>0\ \exists\alpha>0:\qquad \|H_L(T_\alpha\theta)\|_2\ge M.$$

For that same rescaling, predictions and loss agree with the original ones, and the transformed parameter remains a critical local minimum with the required differentiability. The subscript $2$ denotes the Euclidean spectral norm. The source statement and its interpretation are in Section 4.2, PDF pp. 5–6. The relevant displays in all three targets are unnumbered.

What the formalization establishes

The result separates prediction behavior from this particular numerical measure of parameter-space curvature. Pointwise identical predictors have identical function-based evaluation losses wherever those are defined, even though their Hessian sharpness can be made arbitrarily large under the stated conditions. This is the scope of the obstruction: it concerns the unnormalized Euclidean Hessian norm and this rescaling symmetry. It does not assert that training reaches every point on a scaling orbit or supply a numerical bound on test error. Theorem 4 and following discussion, PDF p. 6.

The completed Lean development connects an explicitly computed ReLU prediction function to its actual first and second derivatives. It provides reusable results about invariant losses, transport of local minima, and curvature under linear changes of parameters. All three published theorem statements were proved unchanged and accepted on 26 September 2026. Both milestones are complete, and the goal has no remaining open leaves.

The analytic obligations

ReLU is not differentiable at every activation boundary. The loss-level local regularity must therefore be retained rather than inferred from the network's syntax. A nonzero symmetric matrix alone is also insufficient for the sharpness claim: local minimality supplies an additional sign constraint. Finally, the second derivative is an operator on the entire parameter space; bounds for a single arbitrarily chosen scalar model do not establish the quantified network result. These are obligations of the formal proof, not hypotheses assuming the desired transformation identities.

Formalization note: scope and conventions

Parameters are represented by EuclideanSpace over the disjoint union of first-layer matrix coordinates and output-weight coordinates. This retains the sum-of-squares geometry rather than a product maximum norm. The Hessian is the derivative of the actual Fréchet derivative, represented as a continuous bilinear form. Its operator norm is the spectral norm under the Euclidean/Riesz identification. The regularity condition excludes reliance on default derivative values at nondifferentiable points.

The statement covers every positive input dimension and hidden width, arbitrary function-based losses with the specified regularity, and arbitrary qualifying minima. It imposes no separate nonzero-weight or active-neuron assumption. An input or output weight block may vanish when the loss hypotheses still hold. The nonzero-Hessian requirement is essential. Scaling by zero or a negative number is outside the claim. No probability model, random initialization, sampling measure, or training algorithm is assumed.

The mission focuses on the single-hidden-layer Hessian result. Volume flatness, the multiple-eigenvalue deep-network theorem, and other reparameterizations remain separate results in the paper. The local environment is Lean 4.30.0 with supported Mathlib revision c5ea00351c28e24afc9f0f84379aa41082b1188f.

Selected references

• Laurent Dinh, Razvan Pascanu, Samy Bengio, Yoshua Bengio. Sharp Minima Can Generalize For Deep Nets. ICML 2017, PMLR 70:1019–1028. arXiv:1703.04933v2. Primary anchors: Section 2, PDF p. 2; Section 3, PDF pp. 3–4, Definitions 3–5 and Theorem 1; Section 4.2, PDF pp. 5–6, Theorems 3–4.
• Nitish Shirish Keskar, Dheevatsa Mudigere, Jorge Nocedal, Mikhail Smelyanskiy, Ping Tak Peter Tang. On Large-Batch Training for Deep Learning: Generalization Gap and Sharp Minima. ICLR 2017. arXiv:1609.04836v2. Historical context.

Motivation

The exponential function turns addition into multiplication. When its inputs are algebraic numbers, that elementary identity meets a rigid arithmetic boundary: distinct algebraic exponents cannot produce an algebraic linear relation among their exponentials. This principle is the Lindemann–Weierstrass theorem, one of the central results of transcendence theory. Its familiar consequences include the transcendence of Euler's number $e$ and of $\pi$, and therefore the impossibility of squaring the circle with straightedge and compass.

The historical line runs from Hermite's 1873 proof that $e$ is transcendental, through Lindemann's 1882 proof that $\pi$ is transcendental, to Weierstrass's general formulation in 1885. Modern algebraic presentations organize the theorem around conjugates, Galois symmetry, algebraic integers, and an auxiliary-polynomial estimate. The Lean development formalized here follows Yuyang Zhao's mathlib contribution PR #28013, whose mathematical reference is Jacobson's Basic Algebra I, §4.12, Theorem 4.22.

Setting

A complex number is algebraic if it is a root of a nonzero polynomial with rational, equivalently integer, coefficients. A complex number is transcendental if it is not algebraic. Write $\overline{\mathbb Q}\subset\mathbb C$ for the field of algebraic complex numbers and $\exp(z)=e^z$ for the complex exponential.

For a family $(u_i)_{i\in I}$ in $\overline{\mathbb Q}$, injectivity means that distinct indices carry distinct exponents. A family $(x_i)$ is linearly independent over $\overline{\mathbb Q}$ when every finite relation $\sum_i a_i x_i=0$ with algebraic coefficients has all $a_i=0$. It is algebraically independent over $\overline{\mathbb Q}$ when no nonzero multivariate polynomial with algebraic coefficients vanishes on the family.

The strongest target uses natural-number linear independence of $(u_i)$: distinct finitely supported tuples of natural coefficients give distinct sums $\sum_i n_i u_i$. This is exactly the condition needed to distinguish the exponent attached to every monomial.

Formalization targets

Exponential linear independence

For every injective algebraic family $(u_i)$,

$$\{e^{u_i}:i\in I\}\text{ is linearly independent over }\overline{\mathbb Q}.$$

This includes the finite Lindemann–Weierstrass relation as its load-bearing finite core.

Hermite–Lindemann and classical constants

For every nonzero algebraic $a\in\mathbb C$,

$$e^a\text{ is transcendental}.$$

The same development records the transcendence of $e$, the transcendence of $\pi$, and the transcendence of every nonzero principal logarithm of an algebraic complex number.

Integer winding consumer

Let $\alpha\ne0$ be algebraic and let $w:I\to\mathbb Z$ be injective. The proved Hermite–Lindemann theorem discharges the formerly conditional winding interface and gives

$$\bigl(e^{i\alpha w(j)}\bigr)_{j\in I}\text{ linearly independent over }\overline{\mathbb Q}.$$

The integer labels are inputs to this arithmetic theorem. A separate topological or dynamical development is responsible for producing them as winding numbers.

Algebraic independence capstone

If $(u_i)$ is a natural-number-linearly-independent family in $\overline{\mathbb Q}$, then

$$\{e^{u_i}:i\in I\}\text{ is algebraically independent over }\overline{\mathbb Q}.$$

This is the mission's capstone because it turns the linear theorem into a reusable multivariate interface: polynomial monomials become exponentials of distinct natural combinations.

Significance

The theorem separates two kinds of structure that otherwise coexist in the exponential map. The character law $e^{x+y}=e^xe^y$ supplies exact multiplicative relations, but the theorem rules out unintended linear relations over algebraic coefficients. For integer winding consumers, one algebraic nonzero generator $a$ produces the two-sided phase family $(e^{na})_{n\in\mathbb Z}$; after a Laurent-polynomial shift, the theorem makes distinct integer labels linearly independent over $\overline{\mathbb Q}$. Winding supplies the discrete labels, while transcendence supplies arithmetic distinguishability.

The formalization contributes more than the named corollaries. It exposes a finite exponential-relation theorem, the algebraic orbit-sum reduction used by it, and general infinite-family interfaces. These components can be reused in later work on exponential polynomials, logarithms of algebraic numbers, and arithmetic representations of topological charges.

This mission formalizes a known theorem; it is not presented as an open mathematical problem. The private theorem graph is already machine-checked against Lean 4.30 and Mathlib revision c5ea00351c28e24afc9f0f84379aa41082b1188f. The mission records that proof as an independently inspectable dependency graph before any later upstream integration.

Difficulty

The analytic approximation alone is insufficient. It produces a small complex error, but smallness does not imply vanishing, and taking a field norm does not repair the gap because the other embeddings have no corresponding analytic bound. Likewise, a field automorphism of $\overline{\mathbb Q}$ cannot be moved through the complex exponential as an algebraic operation.

The formal statement therefore requires both an analytic and an arithmetic layer. The arithmetic layer must replace a hypothetical algebraic relation by a Galois-stable relation with integer data and a genuinely nonzero integer contribution. The analytic layer must then make the absolute value of that integer strictly less than one. Managing conjugacy classes, root multisets, denominator clearing, finite supports, and the asymptotic prime choice in one kernel-checked chain is the central formalization difficulty.

Formalization scope

The development is pinned to Lean 4.30 and Mathlib revision c5ea00351c28e24afc9f0f84379aa41082b1188f. Algebraic complex numbers are represented by integralClosure ℚ ℂ; transcendence corollaries are stated with Transcendental ℤ, which is equivalent to the usual absence of a nonzero integer polynomial relation. The finite theorem uses Fintype; the general linear and algebraic independence theorems permit arbitrary universe-zero index types and reduce relations to finite support internally.

The auxiliary algebraic theorem is stated over an arbitrary algebraically closed field over $\mathbb Q$ and a multiplicative character on its additive group. The analytic consumer specializes this character to the complex exponential. Two small support modules provide quotient lifting for finitely supported functions and evaluation identities for symmetric multivariate polynomials.

The condition $a\ne0$ in Hermite–Lindemann is load-bearing: $e^0=1$ is algebraic. Injectivity of the exponent family is load-bearing for linear independence: duplicate exponents duplicate vectors. The capstone's natural-number linear independence is not algebraic independence of the exponents and must not be silently strengthened or weakened.

The source is an attributed, compatibility-preserving port of the May 2026 Lean 4.30 snapshot of mathlib PR #28013. Platform packaging uses the conservative ASCII rename linearIndependent_exp_finite for the upstream private helper and phi for one Greek binder. The elaborated theorem types were compared against the upstream source; these are naming changes only.

Selected references

• Yuyang Zhao, The Lindemann–Weierstrass theorem, mathlib4 PR #28013, 2022–2026. https://github.com/leanprover-community/mathlib4/pull/28013
• Nathan Jacobson, Basic Algebra I, 2nd edition, W. H. Freeman, 1985, §4.12, Theorem 4.22.
• Mathlib contributors, AnalyticalPart: the analytic estimate for Lindemann–Weierstrass. https://leanprover-community.github.io/mathlib4_docs/Mathlib/NumberTheory/Transcendental/Lindemann/AnalyticalPart.html

Motivation

Essentially every quantitative model written as a rate of change — a mechanical system, a chemical reaction network, a population model, a control loop — is an ordinary differential equation (ODE) together with an initial condition. Before anything can be computed about such a model, two questions must be settled: does a solution through the given initial state exist, and is it the only one? The classical answer is the Picard–Lindelöf theorem: a Lipschitz right-hand side yields a unique local solution. Uniqueness is not a technicality — it is what licenses speaking of the trajectory through a point, hence of a flow, and so it underwrites the entire qualitative theory of dynamical systems that the source text builds afterwards (vector fields, tubular flow, $\omega$-limit sets, Poincaré–Bendixson, Grobman–Hartman, stable manifolds).

This mission is the first in a series formalizing Augusto Armando de Castro Júnior's lecture notes Curso de Equações Diferenciais Ordinárias (2009), a graduate ODE course that develops the theory directly in Banach spaces, not only in $\mathbb R^n$. The book proves existence and uniqueness once, in that general setting, and then reuses it throughout; this mission formalizes that foundation.

Setting

Let $E$ be a real Banach space, $t_0 \in \mathbb R$, $x_0 \in E$, and $a, b > 0$. Write $\bar B(x_0,b) = \{x \in E : \|x - x_0\| \le b\}$ for the closed ball and

$$U \;=\; [t_0-a,\,t_0+a] \times \bar B(x_0,b) \;\subset\; \mathbb R \times E .$$

A map $f : U \to E$ is Lipschitz with respect to the second variable with constant $c>0$ if

$$\|f(z,y_1) - f(z,y_2)\| \;\le\; c\,\|y_1-y_2\| \qquad\text{whenever } (z,y_1),(z,y_2)\in U ,$$

the same $c$ serving for every $z$ (Definição 2.1.1 of the source).

Given $f$, the Cauchy problem (initial value problem) with initial data $(t_0,x_0)$ asks for a curve $\varphi : I \to E$, defined on a nondegenerate interval $I \ni t_0$, such that $(t,\varphi(t)) \in U$ for all $t \in I$, $\varphi(t_0)=x_0$, and $\varphi'(t) = f(t,\varphi(t))$ for all $t \in I$ — one-sided derivatives at the endpoints of $I$ (Definições 1.0.1 and 1.1.1). Equivalently, by the Fundamental Theorem of Calculus, $\varphi$ is continuous with graph in $U$ and satisfies the integral equation

$$\varphi(t) \;=\; x_0 + \int_{t_0}^{t} f\bigl(s,\varphi(s)\bigr)\,ds , \qquad t \in I .$$

Finally, put $M = \sup\{\|f(t,x)\| : (t,x) \in U\}$ and $\alpha = \min\{a,\ b/M\}$.

Target

The goal theorem is Teorema 2.1.2 (Picard) of the source: if $f : U \to E$ is continuous, bounded, and Lipschitz in the second variable, then the Cauchy problem $x' = f(t,x)$, $x(t_0)=x_0$ has a solution on $[t_0-\alpha,\,t_0+\alpha]$, and any two solutions on that interval whose graphs stay in $U$ coincide there:

$$\exists\,\varphi \ \text{solution on } [t_0-\alpha,t_0+\alpha], \qquad \forall\,\psi \ \text{solution on } [t_0-\alpha,t_0+\alpha]: \ \varphi = \psi \ \text{on } [t_0-\alpha,t_0+\alpha].$$

The milestones are the results the source uses to get there, in its own order: the contraction fixed point theorem (Teorema 0.2.10), the equivalence between the Cauchy problem and the integral equation (Capítulo 2, opening paragraphs), the sufficient condition for Lipschitz dependence via a bounded partial derivative (Proposição 2.1.4), and the global version on a whole interval (Corolário 2.1.3).

Significance

Picard's theorem is what makes the initial value problem well posed in the sense of Hadamard's first two requirements. Downstream in the same book it is the hypothesis behind maximal solutions and the escape-from-compacts property (§2.3), continuous and differentiable dependence on initial conditions and parameters (Chapter 3), and the local flow of a vector field (Chapter 4). Without uniqueness none of these statements can even be phrased.

As for formalization status: Mathlib already contains a Picard–Lindelöf development (IsPicardLindelof, ODE_solution_unique and relatives) and a Banach fixed point theorem (ContractingWith.exists_fixedPoint). The work this mission asks for is therefore not the discovery of a proof but a faithful bridge: stating the source's hypotheses as the source states them — a closed ball, a supremum bound $M$, the radius $\alpha=\min\{a,b/M\}$, Lipschitz in the second variable with one constant for all times, uniqueness among solutions whose graph stays in the domain — and deriving them from, or proving them alongside, the library's own formulation. Such bridges are where unfaithful formalizations usually hide, and they are reusable by every later mission in the series.

Difficulty

The obvious route is "cite the library and close the goal". It does not go through unchanged, for three reasons. First, the hypothesis shapes differ: the library packages its assumptions in a structure with its own choice of ball, bound and time radius, and matching $\alpha=\min\{a,b/M\}$ with a supremum-defined $M$ requires the boundedness argument to be redone at the interface. Second, uniqueness here is asserted for solutions in the sense of this mission's definition — derivative within the interval, one-sided at the two endpoints, graph inside $U$ — so a Grönwall-type uniqueness statement must be transported to that formulation, including the endpoint cases. Third, the source works with an arbitrary Banach space $E$ and only assumes $f$ bounded, rather than assuming finite dimension; compactness arguments are unavailable by design.

The remaining genuine mathematical content sits in the milestones: the iterate estimate $\|F^m(\varphi_1)-F^m(\varphi_2)\| \le \frac{c^m\alpha^m}{m!}\,\|\varphi_1-\varphi_2\|$ used by the source to make some iterate of the Picard operator a contraction, and the mean value inequality on a convex open set behind Proposição 2.1.4.

Formalization scope

Conventions this proposal fixes, all visible in the definitions item:

1. Solutions are total functions $\mathbb R \to E$ whose behaviour is constrained only on the interval $I$; uniqueness is therefore stated as agreement on $I$, never as equality of functions.
2. Differentiability is the derivative relative to $I$, which is exactly the source's convention of lateral derivatives at endpoints.
3. The ball $\bar B(x_0,b)$ is closed — the source's proof needs the function space $C^0([t_0-\alpha,t_0+\alpha], \bar B(x_0,b))$ to be a closed subset of $C^0$.
4. $M$ is a least upper bound of $\{\|f(t,x)\| : (t,x)\in U\}$, which encodes both the boundedness hypothesis and the definition of $M$; the extra hypothesis $M > 0$ is stated explicitly because the quotient $b/M$ is otherwise a junk value.
5. The Lipschitz constant $c$ is an explicit parameter with $c>0$, the same for all times, as in Definição 2.1.1.
6. Vacuity is ruled out: the hypotheses are satisfiable — for instance by a nonzero constant $f$ — so the goal is not true by default.

A complete development needs the Bochner and interval integrals, the contraction mapping API, the mean value inequality for Fréchet derivatives, and the ODE files. Contributions of independent interest to the series: the Picard iterate factorial estimate, and the conversion between the library's Picard–Lindelöf hypotheses and the ones above.

Selected references

• A. A. de Castro Júnior, Curso de Equações Diferenciais Ordinárias, lecture notes, 6 January 2009. Teorema 0.2.10 (p. 10), Definição 1.1.1 (p. 34), Definição 2.1.1 (p. 43), Teorema 2.1.2 (p. 44), Corolário 2.1.3 (p. 46), Proposição 2.1.4 (p. 47).
• E. Lindelöf, Sur l'application de la méthode des approximations successives aux équations différentielles ordinaires du premier ordre, C. R. Acad. Sci. Paris 114 (1894), 454–457.
• Mathlib 4, Mathlib/Analysis/ODE/PicardLindelof.lean and Mathlib/Analysis/ODE/Gronwall.lean, https://github.com/leanprover-community/mathlib4.

Motivation: approximating entire continuous functions

An approximation result must specify both the allowed approximants and the error being controlled. Matching finitely many values is different from approximating a function everywhere with one error bound. Polynomial approximation on a closed interval provides a model: finitely described functions can approach an arbitrary continuous function uniformly, without assuming that the function has derivatives or a convergent power-series expansion. Lebl, Theorem 11.7.1.

The broader question replaces polynomials with a collection of continuous functions closed under algebraic operations. The relevant issue is which properties of that collection guarantee approximation of every continuous function. This distinguishes a useful approximation family from one that cannot detect some points or cannot approximate nonzero values at a particular point. The six targets follow the real and complex approximation results in §11.7 of Jiří Lebl’s Basic Analysis, Volume II. Source section.

Setting: function algebras and uniform error

A metric space is a set $X$ with a nonnegative, symmetric distance $d(x,y)$ that vanishes exactly when $x=y$ and satisfies the triangle inequality. It is compact if every cover by open sets has a finite subcover. Let $K$ be either the real numbers $\mathbb R$ or the complex numbers $\mathbb C$, and write $C(X,K)$ for the continuous functions from $X$ to $K$. Products, sums, and scalar multiplication of functions are taken pointwise. The notation $K[t]$ denotes polynomials in one indeterminate $t$ with coefficients in $K$, and $[a,b]=\{x\in\mathbb R:a\le x\le b\}$ for real endpoints $a,b$.

A non-unital function algebra $A$ contains the zero function and is closed under these three operations. It need not contain the constant function $1$. It separates points if, whenever $x\ne y$, some $g\in A$ satisfies $g(x)\ne g(y)$. It vanishes nowhere if, for each $x$, some $g\in A$ satisfies $g(x)\ne0$. The witness may depend on $x$; one everywhere nonzero function is not specified. A complex algebra is self-adjoint if it contains the pointwise complex conjugate of every member. These conventions retain the source’s non-unital setting. Lebl, Definitions 11.7.5, 11.7.7, and 11.7.15.

Uniform convergence of $f_n$ to $f$ means

$$\forall\varepsilon>0\;\exists N\in\mathbb N\;\forall n\ge N\;\forall x\in X, \qquad |f_n(x)-f(x)|<\varepsilon.$$

Here $|\cdot|$ is real absolute value or complex modulus. On compact $X$, the closure $\overline A$ in $C(X,K)$ uses this uniform topology; saying that $A$ is dense means $\overline A=C(X,K)$. Mathlib’s compact-domain convergence interface.

Formalization targets

The first four statements supply approximation, normalization, closure, and interpolation results. The final two state density, with the complex result as the goal. No approximation rate or degree bound is prescribed.

Theorem 11.7.1. For $K=\mathbb R$ and for $K=\mathbb C$, respectively,

$$f\in C([a,b],K)\Longrightarrow \exists(p_n)_{n\in\mathbb N}\subseteq K[t],\qquad p_n\longrightarrow f\ \text{uniformly on }[a,b].$$

The real clause requires real coefficients. Complex polynomials are evaluated at the complex embedding of the real argument. Source theorem.

Corollary 11.7.4. For $a\ge0$,

$$\exists(p_n)\subseteq\mathbb R[t],\qquad (\forall n,\ p_n(0)=0)\ \land\ p_n\longrightarrow |\cdot|\ \text{uniformly on }[-a,a].$$

Source corollary.

Proposition 11.7.6. For compact metric $X$ and either scalar field,

$$A\text{ a non-unital algebra in }C(X,K) \Longrightarrow\overline A\text{ is such an algebra}.$$

Source proposition.

Proposition 11.7.11. For an arbitrary set $X$, without topology, let $A\subseteq K^X$ be an algebra separating points and vanishing nowhere. Then

$$\forall x\ne y\;\forall c,d\in K\;\exists f\in A, \qquad f(x)=c\ \land\ f(y)=d.$$

Both scalar fields belong to this single target. Source proposition.

Theorem 11.7.12. For compact metric $X$,

$$A\subseteq C(X,\mathbb R)\text{ an algebra separating points and vanishing nowhere} \Longrightarrow\overline A=C(X,\mathbb R).$$

Source theorem.

Theorem 11.7.16, complex Stone–Weierstrass. For compact metric $X$,

$$\begin{gathered} A\subseteq C(X,\mathbb C)\text{ a self-adjoint algebra},\\ A\text{ separates points and vanishes nowhere} \end{gathered} \Longrightarrow\overline A=C(X,\mathbb C).$$

Source theorem.

Significance: density without an assumed unit

The density conclusion turns structural conditions on an approximation family into a statement about every continuous target function. Exact interpolation only controls specified values at two points; density controls all points simultaneously to any positive tolerance. The normalized absolute-value result retains a constraint on every approximating polynomial, rather than obtaining normalization only in the limit.

These are established theorems, not open conjectures. Mathlib already has machine-checked polynomial approximation, unital Stone–Weierstrass results, and non-unital algebra infrastructure. The six source-level statements also have standalone proofs checked in the pinned Lean environment. The contribution is an explicit textbook-facing non-unital formulation, with both scalar fields and the source’s normalization and interpolation clauses retained. It is not a claim to the first formalization of Stone–Weierstrass. Polynomial approximation, Stone–Weierstrass library.

Difficulty: local distinctions do not give uniform control

Point separation alone does not say that an algebra can approximate a nonzero value everywhere it is requested. A family may distinguish pairs of points while all its members vanish at one fixed point. Nor does interpolation at a pair of points establish a uniform error bound over an entire compact domain. These are distinct quantifier requirements.

Requiring $1\in A$ would remove the source’s non-unital case instead of resolving it. Likewise, complex scalar multiplication does not itself impose closure under conjugation. The formal difficulty is to preserve all these distinctions while connecting bundled algebras, continuous maps, and uniform closure. A direct use of the library’s unital theorem has an additional hypothesis that is absent here. Library theorem hypotheses.

Formalization scope

Namespace LeblRA uses NonUnitalSubalgebra, ContinuousMap, real and complex polynomials, TendstoUniformly, and topological closure. Domains are arbitrary universe-polymorphic types, with metric and compactness structures only where the source requires them. The interpolation target has neither. Conjugation is the pointwise star operation on complex continuous maps.

The conventional algebra structure includes zero, but not an assumed unit. Empty compact spaces are allowed. Polynomial sequence indices start at zero. The interval approximation theorem permits arbitrary endpoints, including a singleton or an empty interval; the absolute-value corollary assumes $a\ge0$ and includes $a=0$. Neither finite-dimensional approximation spaces nor degree bounds are imposed. Replacing density by a finite-domain special case, adding a constant-one hypothesis, or assuming density itself would change the targets.

Reusable infrastructure includes non-unital subalgebras and their closures, polynomial evaluation, compact-domain uniform convergence, and real/complex continuous function spaces. The environment is Lean 4.29.0-rc3 with Mathlib revision 777aaa61dcd2a1258d2b4962dbe983ede4d23b2e. Source-faithful alternative proofs and reusable interfaces between these existing structures are welcome; extra alias definitions are unnecessary. Non-unital algebra structures, topological closures.

Selected references

• Jiří Lebl, Basic Analysis: Introduction to Real Analysis, Volume II, author-published open textbook, version 6.3, 2026, §11.7. Section text; edition information.
• The Mathlib community, Mathlib, Lean mathematical library, revision 777aaa61dcd2a1258d2b4962dbe983ede4d23b2e, 2026. Polynomial approximation, Stone–Weierstrass and zero-preserving continuous maps, non-unital algebra closures.

Motivation: limits of families of functions

Analysis often produces a sequence of candidate functions rather than a finished function. A useful existence theorem must say when some candidates approach a single limit everywhere with a common error bound. Ordinary boundedness is insufficient: Lebl gives bounded continuous functions on a closed interval with no uniformly convergent subsequence. The missing condition concerns how consistently the functions respond to nearby inputs. Examples 11.6.2–11.6.4.

The Arzelà–Ascoli theorem answers this question for continuous complex-valued functions on a compact metric domain. Its uses include existence questions for differential equations and compactness properties of integral operators, both discussed in the source section. These applications require control of entire functions, not merely convergence at isolated points. Differential-equation application, integral-operator application.

The four targets follow §11.6 of Jiří Lebl’s Basic Analysis, Volume II, a textbook treatment of equicontinuity and compactness for uniform convergence. Author’s book page.

Setting: pointwise control and uniform control

A metric space is a set $X$ with a distance $d(x,y)$ that is nonnegative, symmetric, vanishes exactly when $x=y$, and satisfies the triangle inequality. It is compact when every cover by open sets has a finite subcover. Here $\mathbb C$ denotes the complex numbers, $|z|$ their absolute value, and $F_n:X\to\mathbb C$ the function at index $n\in\mathbb N$. Write $C(X,\mathbb C)$ for the continuous functions.

The sequence is pointwise bounded if each input has its own bound, and uniformly bounded if one bound works for every input and index:

$$\forall x\in X\;\exists M_x\in\mathbb R\;\forall n\in\mathbb N, \quad |F_n(x)|\le M_x,$$ $$\exists M\in\mathbb R\;\forall n\in\mathbb N\;\forall x\in X, \quad |F_n(x)|\le M.$$

It is uniformly equicontinuous when

$$\forall\varepsilon>0\;\exists\delta>0\;\forall x,y\in X\;\forall n\in\mathbb N, \quad d(x,y)<\delta\Longrightarrow |F_n(x)-F_n(y)|<\varepsilon.$$

Thus $\delta$ cannot depend on the function index or the points. These are the source’s distinct boundedness and common-continuity conditions. Definition 11.6.1, Definition 11.6.6.

A subsequence has the form $F_{\varphi(n)}$, where $\varphi:\mathbb N\to\mathbb N$ is strictly increasing. Pointwise convergence to $f$ means convergence to $f(x)$ separately for every $x$. Uniform convergence means that for each $\varepsilon>0$ there is one $N$ such that $|F_n(x)-f(x)|<\varepsilon$ for every $n\ge N$ and every $x$. A subset $D\subseteq X$ is dense if its closure $\overline D$ is all of $X$.

Formalization targets

The supporting targets distinguish countable domains, a necessary continuity condition, and the density property of compact metric spaces. The final target combines the hypotheses into uniform-convergence compactness; no quantitative rate is prescribed.

Proposition 11.6.5. For an arbitrary countable set $X$, without any topology or continuity assumption,

$$F_n\text{ pointwise bounded} \Longrightarrow \exists\varphi,f,\quad \varphi\text{ strictly increasing}\quad\land\quad \forall x\in X,\ F_{\varphi(n)}(x)\longrightarrow f(x).$$

Source proposition.

Proposition 11.6.7. For compact metric $X$,

$$F_n\in C(X,\mathbb C),\quad F_n\longrightarrow f\text{ uniformly} \Longrightarrow F_n\text{ uniformly equicontinuous}.$$

Source proposition.

Proposition 11.6.8. Every compact metric space satisfies

$$\exists D\subseteq X,\quad D\text{ countable}\ \land\ \overline D=X.$$

Source proposition.

Theorem 11.6.9, Arzelà–Ascoli. Suppose $X$ is compact metric, $F_n\in C(X,\mathbb C)$, and the sequence is pointwise bounded and uniformly equicontinuous. The complete conclusion is

$$\left(\exists M\in\mathbb R\;\forall n,x,\ |F_n(x)|\le M\right) \quad\land\quad \left(\exists\varphi:\mathbb N\to\mathbb N\;\exists f\in C(X,\mathbb C),\quad \varphi\text{ strictly increasing},\quad F_{\varphi(n)}\longrightarrow f\text{ uniformly}\right).$$

Both the global bound and the subsequence conclusion are required. The limit belongs to $C(X,\mathbb C)$, so its continuity is explicit. Source theorem.

Significance: a compactness criterion with explicit hypotheses

The result supplies a uniform limit under hypotheses that concern individual inputs and a shared continuity condition. It therefore identifies a usable replacement for boundedness alone in a space of functions. The distinction matters downstream: retaining only pointwise convergence would not provide a common error bound across the domain, and assuming uniform boundedness in advance would discard one of the theorem’s conclusions. Lebl, Theorem 11.6.9.

These are established theorems, not open conjectures. Mathlib already contains machine-checked general Arzelà–Ascoli results, compactness and convergent-subsequence infrastructure, and the countable-dense-set interface. The four source-level statements also have ordinary local Lean proofs checked against their exact types. The contribution is a faithful textbook-facing formulation that keeps the distinct hypotheses, quantifier order, arbitrary countable domain, and both capstone conclusions visible. It is not a claim to the first formalization of Arzelà–Ascoli. Mathlib Ascoli development, countable dense subsets.

Difficulty: preserving the quantifier order

Convergence at every point does not automatically mean uniform convergence. A permissible index threshold may depend on the point, and different pointwise limits may require different subsequences. Likewise, separate continuity of every $F_n$ does not give a single $\delta$ valid for all $n$. Replacing these statements with their uniform versions silently changes the problem. Lebl’s bounded sequence $x\mapsto x^n$ on $[0,1]$ already rules out the naive implication from bounded continuous functions to a uniformly convergent subsequence. Example 11.6.3.

The formal challenge is to retain these distinctions across the representations of functions, convergence, and compactness. In particular, the countable-domain proposition must not acquire a compactness assumption, while the capstone must not acquire global bounds as an extra premise.

Formalization scope

The development uses namespace LeblRA, arbitrary universe-polymorphic domain types, Lean’s complex numbers, and zero-based natural-number indices. Zero-based indexing only reindexes the source’s sequence starting at one. A strictly increasing map is represented by StrictMono; pointwise limits use Tendsto at atTop, uniform limits use TendstoUniformly, and density uses Dense. Finite and empty domains remain allowed.

The boundedness and equicontinuity hypotheses are written as explicit quantifiers, not new custom definitions. No claim may be replaced by a finite-domain special case, a vacuous hypothesis, or a statement that assumes its uniform conclusion.

Reusable infrastructure consists of complex norms, metric and compact spaces, continuous maps, uniform convergence, equicontinuity, and sequence compactness. The pinned environment is Lean 4.29.0-rc3 with Mathlib revision 777aaa61dcd2a1258d2b4962dbe983ede4d23b2e. Source-faithful alternative proofs and explicit equivalences between the raw conditions and library predicates are welcome; applications beyond the four numbered targets are outside this scope. Uniform-convergence interface, sequence compactness.

Selected references

• Jiří Lebl, Basic Analysis: Introduction to Real Analysis, Volume II, author-published open textbook, version 6.3, 2026, §11.6. Section text; edition information.
• The Mathlib community, Mathlib, Lean mathematical library, revision 777aaa61dcd2a1258d2b4962dbe983ede4d23b2e, 2026. General Ascoli theorems, uniform convergence, topological bases and separability.