All missions

Motivation

A second-order elliptic equation in divergence form, $Lu = -\sum_{i,j}\partial_i(a_{ij}\partial_j u) = f$, is usually solved in a weak sense: the Lax–Milgram theorem or the Fredholm alternative produces a function $u \in H^1(\Omega)$, which has only first-order weak derivatives, and the equation holds after one integration by parts against every test function. The phrase "solution of a PDE" then covers objects for which the second derivatives appearing in $L$ need not exist. Regularity theory closes this gap: under smoothness of the coefficients and the data, weak solutions have exactly as many derivatives as the equation suggests. It is used throughout the calculus of variations, spectral theory and nonlinear PDE.

The interior $H^2$ estimate for divergence-form operators with $C^1$ coefficients goes back to the difference-quotient technique of L. Nirenberg (1955) and is standard in textbooks such as Evans, Partial Differential Equations, §6.3, and Gilbarg–Trudinger, Chapter 8. This mission follows the treatment in J. K. Hunter's lecture notes, §4.11 and Appendix 4.C.

Setting

Points of $\mathbb{R}^n$ are written $x = (x_1, \dots, x_n)$, and $e_i$ is the $i$th standard unit vector. Let $\Omega \subseteq \mathbb{R}^n$ be an open set. A set $\Omega'$ is compactly contained in $\Omega$, written $\Omega' \Subset \Omega$, if $\Omega'$ is nonempty and open, its closure $\overline{\Omega'}$ is compact, and $\overline{\Omega'} \subset \Omega$.

A test function is an infinitely differentiable $\phi$ with compact support inside $\Omega$ (the space $C_c^\infty(\Omega)$). A function $g$ is the weak derivative $\partial^\alpha f$ of a locally integrable $f$ (multi-index $\alpha$) if $\int_\Omega g\phi\,dx = (-1)^{|\alpha|}\int_\Omega f\,\partial^\alpha\phi\,dx$ for all test functions $\phi$. The Sobolev space $H^k(\Omega) = W^{k,2}(\Omega)$ consists of the functions whose weak derivatives of order at most $k$ exist and lie in $L^2(\Omega)$, with norm $\|u\|_{H^k(\Omega)} = (\sum_{|\alpha|\le k}\|\partial^\alpha u\|_{L^2(\Omega)}^2)^{1/2}$; more generally $W^{k,p}(\Omega)$ uses $L^p$. The space $H^1_0(\Omega)$ is the closure of $C_c^\infty(\Omega)$ in $H^1(\Omega)$.

The coefficients are functions $a_{ij}$, $1 \le i, j \le n$, which are bounded ($a_{ij} \in L^\infty(\Omega)$), symmetric ($a_{ij} = a_{ji}$) and uniformly elliptic: for some $\theta > 0$,

$$\sum_{i,j=1}^n a_{ij}(x)\xi_i\xi_j \ge \theta|\xi|^2 \quad\text{for a.e. } x \in \Omega \text{ and all } \xi \in \mathbb{R}^n.$$

Given $f \in L^2(\Omega)$, a function $u \in H^1(\Omega)$ is a weak solution of $Lu = f$ if

$$a(u, v) := \sum_{i,j=1}^n \int_\Omega a_{ij}\,\partial_i u\,\partial_j v\,dx = \int_\Omega f v\,dx \quad \text{for all } v \in H^1_0(\Omega).$$

No boundary condition is imposed on $u$.

For $h \ne 0$ the $i$th difference quotient of $u : \mathbb{R}^n \to \mathbb{R}$ is $D_i^h u(x) = (u(x + he_i) - u(x))/h$, and $D^h u = (D_1^h u, \dots, D_n^h u)$ with pointwise length $|D^h u| = (\sum_i (D_i^h u)^2)^{1/2}$.

Formalization targets

Goal: interior $H^2$ regularity (Theorem 4.27)

If moreover $a_{ij} \in C^1(\Omega)$, then for every $\Omega' \Subset \Omega$ there is a constant $C$, depending only on $n$, $\Omega'$, $\Omega$ and the coefficients, such that every weak solution $u$ of $Lu = f$ with $f \in L^2(\Omega)$ satisfies $u \in H^2(\Omega')$ and

$$\|u\|_{H^2(\Omega')} \le C\big(\|f\|_{L^2(\Omega)} + \|u\|_{L^2(\Omega)}\big).$$

Milestones: difference quotients (Appendix 4.C)

• Proposition 4.52 (1): if $u$ and its weak derivative $\partial_i u$ are locally integrable on $\mathbb{R}^n$, then $\partial_i D_j^h u = D_j^h\partial_i u$.
• Proposition 4.52 (2): for $u \in L^p(\mathbb{R}^n)$, $v \in L^{p'}(\mathbb{R}^n)$, $1 \le p \le \infty$, $\int (D_i^h u)\,v\,dx = -\int u\,(D_i^{-h}v)\,dx$.
• Theorem 4.53 (1): with $d = \operatorname{dist}(\Omega', \partial\Omega)$, $1 \le p < \infty$ and $0 < |h| < d$, $\|D_i^h u\|_{L^p(\Omega')} \le \|\partial_i u\|_{L^p(\Omega)}$ for each $i$.
• Theorem 4.53 (2): if $u \in L^p(\Omega)$, $1 < p < \infty$, and $\|D^h u\|_{L^p(\Omega')} \le C$ for all $0 < |h| < d/2$, then $u \in W^{1,p}(\Omega')$ and $\|Du\|_{L^p(\Omega')} \le C$.

Stronger targets

• Theorem 4.28: if $a_{ij} \in C^{k+1}(\Omega)$ and $f \in H^k(\Omega)$, then $u \in H^{k+2}(\Omega')$ with $\|u\|_{H^{k+2}(\Omega')} \le C(\|f\|_{H^k(\Omega)} + \|u\|_{L^2(\Omega)})$, $C$ depending only on $n, k, \Omega', \Omega$ and the coefficients.
• Corollary 4.29: if $a_{ij}, f \in C^\infty(\Omega)$, then $u$ agrees a.e. in $\Omega$ with a $C^\infty(\Omega)$ function.

Significance

The goal theorem shows that weak solutions of divergence-form equations with $C^1$ coefficients are strong solutions: their second weak derivatives are square integrable on compact subsets, so the equation $Lu = f$ holds pointwise almost everywhere. The iterated version (Theorem 4.28) and its corollary turn the existence theory for weak solutions into existence of smooth solutions whenever the coefficients and data are smooth; in combination with Sobolev embedding this is how one proves that eigenfunctions of the Dirichlet Laplacian on an open set are smooth in its interior.

All of these results are classical and fully proved in the literature. To the best of the platform's records, none is formalized: Mathlib has Lebesgue spaces, Fréchet derivatives and Hilbert-space tools, but neither weak derivatives nor Sobolev spaces on open sets, and there is no elliptic regularity result in any proof assistant known to the maintainers. A complete development would therefore also deliver reusable infrastructure: weak derivatives, $W^{k,p}(\Omega)$ and its norm, difference quotients and their calculus, and cut-off functions subordinate to $\Omega' \Subset \Omega$.

Difficulty

The formal computation behind the estimate — testing the equation against $-\partial_k(\eta^2\partial_k u)$ for a cut-off $\eta$ and using ellipticity — is illegitimate for a weak solution, because the test function involves second derivatives of $u$ that are not yet known to exist. Replacing derivatives by difference quotients makes every step meaningful but requires a separate theory: commuting difference quotients with weak derivatives, a discrete product rule and integration by parts, and a compactness argument in $L^p$ (reflexivity) that turns an $h$-uniform bound into a weak derivative. The error terms involve difference quotients of the coefficients, which is where $a_{ij} \in C^1$ enters, and the final estimate has to be closed with a Cauchy inequality and a second localization to replace $\|u\|_{H^1}$ by $\|u\|_{L^2}$.

Formalization scope

Space is $\mathbb{R}^n$ = EuclideanSpace ℝ (Fin n) with Lebesgue measure volume; coordinates are 0-based (i : Fin n), so the book's $e_1, \dots, e_n$ are EuclideanSpace.single 0 1, …. Functions are real-valued on all of $\mathbb{R}^n$ and only their values on the relevant open set matter. Weak derivatives (HasWeakDeriv, weakDeriv), $W^{k,p}(\Omega)$ (MemW), its norm (sobolevNorm, valued in ℝ≥0∞) and $W^{k,p}_0(\Omega)$ (MemW0) are defined in the mission; weakDeriv is a chosen representative and is only used under hypotheses guaranteeing existence. Exponents are p : ℝ≥0∞; conjugate exponents use ENNReal.HolderConjugate. $C^k(\Omega)$ and $C^\infty(\Omega)$ are ContDiffOn ℝ k and ContDiffOn ℝ ∞ on $\Omega$ (smooth, not analytic); "$u \in C^\infty(\Omega)$" for a Sobolev function means a.e. equality on $\Omega$ with such a function.

Conventions committed to:

• The standing assumptions of §4.6 on the operator — $a_{ij} \in L^\infty(\Omega)$, $a_{ij} = a_{ji}$, uniform ellipticity — are explicit hypotheses of Theorems 4.27–4.29, and $f \in L^2(\Omega)$ (the setting (4.34)) is a hypothesis of Corollary 4.29.
• Theorem 4.27 assumes $a_{ij} \in C^1(\Omega)$ as printed, not $C^1(\overline{\Omega})$.
• Constants: ∃ C : ℝ is quantified after $\Omega$, the coefficients, the ellipticity constant and $\Omega'$ (and $k$), and before $f$ and $u$.
• $\operatorname{dist}(\Omega', \partial\Omega)$ in Theorem 4.53 is modelled by any $d > 0$ with $B(x, d) \subseteq \Omega$ for all $x \in \Omega'$; the largest such $d$ is the book's distance (and $+\infty$ when $\Omega = \mathbb{R}^n$), so this is the book's condition and avoids Lean's convention that the distance to the empty set is $0$.
• Two corrections of the printed statements: Proposition 4.52 (2) is stated with $D_i^{-h}v$ on the right, as the book's proof derives; Theorem 4.53 (1) is stated componentwise, $\|D_i^h u\|_{L^p(\Omega')} \le \|\partial_i u\|_{L^p(\Omega)}$, which is what its proof establishes and what the proof of Theorem 4.27 uses (the printed vector form with Euclidean lengths fails for large $p$, e.g. for $u = \max(x_1, x_2)$).

The theorems are not trivialized by junk values: the difference quotient is only used at $h \ne 0$, the weak formulation's Bochner integrals are integrable under the stated $L^\infty$ and $L^2$ hypotheses, and the conclusion $u \in H^2(\Omega')$ asserts existence of all weak derivatives of order at most two, not merely a bound on a norm that could be computed from junk representatives.

Contributions welcome: a library of weak derivatives and Sobolev spaces on open subsets of $\mathbb{R}^n$ compatible with these definitions, cut-off functions for $\Omega' \Subset \Omega$ (Mathlib's ContDiffBump and exists_smooth_tsupport_subset are natural starting points), and Banach–Alaoglu for $L^p$, $1 < p < \infty$.

Selected references

• J. K. Hunter, Notes on Partial Differential Equations, UC Davis lecture notes, revised 6/18/2014, §4.11 and Appendix 4.C. https://www.math.ucdavis.edu/~hunter/pdes/pde_notes.pdf
• L. C. Evans, Partial Differential Equations, 2nd ed., Graduate Studies in Mathematics 19, American Mathematical Society, 2010, §5.8.2 and §6.3. https://doi.org/10.1090/gsm/019
• D. Gilbarg and N. S. Trudinger, Elliptic Partial Differential Equations of Second Order, Classics in Mathematics, Springer, 2001, §7.11 and §8.3. https://doi.org/10.1007/978-3-642-61798-0
• L. Nirenberg, Remarks on strongly elliptic partial differential equations, Communications on Pure and Applied Mathematics 8 (1955), 649–675. https://doi.org/10.1002/cpa.3160080414

Motivation

Algorithmic mechanism design asks for algorithms whose inputs are held by self-interested parties. Each party reports its private data, the algorithm computes an outcome, and payments are arranged so that no party gains by misreporting. Nisan and Ronen introduced the field in Algorithmic Mechanism Design (Games Econ. Behav. 35, 2001). Their running example is task scheduling on unrelated machines: $k$ tasks are distributed among $n$ machines owned by different agents, each agent knows only its own processing times, and the designer wants to minimize the make-span.

Without incentives the problem is classical: minimizing make-span on unrelated machines is NP-hard and admits a polynomial 2-approximation (Lenstra, Shmoys, Tardos, 1990). With selfish agents the question changes: which approximation ratios can a truthful mechanism guarantee? This mission formalizes the paper's upper bound, the MinWork mechanism, which is the benchmark every later lower bound for truthful scheduling is compared with.

Timeline.

• 1961: Vickrey introduces the second-price auction (J. Finance 16).
• 1971–1973: Clarke and Groves generalize it to the VCG family of truthful mechanisms for utilitarian objectives (Groves, Econometrica 41, 1973).
• 1999/2001: Nisan and Ronen show MinWork is a strongly truthful $n$-approximation, and that no truthful mechanism beats ratio 2.
• 2007: Christodoulou, Koutsoupias and Vidali raise the deterministic lower bound to $1+\sqrt2$ for $n \ge 3$; Koutsoupias and Vidali later raise it to $1+\varphi \approx 2.618$.
• 2023: Christodoulou, Koutsoupias and Kovács prove the Nisan–Ronen conjecture: no deterministic truthful mechanism achieves a ratio below $n$ (STOC 2023, arXiv:2301.11905), so MinWork is optimal among deterministic truthful mechanisms.

Setting

There are $n$ agents and $k$ tasks. Agent $i$'s type is the vector $t^i = (t^i_1,\dots,t^i_k)$ of positive times, $t^i_j > 0$ being the time agent $i$ needs to perform task $j$. A type vector is $t = (t^1,\dots,t^n)$. An allocation $x$ sends each task $j$ to one agent; $x^i$ is the set of tasks agent $i$ receives. The make-span of $x$ is

$$g(x,t) = \max_{i} \sum_{j \in x^i} t^i_j ,$$

and agent $i$'s valuation is $v^i(x,t^i) = -\sum_{j \in x^i} t^i_j$.

A direct mechanism asks every agent to declare a type, computes an allocation $x(d)$ from the declared vector $d$, and hands agent $i$ a payment $p^i(d)$. Agent $i$'s utility is $p^i(d) + v^i(x(d), t^i)$, with $t^i$ its true type. The mechanism is truthful if declaring $t^i$ maximizes agent $i$'s utility for every declaration of the others, and strongly truthful if truth-telling is the only such dominant strategy. An allocation rule is a $c$-approximation if $g(x(t),t) \le c \cdot g(y,t)$ for every type vector $t$ and every allocation $y$.

The MinWork mechanism allocates each task to an agent with minimal declared time for it, breaking ties arbitrarily. For each task it wins, an agent receives the second-best declared time $\min_{i' \ne i} d^{i'}_j$:

$$p^i(d) = \sum_{j \in x^i(d)} \min_{i' \neq i} d^{i'}_j .$$

The Lean development uses the same names: load, makespan, IsTruthful, IsStronglyTruthful, IsApprox, IsMinWorkAlloc, secondBest, minTime, minWorkPay.

Formalization targets

Goal: Theorem 4.1

For $n \ge 2$ and every MinWork allocation rule $x$ with payments $p$ as above,

$$(x,p)\ \text{is strongly truthful} \quad\text{and}\quad g(x(t),t) \le n \cdot g(y,t)\ \ \text{for all positive } t \text{ and all allocations } y .$$

Milestones

1. Theorem 3.1 (Groves): a VGC mechanism is truthful. This is an existing platform theorem, used as a reference.
2. MinWork belongs to the VGC family. Its allocation maximizes $\sum_i v^i(t^i,x)$, and its payment is $\sum_{i'\ne i} v^{i'}(t^{i'},x(t)) + h^{-i}$ with $h^{-i} = \sum_j \min_{i'\ne i} t^{i'}_j$.
3. Claim 4.2: MinWork is strongly truthful.
4. $g(x(t),t) \le \sum_{j} \min_i t^i_j$.
5. $g(y,t) \ge \frac1n \sum_j \min_i t^i_j$ for every allocation $y$.
6. Claim 4.3: MinWork is an $n$-approximation.

Significance

The theorem gives the first positive result for truthful scheduling: a mechanism that is truthful in the strongest sense and is within a factor $n$ of optimal, whatever the tie-breaking rule. Every lower bound in the paper (Theorems 4.6, 4.10 and 4.12) and in the later literature measures itself against this ratio. Since the 2023 resolution of the Nisan–Ronen conjecture, the ratio $n$ is known to be tight for deterministic truthful mechanisms.

The result is proved in the paper; it is not known to be formalized in any proof assistant. The platform already has Groves' theorem in an abstract form (AGT.vcg_incentive_compatible). This mission connects that abstract statement to a concrete combinatorial mechanism, and it adds the strict part of strong truthfulness for any number of tasks and agents, which the paper proves only for one task and two agents. The vocabulary (make-span over unrelated machines, direct scheduling mechanisms, strong truthfulness) is shared with the seven later missions of this series.

Difficulty

Truthfulness follows from Groves' theorem once MinWork is identified as a VGC mechanism. The identification requires the payment identity at every declared vector and under every tie-breaking rule, including ties at the winning time. The main difficulty is the strict part of strong truthfulness. A misreport that differs from the truth only on one task must still be shown to lose strictly for some declarations of the others. Those declarations must stay positive, and on every other task they must leave the outcome unchanged. The paper's proof covers only one task and two agents and leaves the general case as "similar". Its printed inequality also has the two utilities in the wrong order (see below), so it cannot be transcribed directly.

Formalization scope

• Agents are Fin n and tasks are Fin k. An allocation is a function Fin k → Fin n, and an agent may receive no task. Types are positive reals, and every truthfulness and approximation quantifier ranges over positive true types, positive misreports and positive declarations of the others.
• Payments are handed to the agent, so utility is the payment minus the true time spent. Payments are computed from the declared vector, never from true types.
• The allocation rule is a parameter satisfying the MinWork specification (IsMinWorkAlloc). Every result holds for every tie-breaking rule, including rules that depend on the whole declared vector. No particular argmin is fixed.
• $n \ge 2$ is a hypothesis of the goal and of the truthfulness items: with a single agent the paper's second-best minimum is undefined. The approximation items need only $n \ge 1$. There is no hypothesis on $k$.
• The make-span and both minima are Finset.sup' / Finset.inf' over nonempty finite sets, so they are true maxima and minima with no default values.
• Strong truthfulness is formalized as truthfulness plus: every misreport $d^i \ne t^i$ is strictly worse than the truth for some positive declarations of the others. Given truthfulness this is equivalent to Definition 5. A formalization that states only that truth-telling is dominant, or proves strictness only for single-task instances, does not meet the goal. Neither does an existential ratio in place of $n$.
• Printed slip: in the proof of Claim 4.2 (p. 177) the case $d^i > t^i$ reads "the utility for agent $i$ is $t^i - d^i < 0$, instead of 0 in the case of truth-telling". With the Definition 11 payments the misreporting agent loses the task (utility 0), and the truthful agent wins it with utility $d^{3-i} - t^i > 0$. The milestone text keeps the paper's words; the Lean statements assert what the argument establishes.
• Out of scope: running time ("polynomial time"), and the paper's general revelation-principle framework (Proposition 2.1).
• Welcome contributions: proofs of the milestones, and a reusable lemma connecting the local VGC milestone to AGT.vcg_incentive_compatible.

Selected references

• N. Nisan, A. Ronen, Algorithmic Mechanism Design, Games and Economic Behavior 35 (2001) 166–196. https://doi.org/10.1006/game.1999.0790
• T. Groves, Incentives in Teams, Econometrica 41 (1973) 617–631. https://doi.org/10.2307/1914085
• W. Vickrey, Counterspeculation, Auctions, and Competitive Sealed Tenders, Journal of Finance 16 (1961) 8–37. https://doi.org/10.1111/j.1540-6261.1961.tb02789.x
• J. K. Lenstra, D. B. Shmoys, É. Tardos, Approximation algorithms for scheduling unrelated parallel machines, Mathematical Programming 46 (1990) 259–271. https://doi.org/10.1007/BF01585745
• G. Christodoulou, E. Koutsoupias, A. Kovács, A Proof of the Nisan-Ronen Conjecture, STOC 2023. https://arxiv.org/abs/2301.11905

Motivation

Hilbert's Nullstellensatz ("theorem of zeros") is the basic link between algebra and geometry. It was proved by David Hilbert in his second major paper on invariant theory in 1893, after his 1890 paper that proved the basis theorem, and it is a foundational result of algebraic geometry. It gives an algebraic criterion for when a system of polynomial equations over an algebraically closed field has a solution, and an algebraic criterion for when one polynomial vanishes wherever a given family does. Every dictionary between affine varieties and ideals — points and maximal ideals, algebraic sets and radical ideals, irreducible sets and prime ideals — is a consequence.

This mission follows the Wikipedia article Hilbert's Nullstellensatz (snapshot of 27 September 2026): its introduction, its section Formulations, the statement of Zariski's lemma from Proofs, and the first theorem of Generalizations (finitely generated algebras over Jacobson rings).

Setting

Let $k$ be a field and $K$ an algebraically closed field extension of $k$ (every non-constant polynomial over $K$ has a root in $K$). Write $k[X_1,\dots,X_n]$ for the polynomial ring in $n$ variables. A point is an $n$-tuple $a = (a_1,\dots,a_n) \in K^n$, and $f(a)$ is the value of a polynomial $f$ at $a$.

• For an ideal $J$, the algebraic set (zero locus) is $\mathrm V(J) = \{a \in K^n : f(a) = 0 \text{ for all } f \in J\}$.
• For $U \subseteq K^n$, the vanishing ideal is $\mathrm I(U) = \{p : p(a) = 0 \text{ for all } a \in U\}$.
• The radical of $J$ is $\sqrt J = \{p : p^r \in J \text{ for some } r \in \mathbb N\}$.
• For $a \in K^n$, $\mathfrak m_a = (X_1 - a_1, \dots, X_n - a_n)$ is the ideal of the point.
• A subset $W \subseteq K^n$ is irreducible (Zariski topology) if it is nonempty and is not covered by two algebraic sets without lying in one of them.
• A commutative ring is Jacobson if every radical ideal is an intersection of maximal ideals.

Formalization targets

Goal: the Nullstellensatz

If $p \in k[X_1,\dots,X_n]$ vanishes on $\mathrm V(J) \subseteq K^n$, then

$$\exists\, r \in \mathbb N,\qquad p^r \in J.$$

This is the statement of the article's section Formulations, with the coefficient field $k$ and the algebraically closed field $K$ allowed to differ.

Milestones

1. Systems of equations. Over algebraically closed $K$: a system $f_1 = \dots = f_m = 0$ has no solution in $K^n$ iff $g_1 f_1 + \dots + g_m f_m = 1$ for some $g_i$; and $f$ vanishes on all solutions iff $f^r = g_1 f_1 + \dots + g_m f_m$ for some $r$ and $g_i$.
2. Geometric form. $\mathrm I(\mathrm V(J)) = \sqrt J$.
3. Weak Nullstellensatz. A proper ideal of $k[X_1,\dots,X_n]$ has a common zero in $K^n$; algebraic closedness is needed, as $(X^2+1) \subseteq \mathbb R[X]$ shows; for $K = \mathbb C$, $n = 1$ this is the fundamental theorem of algebra: $P$ has a complex root iff $\deg P \ne 0$.
4. Correspondences. $\mathrm V$ is an order-reversing bijection from radical ideals onto algebraic sets, with inverse $\mathrm I$; $\mathrm I(\{a\}) = \mathfrak m_a$ is maximal; every maximal ideal of $K[X_1,\dots,X_n]$ is some $\mathfrak m_a$; an algebraic set $W$ is irreducible iff $\mathrm I(W)$ is prime.
5. Intersections. $\sqrt J = \bigcap_{\mathfrak m \supseteq J} \mathfrak m = \bigcap_{a \in \mathrm V(J)} \mathfrak m_a$.
6. Zariski's lemma. A field finitely generated as an algebra over a field $K$ is a finite extension of $K$.
7. Jacobson rings. A finitely generated algebra $S$ over a Jacobson ring $R$ is Jacobson, and for a maximal ideal $\mathfrak n \subseteq S$, $\mathfrak n \cap R$ is maximal and $S/\mathfrak n$ is finite over $R/(\mathfrak n \cap R)$.

Significance

The Nullstellensatz makes the zero sets of polynomial systems accessible through ideals: solvability of a system becomes the ideal-membership question $1 \in J$, and the geometry of algebraic sets becomes the algebra of radical ideals. Consequences include the identification of the points of $K^n$ with the maximal ideals of $K[X_1,\dots,X_n]$, the description of irreducible algebraic sets by prime ideals, and the reduction of the fundamental theorem of algebra to the case $n=1$. The Jacobson-ring version extends the first equality of the intersection formula to every finitely generated algebra over a field.

All statements here are classical and proved. Mathlib already contains versions of several of them in its own vocabulary (Jacobson rings, Zariski's lemma, and a Nullstellensatz over an algebraically closed coefficient field). What this mission adds is a single set of statements matching the article's formulations: the version with separate fields $k \subseteq K$, the explicit systems-of-equations form, the point-ideal and irreducibility correspondences over $K^n$, and the intersection formula — and, for solvers, the bridges from these concrete statements to Mathlib's abstract ones.

Difficulty

The inclusion $\sqrt J \subseteq \mathrm I(\mathrm V(J))$ is immediate; the content is the reverse inclusion, which requires producing a point of $K^n$ from purely algebraic data. When $k \ne K$ the ideal $J$ lives over $k$ while the points live over $K$, so a result stated only for $K[X_1,\dots,X_n]$ does not apply directly: an ideal of $k[X]$ must be related to the ideal it generates in $K[X]$ without losing membership information. For the correspondences, the explicit ideals $\mathfrak m_a$ and the closed-set definition of irreducibility must be matched with the abstract notions (maximal spectrum, irreducible closed subsets) used in the library.

Formalization scope

• Points of $K^n$ are functions $\mathrm{Fin}\,n \to K$; polynomials are MvPolynomial (Fin n) k. When $k \ne K$, $K$ is a $k$-algebra and evaluation of a polynomial over $k$ at a point of $K^n$ goes through $k \to K$.
• $n = 0$ is allowed throughout; so is the unit ideal $J = k[X]$, where $\mathrm V(J) = \emptyset$ and empty intersections of ideals are the whole ring.
• Irreducibility is stated through closed sets (algebraic sets) without putting a topology on $K^n$. The degree in the $n=1$ statement is Mathlib's Polynomial.degree, with $\deg 0 = -\infty$.
• In the goal, the exponent $r$ may be $0$; that witness only works when $J$ is the unit ideal, so it does not trivialize the statement.
• Out of scope: the proofs via resultants and Gröbner bases, the effective Nullstellensatz, Lang's infinite-variable version, the scheme-theoretic generalizations, and the projective and analytic Nullstellensätze.
• Reusable output: the definitions $\mathrm V$, $\mathrm I$, algebraic set, irreducible set and $\mathfrak m_a$, and bridges to Mathlib's MvPolynomial.zeroLocus, MvPolynomial.vanishingIdeal, and IsJacobsonRing.

Selected references

• D. Hilbert, Ueber die vollen Invariantensysteme, Mathematische Annalen 42 (1893).
• Wikipedia contributors, Hilbert's Nullstellensatz. https://en.wikipedia.org/wiki/Hilbert%27s_Nullstellensatz
• M. F. Atiyah, I. G. Macdonald, Introduction to Commutative Algebra, Addison-Wesley, 1969, Chapters 5 and 7.
• D. Eisenbud, Commutative Algebra with a View Toward Algebraic Geometry, Springer GTM 150, 1995, Chapter 4.

Motivation

Caching (online paging) is one of the oldest problems in online algorithms: a fast memory of $k$ slots serves a sequence of requests, and every request for an element not in the fast memory is a cache miss that forces the element to be loaded, possibly evicting another one. With the whole request sequence known in advance, evicting the element whose next request is furthest in the future is optimal (Bélády, 1966). Without that knowledge, no deterministic algorithm is better than $k$-competitive, and the best randomized algorithms are $\Theta(\log k)$-competitive (Fiat, Karp, Luby, McGeoch, Sleator and Young, 1991).

Lykouris and Vassilvitskii asked what happens in between: an online algorithm receives, with every request, a machine-learned prediction of the element's next arrival time. A good predictor should make the algorithm nearly as good as Bélády's rule (consistency), and a bad predictor should never make it worse than a classical algorithm (robustness). Their paper (arXiv:1802.05399v4; J. ACM 2021) is one of the founding papers of learning-augmented algorithms, and its algorithm, Predictive Marker, is the reference point for the later literature on caching with predictions.

Timeline.

• 1966: Bélády's furthest-in-future rule is optimal offline.
• 1985: Sleator and Tarjan show that deterministic online paging is at best $k$-competitive.
• 1991: Fiat et al. introduce the Marker algorithm, $2H_k$-competitive, and the clean-element lower bound on the optimum.
• 2018: Lykouris and Vassilvitskii (arXiv:1802.05399) introduce Predictive Marker, with ratio $2\min(1+2S_\ell(\epsilon), 2H_k)$ for an $\epsilon$-accurate predictor.
• 2020: Rohatgi (arXiv:1910.12172, SODA 2020) and Wei (arXiv:2005.13716, APPROX/RANDOM 2020) improve the dependence on the error.

Setting

A request sequence $\sigma = (z_1, \dots, z_n)$ lists elements of a set $Z$. A cache of size $k \ge 1$ starts empty. A request for a cached element is a hit; otherwise it is a miss, the element is loaded, and if the cache is full some element is evicted first. The offline optimum $\mathrm{Opt}(\sigma)$ is the least number of misses over all eviction schedules chosen with knowledge of $\sigma$.

With each request $z_i$ the algorithm receives a real prediction $h_i$. The true label $y_i$ is the position of the next request of $z_i$, or $n+1$ if there is none. For a loss function $\ell \ge 0$, the error of the predictions is $\eta_\ell(h,\sigma) = \sum_i \ell(y_i, h_i)$, and the predictions are $\epsilon$-accurate when $\eta_\ell(h,\sigma) \le \epsilon \cdot \mathrm{Opt}(\sigma)$.

The spread of $\ell$ measures how cheaply a predictor can get the order of arrivals completely wrong: $S_\ell(m)$ is the least length $T \ge 1$ such that every strictly increasing integer sequence $a_1 < \dots < a_T$ and every non-increasing real sequence $b_1 \ge \dots \ge b_T$ have total loss $\sum_i \ell(a_i, b_i) \ge m$.

Predictive Marker (Algorithm 1) works in the phases of the Marker algorithm. Requested elements are marked. A phase ends when the cache is full, every cached element is marked, and a miss occurs; then all marks are removed. An element requested in a phase but not in the previous one is clean, and $Q(\sigma)$ is the total number of clean elements. Each clean miss starts a chain. An element evicted in the current phase that is requested again (a stale miss) extends the chain in which it was evicted. Evictions are among unmarked elements. As long as the chain's length $n(r,c)$ is at most $H_k = 1 + \tfrac12 + \dots + \tfrac1k$, the evicted element is one with the largest prediction. After that it is chosen uniformly at random. The expected number of misses of Predictive Marker is $\mathrm{cost}_{PM}(\sigma)$.

Formalization targets

Goal: Theorem 3.3

If $S$ is concave on $[0,\infty)$ and majorizes the spread, then for every $\epsilon \ge 0$, every tie-breaking rule, and every sequence with $\epsilon$-accurate predictions,

$$\mathbb E\bigl[\mathrm{cost}_{PM}(\sigma)\bigr] \le 2\cdot\min\bigl(1 + 2S(\epsilon),\ 2H_k\bigr)\cdot \mathrm{Opt}(\sigma).$$

Milestones

• Claim 1 (Fiat et al.): $Q(\sigma) \le 2\,\mathrm{Opt}(\sigma)$.
• Proof of Theorem 3.3, last sentence: $\mathrm{Opt}(\sigma) \le Q(\sigma)$.
• Lemma 3.3: a chain that evicts by the predictions only has length $n(r,c) \le 1 + S(\eta_{r,c})$, where $\eta_{r,c}$ is the error of the predictions on the elements evicted into it.
• Lemma 3.4: $\mathbb E[n(r,c)] \le \mathbb E[\min(1 + 2S(\eta_{r,c}), 2H_k)]$.

Significance

The result. Theorem 3.3 gives both guarantees at once. For an exact predictor ($\epsilon = 0$) the ratio is a constant, $2(1 + 2S(0))$, independent of $k$; for an arbitrary predictor it is $4H_k$, within a constant factor of the optimal randomized ratio. In between, the ratio degrades with the error at the rate of the spread: for the absolute loss the spread grows like $\sqrt m$, so the ratio grows like $\sqrt\epsilon$. The spread and the chain decomposition are the tools later papers build on to trade consistency against robustness.

Formalizing it. The theorem is proved on paper; no machine-checked proof of it, of the Marker analysis, or of the clean-element bound of Fiat et al. is known. A formalization supplies a precise model of a randomized online algorithm with predictions. It also settles the details the paper leaves implicit: the eviction missing from the clean branch of Algorithm 1 as printed, the cap $2H_k$ printed as $2\log k$ in Lemma 3.4, and the behaviour of the spread at $0$.

Difficulty

The obvious argument charges every miss to a chain and bounds each chain separately. That works for chains that follow the predictions, but a chain that switches to random evictions interacts with every other chain of the phase, because all of them evict from the same pool of unmarked elements. A bound on its expected length must hold whatever the other chains evict, including evictions that depend on earlier coin flips. A second difficulty is summing. The chain errors $\eta_{r,c}$ and the chain lengths are both random, while the hypothesis controls only the total error $\eta_\ell(h,\sigma)$ against $\mathrm{Opt}(\sigma)$, not the number of chains $Q(\sigma)$ in which the error is spread.

Formalization scope

Elements form a type with decidable equality. A request sequence is a list; predictions are one real per request, and every real sequence is allowed. Labels are 1-based next-arrival positions, with $n+1$ for elements never requested again. The paper prints the label with equal features; the element is meant. $\mathrm{Opt}$ is computed as the minimum over all demand-paging schedules from the empty cache, which loses no generality. $H_k$ is harmonic k as a real number, never $\log k$.

Predictive Marker is a PMF over final states. The random eviction of line 21 is uniform over the unmarked cached elements, and ties in the arg max are a parameter quantified universally. The eviction of lines 23–24 is also performed after a clean miss; as printed, it sits only in the stale branch. The expected cost lies in $[0,\infty]$.

The spread takes real arguments and lengths $T \ge 1$. $S$ must be concave on $[0,\infty)$, finite, and at least the spread. It must also be continuous at $0$, which the paper does not say: without it the chain lemma fails for losses whose minimal reversed-order loss stays $0$ over several lengths. $\epsilon$-accuracy is the pointwise condition on the given pair $(\sigma, h)$. The competitive ratio is written as a product, so $\mathrm{Opt}(\sigma) = 0$ needs no special case. Lemma 3.3 is stated pointwise for chains without random evictions, as its proof shows. Lemma 3.4 has $2H_k$ in place of the printed $2\log k$, with the minimum inside the expectation because $\eta_{r,c}$ is random.

The statement must not be trivialized. $\mathrm{Opt}$ is the true offline optimum, not Bélády's rule applied to the predictions. The expectation is taken over Predictive Marker's own run, never compared with itself. The spread hypothesis is satisfiable; for example, the constant loss $1$ has spread $\max(1,\lceil m\rceil) \le m + 1$.

Out of scope: Lemma 3.2 (the special-marking algorithm SM, which enters only through Lemma 3.4's proof); Lemma 3.1 and Corollaries 1–2, whose printed constants are false for small $m$ or disagree with Theorem 3.3; the lower bounds of §3.1 and §3.4; the extensions of §4; the experiments of §5; running time and learnability.

Welcome contributions: the Marker phase structure and its equivalence with the combinatorial phases, the clean-element bounds $Q/2 \le \mathrm{Opt} \le Q$ (reusable for any marking algorithm), and a bound on the expected number of misses caused by elements evicted uniformly at random within a phase.

Selected references

• T. Lykouris, S. Vassilvitskii, Competitive Caching with Machine Learned Advice, arXiv:1802.05399v4, 2020; J. ACM 68(4), 2021. https://arxiv.org/abs/1802.05399v4
• A. Fiat, R. M. Karp, M. Luby, L. A. McGeoch, D. D. Sleator, N. E. Young, Competitive paging algorithms, J. Algorithms 12(4), 1991. https://doi.org/10.1016/0196-6774(91)90041-V
• L. A. Bélády, A study of replacement algorithms for a virtual-storage computer, IBM Systems Journal 5(2), 1966. https://doi.org/10.1147/sj.52.0078
• D. D. Sleator, R. E. Tarjan, Amortized efficiency of list update and paging rules, Comm. ACM 28(2), 1985. https://doi.org/10.1145/2786.2793
• D. Rohatgi, Near-optimal bounds for online caching with machine learned advice, SODA 2020. https://arxiv.org/abs/1910.12172
• A. Wei, Better and simpler learning-augmented online caching, APPROX/RANDOM 2020. https://arxiv.org/abs/2005.13716

Motivation

Column generation solves linear programs with far too many variables to list: one works with a small subset $J' \subseteq J$ of the columns, the restricted master problem (RMP), and adds columns of negative reduced cost as a pricing problem finds them (Lübbecke and Desrosiers 2005, §2.1). Many integer programs from vehicle routing, crew scheduling and crew pairing are reformulated so that the master problem is a set-partitioning problem: every row (a customer, a flight leg, a task) must be covered by exactly one selected column (a route, a pairing, a schedule). The linear relaxation of such a master is solved by column generation, and an integer solution is then sought by branch-and-price, branch-and-bound with column generation at every node.

Branching in branch-and-price is not free. Fixing a master variable $\lambda_j$ to $0$ does not stop the pricing problem from regenerating the same column, and handling that complicates the pricing problem. The rule that avoids this for set partitioning goes back to Ryan and Foster (1981): branch on a pair of rows, requiring them to be covered either by the same column or by two different columns. Both requirements are constraints the pricing problem can respect directly. Lübbecke and Desrosiers call it "the most common scheme in conjunction with column generation" (§7.3, p. 1020) and state the proposition that makes it well defined as their Proposition 3.

Timeline:

• 1981: Ryan and Foster introduce the pair-of-rows branching rule for set partitioning in crew scheduling.
• 1998: the branch-and-price survey of Barnhart et al. (1998) presents the rule as the branching scheme for set-partitioning masters.
• 2005: Lübbecke and Desrosiers state it as Proposition 3 of their survey, attributing it to Ryan and Foster without proof.

Setting

Rows are indexed by $\{1, \dots, m\}$ and columns by a finite set $J'$. A matrix $A = (a_{rj}) \in \{0,1\}^{m \times |J'|}$ has every entry equal to $0$ or $1$; column $j$ covers row $r$ when $a_{rj} = 1$. The set-partitioning system of the RMP's linear relaxation is

$$A\lambda = \mathbf 1, \qquad \lambda \ge \mathbf 0, \qquad \lambda \in \mathbb R^{J'} .$$

A vector $\lambda$ is a basic feasible solution of this system when it satisfies all its constraints and, among the constraints active at $\lambda$ (the $m$ equality rows, and the constraints $\lambda_j \ge 0$ with $\lambda_j = 0$), there are $|J'|$ linearly independent ones. Equivalently, $\lambda$ is feasible and the columns of $A$ in the support of $\lambda$ are linearly independent. A solution is fractional when it is not a $0/1$ vector, $\lambda \notin \{0,1\}^{|J'|}$.

For two rows $r, s$ the Ryan–Foster quantity is $\sum_{j \in J'} a_{rj} a_{sj} \lambda_j$, written pairCover A lam r s in Lean: the total weight on the columns that cover both rows. For $r = s$ it is the row sum, equal to $1$ on every feasible $\lambda$.

Formalization targets

Goal: Proposition 3 (p. 1020)

For every $0/1$ matrix $A$ and every fractional basic feasible solution $\lambda$ of $A\lambda = \mathbf 1$, $\lambda \ge \mathbf 0$,

$$\exists\, r, s \in \{1, \dots, m\}: \qquad 0 < \sum_{j \in J'} a_{rj}\, a_{sj}\, \lambda_j < 1 .$$

The two rows are automatically distinct. The statement concerns every fractional basic solution, not only an optimal one, and no cost vector enters it.

Milestone: the branches keep every integer solution (§7.3, p. 1020)

For every $0/1$ solution $\lambda \in \{0,1\}^{|J'|}$ of $A\lambda = \mathbf 1$ and every pair of rows $r, s$,

$$\sum_{j \in J'} a_{rj}\, a_{sj}\, \lambda_j \in \{0, 1\} .$$

This is the paper's requirement that "integer solutions remain intact" (p. 1019), specialised to the two branches "$= 1$" and "$= 0$" of the paragraph after Proposition 3.

Significance

Proposition 3 is what makes Ryan–Foster branching a valid branching scheme in the sense of §7.3: the current fractional solution violates both branches for the chosen pair, so it is excluded from both children, while by the milestone every integer solution survives in one of them. The same pair-of-rows idea underlies branching in bin packing, graph colouring, vehicle routing and crew scheduling codes, where it is used because both branches translate into constraints on the pricing problem rather than on individual master variables.

The paper states the result and refers its proof to Ryan and Foster (1981); no machine-checked version of the proposition is known. This mission produces a formal statement tied to a standard, representation-aware definition of basic solutions (Bertsimas–Tsitsiklis Definition 2.9, already on the platform) and, once proved, a verified lemma that any formal development of branch-and-price for set partitioning can cite.

Difficulty

An argument that uses only feasibility and a fractional coordinate cannot work. Without basicness the claim is false: with one row and two identical columns, $A = [1\ 1]$, the vector $\lambda = (\tfrac12, \tfrac12)$ is feasible and fractional, yet the only pair of rows is $r = s$, whose quantity is $1$. The difficulty is to turn basicness, a linear-algebra condition, into a combinatorial statement about which rows the fractional columns cover. A set-partitioning matrix need not have full row rank, so the familiar description of basic solutions through an invertible basis matrix is not available in general.

Formalization scope

• Rows are Fin m and columns Fin n, so $J'$ is identified with $\{0, \dots, n-1\}$. $A$ is a real matrix Matrix (Fin m) (Fin n) ℝ with the hypothesis IsZeroOneMatrix A (every entry $0$ or $1$); $\lambda$ is lam : Fin n → ℝ, since λ is a Lean keyword. Columns are $0/1$ vectors; the equivalent reading as subsets of the rows is only prose.
• "Basic solution" is not defined in the paper. It is read as Bertsimas–Tsitsiklis Definition 2.9 for the standard-form constraint family: LinearOptimization.IsBasicFeasibleSolution (LinearOptimization.stdFormSystem A (fun _ => 1)) lam, from the platform definitions BasicSolution and ActiveConstraints. This definition needs no full-row-rank assumption, which a set-partitioning matrix need not satisfy, and it is not replaced by an ad hoc support condition.
• Typo correction. The paper writes "i.e., $\lambda \notin \{0,1\}^m$". Since $\lambda$ has one coordinate per column, the statement reads it as $\lambda \notin \{0,1\}^{|J'|}$: ¬ IsZeroOneVector lam.
• The rows $r, s$ range over all of $\{1, \dots, m\}$, including $r = s$, as on the page; no distinctness is assumed or required.
• "Fractional basic solution" is any such solution, not the RMP optimum; no costs or optimality hypothesis enter.
• The milestone reads the paragraph after Proposition 3, together with the validity requirement "integer solutions remain intact" (p. 1019), as the dichotomy for all $0/1$ solutions of $A\lambda = \mathbf 1$. The sentence about transferring the branching information to the pricing problem is not formalized.
• Edge cases: for $m = 0$ basicness forces $\lambda = 0$, and for $n = 0$ the vector is empty; in both cases no fractional basic solution exists and the goal is vacuous, as on the page.
• A trivializing formalization is ruled out: dropping basicness makes the goal false (the $[1\ 1]$ example above), dropping the $0/1$ hypothesis on $A$ changes the meaning of the quantity, and replacing "fractional basic" by an unsatisfiable hypothesis would make it empty; the hypotheses are satisfied, for instance, by three rows, the columns $\{1,2\}, \{2,3\}, \{1,3\}$ and $\lambda = (\tfrac12, \tfrac12, \tfrac12)$.

A complete development needs linear-algebra facts about basic solutions of standard-form systems without a rank assumption (support columns linearly independent), which are reusable beyond this mission. Contributions welcome: that characterization as a lemma, and proofs of the milestone and of the goal.

Selected references

• M. E. Lübbecke and J. Desrosiers, Selected Topics in Column Generation, Operations Research 53(6):1007–1023, 2005. https://doi.org/10.1287/opre.1050.0234
• D. M. Ryan and B. A. Foster, An integer programming approach to scheduling, in A. Wren (ed.), Computer Scheduling of Public Transport, North-Holland, 1981, pp. 269–280.
• C. Barnhart, E. L. Johnson, G. L. Nemhauser, M. W. P. Savelsbergh and P. H. Vance, Branch-and-Price: Column Generation for Solving Huge Integer Programs, Operations Research 46(3):316–329, 1998. https://doi.org/10.1287/opre.46.3.316
• D. Bertsimas and J. N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997, Definition 2.9.

Why regular Sturm–Liouville problems

Separation of variables reduces the heat equation, the wave equation and the Schrödinger equation on an interval to an eigenvalue problem for a second-order ordinary differential operator with boundary conditions at both ends. Whether the method works depends on one fact: the eigenfunctions of that operator must be complete, so that every reasonable initial profile can be expanded in them. Chapter 5 of Gerald Teschl's Ordinary Differential Equations and Dynamical Systems (author's preliminary version of AMS GSM 140, 2012) proves this for regular Sturm–Liouville problems. It does so without Lebesgue integration or Hilbert-space completeness: it works in the space of continuous functions with a weighted scalar product, and it develops the necessary spectral theory of compact symmetric operators from scratch.

A short history. Sturm and Liouville (1836–1837) studied the zeros and the eigenvalues of such equations and the expansion of functions in eigenfunctions. Hilbert and Schmidt (1904–1907) put the expansion on a rigorous footing through their theory of integral equations with symmetric kernels, from which the abstract spectral theorem for compact symmetric operators emerged.

Setting

Let $a < b$ and let $p, q, r$ be real functions on $[a,b]$ with

$$r, q \in C([a,b], \mathbb{R}), \qquad p \in C^1([a,b], \mathbb{R}), \qquad p(x) > 0,\ r(x) > 0 \ \ (x \in [a,b]). \qquad (5.45)$$

These regularity assumptions hold throughout. The Sturm–Liouville operator is

$$L f = \frac{1}{r}\Bigl( -(p f')' + q f \Bigr),$$

acting on the domain

$$D(L) = \{ f \in C^2([a,b], \mathbb{C}) : \cos(\alpha) f(a) - \sin(\alpha) p(a) f'(a) = 0,\ \ \cos(\beta) f(b) - \sin(\beta) p(b) f'(b) = 0 \}$$

for fixed real $\alpha, \beta$ (the separated boundary conditions; $\alpha = 0$ is Dirichlet, $\alpha = \pi/2$ Neumann). The underlying space is $H_0 = C([a,b], \mathbb{C})$ with the weighted scalar product

$$\langle f, g \rangle = \int_a^b f(x)^* g(x)\, r(x)\, dx$$

and norm $\|f\| = \sqrt{\langle f, f\rangle}$. $H_0$ is an inner product space but it is not complete. A number $z \in \mathbb{C}$ is an eigenvalue of $L$ if $L f = z f$ for some $f \in D(L)$ that does not vanish identically; $f$ is an eigenfunction. An orthonormal basis of $H_0$ is an orthonormal sequence $(u_n)$ such that $\|f - \sum_{n<N} \langle u_n, f\rangle u_n\| \to 0$ for every $f \in H_0$.

For the abstract part, $H_0$ is any complex inner product space (again not assumed complete). A linear operator $A$ on a dense subspace is symmetric if $\langle g, Af\rangle = \langle Ag, f\rangle$; an everywhere defined $A$ is compact if $(A f_n)$ has a convergent subsequence in $H_0$ whenever $(f_n)$ is bounded.

For $z \in \mathbb{C}$ let $u_a(z,\cdot)$, $u_b(z,\cdot)$ solve $L u = z u$ with $u_a(z,a) = \sin\alpha$, $p(a)u_a'(z,a) = \cos\alpha$, $u_b(z,b) = \sin\beta$, $p(b)u_b'(z,b) = \cos\beta$. Their Wronskian is $W(z) = u_b p u_a' - p u_b' u_a$, which does not depend on the point where it is evaluated. When $W(z) \neq 0$, the resolvent $R_L(z)$ is the integral operator with the Green function $G(z,x,t) = W(z)^{-1} u_b(z,\max(x,t))\, u_a(z,\min(x,t))$ and weight $r$.

Formalization targets

Goal: eigenfunction expansion (Theorem 5.11)

There are real numbers $E_n$ and real-valued eigenfunctions $u_n \in D(L)$, $L u_n = E_n u_n$, such that:

• the $E_n$ are pairwise distinct and are all the eigenvalues of $L$, and every eigenfunction for $E_n$ is a multiple of $u_n$ (the eigenvalues are simple);
• $|E_n| \to \infty$ (the eigenvalues accumulate only at $\infty$);
• $\langle u_m, u_n \rangle = \delta_{mn}$, and for every $f \in H_0$

$$f = \sum_{n=0}^{\infty} \langle u_n, f \rangle\, u_n \quad \text{in } H_0, \qquad (5.70)$$

• for $f \in D(L)$ the series (5.70) converges uniformly on $[a,b]$.

Milestones

1. Theorem 5.4. Eigenvalues of a symmetric operator are real, and eigenvectors for different eigenvalues are orthogonal.
2. Theorem 5.5. A compact symmetric operator on a nonzero inner product space has an eigenvalue $\alpha_0$ with $|\alpha_0| = \|A\| = \sup_{\|f\|=1}\|Af\|$.
3. Theorem 5.6 (spectral theorem). A compact symmetric operator has real eigenvalues $\alpha_j$ with orthonormal eigenvectors $u_j$, infinitely many when $H_0$ is infinite dimensional and then $\alpha_j \to 0$, and $f = \sum_j \langle u_j, f\rangle u_j$ for every $f \in \operatorname{Ran}(A)$; if $\operatorname{Ran}(A)$ is dense the $u_j$ are an orthonormal basis.
4. Lemma 5.9. $W(z)$ is an entire function of $z$ whose zeros are exactly the eigenvalues of $L$.
5. Lemma 5.10. For $W(z) \ne 0$, $R_L(z)$ is compact on $H_0$, and symmetric for real $z$.
6. Lemma 5.12 (Rayleigh–Ritz). The eigenvalues can be ordered $E_0 < E_1 < \cdots$; $E_0 = \min \langle f, Lf\rangle = \min Q(f)$ over normalized $f \in D(L)$, attained exactly at the eigenfunctions for $E_0$; and $\min_{[a,b]} q \le E_0$ when $0 \le \alpha \le \pi/2 \le \beta \le \pi$. Here $Q$ is the quadratic form $\int_a^b (p |f'|^2 + q |f|^2)\,dx$ plus the boundary terms $\cot(\alpha)|f(a)|^2 - \cot(\beta)|f(b)|^2$ (dropped when the angle is $0$).

Significance

Theorem 5.11 is the statement that makes eigenfunction expansions legitimate: Fourier sine and cosine series are its special case $p = r = 1$, $q = 0$, and it covers any positive weight and any smooth positive stiffness with separated boundary conditions. Solutions of the heat and wave equations on an interval with variable coefficients are built from it. The uniform convergence for $f \in D(L)$ is the version needed to differentiate or evaluate such series pointwise. Lemma 5.12 provides the variational characterisation of the lowest eigenvalue, the starting point for comparison theorems and eigenvalue estimates.

On the formal side, Mathlib has the spectral theorem for self-adjoint operators on finite-dimensional spaces, compact operators on normed spaces, and $L^2$ spaces. It has no Sturm–Liouville theory, no Green functions for boundary value problems, and no spectral theorem for compact symmetric operators on incomplete inner product spaces. The platform has finite-dimensional Rayleigh-quotient results and compactness of $L^2$ convolution operators, but nothing on this setting. The results here are classical and proved; what is missing is a machine-checked proof in the book's elementary setting of continuous functions.

Difficulty

The operator $L$ is unbounded on $H_0$ (Problem 5.16), so the obvious first idea, applying a spectral theorem for compact or bounded symmetric operators to $L$ itself, does not work. Completeness of the eigenfunctions is also subtle because $H_0$ is not complete. Hilbert-space arguments that produce limits in a completion, or that go through $L^2$, do not by themselves give an expansion of a continuous function in continuous eigenfunctions with convergence in $H_0$, still less uniform convergence. Simplicity of the eigenvalues depends on the separated boundary conditions and fails for periodic ones. On the formal side, one needs analytic dependence of solutions of a linear ODE on a complex parameter, one-sided derivatives at the endpoints, and interval integrals of piecewise-defined kernels.

Formalization scope

• Spaces. The abstract results use a type with [NormedAddCommGroup E] [InnerProductSpace ℂ E] and no CompleteSpace. Symmetry on a dense domain is IsSymmetricOp; for everywhere defined operators it is Mathlib's LinearMap.IsSymmetric. Compactness is IsCompactOp: subsequences converge in $H_0$ itself. $H_0 = C([a,b],\mathbb{C})$ is represented by functions $\mathbb{R} \to \mathbb{C}$ continuous on Set.Icc a b, with SLInner the weighted scalar product (5.52) as an interval integral. It is not $L^2$ and not a HilbertBasis.
• Operator and domain. SLOp, SLDomain, IsSLEigenfunction implement (5.53)–(5.55) with derivWithin on Set.Icc a b (one-sided at the endpoints) and ContDiffOn ℝ 2. RegularSL is (5.45), including $a < b$. $\alpha, \beta$ are arbitrary reals.
• Quantifier readings. "Countable, discrete, accumulating only at $\infty$" is an injective sequence $E_n$ exhausting the eigenvalues with $|E_n| \to \infty$. "Simple" is: every eigenfunction for $E_n$ equals $c\,u_n$ on $[a,b]$. "Can be chosen real-valued" is an existential choice of $u_n : \mathbb{R} \to \mathbb{R}$. $\|A\|$ in Theorem 5.5 is expressed by IsLUB of $\{\|Af\| : \|f\|=1\}$, and Theorem 5.5 assumes $H_0 \neq \{0\}$. In Theorem 5.6, $N \in \mathbb{N}_0 \cup \{\infty\}$ is ℕ∞: $N = \infty$ in infinite dimension and $N = \dim H_0$ otherwise. The minima of Lemma 5.12 are IsLeast (attained), and "equality iff $f = u_0$" reads as "iff $f$ is an eigenfunction for $E_0$", i.e. $f = c\,u_0$ with $|c| = 1$. $\min q \le E_0$ is $\exists x \in [a,b],\ q(x) \le E_0$. Norm convergence is $\operatorname{Re}\langle f - S_N, f - S_N\rangle \to 0$.
• Ruling out trivial readings. The resolvent is only considered with $W(z) \ne 0$ (Lean's $0^{-1} = 0$ would make it the zero operator). Scalar products are only applied to functions continuous on $[a,b]$, so no integral takes a junk value. Eigenfunctions must be nonzero on $[a,b]$. The expansion must hold in the weighted norm for every continuous $f$, which an orthonormal family that is merely orthonormal would not satisfy.

A complete development needs linear ODEs with a complex parameter and their analytic dependence on it, Green functions, an Arzelà–Ascoli argument in $C([a,b])$, and the spectral theorem for compact symmetric operators on an inner product space. The definitions RegularSL, SLOp, SLDomain, SLInner and SLWronskian are reusable for the oscillation and comparison theory (Theorems 5.17–5.25) in the rest of the chapter. Contributions connecting IsCompactOp to Mathlib's IsCompactOperator on the completion are welcome.

Selected references

• G. Teschl, Ordinary Differential Equations and Dynamical Systems, Graduate Studies in Mathematics 140, American Mathematical Society, 2012. Author's preliminary version: https://www.mat.univie.ac.at/~gerald/ftp/book-ode/ode.pdf ; published version: https://doi.org/10.1090/gsm/140
• J. C. F. Sturm, Mémoire sur les équations différentielles linéaires du second ordre, Journal de Mathématiques Pures et Appliquées 1 (1836), 106–186. http://www.numdam.org/item/JMPA_1836_1_1__106_0/
• J. Liouville, Mémoire sur le développement des fonctions ou parties de fonctions en séries dont les divers termes sont assujettis à satisfaire à une même équation différentielle du second ordre, Journal de Mathématiques Pures et Appliquées 1 (1836), 253–265. http://www.numdam.org/item/JMPA_1836_1_1__253_0/
• E. Schmidt, Zur Theorie der linearen und nichtlinearen Integralgleichungen. I, Mathematische Annalen 63 (1907), 433–476. https://doi.org/10.1007/BF01449770