Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Quasi-Newton methods such as BFGS were designed for smooth objectives, yet in practice they are routinely run on nonsmooth functions and they often work well there: on many nonsmooth problems the iterates converge to a minimizer at a linear rate, measured against the total number of function evaluations. Lewis and Overton (Math. Program. 141 (2013) 135–163) set out to explain this behaviour. Almost nothing about it is proved, so they analyse the simplest cases in detail.
The very simplest case is the subject of this mission: minimizing the absolute value on the real line. In dimension one the quasi-Newton update is completely determined by the secant equation, so the method is the classical secant method, combined with a bisection-type Armijo–Wolfe line search. Even here the behaviour is far from obvious. Steepest descent on needs about function trials to reach accuracy , because the closer the iterate is to zero, the more bisections its fixed-size step needs. The secant method needs only about , the cost of bisection. Lewis and Overton show that the iterates of the secant method trace out an expansion of the starting point as an alternating sum of powers of two, which accounts exactly for the number of trials.
The objective is on , with gradient at every .
The line search (Algorithm 4.6, p. 147). Given two tests on steps , an Armijo test and a Wolfe test , the line search starts with , and . Each trial examines the current . If fails, it sets . Otherwise, if fails, it sets . Otherwise it stops and returns . The next trial step is when and otherwise. So the line search doubles until the step is bracketed, then bisects.
The tests of §5.1. At an iterate with direction (where ), take the line search objective , the Armijo parameter , and replace the differentiability check by a termination rule. The conditions become
The secant method. Start at with . At step set , let be the step returned by the line search, and put . If the method terminates at the minimizer. Otherwise is the solution of the secant equation with . The -th line search takes trials. The trial points of all line searches, listed in order, give the function trial values .
Alternating binary expansions. For , an alternating binary expansion is a length and integers (with terms when ) such that
It is canonical if either or its last gap satisfies .
Rates (p. 141). A sequence is Q-linear with rate if . A sequence is R-linear with rate if for all , for some converging to Q-linearly with rate .
Let have the canonical expansion . Then the secant method from with satisfies
If , the method terminates at zero after finitely many trials. If , the function trial values converge to R-linearly with rate . All four conclusions are exact: the iterates are equal to the tails of the expansion, and the trial counts are equalities.
The theorem gives a complete description of a quasi-Newton method on a nonsmooth function, in the one setting where the description is exact. It identifies each iterate, counts every function evaluation, and decides termination. Two things follow. After trials the error is below , so accuracy costs about trials, compared with the quadratic count for steepest descent. The analysis also shows that choosing the Armijo parameter is harmless for , which the paper contrasts with the tilted function . The R-linear rate of all trial values is the one-dimensional instance of the rates the paper observes numerically for BFGS on the Euclidean norm in higher dimensions (§5.2). Those rates remain unexplained.
The result is proved on paper: in Lewis–Overton, with the detailed analysis attributed to the companion report [31]. To our knowledge none of it has been formalized. This mission produces a machine-checked account of an algorithm as executed: a bisection line search counted trial by trial, a secant update, and the number-theoretic fact that this process computes an alternating binary expansion. It also states and fixes the two places where the printed text is inaccurate (see Formalization scope).
The first line search is easy to analyse directly: with it returns the unique power of two in . The difficulty starts with the second. The step returned by Algorithm 4.6 depends on the whole bisection history, and the new direction depends on the previous step through the secant update. The statement therefore has to be proved by an induction that carries an exact invariant. That invariant ties , and the line-search bracket to the tail of the expansion, and the trial count to the gap .
A natural first attempt is to describe each line search as "returns the power of two in the Armijo–Wolfe interval". That does not determine the trial count: the count depends on where the bisection starts and in which order it halves, and it uses the specific directions . The R-linear statement adds a further layer. Trial values inside one line search are not monotone, so the dominating Q-linear sequence has to be built over the global trial index, across line searches of different lengths.
The uniqueness half is elementary but needs care. Without canonicity it is false, and a finite expansion has to be told apart from an infinite one.
WithTop ℝ. A trial count is the index of the first trial passing both tests, plus one. Every statement about trial counts also asserts that the line search terminates, so the junk value of an empty stopping set cannot be used. The step is not defined as a closed form: that is what the theorem proves.ℕ∞, the exponents are a : ℕ → ℤ (negative when ), and the powers are integer powers. The series is a HasSum whose terms beyond vanish. Indices start at , as printed.The development needs only Mathlib's real analysis, tsum/HasSum and filters. The expansion definitions and the R-linear predicate can be reused for other rate statements. Contributions are welcome on the line-search invariant, the trial-count lemmas, and the existence and uniqueness of the canonical expansion.
Random coordinate descent minimizes a smooth convex function by updating one coordinate at a time, chosen at random. Each iteration needs a single partial derivative instead of the full gradient, which is what makes the method usable on problems whose dimension is in the millions or billions ("huge-scale" problems). Nesterov's paper Efficiency of coordinate descent methods on huge-scale optimization problems (CORE Discussion Paper 2010/2; journal version SIAM J. Optim. 22 (2012) 341–362, doi:10.1137/100802001) gave the first global efficiency estimates for such methods and started a large literature on randomized block and coordinate methods.
The basic method RCDM of the paper takes, along coordinate , a step of length , where is a Lipschitz constant of the -th partial derivative along the -th coordinate. For simple functions these constants are known; for more complicated ones they are not, and a practical method has to estimate them on the fly. Section 6.1 of the paper analyses a backtracking strategy with restore for this purpose and proves that it keeps the efficiency of RCDM up to a constant factor. This mission formalizes that analysis, Theorem 7 of the paper.
Write and for the -th standard basis vector of , . The function is convex and differentiable, attains its minimum , and its partial derivatives are coordinate-wise Lipschitz with constants ((2.2) with one-dimensional blocks):
The weighted norm and its dual are and ((2.7) with ), and
measures the size of the initial level set, being the set of minimizers.
The random adaptive coordinate descent method RACDM (6.1) keeps estimates , initialised with given lower bounds . At iteration it
The loop test uses only the sign of one partial derivative and never a function value. With (the expectation over ) and the number of partial derivatives computed in iterations , Theorem 7 states three facts about this method.
This is the rate of RCDM, ((2.14)), with a larger constant.
The result shows that the constants in RCDM need not be known: a method that starts from any lower bounds and adjusts them by doubling and halving converges at the same rate, and pays on average about two partial derivatives per iteration plus a logarithmic one-time overhead. This is what makes random coordinate descent applicable to functions whose coordinate smoothness is not available in closed form, and the doubling-with-restore pattern recurs in later adaptive and accelerated coordinate methods (the paper itself indicates the same technique for its accelerated method, (6.5)).
The theorem is proved in the paper; to our knowledge no machine-checked proof exists. The known-constant analogues for scalar coordinates are on Prove2Me in Bubeck's §6.4 development (the one-step and expected decreases are proved there; the rate is open). This mission adds a formal model of the adaptive method itself, including its doubling loop as a first-failure search, and the three statements of Theorem 7 on top of the published coordinate-descent definitions.
The analysis of RCDM rests on the one-step bound , which follows from the smoothness of along the coordinate line. For RACDM the step uses an estimate that may be smaller than , and then the same argument gives no decrease at all: a step that is too long can increase . The method never checks function values, so the decrease has to be extracted from the sign test alone, and it holds only because is convex along the line, not merely smooth. A second point is that the estimates are random and depend on the whole history, so the expected decrease must hold for every state the method can reach; this is what item 1 secures. The counting statement needs the exact number of loop iterations, so the loop has to be modelled as the least number of doublings after which the test fails, not as some number of doublings.
The formalization works with scalar coordinates (, as the paper does in §6.1) on EuclideanSpace ℝ (Fin n), coordinates indexed . It reuses the published definition ConvexOptAlg_CoordDescent_Defs: IsCoordSmooth f g L is (2.2) with an explicit gradient map , wnorm L 1 and wnormDual L 1 are and , and rcdExpect L 0 k is the expectation over uniform draws as a finite weighted sum. The mission's own definition NesterovRCD.Adaptive.RACDM encodes the trial point, the number of doublings (a minimum over ), one iteration, the run along an explicit sequence of draws, and the count .
The following choices are made explicitly.
A trivializing encoding is ruled out: the loop count is the least at which the sign test fails (an arbitrary admissible would change the method and make the count meaningless), the draws are uniform, and the rate is stated in the norm of the true constants , not of the estimates. Contributions welcome: proofs of the milestones, a one-dimensional co-coercivity lemma for convex smooth functions of one variable (reusable well beyond this mission), and the recursion argument from the expected decrease to the rate.
Plünnecke–Ruzsa inequalities bound the size of iterated sumsets: if and are finite subsets of an abelian group with , then for every , where . They are a basic tool of additive combinatorics, used in Freiman-type structure theorems, sum–product estimates and the study of approximate groups. Plünnecke's original proof went through a graph-theoretic argument; Ruzsa simplified and extended it.
G. Petridis, New proofs of Plünnecke-type estimates for product sets in groups (arXiv:1101.3507v3, 2011; Combinatorica 32, 2012, doi:10.1007/s00493-012-2818-5), gave a short, purely combinatorial proof. Its core (Proposition 2.1, p. 5) is that a subset minimising satisfies for every finite , in any group.
In a non-abelian group the hypothesis alone does not control or . Tao (Product set estimates for non-commutative groups, Combinatorica 28, 2008) showed that an extra condition on triple products restores polynomial bounds, without explicit exponents. Petridis' §4 makes Tao's bound explicit for a single set; this mission is §5 of the paper, which treats two sets and of comparable size.
Timeline:
Let be a group, written multiplicatively and not necessarily commutative. For finite subsets write
for the number of elements, ( factors), and for . The order of factors matters: multiplies on the left of .
The three hypotheses of the mission are, for finite and real numbers :
A minimal-growth subset of (with respect to ) is a nonempty with for every nonempty . In Lean this is written cross-multiplied: .
If is nonempty and (1)–(3) hold, there is a nonempty such that for every integer
The same serves every .
Theorem 1.7 extends the Plünnecke–Ruzsa inequality to non-abelian groups with explicit exponents, under hypotheses that are checkable on and alone. Bounds of this kind feed into the theory of approximate groups, where polynomial dependence on the doubling constants is what keeps later structure theorems quantitative. The witness is a large-enough piece of on which all powers of grow at a controlled rate, which is the form in which such bounds are used.
The result is proved in the paper. Mathlib formalizes Petridis' Proposition 2.1 (Finset.pluennecke_petridis_inequality_mul, in any group) and the abelian Plünnecke–Ruzsa inequalities (Finset.pluennecke_ruzsa_inequality_*, for commutative groups), but not the non-abelian estimates of §5. This mission adds them: the corollary on , the comparable-size bound for , and the full Theorem 1.7. Companion missions of this series formalize the abelian Theorem 3.1 and the explicit form of Tao's theorem (Theorem 1.6).
The abelian argument iterates with , which needs , i.e. commutativity. In a non-abelian group and powers of cannot be reordered, so the bound on does not iterate directly. A second obstacle is that the hypotheses control products of and , while the induction needs control of sets such as and , built from inverses; the hypotheses say nothing directly about such sets, and every passage between them and products of and costs further powers of and , which is why the exponents grow like and rather than . The abelian bound should not be expected to transfer unchanged.
All statements use Mathlib's pointwise Finset algebra under open scoped Pointwise, in {G : Type*} [Group G] [DecidableEq G] — never CommGroup. is X * Y, is A * {b} * B, is S * B ^ h with B ^ 0 = {1}, is X⁻¹. Cardinalities are cast to ℝ; are arbitrary reals, with no sign hypotheses beyond what the page states. Exponents are natural numbers, exact under 1 < h (goal) and 2 ≤ h (inductive step).
Conventions committed to:
Proof tools available in Mathlib: Ruzsa's covering lemma (Lemma 4.1 of the paper, Finset.ruzsa_covering_mul), Ruzsa's triangle inequality (Lemma 4.2, Finset.ruzsa_triangle_inequality_mul_mulInv_mul and siblings, with Finset.card_inv), Proposition 2.1 (Finset.pluennecke_petridis_inequality_mul), and Finset.card_singleton_mul. No new definitions are needed. Proofs of any milestone are welcome; the inequalities (15)–(17) of p. 13 are natural auxiliary lemmas for the inductive step.
Dynamic programming rests on time consistency: a control that is optimal when viewed from time stays optimal when viewed from any later time. Many problems of mathematical finance lack this property. The continuous-time mean–variance portfolio problem (Zhou–Li 2000) contains a variance, that is, a nonlinear function of an expectation, and state-dependent risk aversion (Björk–Murgoci–Zhou) lets the criterion itself depend on the current state. For such problems an optimal control computed today is abandoned tomorrow, and the HJB equation is not available.
One response, going back to the game-theoretic view of non-commitment (Ekeland–Lazrak, arXiv:math/0604264; Björk–Murgoci, SSRN 1694759), is to replace optimality by equilibrium: a control that no "future self" can improve by deviating on an infinitesimally short interval. Those works consider feedback (Markov) controls. Hu, Jin and Zhou (arXiv:1111.0818v1) define equilibrium within open-loop controls for a general stochastic linear–quadratic (LQ) problem with random coefficients, and characterize it by a flow of forward–backward SDEs, in the spirit of the stochastic maximum principle (Peng 1990). This mission formalizes that characterization: §2 and §3 of the paper, up to Theorem 3.2. The other two missions of the series build on it. Mission II treats a scalar state with deterministic coefficients (Theorem 4.4), and Mission III treats mean–variance portfolio selection (Theorem 5.4).
Let be a standard -dimensional Brownian motion on with its filtration , and let . A control is a process , that is, progressively measurable with . Its state solves the linear SDE
Here is a bounded deterministic matrix function. (), () and () are essentially bounded progressive processes, and . At time , with state and , the cost is
are bounded symmetric processes with , and are symmetric with . The last two terms make the problem time-inconsistent. Given with state , the spike variation at is for . The control is an equilibrium (Definition 2.1) if for every and every such , almost surely
For each , the first adjoint process solves on the BSDE (3.1) with driver and terminal value . The second adjoint process solves the matrix BSDE (3.2) with terminal value . With these, define
Suppose , its state , and for every a solution of (3.1) are given, and suppose satisfies condition (3.4):
Then is an equilibrium control.
Theorem 3.2 is the paper's general tool. Its two explicit results are applications of it. With a scalar state and deterministic coefficients, a pair of coupled Riccati-type equations gives a linear feedback equilibrium (Theorem 4.4). In mean–variance portfolio selection with state-dependent risk aversion and a possibly random risk premium, the equilibrium strategy is found through a quadratic BSDE (Theorem 5.4). Each is proved by exhibiting a solution of the flow (3.6) and checking (3.4). The theorem therefore separates the existence question (solving a flow of FBSDEs) from the equilibrium question. The paper notes that the general existence question remains open.
The results are proved in the paper and have no machine-checked proof. The mission produces a precise statement of open-loop equilibrium for a stochastic LQ problem with random coefficients, together with Lean statements of the spike expansion and of the adjoint flows. Mission II and Mission III restate the same model, and their final steps apply this theorem. Formal proofs of the milestones exercise Itô calculus for linear SDEs and BSDEs with bounded coefficients: product rules, conditional estimates, and uniqueness and sign properties of linear BSDEs. This is infrastructure that Mathlib does not yet have.
The obvious argument is a first-order expansion of in . It fails because the spike changes the control by , which is not small, on a set of small measure. The state's deviation is then of order in , its square contributes at order , and a second-order term appears that a first-order adjoint cannot capture. Two features are absent from the classical maximum principle. The adjoint equations form a whole flow indexed by , because the terminal value of (3.1) contains and . And every statement is conditional on , so the expansion has to hold almost surely at the level of conditional expectations. That rules out arguments based on unconditional expectations.
Brownian motion, , Itô integrals and SDE solutions come from the published definition Peng1990_SMP_Stochastic. The formalization commits to the following conventions.
The conclusion of the goal is Definition 2.1 itself. It mentions neither nor the adjoint processes, so the goal cannot be closed by unfolding. A definition of equilibrium in terms of (3.4) or (3.5) would make Theorem 3.2 trivially true and is ruled out. Condition (3.5) of p. 6 is not a hypothesis of any statement. A degenerate, noise-free example checks that the hypotheses of the goal can hold together.
Contributions are welcome as follows. Proofs of the three milestones are reusable for Missions II and III and for any spike-variation argument. So are general lemmas on linear SDEs and BSDEs over Peng's Itô integral: uniqueness, conditional moment bounds, the Itô product rule, and positivity of linear matrix BSDEs.
A differential variational inequality (DVI) couples an ordinary differential equation with a finite-dimensional variational inequality whose solution acts as an algebraic input to the dynamics. The class contains linear complementarity systems, mechanical systems with unilateral contact and friction, dynamic Nash games and many hybrid engineering models. Pang and Stewart's paper (Math. Program. 113 (2008); author's version hal-01366027v1) set up a unified theory of such systems: existence of solutions, uniqueness, and convergence of numerical time-stepping schemes.
The numerical question is the practical one. A DVI is solved by discretizing time and solving one finite-dimensional variational inequality per step. Whether the discrete trajectories approximate a true solution as the step size shrinks is not automatic: the algebraic variable can switch discontinuously, so the discrete 's need not converge pointwise. Section 7 of the paper answers this for a semi-implicit Euler scheme applied to the initial-value problem, and the answer is also an existence proof for the DVI.
Fix and write . Let be a nonempty closed convex set, let , , and . For , is the set of with for all . The initial-value DVI (6.2) is
The standing assumptions are (A): , and are Lipschitz continuous on (for the metric ), and (B): .
A weak solution is a pair with , integrable on with for almost every , the integral equation for , and the integral form of the VI,
The time-stepping scheme (7.2) uses a step , grid points , a parameter , and :
for . The iterates are turned into functions of time: is the continuous piecewise linear interpolant of the , and is the piecewise constant interpolant equal to on .
Suppose the iterates satisfy the uniform bounds (7.5),
for all small . Then along some ,
If moreover (a) with Lipschitz and (7.6), or (b) with positive semidefinite, then every such limit pair is a weak solution of (6.2).
The proof decomposes into the paper's own steps: Lemma 7.1 (the implicit Euler step is uniquely solvable, with the bounds (7.4)); the uniform step bound , which makes equicontinuous; the fact that a weak limit of -valued functions is -valued almost everywhere; the integral VI (7.7) under (a); the integral equation (7.8); and the weak lower semicontinuity (7.9) of for positive semidefinite , which handles (b).
Lemma 7.2 (a discrete Gronwall bound giving (7.5) from one-step growth conditions), Lemma 7.3 ((7.5) from linear growth of the VI solutions) and Proposition 7.1 (existence of the iterates for small ) are included as further targets: together with Theorem 7.1 they reduce the hypotheses on the iterates to conditions on .
Theorem 7.1 is simultaneously a convergence theorem for a practical numerical method and an existence theorem: any scheme with bounded iterates produces, in the limit, a weak solution of the DVI. Combined with Proposition 7.1 and Lemma 7.3 it yields existence for DVIs whose VI part has linearly growing solution sets, including linear complementarity systems with positive semidefinite , without the upper-semicontinuity machinery of differential inclusions. Case (b) covers monotone linear complementarity systems, the class arising in passive electrical networks and frictionless contact.
The results are proved in the paper. None of them is machine-checked. A formalization would produce a reusable Lean account of Euler polygons, equicontinuity estimates for discrete schemes, and weak limits of constrained sequences, all of which recur in the numerical analysis of nonsmooth dynamical systems.
The obvious argument would pass to the limit in each step of the scheme pointwise. This fails because has no pointwise or strong limit in general: only weak compactness is available. The nonlinear term does not commute with weak limits, so the variational inequality cannot be passed to the limit directly. Each of the two cases supplies the missing compactness or convexity: in (a) the bound (7.6) makes converge uniformly, and in (b) positive semidefiniteness makes the quadratic term weakly lower semicontinuous. Membership also does not follow from pointwise reasoning and needs convexity of .
Vectors are EuclideanSpace ℝ (Fin k), inner products are ⟪u, v⟫_ℝ, and matrices are continuous linear maps with the operator norm. is the published definition SolodovSvaiterVI.Alg21.viSol Φ K. Positive semidefinite matrices are not assumed symmetric.
Step sizes are with an integer , so that the grid ends exactly at . "For all " becomes "for all ", and "" becomes a strictly increasing sequence of 's. The iterates are a family indexed by and are hypotheses of the goal; their existence is the separate Proposition 7.1. Weak convergence in is tested against every function, and the uniform convergence of is on all of . Condition (7.6) is imposed for , because the paper's convention makes vacuous.
A weak solution carries integrability of both integrands as explicit conditions. Without them a non-integrable pair would satisfy the integral conditions vacuously, since a Lean integral of a non-integrable function is zero. The following readings are also excluded: convergence of the scheme only at grid points; a scheme in which solves the VI at instead of ; and a conclusion about one particular subsequence instead of every subsequence along which both limits exist.
A complete development needs: compactness in (Arzelà–Ascoli), weak sequential compactness of bounded sets in , Mazur's lemma on convex combinations, and estimates for piecewise linear and piecewise constant interpolants. The last two items are reusable for other time-stepping schemes. Proofs of any milestone, and of auxiliary interpolation lemmas, are welcome.
Out of scope: the weaker Carathéodory assumption (A′), the implicit scheme (7.3), the cited fixed-point theorems 7.2–7.3, and Theorem 7.4 (which combines Theorem 7.1 with the existence results of §6).
Quasi-Newton methods such as BFGS were designed for smooth objectives, yet in practice they are routinely and successfully applied to nonsmooth functions. Lewis and Overton (Math. Program. 141 (2013) 135–163) study why. A quasi-Newton step needs a step length along each search direction, and on a nonsmooth function the usual line searches have to decide what to do at points where the function is not differentiable. Classical inexact line searches for nonsmooth optimization (Lemaréchal 1981, Wolfe 1975, Mifflin 1977) ask an oracle for a subgradient at such points. Lewis and Overton propose a simpler rule: a trial point at which the objective is not differentiable simply fails the Wolfe test. This mission formalizes the analysis of that line search, §4 of the paper: when an acceptable step exists, when the bisection search finds one, what happens when it does not, and how many trials it takes on a convex function.
Let be an iterate of an optimization algorithm and a search direction. The line search objective is for . Only enters the analysis.
Assumption 4.1. The function is absolutely continuous on every bounded interval and bounded below, and
The number plays the role of the directional derivative .
Armijo and Wolfe conditions. Fix constants in . For ,
An Armijo–Wolfe step is a satisfying both.
Algorithm 4.6. Start from , , . At each trial: if fails, set ; otherwise, if fails, set ; otherwise stop. Then set if , and otherwise. So the search doubles until fails and then bisects the bracket . Write for the state before trial (lsRun), so . The search terminates if some trial passes both tests (Terminates).
Under Assumption 4.1 and :
Theorem 4.7 is the convergence guarantee for the line search used by the BFGS implementation analysed in the rest of the paper. It isolates the only failure mode: a derivative that oscillates as increases to a limit point, which condition (4.8) excludes. The paper notes that (4.8) holds for every semi-algebraic , so the search terminates on the functions met in practice. The same line search is the one whose trial sequence produces the binary-expansion behaviour of the secant method in §5. Theorem 4.5 shows that an acceptable step exists on a set of positive measure, which is why a sampling line search is not defeated by the null set of nondifferentiable points. Proposition 4.11 bounds the work per line search on convex functions.
All statements are proved in the paper. None has been formalized; there is no line search for nonsmooth functions on Prove2Me or in Mathlib. A formalization checks the measure-theoretic argument (absolute continuity and the fundamental theorem of calculus for Lebesgue integrals), the bookkeeping of the bisection, and the complexity count, where the printed upper bound turns out to be false for .
The obvious proof of termination fails: on a nonsmooth function the bisection can land on a kink at every trial, and the paper's §4.2 constructs a convex where it does. Termination therefore cannot follow from Assumption 4.1 alone, and both the existence of acceptable steps and the convergence of the brackets have to be argued through measure: Lemma 4.4 needs the fundamental theorem of calculus for absolutely continuous functions and a supremum argument over almost-everywhere inequalities. The non-termination analysis has to combine the bracket invariant with Lemma 4.4 on every late bracket and with a limit argument for (4.9). The complexity bound needs a careful count of doubling and bisection trials, including the regime where no doubling occurs.
The objective is h : ℝ → ℝ; only its values on enter. Lebesgue measure is volume with values in , and "nonzero measure" is volume S ≠ 0. Limits superior and inferior are computed in EReal. The upper bound is in WithTop ℝ, with . Stopping freezes the state of lsRun. Mathlib's deriv is at nondifferentiable points, so the Wolfe condition, condition (4.8) and (4.9) all state differentiability explicitly.
Deviations from the page, each disclosed in the item's Formalization Note:
Algorithm 4.6 is encoded as the literal state machine; a definition of the search as "some Armijo–Wolfe step" or as an arbitrary nested sequence of brackets would make the goal trivial and is ruled out. The Wolfe condition includes differentiability; without it every kink would pass, since .
A complete development needs absolute continuity (AbsolutelyContinuousOnInterval, with almost-everywhere differentiability and the fundamental theorem of calculus, both in Mathlib), the mean value theorem, and facts about one-sided derivatives of convex functions. Lemma 4.4 and the bracket invariant are reusable for other bracketing line searches. Contributions of the milestones in order, of proofs of the definitions' basic properties (all trial steps are positive, the brackets are monotone), and of the §4.2 non-termination example are welcome.
Quasi-Newton methods, BFGS above all, are the standard tool for smooth unconstrained minimization. They are also used directly on nonsmooth functions, where in practice they often converge to stationary points with linearly converging function values; the paper documents applications such as the design of low-order controllers (Lewis–Overton 2013, abstract and §1). Theory lags behind: as Lukšan and Vlček wrote, quoted on p. 136, "no global convergence has been proved for standard variable metric methods applied to nonsmooth problems". Methods with proved convergence modify quasi-Newton steps with bundle ideas; the unmodified method remains unexplained.
Lewis and Overton isolate the simplest nonsmooth case in which a complete analysis is possible: the Euclidean norm in the plane, minimized by any quasi-Newton method with an exact line search. The norm is differentiable everywhere except at its minimizer, so the method is well defined until it reaches the solution, yet the function is genuinely nonsmooth at the point the iterates approach. This mission formalizes that analysis (§3.1 of the paper).
Write for the Euclidean norm of and . For , is differentiable with gradient ; at it is not differentiable.
A quasi-Newton method (Algorithm 2.1 of the paper) starts from and a symmetric positive definite matrix . At iteration it
The line search is exact: minimizes . For the norm, the method stops exactly when some iterate equals ; "the algorithm does not terminate" means for every . The BFGS update (2.2) is one particular choice of .
Two plane notions describe the motion of the iterates: the unsigned angle , and the orientation sign of , positive when is a counterclockwise turn of . A real sequence converges to Q-linearly with rate when and (p. 141). Finally, denotes the angle between and .
For every non-terminating run of the method above, with any positive definite secant updates,
and there is with for all large : the iterates eventually rotate in one consistent direction.
Theorem 3.2 is a complete convergence-rate analysis of unmodified quasi-Newton methods on a function that is nonsmooth at its minimizer. It shows that the observed linear convergence is not an artefact of a particular update: the rate and the turn are forced by the exact line search and the secant condition alone, for every positive definite secant update. Proposition 3.3 shows that both constants are attained exactly by BFGS, so the theorem cannot be improved. The paper's experiments for (§3.2, p. 143) suggest similar behaviour, with observed rates growing with , and the authors state that they do not know how to extend the analysis; a formal two-dimensional analysis is the natural base for any attempt in higher dimension.
As far as we know none of these results has a machine-checked proof. A formalization would contribute the first verified statements about quasi-Newton iterations on a nonsmooth function, a reusable form of the exact-line-search orthogonality (Proposition 3.1, valid for any in any dimension), and an explicit, checked BFGS run in closed form.
The analysis rests on rotating and scaling so that , after which every quantity is an explicit trigonometric expression. In a formal setting this "without loss of generality" is not free: one must show that the exact step, the angles, the secant condition and the next direction all transform correctly under rotations and scalings, or carry out the computation in invariant form. The direction is only known up to sign from Proposition 3.1; fixing the sign requires positive definiteness of . The orientation claim is the most delicate part: the paper argues it from approximate values for large , which has to become an exact sign argument that holds eventually. Proposition 3.3 needs an induction through the BFGS formula with exact arithmetic in , including that each updated matrix stays positive definite.
Vectors are Fin 2 → ℝ (or Fin n → ℝ in Proposition 3.1) and matrices Matrix (Fin 2) (Fin 2) ℝ. The Euclidean norm is written out as , since Lean's default norm on Fin 2 → ℝ is the sup norm; with the sup norm every statement would change meaning. The gradient of the norm is the explicit formula . Positive definiteness is Matrix.PosDef, which includes symmetry (Proposition 3.1 needs it). A run is the predicate IsExactNormRun: , positive definite , , exact steps minimizing over all real (equivalent to here, because is a descent direction), and the secant condition whenever the method has not stopped. Non-termination is the separate hypothesis for all . Q-linear convergence of the vectors is read through the real sequence , following the proof's last line. Angles are unsigned and orientation is the sign of cross; "consistent orientation" is an eventual sign, not a limit of signed angles.
Corrections relative to the printed text, each disclosed in the item's Formalization Note:
A trivializing formalization is ruled out: the run predicate keeps positive definiteness and exactness (without them may be an ascent direction and Theorem 3.2 is false), its secant field is guarded so that it never involves the junk gradient at , and Proposition 3.3's existence clause certifies that the predicate is satisfiable.
The development needs elementary plane geometry with arccos, the BFGS update (reused from the published definition ShannoCG.SCONB.bfgsUpdate), and the contraction principle (Mathlib's ContractingWith). Rotation-invariance lemmas for the method would be reusable for any analysis of quasi-Newton methods on norms. Proofs of any milestone, and in particular an invariant treatment of the normalization step, are welcome.
Fourier analysis of functions on the discrete cube is the main tool behind tight inapproximability results under the Unique Games Conjecture. In the MAX-CUT reduction of Khot, Kindler, Mossel and O'Donnell (SIAM J. Comput. 2007), soundness rests on the Majority Is Stablest theorem: among bounded functions in which no coordinate has large influence, the majority function is asymptotically the most noise stable. That theorem was a conjecture when the paper was written and was proved by Mossel, O'Donnell and Oleszkiewicz (Annals of Math. 2010) using an invariance principle.
Section 6.2 of the paper records special cases of Majority Is Stablest that have short, self-contained proofs. Theorem 6 is the case where the noise parameter tends to . There the noise stability is dominated by the Fourier weight at level 1, and the statement says that a bounded function with small influences has level-one weight at most , up to an explicit error linear in the largest influence. Bounds on the level-one weight also appear in Talagrand's work on correlation of monotone sets (Combinatorica 1996), which the paper compares against (its Theorem 18), and the level-one inequality is a standard chapter of the analysis of Boolean functions (O'Donnell 2014).
Points of the discrete cube are sign vectors ; following the paper, the bit TRUE is read as and FALSE as . The cube carries the uniform probability measure, so , and real functions form an inner product space with .
For the parity ; the parities form an orthonormal basis, and the Fourier coefficient of at is . The weight of at level 1 is
The influence of coordinate on (Definition 2) is
the expected variance of when all coordinates but are fixed at random and is a uniform sign. The linear part of is , and , , .
Throughout, .
For every , every and every with for all ,
The constant is explicit, and the goal states it exactly as printed.
The result. The constant is sharp: majority on variables has influences of order and level-one weight tending to , which is for a standard Gaussian . Theorem 6 thus identifies the extremal level-one weight of low-influence bounded functions and gives a rate linear in the maximal influence. It is the instance of Majority Is Stablest, obtained without the invariance principle, and level-one bounds of this type are used in hardness reductions and in the study of noise sensitivity.
Formalizing it. The milestones together give a complete formal route from bounded functions to the stated bound, except for one step discussed below. They also produce a reusable layer of Boolean Fourier analysis: Fourier coefficients, level weights, influences in their variance form and the Fourier formula for influences. Mathlib contains no development of influences or level weights on the cube, and the platform has none either; the König–Schütt–Tomczak-Jaegermann inequality, a sharp quantitative central limit bound for Rademacher sums (J. Reine Angew. Math. 1999), has no machine-checked proof.
Status. The published proof's first step, , is valid for Boolean-valued but not for -valued ; for -valued the statement is posed as printed. For with one has , and the argument as written then yields only . Numerical search over small cubes has found no function violating the printed bound. A proof of the goal for bounded , or a counterexample, is therefore a genuine contribution.
The obvious argument replaces by a Gaussian with the same variance and uses . A central limit theorem with an error term is needed, and generic Berry–Esseen bounds give an additive error with a constant far from ; the exact constant requires the sharp Rademacher-sum inequality, whose proof is a delicate analysis of as a function of the coefficients. The second obstacle is the passage from influences to coefficients. For bounded only holds, so a bound on influences controls coefficients only at scale ; feeding that into the chain loses the linear dependence on . Recovering the printed rate for non-Boolean needs an idea beyond the published proof.
A point of the cube is Fin n → Bool, mapped to a sign by pm with pm true = -1 and pm false = 1. Expectations are normalised finite sums, so no measure theory is involved. A function is a real function with the hypothesis ∀ x, |f x| ≤ 1. The influence is defined as on the page, as the average over the cube of , which is the variance in ; it is not defined by its Fourier formula, which is a milestone. The level-one weight is . The constant is written out as 2 * (1 - Real.sqrt (2 / Real.pi)); an existentially quantified constant would be a weaker theorem. The case is allowed.
Two hypotheses are added and disclosed: in Theorem 6 and in the König–Schütt–Tomczak-Jaegermann bound. For each follows from the other hypotheses; for the influence (resp. coefficient) hypothesis is empty and is what the page assumes.
A trivializing formalization would drop the range hypothesis (then scaled dictators refute the bound and the statement is false), define influence through Fourier coefficients (which makes Proposition 7.2 definitional), or weaken the hypothesis of the goal to a bound on the coefficients ; none of these is used here. In particular, the goal is not strengthened to Boolean-valued , where the published proof applies verbatim.
Contributions welcome: proofs of Parseval-type identities for the linear part, of Proposition 7.2, of the elementary quadratic step, of the König–Schütt–Tomczak-Jaegermann inequality, and of the goal itself. The cube layer is reusable for any later formalization of Boolean function analysis.
A differential variational inequality (DVI) couples an ordinary differential equation for a state with a finite-dimensional variational inequality that the algebraic variable must solve at every instant. The class contains complementarity systems from contact mechanics and electrical circuits with diodes, linear complementarity systems from control theory, differential Nash games, and the first-order optimality conditions of optimal control problems with inequality constraints. J.-S. Pang and D. E. Stewart introduced the unified framework in Differential variational inequalities, Math. Program. 113 (2008) (author's version, hal-01366027), and Section 6 of that paper settles the first question any such model raises: when does the initial-value problem have a solution on a whole prescribed time interval?
Before this work, existence results for these systems were tied to special structure: linear complementarity systems with "minimal" and "passive" data, or a given initial condition compatible with the complementarity kernel. Theorem 6.1 gives existence for every initial state under five separate conditions on the variational inequality, each describing a different class of DVIs.
Fix and write . For a set and a map , the variational inequality asks for with for all ; its solution set is . The initial-value DVI studied here is
with nonempty, closed and convex, , , and . Two standing assumptions hold throughout: (A) , , are Lipschitz continuous on ; (B) is bounded on in operator norm.
A pair is a weak solution (in the sense of Carathéodory) on if ; is integrable on with almost everywhere; for , with an integrable integrand; and for every continuous ,
with an integrable integrand. The existence proof passes through the differential inclusion with the set-valued right-hand side
Further objects: the recession cone ; the dual cone ; the VI kernel , the solution set of ; an R₀ pair , one with ; a psd-plus matrix , one with for all and ; and the linear growth property
Under (A) and (B), if any one of the following holds, then (6.2) has a weak solution on for every :
Theorem 6.1 is the existence result behind the rest of the paper: Sections 7 and 8 prove that time-stepping schemes converge to weak solutions of (6.2), and those results are informative only for problems that have solutions. Condition (d) gives existence for every initial state of linear complementarity systems , with , where earlier results required passivity or a compatible initial state. Propositions 6.2–6.5 are results on static variational inequalities in their own right: the linear growth of solution sets in the data had not been a focus of VI theory.
The result is proved in the paper, modulo two cited theorems (Deimling's existence theorem for convex-valued differential inclusions and Filippov's measurable selection lemma). None of it is formalized. A Lean development would supply set-valued upper semicontinuity, Carathéodory solutions of differential inclusions, and existence and linear growth theory for VIs on closed convex and polyhedral sets: material with uses well beyond this paper.
The obvious route, solving the VI for as a function of and substituting into the ODE, fails: the solution map is in general set-valued and discontinuous, so the resulting right-hand side is neither single-valued nor continuous, and classical ODE existence does not apply. The detour through the differential inclusion (6.4) requires convex values, which hold when is monotone but must be proved separately in case (e), where is not monotone. It also requires linear growth (6.5), which for unbounded is a genuine statement about the asymptotics of VI solutions and needs a different argument under each of the five conditions: coercivity, a recession-cone condition, the VI kernel, or a fixed-point argument on polyhedra. Finally, Deimling's theorem and Filippov's lemma are substantial results of set-valued analysis that are not in Mathlib.
Points of are EuclideanSpace ℝ (Fin k); matrices are continuous linear maps, is the operator norm and the adjoint. Data on are curried functions on of which only the values on matter, and Lipschitz continuity on uses the metric . is the published definition SolodovSvaiterVI.Alg21.viSol Φ K. Positive semidefinite matrices are not assumed symmetric. "Monotone" in (a) and Proposition 6.2 means monotone on . The coercivity (6.6) is written in the equivalent form " for with ". Upper semicontinuity is the open-neighbourhood form relative to . In Proposition 6.4 (b) the Lipschitz property is stated on the dual cone , where the paper's proof establishes it (the statement prints ). Nonemptiness of , the paper's standing assumption on variational inequalities, is a hypothesis throughout.
The weak-solution definitions carry explicit integrability conditions on the integrands of the integral equation and of (2.4), and (2.4) is required for every continuous with values in . A definition without those integrability conditions (a Lean integral of a non-integrable function is zero), a variational condition tested only on constant , or (A)–(B) replaced by global boundedness of and would make the goal a different and weaker statement; none of these is used.
Contributions welcome at every level: proofs of the milestones, a general theory of upper semicontinuous set-valued maps and Carathéodory solutions of differential inclusions, and existence results for variational inequalities via recession cones and degree theory.
A spectral sparsifier of a weighted graph is a graph on the same vertices, with few edges, whose Laplacian quadratic form is within a factor of that of on every vector. Spielman and Teng introduced the notion in their work on nearly-linear-time solvers for symmetric diagonally dominant linear systems (Spielman–Teng 2004; arXiv:0808.4134): a sparsifier can replace a dense graph as a preconditioner, and it preserves every cut value up to the same factor, strengthening the cut sparsifiers of Benczúr and Karger (BK96).
Their construction first handles graphs whose edge weights lie in a bounded range. Arbitrary weights need an extra idea, which §10.2 of Spectral Sparsification of Graphs formalizes as Lemma 10.2 (Pullback): when a graph's vertex classes are held together by edges far heavier than those between them, one may contract each class to a single vertex, sparsify the much smaller contracted graph, and pull the result back to the original vertices. The approximation factor degrades only by , where measures the gap between heavy and light weights. The same contraction idea goes back to Benczúr and Karger's treatment of weighted cut sparsifiers.
A weighted graph on a finite set , , is a symmetric function with ; its edges are the pairs with . Its Laplacian quadratic form is
A graph is a -approximation of if for all . We write when for all , for the graph whose weights are the sums, and for the single edge of weight .
Let be a partition of with map . Write for the edges between different parts, , and , . The contraction of under is the graph on with weight for and no self-loops. Given a graph on , a graph on is a pullback of under if every edge of joins different parts, is the contraction of , and for every edge of exactly one edge of has , . A pullback thus has as many edges as .
Let , , let be a -approximation of the contraction of under , and let be a pullback of . Assume (1) each is connected by edges in , (2) every edge in has weight at least , (3) every edge in has weight . Then
Choose representatives ; let , be the copies of , on , and , .
The constants are the paper's; the goal is the lemma as printed.
Lemma 10.2 is the reduction from arbitrary weights to bounded weights in Spielman and Teng's sparsification algorithm (Sparsify, §10.2): the edges of each weight scale are sparsified on a graph in which all much heavier edges have been contracted, so the number of vertices handled at each scale stays small, and the total size of the sparsifier is only a logarithmic factor larger than in the bounded-weight case. The statement itself is purely about quadratic forms and holds for any approximation of the contraction, however it was obtained; it applies equally to later sparsification methods such as sampling by effective resistances.
The lemma is proved in the paper. As far as is known, none of these statements has a machine-checked proof: Mathlib has the Laplacian of a simple graph (SimpleGraph.lapMatrix) but no weighted Laplacian order, no contraction of weighted graphs and no notion of spectral approximation. The mission produces those objects and a complete formal proof of the lemma and its intermediate claims.
The individual steps are elementary, but the proof combines three kinds of bookkeeping. Lemma 10.3 is a Cauchy–Schwarz inequality along a path, which must be applied to a path assembled from two walks inside parts and one edge between representatives; obtaining a simple path of length at most from the connectivity hypothesis requires shortening walks. The summed bounds require recognising that the copies of the unit edges between representatives add up exactly to , which uses hypothesis 3 and the fact that contraction counts each edge between two parts once. Claim (c) needs, in addition, that the total weight of is at most times that of and that each pullback edge has the weight of its image edge. The constants are tight in one place: requires both and .
A natural shortcut, comparing with directly, fails: and have different edges, and their Laplacians are only comparable through the heavy intra-part edges.
A weighted graph is a function w : V → V → ℝ on a Fintype V with IsWGraph w (symmetric, nonnegative, zero diagonal); sums and scalar multiples are pointwise. lapForm w x is , IsApprox σ w̃ w keeps both inequalities of the definition, and GraphLE is . The partition is a surjective map π : V → Fin k (nonempty parts). , are crossPart w π, intraPart w π; hypothesis 1 is reachability, between any two vertices of the same part, in the simple graph of -edges. Representatives are any r : Fin k → V with π (r i) = i, and liftAlong r z places a graph on Fin k on them; the goal does not mention representatives. is Fintype.card V.
Two hypotheses implicit in the paper are explicit: (with the lemma is false), and that every edge of a pullback joins two different parts (contraction cannot see an edge inside a part, so without this a pullback could carry an arbitrary heavy edge and the lemma would be false). In Lemma 10.3 the edge weights are positive and the path has at least one edge.
A trivializing formalization is ruled out: dropping hypothesis 2 or 3, allowing or intra-part pullback edges, or letting the pullback forget the uniqueness of the edge over each makes the statement false or weaker, and stating only one of the two inequalities of -approximation is a different theorem. Every statement here keeps both.
The algorithm Sparsify and its analysis (Lemma 10.4, Theorem 10.5, Proposition 10.6, Theorem 10.7, Lemmas 10.8–10.9) and all running-time claims are out of scope. The weighted Laplacian form, its additivity and nonnegativity, and the transport of a quadratic form along an injective vertex map are reusable beyond this mission; contributions of such general lemmas, and a proof of Lemma 10.3 by Cauchy–Schwarz, are welcome.
A manufacturer must commit to production before its retail customer knows what the market will demand, while the customer would rather postpone its purchase until better information arrives. Left uncoordinated, each firm protects itself: the customer inflates forecasts it is not bound by, and the manufacturer, discounting those forecasts, builds less than the supply chain as a whole should. Quantity flexibility (QF) contracts, used in practice in the electronics and computer industries (Sun Microsystems, Solectron, Nippon Otis and others are cited in the paper), address this by tying the customer's forecast to a band: the manufacturer guarantees supply up to a percentage above the forecast, and the customer promises to buy at least a percentage below it.
Tsay (1999) gives a two-stage model of such a contract with a demand signal that arrives between production and purchase, shows that a supply chain without commitment underproduces, and characterizes when a QF contract restores efficiency. This mission formalizes the efficiency result for the case in which the signal predicts demand perfectly (Proposition 6(a)), together with the steps of the equilibrium that it rests on.
A manufacturer (EM) produces at unit cost and sells to a retailer at unit transfer price ; the retailer sells at price , unsold units are salvaged at at either site, and each unit of unmet demand costs a goodwill loss . The standing assumptions are , and .
Before production, the retailer states a forecast . A QF contract with and obliges the EM to make up to available and the retailer to buy at least . The EM then builds . A demand signal with distribution function is observed, the retailer buys , and market demand is filled from the retailer's stock. In this mission the signal is perfect (): market demand equals , so its distribution equals .
Given , the retailer's profit from buying is
and it buys , the point of the interval closest to . The EM's expected profit (2) is . The retailer's forecast problem maximizes with the EM building . A central planner earns , maximized at
The total flexibility of the contract is .
With , the QF contract with flexibility and transfer price
is system-efficient: the retailer's unique optimal forecast is , the EM's unique optimal production given is , and the resulting expected system profit equals .
The result shows that one contract form, by choosing the transfer price as a function of the flexibility, yields a whole menu of contracts each of which coordinates the supply chain, so that the two firms can trade price against flexibility without losing system profit. Its corollaries in the paper, that any split of expected profit is achievable by some efficient contract and that more flexibility shifts profit to the manufacturer, rest on (4).
The paper prints no proofs ("All proofs are omitted due to space limitations", p. 1341). A machine-checked development supplies them, makes explicit the regularity the argument needs (finite variance, a continuous and strictly increasing , a positive efficient quantity), and gives reusable statements about newsvendor objectives with a clipped purchase. To our knowledge none of these results has been formalized before; the platform's quantity-flexibility theorems in other models (no manufacturer production stage, , retailer side only) do not cover them.
Each firm optimizes its own objective, and the efficient price must work for both at once. Making the retailer's first-order condition hold at pins down , so nothing is left to adjust for the EM, whose incentive to build more than the contracted has to be ruled out separately at that same price. The retailer's objective is an expectation of a non-smooth function of a clipped purchase, so its derivative must be computed through the distribution of on two moving thresholds and , and strict concavity must come from the strict increase of rather than from a density.
All objects live in the namespace TsayQF.EffQF. The law of is a probability measure on with , whose distribution function cdf ν is differentiable and strictly increasing on (the paper's "differentiable and invertible"). Expectations are Bochner integrals; finite variance makes every integrand integrable. Inverse distribution functions are not used: enters as a real number with the hypothesis , which determines it uniquely, and (4) is defined in its printed shape. Optimality is IsMaxOn over the decision's natural set: forecasts in , the EM's production in , purchases in , central production in .
Hypotheses made explicit: in the goal and a positive marginal value of the forecast at in Proposition 3(a), both standing for the paper's presumption that demand is almost certainly nonnegative; (Proposition 3's case). The transfer price is only required to satisfy rather than , because can exceed when . The milestones are the instances of the paper's general statements.
Two modelling choices are fixed. The retailer's forecast objective takes the EM's production to be , as §6.1 does after Proposition 2; the full game in which the retailer anticipates other EM responses is not modelled, and the goal instead verifies that the EM's unique best response at is exactly . The efficient price is the explicit formula (4), not "a price that makes optimal", which would make the goal a tautology; likewise system efficiency is stated as an inequality against at every production level, not by definition.
Needed infrastructure: derivatives of expectations of piecewise-linear functions of a clipped variable, and the newsvendor fractile characterization. Both are reusable for other contract models. Proofs of any milestone, and of the goal from the milestones, are welcome.
A manufacturer must commit to production before a retailer knows how much it will buy. In practice the retailer sends a forecast first, and the manufacturer plans against it. When the forecast binds neither party, the retailer has no reason to report it honestly, and the manufacturer has no reason to plan for the market rather than for its own margin. Purchasing managers have described this to Tsay directly, and Lee, Padmanabhan and Whang (1997) document such "phantom ordering" in several case studies.
A. A. Tsay, The Quantity Flexibility Contract and Supplier-Customer Incentives (Management Science, 1999), models the situation as a two-stage newsvendor game with a demand-information update between production and purchase. Its first result, Proposition 1, is the benchmark the rest of the paper builds on. Even when both parties share the same beliefs about demand, a linear transfer price alone leaves the manufacturer underproducing relative to a central planner, and the supply chain loses expected profit, for every transfer price. That inefficiency motivates the quantity flexibility (QF) contract studied in the remainder of the paper and in the companion mission of this series.
Costs. The retail price is and the unit transfer price paid by the retailer to the manufacturer (the EM) is . The unit production cost is , the unit salvage value is (the same for either party), and the unit goodwill loss on unmet demand is . The paper's standing assumptions (§3.1, p. 1344) are
Three critical fractiles recur:
Demand (§3.3). Market demand is . The signal has distribution function , which is differentiable and strictly increasing, and finite variance. The error is independent of . is the distribution function of , is the standard normal distribution function, and .
Timing (§3.2). The EM produces knowing only the prior. Then is observed and the retailer buys . Then is realized, and both parties salvage their surplus. Given , the retailer's expected profit from purchase is
Without commitment the retailer buys . The EM's expected profit is
and the retailer's is . A central planner producing before the signal earns
Let maximize and maximize . Then, for every transfer price admitted by the standing assumptions,
and the retailer's optimal purchase under is . 3. §5.2, p. 1347. The EM's optimal production exists and is unique:
Proposition 1 shows that sharing demand information does not remove inefficiency. Under common beliefs and with no commitment, no linear transfer price makes the decentralized chain efficient. Adjusting moves profit between the parties but cannot recover the planner's expected profit. This is the reason the paper studies richer contracts, and the efficiency result for the QF contract (the paper's Proposition 6) is measured against the benchmark defined here.
The paper prints no proofs ("All proofs are omitted due to space limitations", p. 1341). A machine-checked development therefore supplies arguments the published record does not contain. It also exhibits the exact hypotheses the result needs. In particular it covers the degenerate case , where the signal is perfect. No part of this mission has a prior formal proof. Newsvendor critical-fractile results exist on Prove2Me for single-decision models, but without the production stage and information update used here.
The EM and the planner solve newsvendor problems against different demand laws. The EM faces the retailer's purchase , while the planner faces . Their fractiles are and . The obvious comparison, , settles the case only. For the two quantities are inverse distribution functions of different random variables. may be negative, and the planner's distribution is a convolution. A comparison of fractiles alone therefore does not order and . The strict profit gap also needs more than optimality of : it requires comparing the decentralized system profit at with the planner's profit at the same production, and then using uniqueness of the planner's optimum.
The analytic infrastructure is also substantial. It includes differentiating expectations of piecewise-linear functions under a Gaussian law and under a general prior, continuity and strict monotonicity of a convolution's distribution function, and existence of a root of .
All objects live in the namespace TsayQF.NoCommit, in one definitions file Model.
Data with fields and the standing assumptions (i)–(iii) as fields. "For any " is quantification over all Data. No sign is imposed on .ν on ℝ; is cdf ν. "Differentiable and invertible" is Differentiable ℝ (cdf ν) together with StrictMono (cdf ν), and "mean and variance" is MemLp id 2 ν.v : ℝ≥0, so and v = 0 is allowed. The law of is the pushforward of ν.prod (gaussianReal 0 v) under addition, and given demand has law gaussianReal μ v.z with hypothesis cdf (gaussianReal 0 1) z = kR D. The milestones state existence of a solution of each fractile equation and characterize the maximizers by it.IsMaxOn over Set.univ for productions and over Set.Iic Q for the purchase. Productions range over ; the paper's presumption that and are almost certainly nonnegative is not imposed, because no result here needs it.The goal must not be weakened to non-strict inequalities, and the EM's demand must remain the retailer's purchase , not market demand. Either change trivializes the result or changes it. Reusable pieces are the newsvendor critical-fractile characterization for a general continuous strictly increasing distribution, and monotonicity and continuity of the distribution function of a sum of independent variables with one Gaussian summand. Proofs of the milestones as standalone lemmas are welcome.
Stochastic differential equations (SDEs) are simulated almost always by time-stepping schemes, and the cheapest and most widely used is the explicit Euler (Euler–Maruyama) scheme. Its strong convergence with order is classical when the coefficients are globally Lipschitz. Many models in applications are not: Langevin dynamics with confining potentials, stochastic Ginzburg–Landau equations, and population or volatility models have drifts such as that grow superlinearly.
For such drifts the explicit Euler scheme fails. Hutzenthaler, Jentzen and Kloeden showed in 2011 (Proc. R. Soc. A 467) that its absolute moments diverge to infinity whenever the drift or the diffusion grows superlinearly, so it does not converge in . Implicit schemes do converge (Higham, Mao and Stuart, SIAM J. Numer. Anal. 40, 2002), but each step requires solving a nonlinear equation.
The paper of this mission (Hutzenthaler, Jentzen and Kloeden, Ann. Appl. Probab. 22(4), 2012) introduces a tamed Euler scheme: an explicit method that costs the same as the Euler scheme, modified by a second-order term in the drift. It proves strong convergence with order under a one-sided Lipschitz drift whose derivative grows at most polynomially. The scheme started a line of work on tamed and truncated methods, among them Sabanis's schemes that tame drift and diffusion together for superlinearly growing diffusion coefficients (Ann. Appl. Probab. 26(4), 2016), formalized on this platform in the series "Euler Approximations with Varying Coefficients".
Fix and . Let be a probability space with a filtration , and let be an -dimensional standard -Brownian motion. On , is the Euclidean norm and the inner product. For a matrix , is the operator norm.
The initial value is -measurable with for every . The drift is continuously differentiable and the diffusion is . There is one constant with
for all . The exact solution is an adapted process with continuous paths and
For , let . The tamed Euler scheme is and
On its interpolation is
In Lean, states live in EthierKurtz.SDEState d, takes values in Matrix (Fin d) (Fin m) ℝ, the standing hypotheses are the structures Coefficients and Setting, and the scheme is Y, Ybar, all in the namespace TamedEuler.Convergence.
There is a family , , such that for every solution
The constants are left unspecified; only the order is asserted.
These are the ten lemmas the proof rests on, in the paper's order:
The theorem gives an explicit scheme whose cost per step is the Euler cost and whose strong error is in every , uniformly in time, for the superlinear drifts on which the explicit Euler scheme diverges. Strong error bounds of this kind are what multilevel Monte Carlo (Giles 2008) needs, as the paper notes on p. 3: its complexity analysis requires strong convergence of the coarse and fine levels, and the explicit Euler scheme supplies none for these equations. The moment bound of Lemma 3.9 answers, for the tamed scheme, the open problem Higham, Mao and Stuart formulated in 2002 on when moment bounds hold for explicit methods (quoted on p. 8).
The result is proved in the paper; it has not been formalized. The mission formalizes the statement, its ten lemmas and the scheme. The dominator construction (13)–(14) is a pathwise argument that can be checked independently of the probability. The two Burkholder–Davis–Gundy inequalities with the explicit constant are reusable tools for any numerical analysis of SDEs.
Once the moments of are bounded uniformly in , the convergence proof follows the globally Lipschitz pattern: an Itô or Gronwall argument on . The difficulty is the moment bound itself. The obvious approach is a Gronwall recursion for in terms of . For superlinear it does not close: the term grows faster than , and for the untamed scheme the moments do in fact diverge. A newcomer's first idea, using the one-sided Lipschitz bound in expectation, fails for the same reason. The paper instead dominates the scheme pathwise on events and controls the rare complement separately (Lemmas 3.1, 3.5, 3.6).
The Lean development commits to the following conventions.
ℱ.IsRightContinuous) together with adaptedness to its -completion, which is how the published SabanisEuler.Shared.IsSolution treats completeness.SabanisEuler.Shared.IsWienerMartingale, defined on rather than ; this is the usual extension. Time is ℝ≥0.IsSolution relation, whose stochastic integral is the Ethier–Kurtz Brownian Itô-integral relation. Existence and uniqueness are cited by the paper, not claimed. enters IsSolution entrywise through toDiffusion. Every norm of in a hypothesis or conclusion is the operator norm opNorm.lintegral or eLpNorm, never as a Bochner integral that could default to .A trivializing formalization is ruled out: the scheme is (8) exactly, with only the drift tamed and the step size . The error is taken against the same Brownian path that drives . The setting is satisfiable for the paper's example , with (checked in a sorry-free verification file, given any Brownian motion). Replacing the Itô integral by a postulated operator or a pathwise integral is not admitted.
A complete development needs:
The BDG inequalities and the Gaussian moment identity are reusable beyond this mission. Contributions to any lemma, or to the stochastic-calculus infrastructure underneath, are welcome.
Minimizing the sum of the largest eigenvalues of a symmetric matrix that depends affinely on parameters is a basic problem of eigenvalue optimization (survey: A. S. Lewis and M. L. Overton, Eigenvalue optimization, Acta Numerica 5, 1996, doi:10.1017/S0962492900002646). Its objective is convex, and is differentiable at exactly when ; at optimal solutions the eigenvalues tend to coalesce, which makes the problem a model problem of nonsmooth optimization. G. Pataki, On the rank of extreme matrices in semidefinite programs and the multiplicity of optimal eigenvalues (Math. Oper. Res. 23(2), 1998, doi:10.1287/moor.23.2.339), gives a quantitative explanation in terms of the number of free parameters.
The paper also proves a bound on the rank of extreme points of semidefinite programs, now often called the Pataki bound (also obtained by Barvinok, 1995): an extreme point of satisfies . This bound is used throughout low-rank semidefinite optimization, for instance in the Burer–Monteiro approach.
is the space of real symmetric matrices, means is symmetric positive semidefinite, and . For , are its eigenvalues and, for ,
The multiplicity is the largest with for some .
A face of a convex set is a convex such that , , imply ; an extreme point is a one-point face; is the maximal number of affinely independent points of , minus one. Write and
Let be linearly independent, , and assume and (the standing assumptions of §4). The affine eigenvalue problem is
and denotes its set of optimal solutions, a closed convex set. For the semidefinite program
has optimal value ; is its set of optimal solutions .
If is an extreme point of and , then
The theorem says that once the number of free parameters exceeds , the -th and -st eigenvalues necessarily coincide at extreme optimal solutions, so is typically nonsmooth at its minimizers, and it bounds from below the dimension of the subdifferential , which is . The intermediate rank bounds of §2 are reusable on their own for any semidefinite program.
The results are proved in the paper. As far as is known, none of them (neither the Pataki rank bound, nor the semidefinite characterization of , nor Theorem 4.3) has a machine-checked proof. Formalizing them produces a library of faces and dimensions of spectrahedra, the SDP representation of the Ky Fan sum , and the multiplicity bound itself.
Extremality of in is a statement in the parameter space and gives no direct information on the spectrum of : perturbation arguments on the eigenvalues alone break down precisely at the coalesced eigenvalues the theorem is about, where is not differentiable. The quantitative bound (4.30) also needs more than the optimal value : it depends on the whole optimal set , on the dimension of faces of spectrahedra, and on an exact count relating the ranks of the optimal to the multiplicity of . None of these (faces and dimension of spectrahedra, the semidefinite representation of , eigenvalue run lengths) is in Mathlib.
Matrices are Matrix (Fin n) (Fin n) ℝ; is the published BurerMonteiro.RankIncrease.frob, the primal and dual feasible sets are the published IsPrimalFeasible/IsDualFeasible, and is the published ProjLikeRetr.Spectral.eig B ⟨i-1,_⟩ (Mathlib's nonincreasing eigenvalues, 0-based). Every matrix whose eigenvalues are taken is assumed symmetric. Faces, extreme points and dimension are defined as on p. 341; dimension is integer valued with . All rank bounds are compared in . is the argmin set and is the set of feasible points no worse than every feasible point; no infimum is used. Optimal values are stated as least elements of the set of feasible objective values.
Hypotheses added relative to the page, each disclosed in its item: in the statements of §3, which mention ; (p. 340) in every §4 statement; one common matrix order in Theorem 2.2; and in the rank identity of p. 348, which is false as printed when (, , gives ) and is used in the paper only in the equal case. The linear independence of is kept with included, as on p. 348.
Trivializing formalizations are ruled out: is not defined through a possibly junk infimum, a face must be convex and contained in the set, the dimension is not a junk , is the run length of equal eigenvalues and not a constant or an index, and the eigenvalues are only ever taken of symmetric matrices.
A complete development needs: the rank–dimension bound for faces of spectrahedra (reusable for any SDP), the semidefinite characterization of with its optimal set, and convexity facts on . Proofs of any milestone, alternative proofs of the rank bounds, and the general smooth case of §5 are welcome.
A non-interactive zero-knowledge (NIZK) proof lets a prover convince a verifier that a statement is true by sending a single message, without revealing why it is true. Groth, Ostrovsky and Sahai (J. ACM 59(3), 2012) gave NIZK proofs for Circuit SAT of size for a circuit and security parameter , the first perfect NIZK arguments for all of NP, and the first non-interactive zaps based on a standard cryptographic assumption. These constructions use a single algebraic primitive, the homomorphic proof commitment: a commitment scheme with two kinds of keys, together with a short proof that a committed value is or .
The paper gives two instances of this primitive. One rests on the subgroup decision assumption in composite-order groups. The other, the subject of this mission, rests on the decisional linear assumption of Boneh, Boyen and Shacham (CRYPTO 2004) in prime-order bilinear groups. Prime-order groups are the setting of most later pairing-based proof systems, including the Groth–Sahai proofs (EUROCRYPT 2008), and their decisional-linear instantiation uses commitment keys of the same linear-tuple form as this mission.
A DLIN bilinear group is a tuple : is a prime, and are groups of order , is bilinear ( for all , ), generates , and generates . A triple is a linear tuple with respect to .
The scheme (Figure 2 of the paper) works as follows.
The perfect properties of Section 3 are: homomorphism, perfect binding, perfect extractability, perfect trapdoor opening and its indistinguishability, perfect completeness, perfect soundness, perfect witness indistinguishability (WI), and perfect non-erasure WI. Non-erasure WI asks that a simulator turn the randomness of a proof made with one witness into randomness that explains the same proof under the other witness.
For every DLIN bilinear group, the scheme of Figure 2 is homomorphic on both kinds of key and perfectly binding and extractable on binding keys. On hiding keys it has perfect trapdoor opening and perfect trapdoor-opening indistinguishability. Its 0/1 proof is perfectly complete on both kinds of key, perfectly sound on binding keys, and perfectly WI and perfectly non-erasure WI on hiding keys. Soundness, for example, reads
The milestones follow the paper's proof:
The perfect properties are what the paper's later results consume. Perfect soundness and extractability on binding keys give the perfectly sound NIZK proof of knowledge for Circuit SAT (Theorem 6). Perfect WI, trapdoor opening and non-erasure WI on hiding keys give perfect zero-knowledge (Lemma 8 and Theorem 11) and the adaptive and UC-secure variants of Sections 7 and 8. Theorem 4 transfers all of this to prime-order bilinear groups under the decisional linear assumption.
The theorem is published and its proof is short, but the printed construction contains an error. With the signs of in and as printed in Figure 2, an honest proof fails the fourth and sixth verification equations whenever . A machine-checked proof fixes the corrected construction, under which the paper's own witness-indistinguishability argument goes through. No formalization of this scheme, or of the decisional linear setting, exists on the platform or in Mathlib.
The algebra is modest. The work lies in carrying exponents in through powers in groups of order , and in getting the soundness argument right. An accepted proof only constrains discrete logarithms of the proof elements, so the six pairing equations must first be turned into six equations between exponents. That step is valid only because , and are nondegenerate. Soundness then needs the observation that the product of two specific linear forms vanishes, and it fails outright on a hiding key (). Witness indistinguishability is an exact identity between proofs, which holds only for the corrected prover.
G →* G →* GT, which is equivalent to bilinearity. generates and generates .ZMod p, acting through their representative in .Classical safety-stock formulas assume that demand is stationary: independent and identically distributed around a fixed mean. Many products do not behave that way. Their demand level drifts, and the forecast has to follow it. Graves (A single-item inventory model for a nonstationary demand process, Manuf. Serv. Oper. Manag. 1(1):50–61, 1999) works out what such drift costs in inventory when it is modelled by the simplest nonstationary time series used in forecasting practice. The model is the integrated moving average process of order , for which the exponentially weighted moving average is the optimal forecast (Muth, 1960; Box, Jenkins and Reinsel, 1994).
The paper answers two questions. For one stage under an adaptive base-stock policy, it gives the exact distribution of the inventory, and hence the safety stock. For two stages in series, it shows that the order stream the downstream stage passes upstream is again of the same type, amplified. This is an explicit instance of the bullwhip effect of Lee, Padmanabhan and Whang (1997). The paper then gives the distribution of the upstream inventory. That last distribution, equation (16), is the goal of this mission.
Time is indexed by periods ; operation starts in period . Fix a mean level , a parameter with , a downstream lead time and an upstream lead time . The shocks are independent random variables, each normal with mean and variance .
Downstream stage (§2). The demand is the IMA(0,1,1) process
The forecast , made after observing , is the exponentially weighted moving average
The order , placed in period and delivered in period , follows the adaptive base-stock policy
The inventory at the end of period (negative values are backorders) obeys
where is an initial inventory chosen by the planner. Orders may be negative.
Upstream stage (§3). It sees the orders as its demand. It forecasts them with smoothing constant ,
orders for and for (15), and holds inventory
with initial inventory .
In Lean, IsStage μ α L ε d F q x is the conjunction of (1), (3), (6), (7) and the boundary condition. IsUpstream μ β K q G p y is (11), (14), (15) and its boundary condition. upBeta α L is , and IsTwoStage is the conjunction of the two stages.
For every period (and ), the upstream inventory is normally distributed with
Two further statements of the paper are included as plain theorems: the order amplification (p. 55), stated as: and are independent of with laws and , and the critical-fractile rule (p. 54). Under that rule, setting gives .
Equation (8) is a closed-form safety-stock formula for nonstationary demand. For the standard deviation of the inventory grows faster than , so the textbook square-root law understates the safety stock. Equation (16) carries the formula one stage up a supply chain. With , the upstream safety stock depends on the downstream lead time , not only on the upstream lead time . The paper concludes that shortening the downstream lead time can matter more than shortening the upstream one. P1 and P2 underlie these conclusions: they write each inventory as a fixed linear combination of a bounded window of shocks.
All results here are proved in the paper. None of them, and none of the model's objects, is formalized on Prove2Me or, as far as is known, anywhere else. The mission produces machine-checked versions of the closed forms and distributions. It also produces a reusable statement that a finite linear combination of independent Gaussian shocks is Gaussian, which Mathlib has only for two summands.
The pathwise milestones are inductions on the period, but they are not uniform. The inventory recursion (6) reads orders periods back, so P1 has two regimes: , where every order read is a policy order, and , where some are the boundary orders . The paper treats the second regime only by "direct substitution", and a single statement has to cover both.
P2 is not a second copy of P1. The upstream stage is defined by its own recursions (11), (14), (15). It becomes an instance of the single-stage model only after (10) and the forecast identity have been proved, and P1 must then be applied with parameter and shocks . The distributional statements (8) and (16) need the law of a finite weighted sum of independent normal variables. Mathlib provides the two-variable case; the finite-sum version, with a -indexed window of shocks, has to be built from it.
All sequences are functions ; lead times are natural numbers, cast to in indices and to in coefficients, so no truncated subtraction occurs. The model is a predicate on sequences, and the objects are constrained only by the paper's recursions (1), (3), (6), (7), (11), (14), (15) and the boundary conditions for . None of the closed forms (2), (5), (9), (10), P1 or P2 is built into a definition. In particular the upstream stage is not defined as an instance of the downstream one, which would assume (10). The paper's convention for is implemented by a masked sequence masked ε in P1 and P2, not by a hypothesis. The standing assumption is a hypothesis of every theorem.
In (8) and (16) the shocks live on a probability space . They are measurable and mutually independent over periods (iIndepFun over ), each with law gaussianReal 0 (σ²). The system equations hold for every outcome, and the initial inventory is a constant. "Normally distributed with mean and standard deviation " is the law equality P.map (y t) = gaussianReal m (s²). A statement only about the variance would be weaker than the paper's claim and does not count. The critical-fractile theorem adds and ; without them the inventory is constant and the claim fails.
Contributions are welcome on the finite Gaussian-sum lemma, which is independent of this paper, and on any milestone in any order.
A non-interactive zero-knowledge (NIZK) proof lets a prover convince a verifier that a statement is true by sending a single message, computed from a common reference string that both parties share, without revealing anything beyond the truth of the statement. NIZK proofs were introduced by Blum, Feldman and Micali (STOC 1988) and are a building block of chosen-ciphertext secure encryption, signatures and secure multi-party computation. For a long time every NIZK proof for all of NP was zero-knowledge only computationally: a simulator produced proofs that no efficient adversary could tell apart from real ones.
Groth, Ostrovsky and Sahai (J. ACM 59(3), 2012; conference versions at Eurocrypt 2006 and Crypto 2006) gave the first NIZK argument for all of NP whose zero-knowledge is perfect: real and simulated proofs have exactly the same distribution, so even an unbounded adversary learns nothing. The construction is the Circuit SAT proof of their Figure 3, run on a perfectly hiding key of a homomorphic proof commitment scheme. Its zero-knowledge is Lemma 8 of the paper, and it is the zero-knowledge half of their Theorem 11.
A homomorphic proof commitment scheme has a message space (a finite cyclic group with generator , here ), a randomizer space and a commitment space , all finite abelian groups, and a commitment function . A hiding key generator outputs a commitment key together with a trapdoor . The scheme is assumed to have:
A NAND circuit on wires is a list of gates and an output wire ; a witness satisfies it, , if for every gate and . The prover of Figure 3, with , commits to every wire, with , proves that each commitment contains or , and for each gate proves that contains or .
The simulator is , returning and , and , which commits to on every wire except the output wire, and makes all the 0/1 proofs from openings it knows or obtains with the trapdoor. In the zero-knowledge game an adaptive adversary reads , submits pairs to an oracle one at a time, sees each answer before choosing the next, and outputs a bit. The real oracle answers with , the simulation oracle with ; both answer failure when .
For every adaptive adversary ,
where is restricted to its first output.
Lemma 8 makes the Circuit SAT argument of Section 7 the first perfect NIZK argument for every language in NP. Combined with the computational indistinguishability of binding and hiding keys it also gives the computational zero-knowledge of the proof of Figure 3 (Theorem 6), and it is the template for the perfect zero-knowledge of the universally composable NIZK of the paper's Section 8. The same simulation pattern, commit to everywhere and use the trapdoor where an opening is needed, recurs in later pairing-based proof systems such as Groth–Sahai proofs.
The result is proved in the paper; to our knowledge it has not been machine-checked. A formal proof fixes the simulator completely, including the cases the paper leaves to the reader, and makes the adaptive multi-query argument explicit: the paper's proof treats one proof at a time and does not spell out why answering many adaptively chosen queries preserves equality of distributions.
The real and simulated proofs never use the same randomizers, so the proof cannot compare outputs value by value; it must compare laws. Two gaps in the printed argument need to be closed. First, witness indistinguishability is assumed only for one opening to against one opening to , while comparing a simulated gate proof with a real one compares two openings that may carry the same message; the trapdoor supplies the missing intermediate opening. Second, the printed gate recipe gives the gate commitment the message only when no input of the gate is the output wire; when the output wire is an input, the message is or , and has no 0/1 opening, so the simulator must open the gate commitment itself with the trapdoor. The adaptive adversary adds a third point: equality of laws must survive an arbitrary interaction in which later queries depend on earlier answers.
ZMod N with (the paper describes Figure 3 for order at least 4, p. 14); and are finite nonempty types, a commutative group. Key generators and the 0/1 prover's randomness are probability mass functions; the coins are uniform.A non-interactive zero-knowledge (NIZK) proof lets a prover convince a verifier that a statement is true by sending a single message, without revealing why it is true. NIZK proofs are a basic building block of public-key cryptography: chosen-ciphertext secure encryption, signature schemes and secure multi-party computation all use them. Groth, Ostrovsky and Sahai, New Techniques for Noninteractive Zero-Knowledge (J. ACM 59(3), 2012; conference versions at Eurocrypt 2006 and Crypto 2006), built the first NIZK proofs for all of NP that are perfectly sound and the first NIZK arguments that are perfectly zero-knowledge, using bilinear groups.
The construction rests on a single primitive, the homomorphic proof commitment: a commitment scheme with two kinds of keys (perfectly binding and perfectly hiding) together with a short non-interactive proof that a commitment contains or . Section 4 of the paper instantiates this primitive in a bilinear group of composite order , building on the encryption scheme of Boneh, Goh and Nissim (TCC 2005); Section 5 gives a second instantiation in prime-order groups. Theorem 2 states that the composite-order scheme of Figure 1 has all the required properties. This mission formalizes the part of Theorem 2 that is an exact mathematical statement.
Timeline: Boneh, Goh and Nissim (2005) introduced the subgroup decision assumption and the encryption in groups of order . Groth, Ostrovsky and Sahai (Eurocrypt 2006) used it for perfect NIZK; the simple 0/1 proof used in Figure 1 is due to an observation of Boyen and Waters (Eurocrypt 2006), as the paper's footnote 7 records. The journal version (2012) presents both instantiations through the abstract notion of a homomorphic proof commitment.
A BGN bilinear group is a tuple where are primes, and are finite commutative groups of order , is bilinear ( for all , ), generates , and generates .
The commitment key is for an element of one of two kinds:
The commitment to a message with randomizer is . The trapdoor opening is . The 0/1 proof for a commitment is , and the verifier accepts when . The extractor computes and searches for with .
For every BGN bilinear group, the scheme above satisfies:
with binding, soundness and extractability on binding keys, and trapdoor opening and witness indistinguishability on hiding keys.
The milestones follow the proof of Theorem 2 (p. 9) and Figure 1 (p. 10): the homomorphic property; perfect binding; the extraction identity ; the trapdoor identity and the uniqueness of openings on a hiding key; the completeness display ; the decomposition of every element as on a binding key; the step " of order or implies or "; perfect soundness; and the uniqueness of the proof on a hiding key, which gives witness indistinguishability.
Theorem 2 is one of the two instantiations on which every exact result of the paper rests. Plugged into the Circuit-SAT construction of Section 6, the binding-key properties give a perfectly sound NIZK proof and a perfect proof of knowledge for every NP relation, and the hiding-key properties give a perfect zero-knowledge NIZK argument. The same composite-order techniques underlie later pairing-based proof systems, notably the Groth–Sahai proofs.
The paper's proof is about one page of group computations and has, as far as the planning of this series found, no machine-checked counterpart. The mission produces a reusable model of composite-order bilinear groups and of the BGN commitment, and checks details the paper leaves implicit: the message space versus exponents taken modulo , the role of the non-degeneracy of , and the order arguments behind soundness.
Each property is elementary on its own, but soundness is not a plain computation: the verifier only sees and , and the conclusion asks for an opening of with message in from a single pairing equation. An argument that only manipulates the equation symbolically cannot reach it; the statement depends on the orders of elements in , on generating (with a degenerate pairing soundness is false), and on and being distinct primes. A second subtlety is that a message is only determined modulo by a commitment under a binding key, while the conclusion asks for a message that is exactly or in .
Fintype.card = p * q; is a homomorphism G →* G →* GT, which is exactly bilinearity; generates and generates (both as hypotheses of the structure BGNSetup).ZMod n; is to the representative of in . The paper's message space is , but is not well defined for in a group of order ; binding and extraction therefore compare messages modulo .A prophet inequality compares two players facing the same random sequence of rewards . The gambler sees the values one at a time and must decide, as each value arrives, whether to stop and collect it; a value passed over is lost. The prophet knows the whole sequence in advance and simply takes its maximum. In 1978 Krengel, Sucheston and Garling showed that when the are independent, non-negative and , the gambler has a stopping rule with
and that the factor cannot be improved. This inequality, labelled (1) in Kleinberg and Weinberg's Matroid Prophet Inequalities (arXiv:1201.4764, STOC 2012), is the starting point of optimal stopping theory's prophet inequalities and, more recently, of a large literature in online algorithms and algorithmic mechanism design, where it is the reason that a single posted price can extract a constant fraction of the optimal welfare or revenue.
Timeline.
This mission formalizes that §3.1 result.
Let be a probability space and . Let be real random variables on that are independent (as a family), non-negative, and such that the prophet's value has finite expectation. Define
The single-threshold rule observes in order and stops at the first time with , collecting . If no reaches , the rule accepts nothing and collects . Write for the amount collected; it equals on the event , which has probability , and off it.
In Lean the variables are X : Fin n → Ω → ℝ with [NeZero n]; is maxX X, is thr P X, is stopProb P X, and is reward P X, all in the namespace MatroidProphetKW.RankOne.
This is inequality (1) for an explicit rule, which is stronger than (1)'s existence statement. The constant is sharp, so the goal is stated with it.
The result. A threshold that depends on the distributions only through one number, , already matches the optimal worst-case guarantee of the best stopping rule. Because it is a single price, the rule translates directly into a posted-price mechanism: a seller who posts the price to arriving buyers obtains half of the expected maximum value. The same accounting, in which accepted value is charged against the threshold and rejected value against the probability of having accepted nothing, is what Kleinberg and Weinberg generalize to matroids (missions 1 and 2 of this series).
Formalizing it. The result is proved and classical; the work here is to formalize its known proof. No machine-checked proof of the factor-2 prophet inequality is in Mathlib, and none was found among the platform's published theorems in October 2026. A completed development provides the inequality itself, the tail comparisons, and the layer-cake bookkeeping for a stopped reward, all of which are reusable for other single-threshold prophet inequalities (Samuel-Cahn's median rule, -choice and posted-price variants).
The expected reward of the rule is not a function of the marginals of the individual alone in an obvious way: the event that the rule is still running when arrives depends on , and the reward is at a random index. The natural first attempt, comparing and pointwise, fails, since on a given outcome the rule may stop early at a value just above while the maximum comes later. The comparison has to be made between distributions, at each level , and it has to use independence to decouple "nothing accepted before time " from "". The rest is measure-theoretic bookkeeping that is routine on paper and not routine in Lean: expressing expectations of non-negative variables as integrals of tail probabilities, splitting them at , and keeping track of integrability.
Ω with a MeasurableSpace, P : Measure Ω with [IsProbabilityMeasure P].X : Fin n → Ω → ℝ, [NeZero n]; each X i measurable; iIndepFun X P (mutual independence); 0 ≤ X i ω for all i, ω; Integrable (maxX X) P, which is the paper's .Finset.sup' over the nonempty index set; no junk supremum.∫ ω, … ∂P) and Measure.real probabilities. Tail integrals are Lebesgue integrals of over and .The threshold is a definition, , not a free parameter constrained by hypotheses; a formalization in which is arbitrary and the upper-tail bound is assumed would make the goal a rearrangement of its hypotheses, and is ruled out.
Infrastructure that a complete development needs, and that is welcome as separate contributions: the layer-cake formula for non-negative integrable split at a level (Mathlib has the unsplit form, MeasureTheory.integral_eq_integral_meas_lt); measurability and integrability of the stopped reward (it is dominated by ); and the probability of the event "the first values are below and " as a product under iIndepFun.
Transient stability asks whether a power grid, after a large disturbance such as a fault or a line trip, returns to synchronous operation in which all generators rotate at a common frequency. The classical approach builds energy functions for the swing equations and estimates regions of attraction numerically; it gives no closed-form test relating synchronization to the network's parameters, and it handles transfer conductances (losses) only when they are "sufficiently small" without saying how small.
Dörfler and Bullo (arXiv:0910.5673v4; SIAM J. Control Optim. 50(3), 2012) observe that, for strongly overdamped generators, the network-reduced swing equations behave like a first-order non-uniform Kuramoto model, and they give purely algebraic conditions under which this model synchronizes. The same model is a generalization of the classical Kuramoto model of coupled oscillators, studied in physics, neuroscience and control, with heterogeneous time constants, asymmetric effective coupling and phase shifts. This mission formalizes the first of the paper's two synchronization conditions, Theorem V.3, which is also statements 1)–2) of the paper's main result, Theorem III.2.
There are oscillators with phases . Each has a time constant and a natural frequency ; each pair has a coupling weight and a phase shift , with . The non-uniform Kuramoto model is
The phases live on the torus. For an arc length , the set consists of configurations whose phases all lie in the interior of some arc of length , and is its closure (with the synchronized configurations). A set is positively invariant if every solution starting in it stays in it. A solution achieves exponential frequency synchronization if all frequencies converge exponentially fast to a common value .
The condition of the theorem compares two numbers built from the parameters, with :
is the weakest lossless coupling of an oscillator to the network; measures the spread of natural frequencies and the losses. When , put , and .
If is complete ( for ) and
then (1) is positively invariant for every , and every solution starting in eventually stays in for each ; (2) every solution starting in achieves exponential frequency synchronization to some , and when the solution starts in .
The milestones follow the paper's proof. Theorem V.1 is a frequency-synchronization theorem for phase-cohesive oscillators under a globally reachable node, with the explicit rate
when and . Its supporting steps are the frequency dynamics (20) and a dihedral-angle bound. The phase-cohesiveness argument of Theorem V.3 is split into a trigonometric lower bound, a pointwise bound on the growth rate of the arc containing all phases, the characterization of by inequality (30), positive invariance, and the entry into .
The theorem turns synchronization of a heterogeneous, lossy oscillator network into one inequality among explicit parameters. For the classical Kuramoto model it specializes to (Remark V.4), which improved the sufficient conditions known at the time. For power networks it gives, through Theorem III.2, a computable sufficient condition for transient stability when generator inertia is small relative to damping.
To our knowledge none of these results has a machine-checked proof. The development needs ODE comparison arguments for a non-smooth Lyapunov function (the arc length) and an exponential convergence theorem for time-varying consensus. Both are general tools that are not in Mathlib and would be reusable for other consensus and synchronization results. The mission also records two clauses of the printed theorem that are false as stated, with counterexamples, and states the corrected theorem.
The arc length is only Lipschitz, so its decrease along solutions must be argued through Dini derivatives and a comparison lemma rather than by differentiation. Positive invariance at the boundary holds with a non-strict inequality, so a naive "strictly decreasing at the boundary" argument does not apply there. Frequency synchronization rests on a contraction property of linear consensus with time-varying, state-dependent weights. The weights are positive only after the phases have entered . Before that the frequency range can expand, which is why the range clause of the printed theorem fails for initial arcs longer than .
Phases are represented by real lifts . means that all pairwise differences of the lift are at most , and that they are strictly less than . Conclusions are stated for the same continuous lift, which is at least as strong as membership on the torus. A solution is a map with derivative (one-sided at ) equal to the right-hand side of (8) for all . Every statement quantifies over all such solutions. always denotes the vector field along the solution. Minima and maxima over are over ordered pairs, and is assumed so that they exist. The conventions are explicit hypotheses. and are defined by , and a milestone certifies that they are the unique solutions in the printed ranges. is the second-smallest eigenvalue of the symmetric Laplacian.
The source is the arXiv preprint v4 of the SICON article, cited with its own page and theorem numbers. Three corrections relative to the printed text are made and disclosed in the items:
No statement is trivially satisfiable. The solution predicate holds for actual solutions (for example the synchronous solution), condition (26) is satisfiable (take and ), the exponential rate is required to be strictly positive, and are specific numbers rather than existential witnesses.
Contributions are welcome on all milestones. The trigonometric bound, the dihedral-angle bound and the characterization are elementary. The comparison lemma for Dini derivatives and the consensus contraction theorem are reusable infrastructure.
A spectral sparsifier of a graph is a much sparser weighted graph whose Laplacian quadratic form is within a factor of the original on every vector. Spielman and Teng introduced the notion in Spectral Sparsification of Graphs as a strengthening of the cut sparsifiers of Benczúr and Karger: a spectral sparsifier preserves every cut, and in addition every quantity determined by the Laplacian quadratic form, such as effective resistances, eigenvalues and the behaviour of random walks. Sparsifiers are the reason linear systems in graph Laplacians can be solved in nearly linear time: one preconditions with a sparsifier and solves the sparse system instead (Spielman–Teng, arXiv:cs/0607105).
The construction in the paper has two halves: decompose the graph into pieces of high conductance, then sparsify each piece by random sampling. This mission is the second half, Theorem 6.1 of §6: in a graph whose normalized Laplacian has a spectral gap, keeping each edge independently with probability inversely proportional to the smaller degree of its endpoints, and reweighting kept edges by the inverse probability, produces a -spectral approximation with few edges, with high probability.
Timeline. Benczúr and Karger (1996) sampled edges with probabilities depending on edge strength and preserved cuts. Achlioptas and McSherry (2001) analysed random sampling of matrices through the random-matrix norm bound of Füredi and Komlós (1981), corrected by Vu (2007). Spielman and Teng (arXiv 2008, SIAM J. Comput. 2011) proved Theorem 6.1 by refining the Füredi–Komlós trace method for downsampling graphs that may already be sparse. Spielman and Srivastava (2008) later replaced conductance-based probabilities by effective resistances.
Let be an unweighted graph on a finite vertex set , , with degrees , adjacency matrix , diagonal degree matrix and Laplacian . Its quadratic form is
A weighted graph on with weights has the form . is a -approximation of if for all
When every degree is positive, the normalized Laplacian is ; its eigenvalues lie in , and a lower bound on its smallest non-zero eigenvalue measures how well connected each component of is (by Cheeger's inequality it is equivalent to high conductance up to squaring).
Sampling. For a parameter , edge is assigned
each edge is kept independently with probability , and a kept edge gets weight . The sampled adjacency matrix then has ; is the diagonal matrix of weighted degrees of the sampled graph.
The procedure. In Theorem 6.1 sampling is applied only to the edges of an induced subgraph , ; the other edges are kept with weight 1. sets and uses the degrees of ; the paper takes .
For , without isolated vertices whose smallest non-zero normalized Laplacian eigenvalue is at least , , and an even integer : with probability at least , simultaneously
Theorem 6.1 is the sampling engine of the first nearly-linear-time spectral sparsification algorithm: combined with a decomposition of an arbitrary graph into high-conductance pieces (§7–§10 of the paper), it yields sparsifiers with edges, which in turn give the nearly-linear-time Laplacian solvers that underlie fast algorithms for electrical flows, maximum flow approximation and graph partitioning. Lemma 6.3 is a self-contained random-matrix result: a norm bound for the normalized deviation of a downsampled graph that does not assume the original graph is dense.
The result is proved in the paper. As far as is known, none of it is formalized in Lean or Mathlib: Mathlib has the graph Laplacian (SimpleGraph.lapMatrix) and the spectral theorem for Hermitian matrices, but no normalized Laplacian, no spectral approximation and no trace-method bounds for random matrices. A complete formalization would be the first machine-checked proof of a spectral sparsification theorem, and the milestones (the trace-method moment bound, Chernoff for weighted two-point sums) are reusable on their own.
The obvious argument — bound each entry of and apply a matrix concentration inequality — needs either a matrix Chernoff bound (not in the paper, and not in Mathlib) or the Füredi–Komlós trace method, which assumes every edge can appear and so fails when the graph is already sparse: a vertex of small degree has no room for its entries to average out. The paper's sampling probabilities keep every edge at a vertex of degree at most , and the trace computation has to exploit exactly this through the moment bound of Lemma 6.6 and a combinatorial count of closed walks. Formally, the obstacles are the walk-counting argument of Lemma 6.4, the passage from a trace bound to an eigenvalue bound for the non-symmetric (similar to a symmetric matrix), and Lemma 6.2's restriction to the orthogonal complement of the kernel, which must handle disconnected in the goal.
V; graphs are SimpleGraph V with decidable adjacency; weighted graphs are weight functions V → V → ℝ (symmetric, nonnegative, loopless). The quadratic form is ; a -approximation keeps both inequalities of (2).In the job shop problem, jobs are sequences of operations, each to be processed on a given machine for a given time, and the goal is a schedule of minimum makespan (the time at which the last job finishes). Two numbers bound the optimum from below: the longest job and the most loaded machine. Their maximum is written . The best approximation algorithms for job shops have a performance guarantee polylogarithmic in (Shmoys, Stein and Wein 1994; Goldberg, Paterson, Srinivasan and Sweedyk 2001). Whether flow shops and job shops admit a constant-factor approximation was Open Problem 7 of Schuurman and Woeginger (1999).
Mastrolilli and Svensson (J. ACM 58(5), 2011) answered it negatively for the generalized flow shop. Their Theorem 1.2 states that for all sufficiently large constants it is NP-hard to distinguish generalized flow shop instances with a schedule of makespan from instances in which no schedule finishes more than half of the jobs within . The proof is a gap-preserving reduction from graph colouring. This mission formalizes the combinatorial heart of that reduction.
Timeline. Shmoys, Stein and Wein (1994) gave an -approximation for job shops, improved by a factor by Goldberg et al. (2001). Williamson et al. (1997) proved that approximating flow shops with unit operations within a ratio better than is NP-hard. Feige and Scheideler (2002) gave acyclic job shop instances with optimum and asked whether flow shops admit a much better upper bound than . Khot (2001) proved the colouring hardness this reduction starts from. Mastrolilli and Svensson (FOCS 2008; J. ACM 2011) proved Theorem 1.2 and its job shop variants.
A generalized flow shop (flow shop with jumps) is a job shop with a fixed linear order on the machines in which every job visits its machines in increasing order but may skip machines. Operations may have length . A zero-length operation still occupies its machine for an instant, so it cannot be processed strictly inside another operation on the same machine.
Let be a simple graph with vertices whose vertices are partitioned into independent sets . Vertex has frequency . For an integer write . The instance has groups of machines, each with one machine per vertex. The machines are ordered by group first and, within a group, by decreasing frequency. A vertex of frequency owns groups of identical jobs. The job has a long-operation of length on each of the machines , where . It also has a short-operation of length on every machine of every neighbour of , in every group. A long-operation is good if the next long-operation of the same job starts at most time units after it ends. is the set of first halves of the good long-operations on , and is the time they cover.
is the chromatic number of and the size of its largest independent set.
For every graph with a proper colouring into classes and every integer , with :
Remark 3.6 (lengths, loads, operation count), Claim 3.8 (an independent set's jobs fit in ), Lemma 3.7 (completeness), Lemma 3.10 (most long-operations are good), Lemma 3.11 (adjacent vertices have disjoint -intervals), Lemma 3.12 (one group carries of first-half time), and Lemma 3.9 (soundness: an independent set of size ).
The result. Together with Khot's colouring hardness, the gap shows that no polynomial-time algorithm approximates the generalized flow shop within any constant factor unless P = NP, and rules out an -approximation under a stronger complexity assumption (Theorem 1.3). It also shows that on the no-instances of the reduction every schedule has makespan greater than , far above the trivial lower bound . Because soundness bounds the number of jobs finished early, the same reduction also gives hardness for the sum of completion times (footnote 2).
Formalizing it. The paper proves every statement of this mission; none is open. As far as the catalog shows, none has a machine-checked proof. The soundness argument rests on a timing property of zero-length operations: a job of higher frequency must wait for a long-operation of an adjacent lower-frequency job. Such properties are easy to state loosely and easy to get wrong, so a verified proof would be useful. A formal proof would also make explicit the thresholds the paper leaves as "sufficiently large ".
Completeness is constructive and routine once the job and machine indexing is under control. The difficulty is soundness. One might argue directly that jobs of adjacent vertices never overlap in time, but that is false: a schedule may run them in parallel at the cost of delays. The argument controls it only on average. It throws away the jobs that finish late and the long-operations followed by a long delay. It shows that the first halves of the remaining long-operations of adjacent vertices are disjoint in each machine group. Then it finds a moment covered by many such first halves. Each step needs a precise count: of good operations per job, of covered time per group, and of overlap multiplicity at a point. The degenerate conventions (empty colour classes, , the last long-operation of a job) have to be handled throughout.
The instance is the published JobShopLTAS.Core.Instance (machines and jobs Fin (r^{2d} n), real nonnegative processing times, disjunctive machine constraint under which a zero-length operation cannot sit strictly inside another operation on its machine), with its IsFeasibleSchedule and makespan. The graph has vertex set Fin n and the partition into independent sets is a Mathlib proper colouring G.Coloring (Fin d). Frequencies are 1-based, as are group indices. Within a group the paper leaves machines of equal frequency unordered; they are ordered by vertex index. Every job's operation list is its machine set sorted by the global order. is the Lebesgue measure of the union of the intervals.
Explicit readings of the paper's wording:
Not formalized: "NP-hard", "for all sufficiently large ", "in time polynomial in and ", Khot's Theorem 1.7, the choice , , and the randomized Lemma 3.1 behind Theorem 1.3.
A model in which zero-length operations occupy no machine time would make soundness false, and stating soundness only for schedules of an independent set's jobs would make it vacuous. The goal is about every feasible schedule of , built from , in the published model, where zero-length operations do conflict.
A complete development needs counting lemmas for the indexing of jobs and machines, sorting facts for the operation lists, and a measure-theoretic averaging argument (a point covered by many intervals). The averaging argument and the good-operation counting are shared with the flow shop gap of Theorem 1.1 and reusable there. Proofs of any milestone, and sorry-free sanity checks on small instances, are welcome.
Many models in operations management and economics need the demand or valuation distribution to be regular in some way, so that an optimal price, order quantity or contract is unique. Pricing a service to one customer whose valuation has survival function is a typical example. The seller maximizes . The first-order condition is , where is the generalized failure rate and is the ordinary failure rate. When is increasing (the IGFR property, introduced by Lariviere and Porteus 2001), the optimal price is unique and solves .
The best-known regularity class is the class of IFR laws, those with increasing failure rate. Every IFR law has finite moments of all orders (Barlow and Proschan 1965). IGFR laws are a larger class that includes heavy-tailed laws, and Lariviere (2006) identifies exactly which of their moments are finite. The answer is given by one number, the limit of the generalized failure rate. A consequence used in pricing models is that a valuation law with a finite mean has eventually, so the pricing problem has a finite solution.
Let be a nonnegative random variable with distribution function and survival function . Assume has a density . The failure rate is
and the generalized failure rate is . is IGFR if is weakly increasing on . has support , with , if exactly for and for every . For a real , the -th moment is .
The comparison law is the Pareto law with scale and parameter , which has density for . Its generalized failure rate is identically on , and its -th moment is finite exactly when . For a level with , write for conditional on . A random variable is stochastically smaller than if for all real .
In Lean, is its law μ : Measure ℝ, is cdf μ, is survival μ, is failureRate μ φ, is genFailureRate μ φ, and is nthMoment μ n.
Suppose is IGFR with support and , where may be infinite. Then for every real ,
The statement fixes no constants. It covers (all moments finite) and the boundary case (infinite moment).
The two Pareto facts of the §3 preamble come first:
Six claims from the proof follow:
Two consequences stated after the theorem are included as further targets. First, an IGFR law with support and a finite mean has beyond some finite point. Second, a strictly IGFR law with a finite -st moment satisfies the two conditions of Van Mieghem and Dada (1999): has at most one zero, and .
The theorem gives a complete moment criterion for IGFR laws in terms of the single number . Among IGFR laws, finiteness of the mean, the variance or any higher moment can therefore be read off the tail of . One consequence is that a finite mean is enough for the IGFR pricing problem to have a finite solution, which replaces the separate condition " exceeds one at a finite point". The theorem generalizes Lemma 2 of Lariviere and Porteus (2001), and the paper uses it to connect IGFR laws to the Van Mieghem–Dada condition.
The result is proved on paper but has not been formalized. Formalizing it adds three things:
Pareto.lean lacks;The core of the proof is a comparison: a pointwise bound beyond a level becomes a stochastic order against a Pareto tail. This needs the representation , which uses the fundamental theorem of calculus for across the left end of the support, where may have a kink. It also needs to be stated for the conditional law, whose density is a rescaled restriction.
An obvious first attempt is to bound directly by with the given bound on . That bound controls , not , so it says nothing directly. The survival representation is what converts it.
A second obstacle is the boundary case , with finite. A strict margin is no longer available there. It needs the non-strict bound , which follows from monotonicity, and a Pareto law with parameter exactly .
Laws, not random variables. Every statement is about distributions, so is represented by a probability measure μ on ℝ with μ (Set.Iio 0) = 0. In the goal, nonnegativity also follows from the support hypothesis, and the separate hypothesis is kept for uniformity with the other items.
The density version is pinned. and read pointwise, while "Φ has density φ" determines only up to a null set. The predicate IsRegDensity requires and . It also requires to be the right derivative of at every point of and wherever . The exponential law with satisfies all hypotheses of the goal, with .
IGFR is weak monotonicity of on , as printed. On this set , so Lean's convention never enters.
is an extended nonnegative real. The limit hypothesis is Tendsto (fun ξ => ENNReal.ofReal (g ξ)) atTop (𝓝 κ) with κ : ℝ≥0∞. A real-valued would silently drop the case .
Moments are lower Lebesgue integrals ∫⁻ x, ENNReal.ofReal (x ^ n) ∂μ with a real exponent. The Bochner integral would make "finite" automatic, because it returns for a non-integrable function, so it is not used.
Conditioning and Pareto. is Mathlib's ProbabilityTheory.cond μ (Set.Ioi y), always with . The Pareto law is Mathlib's paretoMeasure S k. "Stochastically smaller" is the published definition StochasticOrders.Usual.UsualOrder applied with the identity map.
Trivialization is ruled out. The goal is a full equivalence with a possibly infinite and an infinite-valued moment. It is not the weaker " implies finite", and the hypotheses are jointly satisfiable.
Recorded deviations. The printed bound "" is a slip (it fails for ). Only the finiteness it is used for is formalized. The Pareto moment fact is stated as an equivalence, which contains the printed "only if".
Infrastructure. A complete development needs:
cond and cdf.The survival representation and the failure-rate/Pareto comparisons are reusable for any heavy-tail result stated through hazard rates. Contributions are welcome at every level, including partial results such as the Pareto lemmas alone.
Search engines sell advertising space query by query. Each advertiser states a bid for each keyword and a daily budget; queries arrive one at a time, and each must be assigned to an advertiser immediately, without knowledge of the queries still to come. The revenue-maximizing assignment of the day can only be computed offline. The adwords problem asks how close an online rule can get to it. It generalizes online bipartite matching, for which Karp, Vazirani and Vazirani (KVV 1990) showed that randomized ranking attains ratio , and -matching, for which Kalyanasundaram and Pruhs (KP 2000) showed that the deterministic BALANCE algorithm attains as the budget grows.
Mehta, Saberi, Vazirani and Vazirani (J. ACM 2007) gave a deterministic algorithm for arbitrary bids that weighs each bid by a function of the fraction of budget already spent, and proved that it is -competitive when bids are small compared to budgets. The algorithm and its tradeoff function became the reference point for the online budgeted-allocation literature, including the primal-dual analysis of Buchbinder, Jain and Naor (ESA 2007).
There are bidders, each with budget , and a sequence of queries . Bidder bids for the query at position . An allocation assigns each query to at most one bidder. Bidder 's spend before position is , and is alive while its spend is below . The revenue of is .
Fix an integer and split each budget into equal slabs; a spent fraction lies in slab , and in slab . Given a tradeoff function on slabs, the discrete tradeoff algorithm assigns each arriving query to an alive bidder maximizing
ties broken arbitrarily. Every allocation produced this way, for any tie-breaking, is a run.
The analysis uses the factor-revealing LP : maximize subject to and , written , , , and its dual . Its optimal dual solution is , and Theorem 8's tradeoff function is
For every there is such that for every there is such that, for every instance with bids in , every run of the algorithm with , and every allocation ,
The goal fixes no rate in or : it asserts only that the ratio tends to .
Theorem 8 gives an online algorithm for budgeted allocation with arbitrary bids whose revenue is within a factor of the offline optimum, the best possible ratio even for randomized algorithms (Theorem 9 of the same paper, the second mission of this series). It reduces to BALANCE when all bids are equal, and its tradeoff function in the limit is the function used in later work on online budgeted allocation and display-ad allocation.
The result is proved in the paper; none of it is formalized. The work here is to formalize the proof in a version that holds for actual runs. The paper's argument makes two simplifications with "negligible error": bidders of type spend exactly of their budget, and the offline optimum exhausts every budget. A formal proof must carry the bid size through the slab boundaries and compare with an arbitrary offline allocation. The LP lemmas (Lemmas 3–5) are self-contained statements about one triangular linear program and are reusable for factor-revealing analyses of BALANCE.
The milestones are short: Lemmas 3–5 are finite linear algebra with geometric sums, Lemma 6 is one application of the assignment rule plus monotonicity of spend, and Lemma 7 regroups finite sums. The difficulty is in Theorem 8. The paper's proof chains Lemmas 4, 5 and 7 through the LP , whose right-hand side is computed from the numbers of bidders of each type under the assumption that a bidder of type spends exactly . In an actual run this identity fails: a single bid can straddle a slab boundary, and types are intervals, not points. So the chain does not compose literally, and the natural first attempt, instantiating Lemma 5 with the run's quantities, does not apply. The slab-wise inequalities that do hold, with an error of order , have to replace the equalities, and the comparison with an offline allocation that does not exhaust budgets has to be made through capped revenues.
Bidders are Fin N and query positions Fin M, zero-based; slabs and LP coordinates keep the paper's 1-based ranges, with vectors as functions read on . Budgets are (the paper's standing simplification of §2). Bids are real and nonnegative.
A run is a predicate on the whole allocation: at position , if some bidder is alive the query goes to an alive maximizer of bid , where spends are computed from earlier positions only; the query is unassigned only when all budgets are exhausted. Every tie-breaking rule gives a run, and the goal holds for all of them. is the full bid of the chosen bidder; revenue is capped at the budget.
Conventions the statements commit to:
Trivializing formalizations are ruled out: a run cannot leave a query unassigned while a bidder has budget, so the empty allocation is not a run; no hypothesis of the form "bidders of type spend exactly " or "the optimum exhausts every budget" is imposed, since either would make the goal vacuous on most instances.
All definitions are local to the namespace AdWordsMSVV.Tradeoff. Related platform items analyse a different algorithm: BJNAdAuctions.Basic.* and OnlinePrimalDual.AdAuctions.* formalize the Buchbinder–Jain–Naor primal-dual algorithm, which updates a covering variable multiplicatively and has ratio ; they are not reused. Proofs of any milestone, and lemmas carrying the bid-size error through slab boundaries, are welcome.
Large service systems (call centers, hospital wards, cloud server pools) run with many servers, and for many of them no exact formula describes how the number of busy servers moves over time. Heavy-traffic limits replace such a system by a diffusion process that is easier to analyze. The many-server regime, in which the number of servers and the arrival rate grow together, goes back to Halfin and Whitt (1981) and is the basis of square-root staffing rules in call-center practice.
The simplest many-server model is the queue. Its stationary number in system is Poisson with mean , so the centered and -scaled stationary count is asymptotically normal when . The question here is about the whole process: does the scaled number in system converge, as a random path, to a diffusion? The classical answer, the Ornstein–Uhlenbeck limit, was first established by Iglehart (1965) with Stone's theorem for birth-and-death processes, and was revisited by strong approximation (Mandelbaum, Massey and Reiman 1998) and, for general service times, by Krichagina and Puhalskii (1997).
Pang, Talreja and Whitt (2007) is a tutorial survey that proves this limit, and its finite-waiting-room extension, with martingale methods. The authors present the argument as a template for non-Markovian and network models (Reed 2009; Dai and Tezcan; Gurvich and Whitt). This mission formalizes the result and the steps of the paper's proof.
Fix a service rate . For each , the -th system has arrival rate . Let and be independent Poisson processes of rate , and let be a random initial number of customers, independent of and . The number in system is the -valued process with right-continuous paths having left limits that satisfies, almost surely,
The departure term is a random time change: each of the customers in service completes service at rate . The diffusion-scaled process is , the paper's (3). The space consists of paths on that are right-continuous with left limits, and denotes convergence in distribution.
The limit is the Ornstein–Uhlenbeck (OU) process , driven by a standard Brownian motion , with independent of :
The proof also uses the scaled martingales and , the fluid processes and , and stochastic boundedness. A sequence of real random variables is stochastically bounded if it is tight, and a sequence of processes is stochastically bounded in if is, for every .
If in , with an arbitrary limit law , then
where is the OU process (5) with . The goal fixes no initial distribution and assumes no moment condition on .
Theorem 1.1 describes the transient behavior of a large infinite-server system, not only its stationary law: fluctuations of order around the offered load form a Gaussian Markov process that relaxes at rate . It is the reference case for the Halfin–Whitt regime, whose finite-server version, Theorem 1.2 of the same paper (the queue), is the subject of the companion mission. The milestones are general tools reused well beyond queueing: Gronwall's inequality, the Lipschitz integral map, the Poisson FCLT, stochastic boundedness via Lenglart's inequality, and the fluid limit from stochastic boundedness.
The theorem is proved and classical; no machine-checked proof of it, or of the milestones below, is known. No formal library currently has the Poisson functional central limit theorem in , compensators of counting processes, or random time changes of martingales. Formalizing the paper's proof would produce these, plus a template for the martingale method of heavy-traffic analysis. Alternative proofs, such as the paper's §4.3 route without martingales, are equally welcome as solutions.
Equation (12) is a fixed-point equation: appears inside the argument of . The integral map of Theorem 4.1 is continuous, so the obvious argument is to apply the continuous-mapping theorem to the martingale representation. That reduces the goal to the joint convergence of . But is a Poisson martingale evaluated at the random time , and its limit is identified only after the fluid limit is known. The fluid limit is itself a statement about the whole sequence , and it needs a separate argument, either Gronwall at fluid scale or stochastic boundedness. Lemma 3.2 requires optional stopping at the continuum of stopping times , and the moment conditions (22) must be checked through the crude bound. Removing needs a truncation of the initial conditions (§6.3).
CouplingConverges): a Skorokhod representation with almost-sure uniform convergence on compact intervals. Convergence to a deterministic path is uniform convergence on compacts in probability (UocInProb). is stated with bounded continuous test functions.Type.A formalization that fixes , assumes converges almost surely, adds to the goal, or replaces convergence in by convergence of finite-dimensional distributions proves a weaker theorem and does not close the goal.
Contributions are welcome at every level. The Poisson FCLT, Lenglart's inequality and the composition map are reusable library results, independent of queueing.