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.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
A reentrant line is a queueing network in which every customer follows one fixed route but may return to a station after visiting another one. A manufacturing line can have this pattern when a product revisits the same machine at different processing stages. A station can then have little nominal workload and still face unstable queues under an unfortunate service order. Dai and Weiss studied this gap between nominal capacity and fluid stability for reentrant lines in their 1996 paper. The four-class line associated with Lu and Kumar is their sharp example: its behavior changes at a simple cross-station inequality that is different from either station's ordinary workload constraint.
The paper establishes several positive stability results for other disciplines and networks, then gives an exact boundary for the Lu–Kumar line. Here the exact boundary is the focus. The result concerns fluid models, deterministic large-scale approximations of queue trajectories. It does not assert positive Harris recurrence or transience of the underlying stochastic network in both directions. The paper cites Dai's earlier implication from a stable fluid model to a stable stochastic discipline, but the converse was still open in its concluding discussion (Dai and Weiss 1996, pp. 119 and 133).
There are four customer classes, encountered in order . Classes and use station ; classes and use station . Each class has a positive mean service time and service rate . The external arrival rate is normalized to one. The nominal workloads are and , both assumed strictly below one. These assumptions say that each station has enough average capacity for its own stages, but they leave the scheduling decision unresolved.
At time , is the amount of class- fluid, and is the cumulative service time devoted to that class. The fluid equations balance the inflow and outflow of each class. Outside fluid enters class at unit rate; completion of class feeds class until class exits. Service times and idle times are nondecreasing, and a station's idle time can increase only when its total queue content is zero. A pair with these properties is a work-conserving fluid solution.
The Lu–Kumar priority discipline gives class priority over class at station , and class priority over class at station . Its fluid model adds the priority complementarity condition: service capacity available to a priority prefix can be unused only when that prefix has no immediate workload. For either model, fluid stability means that some common time empties every admissible solution with , with all queues remaining zero for . Instability is the negation of this statement; it does not require every solution to diverge.
Theorem 5.1 and Remark 1 give two connected classifications, under , , and :
The first clause captures the paper's existence of an unstable work-conserving policy: on the unstable side, the named priority discipline supplies one; on the other side, every work-conserving fluid model is stable. The second clause records the particular policy classification stated in Remark 1. Equality belongs to the unstable side: the paper exhibits a periodic nonempty solution there (Dai and Weiss 1996, pp. 125–127).
The milestones follow the paper's own statements and proof claims. The real-analysis extinction criterion of Lemma 2.2(ii) and the maximum-of-components criterion of Lemma 3.2 provide the stability language. Display (3.2), already available as a proved platform theorem, identifies the derivative of an attained maximum at a regular point. The priority condition (4.4) implies the ordinary work-conserving condition (1.13). The unstable half records one first cycle, one solution with every scaled cycle, and instability of the priority model. The stable half records the authors' explicit parameter choice, the two linear Lyapunov conditions, and stability of every work-conserving fluid solution.
The threshold says that the two station-load inequalities alone do not characterize stability of all work-conserving service orders. The extra inequality determines when the entire work-conserving fluid class is stable; its failure admits a concrete priority discipline with a nonempty trajectory. At the boundary , growth need not be strict: periodic fluid behavior already defeats finite-time stability. The result therefore distinguishes the paper's global stability region from the larger parameter region in which both stations are nominally underloaded (Dai and Weiss 1996, Remark 1, p. 125).
A machine-checked development would give reusable definitions for a four-stage reentrant fluid model, its priority complementarity condition, and the precise unit-initial-state notion of stability. The local Lean statements in this proposal compile, but their proofs remain open. The published maximum-derivative fact is the one already proved platform component used by this mission. The other milestones identify the mathematical work needed to formalize the known 1996 result, rather than presenting the result as a new open conjecture.
The ordinary load test controls how much service each station needs on average, but it does not control which class receives service when several buffers at a station are nonempty. In the Lu–Kumar priority discipline, serving a high-priority downstream class changes the future arrival pattern seen by the other station. Thus a direct argument from and to queue extinction fails. On the stable side, checking a single station's workload is also insufficient: its content may fall while earlier-stage fluid continues to feed it. The paper formulates two linear components and a finite maximum; the challenge is to obtain a uniform negative drift whenever that maximum is positive, including times when one station is empty and the other determines the active component (Dai and Weiss 1996, pp. 126–128).
Classes and stations are Fin 4 and Fin 2, with zero-based Lean indices: paper class is Lean index . The fixed station map is . Service times remain real parameters with explicit positivity hypotheses. Paths are total functions of real time, while equations and conclusions apply only on . The external arrival rate is one, and initial size is the sum , since class contents are nonnegative. The nominal-load assumptions are the two strict inequalities in (5.1). The named priority ranking is a permutation; it encodes only the station-local comparisons that matter.
Conditions (1.13) and (4.4), printed as complementarity or “increases only when empty,” use an equivalent interval-constancy condition in Lean. No extra Lipschitz or continuity assumption is placed on solutions: the fluid equations and monotone capacity constraints are intended to supply that regularity. Derivatives at regular points are represented with HasDerivAt. Lemma 2.2(ii) uses the non-strict bound , the version used by the paper's applications, although its displayed hypothesis prints . The p. 127 line involving prints ; (5.3) fixes the intended coefficient as .
The goal uses Definition 1.3 exactly: one uniform emptying time for all solutions of unit initial content. An impossible solution predicate, or an instability claim that only asks for a nonzero state at time zero, would not represent the paper's theorem. The mission needs finite-index sum and maximum infrastructure, absolute continuity and almost-everywhere differentiation on nonnegative time, plus elementary algebra of service rates and the cycle scaling. These components can be reused in later fluid-network missions. Contributions that preserve the source's hypotheses and boundary case are welcome.
A multiclass queueing network can be unstable even when every station has enough capacity on average: the queue lengths grow without bound although each server's nominal load is below one. Kumar and Seidman, Lu and Kumar (1991) and Rybko and Stolyar (1992) exhibited such networks under simple priority disciplines. This raised the question of which networks are stable under every reasonable policy, and which policies are stable in every network. Dai (1995) reduced the stability of a queueing network to the stability of its deterministic fluid model, so that the question becomes one about solutions of a system of linear equations and inequalities.
Dai and Weiss (1996) use this reduction to study reentrant lines, the model of semiconductor wafer fabrication in which a single route visits the same machines many times. Section 6 of their paper treats Kelly-type lines, in which every visit to a station has the same mean service time. Kelly (1979) showed that such networks with exponential service times are stable under FIFO and have a product-form stationary distribution. Theorem 6.1 shows that with two stations, and a route that never visits the same station twice in a row, stability holds under every work-conserving policy, not only FIFO. This mission formalizes that theorem.
A reentrant line has stations and classes . Fluid enters class at rate , moves from class to class on service, and leaves after class . Class is served at station with mean service time and rate . The constituency of station is and its nominal workload is . The traffic condition (1.7) is for every .
A fluid model solution is a pair : is the fluid in class at time and the cumulative service time given to class by time . They satisfy, for ,
with nondecreasing, and the idle time , where , is nondecreasing. The solution is work-conserving if increases only at times when station holds no fluid. The immediate volume of station is .
The line is of Kelly type with station means if for every class . Its routing has no immediate feedback if for every . A set of fluid solutions is stable (Definition 1.3) if there is a such that every solution in the set with is empty from time on.
For a two-station Kelly-type reentrant line without immediate feedback that satisfies (1.7), the work-conserving fluid model is stable: there is with
for every work-conserving fluid solution . The number of classes is arbitrary, of either parity, and the route may start at either station.
The milestones follow the proof on p. 130 and the two general lemmas it uses: the extinction criterion of Lemma 2.2 (ii); the derivative of a maximum at an active index, display (3.2), already proved on the platform; the piecewise-linear Lyapunov Lemma 3.2; the drift identity for , with ; the comparison ; and the verification that meet the hypotheses of Lemma 3.2 with .
The result. Theorem 6.1 gives a class of networks in which stability needs no knowledge of the scheduling policy: any policy that never idles a server with work waiting is stable whenever the nominal loads are below one. For queueing networks this is the property usually called global stability. Through Theorem 1.1 of the paper (Dai 1995, Theorem 4.3) the fluid statement implies positive Harris recurrence of the corresponding multiclass queueing network under every work-conserving head-of-the-line policy. The paper's Remarks 2 and 3 show the boundary: with immediate feedback (the line with all means ), or with three stations, a Kelly-type line can be unstable. A two-station Kelly-type line without immediate feedback is a unidirectional ring with one customer type, so the theorem is a special case of the ring-network result the paper proves as Theorem 6.2. That result is an open goal on the platform (ProcessingNetworks.GlobalStability.ring_globally_stable, Dai and Harrison's Theorem 8.24) in a different encoding of the fluid model.
Formalizing it. The theorem is proved in the paper, and the mission formalizes that proof. No machine-checked proof of the result, or of the Lyapunov lemmas it uses, is known to exist. The mission also produces reusable pieces: a fluid model of reentrant lines in the paper's own formulation, an extinction lemma for absolutely continuous functions, and the max-of-linear Lyapunov lemma, which the paper uses again in §§3 and 5.
The obvious Lyapunov function, the total workload, does not work: a work-conserving policy may starve a station while the other one is busy, so the total content need not decrease. The paper's components each decrease at the constant rate while station is busy. When station is idle, can grow, and the argument then needs the comparison , which requires the alternating route. The analytic difficulty is the passage from these pointwise statements to extinction. Fluid paths are only Lipschitz. The maximum need not be differentiable where the maximum switches, and the drift statements hold only almost everywhere. Lemma 2.2 (ii) and the derivative-of-a-maximum fact (3.2) make this step rigorous. The proof for odd is not printed ("can be proved similarly"), and the formal goal covers it.
All objects live in the namespace DaiWeissFluid.KellyType. The conventions are fixed as follows.
Fin K, Fin I). The paper's class is Lean k - 1.ℝ → Fin K → ℝ, and every equation is imposed for only. Derivatives are taken at via HasDerivAt.The goal must not be trivialized. It quantifies over all work-conserving solutions with , and this set is nonempty: a sorry-free witness with is checked locally. Neither the Kelly-type hypothesis nor the absence of immediate feedback may be dropped (Remark 2), nor may the goal be generalized beyond two stations (Remark 3). Restricting it to even , or to a route starting at station 1, would weaken it.
Contributions welcome: proofs of the general Lemmas 2.2 (ii) and 3.2, which apply across the whole series; the drift identity, which is pure algebra from (1.8); the continuity facts for fluid paths (Lipschitz bounds from (1.10)–(1.12)); and the final assembly.
Boundary feedback is the standard way to stabilize vibrating structures governed by wave equations: a sensor measures the velocity at the boundary and an actuator applies a force proportional to it. For the one-dimensional damped wave equation with such feedback, the closed loop is uniformly exponentially stable (Chen, 1979). In practice the measured velocity reaches the actuator only after a computation time, so the feedback acts with a time delay . The question addressed by Datko, Lagnese and Polis (1986) is whether arbitrarily small delays can destroy the stability of a system that is stable without them.
Their note answers it with an explicit example and a sharp threshold on the feedback gain. It is the founding example of delay-induced instability in boundary stabilization, cited by most later work on robustness of boundary control to delays.
Timeline.
Fix real numbers (damping), (feedback gain) and (delay), and put . The delayed system is
A classical solution is a function with complex values satisfying (1), (2), (8).
Separated solutions lead to the eigenvalue problem
The spectrum is the set of for which this problem has a solution not identically zero on . The paper encodes it through the entire functions
and the critical gain . In Lean these are K a, f a k ε ω, h a k ε ω, delaySpectrum a k ε, IsClassicalSolution a k ε u and IsExpUnstableSolution a k ε u in the namespace DatkoDelayWave.BoundaryDelay.
In attack order: the characteristic equation (16) ( for ); separated solutions; Lemma 1 (one zero of forces infinitely many zeros of and in every vertical strip around it); (17)–(18) (no zeros of in the right half-plane below or at the critical gain); the half-plane bound below the critical gain; (19) (no purely imaginary zeros at the critical gain); the explicit zero ; density of the delays ; the root family (12)–(15) above the critical gain; Lemma 2 (an open dense set of delays with zeros of in ); the three parts of the THEOREM separately; and, off the goal's path, the undelayed formula for .
The result shows that exponential stability obtained by boundary velocity feedback is not robust to delays when the gain is above : delays from a dense set of lengths, including arbitrarily small ones, produce exponentially growing modes. When the critical gain is , so every positive gain is fragile. Below the critical gain the spectral gap survives every delay. This identifies a quantitative robustness margin and motivated the later analysis of delayed boundary control, including the Nicaise–Pignotti theorems already posed on the platform for a different, multidimensional model (NicaiseDelayWave.*).
The result is proved in the paper, partly by citation: Lemma 1 is quoted from Datko (1978) without proof, and the open-mapping step of Lemma 2 is sketched. No machine-checked version exists. A formalization would check the threshold computations, supply the strip-zero lemma for this exponential polynomial, and give a rigorous version of the open-mapping step.
The algebraic parts, (16)–(19) and the explicit zeros, are calculations with complex exponentials. The difficulty is in Lemma 1 and Lemma 2. Lemma 1 needs the almost-periodic structure of exponential polynomials in vertical strips together with a Hurwitz or Rouché type argument, and neither is in Mathlib. Lemma 2 needs zeros of to persist under small changes of the real parameter . The paper's route through the logarithmic map (11) does not work as printed, because it is stated with the principal branch exactly on the branch cut. In part (i), the delicate step is excluding accumulation of zeros at the imaginary axis as , which the half-plane estimate alone does not give.
Parameters are real, , eigenfunctions are maps and solutions are maps (space first). Partial derivatives are deriv of the sections. Solutions and eigenfunctions are required to be on all of , resp. ; this loses no eigenvalue, since solutions of (5) are combinations of . Committed readings of the paper's loose phrases:
Trivializing encodings are ruled out: defining the spectrum as the zero set of would make a spurious spectral point, and reading "exponentially unstable" as "the spectrum meets " would delete the solution-level content of part (iii).
A complete development needs zero-counting tools for exponential polynomials in strips (almost periodicity, Hurwitz's theorem), which would be reusable for other delay equations. Contributions to any milestone, and to that general infrastructure, are welcome.
In distributionally robust modelling, a baseline probability model on a space is distrusted, and the analyst reports the largest expected loss over every model within a budget of . Blanchet and Murthy (arXiv:1604.01446; Math. Oper. Res. 44(2), 2019, doi:10.1287/moor.2018.0936) measure the budget with an optimal transport cost and prove strong duality for the resulting worst-case expectation on an arbitrary Polish space, with a lower semicontinuous cost and an upper semicontinuous performance function. Duality computes the worst-case value. A risk manager also wants the worst-case model: a distribution that attains the value, whose structure explains which perturbation of is most harmful.
Such a model need not exist. Unlike the Kantorovich problem, where the set of couplings with two fixed marginals is weakly compact, the feasible set here fixes only one marginal and is not compact in general. Section 5 of the paper gives an example on where the supremum is not attained, then gives abstract conditions under which it is (Proposition 9), and growth conditions on a locally compact normed space that imply them (Corollary 1). Related existence results in were obtained by Gao and Kleywegt (arXiv:1604.02199, 2016) and, for empirical baselines and norm costs, by Mohajerin Esfahani and Kuhn (arXiv:1505.05116, 2018).
Let be a Polish space with its Borel -algebra, a probability measure on , a budget, a cost and a performance function. The standing assumptions are:
The primal feasible set consists of the probability measures on with first marginal and (transport plans out of of cost at most ). The primal objective is and the primal value is . The dual feasible set consists of pairs with , universally measurable and for all . The dual objective is and the dual value is . For put .
Section 5 assumes throughout that is a dual optimal pair with . Write for the plans in concentrated on .
(P-Compactness): for every there are a compact with and such that has compact closure. (P-USC): whenever converge weakly to .
On a normed space : (A3) for , with nondecreasing and . (A4) for an increasing with ; and for every , once .
Let be a real normed space that is locally compact, and let satisfy (A1)–(A4). Under the standing assumption, if there is with
The result. An attained worst case turns duality into a structural statement. By Theorem 1(b) of the paper, an optimizer moves mass from only to maximizers of and, when , uses the full budget. When those maximizers are unique (Remark 8: convex in , concave) the worst-case model is unique and is the image of under a transport map. That map is what stress tests and robust estimators are built from. Without existence, these statements describe an object that may not be there.
Formalizing it. The paper's proofs are complete; nothing here is open. No machine-checked version of this result is known: the worst-case optimal transport literature, including the strong duality of this paper, is unformalized. The mission produces the transport objects of §2 in a form that keeps the paper's generality (Polish space, lower semicontinuous real cost, universally measurable dual variables, the convention), a tightness argument for nearly optimal one-marginal plans, and an upper semicontinuity argument for unbounded upper semicontinuous integrands under uniform integrability.
The obvious argument takes a maximizing sequence and extracts a weak limit. Both steps fail without more structure. First, is not tight: only the first marginal is fixed, and a sequence may push mass to infinity at bounded cost. That is exactly what happens in Example 2 (p. 26), where and the value is approached but never reached. Tightness has to come from the dual: nearly optimal plans concentrate near maximizers of , and (A3)–(A4) with confine those maximizers. Second, is only upper semicontinuous and unbounded, so weak convergence alone does not give . A uniform integrability bound is needed, and it uses the restriction to in an essential way. A third, Lean-specific difficulty is measure-theoretic: is only universally measurable, and the gaps of Remark 4 are integrals against completions.
All declarations sit in the namespace ModelRiskOT.PrimalOpt. Values of , , , and are in EReal. is with lower integrals, and Mathlib's realises the paper's reading of the supremum (footnote 2, p. 5). Integrals of nonnegative or extended-real functions are lower integrals (lintegral), never Bochner integrals. Universal measurability is the published BertsekasShreve.AnalyticSelection.IsUniversallyMeasurable. Weak convergence is the topology of ProbabilityMeasure (S × S). Measures on use the product -algebra.
The following readings are fixed:
EReal convention.LocallyCompactSpace. It also carries PolishSpace, which is redundant, since a locally compact real normed space is finite-dimensional.The goal cannot be satisfied by a junk value: and are EReal suprema and infima, not real sSup, and the hypothesis is kept because Example 2 shows the conclusion fails without it. A sorry-free check that , on satisfy (A1), (A3) and (A4) accompanies the drafts.
A complete development needs Prokhorov's theorem (in Mathlib), a Fatou lemma for weakly converging measures with a lower semicontinuous integrand, an upper semicontinuity theorem for uniformly integrable upper semicontinuous integrands, and the change of variables for universally measurable . The last three are reusable well beyond this mission. Proofs of any milestone, and these general lemmas as separate contributions, are welcome.
A probability model for a risk quantity, such as the reserve process of an insurer or the path of a queue, is usually chosen for tractability or fitted to limited data, and the true law of the system is unknown. Distributional model risk asks how large a probability of interest could be if the true law were any model "close" to . When closeness is measured by an optimal transport cost rather than a likelihood ratio, the competing models may put mass where puts none, which is the situation for rare events such as ruin or buffer overflow: the event of interest often lies outside the support of the baseline.
Blanchet and Murthy (arXiv:1604.01446, Mathematics of Operations Research 44(2), 2019) prove strong duality for worst-case expectations over an optimal-transport ball on a general Polish space, with a lower semicontinuous cost. Their §2.4 specializes the duality to worst-case probabilities of a closed set and obtains a closed-form answer: the worst-case probability of is the baseline probability of an inflated version of . This mission formalizes that result, Theorem 3 of the paper, together with the numbered statements its proof uses.
Let be a Polish space with its Borel -algebra, its probability measures, and the baseline. A cost satisfies Assumption (A1): it is nonnegative, lower semicontinuous, and if and only if .
For , a coupling of and is a probability measure on with marginals and ; is the set of couplings, and the optimal transport cost is
For a budget , the primal feasible set consists of the probability measures on with first marginal and .
Fix a nonempty closed set and let be the cheapest cost of moving unit mass from into . The worst-case probability is
Its dual is the univariate problem
and for a minimizer of (13) the paper defines
If attains the infimum in (13) and , then
Theorem 3 converts a supremum over an infinite-dimensional ball of probability measures into a single probability under the baseline: of the set of points that can reach at cost at most , where is determined by through the one-dimensional function . For the cost of a metric this is the baseline probability of the -neighbourhood of . The paper uses it to compute worst-case ruin probabilities for the Cramér–Lundberg model around a Brownian approximation (§3, §6.1), where is a path space; the result applies there because nothing in it uses local compactness of .
The result is proved in the paper. As far as the platform's corpus shows, neither it nor the strong duality behind it has been formalized. A formal development produces, beyond Theorem 3: a reusable definition of optimal transport costs with lower semicontinuous costs on Polish spaces; the coupling reformulation of the transport ball, which rests on the existence of optimal transport plans (Villani, Optimal Transport, Theorem 4.1), not in Mathlib; and an -optimal-plan argument that avoids assuming a primal optimizer exists.
The heuristic derivation on pp. 9–10 constructs an optimal transport plan that moves each with to a nearest point of and leaves the others in place. It needs a nearest point to exist and to be selectable measurably, which fails for general closed in a non-locally-compact space, and it needs a primal optimizer, which need not exist. Theorem 3 assumes neither, so the construction is not a proof. A second point is the boundary level : when charges it, as for atomic baselines, the identity (15) can fail (for a point mass at distance from and , the worst case is , not ), and the hypothesis is exactly what excludes this. Measurability is a second obstacle: is an infimum of a lower semicontinuous function over and in general only universally measurable, so integrals of it are taken against the completion of .
All objects live in the namespace ModelRiskOT.WorstProb. carries [TopologicalSpace S] [PolishSpace S] [MeasurableSpace S] [BorelSpace S]; is a Measure S with IsProbabilityMeasure; the cost is a real-valued c : S → S → ℝ with (A1) bundled as a structure (nonnegativity, lower semicontinuity on , and ). Committed conventions:
ℝ≥0∞; integrals are lower Lebesgue integrals and the positive part is ENNReal.ofReal. For the universally measurable functions and sets that occur, lower integrals and outer measures agree with the completion of , which is the paper's reading (p. 4). No Bochner integral is used.A formalization in which the transport ball fixes only the first marginal would contain every probability measure and give for every nonempty ; the definitions here fix both marginals of the couplings in , and the hypothesis is kept as stated rather than replaced by continuity of .
A complete development needs the existence of optimal couplings for lower semicontinuous costs (tightness and Prokhorov's theorem, available in Mathlib), the strong duality of the paper's Theorem 1 specialized to indicators (milestone 3; a separate mission in this series formalizes Theorem 1 in general), and universal measurability of through projections of Borel sets. The transport-cost definitions and the coupling reformulation are reusable beyond this mission. Proofs of any milestone are welcome, as are proofs that derive (13) from the general strong duality once that is published.
The single-machine scheduling problem asks for an order in which to process jobs, each with a processing time and a weight, on one machine, respecting a partial order of precedence constraints, so that the weighted sum of completion times is as small as possible. It is NP-hard, and the best known approximation ratio for general precedence constraints is . Ambühl, Mastrolilli, Mutsanas and Svensson (Math. Oper. Res. 36(4), 2011) relate the problem to the dimension theory of partial orders: their Theorem 3.2 states that when the precedence constraints are given together with a realizer of size , the problem has a -approximation algorithm. Small realizers of structured precedence orders therefore translate directly into better approximation ratios.
This mission formalizes one such structural result, Lemma 4.1 of the paper: every convex bipartite order has a realizer of size . Convex bipartite orders form a class of precedence constraints that lies strictly between strong bipartite orders and general bipartite orders (Möhring, 1989). Combined with Theorem 3.2, the lemma gives a -approximation for on this class. According to the authors, the bound for convex bipartite orders had not been known before.
A poset is a set with a reflexive, antisymmetric, transitive relation . Two elements are incomparable, written , when neither nor ; the set of incomparable pairs is . A linear extension of is a linear order on with . A linear order reverses the pair when in . A realizer of size is a family of linear extensions of such that every incomparable pair is reversed by at least one . The dimension is the least for which a realizer of size exists.
A convex bipartite order has jobs split into minus jobs and plus jobs . Each plus job carries two indices , and a minus job precedes exactly when . There are no other precedences: the predecessors of each plus job form a nonempty interval of consecutive minus jobs.
For the Appendix construction, the incomparable pairs are sorted into three sets according to the kinds of the two jobs, the order of their indices and, for a pair (plus job , minus job ), whether precedes some plus job of larger index than . The sets describe what the -th linear order of the realizer must contain.
Equivalently, . The goal holds for every numbering of the jobs and every choice of interval ends .
The result. Lemma 4.1 places convex bipartite orders among the classes of precedence constraints for which has an approximation ratio strictly below , namely through Theorem 3.2 of the paper. The bound is tight: a bipartite order has dimension exactly when it is a strong bipartite order (Möhring), so the bound cannot be lowered for the class of convex bipartite orders. Since also gives for the graph of incomparable pairs, a -realizer yields an optimal colouring of that graph.
Formalizing it. The result is proved in the paper, with a short case analysis in the Appendix. No machine-checked proof is known to exist. Mathlib has no dimension theory of posets: realizers, reversals of incomparable pairs and the construction of linear extensions containing a given acyclic relation have to be set up here. The definitions of realizer and linear extension are stated for an arbitrary relation and can be reused for other dimension bounds (interval orders, semiorders, the other missions of this series).
The three relations are not partial orders. , for instance, is not transitive: with two minus jobs and one plus job with , the pairs and are present but lies in . The step that requires work is to show that each has no cycle, so that it extends to a linear order. For this depends on the convexity of the predecessor intervals and on the numbering of the plus jobs by their left ends: it is not a consequence of bipartiteness alone. The goal itself carries no numbering assumption, so any proof must also account for renumbering the plus jobs.
All declarations live in the namespace SingleMachinePrec.ConvexBipartite.
N → N → Prop. Linear orders use Mathlib's unbundled class IsLinearOrder. A linear extension of is a linear order with ; reverses when and . A realizer of size is a function Fin t → N → N → Prop, so repeated members are allowed, as in the paper's multisets.Fin a ⊕ Fin b: Sum.inl i is the minus job , Sum.inr k the plus job , with indices starting at . The interval ends are maps l r : Fin b → Fin a with l k ≤ r k, and is equality together with the pairs (minus , plus ) with . A file-level instance records that is a partial order. Any convex bipartite order in the paper's sense is one of these after naming its jobs. The cases and are allowed.Monotone l of this milestone only.A trivializing formalization would let the members of the realizer be arbitrary relations, which makes reversing every pair free. Here every member must be a linear order containing .
Contributions welcome: proofs of the two milestones and of the goal; a general lemma that a relation whose transitive closure is antisymmetric extends to a linear order on a finite type; and the renumbering argument that removes the numbering assumption.
Path-following interior point methods solve a linear program by tracking its central path, a smooth curve that runs through the interior of the feasible set and ends at an optimal solution. Their number of iterations is polynomial in the bit size of the input, and whether some interior point method is strongly polynomial (bounded by a polynomial in the number of variables and constraints alone) is open. Bayer and Lagarias called the central path "a fundamental mathematical object underlying Karmarkar's algorithm". Dedieu and Shub proposed its total curvature as an informal complexity measure: a path that turns little should be easy to follow with straight steps. Several results bound that curvature:
A linear program in slack form has a real matrix , , and :
For the point of the central path is the unique solution of
The primal central path is .
For and , the program minimizes over subject to
With slacks it becomes with , , .
For points of Euclidean space with , the turning angle is the angle between the vectors and . For a curve parameterized over , the total curvature is
The milestones also use the field of absolutely convergent generalized real Puiseux series . Such a series can be evaluated at large real , and it has a valuation , its leading exponent. Read over , is one linear program. The valuation of its central path at is the tropical central path , a piecewise-linear curve with an explicit recursive description (Propositions 20–21 of the paper).
For every and there is such that for all ,
for the central path of . Here may depend on and . Both the primal and the primal-dual curves are part of the goal, as in the paper.
The theorem shows that the total curvature of the central path is not bounded by any polynomial in the number of constraints: has constraints and curvature at least about . This settles the conjecture of Deza, Terlaky and Zinchenko in the negative. It also shows that the averaged upper bounds of Dedieu–Malajovich–Shub and De Loera–Sturmfels–Vinzant cannot hold for every region. A companion mission of this series formalizes the paper's second main result, an exponential lower bound on the number of iterations of log-barrier path-following methods on the same family.
The result is proved on paper. As far as is known, it has not been formalized in any proof assistant, and Mathlib has no notion of the total curvature of a curve, of Puiseux-series evaluation and valuation, or of the tropical central path. Formalizing the theorem would give a machine-checked reference point for a much-cited negative result in interior point theory. The Lean definitions of total curvature and of the turning angle are general and reusable.
The total curvature is a supremum over inscribed polygons, and a lower bound needs explicit polygons whose angles can be estimated for every large . The central path of has no closed form, so its points cannot be written down at given parameters . Numerical evidence at a fixed says nothing uniform in . The natural first idea, to compute the path's angles directly from system (1) for a fixed instance, gives no handle on how the number of turns grows with . What is needed is control of the path's geometry uniformly over the whole scale of , with turns located at once, and the threshold is not explicit.
Vectors in which angles are measured are EuclideanSpace ℝ (Fin d). The turning angle is InnerProductGeometry.angle (V - U) (W - V), not Mathlib's vertex angle ∠ U V W, which is minus it. A degenerate triple ( or ) contributes angle . Total curvature is an EReal-valued supremum over strictly increasing parameter sequences in the parameter set, and the goal uses the set . The primal and primal-dual curves are the vectors and . System (1) is the published Vanderbei central-path system with objective . The goal quantifies over every curve solving (1) for all . Existence and uniqueness of that curve is the referenced platform statement VanderbeiLP.CentralPath.central_path_exists_unique and is not posed again. Indices are the paper's, 1-based, mapped to Fin by subtracting one. Powers use integer exponents of the real number .
A trivializing formalization is ruled out explicitly: the curvature is a supremum in EReal (a real sSup of an unbounded set would be ), the turning angle is not the vertex angle, and degenerate polygons cannot add spurious right angles.
Lemmas 22–24 are stated over a model of by coefficient functions with the paper's support and absolute-convergence conditions. Equalities, products and order in are expressed through evaluation at all sufficiently large , which is how the paper characterizes them. Table 1 and the claims of the proof are stated for the explicit tropical central path of given by Propositions 20–21 (milestones of the companion mission), written as a definition here. One repair: the paper's "uniquely attained" claim fails at , , where . It is stated with that case excluded, which the proof does not use.
Welcome contributions: a general theory of total curvature of curves (monotonicity under refinement, behaviour under limits), asymptotics of evaluated Puiseux series, and the comparison between the central path over and its real specializations.
This completed entry lowers the sufficient exponent cutoff for the sharp diagonal Hlawka formula from 90 to 87. The goal is already proved in Lean on Prove2Me: for every real p ≥ 87, the foundation's cyclic constant K_p is the least constant that works for every triple of complex coordinate vectors in every finite dimension.
The statement includes arbitrary unequal-norm and zero triples, as well as dimension zero. It uses the foundation's unchanged definitions and combines admissibility with uniform optimality. This concerns complex diagonal matrices; it does not claim the corresponding result for general matrices or settle the conjecture for all p ≥ 2.
The campaign template is instantiated with value 87. Both items reference the existing accepted theorems.
The proof extends the accepted cutoff-90 Lean development by BrunoDCDO, adapting Ezzeri Esa's construction and analytic argument. The contributions at cutoffs 89, 88 and 87 were submitted by moona3k.
For p ≥ 88, the proof uses the accepted cutoff-88 result. On 87 ≤ p ≤ 88, it retains the localization, box-convexity and cyclic-averaging argument, with confinement parameter q₀ = 5351/15000, an improved cyclic witness (3/(4p))^(1/p), sharper Taylor estimates and exact rational polynomial certificates.
The foundation established cutoff 256; the supplied argument was formalized at cutoff 90. The subsequent accepted results extend the same formula to cutoffs 89, 88 and 87. This entry records the proved cutoff 87 on the campaign timeline; the campaign's cutoff-85 mission remains open.
The Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. The question is how large a comparison constant is needed to make this inequality hold.
This mission asks whether the best possible constant for complex diagonal matrices, already proved in Lean for every real , also holds for every real . This is an open problem: no proof is known. The constant is the one from the foundation mission: the largest comparison constant required by the cyclic family of three diagonal matrices. Because the accepted cutoff-87 theorem already covers every , the new work is the range from 85 to 87.
The cutoff came down from 90 to 87 in a day, through moona3k's proofs at 89, 88 and 87. The 89 proof reran the cutoff-90 argument with sharper, second-order estimates. A numerical model of that argument with retuned constants puts its limit between about 86.6 and 87.5: two of its steps pull the same parameter in opposite directions, and below that point no setting satisfies both. So reaching 85 is expected to need a new idea, not just tighter numbers. The goal theorem below gives the exact statement.
This is an entry in the sharp diagonal Hlawka campaign, which asks for the smallest cutoff at which the same formula holds. Any proof for a cutoff of 85 or lower also settles this mission.
The broader question of optimal constants for Schatten norms appears in Audenaert and Kittaneh’s Problem 7. Extending the sharp diagonal constant to general matrices is a separate challenge.
79aa498bfcf7b22bd91d771fb32ec278e2d4704b. Source libraryMaximum pressure policies schedule a stochastic processing network by choosing, at each decision time, an allocation of processors to activities that maximizes a linear "pressure" built from the current buffer levels and the network's input-output matrix. Dai and Lin (Oper. Res. 53(2), 2005) prove that such policies are throughput optimal: they stabilize the network whenever any policy can. The policies descend from the back-pressure rule of Tassiulas and Ephremides (IEEE TAC 37(12), 1992) for wireless networks and are now standard in switching, manufacturing and data-center scheduling.
The general theory lets a processor split its capacity among several activities at once. In many systems this is impossible: a machine works on one job type at a time. Section 7 of the paper shows that with this restriction Harrison's static planning LP no longer characterizes stability, and Section 8 shows that forbidding preemption can make a maximum pressure policy unstable. Both difficulties disappear for one structural class, the reversed Leontief networks, in which every activity needs exactly one processor. This mission formalizes the two lemmas that make that class work: extreme allocations are integral (Lemma 1), and a maximum pressure allocation is found processor by processor (Lemma 3).
A network has buffers , where Buffer is the outside world and are the internal buffers; activities ; and processors . The resource consumption matrix has if activity requires processor and otherwise. The constituency indicator records that activity processes buffer . An input activity processes only Buffer ; a service activity never processes Buffer . Each processor runs input activities only (an input processor) or service activities only (a service processor). Each activity has a mean processing requirement , rate , and a routing matrix .
The input-output matrix is
An allocation is with for every processor and for every input processor; is the set of allocations, its set of extreme points, and the allocations with integer coordinates. For a buffer-level vector , the network pressure is and the activity pressure is , with for the idle Activity .
The network is reversed Leontief if each activity requires exactly one processor. The possible activities of processor are for an input processor and for a service processor. Under an integer allocation , is the activity processor works on, or if is idle.
For a reversed Leontief network, and ,
A further supporting item, not a milestone, states the decomposition of an allocation along one processor (proof of Lemma 1, p. 215).
The result. Lemma 1 says that, in a reversed Leontief network, the maximum pressure policies of the processor-splitting theory are automatically non-processor-splitting, so the paper's throughput optimality theorem holds in the setting where machines cannot be shared. Lemma 3 says that the maximization over the (exponentially large) set decouples into one small maximization per processor: each processor picks an activity of largest activity pressure among its own options. This separability is what makes the nonpreemptive version of the policy well defined and is the key step towards Theorem 9 (throughput optimality of nonpreemptive maximum pressure policies). It also covers multiclass queueing networks with alternate routes (§9.1), which are reversed Leontief.
Formalizing it. Both lemmas are proved in the paper; to our knowledge neither is machine-checked. The mission produces a reusable Lean model of the allocation polytope of a processing network with input processors, its integer and extreme points, and the activity and network pressures. The integrality of is a total-unimodularity-type fact for a block structure that is not available in Mathlib in this form.
The pressure is linear, so maximizing over equals maximizing over ; the substance is the description of . The polytope is not a box: input processors carry equality constraints and service processors inequality constraints, and in general networks (an activity needing several processors) contains fractional points, as the paper's example in §7 shows. The step that fails for general networks is the decomposition of a fractional allocation along a single processor: it needs every activity of that processor to use no other processor. In Lean, extreme points must be handled through Mathlib's Set.extremePoints, and the argmax over must keep track of the idle option, which exists for service processors and not for input processors.
Indices are 0-based: internal buffers Fin I, buffers with Buffer Fin (I+1) (Buffer is 0, internal buffer is i.succ), activities Fin J, processors Fin K. The idle Activity is none : Option (Fin J), with activity pressure and unit vector . is Set.extremePoints ℝ 𝒜. "Maximizes the pressure over " is stated by domination ( for all ), never through a supremum. is defined by choice of an activity of at level ; it is used only for , where it is unique.
The standing assumptions of §2 are carried as one hypothesis: and are –, constituencies are nonempty, every activity is an input or service activity and needs a processor, processors are input-only or service-only, at least one input activity exists, and . Two disclosed additions: every input processor has at least one activity (otherwise (2) is infeasible and ), and (needed for ). The goal keeps as on the page; two milestones drop it, which strengthens them.
A trivializing formalization would make empty or give input processors an idle option; both are excluded: is the extreme-point set of the real polytope , which is nonempty for a reversed Leontief network under the standing assumptions, and the idle option belongs to only for service processors, as in (60).
Contributions welcome: proofs of the milestones, a general lemma that – points of a subset of the unit cube are extreme, and the separable description of extreme points of products of simplices, which is reusable beyond this mission.
Second-order stochastic dominance constraints let a decision maker require that a random outcome of a decision be preferred to a fixed benchmark outcome by every risk-averse expected-utility maximizer, without choosing a utility function in advance. Dentcheva and Ruszczyński introduced optimization under such constraints in Optimization with stochastic dominance constraints (SIAM J. Optim., 2003), for the case where the decision enters the outcome linearly (the pure-dominance case). Their follow-up paper, Optimality and duality theory for stochastic optimization problems with nonlinear dominance constraints (Math. Program., 2004), allows the decision to affect many random outcomes in a nonlinear, concave way, and derives optimality and duality theory in which the Lagrange multipliers of the dominance constraints are utility functions.
In applications (portfolio selection against a benchmark index is the paper's own example in §6) the probability space is a finite set of scenarios. Section 5 of the paper specialises the theory to that case. This mission formalizes that section: the reduction of the dominance constraints to finitely many inequalities, and the optimality and duality theorems (Theorems 6 and 7) in which the multipliers become piecewise-linear concave utilities.
There are scenarios with probabilities , , and benchmark constraints, indexed by ; . A decision ranges over a convex set . For each scenario , is the objective contribution and the th outcome, all concave. The benchmark has realizations . Write .
The second-order dominance of a finitely distributed (realizations ) over on an interval reads
The split-variable problem (38)–(41) is
for all , , over and . The Slater condition asks for and satisfying the dominance constraints (39) with for all .
The utility set consists of the functions that are concave, nondecreasing, piecewise linear with break points only at the , and zero on . With multipliers for the splitting constraints , the Lagrangian is
Multipliers of the inequalities (39) generate the utility (46). The dual functional is (47).
Under the Slater condition, optimal for (38)–(41) implies that there are and with
conversely, these conditions together with feasibility imply optimality.
Theorem 6 says that, for finitely many scenarios, the infinite-dimensional multiplier of the general theory (a concave utility in a cone of functions, Theorem 2 of the paper) can always be taken piecewise linear with kinks exactly at the benchmark's realizations. The multiplier space becomes finite-dimensional, is a polyhedral cone, and the dual problem of Theorem 7 is a finite-dimensional convex program. The paper's decomposition (49)–(51) of the dual functional and its numerical method in §6 rest on this. Lemma 2 is the standard reduction that makes dominance against a finitely distributed benchmark a finite set of polyhedral constraints, used throughout the later literature on dominance-constrained portfolio optimization.
The results are proved in the paper; none of them is formalized. The mission produces machine-checked statements of the finite-scenario theory, a Lean model of the utility set and of the correspondence between nonnegative multipliers and piecewise-linear utilities, and a Kuhn–Tucker theorem for concave programs with polyhedral constraints and a relative-interior Slater point.
The obvious route to Theorem 6 is to invoke a Kuhn–Tucker theorem. The available formal versions require every inequality constraint to hold strictly at the Slater point and range over all of . Neither fits: the dominance constraint at the smallest realization has right-hand side and a nonnegative left-hand side, so it can never hold strictly, and may be lower-dimensional (a simplex), so only its relative interior is available. The polyhedral structure of (39) must be used, as in Rockafellar's Theorem 28.2. The second obstacle is the converse direction of the multiplier–utility correspondence: a utility in must be written as a nonnegative combination of the kinks , which requires handling repeated realizations and the one-sided slopes at each break point.
Fin N → ℝ; , , are Fin m → Fin n → ℝ; expectations are finite sums and positive parts are max t 0. No measure theory is used.intrinsicInterior ℝ Z, not the topological interior. In the Slater condition only the splitting constraints are strict; the dominance constraints hold non-strictly.EReal supremum.ConvexOptimization.slater_strong_duality, Boyd–Vandenberghe §5.3.2) assumes a strict Slater point for every constraint and no set constraint, so it does not cover milestone 4.A processing network must decide which activities receive scarce processor capacity while jobs move among buffers. Such decisions matter in manufacturing, service systems, and switches: one activity can consume several processors at once, and a job can be routed to another buffer after processing. A policy that sees current buffer levels but does not need to know arrival or routing rates is easier to operate when those rates are difficult to estimate. Dai and Lin's 2005 paper studies whether a maximum pressure policy, which uses the buffer vector and an input-output matrix, can stabilize every network that is stabilizable in their model. Their Theorems 1 and 2 give, respectively, a necessary planning condition for any stabilizing policy and a sufficient condition for maximum pressure under the extreme-allocation-available assumption. Dai and Lin (2005)
Here pathwise stability means that each internal buffer grows sublinearly in time almost surely. This is a rate statement about sample paths. It does not assert positive recurrence of a Markov chain, nor does it require a stationary distribution. The paper allows general primitive processing and routing processes with almost-sure long-run averages. Dai and Lin (2005), §§2–4
There are internal buffers, activities, and processors. Buffer represents the outside world. The matrix records resource use: when activity requires processor . The matrix records which buffers an activity processes. An input activity processes Buffer ; a service activity does not. Input processors serve only input activities and must be fully used, while all processors have at most unit capacity.
For activity , the processing requirements have mean and the routing counts have long-run matrix . Write . The input-output matrix is
Positive means activity consumes net material from internal buffer ; negative means it produces net material there. An allocation assigns nonnegative activity levels subject to the processor capacity bounds and the equality for every input processor. The finite set consists of the extreme points of this allocation set. At buffer vector , allocation has network pressure . The maximum pressure rule chooses an allocation of greatest pressure among the currently feasible members of . Feasibility depends on jobs actually available to each constituent buffer. Dai and Lin (2005), §§2–3
The extreme-allocation-available assumption (EAA) says that for every nonnegative , a pressure maximizer in can be chosen whose constituent buffers all have positive levels. It links the static pressure maximization to the jobs that a policy can process. The static planning LP asks for activity fractions and a service-processor load such that , every input processor has load one, and every service processor has load at most . Dai and Lin (2005), p. 202
The goal is Theorem 2. For a network satisfying EAA and run by a preemptive, processor-splitting maximum pressure policy, LP feasibility with implies
The milestones follow the paper's route from stochastic paths to deterministic fluid limits. A fluid limit is a uniform-on-compact limit of along positive scales . The milestones state that fluid limits satisfy (14)–(18), weak stability of the corresponding fluid model transfers to pathwise stability (Theorem 3), maximum pressure adds (52)–(55) and (20) (Lemmas 5 and 4), quadratic fluid energy obeys (22)–(23), and LP feasibility with EAA makes the maximum-pressure fluid model weakly stable (Theorem 4). Dai and Lin (2005), pp. 203, 213–214
Theorem 2 identifies a policy whose almost-sure buffer growth rate vanishes whenever the planning LP permits load at most one and EAA holds. Together with the paper's necessary condition in Theorem 1, it characterizes the feasibility boundary for this policy class under EAA. Its scope includes networks in which an activity uses multiple processors and processes multiple buffers simultaneously. It does not claim that all such networks satisfy EAA. Dai and Lin (2005), Theorems 1–2
The result is proved in the 2005 article. This mission asks for a machine-checked proof of that known theorem and its selected intermediate claims. The Lean statements are open draft targets. Reusable outcomes include a model of cumulative routing and service counts, a uniform-on-compact fluid-limit interface, and the weak-fluid-stability transfer theorem for networks without a Markov assumption.
Maximizing pressure over the static allocation polytope does not by itself describe an executable service policy. An allocation can demand work from an empty buffer. EAA addresses the existence of a maximizing allocation supported by positive buffer levels, but the stochastic policy acts on actual jobs and completion times. The proof must connect those discrete, pathwise decisions to the limiting differential equation (20). At a regular fluid time, the maximum-pressure equation is decisive; away from regular times, derivatives need not exist. The fluid model therefore carries a time qualifier that cannot simply be dropped. Dai and Lin (2005), pp. 201–203, 214
The Lean model uses finite index types for buffers, activities, and processors. Internal buffers are Fin I; Buffer 0 is the zero index of Fin (I+1), and an internal buffer maps to its successor index. Activity and processor labels use zero-based Fin. Time is real but all network equations are asserted for nonnegative time. The shared Bell–Williams Paths definition supplies the renewal count in and uniform-on-compact distance using the norm. The completion count is required finite wherever the network equations convert it to a natural number; this prevents infinity from becoming a zero count. Bell and Williams (2001)
The network standing assumptions record binary incidence matrices, nonempty constituencies, processor coverage, activity types, and an input activity. Two refinements are explicit: each input processor has an activity, so its mandatory unit allocation is feasible, and , so is defined as the intended positive rate. Routing counts are cumulative and nonnegative. Their row sums are constrained only for buffers an activity processes: the printed sentence requiring the same sum for every buffer conflicts with its immediately preceding statement that the count vanishes when the activity does not process that buffer. The corresponding rows of sum to one for processed buffers and vanish for unprocessed buffers, as follows from (4). Dai and Lin (2005), pp. 199–200
The policy predicate records allocation-time decomposition (49)–(51) and the non-employment consequence of Definition 1 used in (56)–(58). It checks feasibility of a competing extreme allocation through the paper's threshold at every time of the interval. Individual job states and tie breaking are outside the pathwise interface. The goal retains EAA, the exact bound, and all network and policy equations, so an empty allocation set or an unconstrained service path cannot make the target automatic. Contributions formalizing the finite extreme-point set, fluid-limit compactness, Lemmas 4–5, and the weak-stability transfer are welcome.
Infinite-horizon dynamic programs, including discounted Markov decision processes, stochastic games and semi-Markov models, are usually analysed through a single equation: the optimal return solves the optimality equation , where maximizes the one-step return over decisions. Denardo's 1967 paper (SIAM Review 9(2), 165–177) separated the argument from the particular model. It isolated two properties of an abstract return , contraction and monotonicity, and showed that the standard conclusions follow from them alone. The examples of §8 of the paper cover Howard's discounted model, Shapley's stochastic games and Blackwell's, Jewell's and Fox's models.
The plain contraction assumption (each one-step operator shrinks distances by a factor ) fails in models where the process stops only from a subset of states, or where discounting acts only after several transitions. §5 of the paper handles these with the N-stage contraction assumption: only steps of a policy need to contract, while one step only needs to be nonexpansive. This mission formalizes that section. Its companion mission (part 1 of the series) formalizes the plain contraction case.
Timeline:
Let be a set of points. Each point has a decision set . A policy picks a decision at every point, so the policy space is . Let be the bounded real functions on with the metric ; is complete. Write when for every .
The return assigns a real number to each point , decision and . It defines two kinds of operators on :
and both are assumed to map into . An operator on has modulus or less when for all .
Under these assumptions is a contraction, so it has a unique fixed point , the return function of . The optimal return is . The auxiliary operator is .
Under the monotonicity and N-stage contraction assumptions:
The mission also contains two consequences that are not milestones: is optimal for the mathematical programs s.t. and s.t. (§6, p. 171), and a policy is optimal exactly when it attains at every point (§7, p. 173).
Theorem 4 lets models whose one-step operators are not contractions use the contraction-mapping theory of dynamic programming. Under its hypotheses the optimality equation has exactly one bounded solution, and that solution is the optimal return. Successive approximation converges geometrically from below (part (e)). Lemma 2 shows that is the least with and the greatest with . This gives the linear-programming formulation of finite Markov decision processes (Program I) and the policy-improvement argument of §6. The characterization reduces the search for optimal policies to the decisions that attain the maximum in the optimality equation.
The results are proved in the paper. The work of this mission is to formalize them, in the abstract form that Mathlib does not have: monotone operators on bounded functions that are contractive only after steps, with suprema taken over arbitrary, possibly infinite, decision and policy sets. No machine-checked proof of Theorem 4 or of Lemma 2 is known. The closest formal statements, Propositions 4.1–4.2 of Bertsekas and Shreve under their Assumption C, concern a different model (extended-real costs, nonstationary policies) and are themselves unproved formally.
The obvious argument would apply the Banach fixed-point theorem to . That does not work: under the N-stage assumption, need not be a contraction. The paper gives an example (p. 170) with , , where has modulus for every . The supremum over decisions does not commute with composition, so the contraction of each says nothing directly about . The paper therefore works through the auxiliary operator , which is a contraction. The hard step is to show that , the supremum of the policy returns, is a fixed point of . This is the second half of Lemma 2(a), an -argument that uses both monotonicity and the modulus- bound on .
Part (e) holds only for . It is not a contraction property of on all of .
lp (fun _ : Ω => ℝ) ⊤ (as BFun Ω), and its dist is . The order is pointwise (PLe).IsPolicyOperator, IsMaxOperator and IsNStageSupOperator. Every supremum, including (IsOptimalReturn), is a genuine least upper bound (IsLUB). sSup/⨆ are never used, so no junk value can make a statement trivial.ModulusLE B c. NStageContractionAssumption H N c holds , , ModulusLE (H δ)^[N] c and ModulusLE (H δ) 1, with and independent of .v with , the paper's §5 definition. is the conclusion (a), never a hypothesis.IsNStageSupOperator H N E. The milestone Theorem 4 (a)–(c) proves that such an operator exists. is never defined as a fixed point of or . The goal asserts that the pointwise least upper bound of exists in and is the unique fixed point of both.A complete development needs the Banach fixed-point theorem for iterates (Mathlib's ContractingWith, applied to ), suprema of families of real numbers, and induction on iterates. The §3 observation and Lemma 1 are reusable for any monotone operator family on bounded functions. Contributions to every milestone and to the two §6–§7 consequences are welcome.
A stochastic processing network (Harrison 2000) models a system in which processors carry out activities and each activity draws jobs from one or more buffers. Manufacturing lines, call centers with cross-trained agents, and data switches all fit this model. A central question is which scheduling policies are throughput optimal, meaning they stabilize the network whenever any policy can.
Dai and Lin (Oper. Res. 53(2), 2005) show that maximum pressure policies are throughput optimal. These policies generalize the back-pressure rule of Tassiulas and Ephremides (1992) for wireless and switch networks, and at each moment they choose the allocation that maximizes a linear "network pressure". Their main theorem (Theorem 2) has one structural hypothesis, the extreme-allocation-available (EAA) assumption (Assumption 1). It holds for many familiar networks and fails for some (§6.2 gives a counterexample). Theorem 6 identifies a broad class where it always holds: strict Leontief networks, in the sense of Bramson and Williams (2003). This mission formalizes that theorem.
A network has internal buffers , an outside Buffer , activities and processors .
The input-output matrix is
An allocation gives the level at which each activity runs. The allocation set consists of the allocations with for every processor and for every input processor. Write for the set of its extreme points, the extreme allocations. For a buffer-level vector the network pressure is . Buffer is a constituent buffer of if .
Assumption 1 (EAA). For every there is with such that for every constituent buffer of .
A network is strict Leontief if every service activity has exactly one buffer in its constituency, denoted .
The result. Theorem 2 of the paper states that, under EAA, a maximum pressure policy is pathwise stable whenever the static planning problem has a feasible solution with . Theorem 6 removes the EAA hypothesis for strict Leontief networks. In that class maximum pressure is therefore throughput optimal with no further structural condition. The class includes multiclass queueing networks with alternate routes and networks of input-queued data switches (§9), so Theorem 6 is the step that turns the abstract main theorem into a statement about these concrete systems.
Formalizing it. The theorem is proved in the paper and, to our knowledge, has no machine-checked proof. Formalizing it fixes the exact standing assumptions of the model, several of which the paper uses without stating (see below). It also yields a reusable Lean vocabulary for stochastic processing networks with input activities: from (5), the allocation polytope with the input-processor equality (2), extreme allocations, network pressure and EAA. The companion missions of this series on maximum pressure policies build on the same vocabulary.
The naive argument stops at "take a maximizing extreme allocation". A maximizer may run a service activity whose buffer is empty, in which case EAA fails at . Removing such activities gives , which has the right support and pressure but is in general not extreme. The pressure inequality depends on the sign pattern of , which holds only because every service activity has a single buffer. In the network of §6.2 this sign pattern fails and so does EAA. Returning from to an extreme allocation without losing the support property needs a convex-geometry argument about the polytope . In Lean this means relating Set.extremePoints of a compact polyhedron to maximizers of a linear functional and to supports.
Indexing. Internal buffers are Fin I. Buffers including Buffer 0 are Fin (I+1), with Buffer as 0 and internal buffer as i.succ. Activities and processors are 0-based.
Standing assumptions (§2), one predicate Network.Standing.
Disclosed additions to the page.
Conventions.
Set.extremePoints ℝ 𝒜.sSup. Without attainment the statement would be vacuous.Trivializing formalizations ruled out. EAA must not be weakened to a supremum over a possibly empty , and Buffer must not be counted as a constituent buffer. Either change would make the goal trivially true or impossible.
Infrastructure. Solvers need two results:
IsCompact.extremePoints_nonempty and Krein–Milman;Both are reusable beyond this mission. Contributions proving them as general Mathlib-style lemmas are welcome.
Stochastic processing networks (Harrison 2000) model manufacturing lines, data switches, call centers and multiclass queueing networks in one framework: jobs wait in buffers, activities process jobs from one or several buffers at once, each activity may need several processors simultaneously, and routing after service may depend on the activity used. A central control question is which dynamic policy keeps such a network stable whenever any policy can.
Dai and Lin (Oper. Res. 53(2), 2005) answer it with maximum pressure policies, a generalization of the back-pressure policy of Tassiulas and Ephremides (1992) for wireless networks. At each decision time the policy picks an extreme allocation maximizing a linear "network pressure" in the current buffer levels; it needs no arrival-rate information. Their main result (Theorem 2) is pathwise stability whenever Harrison's static planning LP has a feasible solution with . The proof goes through the fluid model: a deterministic, continuous analogue of the network whose stability implies stability of the stochastic system.
This mission formalizes Theorem 5 of the paper, the strong form of the fluid-level result: under a strict load condition and a mild structural assumption, every solution of the maximum pressure fluid model empties in finite time, uniformly over bounded initial states. Fluid stability in this sense (Definition 4) is the property that the standard fluid-limit machinery (Dai 1995) turns into positive Harris recurrence of the stochastic network.
The network has buffers , where Buffer is the outside world and are the internal buffers, activities and processors .
The input-output matrix is . An allocation is with for every processor and for every input processor; is the set of allocations and the set of its extreme points. The network pressure of at buffer level is .
The static planning LP asks for and with , for service processors and for input processors. Assumption 1 (extreme-allocation-available, EAA) says that for every some maximizer of over has on all its constituent buffers. Assumption 2 says there is with componentwise.
A fluid model solution is a pair of paths , buffer levels and cumulative activity times , satisfying (14)–(18): (written out over buffers), , input processors always busy, every processor's busy time at most elapsed time, and nondecreasing with . A time is regular if both paths are differentiable there. Under a maximum pressure policy the solution also satisfies (20): at each regular ,
for every solution of (14)–(18) and (20). The constant depends on the network only.
The result. Theorem 4 of the paper gives only weak stability (a fluid model started empty stays empty) under , which suffices for pathwise stability. Theorem 5 gives a uniform emptying time under , the hypothesis that standard arguments (Dai 1995; Dai and Meyn 1995) need to conclude positive Harris recurrence and moment bounds for the stochastic network. The emptying-time bound is explicit and linear in the initial fluid level.
Formalizing it. The theorem is proved in the paper; to our knowledge no machine-checked proof exists. The closest formalized result on Prove2Me is ProcessingNetworks.BackPressure.bp_maximal_stability (Dai and Harrison's book, Theorem 9.12), which uses the same Lyapunov idea in a different model: exogenous arrival rates, the planning problem , no input activities and no Buffer 0. The present mission formalizes the Dai–Lin model with input processors, where the planning LP has and the equality constraints (2). The definitions file (network, , , pressure, fluid model, (20)) is shared in content with the other missions of this series.
Each algebraic step is short; the work is in the analysis. The obvious route reads as an ordinary differential inequality and integrates it. That requires the inequality almost everywhere, but it is only available at regular points. So one needs: Lipschitz continuity of and on from (16)–(18), almost-everywhere differentiability (Rademacher), and a comparison argument for an absolutely continuous function, , whose derivative bound holds only where . The step "by (20)" also needs the maximum over to dominate every allocation in . That is the vertex property of a bounded polyhedron, which in Lean means compactness of plus a Krein–Milman type argument. The published Dini-derivative extinction criterion ProcessingNetworks.LyapunovCriteria.dini_extinction_criterion (Dai–Harrison Lemma 8.11) is a possible tool for the last step, applied to .
Fin I, buffers as Fin (I+1) with Buffer 0 the index 0 and internal buffer i the index i.succ, activities Fin J, processors Fin K.ℝ → (Fin n → ℝ) constrained only at . Derivatives are deriv, used only at regular points.IsGreatest of the set of pressures over , so the maximum is attained and an empty cannot pass through a junk supremum. is Mathlib's Set.extremePoints.Network.Standing. Two disclosed additions are needed for the objects to make sense: every input processor has an activity, and . The row sums of are not imposed.Contributions of reusable lemmas are welcome, in particular almost-everywhere differentiability of Lipschitz paths on , the vertex property of bounded polyhedra, and extinction of nonnegative absolutely continuous functions with on .
Graham (1966) showed that list scheduling finds a schedule within a factor of optimal for precedence-constrained jobs on identical parallel machines, the first performance guarantee for an approximation algorithm. When the machines run at different speeds (uniformly related machines), the same analysis breaks down, and for two decades the problem resisted a guarantee independent of the speeds better than .
Timeline:
The mission formalizes the makespan half of that paper, up to its Theorem 3.7.
An instance has jobs and machines. Job requires units of processing, and machine runs at speed , so job takes time units on machine . A strict partial order on the jobs gives precedence constraints: means that job may not start until job has completed.
A schedule runs each job without interruption on one machine , from a start time to its completion time . A machine processes at most one job at a time, and forces . Its length is . is the length of an optimal schedule.
Let be the distinct speeds and the number of machines of speed . An assignment names the speed class at which job is to run. Its loads are , and its chain bound is the largest value of over chains of . Speed-based list scheduling is Graham's rule restricted by the assignment: whenever a machine of speed is idle, it starts the first available job on the list with .
The linear program LP has variables , and . It minimizes subject to the following constraints:
From a solution, with , the assignment algorithm gives each job the speed class of largest capacity .
There is an absolute constant such that for every instance with machines and distinct speeds, the better of the two schedules below has length at most
The result gives the first guarantee for , independent of the speeds, and a guarantee depending only on the number of distinct speeds. Through the batching technique of Shmoys, Wein and Williamson it extends to release dates (Corollary 3.8). Since LP also relaxes the preemptive problem, it gives an bound on the ratio between the nonpreemptive and preemptive optima (Corollaries 3.9, 3.10). The "In fact" form, relative to an arbitrary feasible LP solution, drives the paper's algorithm in §4.
The result is proved in the literature but, as far as is known, not formalized. A formal proof requires machine-checking the following:
Later work gave a combinatorial -approximation (Chekuri and Bender, 2001) and an -approximation (Li, 2017). These are not part of this mission.
Graham's argument has two lower bounds:
With different speeds, the first bound fails: a chain may have been run on slow machines, and its length then says nothing about . Forcing every job onto a fast machine repairs chains but can leave most machines idle, so the second bound fails. The paper only guarantees that all machines of one speed are busy at each moment of an idle period. Making this pay off requires an assignment that controls chain lengths and per-class loads simultaneously. That assignment is the delicate part: Theorem 2.1 is the bookkeeping, while Lemmas 3.2 and 3.4 rely on the LP. Two of the formal steps are routine on paper but fiddly in Lean: time-interval accounting over a continuous-time schedule, and the counting of rounded speed classes.
Fin n and machines Fin m with . and . is a strict partial order, and a chain is a finite set of pairwise comparable jobs. is the maximum completion time, or with no jobs.Proofs of any milestone are welcome. Reusable beyond this mission are the following: the model of nonpreemptive schedules on uniformly related machines with precedence, the speed-based list-scheduling predicate with Theorem 2.1, and the LP.
Prove that CLIQUE is NP-complete by reducing the existing 3-SAT language, KSat.KSAT 3, to it. An instance consists of a finite simple undirected graph and an input threshold; it asks whether the graph contains a clique of at least that size.
(https://prove2.me/theorems/d82e8682-c490-4742-a5e5-dd3a0b870b90). The construction specializes Karp’s SAT-to-CLIQUE reduction to 3-SAT.
Fashion and consumer-electronics retailers sell a product at full price early in a season and mark down what is left. Consumers learn the pattern, and some of them wait for the markdown. Such strategic consumers lower the revenue of the full-price period, and the retailer's stocking decision affects how deep the markdown is expected to be. Quick response — a second, more expensive replenishment placed after demand is observed — is usually valued as a way to match supply with exogenous demand (Fisher and Raman 1996; Cachon and Terwiesch, Matching Supply with Demand, 2005). Cachon and Swinney ask how strategic waiting changes that value.
The source is the authors' working paper of April 2007, revised November 25, 2007, not the 2009 Management Science version, whose numbering and wording may differ. Its answer: with strategic consumers the retailer stocks less (Theorem 1), and under an explicit cost condition, quick response is worth more to a retailer facing strategic consumers than to one facing only myopic consumers (Theorem 3).
A retailer sells over two periods. It sells at the exogenous full price in period 1 and at a markdown price chosen at the start of period 2. Leftover units are worth . First-period demand has density and distribution function , and satisfies the monotone scaled likelihood ratio (MSLR) property: for every , is monotonic on the support of .
The market has three segments:
The standing assumptions are and . Let be the fraction of strategic values above .
By a threshold argument (Lemma 1), strategic consumers with value below some buy at and the rest wait. A fraction of demand then buys in period 1, and the inventory left for period 2 is . The period-2 revenue counts the waiting strategic consumers with value at least and, if , the bargain hunters, up to the inventory . The retailer's expected profit at unit cost is
With quick response, units ordered before the season cost and units ordered after observing cost , with . The second order covers all first-period demand and may add stock for the sale. The resulting profit is .
In the sale period, waiting strategic consumers are rationed: they effectively face the inventory , where measures their place in the queue. A strategic consumer with value who waits gains, in expectation,
where is the demand level below which the retailer clears stock at . A rational expectations equilibrium is a pair in which maximizes and is a best response of consumers who correctly expect . The superscript denotes the benchmark with only myopic consumers (): and are the optimal myopic profits without and with quick response.
Assume MSLR and no rationing, , , , and condition (6):
Let be any equilibrium without quick response, any equilibrium with it, and , the myopic optima. Then
The milestones follow the paper's path:
Corollary 1 is the percentage form, .
Theorem 3 identifies a second channel through which quick response creates value. Beyond matching supply to demand, it lets the retailer keep its initial stock low enough that a deep markdown becomes unlikely, so strategic consumers buy at full price. Under (6), all of them do. Quick response thus reduces strategic waiting without withholding availability, unlike the inventory-signalling remedies in the literature, and the theorem quantifies when this effect dominates.
The results are proved in the working paper, partly in a technical appendix. No machine-checked version of them, or of the underlying markdown game, is known. A formalization pins down several statements that the paper states loosely:
It also produces reusable components: the newsvendor with salvage and the reactive-capacity fractile under a general density, and a rational-expectations equilibrium predicate for a retailer–consumer game.
The profit is not concave: with strategic consumers it is concave–convex (Figure 4 of the paper). The newsvendor argument therefore does not give a unique optimal order, and Lemma 3's quasi-concavity rests on MSLR in a short appendix step.
Existence (Theorem 1) needs a fixed point of the map best response, but the consumer best response is a correspondence, not a function, so the printed intermediate-value argument does not apply directly. Theorem 3 needs a statement about every equilibrium with quick response, while Theorem 2's proof only exhibits one. Ruling out an equilibrium with requires comparing the derivative (4) of with the myopic derivative along the whole demand distribution.
Lean represents prices, quantities and valuations as reals, demand by a density on , and expectations as Lebesgue integrals against . The model carries the standing assumptions of §3 as fields, plus the following additions and corrections, each disclosed in the item notes:
Optimal revenues are suprema over all prices (and with quick response). "Optimal order" means a maximizer over all , never a stationary point, and the myopic benchmarks are the same functions at . Defining the optimal revenue by Lemma 2's closed form would make Lemma 2 and the first-order conditions definitional; it is not done.
The fill rate is , set to when no strategic consumer waits. With Lean's instead, would be a best response to every order and Theorem 2's last claim would be trivial.
A complete development needs:
The last two are reusable beyond this mission. Proofs of any milestone, alternative existence arguments, and sorry-free proofs of the newsvendor items are welcome. The comparison ", " of Theorem 2 and §8's numerical study are outside the scope.
In a stochastic multi-armed bandit a player repeatedly chooses one of arms and receives a random reward drawn from that arm's unknown distribution; the aim is to pull suboptimal arms as rarely as possible. Lai and Robbins (1985) and, for general models, Burnetas and Katehakis (1996) showed that any reasonable strategy must pull a suboptimal arm at least times in rounds, where is a minimal Kullback–Leibler divergence defined below. A strategy whose expected number of pulls matches this constant is asymptotically optimal.
For rewards in , classical index policies such as UCB (Auer, Cesa-Bianchi and Fischer, 2002) achieve pulls but with a constant governed by the gap of the means, not by . Cappé, Garivier, Maillard, Munos and Stoltz, Kullback–Leibler upper confidence bounds for optimal sequential allocation, Ann. Statist. 41(3), 2013 (arXiv:1210.1136v4), introduce the KL-UCB family of index policies and prove finite-time bounds whose leading term is the Lai–Robbins/Burnetas–Katehakis constant. This mission formalizes their result for empirical KL-UCB (Algorithm 3, Theorem 2), which is asymptotically optimal in the nonparametric model of finitely supported distributions on . A companion mission covers kl-UCB in one-parameter exponential families (Theorem 1).
Timeline: Lai and Robbins (1985), lower bound for parametric families; Burnetas and Katehakis (1996), lower bound and asymptotically optimal policies for general models; Honda and Takemura (2010, 2011), the DMED algorithm, asymptotically optimal for finitely supported and bounded rewards; Cappé et al. (2013), the first index policy with a non-asymptotic bound whose leading term is optimal in this model.
A bandit has arms with reward distributions in a known model : the set of probability distributions over with finite support. Write , and ; arm is suboptimal if . At each round the player picks an arm based on past observations and observes a reward drawn from . is the number of pulls of arm up to round .
Equivalently, each arm has a reward stack of i.i.d. draws from , all stacks independent, and the -th pull of arm returns . The empirical distribution of the first rewards is , and .
The minimal divergence is
the smallest Kullback–Leibler divergence from to a distribution of the model whose mean exceeds .
Empirical KL-UCB (Algorithm 3) pulls each arm once, then for pulls an arm maximizing
where is the set of probability distributions carried by and . The added point is essential: without it the index is the empirical-likelihood bound, which equals the empirical mean when every observation is .
Assume for all arms and . There is a constant depending only on and such that, for every suboptimal arm and all ,
The constants are the paper's. is the one quantity the main text does not give; it is existentially quantified, before the bandit, so it may depend on nothing but .
Theorem 2 gives a finite-time bound whose leading term, , equals the Burnetas–Katehakis lower bound for the model . Hence empirical KL-UCB is asymptotically optimal among all strategies for finitely supported rewards in , and the regret inherits the optimal constant. Since is at least the Bernoulli divergence of the means, and usually larger, the bound improves on kl-UCB and UCB for the same rewards. Proposition 1 is a non-asymptotic coverage bound for the empirical-likelihood upper confidence bound with the point added, valid for every law on , not only finitely supported ones.
The proofs of Theorem 2 and Proposition 1 are in the paper's supplemental article (Appendix B), not in the main text; no machine-checked proof of either exists. The mission produces formal statements of the theorem and of the proof skeleton (5)–(10) that the paper shares with Theorem 1, and of the two facts about that the bound needs. A formal proof would supply an explicit , which the paper defines only inside the supplement.
The skeleton (5)–(10) is elementary bookkeeping; the difficulty lies in the two sums it leaves, both of which must be shown to be with explicit constants. The second, , needs a deviation estimate for the empirical of a suboptimal arm that is precise enough to keep the leading constant : a bound that only controls the deviation of the empirical mean loses it, since depends on the whole distribution. The first, , concerns the optimal arm after a random number of pulls , which the algorithm itself determines, so fixed-sample bounds such as Proposition 1 do not apply directly. Both need regularity of as a function of a distribution in an infinite-dimensional model, where none of the closed forms of the exponential-family case is available.
Arms are Fin K, and arm of the paper is index . The bandit is the platform's stack-of-rewards model RegretBandits.Stochastic.IsStochasticBandit: (indexed from ) are independent, identically distributed within each arm, with mean . Pull counts and are the platform's pullCount and bestMean. Added to the page, and disclosed in each statement: every reward lies in pathwise (a representation of " is carried by "), every arm choice is measurable, and in the goal the strategy is non-anticipating ( is measurable with respect to the arms and rewards of rounds ). A run of Algorithm 3 is a pathwise predicate: rounds pull distinct arms, and every later round pulls a maximizer of , with ties broken by any rule. KL is Mathlib's InformationTheory.klDiv in , with the empirical distribution as first argument. is kept in and converted to a real number only in the final bounds, where it is finite and positive. Probabilities of events whose measurability is not asserted are outer probabilities. The page's in (10) is stated as the finite sum over that (8) produces. The probability space of Theorem 2 lies in Type.
Trivializing formalizations are ruled out. The index is a supremum over a set that is nonempty (it contains ) and bounded above, so it is never Lean's junk value. and range over , not over all measures. The run predicate has both the initialization and the argmax clause. is quantified before the bandit and the horizon.
Reusable beyond this mission: for , the empirical-likelihood bound of (15), and Proposition 1, a concentration inequality for empirical that applies to any bounded i.i.d. sample. Proofs of any milestone are welcome, as are proofs of the skeleton (5)–(10) that also apply to the companion kl-UCB mission.
Many design problems in control, finance and engineering are convex programs whose constraints depend on an uncertain parameter : a solution must satisfy for every in a possibly infinite set . Enforcing all constraints (robust optimization) is often intractable or overly conservative. The scenario approach draws independent samples of , solves the convex program with those constraints only, and asks how likely it is that the resulting solution violates a fresh constraint. The question matters wherever a randomized design is certified by a confidence statement, from robust control to chance-constrained portfolio selection.
Timeline.
Let be a probability space, with , and let and () be convex closed sets. The violation probability of a point is
For a multi-extraction , the program minimises over . It is assumed that every has a unique solution . A constraint is a support constraint of if its removal changes the solution. A convex has at most support constraints (Proposition 2.2). The problem is fully-supported if, for every , the program built from independent samples has exactly support constraints with -probability one.
Two further objects carry the argument. For of cardinality , is the set of multi-extractions whose support constraints have exactly the indexes in . The violation law is
the distribution of the violation of the solution built from samples.
For a fully-supported problem, every and every ,
The result. Equation (2.3) shows that the scenario bound (2.2) is tight: no bound that depends only on , and can be smaller, because a fully-supported problem attains it. The distribution of is then a Beta law, being the probability that a variable is at least , the same for every fully-supported problem. This is what fixes the sample sizes used in practice: is chosen so that the binomial tail is below a confidence level . Fact (3.2), that has distribution function whatever the problem, is a distribution-free statement of independent interest.
Formalizing it. The result is proved in the source. As far as is known it has no machine-checked proof. The goal statement is already posed on the platform, and this mission supplies the paper's proof structure as milestones. Two milestones are reusable outside the scenario approach: the uniqueness of a distribution on given the moments , and the incomplete-beta identity for binomial tails.
The obvious route would compute the law of directly, but it depends on the geometry of the constraints. The paper never computes it. It obtains the law of only implicitly, through the infinite family of identities (3.4), and recovers it by a uniqueness theorem for moment problems. Two points need care. First, full support holds only almost surely: duplicated samples, for instance, produce programs with fewer than support constraints, so every set identity holds only up to null sets. Second, the claim that removing a non-support constraint keeps the first constraints as the only support constraints uses Proposition 2.2. Two identical non-support constraints show that a constraint can become a support constraint after another is removed, unless the count is bounded by .
Goal. The goal is the already-posed platform statement ScenarioApproach.Generalization.violation_tail_eq_binomial_sum_of_fullySupported (theorem id cffaa932-832c-42ca-9e81-1848ffab7e34), referenced as it stands and not restated. Proposition 2.2 is the platform statement card_support_constraints_le_dim (f70e8aa3-…). This mission adds the PART 1 steps as milestones under ScenarioExact.PartOne.
Representation. Decisions are vectors in EuclideanSpace ℝ (Fin d). A multi-extraction is ω : Fin m → Δ, with 0-based indexes, so is and "" are the indexes . is Measure.pi (fun _ : Fin m => P). , the feasible set, solutions, support constraints and full support are the published definitions violation, feasibleSet, IsSolution, IsSupportConstraint and FullySupported. A support constraint is one whose removal admits a feasible point of strictly smaller cost, which under uniqueness is the paper's "its removal changes the solution". Full support is almost sure, not pointwise.
Hypotheses made explicit. Assumption 1 is entered as existence and uniqueness of the solution for every number of constraints and every sample, together with a family of solution maps θs k, each assumed to solve and to be measurable. Under uniqueness, θs N is the goal's solution map. The paper's "measurability ... is assumed for granted" (p. 4) is replaced by joint measurability of and measurability of the solution maps, the same two hypotheses as the goal. No set is assumed measurable. The nonempty-interior clause of Assumption 1 is unused in PART 1 and is not assumed, so the milestones compose with the goal.
Conventions. is the push-forward measure violationLaw on , with = violationLaw … (Set.Iic α). Integrals against are lower Lebesgue integrals of nonnegative integrands, as extended nonnegative reals: over for , and over for in the partition chain, since that integral comes from the event . The integration-by-parts identity is a real interval integral. Ranges are , , and .
Ruled out. A pointwise "exactly support constraints for every sample" would be unsatisfiable for many problems (repeated samples) and would trivialise the probabilistic content, so it is not used. Assuming measurability of the event or of , or the identity , as a hypothesis would assume part of the conclusion, so none of these is a hypothesis.
Infrastructure. A complete development needs: the support-constraint count (Proposition 2.2, a Helly-type argument), invariance of product measures under coordinate permutations, the change-of-variables formula for push-forward measures, the Hausdorff moment uniqueness theorem on , and the binomial–incomplete-beta identity. The last two are general results, and contributions of them are welcome independently.
MAXCUT asks for a partition of the vertices of a weighted graph into two sets that maximizes the total weight of the edges between them. It is one of Karp's original NP-hard problems, so no polynomial-time exact algorithm is expected, and the natural question is how close a polynomial-time algorithm can come to the optimum. Sampling a uniformly random partition already achieves, in expectation, half of the optimal value. For two decades this factor was essentially the best known.
Goemans and Williamson (J. ACM 42(6), 1995) replaced the combinatorial problem by a semidefinite relaxation, solvable in polynomial time by interior point methods, and rounded its solution with a random Gaussian hyperplane. They proved that the resulting cut has expected weight at least times the maximum. The technique founded the use of semidefinite programming in approximation algorithms. Khot, Kindler, Mossel and O'Donnell (SIAM J. Comput. 37(1), 2007) showed that, assuming the Unique Games Conjecture, no polynomial-time algorithm achieves a better constant. Nesterov (Optim. Methods Softw. 9, 1998) extended the rounding analysis to maximizing any positive semidefinite quadratic form over the hypercube, with the constant .
This mission formalizes the presentation of these results in §6.6 of S. Bubeck, Convex Optimization: Algorithms and Complexity (arXiv:1405.4980v2), pp. 343–347.
Let and let be a symmetric matrix with non-negative entries; is the weight between points and . The graph Laplacian is , where is the diagonal matrix with entries . For the vector encodes a partition, and MAXCUT is (6.7)
Write for the Frobenius inner product and for the symmetric positive semidefinite matrices. Since and has unit diagonal, MAXCUT is bounded above by the SDP relaxation
A solution of the relaxation is any feasible matrix attaining this maximum. The rounding draws , a centered Gaussian vector with covariance , and outputs coordinatewise.
For symmetric with non-negative entries, , any solution of the relaxation, and :
The separately stated Laplacian identity on p. 346 is also included as a theorem item: if for all , then ; for , .
For , a solution of , and :
The result. Theorem 6.11 is a polynomial-time randomized -approximation for MAXCUT: the relaxation is a semidefinite program, and sampling a Gaussian vector and taking signs is cheap. Repeated sampling turns the bound in expectation into a cut of value close to times the optimum with high probability. The same scheme of relaxation followed by randomized rounding underlies approximation algorithms for MAX-2SAT, correlation clustering and quadratic programs over the hypercube, and Nesterov's Theorem 6.13 is the version for an arbitrary positive semidefinite objective.
Formalizing it. Both theorems were proved long ago. To our knowledge neither has a machine-checked proof in Mathlib. The platform has related statements from other books, in different forms: Grothendieck's identity for a standard Gaussian and two unit vectors, and the relaxation guarantee with a Grothendieck constant. This mission states the textbook's results for a Gaussian with a possibly singular covariance matrix, which is the form the rounding uses. A complete development needs Sheppard's formula for a degenerate bivariate Gaussian, an elementary but careful real-variable inequality, and a link between Mathlib's multivariate Gaussian and Gram factorizations of . All three are reusable.
The algebra (the Laplacian identity and milestone 4) is routine. The probabilistic core is Lemma 6.12. The textbook argument reduces it to the probability that a uniformly random direction separates two unit vectors, which is "a quick picture" on paper. In Lean this requires showing that the pair has the law of for a standard Gaussian , and then computing an angular measure in the plane, including the degenerate cases , where the pair is supported on a line. A density-based argument fails there, because has no density when is singular, and singular solutions of the relaxation occur (for instance ). Inequality (6.8) is a statement about a transcendental function on a closed interval with a tight constant ( against the true minimum ), so crude estimates do not suffice near the minimizer .
Matrix (Fin n) (Fin n) ℝ, vectors Fin n → ℝ. is Matrix.PosSemidef, which includes symmetry, and is trace (Mᵀ * X).ProbabilityTheory.multivariateGaussian 0 Σ on EuclideanSpace ℝ (Fin n), defined for every positive semidefinite , singular ones included. Expectations are Bochner integrals against it, and each theorem also asserts integrability of its (bounded) integrand.Real.sign would give , which takes out of ; the two agree almost surely because .Finset.sup') over the Boolean vectors read as vectors, so it is never a junk value. "The solution" of the relaxation means any maximizer, and maximizers exist since the feasible set is compact and contains the identity.Retailers of seasonal goods (fashion, electronics, airline seats) sell a fixed stock over a finite season to customers who arrive over time, and those customers know that prices may fall. A customer who expects a markdown waits, and a seller who ignores this loses revenue. The classical revenue-management literature (Gallego and van Ryzin 1994; Talluri and van Ryzin 2004) models myopic customers who buy on arrival or leave; the literature on forward-looking (strategic) buyers, for instance Aviv and Pazgal (2008), studies particular price paths.
Board and Skrzypacz ask the mechanism-design question: among all selling schemes, which maximizes the seller's expected discounted revenue when buyers arrive over time, have private values and time their purchases strategically? Their answer, published in the Journal of Political Economy in 2016, is that the optimal mechanism has a simple structure: in every period the seller sells to the highest remaining buyer if and only if his value exceeds a cutoff that depends only on the period and the number of units left. When demand is weakly decreasing over time, the cutoffs are characterized by one-period indifference conditions, which in the continuous-time limit can be implemented by posted prices. The source used here is the authors' accepted manuscript of February 6, 2015; all page numbers refer to that manuscript.
A seller has units of a good and sells them over periods ; unsold units are worth zero after period . Payoffs are discounted by . At the start of period a random number of buyers arrives, independently across periods, with a law that may depend on . Each buyer wants one unit; his value is drawn independently from a distribution with continuous density , distribution function and support . The marginal revenue of a buyer with value is
assumed strictly increasing and continuously differentiable, with .
By the standard mechanism-design reduction (§2.1, eq. (2.5)), the seller's problem is to choose when to serve each buyer so as to maximize the expected discounted sum of the served buyers' marginal revenues. The state in period , after the period- entrants have arrived, is the number of units left and the values of the buyers present. The value and the pre-entry value satisfy the Bellman equation (4.3):
where is the set of buyers left after the highest are served and the next period's entrants. Selling one unit to today rather than none gives the difference function
and the cutoff is the smallest with . Comparing selling to today with waiting and selling at least one unit tomorrow (to the best of and the entrants) gives (p. 17). Demand is weakly decreasing in the usual stochastic order if for all and .
If is weakly decreasing in the usual stochastic order then, for every ,
and is the unique root of in for : the seller is indifferent between selling to the cutoff type today and waiting one period to sell that unit tomorrow (the one-period-look-ahead property).
For every and , the optimal rule sells to the highest buyer iff , whatever the values of the lower buyers; ; and is the unique root of .
In attack order:
After the goal, (4.7) gives the period- cutoff equation .
Theorem 1 says that the optimal allocation does not depend on how many buyers are present or what their values are, only on time and inventory. This is what makes the optimal mechanism implementable without eliciting values from buyers as they arrive. Theorem 2 turns the global dynamic program into local indifference conditions. In the continuous-time limit (§5 of the paper) these become differential equations, and the optimum is implemented by posted prices with an auction at the end of the season. Under weakly decreasing demand, therefore, the classical revenue-management practice of posting prices loses nothing against the best possible mechanism.
The paper's results are proved, in prose, with envelope-theorem and coupling arguments. They have not been machine-checked. A formal development would produce a verified backward-induction model of multi-unit dynamic allocation with random arrivals, with the structural results (monotonicity, deterministic cutoffs, monotone comparative statics in inventory and time) that recur across dynamic pricing and optimal stopping. Two printed gaps are recorded below: the positivity of , and the restriction of footnote 12 to .
The obvious argument fails at "deterministic". A priori the cutoff for the highest buyer depends on the values of the lower buyers, because selling a unit today changes which of them will be served later and when. Lemma 3(a) holds only under the induction hypothesis that all future cutoffs are already deterministic and decreasing in inventory, so Lemma 3, Theorem 1 and (A.1) form a single backward induction over periods and units, and none of them can be proved in isolation. The value function is an expectation, over a random number of i.i.d. entrants, of a maximum over sorted values, so continuity and strict monotonicity in (Lemma 3(b), and the same for ) are not available from general facts. The tempting argument for Theorem 2, that cutoffs fall over time simply because fewer buyers arrive later, is incomplete: Lemma 4 has to compare two periods with different arrival laws and different future cutoffs at once.
Periods are natural numbers with , and units are natural numbers. Values, marginal revenues and profits are real numbers. The buyers present form a finite multiset of reals, and an absent buyer is absent, never a value . The value law is the measure with density ; the density is positive and continuous on and zero outside, and is defined from and . Expectations over a cohort are lower Lebesgue integrals against of nonnegative bounded quantities, so no non-measurable or non-integrable integrand can silently become . The value function is defined by the Bellman equation (4.3), with . The sequence problem (4.1) over purchase times is not formalized; the paper says either may be used (footnote 16).
Standing assumptions and handled gaps:
The cutoff is defined from , never as the threshold of an optimal policy, and "optimal" always means maximal in (4.3) over every number of units sold. A formalization that postulates a threshold policy, replaces the random cohort by its mean, or sets absent buyers to value would trivialize or change the statements and is ruled out. The mechanism-design reduction (IC/IR to (2.5)) and the continuous-time results of §5 are out of scope.
The usual stochastic order is the published platform definition StochasticOrders.Usual.UsualOrder. A complete development needs finite-horizon dynamic programming over multisets, expectations of functions of sorted i.i.d. samples, envelope arguments, and monotone coupling for the usual stochastic order on ; these parts are reusable beyond this mission. Proofs of any milestone are welcome, as is a proof that (4.3) agrees with the sequence problem (4.1).
Many optimization problems in machine learning minimize an average of losses, one loss for each observation. A full gradient step examines every observation, while a stochastic gradient step examines one. The latter is cheaper per step, but its sampled gradient can remain noisy even near the optimum. Section 6.3 of Bubeck's monograph studies stochastic variance reduced gradient descent (SVRG), which periodically computes a full gradient at an anchor point and uses it to correct subsequent sampled gradients. The question for this mission is whether that correction gives a geometric reduction of the expected objective gap at the constants printed in Theorem 6.5.
Bubeck places this method alongside full gradient descent and stochastic gradient descent for finite sums. The section records that earlier stochastic average gradient and dual coordinate ascent methods attain a gradient-computation cost of order for the same regime, where is the number of components and is a condition number. The target here is the precise SVRG convergence statement in the book, rather than a comparison of implementation costs. The source's discussion on pp. 334–336 gives the context and the algorithm.
Let be differentiable convex functions, with , and define the finite-sum objective and its gradient by
Each component is -smooth when its gradient is -Lipschitz in the Euclidean norm: for all . The average is -strongly convex, meaning that for all it lies at least above its first-order affine approximation at . The constants and are positive, minimizes over , and .
An epoch begins at an anchor . Its first inner iterate is . For , draw uniformly from , independently across steps and epochs, and update
The next anchor is the average . In particular, this average uses through , while the last updated point is excluded. Starting from an arbitrary and repeating the epoch produces . The expectation of is over all sampled indices in the first epochs.
Theorem 6.5 sets and and asserts, for every ,
The epoch length is a count, so the statement takes and explicitly requires . The goal uses exactly the book's step size, epoch length, and contraction factor.
Lemma 6.4 bounds by . Equation (6.3) bounds the second moment of the corrected sampled direction by the objective gaps at the current point and the anchor. Equation (6.2), the unbiased-direction display, and the one-step display express how that direction changes squared distance to . The later display on p. 338 bounds one epoch for any positive step size with . Finally, equation (6.1) substitutes the stated constants to obtain the factor for one epoch. These seven source claims form the milestone list in reading order.
The theorem gives an explicit accuracy guarantee after a specified number of epochs: an initial gap falls below in expectation. Because each epoch uses a full gradient at its anchor as well as sampled component gradients, the result makes clear which quantity contracts and which operations are counted. It is a concrete linear-rate statement for a method whose individual stochastic gradients need not approach zero at the optimum. Bubeck, §6.3 discusses this issue when introducing the correction term.
The mathematical result is already proved in the monograph. The remaining task is to produce machine-checked proofs of its precise finite-sum model, the single-index estimates, the epoch inequality, and the full repeated-epoch guarantee. The mission drafts those statements and definitions; no proof is claimed for the open theorem items. The finite uniform-average representation and the separation between a conditional one-step average and the full multi-epoch average can be reused in other finite-sum stochastic algorithms.
The sampled component gradient need not be small when is near , so a bound using only its norm does not yield the desired fixed-step contraction. The correction has mean zero relative to the full gradient at the current iterate, but its second moment still depends on both and . The proof must control those two gaps while respecting the fact that depends on earlier samples. A single-index estimate with held fixed and an expectation over complete sample histories are different statements; confusing them would make the goal weaker or false.
The carrier is EuclideanSpace ℝ (Fin n) with its usual inner product and norm. The Fin m components and every sample array are finite. A real-valued uniform average is an ordinary finite sum divided by the number of arrays, and and prevent an empty average. Independent uniform sampling is represented by averaging over every function from step positions to component indices. The multi-epoch sample space has one such block for every epoch. There are no integrals or measurability side conditions.
The component assumptions include differentiability with an explicit gradient map, convexity on all of , and the book's gradient-Lipschitz version of smoothness. Strong convexity is imposed on the average objective alone, using the published OnlineConvexOpt.ConvexBasics.StronglyConvexOn definition on the whole space. The book's standing notation assumes a minimizing exists; this is explicit. Positivity of and , and integrality of , make the displayed divisions and epoch length meaningful. The general epoch bound also requires and . Dimension zero is allowed: the theorem remains a statement about the unique point of and its zero objective gap.
The direction always contains the sampled difference and the full anchor gradient . Replacing that direction with would define gradient descent and would not satisfy this mission's algorithm. Contributions are welcome for the finite averaging identities, the component-gradient estimate, the conditional one-step calculation, the epoch inequality, and the induction across epochs.
Many optimization problems in statistics and machine learning ask to minimize an expected loss , or an average over a large data set. Exact gradients of such an are unavailable or too expensive, but unbiased random estimates are cheap: the gradient of the loss at one sample, or of one randomly chosen summand. The observation that first-order methods still make progress when the gradients are only correct on average goes back to Robbins and Monro (1951) and underlies stochastic gradient descent.
Chapter 6 of S. Bubeck, Convex Optimization: Algorithms and Complexity (2015), studies this setting through stochastic mirror descent (S-MD). Its Section 6.1 shows that in the non-smooth case a noisy oracle costs nothing in rate. Section 6.2 asks what smoothness buys: for a general stochastic oracle it cannot buy acceleration, but Theorem 6.3, whose proof the book takes from Dekel, Gilad-Bachrach, Shamir and Xiao (2012), shows that the rate splits into a noise term of order and a smoothness term of order . The book uses it to justify mini-batch SGD. This mission is the fourteenth of a series that formalizes the section capstones of the book.
Let be a finite-dimensional real vector space with an arbitrary norm . Gradients are linear forms on , the value of at is written , and the dual norm is . Let be compact and convex.
A mirror map is a function on an open convex set with and . It is strictly convex and differentiable on , its gradient takes every value, and as approaches the boundary of . Its Bregman divergence is . The map is 1-strongly convex on if there. A function is -smooth on if for .
A stochastic oracle returns, at a query point , a random linear form . When the query point is itself random, the book requires the conditional expectation given the query point, , to be a subgradient of at . In the smooth case it requires together with the variance bound .
S-MD with step starts at and, writing , iterates
Let , and let minimize on .
Let be convex and -smooth, and let the oracle have variance at most . Then for every , S-MD with step and satisfies
For points and , the smoothness step is
If is the S-MD step, the mirror step is
Combining the two gives a pathwise bound on with the cross term . Taking expectations gives the expected one-step bound
For a convex with , S-MD with satisfies
This rests on the deterministic regret bound (4.10) of mirror descent along arbitrary vectors :
Theorem 6.3 says exactly how much smoothness helps under noise. As it recovers the rate of deterministic smooth optimization. For large the noise term dominates; the book notes, citing Tsybakov (2003), that smoothness brings no acceleration for a general stochastic oracle. Averaging independent oracle answers divides the variance by , so the theorem quantifies the benefit of mini-batches: the noise term shrinks by while the smoothness term is unchanged. Theorem 6.1 is the matching non-smooth statement and the template for stochastic subgradient methods in any norm.
These are classical, proved results. None of them is known to be formalized in Lean, and the platform has no stochastic mirror descent statement. Its stochastic gradient items cover the Euclidean strongly convex case and the non-convex gradient-norm case. This mission adds a reusable stochastic-oracle layer in an arbitrary norm, with conditional expectations given random query points, on top of the mirror-map layer of Chapter 4.
The deterministic steps are short manipulations of Bregman divergences. The difficulty is in the passage to expectations. The query point is random, so unbiasedness enters only through the conditional expectation given . Making the cross term vanish requires pulling the -measurable vector out of a conditional expectation of a dual-valued random variable. Every expectation also has to exist. When blows up at the boundary of , the Bregman terms are not bounded a priori, and their integrability has to be derived from the recursion. A further obstacle is that the minimizer may lie on the boundary of , where is not part of the book's data. Treating informally, or assuming , skips exactly these points.
Φ' f' : E → (E →L[ℝ] ℝ), is g v, and is the operator norm. -smoothness is stated with derivatives relative to . is a total function, constrained only by the mirror-map axioms on .A variance hypothesis stated only at deterministic points would not control the random iterates, and is not used. Run predicates that let be an arbitrary point of would make the theorems false, and are not used either.
A complete development needs: first-order optimality over a convex set, the three-point identity of Bregman divergences, the descent lemma in an arbitrary norm, and continuity of the gradient of a differentiable convex function. On the probability side it needs pull-out and conditional Jensen properties for dual-valued conditional expectations. The probability layer is reusable for every stochastic first-order method in the book, including SVRG and random coordinate descent. Proofs of the milestones are welcome, and so are general lemmas about conditional expectations of continuous-linear-map-valued random variables.
Newton's method is the basic second-order method of continuous optimization: at the current point it replaces the objective by its second-order Taylor model and jumps to the stationary point of that model. Its defining property is speed near a nondegenerate minimum, where the error is squared at every step, so that the number of correct digits roughly doubles per iteration. This local behaviour is what makes Newton's method the inner engine of interior point methods, the polynomial-time algorithms for linear, conic and general convex programming (Nesterov and Nemirovski, 1994). In S. Bubeck's monograph Convex Optimization: Algorithms and Complexity (Foundations and Trends in Machine Learning, 2015; arXiv:1405.4980v2), §5.3.2 recalls the traditional local analysis of Newton's method, Theorem 5.3, before turning to the affine-invariant self-concordance analysis used for interior point methods. This mission formalizes that theorem and the four steps of its proof.
Let carry the Euclidean norm , and write for the operator norm of a linear map , so that . Let be a function, with gradient and Hessian , a linear map (the derivative of the gradient map). For a real number , means for all .
The Hessian is -Lipschitz if for all .
Newton's method starts at and iterates, for ,
A point is a local minimum of if for all in a neighbourhood of ; it has strictly positive Hessian if for some .
Assume the Hessian of is -Lipschitz, , and is a local minimum with , . If , then Newton's method from is well defined (every Hessian along the iterates is invertible, so the sequence exists and is unique) and
The theorem gives a quantitative basin of quadratic convergence: an explicit radius , depending only on the curvature at the minimum and the Lipschitz constant of the Hessian, inside which Newton's method needs only iterations to reach accuracy . It is the classical statement whose shortcomings (dependence on a choice of norm, constants that change under linear changes of variables) motivate the self-concordance theory of the following subsections, and it is the local convergence result invoked whenever a damped or globalized Newton scheme is shown to enter its quadratic phase.
On the formal side, Mathlib has the calculus this needs (Fréchet derivatives, interval integrals of vector-valued maps, operator norms) but no convergence theorem for multivariate Newton's method for minimization. A formal proof produces reusable pieces: the integral form of the mean value theorem for gradients, the stability of a positive-definite lower bound under Lipschitz perturbations, and an inverse-operator norm bound from a quadratic-form lower bound. The result itself is classical and fully proved in the literature; what is open here is its machine-checked proof in this form.
The individual inequalities are short, but the argument is an induction in which well-definedness and the rate are proved together: the Hessian at is invertible only because is still in the ball of radius , and stays in that ball only because of the rate. A proof that first assumes the sequence exists and then bounds it is circular. The proof also passes between two kinds of control on the Hessian, a lower bound on its quadratic form and an operator-norm bound on its inverse, and the second is only meaningful once invertibility is established. Finally, the integral manipulations need integrability of the maps , which comes from the continuity of the Hessian.
is EuclideanSpace ℝ (Fin n). The gradient and Hessian are explicit maps and with ContDiff ℝ 2 f, HasGradientAt f (g x) x and HasFDerivAt g (H x) x at every point; the norm on is Mathlib's operator norm, as on the page. is the quadratic-form inequality. A Newton run is a sequence indexed from satisfying the linear system ; no inverse of a possibly singular operator appears in any hypothesis, and "well defined" is a conclusion: a unique run exists from and every Hessian along it is bijective. The rate and are asserted for every run. The error representation is stated with both sides multiplied by , which is equivalent to the printed form once the Hessian is invertible. Milestones 3 and 4 use only the Lipschitz property and are stated for any Lipschitz map .
Added hypothesis: (the radius divides by ; with , Lean's convention would collapse the hypothesis to ). Convexity of is not assumed, as on the page; is a local minimum and is derived, not assumed. Encoding the Newton step with Lean's inverse (which returns on singular maps), or replacing by mere invertibility, would change the theorem and is ruled out.
A complete development needs the fundamental theorem of calculus for vector-valued maps along segments, Hessian-based quadratic-form estimates, and operator-norm bounds for inverses; all are reusable for the analysis of damped Newton, cubic regularization and interior point methods. Proofs of the milestones independently of the goal are welcome.