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.
Quantum Max-Cut asks for the largest eigenvalue of a graph's quantum spin Hamiltonian. For a graph with nonnegative rational edge weights, write
This campaign tracks expected approximation ratios for classical polynomial-time energy estimation. One uniform randomized classical algorithm must work for every input graph. For each fixed , let be the algorithm's internal fair random bits, and let be its nonnegative rational output. A ratio requires
The expectation averages the algorithm's internal randomness on a fixed graph. Its running time is bounded by a polynomial on every run. Higher ratios are better.
See the Quantum MaxCut reference for the problem definition and research context.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
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?
Two closed subgroups and of a profinite group are locally conjugate if, for every prime , a Sylow -subgroup of is conjugate in to a Sylow -subgroup of . Conjugate subgroups are always locally conjugate. The converse, which lets conjugacy be tested one prime at a time, fails in general. Deciding when it holds is a classical question about supplements of nilpotent normal subgroups.
A profinite group is a compact Hausdorff totally disconnected topological group. Equivalently, it can be described through compatible finite quotient groups. A pronilpotent group has nilpotent finite continuous quotients. A prosupersolvable group has supersolvable finite continuous quotients; a finite group is supersolvable when it admits a normal series with cyclic factors. These properties concern all finite continuous quotients, with no uniform bound on their orders or nilpotency classes.
A subgroup supplements a normal subgroup when . It complements when, in addition, . Two closed subgroups are locally conjugate when, for each prime , a Sylow -subgroup of one is conjugate in to a Sylow -subgroup of the other. For profinite groups, Sylow subgroups are maximal closed pro- subgroups. The conjugating element may depend on the prime. All subgroup notation in the paper carries closedness, as stipulated in §1.2.
The cohomological statements concern a profinite group acting continuously by automorphisms on a discrete group . With a left action, a continuous cocycle satisfies . Two cocycles are equivalent when for one fixed . Their quotient is the pointed set , whose distinguished point is the identity cocycle. Stable classes on a subgroup compare a cocycle with its conjugates after restriction to the relevant intersections. This matters when the subgroup itself is not normal. The definitions follow §§1–1.2.
The central conjugacy assertion is Theorem 1.1. For a closed normal pronilpotent subgroup of a profinite group , assume that is prosupersolvable or is pronilpotent. Then closed supplements of satisfy
Lemma 1.2 asserts, for finite nilpotent coefficients and its stated structural alternatives, a pointed bijection induced by simultaneous restriction:
The other numbered targets are Corollaries 1.3–1.4 and Propositions 2.1–2.3, 3.1–3.2, and 4.1–4.2. They retain the paper's distinctions between finite coefficients, locally finite discrete coefficients, and arbitrary closed pronilpotent subgroups. They also retain the normal-intersection condition in the semidirect-product inclusion and fixed-point results. The abelian conclusions impose no solvability assumption on the ambient profinite group.
Both counterexamples in §1 are targets. The quaternion example realizes in , has exactly two global cohomology classes and trivial Sylow cohomology, and exhibits locally conjugate complements that are not conjugate. The Heisenberg example uses of order , with the Heisenberg group of order , , and . Local containment holds while containment of a conjugate of fails.
The combined goal asserts all eleven numbered results and both counterexamples. Each assertion remains a separate milestone with the source's numbering or, for the unnumbered counterexamples, its section and page.
The conjugacy and containment theorems make precise when separate prime-wise witnesses can be replaced by one global witness. The fixed-point results similarly turn prime-wise fixed points, which can be different points, into a point fixed by the full subgroup. The counterexamples record the limits of these conclusions under weakened hypotheses. These are proved mathematical results of the preprint, rather than new conjectures.
A completed development would also provide reusable formal interfaces for continuous nonabelian first cohomology, stable classes, profinite Sylow and Hall conditions, and local subgroup relations. An earlier local Lean development supplies definitions and substantial proof material. The present draft statements are aligned to the arXiv version; their target proofs remain open in this proposal. Reusing earlier proofs requires checking their types against these interfaces and the pinned environment.
Local conjugators can vary with the prime, and there need not be one conjugator that works for all primes simultaneously. The quaternion example demonstrates this obstruction even in finite groups. Nonabelian cohomology is a pointed set, so the usual additive primary-decomposition language does not itself provide the needed assertion. The transition from finite groups to profinite groups also requires tracking topology, closedness, and continuity. The counterexamples and the finite-versus-profinite distinctions are part of the mathematical scope, not optional simplifications. See §§1–3.
All declarations use the namespace LocalConjugacy. Profinite ambient groups use Mathlib's ProfiniteGrp; subgroups, quotient groups, normality, complements, actions, fixed points, finite Sylow subgroups, nilpotence, and solvability use Mathlib structures or predicates. Custom definitions cover the continuous nonabelian quotient and the profinite local conditions absent from the pinned library interface. Conjugation is written on the left. This changes the notation for the conjugating element, not the conjugacy or inclusion assertion.
The fixed-point targets quantify over nonempty sets with no added topology and require closed stabilizers. Propositions 2.1–2.2 allow infinite locally finite discrete coefficients. Theorem 1.1 allows arbitrary closed pronilpotent . Finite special cases cannot replace these targets. Both counterexamples include explicit isomorphisms to the concrete groups named in the paper. Contributions may reuse the existing proof development, improve the reusable interfaces, or prove the targets directly while preserving these statements.
Quantum mechanics predicts probabilities, but it is notoriously quiet about what a probability is. Categorical quantum mechanics answers that by rewriting the finite-dimensional formalism in the language of dagger categories: a state is a morphism , an effect is a morphism , and the probability of an outcome is a scalar — an endomorphism of the tensor unit. On that translation the Born rule stops being an axiom and becomes a theorem about a complete, disjoint family of effects.
This mission formalizes that theorem, together with the two lemmas it rests on, in Lean 4 over Mathlib. It covers the dagger and measurement material of Chapter 2 of Reutter and Vicary's Categorical Quantum Mechanics.
Fix a monoidal dagger category with zero morphisms. The unit object carries a commutative monoid structure — the scalars. For a state and an effect , the probability that occurs on is the scalar
A family of effects is complete when the induced map satisfies , and disjoint when for . Both conditions are stated for a dagger biproduct of the unit objects.
This is the mission's goal. It fixes nothing beyond completeness and disjointness; the statement is exactly the categorical Born rule for a finite outcome set.
The Born rule is the point where the categorical and the Hilbert-space pictures are reconciled: the abstract statement specialises, in , to the usual . Proving it categorically means the rule is a consequence of the dagger-biproduct structure rather than an extra assumption, which is what makes the framework usable for quantum protocols — measurement, teleportation and the like are all built on complete disjoint families.
The supporting lemmas are reusable well beyond this mission: dagger biproducts are the categorical home of matrix calculus, and the isometry/unitary characterisations of disjointness and completeness are the standard toolkit for any later argument about measurements.
Moderate. The mathematics is elementary once the definitions are in place — the work is in bookkeeping: biproduct universal properties, the interaction of the dagger with the biproduct structure, and careful handling of the scalar monoid. The main intellectual step is realising that completeness alone, not equalizers, gives the second unitary identity.
Formalized here: dagger categories and their morphism classes (§2.3), dagger biproducts
(§2.3.3), and the scalar/state/effect vocabulary with the Born rule (§2.4.3). Mathlib has
no dagger-category theory at all, so the definitions are supplied from scratch as Lean
Definitions and are importable independently of this mission.
Not formalized: the Hilbert-space and relational models, the graphical calculus of §2.2, and the measurement/post-processing material after §2.4.3.
Two corrections to the source are made and documented in the formalization. The printed statement of Proposition 2.55 assumes completeness only, which is false; disjointness is required, as the book's own proof (which invokes Lemma 2.52) already assumes. And the book attributes the identity on to Lemma 2.52, whereas Lemma 2.52 only gives the identity on ; the identity on is Lemma 2.53. Lemma 2.53 is proved here without the book's equalizer hypothesis, so it is strictly stronger than the printed version.
CategoryTheory.Limits.Biproducts and CategoryTheory.Monoidal.Category
API, on which the definitions are built.Stochastic differential equations with superlinearly growing coefficients appear throughout applied probability: population models with cubic damping, Langevin dynamics with polynomial potentials, and stochastic volatility models such as the 3/2-model used for pricing VIX options, whose diffusion coefficient grows like . For such equations the classical explicit Euler–Maruyama method fails: Hutzenthaler, Jentzen and Kloeden (2011) proved that its -th moments diverge whenever a coefficient grows superlinearly, so it cannot converge in . Implicit methods converge (Higham–Mao–Stuart 2002) but cost a nonlinear solve per step.
The tamed Euler schemes are the explicit response.
This mission is the second of three on the paper. Mission I formalizes -convergence without a rate (Theorem 1), mission III the uniform-in-time rate (Theorem 3).
Fix a filtered probability space with right-continuous filtration, a horizon , dimensions , and a -dimensional Wiener martingale : a standard Brownian motion adapted to whose future increments are independent of . The coefficients are Borel maps and ; is the Euclidean norm, the Hilbert–Schmidt norm, the scalar product. The SDE is
with an -measurable initial value . For let and consider the scheme
whose coefficients are frozen at the last grid point, so that is computable step by step. The tamed coefficients of Model 2 are
The hypotheses, with constants :
Under A-2, A-4–A-6, the -condition and , there is a constant independent of with
The constant is existential and may depend on all data except .
Theorem 2 shows that an explicit scheme costing one coefficient evaluation per step attains the same strong order as the classical Euler method under global Lipschitz conditions. It does so for drift and diffusion coefficients that grow polynomially, and for moment orders that are small relative to and . Strong rates are what multilevel Monte Carlo needs: the variance of level corrections is controlled by the rate. When could be taken to be the statement specializes to the classical globally Lipschitz rate (Remark 6).
The result is proved on paper; it has no machine-checked proof. Stochastic integrals are not in Mathlib; this mission uses the Brownian Itô-integral relation published by the Ethier–Kurtz series on the platform. A formal proof would give the first verified strong convergence rate for any Euler-type scheme. Along the way it produces reusable moment bounds for tamed schemes and the control of one-step increments.
The obvious argument applies Itô's formula to and closes a Gronwall inequality. Two steps of it fail without taming. First, the error splits into the monotone part, handled by A-6, and cross terms such as multiplied by ; they are controlled only through moments of of order well above that are uniform in , which the untamed scheme lacks. Second, the taming itself introduces an error that must be shown to be in and not merely . The exponents in the -condition are exactly what the Hölder splittings of these two terms require.
EthierKurtz_HasBrownianItoIntegral, with the integrand cut off after .Feedback laws that damp vibrations in elastic structures are implemented by sensors and actuators, and a physical loop always reacts with some time delay : the damping force at time is computed from the velocity measured at time . Datko, Lagnese and Polis showed in 1986 that an arbitrarily small delay in a boundary feedback can destroy the stability of a one-dimensional wave equation (Datko–Lagnese–Polis, SIAM J. Control Optim. 24 (1986)), and Datko showed that such fragility is common to a broad class of feedback-stabilized hyperbolic systems (Datko, SIAM J. Control Optim. 26 (1988)). Delay-robustness is therefore a genuine question for every stabilizing feedback, not a technicality.
Nicaise and Pignotti (SIAM J. Control Optim. 45 (2006) 1561–1585) identified a simple sufficient condition in several space dimensions: if the feedback contains an undelayed velocity term with gain and a delayed one with gain , and , the energy still decays exponentially; if , instabilities appear for some delays. This mission formalizes the stability half for internal (distributed) damping, localized near the Neumann part of the boundary.
Timeline.
Let , , be a bounded open set with boundary of class , split as with and . Write for the outer unit normal, for the surface measure, for time derivatives and for the Laplacian in .
Geometric hypothesis (1.6)–(1.7): there are a function and with for all , , and on .
Damping coefficient. is an open neighbourhood of (in ), and satisfies
The system (1.12)–(1.16): for gains and delay ,
with on , on , initial data , , and history for .
The energy. Assume (1.8) and fix with (1.10). Then
The first summand is the standard energy ; the second accounts for the velocity history on the delay window.
There exist , depending on the data but not on the solution, such that every solution satisfies
The constants are left existential, as in the paper, so no later sharpening of rates invalidates the goal.
The result. Theorem 1.3 shows that a localized viscous damping acting only near the Neumann boundary keeps its exponential stabilizing effect when part of the feedback is delayed, provided the delayed gain is dominated by the undelayed one. Together with Theorem 1.4 of the same paper (instability for and suitable delays) it gives a sharp threshold in terms of the gains. The energy with its history term became the standard Lyapunov functional for delayed wave and plate equations in the literature that followed.
Formalizing it. The theorem is proved in the paper; no machine-checked proof of it, or of any exponential decay result for a multidimensional wave equation, is known to exist. A complete development would produce reusable Lean infrastructure: energy identities for the wave equation on domains via the divergence theorem, the delay-energy calculus, and an observability inequality for the wave equation with mixed boundary conditions. Each milestone has value on its own; Proposition 4.2 in particular is a classical control-theoretic result.
The energy estimates (milestones 1 and 2) are calculus once the divergence theorem is available. The central difficulty is observability. Energy dissipation alone gives only nonincreasing; exponential decay needs the energy at time to be controlled by the energy dissipated on (Proposition 4.3), and that needs the conservative wave equation to be observable from (Proposition 4.2). The observability inequality does not follow from energy identities: the paper relies on Carleman estimates of Lasiecka–Triggiani–Yao (1999) and a compactness–uniqueness argument, neither of which is available in Mathlib. The obvious attempt, a multiplier identity with alone, leaves boundary terms on that cannot be absorbed without a localization near and a lower-order compactness step.
EuclideanSpace ℝ (Fin n) with 1 ≤ n; solutions are real valued.Needed infrastructure: the divergence theorem on domains (assumed here as a structure field), differentiation under the integral sign for the energies, Carleman estimates or another route to observability for the mixed wave problem, and a compactness argument (Rellich). Contributions of any of these as standalone lemmas are welcome.
The 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. The question is how large a comparison constant is needed to make this inequality hold.
This mission establishes the best possible constant for complex diagonal matrices for every real . The result is proved in Lean. For each exponent, one constant works for every triple of diagonal matrices of the same size, across all finite sizes.
The constant comes from a simple family of three diagonal matrices, called the cyclic family. Varying one parameter determines the largest comparison constant these examples require. The theorem proves that this value also works for every other triple of diagonal matrices, however large. The goal theorem gives the exact formula and statement.
This is the foundation of the sharp diagonal Hlawka campaign. It supplies the shared definitions and supporting results for lowering the exponent cutoff while keeping the same formula. A later mission has now established the result in Lean for every real ; the campaign invites further improvements.
The broader question of optimal constants for Schatten norms appears in Audenaert and Kittaneh’s Problem 7. Extending the sharp diagonal constant to general matrices is a separate challenge.
79aa498bfcf7b22bd91d771fb32ec278e2d4704b. Source libraryA 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.
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.