Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
A fine-tuned model can be stored as a pretrained model together with its parameter changes. Pruning these delta parameters reduces the amount of task-specific information to store. The DARE procedure independently deletes each change with probability and multiplies every surviving change by . This preserves the expected linear-layer output, but a single pruned model can still differ substantially from that expectation.
Deng and coauthors investigate this distinction in DARE the Extreme: Revisiting Delta-Parameter Pruning For Fine-Tuned Models, ICLR 2025. The paper motivates changes to the rescaling rule and to fine-tuning regularization. This mission focuses on its finite-sample mathematical analysis: the relation between random pruning, coefficient energy, and output concentration. Its goal is the Kearns–Saul bound in Appendix E.1, equation (8), PDF p. 30, expressed through the coefficient statistics used in Section 3.2.
The distinction between that appendix result and the printed Theorem 3.1 matters. The mission does not assert the latter's piecewise formula. Its low-pruning branch omits the square root present in equation (8), and its high-pruning branch applies a one-sided refinement to a two-sided event. The exact target below retains the appendix's valid bound across the entire interval .
Fix one output coordinate of a linear layer, an input vector , and a delta-weight row . There are input coordinates. Define the deterministic influence coefficients , their sum , and their energy . Equivalently, the formal statements quantify over every real coefficient vector ; choosing realizes every such vector in the layer model.
The only randomness is the pruning mask. Write for a dropped coordinate, with mutually independent . A mask has probability
Expectations and event probabilities are the finite weighted sums against . A surviving coordinate is rescaled by , where . The output error, original minus pruned, is
DARE uses ; denote its error by . This is the retention-mask formulation in Section 3.2, equation (2), PDF p. 5, with . The empirical coefficient mean and variance are and . These statistics describe a fixed vector, not another source of randomness.
Define the concentration coefficient with its removable singularity filled in:
For every and failure probability , the goal is
This is Appendix E.1, equation (8), PDF p. 30, followed by the unnumbered energy identity on PDF p. 31. Zero coefficients are included: no positive-energy assumption is attached to the goal.
Four supporting milestones state the following results.
The analytic input is Berend–Kontorovich, Section 3, Theorem 4, equation (6), PDF pp. 3–4. The bound on is also stated in the DAREx appendix on PDF p. 30. 4. Exponential output tail: for and ,
This is the unnumbered display immediately preceding equation (8), PDF p. 30.
The target quantifies the error of a randomly selected pruned layer in terms of its actual influence coefficients. It distinguishes preserving an expectation from controlling a realization. The moment identities also expose the bias introduced by choosing a rescaling denominator different from .
Formalization supplies a precise probability model and checks every coefficient, sign, and exceptional case. The finite mask model and its normalization already compile locally with proofs. The five milestone and goal statements have been elaborated, but their theorem proofs remain open. Completing this mission would formalize the selected appendix result; it would not establish the paper's experimental accuracy claims, a whole-network guarantee, or an optimal rescaling rule.
Signed coefficients require exponential-moment control for both positive and negative arguments. The sharper estimate in Berend–Kontorovich, Lemma 5, equation (9), PDF p. 4 has a nonnegative-argument restriction. Using it for an unrestricted absolute tail loses an essential hypothesis.
For example, with , , , and , the error is with probability and with probability . The printed Theorem 3.1 threshold is , so its failure probability exceeds . This concrete source audit is the reason for selecting equation (8), not a claim that the printed theorem has been formally disproved in Lean.
The Lean model uses real coefficients indexed by Fin n and Boolean functions for masks. Nonnegative masses and normalization are proved from the product formula; concentration is never assumed in a structure field. Fixed weights and inputs are external data. Random training, dependence between masks, nonlinear activations, structural pruning, and empirical validation are outside this mission.
The main goal requires for the empirical statistics, for DARE rescaling, and for the confidence level. The moments permit empty coefficient vectors and endpoint probabilities because they use a separate positive . The exponential-tail milestone requires to avoid division by zero; the main goal includes . The value is explicit. No theorem relies on Lean's total division or logarithm to supply a missing analytic hypothesis.
In a scattering experiment a particle arrives from far away, interacts with a target, and leaves again. Far from the target the forces are negligible, so long before and long after the collision the particle should move like a free particle. Scattering theory makes this precise by comparing two quantum dynamics: the free evolution generated by the kinetic energy , and the full evolution generated by . The objects that compare them are the wave operators (Møller operators) , introduced by Møller (1945) and put on a rigorous footing by Jauch (1958) and Kato. Cook (1957) gave the first practical criterion for their existence. Kuroda, Birman, Agmon, Enß and others later developed the theory up to asymptotic completeness for short-range potentials.
This mission formalizes the abstract part of Chapter 12 of Teschl's Mathematical Methods in Quantum Mechanics (AMS GSM 99, 2009): the definition and basic structure of the wave operators, Cook's criterion, and the existence of the wave operators for a square-integrable potential in three dimensions.
Let be a complex Hilbert space. An operator is a linear map on a subspace , its domain; is self-adjoint if is dense and . A projection-valued measure assigns to each Borel set an orthogonal projection , with and for disjoint . The spectral measure of is . By the spectral theorem every self-adjoint equals for a unique : and . The time evolution is the bounded operator with .
For two self-adjoint operators , the wave operators are
is the set of asymptotic states and the set of states that have one. A closed subspace with projection reduces if and for .
On the free Schrödinger operator is with domain the Sobolev space : under the Fourier transform it is multiplication by on . For a real potential , has and .
Let be the free Schrödinger operator on and with a real . Then
that is, exists for every and both signs. Since the spectrum of is purely absolutely continuous, this is exactly what Teschl calls "the wave operators exist" (12.14).
Existence of the wave operators is the first step of every scattering theory for Schrödinger operators: without it the scattering operator is not defined on a useful set of states, and the questions of completeness and asymptotic completeness (Enß's theorem, Theorem 12.12 of the same chapter) cannot be posed. Lemma 12.1 and Theorem 12.2 are the structural facts that make partial isometries intertwining the two Hamiltonians; they imply that restricted to has absolutely continuous spectrum whenever does, and that kinetic energy is conserved in scattering. Cook's criterion is the tool used in practice to prove existence for concrete potentials, including Coulomb-type and time-dependent problems.
The results are classical and proved in the literature. They are not formalized. Mathlib has neither the spectral theorem nor a functional calculus for unbounded self-adjoint operators, and no scattering theory. The platform has no statement about wave operators; its BookProof development contains Stone's theorem for its own structure of unbounded operators, which this mission does not use.
The limit defining involves two unitary groups whose generators do not commute, and neither group is explicit for the perturbed operator . For Cook's criterion the product has to be differentiated in , which needs control of domains: must stay in the domain of , and the derivative of a strongly continuous unitary group exists only on the domain of its generator. For the goal, the time evolution of a general has no decay rate at all, and the potential is unbounded and has no decay assumption beyond square integrability, so the integrability condition of Cook's criterion cannot be checked for every directly. The intertwining relation (12.8) concerns unbounded operators and needs the reduction of the domains, not only an identity between bounded operators.
The formalization uses Lean 4 with Mathlib. Operators are LinearPMaps H →ₗ.[ℂ] H on a complex Hilbert space; self-adjointness is Mathlib's IsSelfAdjoint. Separability is not assumed.
The spectral theorem is not part of this mission. Every statement takes projection-valued measures and as data, with the hypotheses and (domain and quadratic form as above), which is the form the spectral theorem guarantees and which determines and . The time evolutions are and . In the goal, the self-adjointness of (Theorem 10.2 of the book) enters only through the existence of . Nothing is assumed about .
The sign of is a unit s : ℤˣ, and is written as in the variable . is Mathlib's limUnder and is used only on . A formalization that set where the limit fails and then proved only that is isometric would lose the content of the goal; here the goal asserts that the limit exists for every . In Cook's lemma the finiteness of the integral is integrability on , the bound uses the Bochner integral, and the hypothesis that lies in for , which the integrand presupposes, is explicit.
is Mathlib's Lp ℂ 2 on EuclideanSpace ℝ (Fin 3). The free Schrödinger operator is characterized through Mathlib's unitary Fourier transform , not the book's . The constants are translated: and . has and almost everywhere.
A complete development needs a functional calculus for projection-valued measures (strong continuity and differentiability of on , Theorem 5.1), the explicit decay of the free Schrödinger group in ((7.31) of the book), and density of in . These pieces are reusable for the rest of Chapter 12 (incoming and outgoing states, short-range potentials, asymptotic completeness). Proofs of any milestone and of such supporting lemmas are welcome.
Quantum mechanics describes mixed states by density operators: positive operators on a Hilbert space with . Expectation values are traces , perturbation determinants and spectral shift functions are built from traces of resolvent differences, and scattering theory (the Kato–Rosenblum and Birman–Krein theorems) is phrased in terms of trace class perturbations. All of this needs a trace in infinite dimensions, and the trace only makes sense on a restricted class of operators.
This mission formalizes Sections 6.2–6.3 of G. Teschl, Mathematical Methods in Quantum Mechanics, With Applications to Schrödinger Operators (AMS Graduate Studies in Mathematics 99, 2009), the standard route from compact operators through Hilbert–Schmidt operators to the trace class. The theory goes back to von Neumann and Schatten in the 1940s (R. Schatten, Norm Ideals of Completely Continuous Operators, Springer 1960). A modern account is B. Simon, Trace Ideals and Their Applications (AMS 2005).
Let be a complex Hilbert space, with inner product conjugate-linear in the first argument, and let be the bounded linear operators on with the operator norm . An operator is of finite rank if its range is finite dimensional, and the compact operators are the norm closure of the finite rank operators.
For with adjoint , the operator is positive. The singular values of a compact are the square roots of the nonzero eigenvalues of , each repeated according to its multiplicity . For the Schatten -norm and Schatten -class are
A compact is Hilbert–Schmidt if and trace class if . For an orthonormal basis of the trace is
In Lean these are compactOperators H, schattenNorm p K, schattenClass H p, IsHilbertSchmidt K, IsTraceClass K and trace K, in the namespace TeschlQM.TraceClass.
For every trace class and every orthonormal basis the series (6.26) converges, and for any two orthonormal bases ,
The result itself. Lemma 6.15 is what turns the trace into a linear functional on at all. Every later use of the trace rests on it: the normalization of density matrices, the duality , trace formulas and spectral shift functions, and Lidskii's theorem (the trace is the sum of the eigenvalues), which Teschl mentions right after the lemma. The ideal properties (Corollaries 6.11 and 6.14) and the factorization (Lemma 6.13) are the everyday tools for proving that a concrete operator, such as in Chapter 7, is trace class.
Formalizing it. Mathlib has compact operators (IsCompactOperator), Hilbert bases, singular values and the trace of linear maps on finite-dimensional spaces (LinearMap.singularValues, LinearMap.trace), but no infinite-dimensional singular values, Schatten classes, Hilbert–Schmidt or trace class operators, and no basis-independent trace. The Prove2Me corpus has finite-dimensional trace norms (matrices) and kernel operators, but no statement of this section. The results are classical and fully proved in the literature; the work is to formalize them.
The obvious argument for basis independence is to expand in both bases and interchange the two sums. In infinite dimensions that interchange is not justified for an arbitrary bounded : for the identity on an infinite-dimensional space, or for a non-trace-class compact operator, the diagonal series diverges. The trace class hypothesis must therefore enter through a factorization, and the factorization rests on the canonical form of Theorem 6.7, which in turn needs the spectral theorem for the compact self-adjoint operator , including finite multiplicity of its nonzero eigenvalues. A second difficulty is bookkeeping: the singular values are a family with multiplicities that may be finite or countably infinite, and the Schatten norm, the Hilbert–Schmidt sums over a basis and the supremum formula (6.23) all have to be matched as sums in .
{H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]. Separability is not assumed. Orthonormal bases are Mathlib HilbertBasis ι ℂ H with arbitrary index types, so every statement covers the book's separable case.H →L[ℂ] H, products are compositions, adjoints are ContinuousLinearMap.adjoint, and the operator order in Lemma 6.16 is Mathlib's Loewner order ( iff is positive). Traces are compared with the partial order of .IsCompactOperator.trace K is in one fixed, chosen Hilbert basis. The goal states summability in every Hilbert basis, not merely equality of tsum values. Since the tsum of a non-summable family is in Mathlib, a statement asserting only that all tsums agree would be trivially satisfiable by divergent series. That trivializing reading is ruled out.Reusable infrastructure a complete development will produce includes the spectral theorem for compact self-adjoint operators with multiplicities, the singular value decomposition in infinite dimensions, and the Hilbert–Schmidt and trace class ideals. All of these are welcome as independent contributions, and any of them would fill gaps in Mathlib.
An atom with electrons is described, with the nucleus fixed at the origin, by a Schrödinger operator on whose potential does not decay in all directions: moving one electron to infinity while the others stay near the nucleus leaves the remaining Coulomb attraction untouched. For this reason the standard route to the essential spectrum of a one-particle operator, showing that the potential is a relatively compact perturbation of , fails for . The HVZ theorem, due to Zhislin (1960), van Winter (1964) and Hunziker (1966), gives the answer anyway: the essential spectrum of the -electron atom begins exactly at the ground state energy of the ion with one electron removed. It is the basic structural result of -body quantum mechanics, and the starting point for every discussion of bound states, ionization energies and the stability of atoms and molecules.
This mission follows Chapter 11 of Teschl, Mathematical Methods in Quantum Mechanics (AMS GSM 99, 2009), which proves self-adjointness by Kato's theorem and the HVZ theorem by the localization method of Ismagilov, Morgan, Simon and Sigal.
Write for Euclidean space with Lebesgue measure. The Sobolev space is the set of with , and the free Schrödinger operator is with domain (units , mass ). A measurable function acts as the multiplication operator on its maximal domain .
For an operator with domain in a Hilbert space, the resolvent set is the set of for which maps bijectively onto the space with bounded inverse , and is the spectrum. The discrete spectrum consists of the eigenvalues that are isolated points of and have finite-dimensional eigenspaces; the essential spectrum is . is bounded from below if on for some . is bounded if and ; the infimum of admissible is the -bound. is relatively compact with respect to if is compact for one .
For an atom with electrons at , , and constants , the atomic Hamiltonian is
denotes the same operator for electrons with the same constants.
For , is bounded from below, and
with for . The minimum is attained and, for , negative; both are part of the claim.
The result. The HVZ theorem separates the spectrum of an atom into a continuum , fixed by the -electron ion, and a discrete part below it consisting of bound states. The ionization energy of the atom is . Questions such as whether a given atom or negative ion has a bound state at all, whether it has infinitely many (Zhislin's theorem for neutral atoms and positive ions), and how many electrons a nucleus can bind are all formulated relative to the threshold the HVZ theorem identifies. The same argument, with additional notation, covers molecules with fixed nuclei and general -body systems.
Formalizing it. The results are classical and proved in the standard texts (Reed–Simon IV, Cycon–Froese–Kirsch–Simon, Teschl). None is formalized. Mathlib now has the unitary Fourier transform on , tempered distributions and Sobolev spaces defined through the Fourier transform, but no self-adjoint Schrödinger operators, no essential spectrum and no many-body Hamiltonians. This mission asks for formal proofs of Teschl's four supporting results and of the HVZ theorem, and in doing so fixes a concrete representation of , of Coulomb-type multiplication operators and of the -electron atom on which later work (bound states of atoms, scattering) can build.
The obvious argument for the essential spectrum of , relative compactness of followed by Weyl's theorem, is not available: does not vanish as in directions where stays bounded, and it is not relatively compact with respect to on . The inclusion therefore requires decomposing configuration space into regions in which one specific electron is far from the nucleus, controlling the error terms of that decomposition, and comparing the localized pieces with decoupled operators whose spectrum is known; this uses self-adjointness and relative bounds for operators built from the same potentials with one electron removed. The reverse inclusion requires approximate eigenfunctions built from those of and of the free one-electron operator, and a statement that is attained. Negativity of needs the hydrogen-like ground state and a comparison argument across .
Behind all of this sits the analytic layer: Kato's theorem requires that in three dimensions is infinitesimally bounded with respect to and that this survives the passage to through an orthogonal change of variables; the IMS formula requires relating the Fourier definition of to derivatives of products.
The Hilbert space is Lp ℂ 2 volume over EuclideanSpace ℝ ι; for the atom, , so is the Euclidean norm on and is electron x j. Operators are Mathlib LinearPMaps, self-adjointness is Mathlib's IsSelfAdjoint, and sums of unbounded operators are LinearPMap sums with the intersection of the domains. (freeHamiltonian) is defined as with Mathlib's unitary Fourier transform (kernel , no prefactor); this is the same operator on the same domain as Teschl's . Multiplication operators (mulOp) have their maximal domains. (atomicHamiltonian) is freeHamiltonian + mulOp V^{(N)}; the equality of its domain with is a claim of Theorem 11.1, not an assumption. Resolvent set, spectrum, discrete and essential spectrum are defined from the bounded two-sided inverse of , not from Mathlib's Banach-algebra spectrum. The -bound takes values in . The IMS formula is stated in the sense of distributions, tested against functions, since for merely smooth its right-hand side need not lie in . No projection-valued measure or functional calculus is taken as data.
A trivializing formalization is ruled out: is defined as the minimum of the spectrum of the independently constructed -electron operator, never as the infimum of , which would make (11.9) circular; its attainment and negativity are conclusions. The goal covers ; for the ion has no electrons, is not negative, so the negativity of is claimed for only.
A complete development needs the theory of the Fourier transform and , Hardy- or Sobolev-type bounds for in , the Kato–Rellich theorem, Weyl's theorem on relatively compact perturbations, a smooth partition of unity on the sphere, and the Weyl criterion for essential spectrum. The definitions of , multiplication operators, resolvent and essential spectrum are shared with other chapters of this series and are intended for reuse; contributions of general lemmas about them are welcome.
Stochastic differential equations (SDEs) whose coefficients grow faster than linearly appear throughout applied probability: population and epidemic models with cubic damping, Langevin dynamics with non-quadratic potentials, and stochastic volatility models such as the 3/2-model used for pricing VIX options (Goard–Mazur 2013). Their solutions are almost never available in closed form, so they are simulated, and the method of choice is the explicit Euler–Maruyama scheme, because it is cheap and easy to implement.
For superlinearly growing coefficients the classical explicit scheme fails: its moments can diverge even when those of the true solution are finite, so it does not converge in . Implicit schemes repair this at a higher computational cost (Higham–Mao–Stuart 2002). A second repair is to keep the scheme explicit but modify ("tame") its coefficients by an amount that vanishes as the step size goes to zero.
Timeline.
Fix a filtered probability space satisfying the usual conditions, a Wiener martingale in (a standard Brownian motion adapted to whose future increments are independent of ), and a horizon . For , is the Euclidean norm and the scalar product; for a matrix, is the Hilbert–Schmidt norm.
The SDE is
with Borel coefficients , and an -measurable initial value .
For let , the last grid point of mesh before . The scheme is
with the same initial value and Borel coefficient sequences ("varying coefficients"). Between grid points the coefficients are frozen at , so the scheme is explicit.
The hypotheses, with : A-1 continuity of in ; A-2 local boundedness of ; A-3 local monotonicity on ; A-4 coercivity ; A-5 . For the scheme: B-1 for every ; B-2 and for some ; B-3 the coercivity bound of A-4 for , uniformly in .
Under A-1–A-5 and B-1–B-3 with , for every ,
No rate is claimed; the statement holds for every coefficient sequence satisfying B-1–B-3, not only for the paper's tamed Models 1 and 2.
Theorem 1 gives -convergence of a whole class of explicit schemes, with no global Lipschitz condition on either coefficient, for every below the coercivity order . In the 3/2-model of the introduction (, ), earlier explicit results gave -convergence only for (Hutzenthaler–Jentzen 2015, §4.10.3); Theorem 1 gives it for all . The theorem is also the qualitative base on which the paper's rate results (Theorems 2 and 3, separate missions of this series) are built, and it justifies Monte Carlo estimates of moments computed with such schemes.
The result is proved in the paper. It has, to our knowledge, no machine-checked proof anywhere; Mathlib has Brownian motion but no stochastic integral, and the Itô integral used here is the relational definition published by the Ethier–Kurtz series on this platform. A formal proof needs Itô's formula for , Gronwall's lemma for moment functions, the convergence in probability of Theorem 4 (which the paper cites from Gyöngy–Sabanis rather than proving), and a uniform-integrability argument. Each of these is reusable well beyond this paper.
The natural first idea, estimating directly by Itô's formula and Gronwall, fails: under only local monotonicity the difference of drifts cannot be bounded by with a constant uniform in the state, so the Gronwall constant blows up. The route through convergence in probability and uniform moment bounds is forced, and the hard step is Lemma 2: bounding uniformly in . The coefficients of the scheme may grow like , and the frozen argument produces a correction term whose control is exactly where the restriction enters. For fixed finiteness of moments is easy (linear growth); uniformity in is the content.
States are EuclideanSpace ℝ (Fin d); diffusion values are EuclideanSpace ℝ (Fin d × Fin d₁), whose norm is the Hilbert–Schmidt norm. Time is ℝ≥0; coefficients are uncurried maps on ℝ≥0 × ℝ^d, assumed Borel measurable. An Itô process on is a measurable process, adapted to the filtration augmented by all -null sets, with continuous paths on , satisfying the integral equation almost surely simultaneously for all ; the stochastic integral is the platform relation EthierKurtz.HasBrownianItoIntegral, applied coordinatewise with the integrand cut off after . Nothing is required of the processes after , so no existence beyond the horizon is assumed. Right-continuity of the filtration is a hypothesis; completeness is replaced by adaptedness to the augmented filtration, which is weaker, so the formal theorems are at least as strong as the paper's.
The solutions and are hypotheses, all on one probability space with one Wiener process and one initial value; the theorems do not construct them. Expectations are lower Lebesgue integrals in and suprema over are taken in , so no statement can hold because an expectation or a supremum takes a default value. B-1's integrand, a supremum over an uncountable ball, is required to be a.e. measurable in , as the paper's Lebesgue integral presupposes. The exponent in Theorem 1 and Lemma 2 is restricted to , the paper's convention for . The dependence clauses "" (Lemma 1) and "" (Lemma 2) are not formalized: only finiteness, i.e. a bound independent of , is stated, which is what the proofs establish. Theorem 4 is stated with exactly its printed hypotheses.
A trivializing formalization, in which the moment bounds or the limit hold because the expectation or the supremum defaults to , or because the hypotheses on the solutions cannot be met, is ruled out: all quantities live in , and a sorry-free check shows every hypothesis is satisfiable (zero coefficients, constant solutions).
Contributions welcome: Itô's formula for the platform's integral relation, Burkholder–Davis–Gundy or Doob inequalities for it, a Gronwall lemma for measurable moment functions, and the Gyöngy–Sabanis convergence-in-probability theorem.
In one complex variable, every smooth function on a disc is of some smooth , and this is what makes the Mittag-Leffler theorem work: local principal parts can be glued into a global meromorphic function. In several variables the corresponding equation is the -problem: given a differential form with , find with . Whether it is solvable on a domain is measured by the Dolbeault cohomology groups . Their vanishing characterizes domains of holomorphy, and it drives the solution of the additive Cousin I problem, the several-variable Mittag-Leffler problem.
This mission follows §4.4–4.6 of Jiří Lebl's open textbook Tasty Bits of Several Complex Variables (version 4.4, 2026). There the -problem is solved on polydiscs, from the one-variable Cauchy transform through the Dolbeault–Grothendieck lemma. The result is then applied to the Cousin I problem and to domains of holomorphy. The Dolbeault lemma goes back to P. Dolbeault (1953) and A. Grothendieck. The global theory on pseudoconvex domains is due to Hörmander (An Introduction to Complex Analysis in Several Variables, 1966) and to Cartan's Theorem B.
Write for the coordinates of . The Wirtinger derivative of a function is .
For strictly increasing tuples and in , write and . A smooth -form on an open is
where and run over the increasing - and -tuples and each is on . The operator
maps -forms to -forms. A form is -closed if and -exact if ; by convention the only exact -form is . The statement means that every smooth -closed -form on is -exact.
A possibly unbounded polydisc is a product in which each is either a disc or all of ; for example itself. The finite polydisc is .
Cousin I data on an open consist of an open covering of and holomorphic on with and on the respective intersections. A solution is a family of holomorphic on with . The problem is solvable on if all Cousin I data on have solutions.
In Lean these are wirtingerBar, FormCoeffs, dbar, IsSmoothForm, DolbeaultVanishes, polydisc, IsPossiblyUnboundedPolydisc, IsCousinISolvable and IsDomainOfHolomorphy in the namespace LeblSCV.Dolbeault.
Let be a possibly unbounded polydisc, , , and a smooth -form on with . Then there is a smooth -form on with
Theorem 4.4.5 is the model case of the vanishing theorem , , on domains of holomorphy. In particular it solves the -problem on all of . Through Theorem 4.6.5 it gives the Cousin I problem on polydiscs, and therefore the existence of meromorphic functions with prescribed local principal parts there. Theorem 4.5.6 is one half of the cohomological characterization of domains of holomorphy (Remark 4.5.8, item (viii)). The other half is Cartan's Theorem B, which the book states without proof as Theorem 4.4.2.
All targets are classical and fully proved in the book. As far as a search of the Prove2Me corpus and of Mathlib shows, none of them is formalized. Mathlib has real Fréchet derivatives, smooth bump functions and partitions of unity, and Lebesgue measure on . It has no bidegree forms, no operator on forms, no Cauchy transform and no Dolbeault cohomology. This mission builds the -form layer and the first global solvability theorem for .
The one-variable step needs the Cauchy–Pompeiu formula and differentiation under an integral with a weakly singular kernel. Both the smoothness of and the identity require care near .
In several variables, the natural idea is to solve on each of an exhausting sequence of polydiscs and take a limit. It fails as stated: solutions on successive polydiscs differ by -closed forms and need not converge. For the discrepancy has to be corrected exactly, by applying the lemma again with a cutoff. For the discrepancies are holomorphic functions, and they have to be made small by polynomial approximation, so that the corrected solutions converge. The Dolbeault–Grothendieck lemma loses a little of the polydisc at each step, so the argument has to shrink the polydiscs at each stage.
On the formal side, on forms carries signs from reordering wedge products. A wrong sign changes which forms are closed. So the sign convention is fixed in the definition and checked against .
Fin n → ℂ with 0-based indices. Polydiscs use the modulus in each coordinate, as in the book, so the sup norm of Fin n → ℂ agrees with them. No Euclidean ball occurs.FormCoeffs n = Finset (Fin n) → Finset (Fin n) → (Fin n → ℂ) → ℂ: an increasing tuple is the set of its entries, and η A B z is the coefficient of . IsSmoothForm U p q η requires every coefficient to be ContDiffOn ℝ ∞ on and the coefficients of the wrong bidegree to vanish on . Only values on matter.dbar is Definition 4.4.1 written in the increasing basis. The coefficient of is . A sorry-free check confirms that this sign convention makes the mixed second derivatives cancel in , and that .ℝ≥0∞, with meaning the factor .DifferentiableOn ℂ. A domain is an open connected set. Cousin index types range over Type, which loses nothing.dbar defined here, or of the one-variable lemma for general piecewise- domains, are welcome.Boundary feedback stabilization of the wave equation asks whether a vibrating body at rest on part of its boundary can be brought to rest by a damping law on the rest of its boundary. With the undelayed velocity feedback , the energy decays exponentially under geometric conditions on the domain; results of this kind go back to Chen (1979, 1981), Lagnese (1983, 1988), Lasiecka and Triggiani (1987), and Komornik and Zuazua (1990).
Real controllers act with a delay, and delays can destroy stability. Datko, Lagnese and Polis (1986) and Datko (1988) showed that an arbitrarily small delay in a boundary feedback that stabilizes the one-dimensional wave equation can make the closed loop unstable. For a feedback made of an undelayed part and a delayed part, , Xu, Yung and Li (2006) proved, by spectral analysis in one space dimension, that the system is stable when . Nicaise and Pignotti (2006) extended the stability result to bounded domains in any dimension . This mission formalizes that extension: Theorem 1.1 of their paper.
Let () be a bounded open set whose boundary is of class . The boundary is split as , with and . Let be the outer unit normal and the surface measure on . Fix the undelayed gain , the delayed gain and the delay . The problem is
with initial data and in , and a history on (1.4)–(1.5).
The geometric hypothesis requires a function and a constant with two properties:
For example, satisfies both on an annulus whose inner sphere is .
Assume the gain condition
and fix with
The energy of a solution is the standard wave energy plus a term that stores the delayed velocity:
There are constants , depending on but not on the solution, such that every regular solution satisfies
The constants are existential and are not fixed numerically. Any valid pair proves the goal.
The theorem shows that adding a delayed component to a stabilizing boundary feedback preserves exponential decay if the delayed gain is dominated by the undelayed gain. It holds in every dimension, under the same geometric condition that governs the undelayed problem. The companion Theorem 1.2 of the same paper shows that the condition cannot be removed: when it fails, there are delays for which some solutions keep constant, positive standard energy. The Lyapunov functional (1.9) became a standard device for delayed feedbacks in later work on wave, plate and Timoshenko systems.
The result was proved in 2006. It has no machine-checked proof. This mission produces:
The dissipation inequality (Proposition 3.1) is a calculation: Green's formula, a change of variables in the delay variable , and Young's inequality. The difficulty is entirely in the observability inequality (3.10). The obvious multiplier argument, which multiplies the equation by and integrates, leaves a lower-order term that the boundary observation does not control.
The paper removes that term in two steps. The first is a Carleman-type estimate of Lasiecka, Triggiani and Yao (1999), which is where hypotheses (1.6)–(1.7) enter. The second is a compactness–uniqueness argument closed by Holmgren's uniqueness theorem. None of these tools exists in Mathlib, and neither does Green's formula on a curved domain. The final step from a one-period contraction to exponential decay uses time-translation invariance and monotonicity of .
Domain. A MixedDomain n bundles the following:
The outer normal is . The Gauss–Green requirement determines uniquely as the surface measure, so the normalization of in (1.9) and (1.10) is the paper's.
Solutions are real-valued and classical: is one function on . It satisfies (1.1)–(1.3) for , and its values at are the initial data and the history. Time derivatives are one-variable derivatives in , and . This is a subclass of the paper's solutions, so the formal theorems are the paper's restricted to smooth, compatible data.
Added hypothesis. In Proposition 3.2, the contraction step and the goal, every connected component of has a boundary point in (true whenever is connected). The paper's uniqueness step (", on , on , so ") needs every component of to meet .
Strengthened statements. The identity (3.6) and Propositions 3.1 and (3.22) omit hypotheses they do not use. Proposition 3.1 states the explicit constant from the end of its proof.
Conventions. Condition (1.10) is strict. The energy is of (1.9), with the delay term, and not the standard energy. Derivatives of are asserted with HasDerivAt.
Excluded trivializations. Three things would make the statements empty or different, and none of them is allowed:
The degenerate case is already excluded by (1.6), (1.7) and Gauss–Green together.
Infrastructure needed and welcome:
MixedDomain;The last lemma and Gauss–Green on domains are reusable far beyond this mission.
The first step in analysing a nonlinear differential equation near an equilibrium is usually to replace by its derivative there and study the linear system , which can be solved explicitly. This step is justified only if the linearization predicts the qualitative behaviour of the nonlinear system correctly. The Hartman–Grobman theorem makes that precise. If no eigenvalue of lies on the imaginary axis, then near the equilibrium the nonlinear flow is a continuous deformation of the linear flow . The phase portrait, including which solutions approach the equilibrium and which leave it, is the linear one up to a homeomorphism.
The theorem was proved independently by D. M. Grobman (1959) and P. Hartman (1960, Proc. AMS 11). C. Pugh gave the proof by a global contraction argument (1969, Amer. J. Math. 91) that most textbooks follow, including this one.
This mission formalizes the Hartman–Grobman part of Chapters 9 and 10 of Teschl, Ordinary Differential Equations and Dynamical Systems (AMS Graduate Studies in Mathematics 140, 2012; author's preliminary version): the linear stable and unstable subspaces, the conjugacy lemma for maps, and the theorem for flows and for maps.
Let and let be a real matrix. Its eigenvalues are the complex numbers with for some nonzero . For a set , the spectral subspace is the set of real vectors lying in the sum of the generalized eigenspaces with , where is the algebraic multiplicity.
For the linear flow , the stable subspace is and the unstable subspace is . is hyperbolic (for flows) if no eigenvalue has zero real part. For the linear map , the contracting and expanding subspaces are and , and is hyperbolic (for maps) if no eigenvalue lies on the unit circle.
A vector field is a map on an open set . Its flow is the maximal solution of , , defined for in the maximal interval . A point with is a fixed point. It is hyperbolic if the Jacobian matrix is hyperbolic. Two flows are topologically conjugate if there is a homeomorphism of with .
Let be a hyperbolic fixed point of the vector field , with and flow . Then there are a homeomorphism of , with bounded, and a neighborhood of such that
for all and with for every between and .
In attack order:
and is a homeomorphism when is invertible. 3. Corollary 9.8: such a conjugating homeomorphism of the form identity plus bounded is unique. 4. Theorem 10.4 (Hartman–Grobman for maps): a local diffeomorphism with a hyperbolic fixed point satisfies near , with . 5. Theorem 9.10: two hyperbolic linear flows whose stable and unstable subspaces have equal dimensions are topologically conjugate.
The result itself. Hartman–Grobman reduces the local topological classification of hyperbolic equilibria to linear algebra. Together with Theorem 9.10 it shows that, near a hyperbolic fixed point, a vector field is determined up to local topological conjugacy by two integers: the dimensions of the stable and unstable subspaces. In particular, stability and instability of a hyperbolic equilibrium can be read off the eigenvalues of the Jacobian.
Formalizing it. Mathlib has the matrix exponential, generalized eigenspaces and homeomorphisms. It has no hyperbolic splitting of a matrix, no conjugacy theory for flows or maps, and no local flow of an ODE with maximal intervals; none of these results has a machine-checked proof on this platform. The mission builds the linear hyperbolic layer (spectral subspaces with exponential rates), the functional-analytic conjugacy lemma, and the local theorems on top of them.
The naive idea is to conjugate the nonlinear flow to its linearization directly on a small ball. That fails because a small ball is not invariant: orbits of a saddle leave every neighborhood of the fixed point, and a conjugacy defined only on the ball cannot be propagated along them. The book's route first makes the problem global and then solves a functional equation. Solving it requires an operator-norm estimate on a space of bounded continuous functions, with a norm on adapted to the hyperbolic splitting.
A second difficulty is passing from one time to all times. A conjugacy for the time-one map has to be upgraded to one for the whole flow, which needs a uniqueness statement (Corollary 9.8) and control of the derivative of the flow through the variational equation. Throughout, the flow is local, so every identity also carries the claim that lies in the maximal interval of .
The state space is Fin n → ℝ; matrices are Matrix (Fin n) (Fin n) ℝ, is NormedSpace.exp (t • A) acting by mulVec, and eigenvalues are those of the complexified matrix. The subspaces are defined spectrally, exactly as the book's (9.2), with the book's sign convention ( is the stable or contracting side for both flows and maps). The flow is local and enters through IsMaximalFlow f M I Φ, the unique maximal integral curves on an open phase space . No completeness is assumed.
Conventions and quantifier readings:
A trivializing formalization is ruled out. The conjugacy at the single point , or at only, holds for every (both sides are , respectively ). The goal instead fixes and first and requires the identity on every orbit segment inside , with the maximal flow of rather than an arbitrary map.
Needed infrastructure:
The linear layer and the conjugacy lemma are reusable for the stable manifold theorem, for periodic orbits (Chapter 12) and for the horseshoe (Chapter 13). Standalone contributions of those layers are welcome.
Caching (online paging) is one of the oldest problems in online algorithms: a fast memory of 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 -competitive, and the best randomized algorithms are -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.
A request sequence lists elements of a set . A cache of size 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 is the least number of misses over all eviction schedules chosen with knowledge of .
With each request the algorithm receives a real prediction . The true label is the position of the next request of , or if there is none. For a loss function , the error of the predictions is , and the predictions are -accurate when .
The spread of measures how cheaply a predictor can get the order of arrivals completely wrong: is the least length such that every strictly increasing integer sequence and every non-increasing real sequence have total loss .
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 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 is at most , 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 .
If is concave on and majorizes the spread, then for every , every tie-breaking rule, and every sequence with -accurate predictions,
The result. Theorem 3.3 gives both guarantees at once. For an exact predictor () the ratio is a constant, , independent of ; for an arbitrary predictor it is , 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 , so the ratio grows like . 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 printed as in Lemma 3.4, and the behaviour of the spread at .
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 and the chain lengths are both random, while the hypothesis controls only the total error against , not the number of chains in which the error is spread.
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 for elements never requested again. The paper prints the label with equal features; the element is meant. is computed as the minimum over all demand-paging schedules from the empty cache, which loses no generality. is harmonic k as a real number, never .
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 .
The spread takes real arguments and lengths . must be concave on , finite, and at least the spread. It must also be continuous at , which the paper does not say: without it the chain lemma fails for losses whose minimal reversed-order loss stays over several lengths. -accuracy is the pointwise condition on the given pair . The competitive ratio is written as a product, so needs no special case. Lemma 3.3 is stated pointwise for chains without random evictions, as its proof shows. Lemma 3.4 has in place of the printed , with the minimum inside the expectation because is random.
The statement must not be trivialized. 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 has spread .
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 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 (reusable for any marking algorithm), and a bound on the expected number of misses caused by elements evicted uniformly at random within a phase.
Many linear differential equations of mathematical physics have coefficients with singular points. Examples are the Bessel equation , which comes from separating variables in the Laplace and wave equations in cylindrical coordinates, and the Legendre, hypergeometric and confluent hypergeometric equations. Near a singular point the usual power-series method breaks down, and the practical question is how solutions behave as approaches the singularity. Evaluating special functions, matching asymptotics and computing connection coefficients all depend on the answer.
For second-order equations the answer goes back to Lazarus Fuchs (Zur Theorie der linearen Differentialgleichungen mit veränderlichen Coefficienten, J. reine angew. Math. 66 (1866), 121–160, doi:10.1515/crll.1866.66.121) and to Georg Frobenius (Ueber die Integration der linearen Differentialgleichungen durch Reihen, J. reine angew. Math. 76 (1873), 214–235, doi:10.1515/crll.1873.76.214). Frobenius's generalized power-series ansatz is known as the Frobenius method. This mission follows Chapter 4 of G. Teschl, Ordinary Differential Equations and Dynamical Systems (AMS Graduate Studies in Mathematics 140, 2012, doi:10.1090/gsm/140), in the author's preliminary version.
All functions are complex-valued functions of a complex variable , and derivatives are complex derivatives. The object is the second-order linear equation
near the point , where the coefficients may be singular. A function that is holomorphic on a punctured disc has a pole of order at most at if extends to a function analytic at . The point is a regular singular point of (4.20) if has a pole of order at most one and a pole of order at most two there:
In Lean these hypotheses are functions holomorphic on with and for . The general notion is TeschlODE.Frobenius.HasPoleOfOrderAtMost f k.
The indicial equation is . Its roots, the characteristic exponents, are
where the square root is the principal branch, so that . In Lean they are charExponents p₀ q₀.
The functions and are single-valued only after a branch cut is chosen. As the book does, solutions are considered on the slit punctured disc (slitDisc R), using the principal branches. A solution of (4.20) on an open set is IsSolution p q D u. A fundamental system is a pair of solutions that are linearly independent over on .
Let be a regular singular point as in (4.30), with holomorphic on , . Let be the characteristic exponents of , . Then there are functions , holomorphic on the whole disc with , such that on the following holds.
form a fundamental system.
The requirement that be holomorphic on the full disc is the book's statement that the radius of convergence of is at least the smaller of the radii of convergence of and .
In attack order:
Theorem 4.5 is the basic structural theorem for linear equations at a regular singular point. It determines the leading behaviour of each solution from two numbers read off the coefficients. It says exactly when a logarithm can occur, and it guarantees that the series part converges on the full disc on which the coefficients converge. Theorem 4.6 shows that the regular-singular hypothesis cannot be weakened. The series expansions of Bessel functions , of Legendre functions and of the hypergeometric function , and the logarithmic second solutions for integer order, are all instances of the theorem. The theorem is also the local ingredient of the classification of Fuchsian equations, including the Riemann -symbol.
Mathlib has holomorphic functions, power series with radius of convergence, the principal complex power and logarithm, and a real-variable ODE layer. It has no complex-analytic existence theorem for differential equations and no Frobenius theory. The results here are classical and proved in the book, but to our knowledge none of them has a machine-checked proof. The platform has real-variable regular-singular estimates (the RegularSingular namespace), which are a different setting. A formal Theorem 4.5 would give a foundation for formal special-function theory, for example Bessel functions defined as solutions of their equation.
The formal power-series computation is mechanical: substitute , compare coefficients, and read off the indicial equation and a recursion for the . The difficulty is everything around it. First, the recursion for the second exponent breaks down exactly when , and the form of the second solution changes there. Whether a logarithm really appears depends on a compatibility condition that can go either way when . Second, the claim is about actual solutions on a slit domain, not formal series. This needs convergence estimates for the recursion and the principal branches of and . Third, the radius claim asks for convergence on the whole disc of the coefficients, not just on some small disc. Fourth, linear independence of the two solutions has to be proved on the slit domain.
Milestones 1 and 3 need the complex analogues of Picard iteration and analytic continuation, which Mathlib does not supply for differential equations.
Namespace TeschlODE.Frobenius. Complex derivatives are HasDerivAt/deriv/DifferentiableAt ℂ, and holomorphy on a set is DifferentiableOn ℂ. Radii are ENNReal, so is allowed. Discs are Metric.eball 0 R. Powers and logarithms are Mathlib's principal Complex.cpow and Complex.log, used only on slitDisc R = Metric.eball 0 R ∩ Complex.slitPlane. On the full punctured disc these functions are discontinuous along the negative axis, and the theorem would be false there. "Fundamental system" is linear independence over on the solution domain. Without independence Case 1 would hold trivially with . "" is ∃ m : ℕ, α₁ - α₂ = m. The book's "the constant might be zero unless " is the clause .
Quantifier readings:
IsOpen Ω together with SimplyConnectedSpace Ω. "The largest disc" has radius Metric.infEDist z₀ Ωᶜ.The trivializing formalization, with the two solutions not required to be linearly independent or with unconstrained away from , is ruled out by the independence clause and by requiring to be holomorphic on the whole disc with .
A full development needs the following: the complex Picard iteration, analytic continuation along paths (the monodromy theorem), Cauchy-type estimates for recursively defined power series, and the calculus of and on the slit plane. The definitions slitDisc, IsSolution, charExponents and HasPoleOfOrderAtMost can be reused for the Bessel, Legendre and hypergeometric equations (Problems 4.5–4.18 of the book). Contributions such as a general complex-analytic ODE existence theorem are welcome.
Zero sets of holomorphic functions are the basic objects of local complex-analytic geometry. In one variable they are discrete, and nothing more needs to be said; in two or more variables the zero set of a single function is a surface, a curve or a higher-dimensional object that can have singular points, such as the cusp or the crossing lines in . The theory of complex-analytic subvarieties describes these sets: where they are manifolds, what their dimension is, how they decompose into irreducible pieces, and how large their singular part can be. It underlies the local theory of singularities, the study of holomorphic maps and their fibres, and complex-analytic geometry more broadly (see Chirka, Complex Analytic Sets, https://doi.org/10.1007/978-94-009-2366-9, and Gunning–Rossi, Analytic Functions of Several Complex Variables).
This mission formalizes the part of this theory developed in §6.5–6.7 of Jiří Lebl's textbook Tasty Bits of Several Complex Variables (version 4.4, 2026, https://www.jirka.org/scv/scv.pdf), culminating in the theorem that the singular set of a hypervariety (a subvariety of pure codimension one) is itself a subvariety, of dimension at most .
Throughout, is the space of -tuples , and a function on an open set is holomorphic if it is complex differentiable there.
A subvariety of an open set is a set such that every point has an open neighborhood and a family of holomorphic functions on , possibly infinite, with
The condition is imposed near every point of , so a subvariety is closed in .
A point is a regular point of dimension if, after a permutation of the coordinates, , there are open sets , and a holomorphic map with
one writes . The set of regular points is and the singular set is . The subvariety has pure dimension if at every regular point , and pure codimension if it has pure dimension . A subvariety of pure codimension one is a hypervariety. The dimension of is the maximum of over .
Local statements use germs. Sets , have the same germ at , written , if for some neighborhood of , and if . The ring consists of germs at of functions holomorphic near , and
is the ideal of germs vanishing on near , where . A germ of a subvariety is reducible if it is the union of two germs of subvarieties neither of which contains the other, and irreducible otherwise.
For an open set and a subvariety of pure codimension one,
The result itself. The goal theorem is the codimension-one case of the general statement that the singular locus of any complex-analytic subvariety is a subvariety of strictly smaller dimension (stated without proof in the book as Theorem 6.5.11). It makes induction on dimension possible for hypervarieties: removing the singular set leaves a complex manifold of dimension , and what is removed is again analytic and smaller. In particular, a complex curve in given by one equation has only isolated singular points. Theorem 6.6.1 says that hypervarieties are exactly the sets locally cut out by one function generating the full ideal of vanishing germs, which fails in higher codimension (Example 6.6.2 gives a codimension-two subvariety of not cut out by two functions).
Formalizing it. To our knowledge no proof assistant library currently contains complex-analytic subvarieties of open subsets of , their regular and singular points, or local dimension. Mathlib has schemes and Zariski-closed sets, which are algebraic and do not cover analytic sets such as , and it has germs of functions and one-variable zero sets of analytic functions. The mission therefore builds the basic vocabulary of local analytic geometry, and proves its first structural theorems, from the book's proofs.
Being a subvariety is a local condition near every point of , and the singular set is defined negatively, as the points where no coordinate projection exhibits as a graph. To show is a subvariety one has to produce holomorphic functions whose common zeros in are exactly the singular points. There is no natural finite list of them: the discriminants from one generic linear coordinate system do not suffice, because the book shows that near some regular points every fixed coordinate system sees a non-simple root (Figure 6.7). The proof needs infinitely many coordinate changes. It also needs Weierstrass preparation, the discriminant of a Weierstrass polynomial, and the principal-ideal description of Theorem 6.6.1. None of these are in Mathlib for convergent power series in several variables. The dimension bound is a separate claim: knowing that is a subvariety does not by itself exclude that it contains an -dimensional manifold piece.
Fin n → ℂ. Holomorphic on an open set is DifferentiableOn ℂ, which is equivalent to the book's Definition 1.1.2 on open sets. A domain is IsOpen U ∧ IsConnected U (nonempty).IsSubvariety U X includes IsOpen U and X ⊆ U; the families are arbitrary sets of functions.Fin n ≃ Fin k ⊕ Fin m for the permutation and the split into , , so no natural-number subtraction occurs.ℤ, and "" is "every regular point of has dimension " in ℤ. For the bound is , so the singular set must be empty. For the bound holds vacuously, where the book's maximum over the empty set is undefined.GermEq and GermSubset are the relations of Definition 6.1.3. is a Subring of Mathlib's Filter.Germ (nhds p) ℂ, and is an Ideal of it. "Generated by " is Ideal.span {(f,p)}.Infrastructure a complete development needs is Weierstrass preparation and division for convergent power series in several variables, the discriminant of a Weierstrass polynomial (Theorem 6.3.3), Noetherianity of , and the Riemann extension theorem. All of them can be reused well beyond this mission. Contributions of any of these are welcome, as are proofs of the milestones independently of the goal.
Local complex analytic geometry studies zero sets of holomorphic functions near a point. The natural algebraic object for this is the ring of germs of holomorphic functions at : two functions are identified if they agree near . The ring is the local ring of the complex manifold at in the sense of analytic geometry; its algebraic properties (Noetherian, integral domain, unique factorization) are what make the local theory of analytic varieties, their irreducible components and their singular sets work. This mission formalizes the section of Jiří Lebl's textbook Tasty Bits of Several Complex Variables (jirka.org/scv) that establishes these properties, together with the two tools they rest on, the Weierstrass preparation and division theorems.
The preparation theorem goes back to Weierstrass (published 1886). Rückert (1933) used preparation and division to prove that the ring of convergent power series is Noetherian, the starting point of the algebraic treatment of local analytic geometry.
A point of is ; when a last variable is singled out, with . A function on an open set is holomorphic if it is complex differentiable there; is the set of holomorphic functions on . A domain is a nonempty connected open set.
A germ at is an equivalence class of functions defined on neighborhoods of , two functions being equivalent if they agree on some neighborhood of . Germs of complex-valued functions form a commutative ring under pointwise operations of representatives. The ring of germs of holomorphic functions consists of the germs having a representative holomorphic on a neighborhood of .
For holomorphic near , write with homogeneous of degree . The order of vanishing is the least with , and if .
A Weierstrass polynomial of degree on an open in is a monic polynomial in ,
with coefficients holomorphic on and . A polydisc is a product of open discs. For a fixed , zeros of are geometrically distinct if they are distinct points; a zero is geometrically unique if it is the only one.
For every and ,
it is an integral domain, and up to multiplication by units and permutation every nonzero nonunit has a unique factorization into irreducible elements of .
In attack order:
with nowhere zero and a Weierstrass polynomial of degree with coefficients holomorphic in whose zeros in lie in for all ; and are unique. 2. Theorem 6.2.5 (Weierstrass division). For holomorphic near and a Weierstrass polynomial of degree , there are a neighborhood of and unique , a polynomial in of degree less than , with on . 3. Proposition 6.3.1. On domains , if for every the function has a geometrically unique zero , then is holomorphic in . 4. Theorem 6.3.3 (discriminant). For a bounded domain, a domain, whose zero set has no limit points on , there are and a holomorphic on such that has exactly geometrically distinct zeros in for and fewer than for . 5. Theorem 6.4.1. is Noetherian.
The preparation theorem reduces a holomorphic function near a point, after a unit, to a polynomial in one variable over the ring of functions of the others; the division theorem is division with remainder by such a polynomial. Together they turn in variables into an object controlled by the polynomial ring in variables, and that is how both the Noetherian property and unique factorization are proved. Unique factorization gives the decomposition of a germ of a hypersurface into irreducible components; the Noetherian property says that every germ of an analytic variety is cut out by finitely many functions. Proposition 6.3.1 and Theorem 6.3.3 describe how the zeros of move with , the input to the study of hypervarieties in the following sections.
The results are classical. The book proves them, leaving some steps as exercises: uniqueness in the division theorem (Exercise 6.2.10), the one-variable cases of 6.4.1 and 6.4.2 (Exercises 6.4.2, 6.4.6), and the irreducibility step in 6.4.2 (Exercise 6.4.7). Mathlib has the algebra (Noetherian rings, unique factorization monoids, Hilbert's basis theorem, the Gauss lemma for polynomial rings), germs along filters, and one-variable complex analysis. The platform has the Weierstrass preparation and division theorems for formal power series over complete local rings. None of the statements of this mission about convergent germs and holomorphic functions has a machine-checked proof.
The statements concern convergent objects, and the algebra alone does not see convergence. The formal preparation and division theorems produce a factorization or a quotient as formal power series; they do not say that the output converges, nor that it is holomorphic on a fixed neighborhood, nor where the zeros of the Weierstrass polynomial lie. Likewise, the formal power series ring is known to be a Noetherian UFD, but is a proper subring and neither property passes to subrings. The coefficients of the Weierstrass polynomial are built from the zeros of , which in general cannot be chosen continuously in (the two square roots of already show this), so the holomorphy of the coefficients cannot come from the zeros one at a time.
For the goal, the induction on requires identifying in variables, its polynomial ring, and a subring of in variables, and moving between germs and representatives on explicit neighborhoods. A linear change of coordinates is needed to reach the hypothesis of the preparation theorem, so invariance of under such changes is also part of the work.
Fin n → ℂ; where a last variable is singled out, is (Fin d → ℂ) × ℂ with , so is the case . Holomorphic on an open set is DifferentiableOn ℂ, which agrees with the book's Definition 1.1.2 on open sets.GermRing n p: the subring of Mathlib's germ ring (𝓝 p).Germ ℂ of germs with a representative complex-differentiable at every point near . The goal produces the IsDomain structure and asserts UniqueFactorizationMonoid; Theorem 6.4.1 is IsNoetherianRing.MvPowerSeries (Fin n) ℂ. Both change the theorem; convergence is the whole point.ℕ∞-valued: the least with nonzero -th derivative at , and if there is none.Set.encard. The book writes with ; the statement allows , since for without zeros no can satisfy the conclusion.A complete development needs the one-variable argument principle and Cauchy integral formula with holomorphic parameters, Newton's identities, Radó's theorem (for 6.3.3), Hilbert's basis theorem and the Gauss lemma (in Mathlib), and the identification of in variables with a subring of in variables. A general API for rings of holomorphic germs and their changes of coordinates is reusable in the next mission of this series (hypervarieties and their singular sets); contributions of it as standalone lemmas are welcome.
On a domain in with there is in general no Cauchy integral formula whose kernel is holomorphic in the evaluation point and independent of choices: the Bochner–Martinelli kernel works on every domain but is not holomorphic in the right variable. The Bergman kernel is the canonical replacement. It is attached to every domain , it reproduces every square-integrable holomorphic function on , and it is holomorphic in one variable and antiholomorphic in the other. Stefan Bergman introduced it in one and several variables in the 1920s–1930s (Bergman, The Kernel Function and Conformal Mapping, 1950). Aronszajn's theory of reproducing kernels (Aronszajn 1950) places it inside a general Hilbert-space framework. The kernel's boundary behaviour is the central tool in Fefferman's theorem that biholomorphisms between smoothly bounded strongly pseudoconvex domains extend smoothly to the boundary (Fefferman 1974).
This mission formalizes the construction of the kernel and its basic structure theory, following Chapter 5 of Jiří Lebl's Tasty Bits of Several Complex Variables (version 4.4, 2026).
Write for Fin n → ℂ and for Lebesgue measure on (volume). A domain is a connected open set . The space consists of the square-integrable functions on , modulo equality almost everywhere. It carries the inner product
The Bergman space bergmanSpace U is
It consists of those classes in that contain a function holomorphic on (DifferentiableOn ℂ). It is a linear subspace of and carries the norm . For and , denotes the value at of the holomorphic function in the class (holoRep U f z). This value is unambiguous because is open.
For , suppose there is an element with
Such a is unique (bergmanRepresenter U z). The Bergman kernel is then
In Lean, bergmanKernel U z ζ is : the second argument is itself, and pairs range over .
A family in , over an arbitrary index set , is a complete orthonormal system (IsCompleteOrthonormalSystem U φ) if it is orthonormal and its linear span is dense in .
Let be a domain and let be a complete orthonormal system for . Then
with uniform convergence on compact subsets of . In Lean the conclusion reads as follows: for every compact , the finite partial sums over converge to bergmanKernel U z ζ uniformly on as increases along the finite subsets of .
with integrable integrand. 3. Proposition 5.2.2 (p. 162). is holomorphic in and antiholomorphic in , and .
The result itself. The Bergman kernel can rarely be written in closed form. Proposition 5.2.5 computes it from any orthonormal basis of . For the unit ball, the normalized monomials give the closed form (Exercises 5.2.9–5.2.10). For the polydisc they give a product of one-variable kernels (Exercise 5.2.8). The expansion is also the standard route to the kernel's positivity on the diagonal, , and so to the Bergman metric. Lemma 5.2.1, the milestone underneath, is what makes a Hilbert space and point evaluation continuous. It is the reason a reproducing kernel exists at all.
Formalizing it. These results are classical and fully proved in the book. As far as a search of the platform shows, none of them has a machine-checked proof: Mathlib has spaces, Hilbert bases and the Riesz representation theorem, but no Bergman space. The platform's reproducing-kernel entries (Moore–Aronszajn, real-valued RKHS statements) start from a positive semidefinite kernel, which is the opposite direction and not about . What remains is to formalize the known proofs, and to build a reusable Bergman-space layer on which the biholomorphic transformation law (Exercise 5.2.7) and explicit kernels could later be stated.
The obvious argument for the goal expands in the orthonormal system. For each fixed , that expansion converges in in the variable only. Upgrading convergence to uniform convergence on compacts in needs Lemma 5.2.1. Uniformity in the pair is a further step: a bound for each fixed does not give it, and the tails must be controlled simultaneously in both variables. The sum is over an arbitrary index set, so the convergence to be proved is that of an unordered sum, uniformly on a compact set.
On the formal side, elements of are equivalence classes. Every pointwise statement therefore passes through the holomorphic representative, and needs the fact that continuous functions agreeing almost everywhere on an open set agree on it. Lemma 5.2.1 needs the mean-value property on polydiscs, and Cauchy–Schwarz on a polydisc inside . The kernel exists only once completeness of and the Riesz representation theorem are combined.
Fin n → ℂ with volume, the product of Lebesgue measures on ; this is . No Euclidean ball or norm appears in any statement, so the sup norm on Fin n → ℂ plays no role.IsOpen U ∧ IsConnected U. Holomorphic means DifferentiableOn ℂ on the open set , which is equivalent to the book's Definition 1.1.2 by Osgood's lemma (Proposition 1.1.3, Theorem 1.2.1).Submodule ℂ of Lp ℂ 2 (volume.restrict U), with the norm and inner product. Mathlib's inner product is conjugate-linear in its first argument. The book's is therefore written as an explicit integral wherever the order matters (the definition of ). Orthonormality does not depend on the convention.bergmanKernel U z ζ means . Compact subsets of in the variables correspond to compact subsets of in the variables .A complete development needs the following:
InnerProductSpace.toDual);HilbertBasis);The Bergman-space layer (holomorphic representatives, continuity of point evaluation, the kernel) is reusable for any later work on Bergman metrics, transformation laws or explicit kernels. Contributions of that layer as separate lemmas are welcome.
In one complex variable every open set is the natural domain of some holomorphic function: on a punctured disc cannot be continued across the puncture. In two or more variables this fails in a striking way. Hartogs observed in 1906 that a function holomorphic on the complement of a compact set inside a domain always extends across the hole (Hartogs, Math. Ann. 62, 1906). This Hartogs phenomenon is the first place where several complex variables departs from the one-variable theory, and it forces the notions of domain of holomorphy and pseudoconvexity that organize the rest of the subject.
Timeline. Hartogs's original argument (1906) had gaps. A complete proof was given by Fueter in 1939 for , and independently by Bochner and Martinelli for general in the early 1940s. The proof now standard, via the compactly supported -problem, is due to Ehrenpreis (Ehrenpreis, Bull. Amer. Math. Soc. 67, 1961). This mission follows the presentation in §4.1–4.3 of Lebl's textbook (Lebl, version 4.4, 2026).
Write for -tuples of complex numbers, . A domain is a nonempty connected open set. A function on an open set is holomorphic if it is complex differentiable there (for open sets this agrees with the textbook's definition by local boundedness and separate holomorphy).
The Wirtinger derivatives of a differentiable function are
and in one variable . A function is holomorphic exactly when all vanish.
A -form is an expression with coefficient functions . For a smooth , , so the equation is the system for all . Since mixed partial derivatives commute, a solution can exist only if the compatibility conditions hold.
In one variable, the area element is written , where is Lebesgue measure on .
Let , a domain, compact with connected, and holomorphic on . Then
where uniqueness means any two such extensions agree on .
The result. The Hartogs phenomenon shows that isolated singularities, and more generally compact singular sets, do not exist for holomorphic functions of several variables. Direct consequences include Corollary 4.3.2, the fact that the complement of a bounded domain of holomorphy is connected, and the extension of CR functions from the boundary of a bounded domain (the Hartogs–Bochner and Severi theorems). It is the reason the domain of a holomorphic function in carries geometric information, which leads to pseudoconvexity and the Levi problem. Theorem 4.2.1 is the simplest solvability statement for the -equation, a model for the Dolbeault and Hörmander theories.
Formalizing it. All results here are classical and proved in the book; none is formalized. Mathlib has the one-variable Cauchy integral formula on discs, but it has no Cauchy–Pompeiu formula, no Cauchy transform with a identity, and no -problem in . A complete development would provide a reusable one-variable solution operator, differentiation under a singular integral, and the removable-compact-set theorem for holomorphic functions of several variables.
The first idea, extending one complex line at a time by one-variable Cauchy integrals, works only for special shapes of (Hartogs figures): for a general compact with connected complement the one-variable slices of can be complicated, and patching slice-wise extensions into one holomorphic function is where the historical proofs had gaps. The milestones carry their own analytic difficulties. The kernel is singular, so the area integrals must first be shown to converge, and a -derivative cannot be moved naively under the integral (doing so would give , contradicting Lemma 4.4.6). In Theorem 4.2.1 the delicate point is compact support of the solution, which is where enters: for the equation is solvable but in general has no compactly supported solution.
Fin n → ℂ; functions are total, and only their values on the sets named in the hypotheses matter. Holomorphic is DifferentiableOn ℂ on an open set. A domain is IsOpen U ∧ IsConnected U. " compact" is IsCompact K ∧ K ⊆ U. The hypothesis is 2 ≤ n and is essential.wirtingerBar k f is built from real one-variable derivs; dbar f is its one-variable analogue. Smooth means real (ContDiff ℝ ∞), not analytic; compact support is HasCompactSupport.circleIntegral, and is times the Lebesgue (Bochner) integral over the disc. Integrability of the singular integrand is part of the conclusion, so a vanishing Bochner integral cannot make a statement hold vacuously.∃! among compactly supported smooth functions.In one complex variable every domain is the natural domain of some holomorphic function. In several variables this fails: there are open sets , , on which every holomorphic function extends past part of the boundary. The first example is the Hartogs figure (Hartogs, 1906). The question of which domains are natural domains of holomorphic functions, the domains of holomorphy, drove the development of the subject for half a century. E. E. Levi (1911) found a necessary condition for domains with smooth boundary: a sign condition on a Hermitian form attached to the boundary, now called the Levi form. The converse, the Levi problem, was settled in the 1950s by Oka, Bremermann and Norguet. Hörmander's approach is a later proof (Hörmander, An Introduction to Complex Analysis in Several Variables).
This mission follows §2.1–2.3 of J. Lebl, Tasty Bits of Several Complex Variables (version 4.4, 2026, jirka.org/scv). Those sections go from the Hartogs figure and the continuity principle, through tangent vectors and the Levi form of a smooth boundary, to the tomato can principle. That principle is the easy direction of the Levi problem: a domain of holomorphy with smooth boundary has no negative Levi eigenvalue.
Write for -tuples with , and . A function on an open set is holomorphic if it is complex differentiable at every point, and is the set of holomorphic functions on . is the polydisc of radius about , the set where every coordinate satisfies .
A domain is a nonempty connected open set. A domain is a domain of holomorphy if there are no nonempty open sets with connected, and such that every agrees on with some .
Identify with . An open set has smooth boundary if every has an open neighbourhood and a function with the following properties:
Such an is a defining function at . With the Wirtinger derivatives and , the holomorphic tangent space is
and the Levi form is the Hermitian form
is pseudoconvex at if there, and strongly pseudoconvex if on nonzero vectors. The inertia of is its number of positive and negative eigenvalues, the largest dimensions of subspaces of on which it is positive or negative definite.
If has smooth boundary, , and for some , then there is a connected open with
and, if is connected, is not a domain of holomorphy.
The tomato can principle is the necessity half of the solution of the Levi problem: pseudoconvexity is a local, computable condition on the boundary that every domain of holomorphy with smooth boundary satisfies. Together with its converse, it lets one decide whether a smooth domain is a domain of holomorphy by computing second derivatives of a defining function. The Hartogs figure and the continuity principle are the standard ways to extend holomorphic functions, and later chapters use them for the Hartogs phenomenon and for Hartogs pseudoconvexity. The invariance results make the Levi form's inertia a biholomorphic invariant of a boundary point. The normal form is the usual starting point for local computations in CR geometry.
All results are classical and proved in the source, except Proposition 2.3.6, which the book leaves as an exercise. None of them is formalized in Mathlib or on the platform: Mathlib has holomorphic functions of several variables, but no Hartogs extension, no Levi form and no pseudoconvexity. The platform's ray_hartogs is Hartogs's theorem on separate analyticity, a different result. The mission produces faithful statements of this chain, together with definitions of smooth boundaries, holomorphic tangent vectors and the Levi form that later missions of the series need.
The goal combines three independent pieces of machinery. The Hartogs figure needs holomorphy of Cauchy integrals over a torus with a holomorphic parameter, and the identity theorem on a polydisc. Reducing to the normal form needs the implicit function theorem for real hypersurfaces, second-order Taylor expansion in Wirtinger coordinates, a polynomial holomorphic change of coordinates, and Sylvester's law of inertia. The inertia results need the chain rule for Wirtinger derivatives of , and the fact that two defining functions differ by a positive smooth factor. That last fact is itself a division lemma for smooth functions vanishing on a hypersurface.
The naive formalization of "the Levi form has a negative eigenvalue" as a negative eigenvalue of the complex Hessian on all of is wrong. The complex Hessian changes under the choice of defining function, and only its restriction to has invariant signs.
is Fin n → ℂ. Its Mathlib norm is the sup norm, so Metric.ball p s is exactly the polydisc . No Euclidean ball occurs in these statements. Holomorphic on an open set is DifferentiableOn ℂ, which is equivalent there to the book's Definition 1.1.2. Functions are ambient maps whose values off the relevant set are irrelevant.
Smooth means ContDiffOn ℝ ∞ on the open neighbourhood . Real partial derivatives are fderiv ℝ in the directions and , and Wirtinger derivatives are built from them. is the submodule holTangent r p of coefficient vectors, computed from the defining function in use. The Levi form is compared through its real part. The inertia is the pair leviPosIndex, leviNegIndex: suprema over ℕ of dimensions of definite subspaces, nonempty (the zero subspace) and bounded by . The book's is VanishesToOrder 3: the function and its derivatives of order at most two vanish at the point. It is not Mathlib's IsBigO.
Conventions and restrictions:
A trivializing formalization is excluded: the Levi form is restricted to holTangent r p, never the full complex Hessian, and the defining function must carry the sign condition. So neither a hypothesis that fails for every open set nor one that holds for every open set can make the goal vacuous or trivial.
A complete development needs parameter-dependent Cauchy integrals on polydiscs, a real implicit function theorem for hypersurfaces, a smooth division lemma, a Wirtinger chain rule, and Sylvester's law of inertia for Hermitian forms restricted to subspaces. These pieces are reusable across the series, and contributions of any of them are welcome.
Many systems of first-order partial differential equations arising in physics — linear acoustics, Maxwell's equations, linearized gas dynamics, the Tricomi equation of transonic flow — can be written as symmetric systems with symmetric coefficient matrices . K. O. Friedrichs showed in 1958 (Friedrichs 1958) that a single energy argument gives existence and uniqueness for boundary value problems of this form under positivity conditions on the equation and the boundary condition, regardless of whether the system is elliptic, hyperbolic or of mixed type. The theory is the subject of Chapter 8 of J. K. Hunter's Notes on Partial Differential Equations (UC Davis, revised 6/18/2014), which this mission follows.
The core analytic tool of the theory is older. In 1944 Friedrichs introduced mollifiers precisely to prove that weak and strong extensions of differential operators coincide (Friedrichs 1944); the key estimate is a bound on the commutator of a mollifier with a first-order operator with Lipschitz coefficients. Lax and Phillips (1960) developed the boundary version for dissipative symmetric operators.
Write points of as and give its Euclidean norm . Let be matrix-valued coefficients. The first-order operator and its formal adjoint are (summation over )
A mollifier profile is a , compactly supported, non-negative, radially symmetric with . For set and define the smoothing operator . The commutator is defined for .
For the boundary value problem, is a bounded open set with -boundary, its outward unit normal, and the problem is
with boundary matrix . The system is positive symmetric with constant if the are symmetric and in . The boundary condition is maximally positive if is nonsingular on and there is a matrix function on with , and . A weak solution with data is with for every .
Let and . For each the commutator extends to a bounded operator on , and
The goal asserts only the shape: a uniform bound exists, with no value fixed.
Under the smoothness, positivity and maximal positivity conditions above, with the norm,
smooth solutions are unique; and for every a weak solution exists.
The commutator lemma is what turns weak solutions into strong ones: mollifying a weak solution produces smooth functions that solve the equation up to an error , and the lemma says this error vanishes in the limit. Friedrichs' "weak equals strong" theorem (Theorem 8.12 of the notes), the uniqueness of weak solutions (Corollary 8.13), and much of the theory of hyperbolic systems and pseudo-differential commutator estimates rest on it. The energy estimates of Theorem 8.6 and the existence theorem 8.9 are the two halves of the Friedrichs theory that do not need mollification: an a priori bound for smooth functions satisfying the boundary condition, and existence by duality.
All of these results are classical and proved. As far as a search of the platform and of Mathlib shows, none is formalized: Mathlib has convolution, ContDiffBump mollifiers and spaces, but no commutator estimates, no divergence theorem on domains, and no Friedrichs systems. The mission would produce the first machine-checked commutator estimate for mollifiers and first-order operators with Lipschitz coefficients, and the first formal treatment of positive symmetric boundary value problems.
The obvious argument for the goal — bound and separately — fails: each term involves , which is not controlled by , and each is of size after moving the derivative onto . Only the difference is bounded, and only because the coefficient difference is of size on the support of . The cancellation between the two terms is the whole content of the uniform bound. Convergence to zero on smooth compactly supported is easy, but it does not by itself give convergence on all of .
For the milestones, the central difficulty is Green's theorem: the energy identity requires the divergence theorem on a bounded domain for vector fields, with the outward normal and surface measure, none of which Mathlib provides for general domains.
EuclideanSpace ℝ (Fin n) and EuclideanSpace ℝ (Fin m), so is Euclidean and is Lp (EuclideanSpace ℝ (Fin m)) 2 volume. Coordinates are 0-based: A i is .T : ℝ → (L² →L[ℝ] L²). "Extends" means: for and every , T ε applied to the class of agrees a.e. with the pointwise commutator. Because is dense in , this pins down each T ε; a bound stated on only would be weaker than the lemma and is not what is asked.ContDiff ℝ ∞ (smooth, not analytic).eLpNorm · 2 in , so no integrability condition is hidden in the estimates.Needed infrastructure: Young's convolution inequality on , density of in , differentiation under the convolution integral, and, for the milestones, the divergence theorem on bounded domains together with the Riesz representation theorem. The divergence theorem on domains, and the commutator estimate itself, are reusable well beyond this mission. Contributions of any of these are welcome.
Hyperbolic partial differential equations model waves: acoustic, elastic, electromagnetic and gravitational. Their qualitative behaviour differs sharply from that of parabolic equations. They have finite speed of propagation, they are reversible in time, and they do not smooth their data: a singularity in the initial state is transported, not damped. The analytical consequence is that energy estimates for hyperbolic equations are weaker than for parabolic ones, and the existence theory has to be run in spaces that carry exactly one derivative's worth of information.
This mission formalizes the energy-space well-posedness theory for linear second-order hyperbolic equations with time-dependent coefficients, following Chapter 7 of J. K. Hunter's lecture notes Notes on Partial Differential Equations (UC Davis, revised 6/18/2014). The same theory appears in L. C. Evans, Partial Differential Equations, §7.2, and goes back to the Galerkin and energy methods of J.-L. Lions and E. Magenes.
Let be a bounded open set and . A test function is a smooth function with compact support in ; the Sobolev space is the closure of the test functions in the norm , where is the weak gradient. carries the inner product , and is the dual space with pairing . There are embeddings .
The operator is
with bilinear form on , and is the same form built from the time derivatives , . Assumption 7.1 requires , , and uniform ellipticity: for some .
A vector-valued function has weak time derivative if for all test functions on , the integrals being Bochner integrals. The problem is
A weak solution (Definition 7.2) is a function with weak derivatives , such that , , , and for every
with and .
Under Assumption 7.1 there is a constant , depending only on , and the coefficients, such that for every , , there is a unique weak solution, and
and the energy is absolutely continuous.
Theorem 7.3 is the basic well-posedness result for linear wave equations in inhomogeneous, time-dependent media in the natural energy space. It is the starting point for the regularity theory of such solutions, for finite-speed-of-propagation arguments in a weak setting, and for fixed-point constructions for semilinear wave equations, which linearize around a known solution and need exactly this estimate with a constant depending only on the coefficients. Lemma 7.8 and Lemma 7.10 are general tools that recur in evolution equations: the first converts uniform-in-time bounds into weak continuity, the second justifies an energy identity for solutions too rough to differentiate directly.
The results are classical and fully proved in the literature, and to our knowledge no machine-checked version exists. Formalizing them requires vector-valued Sobolev spaces in time, Bochner-integral weak derivatives and duality arguments. These are largely absent from Mathlib and would be reused by any formal treatment of evolution equations, parabolic ones included.
The obvious approach, testing the equation with to obtain energy conservation, is not available for weak solutions: lies only in , not in , so the pairing is undefined. This affects both halves of the theorem. For existence, the energy estimate holds only for the finite-dimensional approximations, and the limit is obtained in weak-star topologies of in time, which give neither continuity in time nor the initial conditions directly. For uniqueness, a different test function is needed. The continuity requirements of Definition 7.2 are an essential part of the statement, not a technicality, and establishing them for the constructed solution is a large part of the work.
EuclideanSpace ℝ (Fin n) with Lebesgue measure; coordinates are 0-based. is modelled by jets : the closure of in , with norm exactly . is StrongDual ℝ (H10 n Ω), and acts by .ℝ≥0∞-valued (eLpNorm, ‖·‖ₑ), and the constants are finite (ℝ≥0). Each constant is quantified before the data ; in Proposition 7.6 it also precedes the eigenbasis and .A complete development needs Bochner-valued Sobolev spaces on an interval, Banach–Alaoglu in , linear ODE systems with coefficients, Gronwall's inequality, and the spectral theory of the Dirichlet Laplacian. The time-dependent function-space layer is reusable for parabolic and Schrödinger-type equations. Contributions of general lemmas on vector-valued weak derivatives are welcome.
Reaction–diffusion equations are the standard model for the interplay of diffusion with local growth or decay: chemical kinetics, population dynamics, and the bifurcation of equilibria of partial differential equations. The special case
(the Chafee–Infante equation on bounded domains, Chafee and Infante 1974) is the model equation for loss of stability: is linearly stable for and unstable for , and for , the reaction term produces a supercritical pitchfork bifurcation. Before any of that dynamics can be studied, one needs solutions to exist. §5.5 of J. K. Hunter's Notes on Partial Differential Equations (UC Davis, revised 6/18/2014) proves local existence by rewriting the equation as an integral equation and applying the contraction mapping theorem. This argument, the "mild solution" method of Kato and Segal, is the template for local well-posedness of semilinear parabolic and dispersive equations (Pazy 1983, Henry 1981).
Write for Euclidean space with Lebesgue measure. For the Fourier transform is , defined by this formula on Schwartz functions and extended to by Plancherel's theorem. For , the Sobolev space consists of the with finite norm
The heat semigroup , , is the Fourier multiplier . For it is convolution with the heat kernel .
Fix and an integer , and let act pointwise on functions. The initial value problem is
Write for the curves that are continuous on in the norm, normed by . A mild solution on with values in is a curve satisfying the Duhamel formula
The right-hand side, viewed as a function of , is the map .
Let and . For every there is , depending only on , such that for every with , (5.34) has a mild solution , and any two mild solutions on coincide.
where all norms are in and depends on .
The theorem is the base case of the semigroup approach to nonlinear evolution equations. The existence time depends only on the size of the data, so an a priori bound on upgrades local existence to global existence. The same scheme, with for a sectorial operator , covers general semilinear parabolic problems. The smoothing estimate and the fractional Sobolev embedding are also used separately, in parabolic regularity theory and in the analysis of dispersive equations.
The results are classical and proved in the notes. None of them has a machine-checked proof on this platform. Mathlib has the Fourier transform and Plancherel's theorem, tempered distributions, and a Bessel-potential definition of Sobolev spaces, but no fractional Sobolev embedding on and no mild-solution theory for semilinear heat equations. The mission asks for complete formal proofs of the three milestones and the goal, stated for the concrete objects above.
The obvious fixed-point argument needs three separate analytic inputs. The first is that the operator norm of blows up like , which is integrable only because . The second is that is locally Lipschitz from to , which needs the embedding and fails for . The third is that the Duhamel integral defines a continuous -valued curve even though its integrand is singular at . With these in hand, the contraction must be run on a ball whose radius is fixed by the data, with chosen uniformly over that ball. Uniqueness is claimed in all of , not only in the ball where the contraction runs, so an extra argument is needed to exclude solutions that leave the ball.
EuclideanSpace ℝ (Fin n) with volume. The solution and the data are real-valued. Theorem 5.79 and Lemma 5.50 are stated for complex-valued functions. A curve is a map ℝ → (ℝⁿ → ℝ), and only its values on matter.Lp.fourierTransformₗᵢ (kernel , no prefactor) as . Mathlib's constants are never used for the book's.hsNorm is valued in and is off , so means hsNorm n s f < ⊤. The factor is inside the square root, as in the book's inner product and in its proof of Lemma 5.50. Definition 5.74 prints it outside, which is inconsistent with both. With this choice .Many control tasks come with a deadline: a consensus protocol or a regulation task must reach its target by a time fixed in advance, whatever the initial condition. Prescribed-time stabilization asks for a feedback law that brings every trajectory of a control system to the equilibrium by a user-chosen time . The basic test case is the chain of integrators , the normal form of every single-input feedback-linearizable system.
Two routes to prescribed-time stabilization exist. Time-varying gains that blow up as (Song, Wang, Holloway and Krstić, Automatica 2017) are fragile under measurement noise. Fixed-time stabilization gives a settling time bounded uniformly over all initial conditions, and a time rescaling then turns the uniform bound into any prescribed . Chitour, Ushirobira and Bouhemou (SIAM J. Control Optim. 2020) follow the second route with an explicit, continuous feedback. It combines Hong's backstepping homogeneous controller (Systems Control Lett. 2002) with a degree of homogeneity that depends on the state (Harmouche, Laghrouche, Chitour and Hamerlain, Int. J. Control 2017). A continuity device of Lopez-Ramirez, Efimov, Polyakov and Perruquetti (Int. J. Robust Nonlinear Control 2018) makes that degree a continuous function of the state. This mission formalizes the construction and its main results, §4.1–4.2 of the paper.
Fix and write with the Euclidean norm. Let be the -th Jordan block (, ). The pure chain of integrators (31) is
For and write . Given gains and , set and . Define and
The homogeneous feedback is (Definition 23). The associated Lyapunov function is
and (36) is the decay inequality , with and one constant for all in the range.
For and , the state-dependent degree of (49) equals where and where , and it interpolates linearly in in between. The closed-loop controller is . With , let be the largest with , and the smallest with . Set
Finally is the dilation of (5).
A system is globally fixed-time stable with settling time at most if the origin is an equilibrium, solutions exist from every initial state, it is Lyapunov stable, and every solution vanishes for all (Definition 1 with ).
Let the gains and satisfy (36). There are and such that, for every and every with
the feedback makes (31) globally fixed-time stable with settling time at most .
The result gives a static, continuous state feedback for the chain of integrators with an explicit settling-time bound. It is robust to a bounded uncertain input gain, and the rescaled controller meets any prescribed deadline. Unlike time-varying designs, the gains stay bounded, which is what the paper's ISS analysis in §4.3 builds on. The constants in (52) are explicit in terms of and the radii , so the rescaling factor is computable.
The results are proved on paper; no machine-checked proof is known. A formalization would check the parameter bookkeeping of the construction: index shifts, exponents, the three-phase settling-time estimate, and the interplay of two different dilations. It would also produce reusable definitions of Carathéodory solutions and of finite-, fixed- and prescribed-time stability, which the platform does not yet have.
The obvious argument uses the Lyapunov function for the varying-degree controller. That fails: depends on , so acquires a term from the derivative of . The proof instead handles three regions separately, with outside , on the shell , and inside . On the shell the controller is a perturbation of the linear one, and bounding that perturbation needs uniform Hölder estimates in (Lemmas 31–32). The closed loop is only continuous, so solutions need not be unique and every stability claim is about all solutions. Proposition 24 itself is a recursive gain construction whose constants must be uniform in .
States are EuclideanSpace ℝ (Fin n); the paper's index is j.val + 1. Solutions are Carathéodory solutions on in integral form, with integrability stated. Every stability property quantifies over all solutions, and existence of a solution from each initial state is part of Lyapunov stability. is read as ; the paper never defines it. is the Fréchet derivative applied to the vector field. and are the supremum and infimum of the admissible radii.
Hypotheses and readings that differ from the page:
A formalization in which (36) is dropped, or is chosen freely, or a trajectory is only required to exist, would be trivial or false. Any trivializing reading of this kind is ruled out: stability is required of every solution, and is tied to (36).
Needed infrastructure: signed powers and their Hölder estimates (42), differentiability of , weighted homogeneity, Carathéodory existence for continuous right-hand sides, and comparison lemmas for . The stability definitions and the comparison lemmas are reusable beyond this mission. Contributions of any of these are welcome.
Servers in manufacturing lines, communication links and service systems break down, are taken offline for maintenance, or go on vacation. When the interruptions are rare but long, they dominate congestion. A single down period can build a backlog that takes a long time to clear, and in a network that backlog propagates downstream. Standard heavy-traffic diffusion approximations, which describe queue lengths by reflected Brownian motion, do not capture this effect.
Chen and Whitt (Queueing Systems 13, 1993) identify a regime in which the effect survives in the limit. Up times are of order and down times of order , while the load is within of capacity. Under the diffusion scaling each down period then becomes a jump, and the limit of the queue-length process is a reflected jump-diffusion. The paper generalises the single-station result of Kella and Whitt (Adv. Appl. Probab. 22, 1990; reference [22] of the paper) to open networks.
Timeline:
A network has single-server stations. Customers arrive from outside station according to a counting process . Station completes services in its first units of busy time. The th departure from station is routed to station when the indicator , and counts such departures. Station alternates up periods and down periods , starting up, and is its cumulative down time in . With a work-conserving discipline, the queue length and the busy time satisfy
and the idle time is .
The reflection map associated with a matrix takes a path to the pair with , nondecreasing, and increasing only when .
A sequence of networks is indexed by . The arrival, service and routing processes satisfy functional central limit theorems with rates and at speed . Up and down times scale as . The network is balanced, , with the routing matrix. The limit down time is the sum of over the up periods completed by time , which is a pure-jump process.
The topology on paths with jumps compares completed graphs, in which each jump is filled in by the straight segment from to , through their monotone parametrisations.
For a single station with feedback probability , with , , and ,
Here , and , with and
The paper states Theorem 4.1 for stations, with the analogous formulas and . The mission's goal is its case (see Formalization scope).
The theorem yields a tractable approximation for networks with rare long interruptions: a reflected Lévy-type process driven by a Brownian part and a compound jump part. Its distribution can be studied through the reflection map. The jump directions make explicit how an outage at one station drains its downstream stations while its own queue builds up. Remark (4.3) of the paper derives a diffusion analogue of Little's law from the same limit.
The theorem is proved in the paper, and no part of it has been formalized. A formalization would produce the first machine-checked topology on paths with jumps, a heavy-traffic limit theorem for a queueing network, and the random-time-change argument for counting processes.
The obvious argument chains three facts: the primitive processes converge, hence so does the scaled free process , and the reflection map is continuous. Two steps break. First, subtraction is not continuous in when the two paths jump at the same time in opposite directions, so the joint convergence of across stations needs (4.11) and one common parametrisation. Second, the reflection map is Lipschitz in the uniform topology, but the uniform topology cannot see jumps that occur at nearby times. Carrying the convergence through the reflection map in the topology requires controlling how the regulator and the regulated process move along each jump segment of , jointly for all coordinates.
Stations are Fin J; the network index is n : ℕ, and only enters. Durations are indexed from in Lean. The queue length is integer valued, (3.2) is computed in , and a solution satisfies .
A trivializing formalization is excluded. The hypotheses are satisfiable (for example by deterministic arrival and service processes), is used only when , and laws are compared only for measurable path maps.
Needed infrastructure: the Skorohod space with the topology and its characterization on , continuity of addition and of composition with continuous time changes, the multidimensional reflection map on paths with jumps, and a Skorohod representation argument. Proofs of Lemma 4.1 and Lemma 4.2 are welcome independently.
Many engineered systems switch between a finite number of operating modes at random times: a power grid after a line failure, a networked controller whose links drop, a manufacturing plant whose machines break down and are repaired. A standard model for such systems is a hybrid stochastic differential equation, also called an SDE with Markovian switching: the state follows an Itô equation whose coefficients depend on a mode that evolves as a continuous-time Markov chain. The monograph of Mao and Yuan (Stochastic Differential Equations with Markovian Switching, 2006) develops the stability theory of these equations.
A controller that stabilizes such a system usually needs the current state. In practice the state is sampled: it is observed at times and the control is held between observations. Mao (Automatica 49, 2013) showed that, under a global Lipschitz condition on the drift and diffusion, a feedback control based on discrete-time observations makes a hybrid SDE mean-square exponentially stable when is small enough. You, Liu, Lu, Mao and Qiu (SIAM J. Control Optim. 53(2), 2015) replaced that condition by local Lipschitz continuity plus linear growth, gave an explicit bound (3.5) on the admissible observation interval, and proved -stability, asymptotic stability, and, in Section 4, exponential stability in mean square and almost surely with an explicit rate. This mission formalizes that exponential stability result, Theorem 4.2, and the steps of its proof.
Let be a probability space with a filtration satisfying the usual conditions (increasing, right-continuous, contains the null sets). On it live an -dimensional -Brownian motion and a right-continuous -Markov chain on with generator ( for , zero row sums), independent of . Fix and the sampling time . The controlled system is
with and .
The hypotheses are:
Put , (positive by (3.5)), and
In Lean these are Assumption21, Assumption22, C21, LU, Assumption31, Assumption41, Condition35, theta, lam, H1, H2, rateEquationLHS; the basis is HybridSetup, the Itô integral IsItoIntegral, the sampling time delta, solutions SolvesSampledHybridSDE, and the functional (4.7) Vbar, all in the namespace You2015.Expo.
Under the hypotheses above, the equation
has a unique root , and every solution of (2.1) satisfies
for all , .
The result. Theorem 4.2 gives a quantitative guarantee: a controller that samples the state every units makes the switching system decay exponentially, with a rate computable from the constants of the assumptions. Asymptotic stability (Section 3 of the paper) says nothing about how fast trajectories settle; the rate is what a designer trades against the sampling cost when choosing . The almost sure statement concerns individual trajectories, which is what an operator observes.
Formalizing it. The results are proved in the paper; none of them is machine-checked. Mathlib has real Brownian motion but no Itô integral, no stochastic differential equations and no continuous-time Markov chains. The mission therefore also produces a definition layer: a filtration under the usual conditions, a multidimensional -Brownian motion, an -Markov chain with a given generator, the Itô integral of vector-valued integrands, and the solution notion of an SDE with Markovian switching and a sampled-state delay. A related but different layer exists on Prove2Me for Ethier–Kurtz (EthierKurtz_IsStandardBrownian, EthierKurtz_HasBrownianItoIntegral, EthierKurtz_SolvesBrownianSDE); it has no mode switching and no sampled state, so it cannot express (2.1). Formalization also checks the constants: it found that the printed in (4.5) disagrees with the paper's own derivation (see below).
Equation (2.1) is a stochastic differential delay equation whose delay is bounded but jumps at every observation time, so the delay-equation stability theorems that require a differentiable delay with derivative below one (Mao–Yuan, p. 285) do not apply. A Lyapunov function of the current state alone leaves the term , which has no sign and depends on the path over a whole observation interval. An exponential rate requires controlling this delay term with an exponential weight, and the weight inflates the delay contribution by a factor ; the rate equation (4.4) records exactly this balance. The almost sure part does not follow from the mean-square part by Chebyshev's inequality at fixed times alone: a pathwise bound needs control of the supremum of over each unit interval, which involves the martingale part of the solution.
Conventions committed to in Lean:
EuclideanSpace ℝ (Fin n), so is the Euclidean norm; the explicit constants in (3.5), (3.21), (4.5) depend on it. The diffusion is given by its columns and (trace norm). Modes are Fin N (0-based). Time is ℝ≥0; time integrals are over subsets of at s.toNNReal.Real.log 0 = 0 never enters. In (4.3) the almost-sure quantifier is outside the quantifier over .A trivializing formalization is ruled out: the expectations are not Bochner integrals, is never evaluated, the goal asserts that the rate equation has exactly one positive root (so the stability clauses are not vacuous), the solution notion admits the true solution and requires path continuity, and the derivative witnesses of are tied to . A sorry-free local check confirms that Assumptions 2.1, 2.2, 4.1, condition (3.5) and hold for , , , , , , , , ; for these data by hand.
Welcome contributions: the Itô isometry and Itô's formula for the integral defined here, a generalized Itô formula for functions of a Markov-modulated Itô process, the Burkholder–Davis–Gundy inequality, and the Borel–Cantelli argument that turns mean-square exponential decay into almost sure decay. These are reusable far beyond this mission. Section 3 of the paper (asymptotic stability) is a separate mission of the same series.
A Russian option is a perpetual American-type claim that pays, when the holder exercises at time , the maximum of the asset price seen so far, discounted by . It was introduced by Shepp and Shiryaev for the Black–Scholes market (Shepp–Shiryaev 1993), where the underlying log-price is a Brownian motion with drift. Empirical work on asset returns (skewness, heavy tails, downward jumps) motivates replacing the Brownian motion by a Lévy process with negative jumps only. Avram, Kyprianou and Pistorius (2004) solve the Russian optimal stopping problem in that model in closed form, in terms of the scale functions of the process.
Timeline. 1993: Shepp and Shiryaev solve the Russian problem for geometric Brownian motion; Duffie and Harrison give its no-arbitrage price. Graversen and Peskir, and Kyprianou and Pistorius, treat further variants within the Black–Scholes market (the works the paper cites in §6). 2004: Avram, Kyprianou and Pistorius solve it for every spectrally negative Lévy process, covering both unbounded and bounded variation, using the exit problem of the reflected process (their Theorem 1, the subject of the first mission of this series).
Let be a filtered probability space with a right-continuous filtration, and a spectrally negative Lévy process for : , càdlàg paths with no positive jumps, independent and stationary increments with independent of , and paths that are not monotone. The standing assumption of the paper is that has unbounded variation, or bounded variation and a Lévy measure absolutely continuous with respect to Lebesgue measure.
The Laplace exponent is , and is the largest root of . For the -scale function is the unique function that vanishes on , is continuous on , and satisfies for . Then . The tilted scale functions are those of the exponent .
Fix with (the risk-neutral condition), and let be the Esscher measure, . For , under the process starts at with running maximum , and the reflected process starts at . The passage time is . Fix and put .
The Russian optimal stopping problem (28) is
the supremum over all -almost surely finite -stopping times. The option price is .
With the optimal level (30) and the candidate value
for every ,
and is a -a.s. finite -stopping time.
The result. Theorem 2 gives the price of the perpetual Russian option and its optimal exercise rule for every exponential spectrally negative Lévy market. The rule is to exercise when the ratio of the running maximum to the current price first reaches . The level is explicit through scale functions, and it separates the regimes: for bounded variation with , immediate exercise is optimal. The theorem is the model case of a general method: an optimal stopping problem for a functional of is reduced, by a change of measure, to one for the reflected process, and solved by verification. The same method underlies the Canadized Russian option (third mission of the series).
Formalizing it. The result is proved in the paper; it has no machine-checked proof. This mission produces a Lean statement of the full verification theorem, including admissibility of . It also states the analytic facts about scale functions that the proof relies on (Lemmas 1, 2 and Remarks 3, 4), which apply to any problem phrased in scale functions.
The obvious route is the classical verification: show that is a supermartingale, apply optional stopping, and check equality at . The first step fails as a direct Itô computation. In the unbounded-variation case is only at , and in the bounded-variation case only continuous there. The generator of is nonlocal, so smoothness away from does not control the jump part of the process across the boundary. The equality case needs the exact value of stopping at (Corollary 1). That value requires the overshoot of over , which is caused by a downward jump of , and the exit problem of the reflected process. Finally, is not equivalent to on , so passing from -facts to -facts is valid only on each .
Conventions committed to in Lean:
ℝ≥0) and values are real. Random times take values in (WithTop ℝ≥0), and the payoff is set to on , a -null event for admissible .Function.rightLim, and is the real infimum (30); its nonemptiness is Lemma 2, not a hypothesis. extends the paper's , .A trivializing formalization is ruled out: the supremum ranges over every -a.s. finite stopping time of the given filtration (not only passage times, not a smaller filtration), and it is taken in , where no junk value of an unbounded real supremum can occur.
Infrastructure a complete development needs: Lévy processes on path space, their Laplace exponents and Esscher transforms, scale functions (existence, uniqueness, smoothness under the standing assumption), the reflected process and the exit identity of Theorem 1, optional stopping for continuous-time supermartingales, and Itô/change-of-variables formulas for semimartingales with jumps. The scale-function and Esscher layers are reusable for the other missions of this series and for any fluctuation-theory problem. Contributions to any of these layers, or to the milestones separately, are welcome.
Stochastic approximation is the family of recursive algorithms that locate a zero of a vector field from noisy evaluations of it. Temporal-difference learning, Q-learning, actor–critic methods and stochastic gradient descent are all instances. In practice these algorithms are often run with a constant or bounded, non-vanishing stepsize: the iterate keeps adapting to new data and never freezes, at the price of never converging exactly. The natural question for such a scheme is quantitative: how far from the target does the iterate stay in the long run, and how does that distance scale with the stepsize?
Borkar and Meyn (SIAM J. Control Optim. 38(2), 2000) answer both halves of the question under one set of hypotheses. First, stability of a "fluid" ODE obtained by scaling at infinity implies that the iterates have bounded second moments, with no a priori boundedness or projection assumption. Second, if the ODE has a globally exponentially stable equilibrium , the asymptotic mean-square error is of the order of the largest stepsize. The first result replaced the usual stochastic-Lyapunov-function verification in reinforcement-learning applications (Section 3 of the paper). This mission formalizes the bounded-stepsize branch of the paper. A companion mission (… I: Stability and Almost-Sure Convergence under Tapering Stepsizes) covers the vanishing-stepsize branch.
Fix and a Lipschitz vector field . The stochastic approximation recursion (1.1) is
with a deterministic step sequence and a noise sequence on a probability space . The associated ODE (1.2) is .
An equilibrium of (1.2) is globally asymptotically stable if it is Lyapunov stable and attracts every solution. It is globally exponentially asymptotically stable if there are and with for every solution.
The proofs compare the iterates with ODE solutions on a time grid: , blocks of length about , the interpolated path of the iterates, its rescaled version with , and the ODE solutions , restarted at each block.
Under (A1), (A2) and (BS), if is a globally asymptotically and globally exponentially asymptotically stable equilibrium of (1.2), there are and such that for all and every initial condition ,
The constant is uniform in the stepsizes and in . No rate constant is fixed: only the linear dependence on is asserted.
The result. Theorem 2.1(ii) says that a stability property of a deterministic ODE at infinity controls a stochastic recursion in mean square, uniformly over initial conditions. Theorem 2.3(ii) turns this into an error bound: with a non-vanishing stepsize the iterate does not converge, but its mean-square distance from is eventually . This is the quantitative justification for constant-stepsize stochastic approximation in reinforcement learning and adaptive control, and it is the starting point of the trade-off between bias (small stepsize) and speed (large stepsize) discussed in Section 2.2 of the paper.
Formalizing it. The results are proved in the paper, partly by sketch: Lemma 4.8's proof refers to "familiar arguments using the Bellman–Gronwall lemma", and the paper writes several bounds as . A formal proof makes every constant and its dependence explicit, which the paper's quantifier order leaves partly implicit (see the scope section). No machine-checked proof of these results, or of any stochastic-approximation stability theorem in this generality, is known to exist.
The natural first argument, that the iterates track the ODE and the ODE converges, needs the iterates to be bounded. Bounded iterates are exactly what is being proved, so the argument is circular. The paper breaks the circularity by rescaling: on each block the iterate is divided by , so that on large scales it tracks the fluid ODE, whose stability contracts the norm by a fixed factor per block. Making this work in mean square requires conditional second-moment estimates that are uniform in the stepsize and the scale (Lemma 4.7). A second difficulty is that the stepsize does not vanish: the tracking error per block does not go to zero, and the goal's content is precisely that it is of order with a constant that does not depend on .
EuclideanSpace ℝ (Fin d). ODE solutions are forward solutions: continuous on with right derivatives. Stability notions are the standard ones, with exponential stability in the form the proof of Theorem 2.3(ii) uses.Useful infrastructure, reusable beyond this mission: Bellman–Gronwall inequalities in discrete time (Lemma 4.3 of the paper), stability of scaled ODEs, and conditional second-moment estimates for martingale-difference-driven recursions. Contributions of any of these as separate lemmas are welcome.
An insurance company's surplus in the Cramér–Lundberg model grows linearly with premiums and falls by claims arriving as a compound Poisson process. When premium income exceeds the expected claims, the surplus drifts to infinity. De Finetti (1957) proposed that the surplus above a barrier should instead be paid to shareholders as dividends, and the resulting optimal dividend problem — maximize the expected discounted dividends — is a central problem of risk theory. A barrier policy, however, drives the surplus below zero with probability one. Harrison and Taylor (1978) and Løkka and Zervos studied, for Brownian motion, a variant with bail-out loans: ruin is forbidden, and the shareholders must inject capital whenever the surplus would become negative, at a cost per unit.
Avram, Palmowski and Pistorius (Ann. Appl. Probab. 17 (2007)) solved the bail-out problem when the surplus is a general spectrally negative Lévy process, which includes the Cramér–Lundberg model, Brownian motion with drift and their sums. They showed that the optimal policy is a double barrier policy for every initial capital. This mission formalizes that result, Theorem 3 of the paper.
Timeline:
A spectrally negative Lévy process on a filtered probability space starts at , has càdlàg paths, is -adapted, and has stationary increments with independent of . Its jumps are all negative, and for , where the Laplace exponent is
With initial capital the surplus is . The standing assumptions are: does not have monotone paths; (so is finite); , or , or has a density (condition (3.3)).
A policy consists of nondecreasing adapted processes with : cumulative dividends (left-continuous) and cumulative injected capital (right-continuous). The controlled surplus is . The policy is admissible if for and almost surely. Its value and the value function are
with discount rate and cost . The double-barrier strategy pays out at once and then the minimal dividends and injections that keep in : is carried by and by .
The -scale function vanishes on , is continuous and nondecreasing on , and satisfies for , the largest root of . Set , , . The candidate value of is
and the barrier level is , with .
Theorem 3 answers the bail-out problem completely: for every initial capital and every spectrally negative Lévy surplus, the optimal policy is a double barrier with an explicit level and an explicit value in terms of scale functions. In the classical problem without injections (Theorem 2 of the same paper) the analogous conclusion needs an extra generator condition, and Azcue and Muler exhibited Cramér–Lundberg models where barrier policies are not optimal. The result is the basis of later work on dividends with capital injection, transaction costs and Parisian ruin.
The result has a published proof. What this mission adds is a machine-checked version. As far as is known, no part of the theory used — Lévy processes, scale functions, doubly reflected processes, the generator of a Lévy process, singular stochastic control — has been formalized in Lean's Mathlib.
The value function is a supremum over all adapted singular controls. Its upper bound requires a verification argument: Itô's formula for with a semimartingale that has jumps, a controlled bounded-variation part and a possibly nonzero continuous martingale part, followed by localization and limits. A function that satisfies the variational inequality only in the viscosity sense is not enough, so the candidate must be shown to be regular enough and to satisfy everywhere on . Above the barrier this inequality does not follow from a martingale property: the paper derives it from concavity and a comparison with higher barriers, through the resolvent of the doubly reflected process. The lower bound requires the existence and value of the doubly reflected process, and computing that value needs fluctuation identities (two-sided exit, overshoot) that are themselves theorems about scale functions.
Time is indexed by . The process is a structure carrying the triplet , the paths, adaptedness, independence of future increments from , stationarity, the Laplace-exponent identity, and the usual conditions on the filtration. is the law of . Policy values are computed as in the extended reals from two -valued expectations, and the value function is a supremum in the extended reals; a policy with both expectations infinite gets . Stieltjes integrals include the jump at time . The scale function is a hypothesis IsScaleFunction (it is unique), and lives in , so an empty defining set gives . The double-barrier strategy is characterized by the two-sided Skorokhod conditions plus mutual singularity of and , which pins the level- policy of bounded-variation processes. These conditions hold almost surely, and they are stated on the post-decision surplus : is carried by and by . This is the paper's "minimal amount" (p. 4) and matches its construction on pp. 10–11. The closure-of-support wording of (4.2) on its own would also admit non-minimal lump dividends. Admissibility, for together with (2.3), is likewise required almost surely.
Printed slips corrected (milestone texts are verbatim):
The goal cannot be satisfied trivially. It asserts equality of the value function with , not only an inequality. Existence of the optimal policy is part of the conclusion. Generator statements carry integrability of the jump integrand, so a non-integrable integrand cannot make them true with the junk value .
A complete development needs Lévy processes and their Laplace exponents, scale functions, first-passage and two-sided exit identities, reflected and doubly reflected processes, Itô's formula for semimartingales with jumps, and a verification theorem for singular control. All of these are reusable well beyond this mission. Contributions of any of these foundations are welcome, as are proofs of the analytic milestones (Lemma 3, Proposition 3(ii)) from the scale-function properties.
Tree-width measures how closely a graph resembles a tree. Graphs of bounded tree-width admit dynamic-programming algorithms for problems that are NP-hard in general (colouring, Hamiltonicity, and every property expressible in monadic second-order logic, by Courcelle's theorem), which is why the parameter is central to parameterized complexity and to combinatorial optimization on sparse networks. The question this mission addresses is structural: which excluded substructures force bounded tree-width?
The answer is the Excluded Grid Theorem of Robertson and Seymour: excluding a fixed graph as a minor bounds the tree-width if and only if is planar. The "only if" direction is easy, since grids are planar and have unbounded tree-width. The "if" direction is the content of Graph Minors. V. Excluding a Planar Graph (J. Combin. Theory Ser. B 41 (1986) 92–114). It is a cornerstone of the Graph Minors series that culminates in the Robertson–Seymour theorem (graphs are well-quasi-ordered by the minor relation), and it underlies polynomial-time minor testing for planar (Graph Minors XIII) and the Erdős–Pósa-type results of Sect. 8 of the same paper.
Timeline. Robertson and Seymour, Graph Minors V (1986): tree-width at most an explicit, iterated-exponential function of the grid size. Robertson, Seymour and Thomas, Quickly excluding a planar graph (JCTB 62, 1994): bound for the -grid. Chekuri and Chuzhoy (J. ACM 2016): the first polynomial bound. Chuzhoy and Tan (JCTB 2021): .
Graphs are finite. A graph is a minor of if can be obtained by contraction from a subgraph of ; equivalently, there are nonempty, pairwise disjoint vertex sets , one per vertex of , each inducing a connected subgraph, such that every edge of is matched by an edge of between and .
A tree-decomposition of is a tree together with bags () such that every vertex lies in some bag, both ends of every edge lie in a common bag, and whenever lies on the path of between and . Its width is , and the tree-width is the least width of a tree-decomposition of .
The -grid has vertex set , with adjacent to exactly when . For even , is the class of graphs with no minor isomorphic to the -grid. Every planar graph is a minor of some even grid of size at least 6; denotes the least such size.
The paper fixes explicit parameters. For : and . Then ; and ; ; ; ; ; ; ; ; .
Two auxiliary structures carry the argument. An -web is a pair of families of paths , , each family vertex-disjoint, every meeting every , and all paths pairwise edge-disjoint. An -mesh is the same with arbitrary connected subgraphs in place of paths and without edge-disjointness.
For every finite planar graph and every finite graph ,
For even and ,
The theorem converts a qualitative exclusion (no minor) into a quantitative width bound, and it is the entry point of the structure theory of minor-closed classes: every minor-closed class excluding a planar graph has bounded tree-width, and hence all MSO-definable problems on it are solvable in linear time. It is used in the proof of the graph minor theorem, in minor testing, and in the Erdős–Pósa property for planar minors (Sect. 8 of the paper).
The result is proved and classical; to our knowledge it has not been machine-checked in any proof assistant, and Mathlib has no graph minors, tree-decompositions or Menger's theorem. A formalization produces reusable definitions (branch-set minors, tree-decompositions, separations, grids) and a checked proof of the paper's explicit bound. The goal is stated with the paper's constant , not an optimized one; later improvements are stronger variants, not replacements.
The obvious attempt, building a tree-decomposition greedily from small separations, fails because nothing forces small balanced separations to exist. The whole argument supplies them: a graph without a large grid minor has no large mesh (5.3), and a graph with no large mesh has a balanced separation of bounded order (7.1). The step from no grid to no mesh goes through webs and spiders (Sect. 4) and relies on two results from Graph Minors I ((3.1) and (4.3) of the paper, cited without proof), which themselves depend on Menger's theorem. The balanced-cut lemmas (6.2)–(6.4) rest on Tutte's ordering of 2-connected graphs. None of this infrastructure exists in Mathlib.
Graphs are Mathlib SimpleGraphs on finite types (Fintype V, DecidableEq V). The paper allows loops and multiple edges; for this changes nothing, since every notion used depends only on adjacency, and for in the goal it specializes the theorem to simple planar graphs. Minors use the branch-set model (IsMinor); planarity (IsPlanar) is the existence of a crossing-free drawing in , mirroring the platform's FourColor.IsPlanar. Tree-width is not defined as an infimum; "tree-width at most " (TreewidthLE) is the existence of a tree-decomposition with all bags of size over a finite tree. enters the goal as a hypothesis IsLeast {t | Even t ∧ 6 ≤ t ∧ IsMinor H (grid t)} θ, which is satisfiable for every planar by the Sect. 2 milestone, so the goal is not vacuous. Every statement of Sects. 3–7 that mentions carries the standing assumption " even, " as hypotheses. Rational bounds such as and are compared in .
Two printed statements are corrected. (4.5) is printed for and is stated for , the only range on which are defined. (5.1) is false as printed for , , so it carries the hypothesis " implies "; the paper uses it only with .
Needed infrastructure, reusable well beyond this mission: Menger's theorem, the Graph Minors I linkage results, Tutte's ordering of 2-connected graphs, and a library of lemmas for minors and tree-decompositions. Proofs of any milestone, of the cited results as separate theorems, and of basic API for the definitions are welcome.