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.
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?
Queueing control problems (admission control, routing, service-rate selection, flow control) are naturally posed as Markov decision chains with a denumerably infinite state space, such as the number of customers in a buffer, and are usually judged by their long-run average cost per unit time. When the state space is finite, Chapter 6 of Sennott's book shows that an average cost optimal stationary policy always exists. On a countable state space this fails: Section 7.1 of the book gives examples in which no average cost optimal policy exists, and one in which no stationary policy comes within a given distance of the minimum average cost. The question addressed by this mission is under which verifiable conditions on the discounted value functions a countable-state model has a constant minimum average cost and an optimal stationary policy.
Timeline, following the book's bibliographic notes (p. 163). The book names Taylor (1965) and Derman (1966) as earlier pivotal work and Ross (1968), and his 1983 textbook, as the direct predecessor. Sennott (1989, Operations Research 37) weakened Ross's assumptions to cover models with unbounded costs, and proved the main result of Section 7.2; the (SEN) assumptions of Chapter 7 are the cleaner version of Sennott (1993). Cavazos-Cadena (1991) gave the example, adapted as Example 7.3.1 of the book, showing that under these assumptions the optimality inequality can be strict. The weaker (H*) assumptions of Section 7.7 appear, in a slightly different form, in Sennott (1995). Part (iv) of Theorem 7.2.3 is new in the book.
A Markov decision chain (MDC) has a countable state space , for each state a finite nonempty action set , a nonnegative finite cost , and transition probabilities with . A policy chooses the action at time at random according to a distribution that may depend on the whole history ; a stationary policy always chooses in state .
For an initial state , the -horizon cost is , the average cost is , and the minimum average cost is over all policies. A policy is average cost optimal if . For the discounted value function is . All these quantities lie in .
Fix a distinguished state and put . The (SEN) assumptions are:
A limit function is a pointwise limit of along some sequence . If is a stationary policy realizing the discount optimality equation , a limit point is a stationary policy with for large , for each , along some .
Under (SEN), there is a finite constant independent of ; limit functions exist, satisfy and the average cost optimality inequality (ACOI)
every stationary policy realizing the minimum is average cost optimal with and ; every limit point of discount optimal stationary policies is average cost optimal and satisfies the corresponding inequality for an associated limit function; and the average cost of any optimal policy is a limit, not only a limit supremum.
Theorem 7.2.3 is the existence theorem the rest of Chapter 7 builds on (p. 128): the ACOE results of Section 7.4, the (BOR) and (CAV) sufficient conditions of Section 7.5, and the worked queueing models of Section 7.6 all work under (SEN) and invoke it. It justifies computing an average cost optimal policy for a queueing model as a limit of discount optimal policies, and it shows that the minimum average cost is the Abelian limit of the normalized discounted value.
The results are proved in the book and in Sennott (1989, 1993, 1995), but none of them has a machine-checked proof: Mathlib has no Markov decision processes, and the platform's average cost results concern finite state spaces or Borel models with different assumptions. The formalization produces a general-policy, countable-state MDC development with extended-real values, reusable by the later missions of this series.
On a finite state space the relative value functions are bounded and the Abelian limit can be controlled directly. Here is bounded above only by a function that may be unbounded, so passing to the limit in the discounted optimality equation cannot use dominated convergence, and in general only an inequality survives in the limit; Example 7.3.1 shows that the inequality in the ACOI can be strict. Showing that a policy realizing the ACOI is optimal requires control of for a function that is unbounded above, and part (iv) requires comparing the limit inferior and limit superior of Cesàro averages for an arbitrary, possibly history-dependent optimal policy.
The state space is any countable type ([Countable S]); actions form a type with finite nonempty Finset action sets; costs are ℝ≥0; transition probabilities, costs over time and value functions are ℝ≥0∞. Policies are general: randomized and history dependent, with histories encoded as finite state and action sequences and the process law built by an explicit recursive product. Finite horizon costs have terminal cost , as the chapter prescribes.
The relative value is computed in EReal, never through a truncated real subtraction: a state with gives , so (SEN2) cannot hold through a junk value, and (SEN1) is a bound by a finite constant that itself forces . Sums and expectations of real functions are extended reals, computed as positive part minus negative part; they are never Bochner integrals and never default to when not summable. The limit is the filter 𝓝[<] 1. Limit functions and limit points follow Definition 7.2.2 literally, over arbitrary sequences in , and the (SEN), (H), (H*) sets are predicates carrying their witnesses and .
A development that bounds only as a free function, rather than the one built from the infimum over all policies, or that quantifies only over stationary policies in , proves a different and weaker theorem and does not count.
Needed infrastructure: the law of the controlled process under a general policy, monotone and Fatou-type limit interchanges for countable sums, the Abelian inequality (Proposition 6.1.1 of the book), and the existence and optimality of discount optimal stationary policies (Theorem 4.1.4). The MDC layer and these two results are shared with other missions of the series; contributions to them are welcome.
The solution concept of von Neumann and Morgenstern — today usually called a stable set — was the first general answer to the question of what a rational outcome of a many-player cooperative game should be. It was introduced in Theory of Games and Economic Behavior (1944), and Chapter VI of that book states it exactly (§30) and then tests it on the smallest nontrivial case: the essential zero-sum three-person game (§32). The complete determination of all solutions of that game, (32:A)–(32:B) on p. 288, is the book's first full answer to "what are all the solutions of a given game?", and it is the result that made visible the two features every later discussion of stable sets has had to address: a game can have many solutions, and a solution can be an infinite set of imputations that discriminates against one player.
Stable sets remain an active topic in cooperative game theory: Lucas (1968) showed that some games have no stable set, and the literature on existence, uniqueness and structure (for example Shapley 1971 on convex games, whose core is the unique stable set) builds on the definitions formalized here.
A zero-sum -person game with players is described by its characteristic function , a real number for each set of players, satisfying (25:3:a)–(25:3:c):
An imputation is a vector with for each player and (30:1), (30:2). A set is effective for if (30:3). An imputation dominates , , if some nonempty set is effective for and for all (30:4). A solution is a set of imputations such that no element of dominates another element of (30:5:a) and every imputation outside is dominated by some element of (30:5:b).
Two characteristic functions are strategically equivalent if for constants with (27:1), (27:2). Every is strategically equivalent to exactly one reduced function (27:A); the game is inessential if and essential otherwise (27.3).
For three players, an essential game in reduced form with the unit chosen so that has
and its imputations are the points of the fundamental triangle , .
For the game (32:1), a set is a solution if and only if either
or, for some player and some with
is the set of all imputations with ((32:7), (32:7*), (32:7**), (32:A)). Both directions are part of the goal.
For general (§31): domination is irreflexive (31:K); an inessential game has exactly one imputation and an essential game infinitely many (31:I); solutions are never empty (31:J); in an essential game every imputation is dominated by one it does not dominate (31:L); an undominated imputation exists iff the game is inessential (31:M); a one-element solution exists iff the game is inessential, and it is then the only solution (31:P); strategic equivalence induces an isomorphism of imputations, effective sets, domination and solutions (31:Q).
For the three-person game (§32): domination is the coordinate condition (32:4) on two of the three players; two mutually undominated imputations agree in one coordinate (32:5); the set (32:6) is a solution (32:B); every set (32:7) with in the range (32:8) is a solution (32:A).
The goal is the first complete classification of the stable sets of a game. It shows that solutions are not unique and need not be finite: next to the symmetric three-point solution there is a one-parameter family, for each of the three players, of solutions that fix that player's payoff at and let the other two bargain freely. The book's interpretation of these "discriminatory" solutions (§33) as standards of behaviour is one of the lasting ideas of the theory. The general- results of §31 fix the trivial case completely: an inessential game has a unique, one-point solution, so every essential game has only solutions with at least two elements and an empty core. (31:Q) justifies working with reduced forms throughout the later chapters.
The results are proved in the book; none has a machine-checked proof on the platform as of this writing. The existing stable-set definitions on the platform concern feasible payoff vectors of a superadditive game, not imputations of a zero-sum game, so this mission also provides the book's definitions in the form every later chapter of the series (decomposition, simple games, general games) uses.
The "if" direction of the goal is a finite case analysis per set, but (30:5:b) must be checked for every imputation outside the set, with the dominating element chosen as a function of it. The "only if" direction is the substance: from an arbitrary solution — a possibly infinite, a priori unstructured subset of the triangle — one must derive that it is exactly one of the listed sets. The book's argument is geometric (Figures 54–60) and leans on pictures of dominated regions; the delicate points are the exclusion of the limiting position , where a single point of the triangle stays undominated, and the proof that a solution with two points on a horizontal line and one point off it must be exactly (32:6). The endpoint is included and must be handled; the endpoint is excluded and must be refuted.
Players are Fin n (the book's player is index ; for three players are 0, 1, 2), coalitions are Finset (Fin n), characteristic functions are Finset (Fin n) → ℝ, imputations are vectors Fin n → ℝ. The domination relation is defined on all vectors but every statement restricts it to imputations; solutions are sets of imputations and (30:5:b) quantifies over imputations only.
Standing hypotheses instantiated in the statements:
IsCharFunction v), the book's standing assumption for "a zero-sum -person game";Domination requires all three clauses of (30:4): dropping " not empty" makes every imputation dominate every other through and turns the goal into a statement about the empty solution; the definitions keep all three. The general- statements carry the characteristic-function hypotheses because without them a set function with no imputation has the empty set as a vacuous solution.
The dimension claim "an -dimensional continuum" in (31:I) is not formalized; only "infinitely many imputations" is. Contributions welcome: proofs of the milestones, a proof of the transfer of the goal to all essential three-person games through (31:Q), and reusable lemmas on domination via two-element coalitions.
Spare-parts inventory models for repairable items rest on Palm's theorem: if demands arrive as a Poisson process with constant rate and each demanded unit spends an independent, identically distributed resupply time with mean in the pipeline, the number of units in resupply is Poisson with mean in steady state. Stock levels, backorders and fill rates are all computed from that distribution.
Both assumptions fail in practice. Military flying programmes ramp up and down within weeks, repair shops close for periods, and commercial parts distribution centres see demand that varies by day of the week. Chapter 9 of Muckstadt's Analysis and Algorithms for Service Parts Supply Chains (Springer 2005, DOI 10.1007/b138879) extends Palm's theorem to a nonstationary Poisson demand process with time-dependent resupply-time distributions, gives the compound (multi-unit order) version, and uses the result to compute, at any time , the distribution of units in repair at the depot of a two-echelon system.
Timeline: Palm (1938) proved the stationary result for telephone traffic; Feeney and Sherbrooke (1966) extended it to compound Poisson demand; Hillestad and Carrillo (RAND, 1980) and Crawford (RAND, 1981) developed the time-dependent extensions, summarized by Carrillo (RAND, 1989). The chapter presents these results.
A single item is stocked at one location, and every demand is for one unit.
The mean of is
In the compound version (Section 9.2), orders arrive as above and each order is for units, with a time-stationary law . All units of an order share its resupply time, counts units demanded in , and is the -fold convolution of .
In the two-echelon version (Section 9.3), base has failure rate . A failure is repaired at the base with probability and at the depot otherwise. Depot repair of a failure occurring at time takes a deterministic time with for (no crossing). Write .
For every ,
This is an exact statement at each finite time, not a limit. With constant and it reduces to the finite-time step of Palm's theorem.
A plain supporting item states that is Poisson with mean , the factor the proof of Theorem 13 uses.
Theorem 13 gives the full distribution of the pipeline at every instant. Time-dependent expected backorders, , and fill rates follow from it, so stock levels can be planned against a surge or a repair outage without a steady-state approximation. Theorem 14 does the same for multi-unit orders. The depot result feeds the base-level convolution of Section 9.3.3, which in turn gives time-dependent performance measures for a two-echelon system.
These results are proved in the literature, and the chapter reproduces the proofs of Theorems 13 and 14. It cites Theorem 12 without proof ("similar to the one given in Chapter 3"). No machine-checked version of any of them is known, and neither Mathlib nor this platform has a Poisson process, stationary or not, a thinning theorem, or an order-statistics theorem. The formal content of this mission therefore includes the construction and the first distributional facts of the nonstationary Poisson process.
The algebra of the proof is a Poisson mixture of binomials and is short. The difficulty is Theorem 12 and its use. The obvious argument treats "the demands in " as independent draws from and assigns each an independent resupply time with law . Making this rigorous requires identifying the conditional joint law of the epochs given . The resupply time of the -th demand is not independent of its epoch: its law depends on the epoch. So it must be shown that, after conditioning, the marks attached to sorted epochs behave like marks attached to unsorted i.i.d. draws. The book's constant-rate argument (Chapter 3) uses the uniform density on the simplex. Here the density involves , which may vanish on intervals, and need not be invertible.
Stochastic quasigradient (SQG) methods minimize an expectation over a constraint set when neither nor its gradient can be computed, only random vectors whose conditional mean is (close to) a subgradient. They are the workhorse of stochastic programming and, under the name stochastic gradient descent, of large-scale statistical learning. The classical convergence theory, going back to Robbins and Monro (1951) and to Ermoliev's quasi-Féjer analysis, asks the stepsizes to be chosen in advance with , , . Uryasev, in Chapter 18 of Numerical Techniques for Stochastic Optimization (Ermoliev and Wets, eds., 1988), points out that such programmed rules are slow in practice, and that practitioners want adaptive stepsizes computed on line from the observed directions.
Timeline:
Let be nonempty, convex and compact, its diameter, and convex on an open convex set , with subdifferential . The projection is the point of nearest to . On a probability space, the SQG method generates
from , where the direction is a stochastic quasigradient: with , a bias , and the -algebra induced by .
The adaptive stepsize rule of the chapter is, for fixed , and ,
The step grows when consecutive moves point the same way and shrinks otherwise. The weighted (Cesàro) averages are
The sequence is Cesàro convergent when converges to the solution set.
Chapter 17 (Pflug) uses the same method for over a closed convex , with from i.i.d. and stepsizes adapted to .
Under (18.15), (18.16) and (18.17), almost surely,
and if a.s., then and all accumulation points of are minimizers, almost surely.
Theorem 2 is a convergence guarantee for a stepsize rule that is computed from the run itself. It needs no square summability of the steps, and it tolerates a nonvanishing bias at a cost linear in the bias. This is the regime of practical SQG codes; §18.4–18.5 of the chapter discuss implementation and numerical experiments. Theorem 1 isolates the reason: Cesàro convergence needs only and . It also allows a stepsize that depends on the current direction, provided consecutive steps have ratio tending to .
The volume proves none of the probabilistic results in full. Theorem 1 of Chapter 18 is cited from Uryasev's earlier report. Theorem 2 has an outline proof that reduces it to Theorem 1. Chapter 17 gives a sketch through the Robbins–Siegmund lemma. None of these results is formalized. The mission produces machine-checked statements of all of them, with the misprints of the page resolved, and it separates the pathwise part of the Theorem 2 argument (steps 1 and 2, which are deterministic) from the martingale part (Theorem 1).
The obvious route to a.s. convergence is the quasi-Féjer or Robbins–Siegmund argument. It controls and needs , which is exactly what is not available here. The averaged analysis has to show that the martingale term is almost surely, and that is , when the stepsizes are themselves random. Under condition (2) of Theorem 1, is not even measurable with respect to the -algebra of the conditional expectation. So , and the standard decomposition breaks. For the adaptive rule, the stepsizes are coupled to the iterates through the exponent. Neither nor is given, and both must be derived path by path.
is EuclideanSpace ℝ (Fin n). Sequences are indexed from . Chapter 17 is shifted by one against the page: its , , become indices . Conditional expectations are Mathlib's condExp with respect to the history -algebras of the definition file. Every bound is written out as "for every , eventually ", or in (18.17) as a bound with . Expectations of squared norms are lower Lebesgue integrals. The deterministic proof steps (items 5 to 8) are stated for one sample path.
Readings of the page, each recorded in the item's Formalization Note:
No explicit constants replace an O(·) or an unspecified "C": every constant appears in the book's statements.
A trivializing formalization states Theorem 2 for arbitrary stepsizes satisfying (18.10)–(18.13), which is Theorem 1 again. Here the stepsizes are tied to the iterates by (18.5), and the of (18.17) is the of the rule.
Needed infrastructure: a Robbins–Siegmund almost-supermartingale lemma, which Mathlib does not have; a strong law for martingale differences with random weights (Kronecker's lemma in its stochastic form); nonexpansiveness of the projection onto a closed convex set; and nonemptiness of the subdifferential of a finite convex function on an open set. The first two are reusable across stochastic approximation. Contributions of any of the milestones, or of these lemmas as separate theorems, are welcome.
Decisions under uncertainty are often required to satisfy a constraint that depends on a random parameter , and requiring it for every possible is usually too conservative or infeasible. The scenario approach replaces the unknown distribution of by independent samples (scenarios) and enforces only the sampled constraints; its generalization theorem (Campi and Garatti, 2008) bounds the probability that the resulting decision violates a fresh constraint.
Enforcing all sampled constraints can still be costly: a few unusual scenarios may dominate the solution. A practitioner therefore often discards of the sampled constraints, optimally, greedily or at random, and re-solves. The question is what guarantee survives: the removed constraints were chosen by looking at the data, so the solution is biased towards points of higher risk. Campi and Garatti (2011) answered it with a bound that holds for every removal procedure. This mission formalizes that answer as it is presented in Chapter 3, Section 3.3 and Chapter 5, Section 5.3 of the textbook Introduction to the Scenario Approach (Campi and Garatti, SIAM/MOS 2018), together with its explicit corollary, Theorem 1.2. Applications include chance-constrained control, portfolio selection and prediction, where discarding scenarios trades a controlled amount of risk for a better cost.
A decision ranges over (in Lean, EuclideanSpace ℝ (Fin d)), with a closed convex domain and a linear cost . An uncertain parameter takes values in a measurable space with probability , and each determines a closed convex constraint set . The violation probability of a decision is
Given independent samples with joint law , the scenario program minimizes over . For a set of indexes, the program without the constraints in minimizes the same cost over ; its solution is written . A removal procedure selects, as a function of the whole sample, a set of indexes, and denotes the solution of the program without them. The procedure is required to output a solution that violates exactly the removed constraints (with probability one): a removed constraint that turns out to be satisfied is reinstated and another is removed. Two standing assumptions are used throughout: Assumption 3.4, that and every are convex and closed, and Assumption 3.6, that for every sample size and every sample the scenario program has exactly one solution.
For , under Assumptions 3.4 and 3.6, for every removal procedure and every ,
The bound depends on the problem only through , and on the removal procedure not at all. For it is Theorem 3.7.
Theorem 3.9 certifies every constraint-removal heuristic at once. Since the guarantee is the same for optimal, greedy and random removal, a user may pick the removal strategy purely for cost, and may inspect several values of before choosing, paying only a union bound over the values tried (Section 3.3). Theorem 1.2 turns the bound into an explicit rate: when is held fixed, the violation exceeds the empirical risk by a margin of order , only slightly worse than the rate for estimating the probability of a fixed event. The result also shows that the violation after removal concentrates around the target level, which is the basis of the book's comparison between sampling-and-discarding and simply using fewer scenarios (Example 3.10).
Theorem 3.9 is proved in the literature for general (Campi and Garatti, 2011); the textbook proves it for . To our knowledge no part of the scenario approach has a machine-checked proof. A formal development would supply the first verified version of the removal bound, a Lean treatment of solution maps of random convex programs, and reusable combinatorial and binomial-tail estimates.
The removed set is chosen after seeing the data, so the kept constraints are not an independent sample and Theorem 3.7 cannot be applied to directly. The argument must pass through all fixed index sets and account for the event that the removed constraints are violated; a plain union bound that ignores this event loses a factor and does not give (3.13). For a fixed index set, the probability that the removed scenarios are all violated involves the distribution of , which is only known to be dominated by a Beta law, so a stochastic-domination argument for the increasing function is needed. In general dimension the combinatorial constant comes from a sharper counting than the two-dimensional computation of Section 5.3, and that argument is in the cited paper rather than in the book.
Decisions live in EuclideanSpace ℝ (Fin d), samples of size are maps Fin m → Δ with law Measure.pi (fun _ => P) for a probability measure P, and the violation is the real number (P {δ | θ ∉ Θδ δ}).toReal. Events over samples are compared in ℝ≥0∞ with ENNReal.ofReal of the book's right-hand side. The removal procedure is an arbitrary map I : (Fin N → Δ) → Finset (Fin N) with (I ω).card = k, and θk is a map that, for every sample, solves the program without the constraints in I ω, and violates each of them with probability one. The following implicit hypotheses of the book are written as binders:
∀ᵐ ω ∂ℙ^N), the book's own hypothesis on p. 65, so (5.11) is an inclusion up to a null set as on the page; requiring the violation for every sample would be unsatisfiable for (on a sample with all equal a kept constraint coincides with a removed one) and would make the results vacuous;Theorem 1.2 is stated in the constraint formulation of Chapter 3, to which the book says it "straightforwardly generalizes" (p. 20), with the hypotheses of Theorem 3.9 from which Section 3.3.1 derives it. Eq. (5.14) and the closing display of Section 5.3 are stated for only, as in the book.
A trivializing formalization is excluded: the removal procedure is universally quantified, the solutions are exact minimizers rather than arbitrary feasible points, and the event is the strict ; a statement for one fixed rule, or with unconstrained, would be a different theorem.
A complete development needs: product measures and Fubini over Fin N → Δ, reindexing of the kept constraints as a sample of size , the Beta form of the binomial tail (the platform's binomial_upper_tail_eq_incomplete_beta is available), and stochastic domination for monotone integrands. Solution-map and violation infrastructure is shared with the sibling missions of this series. Contributions on any milestone, including the general- counting argument of the cited paper, are welcome.
The scenario approach turns an optimization problem under uncertainty into a finite, data-driven program: sample instances of the uncertain parameter, optimize against all of them, and certify how often the resulting design fails on a new instance. Its main guarantee (Theorem 3.7 of Campi and Garatti's Introduction to the Scenario Approach) bounds the probability of failure by a binomial tail in and in the number of optimization variables. To reach a failure level with confidence , the number of scenarios grows roughly like (Theorem 1.1 of the book). The product of and is what makes medium- and large-scale designs expensive: each scenario is one more constraint in the program that has to be solved.
FAST (Fast Algorithm for the Scenario Technique), introduced by Carè, Garatti and Campi in Operations Research 62 (2014), removes that product. It solves the program with a moderate number of scenarios and then, instead of re-optimizing, raises the returned cost level until it covers further scenarios. The book presents the algorithm and its guarantee, Theorem 8.5, in §8.3, and refers to the paper for the proof. This mission formalizes that guarantee.
Timeline:
Let be a measurable space carrying a probability measure , and let be a real loss of a decision under the uncertain parameter . As a standing assumption of the book, is convex for every .
Given scenarios drawn independently from , the scenario program (1.4) is
Its solution is and its optimal value . Assumption 3.6 requires that for every and every sample the solution exist and be unique. The pair has components, and is the number that enters every bound.
The risk (Definition 8.2) of a decision with cost level is
the probability that a new instance costs more than promised. It is the violation of the epigraphic constraint .
FAST takes independent scenarios. It solves (1.4) with the first of them, obtaining . In the detuning step it then sets
the smallest level that covers every scenario seen. The output is with .
For every ,
No relation between and is required. When the sum equals and the bound reads .
The first stage is an ordinary scenario program with scenarios. For ,
that is, is dominated by a distribution (recalled on p. 90).
For , makes the right-hand side of (8.5) at most (p. 95).
The result. Theorem 8.5 makes the guarantee of the scenario approach cheap to obtain. With (the book suggests ) and , the total number of scenarios is . This is additive in and rather than multiplicative, and the added scenarios cost only function evaluations, not a larger optimization. The price is suboptimality: is in general higher than the value a classical scenario program with the same confidence would return.
Formalizing it. The result is proved on paper, in the cited 2014 article; the book states it without proof. No part of the scenario theory has been machine-checked on this platform, as far as a search of the catalog shows. The mission produces a checked two-stage bound whose first stage is the loss-function form of Theorem 3.7, which is reusable by every mission of the series that works with program (1.4). The rule is an elementary but explicit sample-size certificate.
The obvious route treats the detuning step as a fresh scenario program with scenarios and applies Theorem 3.7 to it. That fails: is not the solution of that program, and Theorem 3.7 with scenarios gives a bound that is not of the product form (8.5). The level depends on all scenarios at once, including those that determined , and the map is monotone but need not be continuous, so the event is not a simple event about the new scenarios. Underneath the goal sits Theorem 3.7 itself, which is the main theorem of the book and whose proof occupies Chapter 5.
Lean representation:
EuclideanSpace ℝ (Fin n); the book's is written , never with natural-number subtraction.ω : Fin m → Δ with law Measure.pi (fun _ => P), and the same defines the risk. FAST draws one sample ω : Fin (N₁ + N₂) → Δ; its first stage is ω ∘ Fin.castAdd N₂.Finset.sup' over a nonempty index set. runs over all scenarios, not over the new ones only.(P {δ | c < ℓ ν δ}).toReal, with the strict inequality of Definition 8.2 and the strict event of (8.5). Probabilities of sample events are compared in ℝ≥0∞ through ENNReal.ofReal.νstar from samples to decisions, with the hypothesis that νstar ω₁ solves the program for every sample ω₁.Hypotheses the book leaves implicit, stated explicitly:
A formalization that bounds only the new scenarios is ruled out, because is defined as a maximum over all scenarios. So is one that takes as a free variable or drops Assumption 3.6: the goal is stated for the output of FAST as the book defines it.
A complete development needs the scenario program in loss form, product-measure conditioning on , and Theorem 3.7. The loss-form Theorem 3.7 is the reusable piece. Proofs of the milestones and of intermediate conditioning lemmas are welcome.
Chapter 1 of Baccelli and Brémaud's Elements of Queueing Theory builds Palm calculus. Chapter 2 settles when a queue has a stationary regime. Chapter 3 is called simply Formulas, and it is what the first two chapters were for: it computes.
The pattern is always the same. A quantity of interest is observed two ways — from a clock fixed in time, and from an arriving customer — and Palm calculus converts between them. Little's law, the Pollaczek–Khinchin formula and the rate conservation principle are all instances.
Theorem 3.3.1 (p.211) is the one that says when the two views coincide.
This classical result of queueing theory states, in rough terms, that if the arrival point process is Poisson, operational characteristics of the system computed just before arrival times and at arbitrary times are the same (Poisson Arrivals See Time Averages). Some care must be exercised in the application of this principle, and we now give a precise statement, in the
θ_t-framework.
E⁰_A[f(Z(0))] = E[f(Z(0))] (3.3.1)
for every F_t-predictable, flow-compatible {Z(t)} and every non-negative measurable f,
whenever A admits the constant F_t-intensity λ; and, under ergodicity,
lim_N (1/N) Σ_{n=1}^N f(Z(T_n)) = lim_T (1/T) ∫_0^T f(Z(s)) ds . (3.3.2)
The "some care" is the word predictable. PASTA is false without it: an arrival that changes the
state it then observes does not see the time average, and that is exactly what predictability —
measurability for the F_t-predictable σ-field, generated by the sets (a,b] × A with A ∈ F_a —
rules out.
The hypothesis is the constant F_t-intensity, not "A is Poisson". By Watanabe's theorem the two
are equivalent, but that equivalence is a remark on the page and not part of this theorem.
§3.4 derives formulas from conservation equations. Applying the rate conservation principle of
Chapter 1 to Y(t) = e^{iuW(t)} in a GI/GI/1/∞ queue gives Takács' formula
iu E[e^{iuW(0)}] = λ E⁰_A[e^{iuW(0−)}] (E[e^{iuσ_0}] − 1) + iu(1 − ρ) , (3.4.44)
an identity between a stationary expectation and a Palm expectation of the workload just before
an arrival. One substitution turns it into a closed form — and that substitution is PASTA. When the
arrivals are Poisson, E⁰_A[e^{iuW(0−)}] = E[e^{iuW(0)}], and
E[e^{iuW(0)}] = iu(1 − ρ) / ( iu − λ(Ψ_σ(u) − 1) ) , (3.4.45)
the Pollaczek–Khinchin characteristic function formula. The most quoted formula in single-server queueing theory is one application of this mission's goal theorem.
§3.1 carries Little's formula to fluid queues. Lemma 3.1.1 is the set identity that turns the fluid workload into an integral against the arrival measure — the same two instants described from the server's side and from the arrivals' side.
§3.2 applies Campbell's formula to rare events. Lemma 3.2.1 gives a closed form, in a
countable-state Markov chain, for the mean time to make an excursion to a rare set and return; its
two expressions count the same cycle rate from the two ends. Theorem 3.2.1 generalizes
Keilson's asymptotic equivalence to a stationary θ_t-compatible process, replacing cycles by
thinnings of the entrance processes of two disjoint sets.
§3.5 applies the stochastic intensity integration formula to a superposition of on-off fluid sources. Lemma 3.5.1 identifies a conditional expectation with a Palm expectation through Papangelou's theorem — the mean workload while a source is idle equals the mean workload that source sees when it wakes. Lemma 3.5.2 measures the gap between the two Palm expectations of the workload taken with respect to a source's start process and its fluid process.
Nothing here is on the platform or in Mathlib. The nearest platform item,
queueing_general_littles_law, is Stidham's deterministic sample-path law; its own docstring
disclaims probability, expectation, stationarity, ergodicity and FIFO. Baccelli's L = λW is the
Palm identity for a stationary ergodic marked point process, derived from the inversion formula
(1.2.25) — an identity between an expectation under P and a Palm expectation under P⁰_N, not a
pathwise limit. Different framework, different hypotheses, and neither implies the other.
Mathlib has filtrations and adapted processes but no predictability in the form this chapter needs, and no stochastic intensity.
(3.3.1) is an equality in [0, ∞] for every non-negative
measurable f. (3.3.2) asserts that, P-almost surely, both averages converge in [0, ∞] to one
common limit, so both limits exist. Predictability is measurability for the predictable σ-field
P(F_t) of p.55. The concrete form Z(t,ω) = v(t, θ_t ω) of (1.8.1) is not used as the hypothesis,
because for a general history it is strictly weaker. The hypothesis is the constant F_t-intensity,
E[A(a,b] | F_a] = λ(b − a), and not "A is Poisson".u, and for
u ≠ 0 respectively. Their hypotheses are the page's: σ_n is independent of W(T_n−) under
P⁰_A, E⁰_A[e^{iuσ_0}] = E[e^{iuσ_0}], P(W(0) = 0) = 1 − ρ, and ρ < 1. The workload is a
measurable, flow-compatible solution of Lindley's equation. (3.4.45) adds PASTA's hypotheses for
{W(t−)}, and it asserts that its denominator is non-zero.E_α R. The chain is irreducible, F is non-empty,
and hitting times are counted from time 0.E⁰_{F_n(→A)}[τ(F_n)] · Λ_n → 1. Its hypotheses are the section's standing ones: P is
flow-invariant, {X(t)} is flow-compatible, and A and every F_n are regular and disjoint.P⁰_{A^i} is the Palm probability of the random measure A^i, and the workload is
the stationary solution of the fluid-queue equation. Lemma 3.5.1 is an identity in [0, ∞].
Lemma 3.5.2 assumes that E⁰_{A^i}[W(0)] and the expectation defining C_i are finite.A formalization that makes Palm probability an opaque measure with the formulas as axioms, or that weakens predictability to adaptedness, trivializes this mission or makes it false, and is out of scope.
Chapter 2 of Baccelli and Brémaud's Elements of Queueing Theory asks when a queue has a stationary regime. §§2.1–2.4 answer it for the single-server and multiserver queues by Loynes' monotone construction. §§2.5 and 2.11 answer it for the general object those constructions are instances of: a stochastic recurrence
W_{n+1} = h(W_n, ξ_n),
driven by a sequence {ξ_n} compatible with an ergodic shift θ. Two questions arise, and this
mission is about both.
§2.5.3 treats the finite-state case. An ergodic transition matrix on E = {1, …, r} has a
stationary law π, and the classical way to sample it is to run the chain and wait. That gives a
sample whose law converges to π and is never equal to it.
Coupling from the past (Propp and Wilson, 1996) does better. Run one chain from every state,
all sharing a single array {ξ_k(i)} of i.i.d. uniforms indexed by time and current state, started
further and further in the past. Once two chains meet they stay together, so eventually all r
coalesce before time 0 — and Theorem 2.5.1 says the common value they reach has the
distribution π exactly. Theorem 2.5.2 makes it practical: if the updating function
preserves a partial order with a least and a greatest state, and a single uniform sequence drives
every chain, the two extremal chains funnel all the others and their coalescence suffices.
Neither theorem is a statement about a program. Each says that a random variable is almost surely
finite, and that another has a distribution equal to π.
§2.5.4 treats the general case, through Borovkov's idea. An event A_n is renovating of length
m when, on it, W_{n+m} = Φ(ξ_n, …, ξ_{n+m-1}) — the sequence's value m steps ahead forgets
where it came from. Theorem 2.5.3 turns a condition on how often renovating events occur into
the existence of a finite stationary solution Z with Z ∘ θ = h(Z, ξ), and into strong
backwards coupling: W_n ∘ θ^{-n} is not merely convergent to Z but equal to it after a
finite random index.
Corollary 2.5.1 makes the limit independent of the initial condition — one stationary regime,
reached from every starting point. Theorem 2.5.4 is the converse: for ℝ₊^K-valued recurrences
with a constant initial condition, strong backwards coupling produces renovating events. So the
method characterises stability rather than merely detecting it.
§2.11 treats the multidimensional case, where the state is a vector and the natural models are
monotone and homogeneous. Theorem 2.11.1, due to Crandall and Tartar, is the key that unlocks
it: under homogeneity, monotone and non-expansive are the same property. That is what puts these
models within reach of Kingman's subadditive ergodic theorem, and Theorem 2.11.2 collects the
payoff — asymptotic growth rates γ̄ and γ_ exist, both almost surely and in L¹, and do not
depend on the initial condition.
Queueing folklore has a rule of thumb for the stability of an open network: saturate the queues
fed by the external stream, measure the departure intensity µ of the saturated system, and
declare the network stable when λ < µ. The book is careful that this saturation rule "does
not hold for all systems".
Theorem 2.11.3 (p.166), "the main result on the stability region", proves it for Monotone-Homogeneous-Separable networks:
If lim Z_{[-n,0]} → ∞ a.s., then λ γ(0) ≥ 1. If λ γ(0) > 1, then lim Z_{[-n,0]} → ∞ a.s.
Here γ(c) is the growth rate of the network fed by the scaled process cN, so c = 0 places
every arrival at the origin: γ(0) is exactly the saturated system's rate, and µ = γ(0)⁻¹.
Two implications, with a gap between ≥ 1 and > 1 that the book leaves open — as it leaves open
the critical case ρ = 1 of Loynes' theorem. Closing it would assert more than is proved.
Nothing here is on the platform or in Mathlib. There is no coupling from the past, no theory of
renovating events, and no Crandall–Tartar theorem. Order/Hom/* has monotone maps and
Topology/MetricSpace/* has LipschitzWith 1, which is the right ambient notion for
non-expansiveness in the sup-norm, but the equivalence between them under homogeneity is absent.
(P⁰, θ) is
ergodic and {ξ_n} is compatible with θ. The relation Z ∘ θ = h(Z, ξ) holds P⁰-a.s.{W_n^{[C]}}, the sequence its proof on p.119 builds the renovating
events for. The page prints {W_n^{[0]}} in the conclusion, and that version is false. Corollary
2.5.1 uses the renovating condition of (2.5.14), W_{n+m} = Φ(ξ_n, …, ξ_{n+m-1}), where the
page prints W_n.ℝ^K-valued random initial condition Y, under the book's linear lower bound
E[X_n^{[0]}] > −Cn.T_0 = 0,
T_n ∘ θ = T_{n+1} − T_1, ξ_n ∘ θ = ξ_{n+1}, E⁰τ_n = λ^{-1}, E⁰Z_n < ∞. The map X
satisfies (2.11.16) (it depends only on the points and marks in the index window) and the four
framework assumptions for every point process. γ(0) is the a.s. limit of
Z_{[-n,-1]}(0·N)/n. Dropping the marks would reduce the theorem to deterministic service,
and dropping the link between the points and θ makes the second implication false. Neither
is done.≥ 1 and > 1 left
open.Chapter 1 of Baccelli and Brémaud's Elements of Queueing Theory builds a calculus for stationary queues. Chapter 2 asks the prior question: when is there a stationary queue at all?
The G/G/1/∞ queue is one server at unit rate, infinite waiting room, fed by a stationary marked
point process {(T_n, σ_n)} — arrival epochs and required service times. Its workload W(t), the
service still owed by the server, obeys Lindley's equation between arrivals:
W(t) = (W(T_n−) + σ_n − (t − T_n))⁺, t ∈ [T_n, T_{n+1}). (2.1.6)
Nothing in that equation says a solution exists on the whole line, let alone a stationary one. The
answer is a sharp criterion in the traffic intensity ρ = λE⁰_A[σ_0].
Theorem 2.1.1 (p.80), which the book calls "the fundamental result of stability". Under
ρ < 1 there is a unique finite workload process on all of ℝ, compatible with the flow, and
it is given explicitly by the Loynes supremum
W(0) = sup_{n ≤ 0} ( T_n + Σ_{i=n}^{0} σ_i )⁺ , (2.1.12)
with W(T_n−) = 0 for infinitely many negative and infinitely many positive n (2.1.13). If
ρ > 1 there is no finite stationary workload process at all.
Each half earns its place. The supremum is what "the Loynes construction" means: look back from the
origin, take the work brought by customers n, …, 0 less the time −T_n since elapsed, and
maximise over how far back you look. The ρ > 1 half is what turns ρ < 1 from a sufficient
condition into a criterion. The critical case ρ = 1 is an explicit non-result in the book — there
"may or may not" be a stationary workload — and is deliberately absent from the statement.
§2.2 proves the theorem by Loynes' monotone scheme on the Palm space, and two of its steps are worth stating in their own right.
Lemma 2.2.1 (p.87) is the uniqueness engine: a non-negative, a.s. finite Z with
Z − Z∘θ ∈ L¹(P⁰) has E⁰[Z − Z∘θ] = 0. Applied to the difference of two stationary solutions, it
forces that difference to be invariant, and ergodicity then forces it to be zero.
Theorem 2.2.1 (p.90) runs the argument backwards. Its section is titled "Queueing Proof of the Ergodic Theorem", and it is exactly that: the queueing construction yields the pointwise ergodic theorem, in the ratio form
lim_n ( Σ_{i=0}^n σ∘θ^{-i} ) / ( Σ_{i=0}^n τ∘θ^{-i} ) = E⁰[σ]/E⁰[τ], P⁰-a.s.
Mathlib has the mean (von Neumann) ergodic theorem and no pointwise one, so this is absent substrate rather than a restatement.
The multiserver queue (§2.3). With s servers and the least-loaded-server rule, the state is
the ordered workload vector obeying the Kiefer–Wolfowitz recurrence, and the criterion becomes
E⁰[σ] < s E⁰[τ] (Theorem 2.3.1, p.93). Here uniqueness fails: p.94 exhibits a two-point space
with a whole interval of stationary solutions. What survives is that the solution set is bracketed
— M_∞ is minimal, and V^∞_∞ is the largest finite solution (Theorem 2.3.2, p.95).
Coupling (§2.4). Theorem 2.4.1 (p.99) is what "reaches the stationary regime" means: if a
sequence couples with a θ-compatible one, then the law of its whole shifted trajectory converges
in variation to the stationary trajectory's. The proof is one inequality,
|P̃_{X,k} − P̃_{Z,k}| ≤ P(N > k), and the finiteness of the coupling time.
The fluid queue (§2.7). Theorem 2.7.1 (p.131) replaces customers by two θ_t-compatible
random measures, the arrivals A and the service capacity C, and recovers the Loynes supremum
W(t) = sup_{u ≤ t}(A_{u,t} − C_{u,t}) under λ < µ — as the minimal solution, the book
claiming no uniqueness here.
ρ = λE⁰_A[σ_0] takes values in [0, ∞], so an input with E⁰_A[σ_0] = ∞ has ρ = ∞ and
falls under the non-existence half rather than being read as ρ = 0.E⁰[σ]/E⁰[τ] of Theorem
2.2.1, the threshold s E⁰[τ] of Theorem 2.3.1, and the fluid supremum (2.7.7).θ_t-compatible workload processes; maximality
in Theorem 2.3.2 is among measurable finite solutions; the coupling time of Theorem 2.4.1 is a
random variable. A formalization that dropped the explicit supremum, or the ρ > 1 half, would
trivialize the goal and is ruled out.None of it is on the platform or in Mathlib. The nearest platform item,
single_server_queueing_convergence_of_subcritical, presupposes a stationary workload and proves
two-time finite-dimensional convergence to it; Theorem 2.1.1 constructs that workload, proves it
unique, gives it in closed form, and adds the non-existence half. Different conclusion, different
generality, different Mathlib revision.
Chapter 1 of Baccelli and Brémaud's Elements of Queueing Theory has two halves. The first builds
Palm calculus from the Matthes definition of P⁰_N and reaches the Swiss army formula. This
mission is the second: §§1.6, 1.8 and 1.9, which supply the two things the rest of the book runs
on.
§1.6 states, in its own words, "the ergodic theory results to be used later in this book". Five of them, and the book proves none: Birkhoff's pointwise ergodic theorem in discrete (Theorem 1.6.1) and continuous time (Theorem 1.6.4), Kingman's sub-additive ergodic theorem (Theorem 1.6.2), and the extremal characterizations of ergodicity in both settings (Theorems 1.6.3 and 1.6.5) — ergodicity is exactly the impossibility of splitting an invariant probability into two distinct ones.
They are quoted, but they are not decoration. Kingman's theorem is what produces the asymptotic
growth rates of Theorem 2.11.2 and the constant γ(c) on which the saturation rule rests.
Birkhoff's theorem is what makes the time average in PASTA's (3.3.2) a well-defined object, and
what the fluid Loynes theorem invokes for lim_{u→−∞}(A_{u,0} − C_{u,0}) = −∞.
None of the three analytic ones exists in Mathlib. Analysis/InnerProductSpace/MeanErgodic is the
mean (von Neumann, L²) theorem, not almost-everywhere convergence, and there is no sub-additive
ergodic theorem at all. The platform has neither.
§1.8 introduces the stochastic intensity: a point process N admits the (P, F_t)-intensity
{λ(t)} when E[N(a,b] 1_A] = E[(∫_a^b λ(t)dt) 1_A] for A ∈ F_a. Around it sits the notion of a
predictable process — one measurable with respect to the strict past.
Theorem 1.8.1 is the structural fact that makes predictability usable. For the internal history of a marked point process, every predictable process has the concrete form
Z(t, ω) = v(t, θ_t ω), v(t, ·) F_{0−}-measurable. (1.8.1)
That is why mission IV can take this form as PASTA's hypothesis rather than constructing a predictable σ-field: Theorem 1.8.1 says nothing is lost.
Theorem 1.8.2 (p.61), §1.8.4, Watanabe's characterization of Poisson processes. For a
history F_t = F_t^N ∨ G and a G-measurable, locally integrable {λ(t)}, if N admits the
F_t-intensity {λ(t)} then N is a G-conditional Poisson process:
E[ e^{iuN(a,b]} | G ∨ F^N_a ] = exp{ (e^{iu} − 1) ∫_a^b λ(t) dt } . (1.8.12)
A stochastic intensity that carries no information beyond G forces the process to be Poisson
conditionally on G, with the compensator as the parameter — and the conditional characteristic
function is the exact Poisson one, not an approximation. With G trivial and λ constant this is
the ordinary Poisson process, which is the equivalence Remark 3.3.1 of Chapter 3 invokes to explain
the name PASTA. The book: "This result plays a role in queueing theory, especially for proving
that some streams in a queueing network are or are not Poissonian."
§1.9 asks whether the stochastic intensity is the same under P and under P⁰_N — whether the
two probabilities describe the same dynamics. Theorem 1.9.1 says yes, on ℝ₊: the same process
{λ(t)} serves both.
Theorem 1.9.2 is Papangelou's theorem, and it is the deepest statement of the section: N
admits a stochastic intensity if and only if P⁰_N ≪ P on F_{0−}, and then
λ(t) = (μ ∘ θ_t)λ with μ the Radon–Nikodým derivative. A dynamic property and a static one turn
out to be the same thing.
Theorem 1.9.3 is Mecke's characterization: N is Poisson exactly when P ≡ P⁰_N on
F_{0−}. The view from a point of the process and the view from a deterministic instant agree on
the strict past precisely when the process has no memory. It follows in one line from the two
theorems before it.
Four of the five missions in this series import the Chapter 1 substrate; this one adds the two pieces they need from its second half — ergodic theory and the stochastic intensity. Nothing here is on the platform, and Mathlib has filtrations and adapted processes but no predictability in this form, no stochastic intensity, no pointwise ergodic theorem and no Kingman.
Every result is stated in the book's strength, with the book's standing definitions as binders.
A discrete flow is a bijective, measurable, P⁰-preserving map (p.46); a continuous flow is jointly
measurable in (t, ω) (p.3, clause (a)). A history compatible with the flow satisfies
θ_t F_s = F_{s−t} (p.57), and an F_t-intensity is a non-negative, measurable, locally
integrable, adapted process (p.58). The limits of Theorems 1.6.1, 1.6.2 and 1.6.4 are asserted to
exist; Kingman's constant h̄ lies in ℝ ∪ {−∞} and is identified with
inf_n (1/n) E⁰[h_n], the means being extended reals so that E⁰[h_n] = −∞ is not read as 0.
Theorems 1.6.3, 1.6.5, 1.9.2 and 1.9.3 are equivalences, and Theorem 1.9.2 carries the closed form
λ(t) = (μ ∘ θ_t)λ with μ = dP⁰_N/dP on F_{0−}. The goal's conclusion is the exact conditional
characteristic function (1.8.12); a formalization that only asserted some conditional Poisson law,
or conditioned on G alone, would not be this theorem.
Anosov flows are the model of uniformly hyperbolic, chaotic continuous-time dynamics: a nonsingular vector field on a closed manifold is Anosov when the tangent bundle splits as , with uniformly contracted and uniformly expanded by the derivative of the flow. They are structurally stable, so one can hope to classify them up to topological equivalence. In dimension three this classification is far from complete: it is not known which closed 3-manifolds carry Anosov flows, nor how many inequivalent Anosov flows a given manifold can carry.
The classical examples — suspensions of hyperbolic toral automorphisms and geodesic flows of hyperbolic surfaces — are rigid (Plante; Ghys). Non-algebraic examples were built by Franks–Williams (a nontransitive Anosov flow, 1980), Handel–Thurston, Goodman, Fried, Bonatti–Langevin, Fenley, Barbot and others. Several of these examples glue together neighbourhoods of hyperbolic sets along their boundaries. Béguin, Bonatti and Yu (Geom. Topol. 21 (2017)) turned this into a general theory, and used it to answer questions of Katok and of Barbot–Fenley.
A plug is a compact 3-manifold with boundary and a nonsingular C¹ vector field transverse to . The boundary splits into the entrance boundary (where points inwards) and the exit boundary . The maximal invariant set consists of the points whose orbit stays in for all times. The plug is hyperbolic if is a hyperbolic set with one-dimensional strong stable and strong unstable bundles. The entrance lamination and the exit lamination are one-dimensional laminations of the boundary surfaces. The plug has filling MS laminations when every component of (and of ) is a strip: a disc whose accessible boundary consists of two leaves asymptotic to each other at both ends.
A diffeomorphism is a strongly transverse gluing map if and are transverse and cut into squares with sides alternately on leaves of the two laminations. Gluing then gives a closed manifold with an induced vector field . Two triples and are strongly isotopic if they are joined by a continuous path of such data.
Theorem 1.5 lets one build Anosov flows on closed 3-manifolds by gluing hyperbolic plugs. Proposition 1.6 gives a combinatorial criterion for the result to be transitive. Together they answer a question of Katok (Theorem 1.9) and questions of Barbot and Fenley on manifolds with several hyperbolic JSJ pieces supporting transitive Anosov flows (Theorem 1.13). They also show that transitive Anosov flows admit no fully canonical decomposition into finitely many transverse tori (Theorem 1.15). The results are proved in the source paper. None of them is formalized, and Mathlib has no theory of hyperbolic sets for flows, stable manifolds or laminations. A formal proof therefore needs a substantial amount of reusable smooth dynamics.
The glued vector field is generally not hyperbolic: perturbing the gluing map can create solid tori of parallel periodic orbits. The difficulty is to choose the gluing map (and the vector field within its topological equivalence class) so that cone fields on are mapped into themselves by the return map. The return map is the composition of the crossing map of the plug with the gluing map. Contraction and expansion must therefore be controlled simultaneously along two transverse invariant foliations. The paper achieves this after reducing to plugs with an affine Markov partition. The naive approach — fixing and trying to verify hyperbolicity — fails in general (Question 1.4 of the paper remains open).
EuclideanHalfSpace 3 with a structure; closed manifolds are compact, Hausdorff and BoundarylessManifold, and connected where the paper's statements concern a single manifold. Orientability is given by an atlas with positive Jacobians.flowMap X t x is when the orbit is undefined.The mean value problem, also called Smale's mean value conjecture, was posed by Stephen Smale in 1981 in his study of the complexity of root-finding algorithms for polynomials (Smale 1981). For a real differentiable function the mean value theorem produces, between two points, a point where the derivative equals a difference quotient. For a complex polynomial no such point need exist on a segment, and Smale asked for a substitute in which the special point is a critical point of the polynomial (a zero of its derivative). Estimates of this kind control how far Newton-type iterations can move, which is where Smale's original interest came from. The problem appears in lists of unsolved problems in mathematics, including Smale's own list of problems for the next century.
No absolute constant is known that works in every degree.
Let be a polynomial with complex coefficients of degree , and write for its derivative. A critical point of is a complex number with ; since , is a nonconstant polynomial of degree , so has at least one and at most distinct critical points. Fix a complex number that is not a critical point, . For every critical point we then have , and the difference quotient
is well defined. The question is how small this quotient can be made, relative to , by choosing the critical point well.
For every complex polynomial of degree and every with there is a critical point of with
The same with replaced by ; the example shows this constant cannot be lowered.
The result itself. A positive answer gives a sharp, degree-independent mean value inequality for complex polynomials: for every non-critical point, some critical value is reachable along a chord whose slope is at most the local derivative. Bounds of this type feed into the analysis of Newton's method and of path-following root finders, and into the study of how critical values of a polynomial are distributed relative to its values. The conjecture is part of a family of open extremal problems on the geometry of critical points, alongside Sendov's conjecture.
Formalizing it. The goal and the optimal-constant form are open. The milestones are published theorems, none of which is known to have a machine-checked proof. Formalizing Smale's bound and Tischler's special cases would put the classical tools of the subject (critical points of polynomials, univalent function estimates, root location) on a formal footing that later attempts can reuse.
The obvious strategies control the quotient through one critical point at a time: for instance, bounding by integrating along the segment from to . Such estimates lose a constant factor that depends on how the critical points are spread out, and the known uniform arguments all pass through distortion theorems for univalent functions, whose constants lead to close to . Reaching requires using all critical points simultaneously, and no argument doing this in every degree is known. The equality case , in which every critical point is equally bad, shows that any successful argument must be sharp for polynomials with maximally symmetric critical configurations.
Polynomials are elements of ℂ[X] (Mathlib's Polynomial ℂ); the degree is natDegree, the derivative is Polynomial.derivative, evaluation is Polynomial.eval, and the roots of are the multiset P.roots (counted with multiplicity). A critical point is a c : ℂ with P.derivative.eval c = 0. The absolute value is the norm ‖·‖ on ℂ, and the constants and are computed in ℝ from the cast of natDegree.
Every statement assumes . This is the standard normalization and is essential in Lean: division by zero returns , so without it the choice would make the inequality trivially true whenever is itself a critical point. With the hypothesis, every critical point differs from and the quotient is a genuine difference quotient.
Crane's bound is stated as the existence, for each degree , of a constant strictly below that works for all polynomials of degree exactly ; this is equivalent to the best constant in degree being strictly below that value.
A complete development needs basic facts on critical points of complex polynomials (existence, the Gauss–Lucas theorem), and, for the classical bounds, results from the theory of univalent functions such as the Koebe quarter theorem and coefficient estimates. These are reusable well beyond this mission. Contributions of any milestone, of supporting lemmas, and of partial results in fixed small degree are welcome.
A periodic point of a map is a point with for some . A nonwandering point is a much weaker form of recurrence: every neighbourhood of eventually returns to meet itself, for some . Every periodic point is nonwandering, but a nonwandering point need not be periodic, and the orbit of such a point may never come back to exactly.
Pugh's closing lemma asserts that this gap can be closed by an arbitrarily small change of the system: if is nonwandering for a diffeomorphism of a compact manifold, then some diffeomorphism , as close to as desired in the topology, has as a periodic point (Wikipedia, "Pugh's closing lemma"). The result was proved by C. C. Pugh in 1967 (Pugh 1967), in the same paper as the General Density Theorem: for a -generic diffeomorphism the periodic points are dense in the nonwandering set. The source article describes the lemma as establishing a close relationship between chaotic and periodic behaviour and notes that it underlies some autonomous convergence theorems. The article also points to Smale's problems as related material.
Let be a compact smooth manifold of dimension , Hausdorff and without boundary. Write for the set of diffeomorphisms : bijections such that and are continuously differentiable. For , denotes its tangent map on the tangent bundle.
The topology on is the coarsest topology for which is continuous, where the space of continuous self-maps of carries the compact-open topology. Two diffeomorphisms are -close when they, and their derivatives, are uniformly close.
For a map of a topological space:
For every and every ,
Milestones 1–4 are elementary background facts that are not stated in the source article; milestone 5 is the second theorem named in the title of the source's reference.
The result. The closing lemma turns a topological recurrence property into periodicity after a -small perturbation. Combined with genericity arguments it gives the General Density Theorem, so that for generic diffeomorphisms the whole nonwandering set is the closure of the periodic orbits. It is one of the basic perturbation tools of generic dynamics.
Formalizing it. The theorem is classical and proved in the literature. The drafter is not aware of a machine-checked proof. A formalization needs the topology on diffeomorphism groups, local perturbation lemmas in charts and the combinatorics of the closing argument. None of these is currently available in Mathlib as far as the drafter knows.
The first idea is to take the returning piece of orbit near and push it back to with a small local perturbation. This fails in the topology. Moving a point by distance with a bump supported in a ball of radius costs size about , and the return may happen at a distance comparable to the size of the only available ball. The perturbation then fails to be -small. The derivative along the return can also distort any fixed neighbourhood shape without bound. Controlling this distortion is the central difficulty.
BCWCentralizer_Basic. is M ≃ₘ^1⟮𝓡 d, 𝓡 d⟯ M, and the topology is induced by into C(TangentBundle, TangentBundle) with the compact-open topology. On a compact manifold this is the usual topology.PughClosingLemma_nonwandering, shared by all statements. It is reusable for any topological dynamics mission.Welcome contributions: a general theory of the topology on (for example, that it is Baire), local perturbation lemmas, and proofs of the milestones.
Two commuting diffeomorphisms of a manifold share all of their dynamics: permutes the orbits of and preserves every smooth and topological invariant of . The centralizer of ,
always contains the cyclic group , and has trivial centralizer when . S. Smale asked whether diffeomorphisms with trivial centralizer are dense, residual, or even open and dense in (one of Smale's problems for the 21st century).
Timeline: Kopell (1970) answered the question for on the circle; Palis–Yoccoz, Fisher and Burslem obtained results under hyperbolicity or partial hyperbolicity assumptions; Togawa treated generic Axiom A diffeomorphisms in the topology; Bonatti–Crovisier–Vago–Wilkinson showed that trivial-centralizer diffeomorphisms do not contain an open dense set in ; and Bonatti–Crovisier–Wilkinson (this paper, arXiv:0804.1416) proved residuality in for every compact manifold.
is a closed (compact, boundaryless), connected smooth manifold of dimension . is the space of diffeomorphisms of with the topology; a subset is residual if it contains a countable intersection of open dense sets.
There is a residual subset such that for every and every with , one has for some .
Following Section 2 of the paper: the classical upper-semicontinuity lemma used for Proposition 2.5, the wandering part of Theorem A (unbounded distortion is -generic), Proposition 2.5 (density of trivial Lipschitz centralizers implies residuality) and Theorem 2.3 (residuality of trivial Lipschitz centralizers when ).
The theorem answers the second (and hence the first) part of Smale's question in the topology, and exhibits a precise link between dynamical properties of (large derivative and unbounded distortion) and the algebraic structure of inside the group . The result is proved in the literature; it has not been formalized.
The density of trivial centralizers comes from perturbation results (Theorems A and B) that change the derivative without changing the topological dynamics (tidy perturbations in topological towers). Density alone does not give residuality, since the set of diffeomorphisms with the large derivative property is not residual (Appendix); the passage from dense to residual needs the Lipschitz centralizer and a semicontinuity argument.
is a charted space over with a atlas, Hausdorff, compact and connected; is Mathlib's type of diffeomorphisms. The topology is encoded as the topology induced by into the compact-open topology on continuous self-maps of the tangent bundle . Powers , , are taken in the permutation group of . Bi-Lipschitz homeomorphisms are defined chart-locally (equivalent on a compact manifold to bi-Lipschitz for a Riemannian distance). Jacobians are computed with respect to an arbitrary continuous Riemannian metric; the unbounded-distortion property does not depend on this choice.
Contributions welcome: the topology API (Baire property, continuity of composition), the Kupka–Smale and closing-lemma genericity results, and the perturbation machinery of Sections 3–7.
A central configuration of the Newtonian -body problem is a placement of point masses in which the gravitational acceleration of every body points toward the centre of mass and is proportional to its distance from it. Central configurations generate the only explicitly known solutions of the -body problem (the homographic, or self-similar, motions), they are the possible limiting shapes of total collisions, and they organise the topology of the integral manifolds. Counting them is therefore a basic question of celestial mechanics.
Timeline.
Fix bodies with masses ; body sits at . Write , and . A configuration with all is a central configuration (normalised so that the proportionality constant is ) when, for every ,
These equations are invariant under rotations of the plane; imposing removes this freedom, and a solution with this normalisation is a positive normalized central configuration (Definition 1 of the paper; Lean: PosNormalizedCC n m).
The proof works in the complex domain. Introducing unknowns (inverse distances) with turns the equations into the polynomial system (4) on :
A complex solution is a normalized central configuration (Lean: NormalizedCC n m), a real one if all are real (Lean: RealNormalizedCC n m). The potential is (Lean: potential n m).
There is a closed algebraic subset of codimension at least such that for all masses ,
The exceptional set is not made explicit; only its existence and dimension bound are asserted.
The same statement with all complex solutions of system (4) in place of the positive real ones.
For and every positive masses: finitely many positive (Theorem 1, Hampton–Moeckel) and even real (Theorem 5) normalized central configurations; finitely many complex ones unless the masses satisfy explicit polynomial relations (Theorem 3) or are all equal (Theorem 4).
Lemma 1 (a polynomial image of an affine variety is finite or cofinite), Lemma 2 (the potential takes finitely many values on the solution set), and the explicit mass vector .
The result. Theorem 2 is the first finiteness result for planar central configurations of five bodies, settling Smale's 6th problem for for generic masses; before it, no single 5-tuple of positive masses was known to have finitely many planar central configurations. Its four-body part gives a short proof of the Hampton–Moeckel theorem, including the real (not necessarily positive) solutions.
Formalizing it. The results are proved on paper; none of them is formalized. A formal development requires affine elimination theory (Chevalley's theorem on constructible images in the form of Lemma 1), a Sard-type argument on algebraic sets (Lemma 2), and the singular-sequence analysis of Sections 3–9, which is a long case analysis of limiting diagrams together with polynomial eliminations done by computer algebra in the paper.
Finiteness is not a local statement: nondegeneracy fails in general (Palmore), so no implicit-function argument applies, and a continuum of solutions would have to be excluded globally. In the complex domain continua genuinely exist for some masses (Roberts' continuum with a negative mass; its sign-modified version with positive masses solves system (4)), so any proof must use the positivity of the masses in an essential way, and the exceptional mass set of Theorem 2 cannot simply be dropped with the present method.
Fin n; the paper's bodies and are the indices 0 and 1, so the normalisation reads y 1 - y 0 = 0.NormalizedCC they are complex, as in Section 2 of the paper. Lemma 2 carries the paper's standing hypothesis that no nonempty subset of bodies has total mass zero (NoZeroSubMass).(x, y, δ); δ is a full n × n array constrained to be symmetric with zero diagonal, so it carries exactly the unknowns , . Finiteness of the solution set is unaffected by this encoding.massZeroLocus I of an ideal I of with ringKrullDim (ℝ[m] ⧸ I) ≤ 3. Taking is impossible (the quotient has dimension ), so the goal is not trivialised by an exceptional set equal to the whole mass space.Set.Finite of the solution set.Useful reusable infrastructure: finite-or-cofinite images of polynomial maps on affine varieties, and basic facts on central configurations (centre of mass, the identity ).
A base-stock (order-up-to) policy orders, in every period, exactly enough to bring the inventory position (stock on hand plus stock on order minus backorders) up to a target level. It is the policy used in practice for repairable and consumable service parts, and the analysis of every later chapter of Muckstadt's book assumes it. Its optimality is therefore a foundational question, and there are three classical ways to prove it.
This mission formalizes the third approach, in the finite-horizon single-location form presented in Section 2.2.1 of Muckstadt (2005).
A single item is reviewed in periods . An exogenous, time-homogeneous Markov chain on a finite set is observed at the start of period ; given , the demand has law and is independent of . Excess demand is backordered.
Every unit of demand is a customer, and customers are indexed in arrival order, the initially waiting customers first. A customer's distance is once served, while waiting, and for future customers in the order they will arrive. Units are indexed by location: (used), (on hand), (in transit) and (at the supplier, which holds countably many units). The state is
with the location of unit and the distance of customer . In period : units in transit move one location closer and the released units move from to (so an order is on hand periods later); the demand brings the customers at distances to distance and moves the others steps closer; units on hand serve waiting customers, lowest indices first; then is charged per unit on hand and per waiting customer, with . The criterion is the expected cost over the periods, discounted by .
A policy for the whole system chooses a finite set of units at the supplier to release. It is monotone if it releases lower-indexed units first, and committed if unit only ever serves customer . The subsystem is unit with customer under commitment, with state and actions Release and Hold. The set contains the optimal actions of a subsystem whose unit is at the supplier and whose customer is at distance , and the critical distance is
Every policy that, in each period and Markov state , releases the lowest-indexed units at the supplier to raise the inventory position to
is optimal for among all policies, from every starting state. Such a policy exists. The levels are not fixed numbers but the critical distances of the single-unit problem, so the goal asserts the structure of an optimal policy and identifies its levels, without committing to any constant.
and managing every subsystem independently and optimally is optimal for . 3. Lemma 2 (p. 28): implies . 4. Section 2.2.1.2.2 (p. 29): the critical distance policy, release if and only if , is optimal for every subsystem.
The result shows that under Markov-modulated demand a single-location system is optimally run by a state-dependent base-stock policy. The same unit–customer argument gives echelon base-stock optimality in serial systems with noncrossing stochastic lead times (Sections 2.2.2–2.2.3). The decomposition also yields the levels themselves: they are the critical distances of a two-action problem, which can be solved one customer at a time.
The theorems are proved in the literature (Muharremoglu and Tsitsiklis 2008) and in the book. To our knowledge no machine-checked proof of any base-stock optimality theorem exists, by dynamic programming or by decomposition. The book's proof is informal in three places a formalization has to settle:
A formal development makes each of these precise.
The obvious argument says that costs are linear, so the cost of is the sum of unit–customer costs and everything decouples. That is only half of Theorem 4. The pairing of unit with customer holds only under monotone policies, and a general policy for observes the whole infinite state , not just . The lower bound therefore needs Lemma 1 together with the fact that extra information about the demand history does not help a Markov decision problem. The upper bound needs the lowest-index matching to cost no more than committed matching.
The second difficulty is that the threshold structure is not the obvious consequence of Lemma 2. The set of distances at which releasing is optimal must be shown to be an initial segment when ties are allowed. Unbounded demand makes that set possibly unbounded (it is, in the last periods). Finally, the release decisions of the subsystems must be counted to recover an inventory position, which uses the invariant that future customers occupy consecutive distances.
Everything is in the namespace ServiceParts.UnitDecomp, with three definition files.
Model. Model bundles the chain, the demand law, , , and with the standing assumptions , , , together with the per-unit and per-customer motions and a generic finite-horizon expected-cost recursion. Costs are in .
Subsystem. Subsystem defines a subsystem, its optimal cost, , and the critical distance policy.
System. System defines with lowest-index matching, its policies (finite release sets), monotone and committed policies, starting states, the inventory position and the order-up-to release.
Conventions and pinnings:
Corrections to the book:
Out of scope: stochastic noncrossing lead times (Section 2.2.2), serial systems (Section 2.2.3; compare the disproved platform statement SupplyChainTheory.clark_scarf_sequential), and continuous review (Section 2.2.4, which the book calls intuitive).
Proofs of any milestone are welcome. A reusable by-product would be a general lemma that Markov policies are optimal among history-dependent ones for finite-horizon problems with countable randomness and costs in .
A scenario program replaces an uncertain optimization problem by its worst case over finitely many sampled instances. In its simplest form it reads
where is the cost of a decision when the uncertain parameter takes the value , and are independent draws from an unknown probability . The classical guarantee of the scenario approach (Campi and Garatti, 2008) bounds the probability that a new instance produces a cost above the optimal value , and it does so without any knowledge of .
That guarantee concerns a single number, . Two scenario programs with the same and the same optimal value can look very different at the solution: in one, most sampled costs lie just below ; in the other, they are widely scattered. The costs that do not determine the solution still carry information about how the cost of the chosen decision is distributed on future instances. Carè, Garatti and Campi (2015) showed that this information can be extracted with the same distribution-free character as the classical result, which is the subject of this mission. It is Chapter 8, §8.1 ("Probability box") of Campi and Garatti, Introduction to the Scenario Approach (SIAM/MOS 2018), the third mission of the series formalizing that book.
Timeline:
Let be a measurable space with a probability , and a cost that is convex in for every (a standing assumption of the book). For a sample of independent draws from , let be the solution of the program above and its optimal value.
Empirical costs (Definition 8.1). Sort the costs of the solution on the sampled scenarios in decreasing order, ; so .
Risk (Definition 8.2). For a decision and a level , . The risk of the -th empirical cost is , and .
Nondegeneracy (Definition 8.3). For every , with probability , . Costs with index below are excluded because several scenarios typically attain the maximum at .
Support constraints and full support (Definitions 5.1 and 5.4). In epigraph form, subject to , the constraint of scenario is a support constraint if removing it lowers the optimal value; the problem is fully supported if for every the program with scenarios has exactly support constraints with probability .
The ordered Dirichlet distribution with parameters is the law on with density .
Under nondegeneracy, for and all ,
This is an identity of joint distribution functions, not a bound, and it does not depend on or .
The result. The theorem controls the whole distribution function of the cost of the scenario solution on a new instance, not just one quantile of it. Discarding the extreme tails of the laws of yields, with a prescribed confidence , a region (the book's "probability box", Figure 8.2) that contains the entire cumulative distribution function of , computed from the sample alone. The first marginal recovers the classical Theorem 3.7, since makes the risk of at most .
Formalizing it. The theorem is proved in Carè, Garatti and Campi (2015); the book states it and gives no proof. No machine-checked version of the scenario approach, of its generalization theorem, or of ordered Dirichlet laws of risks is known to exist. A formalization would produce a checked proof of the distribution-free identity together with the combinatorial and measure-theoretic infrastructure (order statistics of sampled costs, laws of random risks) that the rest of scenario theory reuses. The milestones separate the classical beta bound, which is also the goal of the first mission of this series, from the new exact joint law.
The obvious attempt treats as the order statistics of the uniform variables . That works only for , when the decision space is a point and the costs are independent. For the decision is itself a function of the whole sample, so the sampled costs at are neither independent nor identically distributed, and the -th cost is tied to the scenarios that determine the solution. The factor and the constant encode exactly this dependence. Any argument must account for which scenarios are active at without assuming full support, since the theorem holds whether or not .
The decision space is EuclideanSpace ℝ (Fin n) and the book's is ; the sample is ω : Fin N → Δ with law Measure.pi (fun _ => P). Empirical costs are read from Tuple.sort with counted from ; risks are real numbers (P {δ | c < ℓ ν δ}).toReal. The right-hand side of the goal is a Lebesgue integral over the box intersected with the ordered simplex, stated for all real . The solution map is a hypothesis-constrained function, never an arbitrary map.
Implicit hypotheses of the book pinned down in the binders:
A statement in which the solution is an arbitrary measurable map, or in which the nondegeneracy or existence hypothesis is unsatisfiable, would make the goal vacuous; the hypotheses here are met, for example, by with a continuous law on , and for by any cost independent of with an atomless law.
A complete development needs: the scenario approach generalization theorem (reusable across this series), laws of order statistics of i.i.d. uniform variables, and the combinatorics of support sets of convex min-max programs. Proofs of the milestones, of the case of the goal, and of auxiliary facts about kthLargest are all welcome.
Feedback laws in engineering are applied with a lag: sensors, actuators and communication channels introduce a time delay between the measurement of a state and the control that reacts to it. For finite-dimensional systems small delays are usually harmless. For distributed systems such as the wave equation they need not be: Datko, Lagnese and Polis (SIAM J. Control Optim. 24, 1986) and Datko (SIAM J. Control Optim. 26, 1988) showed, for one-dimensional examples, that an arbitrarily small delay in a stabilizing feedback can destroy stability. The question matters to anyone who designs boundary or internal controllers for vibrating structures and wants to know whether a stabilizing law is robust to delay.
Nicaise and Pignotti (SIAM J. Control Optim. 45 (2006)) study the wave equation on a bounded domain of with a damping term that combines an instantaneous and a delayed velocity feedback, with coefficients and . They show that the system is exponentially stable when (Theorems 1.1 and 1.3), and that when stability can fail (Theorems 1.2 and 1.4). This mission is Theorem 1.4, the internal-damping instability result, in the case the paper proves.
Let and let be a bounded open set with boundary of class , split as with and . Write for the outer unit normal and for the normal derivative. Let , and let be the delay. With damping coefficient the problem is
with initial data , and a history on . The standard energy of a solution is
The condition is the paper's assumption (1.8). The paper's problem (1.12)–(1.16) carries a general coefficient with and near ; is one such coefficient.
If (1.8) fails, i.e. , then
and the same holds with "" replaced by "", for every . The goal asserts only non-decay, not a rate of growth or the value of the energy, so it survives any sharpening of the examples.
The result shows that the stability threshold of Theorem 1.3 is sharp in the sense that matters for design: at or beyond the threshold there is no delay margin, since delays as small as desired already produce solutions whose energy does not decay. Together with Theorem 1.3 it gives a complete dichotomy in the coefficients for the internally damped wave equation with delay, in any dimension, and it identifies the mechanism (roots of the characteristic equation on or to the right of the imaginary axis) that later work on delayed stabilization has had to avoid.
The result is proved in the paper; to the best of current knowledge it has not been machine-checked. The mission's product is a formal proof of the case together with its algebraic core: the reduction of the transcendental characteristic equation, the analysis of both cases, and the two-sided bounds on the delays. The spectral input it needs, an unbounded sequence of eigenvalues of the mixed Dirichlet–Neumann Laplacian with regular eigenfunctions, is reusable well beyond this paper.
The scalar part is elementary. The difficulty is the spectral input. The small delays come from with , so the proof needs infinitely many eigenvalues of the Laplacian with mixed Dirichlet–Neumann conditions on a domain, with eigenfunctions that are inside and up to the boundary. This requires compactness of the embedding , the spectral theorem for compact self-adjoint operators, and elliptic regularity for a mixed problem, none of which is available in Mathlib for domains in . A single eigenpair gives only the large delays (letting ); it does not give the small ones.
A second point: the paper's own bound bounds only from below, so it does not by itself give ; the upper bound of milestone 6 is needed.
EuclideanSpace ℝ (Fin n) with . The boundary is given by a global defining function (, , on ); ; the surface measure is pinned by the Gauss–Green formula for all fields.Boundary feedback stabilization of the wave equation asks whether a damping term placed on part of the boundary drives the energy of every solution to zero. Without delay the answer is classical: the feedback on a part of the boundary gives exponential energy decay under geometric conditions (Chen, Lagnese, Lasiecka–Triggiani, Komornik–Zuazua). In practice a feedback is applied with a lag, and a small lag can destroy stability. Datko, Lagnese and Polis (doi:10.1137/0324007) and Datko (doi:10.1137/0326040) showed, in one space dimension, that a purely delayed boundary feedback destabilizes the system for arbitrarily small delays.
Nicaise and Pignotti (doi:10.1137/060648891) study a feedback made of an instantaneous part and a delayed part, with weights and , in any space dimension. Their Theorem 1.1 gives exponential decay when . This mission formalizes the converse, Theorem 1.2: when , some delays admit solutions whose energy does not decay at all.
Timeline.
Let and let be a bounded open set with boundary of class . The boundary is split as , with and . Write for the outer unit normal and for the surface measure. Together these data form a mixed domain (MixedDomain n in Lean).
Fix and a delay . The problem (1.1)–(1.3) is
with initial data , and a history on (1.4)–(1.5). The standard energy of a solution is (3.7)
Condition (1.8) of the paper is . This mission concerns the complementary case .
For real functions on , (5.11) defines and .
If , there exist delays and, for each , a classical solution of (1.1)–(1.3) with delay and a constant such that
The statement fixes no formula for the delays and no value of the energy. It asserts only the existence of infinitely many delays for which the energy does not decay.
The result. Theorem 1.2 shows that the threshold of Theorem 1.1 is sharp in the following sense: once the delayed weight reaches the instantaneous one, no geometric assumption restores asymptotic stability for every delay. Together, Theorems 1.1 and 1.2 separate robust from non-robust boundary feedbacks by a single inequality between the two gains. The explicit delays of case (a), , become arbitrarily small or large. So even an arbitrarily short lag in an equally weighted feedback can remove decay.
The formalization. The paper proves the result. It has not been formalized, and Mathlib has no wave equation on domains, no mixed eigenvalue problems and no Sobolev spaces on domains. This mission produces:
Milestones 1 and 2 are calculus and trigonometry. The difficulty sits in producing . The goal needs a nonzero function that is in and up to the boundary and solves an eigenvalue problem with mixed Dirichlet and Neumann (case (a)) or Dirichlet and Robin-type (case (b)) boundary conditions. Existence requires compactness of and of the trace into , followed by elliptic regularity up to a boundary. None of these is in Mathlib.
A shortcut does not work: in case (b) the frequency enters the boundary condition, so is not an eigenfunction of a fixed self-adjoint operator. The page instead minimizes a non-quadratic functional, and its first-variation computation (5.18)–(5.19) needs care: the functional is not 2-homogeneous, so the normalization by does not literally give , although the first-order condition is right.
Taking real parts does not give a real-valued solution with constant energy: in case (b) the energy of oscillates.
A complete development needs the following:
These pieces are reusable well beyond this mission. Contributions of any of them, or of an alternative route to a with the required properties, are welcome.
The alternating direction method of multipliers (ADMM) is a standard method for problems of the form , in which a smooth loss is composed with a structured, possibly nonsmooth regularizer through a linear map . Its convergence theory was developed for convex problems, yet it is routinely run on nonconvex ones: sparse recovery with the constraint, low-rank matrix problems, and total-variation-type models with nonconvex penalties. For such problems a practitioner wants a guarantee about the iterates actually produced, not only about the existence of good subsequences.
Li and Pong (arXiv:1407.0753v6, SIAM J. Optim. 25(4), 2015) gave the first such guarantee for the classical ADMM on nonconvex composite problems with a surjective . Their Theorem 1 shows that cluster points of the (proximal) ADMM are stationary; their Theorem 3, the subject of this mission, shows that for semi-algebraic data the whole sequence converges. The argument adapts the Kurdyka–Łojasiewicz (KL) framework of Attouch, Bolte and Svaiter (Math. Program. 137, 2013) to a setting where the ADMM only decreases its merit function in the -block.
Fix linear, twice continuously differentiable with bounded Hessian, and proper (finite somewhere) and closed (lower semicontinuous). For the augmented Lagrangian is
The ADMM produces from arbitrary by
Assumption 1 with asks for , and symmetric maps with , and for all , , and .
The limiting subdifferential of consists of limits of regular subgradients at points with . A point is stationary if .
A set in is semi-algebraic if it is a finite union of sets cut out by finitely many polynomial equations and strict inequalities ; a function is semi-algebraic if its graph is. A proper has the KL property at if there are , a neighbourhood of and a continuous concave with , , , such that whenever and . A KL function is proper, closed, and KL at every point of .
In the Lean development is augLag h P M β x y z, and also augLagX h P M β as a single function on the triple space with the Euclidean inner product.
Under the standing assumptions and Assumption 1 with , if and are semi-algebraic and the ADMM sequence has a cluster point , then
No constants are fixed: every parameter is quantified exactly as in the paper.
Milestones 6, 7 and 8 together imply the goal.
The result. Theorem 3 upgrades subsequential convergence to convergence of the whole iterate sequence, with finite length of the -trajectory, for a nonconvex ADMM without any convexity of or . Semi-algebraicity covers the paper's applications: polynomial losses, the constraint, and indicators of polyhedral or algebraic sets. Remark 4(1) isolates the only property actually used, the KL property of , so the result extends to any class of functions for which that property is known (for instance, globally subanalytic or o-minimal definable data).
Formalizing it. The result is proved in the paper and, as far as is known, formalized nowhere. The mission produces a machine-checked version of the paper's convergence argument, a Lean definition of the KL property with the correct convention for empty subdifferentials, and a semi-algebraic set predicate over MvPolynomial. Milestone 8 is a published theorem of real algebraic geometry and nonsmooth analysis (Bolte–Daniilidis–Lewis 2007) that the paper quotes without proof; it is part of what a complete development of the goal requires.
The obvious route is to invoke the abstract convergence theorem of Attouch–Bolte–Svaiter for descent methods. It does not apply: its sufficient-decrease hypothesis requires to drop by a multiple of , while the ADMM only guarantees a drop proportional to (Remark 4(2)). The relative-error bound (35) is likewise in terms of the -step alone, and relating the - and -blocks back to the -block uses the surjectivity of and the specific structure of the multiplier update. The neighbourhood on which the KL inequality holds is a neighbourhood of the full triple, whereas the trajectory is controlled only in .
The semi-algebraic part has a separate difficulty: showing that is semi-algebraic needs closure of semi-algebraic sets under projection (the Tarski–Seidenberg theorem), and the KL property of semi-algebraic functions needs the Łojasiewicz inequality for subanalytic or semi-algebraic functions. Mathlib has neither.
Spaces are EuclideanSpace ℝ (Fin n); is a continuous linear map and its adjoint. and take values in EReal, never passed through toReal except where the value is provably finite. is Mathlib's Loewner order on self-maps; the Hessian is fderiv ℝ (gradient h). The ADMM is the proximal-ADMM relation with ; argmin steps are "value at most the value anywhere", with no uniqueness; is unconstrained. The triple space is the nested product, so its inner product is the sum of the block inner products.
The KL inequality is stated for every , which encodes . Writing it with Metric.infDist 0 (∂f x) would give and make the KL property fail at every point with empty subdifferential, so that "semi-algebraic implies KL" becomes false and the goal becomes a statement about a different notion. The KL property is required only at points of , only on a neighbourhood and only for values in ; is differentiable only on the open interval. Semi-algebraicity of an extended-valued function is that of its graph over its real values. is a positive real, which is equivalent to the paper's .
The hypotheses and are part of the theorem, not a simplification: the analogous statement for the proximal ADMM is open (Remark 4(3)). The cluster point is assumed, not derived.
Needed infrastructure: calculus of the limiting subdifferential (a smooth-plus-separable sum rule), the Tarski–Seidenberg theorem, and the Łojasiewicz/KL inequality for semi-algebraic functions. The last two are reusable far beyond this mission; contributions toward them, and toward the analytic core (milestones 1–6), are welcome.
Traffic information systems (TIS) such as navigation apps send drivers private, noisy signals about the state of the road network: incidents, weather, closures. When several such systems coexist, their subscribers act on different information, and the congestion each population experiences depends on how all of them route. A question then arises for transport planners and for the information providers themselves: if travelers are free to choose which system to subscribe to, which market shares of the competing systems are stable?
Wu, Amin and Ozdaglar (Operations Research 69(1):148–163, 2021; preprint arXiv:1808.10590) model this situation as a Bayesian routing game with heterogeneous information and answer the question exactly: the equilibrium adoption rates are the minimizers of a convex function of the population sizes, the equilibrium value of a weighted potential. This mission formalizes that characterization (Theorem 4 of the paper) together with the results its proof rests on. A companion mission (Value of Information in Bayesian Routing Games I) formalizes the paper's other main result, the sign and monotonicity of the relative value of information between two populations.
A Bayesian routing game has a single origin–destination pair, a finite set of edges and a finite nonempty set of routes (each route a set of edges), and a finite set of network states . Travelers of total demand are split into populations , one per TIS; population has size , where the size vector lies in the simplex . Each population receives a signal (its type) from a finite set ; states and type profiles are drawn from a common prior . Edge in state has cost at load , positive, strictly increasing and differentiable.
A strategy profile assigns to each population and type a split of its demand over routes, with ; these form the polytope . It induces route flows and edge loads . A traveler of population with signal forms the belief and evaluates the expected route cost . A Bayesian Wardrop equilibrium (BWE) is a in which every type uses only routes of minimal expected cost. The equilibrium population cost is
The weighted potential is , and is its equilibrium value. In route-flow form, is the same expression in terms of ; route flows satisfy linear constraints (14a)–(14c) (a separability condition across populations, total demand , nonnegativity) and one information impact constraint per population, , where measures how much of the demand reacts to population 's signal. Let be the set of minimizers of subject to (14a)–(14c) only, and
In the two-stage game, travelers first choose a TIS, inducing , and then play . A size vector is a vector of equilibrium adoption rates if no traveler gains by switching TIS:
For every and every BWE of ,
With the existence of a BWE for every , this is the paper's statement that the set of equilibrium adoption rates is .
A separate item states the existence of a BWE for every .
The result. Theorem 4 reduces a question about a two-stage game with a continuum of travelers and private signals to the minimization of one convex function over a simplex. It shows that the stable market shares form a convex set, generally not a single point, so each system's equilibrium adoption rate ranges over an interval; and that this set is determined by the joint information environment of all systems, not by each system's signal alone. On the equilibrium edge load does not depend on the shares at all, which identifies when changes in market shares leave congestion unchanged.
Formalizing it. The proofs of Theorem 1, Proposition 2 and Proposition 5 are in the paper's online e-companion, and Lemma 5 relies on sensitivity results for parametric convex programs cited from the literature. No part of this development has, to our knowledge, been machine-checked. A complete formalization would produce a verified potential-game characterization of Bayesian Wardrop equilibria with heterogeneous information and a verified directional-derivative formula for the optimal value of a parametric convex program; nothing comparable is currently on the platform (the existing Wardrop development covers complete information only).
The direction " implies (31)" is not a pointwise statement about costs: it follows from being the argmin of together with the formula linking directional derivatives of to cost differences. Both are hard. The derivative formula (26) is a statement about the optimal value of a convex program whose feasible set moves with ; its standard proofs pass through uniqueness of Lagrange multipliers, which fails exactly at the degenerate size vectors () that Theorem 4 must cover, since an unused TIS is a legitimate outcome. The identity needs the route-flow reformulation (Proposition 2), in which the size vector enters only through the information impact constraints, and the uniqueness of the minimizing edge load. The natural first idea, comparing population costs directly at a given equilibrium, gives no handle on which size vectors make them equal.
The Lean development lives in the namespace BayesRouting.Adoption. Populations, types, states, edges and routes are finite types; type spaces and the route set are nonempty; routes are edge sets. The game is a structure whose fields include the paper's standing assumptions: the prior is a probability distribution, , and each cost is positive on nonnegative loads, strictly increasing and differentiable (on all of , which loses no generality). One assumption is added: every type profile has positive probability. Without it the equilibrium edge load need not be unique and the beliefs can be undefined; it excludes the paper's Example 2(i) (perfectly correlated signals).
Conventions: size vectors range over the probability simplex; is the infimum of over and is only compared at points of the simplex (outside it the feasible set can be empty and the value is a default); is the last form of the paper's (7), well defined when ; is the maximum over reference profiles, which equals the paper's value on flows satisfying (14a); equilibrium statements are made for every BWE rather than for "the" equilibrium; and similar sets are argmin sets. Lemma 5 is stated for the directions with (otherwise leaves the simplex); is allowed.
A trivializing formalization is ruled out: the existence of a BWE is its own item, so "for every BWE" is not vacuous, and is defined by (30) from the flow problem (28), not as the argmin of , so the goal is not a restatement of Proposition 5.
Infrastructure a complete development needs: KKT conditions for convex programs with linear constraints, convexity of integrals of increasing functions, compactness arguments for existence of minimizers, and one-sided directional derivatives of optimal-value functions. The last two are reusable well beyond this mission. Proofs of any item, and of auxiliary lemmas such as Proposition 1 of the paper (feasible route flows form the polytope ), are welcome.
The Hamiltonian of a single nonrelativistic particle in moving in a potential is the Schrödinger operator acting in . Before anything can be said about the dynamics or the energy levels of such a particle, one must know that is a genuine observable: a self-adjoint operator on a specified domain. For potentials that decay at infinity one also wants the coarse structure of the spectrum, namely that it is bounded below and that everything below the continuum threshold consists of isolated eigenvalues of finite multiplicity. The hydrogen atom, with the Coulomb potential in three dimensions, is the central example.
The self-adjointness results go back to T. Kato's 1951 paper on the Hamiltonians of atoms; the identification of the essential spectrum through relatively compact perturbations is due to H. Weyl's theorem and its later extensions. This mission follows Chapter 10 of G. Teschl, Mathematical Methods in Quantum Mechanics (AMS GSM 99, 2009), Sections 10.1, 10.2, 10.4 and 10.5.
is the complex Hilbert space of square integrable functions with respect to Lebesgue measure. The free Schrödinger operator is with domain the Sobolev space ; equivalently, is the inverse Fourier transform of the maximally defined multiplication by . Units are and mass .
A real function acts by the multiplication operator on its maximal domain . The sum is defined on . denotes the bounded Borel functions vanishing at infinity, and the smooth compactly supported functions.
For a linear operator , the resolvent exists when maps bijectively onto with bounded inverse; the resolvent set collects such and . The point spectrum is the set of eigenvalues; the discrete spectrum consists of the eigenvalues that are isolated in and have finite-dimensional eigenspace; the essential spectrum is . An operator is relatively compact with respect to if and is compact for one . is bounded from below if on for some real , and a subspace is a core of a closed operator if the closure of the restriction to it is the operator itself.
The hydrogen Hamiltonian is on . A function in is positive if it is a.e. and not a.e. zero, and strictly positive if it is a.e.; a bounded operator is positivity improving if it maps positive functions to strictly positive ones.
Let and real with if and if . Then is relatively compact with respect to , and has domain , is self-adjoint and bounded from below, satisfies
and has as a core.
The result. Theorem 10.2 is the existence theorem for one-particle quantum mechanics with decaying potentials. It makes an observable on the natural domain , guarantees a lowest energy, and places the continuum exactly at , so that all spectral information below zero is carried by bound states. Its three-dimensional case covers the Coulomb potential, and the same scheme (relative boundedness, Kato–Rellich, relative compactness, Weyl) is the template for the -body HVZ theorem. The virial theorem, the qualitative and the explicit hydrogen spectrum, and the nondegeneracy of ground states are the standard first applications.
Formalizing it. None of these statements is formalized. Mathlib has the Fourier transform, tempered distributions and Sobolev spaces on the distribution side, and LinearPMap with adjoints and closures, but no free Schrödinger operator as an unbounded operator on , no resolvent set or essential spectrum for unbounded operators, and no self-adjointness theorem for . The mission asks for proofs of Teschl's statements and, with them, a reusable definition of on and of maximally defined multiplication operators.
The goal combines several chapters of the book. A proof needs self-adjointness of on via the Fourier transform, the Sobolev bound of Lemma 10.1 to get with relative bound zero, the Kato–Rellich theorem, compactness of operators of the form (Lemma 7.11) to obtain relative compactness, Weyl's theorem on the invariance of the essential spectrum, with no eigenvalues, and the fact that is a core for . None of these intermediate results is in Mathlib for unbounded operators.
The milestones add their own difficulties: the virial theorem requires the dilation group and a derivative argument on domains; Corollary 10.4 requires a variational argument producing infinitely many negative eigenvalues; Theorem 10.9 requires separation of variables in spherical coordinates and the Laguerre polynomials; and Theorem 10.12 uses the Trotter product formula and strong resolvent convergence to transfer positivity from to .
is EuclideanSpace ℝ (Fin n) with Lebesgue measure and is Mathlib's Lp ℂ 2 volume, a separable complex Hilbert space. Unbounded operators are Mathlib LinearPMaps, sums of unbounded operators are LinearPMap sums on the intersection of domains, self-adjointness is Mathlib's IsSelfAdjoint, and "core" is LinearPMap.HasCore. The resolvent is the bounded two-sided inverse of ; , , , and are defined from it, and Mathlib's Banach-algebra spectrum is not used. Compactness is IsCompactOperator.
The Fourier transform is Mathlib's unitary transform with kernel , not Teschl's . is defined as and as ; both coincide with the book's objects, independently of the normalization. No projection-valued measure or functional calculus is taken as data. is Mathlib's space of continuous functions vanishing at infinity, and positivity of complex values is taken in ComplexOrder.
The virial hypothesis is stated as for almost every , for every , which is what the operator identity means for a multiplication operator. Corollary 10.4's index set is read as the sequence . Only the eigenvalue formula of Theorem 10.9 is included, not its explicit eigenbasis.
A trivializing formalization is ruled out: the only hypotheses of the goal are the function-space conditions on and . Neither , a relative bound below one, nor closedness of is assumed; the equality of the domain with and the relative compactness of are conclusions. The essential spectrum requires all three of "eigenvalue", "isolated" and "finite multiplicity" in its complement, so is a genuine identification.
One-dimensional bin packing asks for the fewest unit-capacity bins that hold a given list of items with sizes in . It is the model behind cutting stock (cutting rolls of paper or steel to ordered widths), memory and file allocation, and batch scheduling on identical machines, and it is NP-hard. Its algorithmic study is therefore about approximation: how close to the optimum a polynomial-time algorithm can guarantee to come.
An instance is a finite multiset of piece sizes, each in the open interval . Write for the number of pieces, for the number of distinct sizes, and for the sum of all sizes. A packing of is a finite multiset of bins, each a multiset of sizes, whose union is exactly and in which every bin has total size at most . Its cost is the number of bins, and is the minimum cost.
A configuration of is a nonempty multiset of sizes occurring in with total at most . With the number of pieces of size and the number of occurrences of in configuration , the fractional bin-packing problem is the linear program
whose optimal value is . A basic feasible solution is an extreme point of its feasible region.
For instances , write if there is a one-to-one map from the pieces of into the pieces of with . Linear grouping with parameter sorts non-increasingly, cuts it into groups of consecutive pieces (the last possibly shorter), rounds every piece of up to the largest size of to get , and outputs and .
ALGORITHM 1 takes and : (1) discard the pieces of size , leaving ; (2) apply linear grouping to with , giving and ; (3) put each piece of in its own bin; (4) obtain from a Fractional Bin-Packing subroutine a basic feasible solution of the LP of with ; (5) round to a packing of with at most bins; (6) shrink the pieces back to obtain a packing of ; (7) insert the discarded pieces, opening a new bin only when a piece fits nowhere. is the cost of the resulting packing.
The additive term depends on only, so ALGORITHM 1 is an asymptotic approximation scheme. The paper prints the factor , which fails for ALGORITHM 1 as printed (see Formalization scope); running the algorithm with gives the paper's main result (4), , stated as a separate corollary with the explicit term .
The result showed that the configuration LP, of exponential size in general, can be used for a guaranteed approximation: its value is within of the integer optimum, and grouping reduces at small cost. The same template (eliminate small items, group, solve the configuration LP, round a basic solution, reinsert) underlies later schemes for bin packing, cutting stock, bin packing with cardinality constraints and scheduling, and the LP-based analysis is the starting point of the Rothvoß and Hoberg–Rothvoß improvements.
The theorems are proved in the literature; none of them has a machine-checked proof on the platform or, to our knowledge, in Mathlib. This mission produces a checked analysis of the algorithm, including a correction: the printed approximation factor is not valid for the algorithm as printed, and the checked statement records the factor its proof yields. The definitions (instances, packings, the configuration LP, basic solutions, the order , any-fit insertion) are reusable for the second mission of the series and for other bin-packing results.
The Lean statements are short, but several proofs need linear-programming structure that is not in Mathlib in this form. Lemma 2 and Corollary 1 use that an extreme point of has at most as many nonzero coordinates as there are rows of ; the configuration LP is indexed by a finite but implicitly described set of multisets. Monotonicity of under ("clearly" in the paper) requires transporting a fractional solution across a piece-to-piece matching whose images are types, not pieces. The existence of a run requires an optimal basic feasible solution of the configuration LP. Lemma 3 concerns an insertion process with unrestricted order and bin choice, so its bound has to hold for every execution, not for one greedy rule.
Multiset ℝ; packings are Multiset (Multiset ℝ) with join equal to the instance, bin loads at most , empty bins allowed and counted. is a natural-number infimum over a set that is always nonempty.Multiset ℝ →₀ ℝ supported on configurations. is a real infimum over a set that is nonempty (singleton configurations) and bounded below by . "Basic" is the extreme-point property; the bound on the number of nonzero coordinates is a consequence, not the definition.Alg1Run ε I P: is a possible output. Every open choice is quantified: the subroutine's output, the packing of Step 5 (any packing within the stated bound), the size reduction of Step 6 (bin by bin), and the insertion of Step 7 (any order, any fitting bin). The goal holds for every run, and a separate item states that a run exists, so the goal is not vacuous.Proofs of any item are welcome; Lemma 2, Corollary 1 and the monotonicity display are the most reusable.
A holomorphic function on an open set of restricts to a real hypersurface as a function that satisfies the tangential Cauchy–Riemann equations: it is annihilated by every antiholomorphic vector tangent to . Functions on with this property are called CR functions, and they are the boundary values that several complex variables studies whenever a domain is approached through its boundary. The basic question is the converse: when is a CR function locally the restriction of a holomorphic function? For smooth data the answer is "not always" (the book's Example 3.2.7 gives a smooth CR function on the hyperplane that is no such restriction). For real-analytic data the answer is "always", and that is Severi's theorem, the goal of this mission.
The mission follows Chapter 3 of Jiří Lebl's open textbook Tasty Bits of Several Complex Variables (version 4.4, 2026), where Severi's theorem is proved by complexification: a real-analytic function of and is treated as a holomorphic function of two independent variables restricted to the diagonal . The milestones are the steps of that route: uniqueness on totally real slices, the two complexification propositions, the fact that restrictions of holomorphic functions are CR, and the normal form of a real-analytic hypersurface.
Write with . A function on an open subset of is real-analytic if near each point it equals a convergent power series in the real coordinates. A set is a real-analytic hypersurface if near each of its points, after choosing one real coordinate among the and collecting the other as , it is the graph of a real-analytic function .
A function on an arbitrary set is smooth (respectively real-analytic) if near each point of it agrees on with a smooth (respectively real-analytic) function defined on an open neighbourhood. A defining function of at is a smooth real function on an open with nonvanishing derivative and ; is a smooth real hypersurface if it has one at every point.
With the Wirtinger derivative , the space of antiholomorphic tangent vectors of at is
A smooth is a CR function if for all and , where is computed on any smooth local extension of . A real-analytic CR function is a CR function that is real-analytic on .
In Lean, is Fin n → ℂ, and these notions are the definitions IsRealAnalyticOn, IsRealAnalyticHypersurface, IsSmoothHypersurface, IsSmoothOnSet / IsRealAnalyticOnSet, antiholTangent and IsSmoothCRFunction / IsRealAnalyticCRFunction of the namespace LeblSCV.CR.
Let be a real-analytic hypersurface, , and a real-analytic CR function. Then there are an open neighbourhood of and with
Severi's theorem identifies the real-analytic CR functions on a real-analytic hypersurface with the local traces of holomorphic functions. Together with Proposition 3.2.6 it shows that, in the real-analytic category, the tangential Cauchy–Riemann equations are exactly the obstruction to holomorphic extension. It is the model for the later extension theorems of the chapter: the Baouendi–Trèves approximation theorem (Theorem 3.3.1) and the Lewy extension theorem (Theorem 3.4.1), which replace real-analyticity with smoothness and pay for it with one-sided extension or approximation. Complexification (Propositions 3.1.3 and 3.1.5) is also a tool in its own right, used for the composition of real-analytic maps (Proposition 3.1.10) and for pluriharmonic functions.
All results here are classical and proved in the book; none of them is formalized in Lean or Mathlib as far as a search of the Prove2Me corpus and Mathlib shows. Mathlib has real and complex analyticity (AnalyticOnNhd), the one-variable and several-variable identity theorems for analytic functions, and the holomorphic implicit function theorem is within reach, but it has no notion of real hypersurface, CR vector or CR function. The mission produces that layer and a checked proof of the first extension theorem for CR functions.
The obvious idea is to take a real-analytic extension of , complexify it to a holomorphic function of variables, and substitute to remove . That produces a holomorphic function of , not of ; showing that it does not depend on requires transporting the CR equations, which hold only on , to the whole complexified hypersurface. That transport is a uniqueness statement for the complexification, and it rests on the normal form of Proposition 3.2.8, itself an application of the holomorphic implicit function theorem to the complexified defining function together with its reality symmetry. On the Lean side, the diagonal is not a complex submanifold, so identity theorems along it (Lemmas 3.1.2 and 3.1.4) do not follow from the standard identity theorem for open sets.
Fin n → ℂ, with 0-based indices; is the product type. The sup norm of Fin n → ℂ never enters a statement: no ball, norm or distance occurs.DifferentiableOn ℂ, which is equivalent to the book's Definition 1.1.2 there. A domain is an open connected (hence nonempty) set.AnalyticOnNhd ℝ on an open set, applied to as a real vector space, which is the book's power series in (equivalently in ).Mathlib.Analysis.Analytic.Basic (analytic functions, AnalyticOnNhd). https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/Analytic/Basic.htmlThe Russian option of Shepp and Shiryaev pays its holder, at an exercise time of their choosing, the running maximum of the stock price, discounted, with no fixed maturity. It is the standard example of a perpetual lookback option, and its value is a model problem of optimal stopping for a two-dimensional Markov process (the price and its running maximum). Perpetual contracts are simple to analyse but economically unrealistic: every real contract ends. Canadization (Carr, Randomization and the American put, Rev. Financial Stud. 11, 1998, https://doi.org/10.1093/rfs/11.3.597) replaces a fixed maturity by an independent exponential time . The holder must exercise before ; if they have not, they are paid the claim evaluated at . Because the exponential law is memoryless, the problem stays time-homogeneous and its value can be computed in closed form, while it approximates a contract of finite expected life .
Avram, Kyprianou and Pistorius (AKP04) solved both the perpetual and the Canadized Russian problem when the log-price is a spectrally negative Lévy process: a process with stationary independent increments whose only jumps are downward. This covers Brownian motion with drift, the Black–Scholes model, and jump-diffusions with downward jumps (crashes). Their answer is written with the scale functions , of the process. This mission is the third of three drawn from that paper, and formalizes the Canadized problem (§7, Theorem 3).
Timeline. Shepp and Shiryaev (1993) solved the Russian option for geometric Brownian motion. Carr (1998) introduced Canadization for the American put. Kyprianou and Pistorius (Ann. Appl. Probab. 13, 2003) studied perpetual options through fluctuation theory; §7 of [AKP04] builds on their calculations. Avram, Kyprianou and Pistorius (2004) solved the perpetual and Canadized problems for general spectrally negative Lévy processes.
Let be a filtered probability space with right-continuous, and let be a spectrally negative Lévy process adapted to : , paths càdlàg with no upward jumps and not monotone, increments stationary and independent of . The standing assumption is that has unbounded variation, or bounded variation and a Lévy measure .
The Laplace exponent is . Fix with , and let be the Esscher measure, .
For the -scale function vanishes on , is continuous on , and satisfies for , where is the largest root of . Further, . All scale functions in this mission are those of .
Starting from (the paper's ), the reflected process is , where and the position is . Its passage time above is .
Let , and let be an exponential random variable of rate which under is independent of . The Canadized Russian problem (32) is
over all -a.s. finite -stopping times . Write .
With
for every :
and is a -a.s. finite -stopping time attaining the supremum. The statement covers every variation regime at once.
In attack order:
The result. Theorem 3 gives the price and the optimal exercise rule of a Russian option with random (exponential) maturity, for every spectrally negative Lévy model at once. It makes three things explicit. The optimal rule is a threshold rule for the reflected process . The threshold is the crossing point of one explicit function of the scale functions. Whenever (possible only with bounded variation), immediate exercise is optimal. Because scale functions are known in closed form for many models, including Brownian motion with drift and hyper-exponential jump-diffusions (§8 of the paper), the theorem produces explicit prices.
Formalizing it. The result is proved on paper. It is not formalized in any proof assistant, and none of its infrastructure is available in Lean. This mission produces:
A machine-checked proof would also check the verification argument, which the paper states in detail only for the unbounded-variation case.
The obvious route is to compute the value of every threshold rule (Lemma 3) and optimize over . That identifies the right candidate, but it does not show that no other stopping time does better. The verification step needs two things for all regimes of : that is a supermartingale, and that stopped at is a martingale. For processes of bounded variation, is only continuous, not , at , so a smooth Itô formula does not apply directly. Computing the expected -integral up to uses excursion theory of away from , which Mathlib does not have. Eliminating is easy only if is independent of the whole filtration. If it is independent of alone, a stopping time could depend on .
ℝ≥0) and values are real. Random times take values in WithTop ℝ≥0, and the payoff is on . Expectations of nonnegative payoffs are lower Lebesgue integrals in , and is an extended-real supremum, so no expectation defaults to . Equalities with a real right-hand side also assert finiteness.