Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
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.
Periodic-review inventory models with a fixed ordering cost are the setting in which the policy is optimal: when the stock falls below a reorder point , order up to a level , otherwise order nothing. Scarf (1960) proved this for independent demands over a finite horizon by introducing -convexity, and Iglehart (1963) extended it to the discounted infinite horizon. In practice the demand distribution changes with an exogenous environment: the economy, the season, the stage of a product's life cycle. Song and Zipkin (Oper. Res. 41(2), 1993) modelled this environment as a Markov chain of demand states in continuous time with Poisson demand.
Sethi and Cheng (Oper. Res. 45(6), 1997) treat the discrete-time version with general demand densities, nonstationary costs and convex surplus costs of linear growth. The companion mission (I) covers their finite-horizon result, Theorem 4.1. This mission covers the nonstationary discounted infinite-horizon result, Theorem 6.2, together with the existence theory (Theorem 6.1, proved in the paper's Appendix) on which it rests.
Demand states form the finite set and follow a Markov chain with transition matrix . In period the demand has the conditional density given , with mean at most . Orders are placed at the start of a period and delivered at once, and unmet demand is backlogged, so the surplus evolves by (2.4). Ordering costs with (2.1), where for and otherwise. The surplus cost is convex and nonnegative, vanishes at , and satisfies (2.2).
An admissible policy chooses each order as a measurable function of the past demand states and demands. With a discount factor , the objective from period , state and surplus is
and the value function is . With (3.1), the dynamic programming equations are
The truncations keep the first periods of (6.1) (6.3), their values are (6.4), and is the cost of never ordering (6.6). The function classes are (nonnegative pointwise limits of continuous functions), (those of linear growth) and (those also uniformly continuous in ). A function is -convex if for all , (4.3). Assumption (4.1) asks , and (4.2) asks as .
Under (2.1), (2.2), (4.1), (4.2) and , there are in such that
attains the infimum in (6.2) at every , and its feedback policy, started at any period and surplus , has cost : it is optimal among all history-dependent policies.
The structural lemma behind the step from -convexity to the form, Proposition 4.2 of the paper (an extension of Bertsekas' lemma to lower semicontinuous functions coercive only at , with possibly infinite , ), is posed in the companion finite-horizon mission and is not repeated here.
Theorem 6.2 says that the classical structure survives two generalizations at once: demand driven by a Markov environment, and nonstationary data over an infinite horizon. The two levels may depend on the period and on the current demand state, so only numbers per period describe an optimal policy, and with cyclic demand only pairs are needed (Corollary 7.1 of the paper). Theorem 6.1 is a self-contained existence result for a positive-cost, unbounded-state dynamic program: value iteration from zero converges to the value function, which solves the optimality equation, and any measurable minimizer is optimal among history-dependent policies.
The results are proved in the paper, with the finite-horizon existence theory delegated to Beyer, Sethi and Taksar (1998). No machine-checked proof of any of them is known. The platform has -convexity (BertsekasKConvex) and the structure lemma of Bertsekas for continuous functions coercive at both ends; it has no discounted infinite-horizon theorem with Markov-modulated demand. The related posed items SongZipkinFluct.FixedCost.theorem5e_theorem6 and theorem5ab concern the Song–Zipkin model (continuous time, Poisson demand, integer levels, stationary data), a different model.
The obvious argument is "the finite-horizon value functions are -convex, so their limit is, and a minimizer of a -convex optimality equation is ". Three steps of it fail as stated.
First, the limit of value iteration need not be the value function, nor solve (6.2), in a positive-cost problem with unbounded actions: exchanging with requires the minimizers of the truncated problems to stay in a compact set uniformly in , and that bound is where the coercivity assumption (4.2) enters. Second, optimality against history-dependent policies, not only Markov ones, requires a verification argument along histories of states and demands. Third, the functions may be unbounded below, in which case the reorder level is and the order-up-to level does not exist; the goal allows this case.
The Lean development (namespace SethiChengSS.Infinite) commits to the following.
Fin L; periods are natural numbers with the paper's base .Pins. The paper prints ; the mission assumes , since is infinite at and the Appendix divides by . Theorem 6.2 is printed without (4.1), which its proof uses through the induction of Section 4; (4.1) is assumed for every period. Theorem 6.1 is printed under (2.1)–(2.2) only, but attainment in (6.2) can fail without coercivity and the Appendix bound (A.3) divides by ; (4.2) is added to (6.9), (6.10) and to the attainment clause of (6.5). "In class " for the sequence is read with one growth constant for all periods. The boundary condition "" of (6.5) is read as , as the next sentence of the paper states.
The goal cannot be met by a degenerate encoding: the value function is the infimum over all admissible history-dependent policies (not the solution of (6.2) by definition), the demand data must be genuine probability densities with bounded mean, and the levels may not be .
A complete development needs: monotone convergence for the path-measure costs, measurable selection of minimizers, the -convexity closure properties (Proposition 4.1 of the paper; several are proved on the platform as BertsekasDP.kconvex_*), and Proposition 4.2. The model file and the infinite-horizon verification argument are reusable for other Markov-modulated inventory models. Contributions toward any milestone, or toward general lemmas on positive-cost dynamic programs, 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.
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 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.
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.
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 why the statement is true. NIZK proofs were introduced by Blum, Feldman and Micali (STOC 1988). They are a basic component of chosen-ciphertext secure encryption, signature schemes and secure multi-party computation.
Groth, Ostrovsky and Sahai (J. ACM 59(3), 2012; conference versions at EUROCRYPT 2006 and CRYPTO 2006) built NIZK proofs for all of NP from bilinear groups. The construction rests on one abstraction, the homomorphic proof commitment, and one protocol, the NIZK proof for Circuit SAT of their Figure 3. Theorem 6 says that the Figure 3 protocol works for every homomorphic proof commitment. This mission formalizes the part of Theorem 6 that holds exactly, with no computational assumption.
A homomorphic proof commitment scheme (Section 3) has a message space , a finite cyclic group with generator . It also has a randomizer space and a commitment space , both finite abelian groups. It comes with algorithms :
The exact properties used here are the following. The homomorphic property is on keys of either mode. Perfect binding says that on binding keys no commitment has openings to two different messages. Perfect completeness of the 0/1 proof says that honest proofs for are always accepted, on keys of either mode. Perfect soundness of the 0/1 proof says that on binding keys an accepted proof implies for some . Perfect extractability says that on binding keys for .
A NAND circuit on wires is a list of gates , with inputs and output , and an output wire . An assignment satisfies it, , when for every gate and .
The protocol of Figure 3 takes with . The prover commits to every wire, , with . It proves with that each contains or . For each gate it proves that contains or , using message and randomizer . The verifier checks and every 0/1 proof.
If and the scheme has the homomorphic property, perfect binding, and perfectly complete and perfectly sound 0/1 proofs, then
The theorem holds for every scheme with these properties, with no assumption on how the scheme is built.
Theorem 6 is the step from a commitment primitive to NIZK proofs for an NP-complete language. With the subgroup-decision commitment of Section 4 or the decisional-linear commitment of Section 5 it gives Corollaries 9 and 10: perfectly sound NIZK proofs for Circuit SAT with proofs of size . When the common reference string is instead a hiding key, the same protocol becomes the perfect NIZK argument of Theorem 11. Its completeness clause is the hiding-key half of the completeness formalized here.
The result is proved in the paper. Lemma 5 and the soundness of the circuit protocol are left to the reader there or proved in three sentences. No machine-checked proof of this theorem, or of any commitment-based NIZK, was found in Mathlib or in the public Lean libraries searched. This mission states its exact content against an abstract scheme interface. The same interface can then be instantiated by machine-checked versions of the concrete commitments, which are the third and fourth missions of this series.
The argument is short, so the difficulty lies in the bookkeeping. On a binding key the verifier only learns that each commitment opens to some bit. Perfect binding is what identifies the message a gate proof certifies with , which in turn identifies it with the wire bits. Lemma 5 must then be checked in rather than in the integers, where , and must be shown to differ from and . This is exactly where enters: for the all-zero assignment passes every gate check, since . The output wire is handled by the literal check together with binding. Completeness needs the prover's convention to be used consistently in the gate proofs.
ZMod N. A finite cyclic group with a chosen generator is this group, and every theorem that needs it assumes 4 ≤ N, the paper's restriction on p. 14.AddCommGroup and a finite CommGroup. Key generators are PMFs. takes its randomness as an argument.Prop, quantified over the support of the relevant generator. The paper's "for all adversaries, " (or ) is equivalent for unbounded adversaries.Fin n with an output wire. No acyclicity is required, so the statements cover every system of NAND constraints.Dropped, because they are computational:
Perfect zero-knowledge on hiding keys (Lemma 8) is the second mission of this series. The definitions of this mission (the scheme interface, NAND circuits, the protocol) are reusable by any formalization of commitment-based proof systems. Proofs of the milestones are welcome in any order.
Khot, Kindler, Mossel and O'Donnell, Optimal Inapproximability Results for MAX-CUT and Other 2-Variable CSPs? (SIAM J. Comput. 37(1), 2007), prove that, assuming the Unique Games Conjecture, the Goemans–Williamson approximation ratio for MAX-CUT is optimal, and they extend the method to MAX-q-CUT and to Γ-MAX-2LIN(q). For the q-ary problems the key analytic input is the theorem of Mossel, O'Donnell and Oleszkiewicz (arXiv:math/0503503), the MOO theorem. It bounds the noise stability of a low-influence function with mean µ by a Gaussian quantity, the correlated Gaussian orthant probability Λ_ρ(µ): the probability that two ρ-correlated standard Gaussians both exceed the threshold t at which a single one has tail mass µ.
The hardness bounds of the paper for Γ-MAX-2LIN(q) are stated in terms of Λ_ρ(1/q). They are explicit only after Λ_ρ(µ) is estimated. Proposition 6.1 of the paper gives such an estimate in closed form, by slightly improving a bound from the proof of Lemma 11.1 of de Klerk, Pasechnik and Warners (Approximate graph colouring and MAX-k-CUT algorithms based on the theta function, J. Combin. Optim., 2004). The same quantity at µ = 1/2 is Sheppard's orthant probability (Phil. Trans. R. Soc. A 192, 1899), the source of the arccos formulas used throughout the MAX-CUT part of the paper.
This mission formalizes Proposition 6.1 and the steps of its printed proof.
Let φ be the standard Gaussian density and N the Gaussian tail probability function:
So N(x) = Pr[X ≥ x] for a standard Gaussian X. N is strictly decreasing from 1 to 0, and N(0) = 1/2.
Let X and Y be independent standard Gaussian random variables. For ρ ∈ [0, 1] put
Then (X, X′) is a centred normal pair with unit variances and covariance ρ, the pair of Definition 8 of the paper. For 0 < µ < 1 let t be the unique real number with Pr[X ≥ t] = µ, and define
The threshold t is positive exactly when µ < 1/2. Λ_ρ(µ) is the noise stability, in Gaussian space, of the indicator of a half-line of measure µ.
The proof uses two exponents. For u, v ∈ ℝ, with ρ < 1 and t > 0,
In Lean these are phi, tailN, orthantProb ρ t, Lambda ρ μ, gExp ρ t u v and hExp ρ t u v in the namespace OptInapprox.Orthant.
For any 0 ≤ µ < 1/2, let t > 0 be the number with N(t) = µ. Then for all 0 ≤ ρ ≤ 1,
The endpoint ρ = 1 is part of the goal. There X′ = X, Λ₁(µ) = µ, and (4) becomes the classical Mills-ratio inequality N(t) ≤ φ(t)/t.
Proposition 6.1 makes the MOO theorem quantitative for thresholds. With the lower bound of milestone 4 it determines Λ_ρ(µ) up to the factor 1 + ρ, and up to 1 + o(1) as µ → 0, since φ(t)/t ∼ N(t) as t → ∞ (Corollary 10, part 1). Through Corollary 10 it yields the asymptotics of qΛ_ρ(1/q) used in the paper's hardness results for MAX-q-CUT and Γ-MAX-2LIN(q). These quantities also appear in later work on q-ary noise stability and on the approximability of 2-CSPs.
The proposition is proved in the paper; nothing here is open. Mathlib (at the pinned revision) contains no proof of it, of the bivariate-normal integral representation (18), or of the Mills-ratio inequality N(t) ≤ φ(t)/t. On the platform, Mills' inequality appears only as an open statement in the two-sided form Pr[|X| > z] ≤ √(2/π)·e^{−z²/2}/z (KLTNuclear.Lasso.gaussian_tail), and there is no item for orthant probabilities. A complete development provides:
Each of these is reusable for Gaussian tail and orthant estimates.
The inequality itself is elementary once (18) and (20) are available. The work lies in the two integral identities and in their measure-theoretic glue.
For (18), the orthant probability is defined as a measure of a set under the product of two one-dimensional Gaussian laws. Writing it as a double integral of the bivariate density is a linear change of variables with Jacobian √(1 − ρ²). The shift and scaling by t then has Jacobian 1/t², and the quadratic form has to be expanded exactly.
For (20), the region u, v ≥ 0 becomes the wedge |s| ≤ r after the rotation, so the inner integral is a truncated Gaussian integral rather than a full one. The closed form appears only after an integration by parts in r, or an equivalent completion of the square.
The endpoint ρ = 1 is not covered by the printed argument, because (18) divides by √(1 − ρ²). It needs Mills' inequality separately. A proof that only treats ρ < 1 does not close the goal.
stdGaussPair is the product of two copies of Mathlib's gaussianReal 0 1 on ℝ × ℝ. orthantProb ρ t is the real-valued measure of {X ≥ t, ρX + √(1 − ρ²)Y ≥ t}, which is the representation the paper itself uses on p. 31.Lambda ρ μ chooses a t with Pr[X ≥ t] = µ, where the probability is taken under gaussianReal 0 1. Such a t is unique, so the choice does not matter. For µ ∉ (0, 1) no such t exists and the value is a placeholder 0 that no statement uses.The two remarks printed right after Proposition 6.1 (on Λ_ρ(1/2) and on removing the factor 1 + ρ) are not part of this mission.
Contributions are welcome on all four milestones, on the case ρ = 1 of the goal (Mills' inequality), and on general lemmas: N as Pr[X ≥ x], monotonicity and positivity of N, and the law of (X, ρX + √(1 − ρ²)Y) as a bivariate normal.
Augmented Lagrangian methods are among the standard ways to solve smooth nonlinear programs. They replace a constrained problem by a sequence of subproblems in which some constraints are moved into the objective through a penalty term and multiplier estimates. The method of Andreani, Birgin, Martínez and Schuverdt (SIAM J. Optim. 18(4), 2007) is the theory behind the ALGENCAN solver. It moves only the "upper-level" constraints into the objective, keeps arbitrary "lower-level" constraints in the subproblems, and requires the subproblems to be solved only approximately.
A convergence theory for such a method has to say what the limit points of the iterates are. This mission is about the second half of that theory (Theorem 4.2): a limit point that is feasible is a KKT point of the original problem, provided it satisfies a weak constraint qualification, the constant positive linear dependence condition (CPLD) of Qi and Wei (SIAM J. Optim. 10(4), 2000). Earlier global convergence results for augmented Lagrangian methods, such as Conn, Gould and Toint's, assumed linear independence of the active gradients (LICQ) at all limit points. CPLD is implied by MFCQ and by LICQ, holds automatically for linear constraints, and is required only at feasible points.
Timeline of the relevant notions:
The problem (2.1) is
with and constraint maps into , all continuously differentiable. and .
The augmented Lagrangian with respect to (2.2) is
Algorithm 3.1 works in outer iterations with a penalty parameter and safeguarded multipliers , that stay in fixed boxes. At iteration it finds and lower-level multipliers , that satisfy the KKT conditions of "minimize on " up to a tolerance . It then computes the first-order estimates and . Finally it increases by a factor unless a feasibility-complementarity measure has decreased by the factor .
A point satisfies CPLD if, whenever some gradients of constraints active at have a nontrivial vanishing linear combination with nonnegative coefficients on the inequalities, those gradients remain linearly dependent at every point of a neighbourhood of .
If is a limit point of and satisfies CPLD with respect to all constraints of (2.1), then is a KKT point of (2.1). If moreover satisfies MFCQ and , then
The theorem says that the algorithm has the right limit points: a feasible limit point is stationary under a constraint qualification weaker than MFCQ and LICQ, with no assumption on the penalty parameters. Milestone 3 is a result of independent interest: an "approximate KKT" sequence converges to a KKT point under CPLD. This sequential argument was later developed into the theory of approximate KKT conditions (Andreani, Haeser & Martínez 2011), and it applies to any algorithm that produces approximate KKT points, not only to this one. Milestone 4 gives the classical fact that MFCQ bounds the multipliers of such sequences.
All results are proved in the paper. As far as is known, none has a machine-checked proof. Neither CPLD nor the augmented Lagrangian method of this paper is formalized in Mathlib or on the platform. The companion missions of this series formalize Theorem 4.1 (feasibility of limit points) and Theorem 5.4 (boundedness of the penalty parameters).
The obvious argument divides the approximate KKT relation by the size of the multipliers, passes to the limit and obtains a contradiction with the constraint qualification. Under CPLD this argument fails, because CPLD does not bound the multipliers: they may diverge along the sequence even though the limit is a KKT point, and the limit of the normalized relation need not contradict anything at itself. CPLD speaks about linear dependence on a whole neighbourhood of , while the relation holds only at the iterates, so the information has to be transferred from to nearby points. A pointwise version of CPLD (dependence at only) is plain positive linear dependence, and with it the statement is false.
A second difficulty is complementarity (milestone 2). The safeguarded multipliers do not vanish on inactive constraints. Whether does depends on whether the penalty parameters are bounded, which needs the update rule of Step 4.
is EuclideanSpace ℝ (Fin n) and is Mathlib's gradient. The problem is a structure of component functions indexed by Fin m. The standing assumption "continuous first derivatives on a sufficiently large and open domain" is read as ContDiff ℝ 1 on all of .
A run of Algorithm 3.1 is a predicate on sequences (IsRun), not a computed object:
KKT, CPLD and MFCQ are defined once for an abstract program with finite index types. The constraints of (2.1) enter as the families and :
"Limit point" is MapClusterPt. (4.8) is required for every strictly increasing reindexing converging to , and it bounds the unsafeguarded estimates , ; the safeguarded ones are bounded by construction and would make (4.8) trivial.
Trivializing formalizations are ruled out:
Contributions welcome: proofs of the four milestones and of the goal, and in particular a reusable conic Carathéodory lemma and a library-level "approximate KKT + CPLD ⇒ KKT" theorem (milestone 3), which is useful well beyond this paper.
Augmented Lagrangian methods solve a constrained problem by minimizing a sequence of penalized subproblems while updating estimates of the Lagrange multipliers. Each subproblem carries a penalty parameter . When grows without bound the subproblems become ill-conditioned and hard to solve, and the method behaves like a plain external penalty method. Avoiding that growth is one of the main reasons for using multiplier updates at all, so conditions under which stays bounded matter both in theory and in practice (Bertsekas 1982; Conn, Gould, Toint 1991).
Andreani, Birgin, Martínez and Schuverdt (SIAM J. Optim. 18 (2007); HAL hal-01295437) propose an augmented Lagrangian method, Algorithm 3.1, in which only some of the constraints are penalized. Their §5 shows that, under classical local hypotheses at the limit point and a subproblem tolerance tied to the current infeasibility, the penalty parameters remain bounded. This mission formalizes that result for equality-constrained problems (Theorem 5.4), together with the general case (Theorem 5.5) as a companion statement.
Let , , , , be continuously differentiable. Problem (2.1) is
The upper-level constraints are penalized by the PHR augmented Lagrangian
while the lower-level constraints stay in the subproblems.
Algorithm 3.1 fixes , , , a box , a bound and tolerances . At outer iteration it finds and lower-level multipliers such that is an -approximate KKT point of minimizing over the lower-level set, in the sense of (3.1)–(3.4). It then forms the first-order multiplier estimates
and safeguarded estimates , which in §5 are the projections of on their boxes. Finally it updates the penalty parameter: with ,
In §5.1 there are no inequality constraints (): problem (5.1), with Lagrangian . Assumptions 1–6 at the limit of are: convergence, feasibility, linear independence of all constraint gradients, near , the second-order sufficient condition with multipliers , and in the interior of the safeguard box.
Under Assumptions 1–6, , and for a sequence ,
with and . 4. (5.10): if , then for large. 5. Contraction: if , then for large.
Theorem 5.5, the general problem (2.1) under Assumptions 7–13 (LICQ, , a second-order condition on the tangent subspace of all active constraints, multipliers inside the safeguard boxes, strict complementarity for the active upper-level inequalities), with ; and two steps of its proof, (5.13) and (5.14).
Theorem 5.4 tells a user of the method when it does not degenerate: if the safeguard box contains the true multipliers and the subproblems are solved to a precision proportional to the current infeasibility, then the penalty parameter is eventually constant. The Remark after Theorem 5.5 draws the practical conclusion that the box should be large enough to contain the true multipliers. The result underlies the analysis of the ALGENCAN solver built on Algorithm 3.1.
The results are proved on paper. To our knowledge none of them, nor the PHR augmented Lagrangian method itself, has a machine-checked formalization. A formal proof would also pin down two gaps in the printed statements, recorded under Formalization scope: the case and the early iterations in Lemma 5.3. The local analysis (a uniformly nonsingular KKT matrix and implicit-function error bounds for multiplier estimates) is reusable for other augmented Lagrangian and SQP methods.
Without the second-order structure there is no reason for to stay bounded: the update test compares consecutive infeasibilities, and nothing in the global theory forces them to decrease geometrically. The local argument has to show that contracts by a factor of order , which requires error bounds for both and that hold uniformly as varies in an interval containing . The uniformity in the perturbation parameter , around the singular-looking limit , is the central difficulty. Applying the implicit function theorem at each fixed does not give it.
is EuclideanSpace ℝ (Fin n). Constraint maps are families of real functions indexed by Fin m, and problem (5.1) is (2.1) with . The norm in (3.1), on and on is Euclidean. Every , and the norms in (3.4), on and on , are the sup norm. The paper's norm is arbitrary and the constants absorb the change. A run of Algorithm 3.1 is a predicate on sequences: x 0 is , the outer iterations are , and the three tolerances of Step 2 are kept separate. The gradient in (3.1) is the true gradient of the defined augmented Lagrangian. "Continuous first derivatives" is on ; "continuous second derivatives near " is ContDiffAt ℝ 2. Hessians are derivatives of gradients. Every statement that uses a Hessian assumes at , so it cannot be a junk value. Assumption 5 is pinned to Fletcher's equality-constrained second-order sufficient condition. Linear independence is that of a family indexed by a sum type, so equal gradients count as dependent.
Added hypotheses, each stated in the item's Formalization Note:
Statements that would trivialize the goal are excluded. These include a run predicate that no sequence satisfies, merging the three tolerances into , collapsing gradient families into sets, a junk Hessian, and assuming or in the goal. The last two appear only as milestone hypotheses.
A complete development needs the PHR gradient formula, uniform invertibility of a continuous family of matrices on a compact interval, a quantitative inverse function estimate for maps, and the convergence of multiplier estimates under LICQ. Proofs of any milestone, and reusable lemmas for these pieces, are welcome.
Augmented Lagrangian methods (the method of multipliers of Hestenes, Powell and Rockafellar) solve a constrained nonlinear program by a sequence of easier subproblems in which some constraints are moved into the objective through a penalty term plus a multiplier estimate. Andreani, Birgin, Martínez and Schuverdt (SIAM J. Optim. 18 (2007); preprint HAL hal-01295437) split the constraints into upper-level constraints, which are penalized, and lower-level constraints, which are kept in every subproblem and may be arbitrary (not only bounds). This is the design of the solver ALGENCAN and of its successors.
A practical method usually cannot guarantee that its iterates approach a feasible point: the problem may be infeasible, and even when it is not, a local method may stall. The question this mission formalizes is what a limit point of the method is when the penalty parameter is or is not driven to infinity. The answer, Theorem 4.1 of the paper, states that infeasible limit points are not arbitrary: they are stationary for the problem of minimizing the upper-level infeasibility over the lower-level set, unless a weak constraint qualification fails there.
The problem is (2.1):
with , , , , , all continuously differentiable. Write and .
The PHR augmented Lagrangian (2.2) with respect to is, for , , ,
Algorithm 3.1 has parameters , , , boxes and , and tolerances with . At outer iteration it finds and lower-level multipliers , satisfying the approximate KKT conditions (3.1)–(3.4) of minimizing over to tolerance ; it chooses new safeguarded multipliers , in the boxes; and it keeps when
and sets otherwise. A run is a sequence produced this way in which the subproblem of Step 2 is always solvable.
A point is a KKT point of a problem with objective , equalities and inequalities if it is feasible and for some and some vanishing on inactive inequalities. The constant positive linear dependence condition (CPLD, Qi and Wei) holds at if every nontrivial null combination of gradients of equalities and active inequalities, with nonnegative coefficients on the inequalities, has gradients that remain linearly dependent at every point near . CPLD is weaker than both LICQ and the Mangasarian–Fromovitz condition.
Let be a run and a limit point of it. If is bounded, then . Otherwise at least one of the following holds:
Theorem 4.1 is the feasibility half of the global convergence theory of the method; Theorem 4.2 of the same paper (a companion mission) shows that feasible limit points satisfying CPLD are KKT points of (2.1). Together they say that the method either finds a stationary point of the original problem or a stationary point of the infeasibility, under a constraint qualification weaker than MFCQ and only at the limit point. Because the lower-level set is arbitrary, the theorem covers the many variants in which bounds, linear constraints or structured sets are kept out of the penalty.
The result is proved in the paper; no machine-checked proof of it is known. Formalizing it requires the gradient of the PHR function, a conic Carathéodory theorem with linear independence (Mathlib contains only the convex-hull version), and the subsequence and normalization arguments of the proof. Each is reusable: milestone 5 is used again, unchanged, in the proof of Theorem 4.2.
The bounded case is elementary. The unbounded case is where the work lies. Dividing the approximate stationarity condition by removes the objective and the multiplier estimates, but the lower-level multipliers divided by need not stay bounded, so no limit can be taken directly. The supports of the lower-level combinations must first be reduced to linearly independent ones, uniformly along a subsequence, before the bounded/unbounded dichotomy on the reduced multipliers yields either a KKT point of (4.1) or a nontrivial null combination at whose gradients are independent at points arbitrarily close to . Taking limits of the original multipliers without this reduction does not work.
is EuclideanSpace ℝ (Fin n); constraint maps are families of real functions indexed by Fin m. Continuous differentiability "on a sufficiently large and open domain" is read as on all of . The norm in (3.1) is the Euclidean one; (3.4), Step 4 and the vectors , use the sup norm. The paper's norm is arbitrary and the results do not depend on the choice. A run is a predicate on sequences indexed by : x 0 is the initial point , the outer iterations are , the three subproblem tolerances are kept separate, and is the true gradient of the defined function (2.2). "Limit point" is a cluster point of the sequence; "bounded" is boundedness above of . KKT and CPLD are defined once for arbitrary finite index types; CPLD carries no feasibility clause, and linear independence is that of a family indexed by a disjoint union, so a repeated gradient counts as dependent.
No hypothesis is added to Theorem 4.1 beyond the reading. Junk values cannot trivialize the statement: the run evaluates (2.2) and only at ; the gradients are taken of functions; the run is satisfiable; and both alternatives (i) and (ii) can fail at the same point, so the second half of the theorem has content.
Contributions are welcome on every milestone. The gradient computation (4.2) and the conic Carathéodory theorem are self-contained and useful beyond this paper.
Multistage stochastic linear programs model sequential decisions under uncertainty: capacity and reservoir planning, hydro-thermal scheduling, inventory and asset–liability management. When the data process is stagewise independent, the problem decomposes by dynamic programming into one linear program per stage, coupled through expected cost-to-go functions. These functions are convex and piecewise linear, and the stochastic dual dynamic programming (SDDP) method of Pereira and Pinto (1991) approximates them from below by cutting planes. SDDP is the standard solution method in the long-term planning of hydro-dominated power systems, and its convergence theory determines what the bounds it reports actually mean.
Shapiro's paper (Optimization Online 2009/12/2509; European J. Oper. Res. 209(1), 2011, doi:10.1016/j.ejor.2010.08.007) analyses SDDP applied to a sample average approximation (SAA) of the true problem, with all of the data random. Its convergence result, Proposition 3.1, asserts finite convergence with probability one when the forward scenarios are subsampled independently. A related almost-sure finite convergence theorem for a different algorithm (DOASA, with randomness only in the right-hand sides and cut sharing across outcomes) is due to Philpott and Guan (2008); it is posed as a separate mission on this platform and is not restated here.
There are stages. The decision satisfies and, at the first stage, with deterministic data . For the data are replaced by a sample , , each with probability , independently across stages, and the stage- constraint is . The SAA cost-to-go functions are defined backwards from :
A scenario is a choice ; there are of them, each of probability . A policy depends only on the outcomes up to stage ; it is optimal for the SAA problem if it is feasible on every scenario and its expected cost is minimal.
SDDP keeps, for each stage, a finite set of cuts whose maximum lies below . An iteration has a forward step: scenarios are sampled, and along each of them the decisions solve the stage problems with in place of , (3.13)–(3.14). It also has a backward step: from down to , at each trial point the stage- problems with the current cuts are solved for all outcomes, and the cut (3.17) is added, where averages over basic optimal (extreme-point) dual solutions .
Suppose the forward scenarios are drawn independently and uniformly from the SAA scenarios, (A1) holds ((3.13) and (3.14) have finite optimal values for every scenario at every iteration), and the backward steps use basic optimal dual solutions. Then
The goal fixes no iteration count, no rate and no number of forward scenarios .
The result separates SDDP's sampling from its convergence: on a finite scenario tree, independent subsampling of forward paths suffices for the method to stop at an optimal policy, without ever enumerating the tree. It explains why the lower bound eventually equals the SAA optimal value, which is what makes the gap-based stopping rules of the paper (§3, Remarks 4–6) meaningful. The paper's closing remark stresses that without independence of the forward scenarios there is no guarantee of convergence.
The proposition is proved in the paper. No machine-checked proof of it, or of any SDDP convergence theorem, exists to our knowledge. Formalizing it requires a precise account of what the method is: which dual solutions, which forward solutions, which order of updates. Several of these points are left implicit on the page.
Finiteness of the cut universe (milestones 4–5) is a statement about extreme points of dual polyhedra whose dimension grows with the cut sets of the next stage, so it must be organized stage by stage from down. The central difficulty is the last step of the argument. Once the approximations have stopped changing, one must show that the stable cuts are exact where the forward policy goes, so that the forward policy satisfies (3.18). The obvious argument, "if (3.18) fails at the last stage where it fails, the next cut there increases ", does not work as printed: (3.18) holding at later stages does not by itself make the next-stage approximation exact at the trial point. Closing this step is where the conventions on forward solutions and on sampling listed below become essential.
The Lean development is in the namespace ShapiroSDDP.Convergence. Stages are numbered
; the data of stage are stored under index (the coupling matrix is indexed by the
decision it multiplies); V t is , with V t ≡ 0 for . Cost-to-go
values are real infima, used only on reachable decisions. The explicit readings are:
iIndepFun);Optimality of a policy is defined by expected cost, never by (3.18), so that milestone 6 is not definitional. Sampling is stated as i.i.d. uniform draws, not as "every scenario recurs", which is milestone 7. All of depend on the outcome. If some lacks full row rank, no basic dual solution exists and no run exists; a sorry-free witness instance shows that all hypotheses of the goal can hold together.
Useful infrastructure: LP weak and strong duality (LinearOptimization.lp_weak_duality,
LinearOptimization.lp_strong_duality exist on the platform in their own encoding), finiteness of
extreme points of polyhedra, attainment for polyhedral objectives, and the second Borel–Cantelli
lemma (ProbabilityTheory.measure_limsup_eq_one). Proofs of any milestone, and reusable lemmas on
LPs with cut epigraphs, are welcome.
The effective resistance between two vertices of a weighted graph is the voltage difference that appears between them when the graph is viewed as an electrical network, edge weights being conductances, and one unit of current is injected at one vertex and extracted at the other. Effective resistances drive the spectral sparsification algorithm of Spielman and Srivastava (arXiv:0803.0929): sampling each edge with probability proportional to its weight times its effective resistance yields a sparse graph whose Laplacian approximates the original one. They are also used as a distance on graphs in the analysis of social and small-world networks, where they reflect how many short paths connect two vertices.
Computing every effective resistance exactly requires the pseudoinverse of the Laplacian, which costs far more than the size of the graph. Section 4 of the paper shows that all of them can be approximated in nearly linear time: a random projection compresses the relevant vectors to dimensions, and the projected vectors are obtained from calls to a fast approximate Laplacian solver (Spielman–Teng). This mission formalizes the deterministic statement that makes this procedure correct, Lemma 9: approximate solves, at a stated accuracy, do not destroy the approximation that the random projection provides.
Let be a connected, simple, weighted undirected graph with vertices, edge set and edge weights . Orient every edge arbitrarily, so that it has a head and a tail. The signed incidence matrix has if is the head of , if is its tail, and otherwise. With the diagonal matrix of weights, the Laplacian is , a symmetric positive semidefinite matrix whose kernel is spanned by the all-ones vector when is connected. Its Moore–Penrose pseudoinverse is , where are orthonormal eigenvectors of with nonzero eigenvalues .
For a vertex let be its indicator vector. The effective resistance between and is
and for an edge with endpoints . The -norm of is . Let and be the smallest and largest edge weights.
A resistance sketch is a matrix (columns indexed by ) with
where is the Euclidean norm. In the paper, for a random matrix with , and the Johnson–Lindenstrauss lemma makes it a sketch with high probability. Write and for the -th rows of and of an approximation , as vectors in .
Let . If is a resistance sketch, if every row satisfies
and if
then for every pair
The lemma is stated for arbitrary , and : nothing about the random projection or the solver enters beyond (4) and the sketch property.
Lemma 9 is the correctness half of the paper's Theorem 2: together with a Johnson–Lindenstrauss lemma and the Spielman–Teng solver it yields a data structure, built in time, that returns any effective resistance to within a factor in time. This in turn makes the effective-resistance sampling of the paper's Theorem 1 run in nearly linear time, and the same sketch-and-solve pattern has been reused in later work on Laplacian solvers, graph sparsification and electrical-flow algorithms.
The result is proved in the paper. Formalizing it produces machine-checked statements of three facts that recur throughout spectral graph theory: the trace identity (Foster's theorem in its weighted form), the lower bound on effective resistances by comparison with the complete graph, and the stability of a resistance sketch under relative -norm errors. Neither Mathlib nor this platform states any of them for the linear-algebraic definition of effective resistance used here.
The hypothesis (4) controls the error row by row, in the -norm on , while the conclusion concerns the columns of applied to , in the Euclidean norm on , and it is a relative bound for every pair at once. A relative bound cannot hold unless is bounded below uniformly over all pairs of distinct vertices, which is where the factors , and of (5) come from. Such a lower bound is false for multigraphs, whose parallel edges can make arbitrarily small, and the relation between the -norm of a row and the Euclidean norms of the columns involves every edge of the graph, not only a path between and .
Proposition 10 is classically derived from Rayleigh's monotonicity law. Its standard formal statement on this platform concerns the probabilistic definition of effective resistance through hitting probabilities of a random walk, which is a different definition from ; no theorem relating the two is available.
The graph is a structure WGraph V E over finite types (vertices, Fintype.card V) and (edges), with head, tail : E → V, head e ≠ tail e, weights w : E → ℝ with 0 < w e. Connectivity is that of the underlying simple graph (Mathlib's SimpleGraph.Connected, which includes ); simplicity means that no two edges join the same unordered pair. Matrices are Mathlib matrices indexed by and . is the published Moore–Penrose pseudoinverse HarmonicGames.Decomposition.pinv of on the Euclidean space , converted back to a matrix; for symmetric this is the spectral pseudoinverse of §2.2. is the sum of squares of the coordinates, not Lean's sup norm. is the real number .
Choices committed to, relative to the page:
A trivializing formalization is ruled out: the goal does not assume the intermediate inequality of the proof, nor a stronger condition on than (5); its hypotheses are satisfiable (for example with and ), and its conclusion is not vacuous for .
Infrastructure that a complete development needs, and that is reusable beyond this mission: the identity and as the projection onto for a connected Laplacian; the trace identity; Loewner-order monotonicity of in the edge weights; and the effective resistances of the complete graph. Contributions of any of these as separate lemmas are welcome. The random projection (Johnson–Lindenstrauss) and the solver's running time are outside this mission.
Markov decision processes model sequential decisions under uncertainty, and their optimal policies are computed from transition probabilities that in practice are estimated from data. Optimal policies can be sensitive to estimation error in those probabilities. Robust dynamic programming replaces each transition law by a set of plausible laws and evaluates a policy by its worst-case expected reward over that set. Garud Iyengar's Robust dynamic programming (CORC Tech Report TR-2002-07, 2002, rev. 2004; Mathematics of Operations Research 30(2), 2005) set up this theory for countable state spaces and history-dependent policies. It isolated the Rectangularity assumption under which the robust problem keeps a Bellman equation. In the same period, Nilim and El Ghaoui studied robust control of Markov decision processes with finite state spaces.
Timeline:
A discounted ambiguous Markov decision process has a countable state set , for each state a nonempty set of admissible actions, for each admissible pair a nonempty set of probability measures on (the ambiguity set), a bounded reward and a discount factor . Decisions are made at epochs .
A policy maps each history to a probability measure on . is the set of all such policies. A deterministic Markov policy plays for maps with . A stationary policy uses one such rule at every epoch.
Under Rectangularity, the adversary picks a law separately at every epoch and history, and may pick a different law each time a state–action pair recurs. This is the dynamic model, and the set of path measures it generates is . In the static model the adversary fixes one per pair. The robust value of a policy and the robust value function are
Let be the bounded functions on with . For a set of deterministic Markov rules, the robust Bellman operator is
is the only bounded solution of this equation, and for every some stationary deterministic policy has .
Corollary 2(b) justifies computing the robust value function by solving a state-wise max–min equation. Value iteration, policy iteration and their approximations all rely on that equation. It also shows that a decision maker facing a history-dependent adversary loses at most by committing to a stationary deterministic rule. Corollary 2(a) and Lemma 2 make robust policy evaluation a fixed point problem and a robust optimization problem. Lemma 3 shows that, for stationary policies, the dynamic model costs nothing relative to the static model, in which the true transition law is fixed but unknown.
The results are proved on paper. The page proves Theorem 4 only by citation to Puterman's non-robust arguments. No machine-checked proof of any of them is known. The platform has finite-state analogues posed by the Nilim–El Ghaoui and Satia–Lave missions, which compare only stationary or Markov controllers. This mission poses the countable, history-dependent version, and proving it would establish them in this generality.
The contraction property is a state-by-state -argument. The hard step is to identify the fixed point with the value of the game against all history-dependent randomized policies. The adversary's choices at different epochs interact only through Rectangularity, so splitting the infimum over path measures into a first-step infimum and a continuation infimum must be justified for an infinite horizon, uncountably many adversary strategies and no attainment of the infima. The ambiguity sets need not be convex or closed. The naive route, "take the minimizing law at each state", is unavailable, and every bound must be carried with an slack. Truncating the infinite sum needs the uniform reward bound. Theorem 4 needs a separate argument that randomization and history dependence do not help the decision maker against the dynamic adversary.
States and actions are countable Lean types; and are sets, assumed nonempty, with no convexity or closedness. Laws are PMFs and as a tsum. The rewards satisfy on admissible actions. This is the reading of the page's "", which its bounds require. The discount factor satisfies . Epochs start at , so the first reward is undiscounted.
A policy maps to a PMF supported on . The dynamic adversary maps to a law in . The path law is built by PMF.bind, and the discounted reward is , which converges absolutely. Values are real infima and suprema over nonempty families bounded by , so no junk value arises. is the predicate "bounded", and is a supremum (the page writes max). All uniqueness claims are uniqueness among bounded functions.
is a supremum over all history-dependent randomized policies. Defining it over deterministic Markov or stationary policies would make Theorem 4 trivial and weaken the goal, so it is ruled out. The adversary in is the dynamic one; the static adversary appears only in Lemma 3.
The mission deviates from the page in three places:
Only the first claim of Lemma 1 is posed. Its second claim, that an -greedy rule is -optimal, is false as printed.
A complete development needs a general toolkit that is reusable beyond this mission: path laws of countable controlled processes with history-dependent policies, a uniform -optimal selection argument for real infima over arbitrary sets, and the Banach fixed point theorem on bounded functions (Mathlib's ContractingWith). Proofs of individual milestones are welcome in any order. Theorem 5(a) is the natural entry point.
An investor who trades continuously in a market driven by Brownian motion, and who may only hold portfolios in a prescribed set, wants to maximize the expected utility of terminal wealth. With power utility , , this is the constant-relative-risk-aversion problem that goes back to Merton (Merton 1971). When there are fewer stocks than sources of noise the market is incomplete, and when portfolio proportions are restricted (no short sales, bounded positions, a fixed allocation) the problem is constrained.
For convex constraints, duality methods settle the problem (Cvitanić–Karatzas 1992; Kramkov–Schachermayer 1999). They do not apply when the constraint set is closed but not convex, as for integer-lot or "all-or-nothing" restrictions. Hu, Imkeller and Müller (2005, arXiv:math/0508448) treat that case by a martingale optimality principle: they build a process that is a supermartingale for every admissible strategy and a martingale for one, and obtain it from a backward stochastic differential equation (BSDE) with a driver that grows quadratically in . The existence theory for such equations is due to Kobylanski (2000).
This mission formalizes the power-utility result, Theorem 14 of the paper. A companion mission treats the exponential-utility result, Theorem 7.
Fix a horizon and a probability space carrying an -dimensional Brownian motion ; is the augmentation of its natural filtration. is the Euclidean norm, and is Lebesgue measure on .
Market. There is a bond with zero interest and stocks with prices . The rates and the volatility are predictable and uniformly bounded, and for constants . The market price of risk is .
Constraints. A closed set of row vectors constrains the proportions of wealth held in the stocks. In the variable the constraint reads . For a closed , , and is the (possibly multi-valued) projection.
Wealth and admissible strategies. From initial capital the wealth (11) is
The admissible class (Definition 13) consists of predictable with for -a.e. and a.s. The value is (12), .
The BSDE. is the class of predictable, -a.e. bounded processes and that of predictable with . The BSDE (15) is
A BMO martingale is one with over stopping times (equation (2)).
(15) has a unique solution , and for
attained by some with
The page prints ; its proof measures utility by , so the value of (12) with carries the factor (see Formalization scope).
The theorem gives the value of a constrained power-utility problem in closed form through one scalar, , of a BSDE, and identifies an optimal strategy as a measurable selection of a projection onto the constraint set. Convexity of the constraint is not needed; when is a convex cone the result recovers the strategy obtained by other methods (Remark 16 of the paper). The same scheme handles exponential and logarithmic utility in the paper's other sections, and the dynamic programming principle of Proposition 15 follows from it.
The result is proved in the paper. As far as the platform's records show, none of it is formalized: there is no quadratic BSDE, no BMO martingale and no continuous-time utility-maximization statement on the platform. A complete formalization would add an existence and uniqueness theory for BSDEs with quadratic growth, the BMO criterion for stochastic exponentials, and a verification theorem for constrained portfolio problems, each reusable well beyond this paper.
The verification argument is short on paper; its inputs are not. Existence for (15) rests on Kobylanski's existence theorem for drivers of quadratic growth, which is not in Mathlib; the Lipschitz theory does not cover a driver growing like . Uniqueness needs a comparison principle for such drivers. Lemma 17 and the martingale property of need the theory of BMO martingales and of their stochastic exponentials, also absent. The comparison milestone concerns processes that are only local supermartingales. A naive attempt that treats as a martingale for every admissible fails: for a general , which is only locally square integrable, it is merely a local supermartingale.
All declarations live in HuImkellerMuller.Power. Time is ℝ≥0; vectors of are EuclideanSpace ℝ (Fin m), with products as inner products; is a Set (Fin d → ℝ). The Brownian motion, the augmented filtration, the measure and the Itô-integral operator I are reused from published definitions (EthierKurtz_IsStandardBrownian, CvitanicKaratzas92_Optimality_Market). The wealth is constructed from I, and ; is computed from and .
Conventions and disclosed readings:
The value is a supremum of lower integrals, never of Bochner integrals: a Bochner expectation of a non-integrable is and would make the supremum meaningless. The goal asserts existence of a solution of (15) and does not take one as a hypothesis, so it cannot hold vacuously.
Contributions welcome: a theory of BSDEs with quadratic growth (Kobylanski), BMO martingales and Kazamaki's criterion, measurable selection of metric projections, and proofs of the deterministic milestone (14) and the growth bound (H1).
Risk-averse stochastic optimization replaces the expected cost of an uncertain outcome by a risk function : conditional value-at-risk, mean–semideviation and mean–upper-semideviation models, and the coherent and convex risk measures of Artzner, Delbaen, Eber and Heath and of Föllmer and Schied. Ruszczyński and Shapiro, Optimization of convex risk functions (Math. Oper. Res. 31, 2006), develop the convex analysis of such functions on general spaces of random variables, so that they can be used inside optimization problems .
Optimality conditions, duality and sensitivity analysis for such problems need two regularity properties of : continuity, and the existence of subgradients that are continuous linear functionals. For extended-valued convex functions on infinite-dimensional spaces neither comes for free. The standard sufficient condition, boundedness from above on a neighbourhood of a point (Ioffe and Tikhomirov), often cannot be used: the paper notes (p. 436) that the cone of nonnegative functions in , , a continuous probability measure, has empty interior. Section 3.1 shows instead that for monotone convex risk functions on a Banach lattice both properties follow from convexity and monotonicity alone. This mission formalizes that result, Proposition 3.1, and its instance, Corollary 3.1.
Let be a real vector space with a partial order , and . Outcomes are costs: smaller is better. A function has domain and is proper if for all and . The paper's axioms used here are
A linear functional , not necessarily continuous, is an algebraic subgradient of at if
When is a Banach space it carries its norm topology and is paired with its dual . The subdifferential is the set of continuous satisfying (3.1), and is subdifferentiable at if .
A Banach lattice is a real Banach space whose order makes it a lattice, compatible with addition, such that implies . Every , , with the almost-everywhere order, is one.
In Lean everything lives in the namespace ConvexRiskFn.Cont: dom, IsProper, A1, A2, IsAlgSubgradient and subdiff are defined in the setting file.
Let be a Banach lattice and proper, satisfying (A1) and (A2). Then
Proposition 3.1 removes lower semicontinuity from the list of assumptions a modeller has to check. In the paper's framework, the dual representation (Theorem 2.2) requires lower semicontinuity. The subdifferential formulas, the Hadamard directional differentiability of composite functions and the optimality conditions of §§3.2 and 6 require continuity or subdifferentiability at the point of interest. On spaces, Corollary 3.1 gives all of these on the interior of the domain from (A1) and (A2) alone, for example for real-valued convex monotone risk functions such as the mean–upper-semideviation and conditional value-at-risk models of §4.
The result is proved in the paper, so the formalization adds no new mathematics. It does add two classical functional-analytic facts that the paper cites without proof: automatic continuity of positive functionals on Banach lattices, and continuity of lower semicontinuous convex functions on open subsets of Banach spaces, here for extended-real-valued functions. As far as a search of Mathlib and of the platform shows, neither is formalized in this generality. Mathlib's continuity result for convex functions is finite-dimensional. Mathlib has the Hahn–Banach extension theorem but no theory of positive functionals on Banach lattices.
An algebraic subgradient exists at an interior point by Hahn–Banach applied to the directional derivative, and in a general Banach space it may be discontinuous. Continuity cannot come from local boundedness either: the usual criterion (bounded above near a point) is exactly what fails for natural examples, since positive cones in , , have empty interior. The order structure has to do the work. Monotonicity forces the subgradient to be positive, and positivity forces continuity on a Banach lattice. That last step needs completeness and solidity of the norm. Without them, positive linear functionals need not be continuous, for example on the space of finitely supported sequences.
The second difficulty is passing from lower semicontinuity at each interior point to continuity on the interior. For a convex function this needs a Baire category argument on the Banach space, and completeness cannot be dropped.
E with NormedAddCommGroup, NormedSpace ℝ, CompleteSpace, Lattice, HasSolidNorm (the solidity condition) and IsOrderedAddMonoid. This is the paper's definition, and it contains the paper's function spaces, so the formal goal is a generalization. Compatibility of the order with multiplication by nonnegative scalars is not assumed; it follows from these axioms.EReal. Convexity (A1) is written with EReal arithmetic, which agrees with the paper's for proper functions. Continuity on the interior is continuity of an EReal-valued function in the order topology. On the interior the function is finite, so this is ordinary continuity.E →L[ℝ] ℝ, i.e. . A version stating only an algebraic (possibly discontinuous) subgradient would be the easy half of the result and is not the goal; it is milestone 2.Lp ℝ p μbar (a.e. classes) with a finite measure (the paper's measures are finite, p. 434) and . Its subgradient is a function with MemLp g q μbar for the Hölder conjugate , paired by the integral.exists_extension_of_le_sublinear in Mathlib), positive functionals on Banach lattices, and the Baire-category continuity theorem for convex lower semicontinuous functions. The last two are reusable well beyond risk functions. Contributions proving any milestone, or proving the Phelps or Levin step in greater generality, are welcome.In a one-stage stochastic program a decision maker observes a random outcome and then picks a decision , subject to constraints that depend on , so as to minimize expected cost. The optimization variable is a whole function , and computing the optimal value is #P-hard even for a uniform distribution on the unit cube (Dyer and Stougie, 2006, cited in the paper as [16, Theorem 3.2]). A standard tractable approximation, introduced for robust optimization by Ben-Tal, Goryashko, Guslitzer and Nemirovski (2004) and carried to stochastic programming by Shapiro–Nemirovski and Chen–Sim–Sun, restricts decisions to linear decision rules . This restriction gives an upper bound on the optimal value.
Kuhn, Wiesemann and Georghiou (2009/2011) study these approximations systematically. Their §3 treats the case where the constraint matrix itself depends on (random recourse). Linear decisions then produce constraints that are quadratic in , and the paper reformulates the resulting semi-infinite problem as a semidefinite program. This mission formalizes that reformulation, the primal half of the paper's Theorem 2.
Uncertainty is a probability measure on , with outcomes . The support of is the smallest closed set of probability one. It is assumed to have the form
for symmetric matrices , where is the first standard basis vector. The first coordinate of every outcome is therefore , so linear functions of are affine functions of the remaining coordinates. is assumed nonempty and bounded, and its linear hull is assumed to be . Let denote the symmetric matrices and the second-moment matrix.
The data are (cost ), (right-hand side , with rows ), and , where the th row of the recourse matrix is . The stochastic program minimizes over square-integrable subject to almost surely. It is strictly feasible if some square-integrable and some satisfy and almost surely.
With linear decisions and quadratic slacks , , one obtains the primal approximation
and the SDP (3.14)
The theorem replaces a problem with infinitely many constraints, one per outcome, by a semidefinite program with variables. Its value is always an upper bound on , and hence on . When the support is a single ellipsoid in the hyperplane (), the bound loses nothing beyond the restriction to linear decisions. For the gap is unavoidable in general: an exact tractable reformulation would decide copositivity, which is NP-hard (Remark 7). Random recourse arises whenever technology or yield coefficients are uncertain, for example in production planning and portfolio problems with uncertain returns.
The result is proved in the paper. As far as is known it has no machine-checked proof. A formalization adds a precise statement of the hypotheses. Writing those hypotheses out showed that the unnumbered §3.2 step needs to have dimension , which spanning alone does not give for nonconvex (see Formalization scope). The other half of Theorem 2, about the lower-bounding SDP (3.18), is false in this preprint and is not part of the mission.
The semi-infinite constraints hold only -almost surely. The first step is to pass from "almost surely" to "for every ", which uses that is exactly the support and that the constraint functions are continuous. A bound alone is not enough. For the equality constraints, a quadratic form that vanishes on must vanish identically. This requires to be large enough, and the obvious argument from " spans " fails when is a finite set. For the inequality constraints with , the implication must be established on all of and not only on the slice . Doing so needs boundedness of (no recession directions) and a strictly feasible point for the S-lemma. The S-lemma itself is a nonconvex duality statement. It is available on the platform.
Outcomes live in Fin k → ℝ, with carried in the setting. Indices are 0-based: is coordinate 0, and range over Fin m, Fin l. " is the support of " is stated as: is closed, , and every ball centred in has positive measure. Mathlib has no Measure.support at this revision. The standing assumptions (probability measure, symmetric , support, nonempty, bounded, spanning) form one predicate assumed by every theorem. Decision rules are Borel measurable square-integrable functions. Optimal values are infima in EReal, for an empty feasible set and for an unbounded one. "Equivalent" means equal optimal values. Each is required symmetric in both problems; is positive semidefiniteness and is componentwise. Strict feasibility of in §3 is the paper's condition (2.9) of §2 with replaced by . The paper uses the phrase without restating it.
Repairs and narrowings:
The goal cannot be trivialized through its definitions. Feasibility is quantified -almost surely for a measure whose support is , not over an empty or arbitrary set. Both optimal values are infima of the same real objective over the problems' own feasible sets. The standing assumptions are satisfiable, for instance by , , and the uniform law on .
The definitions (support of a measure, decision rules, the random-recourse data) are reusable for the other sections of the paper and for related work on decision rules. Proofs of any milestone, Lean lemmas on quadratic forms vanishing on open cones, and an almost-sure-to-support transfer lemma are welcome.
Matrix completion asks to recover a large matrix from a small number of its entries. It is the abstraction behind collaborative filtering (recommender systems in which a users × items rating matrix is observed on a sparse set of pairs), sensor localization from partial distance information, and system identification. Without structure the problem is hopeless; the standard structural assumption is that the unknown matrix has low rank, and the standard convex surrogate for rank is the nuclear norm, the sum of singular values.
In the noiseless case, exact recovery by nuclear-norm minimization from about uniformly sampled entries was established by Candès and Recht (2009) and refined by Candès and Tao (2010) and Gross (2011). With noisy observations the relevant question is a rate: how fast does an estimator's error decrease with the number of observed entries? Koltchinskii, Lounici and Tsybakov (arXiv:1011.6256, Ann. Statist. 2011) introduced a nuclear-norm penalized estimator that uses the known sampling distribution, showed that in matrix completion it is an explicit soft thresholding of the singular values of a rescaled data matrix, and proved for it sharp oracle inequalities (leading constant 1) whose rates are optimal up to logarithmic factors. This mission formalizes the version of that result for bounded responses: Theorem 4 of the paper, together with the probabilistic lemma and the matrix Bernstein inequality it rests on.
Fix positive integers and write for the real matrices, with scalar product , Frobenius norm , nuclear norm (sum of singular values) and operator norm (largest singular value). Set and write .
The matrix completion basis is
where are the canonical basis vectors of . One observes independent random pairs , where is uniformly distributed on and is real, following the trace regression model
for an unknown . Thus is a noisy reading of the entry of selected by ; this is matrix completion under uniform sampling at random (USR), entries possibly sampled more than once.
The estimator is, for a regularization parameter ,
The stochastic error is the random matrix
Assume almost surely. For and
with probability at least , simultaneously for all ,
Theorem 4 is a non-asymptotic, sharp oracle inequality: the leading constant in front of is 1, so the bound applies to misspecified targets ( not low rank) without loss. Taking and of order gives a normalized Frobenius error of order , which the paper's minimax lower bounds (§4) show to be optimal up to the logarithm. Because no model is needed for Lemma 1, the same probability bound also drives the paper's statistical-learning reformulation (Theorem 9).
The theorems here are proved in the paper. What is open is their formalization: no matrix Bernstein inequality, and no oracle inequality for nuclear-norm penalized estimators, has a machine-checked proof on this platform. Proposition 1 in particular is a reusable concentration tool well beyond this paper (covariance estimation, random graphs, sketching).
The deterministic part (milestone 2) needs the subdifferential of the nuclear norm, which is not in Mathlib. The probabilistic part is where the obvious argument fails. Bounding entrywise and summing, or bounding it by the Frobenius norm, loses a factor polynomial in the dimension; a union bound over a net of the unit sphere loses the factor that makes the rate optimal. The correct rate requires a noncommutative Bernstein inequality, controlling the operator norm of a sum of independent random matrices through the matrix variance at the price of only a factor. The matrix-analytic machinery such inequalities depend on (trace inequalities for matrix exponentials, the passage from rectangular to symmetric matrices) is not currently available in Mathlib.
All objects are local to the namespace KLTNuclear.Completion, built on the published MatrixCompletion definitions (RealMatrix, nuclearNorm, spectralNorm, frobeniusNormSq, matrixInner, coordinateMatrix). Conventions:
IsProbabilityMeasure; are hypotheses. is the natural logarithm; .Matrix, so measurability, independence and conditioning on a random matrix use its entry array with the product -algebra; expectations of matrices are entrywise.The source is the arXiv preprint arXiv:1011.6256v4. Welcome contributions: a general matrix Bernstein inequality (Hermitian and rectangular forms), the nuclear-norm subdifferential, and proofs of the deterministic milestone.
Scheduling jobs whose processing times are not known in advance is a basic problem of production planning, project management and computing systems. In the stochastic machine scheduling model only the distribution of each processing time is known beforehand; the actual duration of a job is revealed when the job completes. A solution is then not a schedule but a scheduling policy, which decides at every point in time what to start next on the basis of what has been observed so far.
For precedence-constrained problems, constant-factor guarantees for policies were long unavailable. Möhring, Schulz and Uetz (J. ACM 1999) introduced LP relaxations with load inequalities for stochastic scheduling and obtained the first constant-factor policies for independent jobs. In the deterministic setting, Chekuri, Motwani, Natarajan and Stein (SIAM J. Comput. 2001) gave a list scheduling algorithm with deliberate idle times for . Skutella and Uetz (SIAM J. Comput. 2005) combined the two and gave the first constant-factor approximation for stochastic scheduling with precedence constraints and release dates. This mission formalizes that result.
A finite set of jobs is to be scheduled on identical parallel machines, nonpreemptively. Precedence constraints are the arcs of an acyclic digraph: an arc requires to start no earlier than completes, and is a predecessor of if a directed path leads from to . Job has a release date , before which it must not start, and a weight . Following §2 of the paper, release dates are assumed to respect the precedence constraints (Assumption 2.1: whenever is a predecessor of ).
The processing time of job is a random variable with finite mean ; the are stochastically independent. For a realization of the processing times, a feasible schedule assigns start times such that for every arc and at most jobs are in process at any time. A policy maps realizations to feasible schedules; it is nonanticipatory if what it has started by time depends only on what has been observed by . The completion time of under is .
The coefficient of variation is ; the mission assumes for all and some . With , the set function
defines the LP relaxation: minimize subject to for all , for , and .
Algorithm CMNS takes a priority list and a parameter . Whenever a machine is idle and the first job of the residual list (the jobs not yet scheduled) is available, it is scheduled. Otherwise the first available job of the residual list is deliberately delayed; idle machines accumulate deliberate idle time charged to , and once has been charged it is scheduled out of order. The critical chain of a job is traced backwards through critical predecessors (those completing last, after ); its length is .
If is an optimal LP solution, orders the jobs by nondecreasing and , then for every feasible nonanticipatory policy
The theorem gives a policy with a performance guarantee independent of the number of jobs for , using only the expected processing times and a bound on their coefficients of variation. For NBUE distributions () and it yields , matching the deterministic guarantee of Chekuri et al. The analysis separates cleanly into an algorithmic half (Theorem 2.8, valid for arbitrary distributions) and a polyhedral half (load inequalities and Lemma 3.3), both reused for the in-forest results of the same paper and in later work on stochastic scheduling.
The result is proved in the paper; it has no machine-checked proof. Formalizing it produces a precise definition of nonanticipatory policies and of a list scheduling algorithm with deliberate idle times in continuous time, a formal proof of the Möhring–Schulz–Uetz load inequalities, and a verified approximation guarantee for a stochastic scheduling policy.
Lemma 2.6 is the step where the stochastic setting departs from the deterministic one: the set of out-of-order jobs is random and correlated with the schedule, and the identity holds only because the decision to start a job out of order is taken before its processing time is revealed. Making this rigorous requires a formal notion of nonanticipation and an independence argument over a random set. On the algorithmic side, the bookkeeping of deliberate idle time, which accumulates at a rate equal to the number of idle machines, must be made precise at instants where several jobs start, including jobs of length zero. The load inequalities compare every nonanticipatory policy at once and involve second moments of the processing times, so they cannot be checked policy by policy.
Jobs form a finite type; arcs are a relation whose transitive closure is irreflexive; machine capacity is the counting condition "at most jobs in process", with half-open processing intervals. Processing times may be zero. The CV bound is encoded as finite second moments, positive means and .
Algorithm CMNS is characterized by its rules: a decision order nondecreasing in time, the scheduling rule at each decision, and the condition that after the decisions at any time nothing remains to be done. A CMNS policy is a map with this property for every realization. Nonanticipation and measurability of , which the paper asserts without proof (p. 795; §5), are hypotheses. Critical chains use a fixed tie-breaking order.
Standing assumptions and added hypotheses: independence, Assumption 2.1, , and finite means appear in every statement where they are used. is assumed wherever appears (Lemma 2.7, Theorem 2.8), where the page allows with . Lemma 2.6 assumes that is a linear extension, as in the surrounding Lemma 2.5 and Theorem 2.8; with zero processing times it fails otherwise. Comparator policies have integrable completion times and, like , are measurable for the law of , which §5's requirement that every policy be universally measurable implies.
The goal is not trivialized: comparators range over every feasible nonanticipatory policy, not over list policies or the algorithm itself; is optimal over all , not merely feasible; and the expected cost of CMNS is asserted to be finite, so neither side can collapse to a default integral value.
Contributions welcome: proofs of any milestone, in particular Theorem 3.1 and Lemma 3.3, which are reusable for the companion in-forest mission, and a proof that the CMNS rules determine a unique, nonanticipatory, measurable policy.
An investor who trades in a market with fewer stocks than sources of randomness cannot hedge every risk: the market is incomplete. If the investor also faces a liability due at the horizon and has to respect trading constraints (no short sales, limits on positions in certain stocks, a ban on trading some assets altogether), the question of how to trade optimally becomes a constrained stochastic control problem. With exponential utility , its value function gives the investor's utility indifference price of , a standard pricing rule in incomplete markets.
Earlier treatments needed convexity. Cvitanić and Karatzas (Ann. Appl. Probab. 2 (1992)) proved existence and uniqueness for utility maximization in a Brownian filtration with convex constraints, by convex duality. Delbaen, Grandits, Rheinländer, Samperi, Schweizer and Stricker (Math. Finance 12 (2002)) related exponential utility maximization to the martingale measure of minimal relative entropy. El Karoui and Rouge (Math. Finance 10 (2000)) computed the value function and optimal strategy for exponential utility by backward stochastic differential equations (BSDEs), for strategies confined to a convex cone; Sekine (preprint, 2002) obtained the same BSDE from the Cvitanić–Karatzas duality. Hu, Imkeller and Müller (Ann. Appl. Probab. 15 (2005)) gave a direct BSDE solution that works for closed, possibly nonconvex constraint sets, with a bounded liability. The tool is a BSDE whose driver grows quadratically in the control variable, whose solvability rests on Kobylanski's existence theorem for quadratic BSDEs (Ann. Probab. 28 (2000)).
Fix and an -dimensional Brownian motion on a probability space , and let be the -augmentation of the filtration generated by . There are stocks with prices ; the drift and the volatility matrix are predictable and uniformly bounded, and for constants . The market price of risk is .
A strategy is an -valued predictable process , where is the vector of amounts held in the stocks. Its wealth from initial capital is
The constraint is a closed set , not necessarily convex; in terms of it reads . A strategy is admissible, , when , for -a.e. , and is uniformly integrable. The value function is
with and a bounded -measurable liability . For a closed set , and is the set of nearest points.
Let . The BSDE
has a unique solution , the value function is
and there is an optimal strategy with .
In the order of the proof: the bound (4) on and its closedness; the measurable selection Lemma 11 (a), (b); the identity on p. 8 that dictates ; the growth bound (9) and the local Lipschitz estimate of ; existence and uniqueness for (7); the BMO property of Lemma 12; admissibility and optimality of any predictable selection ; and the comparison for every .
The theorem reduces a constrained, nonconvex control problem to a single quadratic BSDE: the value is read off the initial value , and the optimal strategy is a pointwise nearest-point selection from the constraint set. It requires neither convexity nor duality, and it exhibits non-uniqueness of the optimal strategy when has several points. It is the starting point of the quadratic-BSDE approach to utility maximization, indifference pricing and related equilibrium problems.
The result is proved in the paper; nothing in it is open. As far as is known, none of it is formalized: Mathlib has no stochastic integral against Brownian motion, no BSDE theory and no BMO martingales. A complete development would be the first machine-checked solution of a continuous-time portfolio optimization problem by BSDE methods, and its intermediate results (measurable selection of nearest points, the BMO bound for quadratic BSDEs, the verification argument) are reusable.
The deterministic steps (the identity behind the choice of , the growth and Lipschitz bounds) are short. The hard steps are elsewhere. Existence rests on Kobylanski's theorem for BSDEs with quadratic growth, whose proof is a monotone approximation argument with exponential transforms; the Lipschitz theory of Pardoux–Peng does not apply. Uniqueness and the optimality of need the BMO property of and a Girsanov change of measure with a stochastic exponential of a BMO martingale. The selection Lemma 11 (b) cannot use a projection map because is not convex; a measurable choice from a possibly multivalued nearest-point set is required. Finally the verification argument is a localization: is only a local supermartingale, and passing to the limit uses the uniform integrability built into admissibility.
Time is with ; row vectors of are EuclideanSpace ℝ (Fin m) (so is Euclidean) and products such as are inner products. The Brownian motion is the published EthierKurtz.IsStandardBrownian; the filtration and the stochastic integral come from the published module CvitanicKaratzas92_Optimality_Market (IsAugmentedBrownianFiltration, lebP for , and an Itô-integral operator I). Predictability is measurability for Mathlib's Filtration.predictable. The market price of risk and the wealth are computed from the data, not assumed.
Expectations of are minus lower integrals in , and is an extended real: a Bochner expectation would assign the junk value to non-integrable strategies and make them optimal, which is the trivializing formalization to avoid. Existence and uniqueness of the BSDE solution are part of the goal, not hypotheses, and the optimal strategy is a predictable selection of the nearest-point set, not of a choice function.
Disclosed readings: is assumed (otherwise ); constraints and (8) are read -a.e.; ellipticity holds for -a.e. and all ; is a.s. constant and the value identity holds a.s.; uniqueness is in a.s. for each and -a.e.; " given by Lemma 11" is read as any predictable selection; Lemma 11 (b) assumes full rank of . The equivalence of the - and -formulations (Remark 5), the dynamic principle (Proposition 9) and Remarks 2–10 are out of scope.
Needed infrastructure: Itô calculus for continuous semimartingales, stochastic exponentials, BMO martingales and Kazamaki's criterion, Girsanov's theorem, quadratic BSDEs, and measurable selection. Contributions to any of these are welcome; they serve the companion power-utility mission (Theorem 14) as well.
A risk function assigns to an uncertain cost (a function of the random state ) a single number that a decision maker can minimize. Artzner, Delbaen, Eber and Heath (Math. Finance 9, 1999) singled out four axioms, convexity, monotonicity, translation equivariance and positive homogeneity, and called real-valued functions satisfying all four coherent. Föllmer and Schied (Finance Stoch. 6, 2002) and Frittelli and Rosazza Gianin dropped homogeneity to obtain convex risk measures. In each of these works, a central result is a dual representation: the risk function is a supremum of expectations under a family of probability measures, possibly with a penalty.
Ruszczyński and Shapiro (Math. Oper. Res. 31, 2006) place these representations inside general conjugate duality. Their Theorem 2.2 shows that, for any proper, lower semicontinuous, convex risk function on a locally convex space of measurable functions paired with a space of signed measures, the representation holds over the domain of the conjugate, and each remaining axiom corresponds exactly to a property of the measures in that domain. The paper then builds its optimization theory (subdifferentials of composite risk functions, optimality conditions, duality for nonanticipativity constraints) on this representation.
Timeline. Artzner et al. (1999): the coherent axioms, with a representation for finite . Delbaen (2002): coherent measures on under the Fatou property. Föllmer–Schied (2002): convex risk measures on bounded functions. Cheridito, Delbaen and Kupper (2004): spaces of processes. Rockafellar, Uryasev and Zabarankin (2002–2006): the risk envelope in . Ruszczyński–Shapiro (2006): the general paired-space statement formalized here.
Outcomes are costs: smaller values of are better. Let be a measurable space and the space of finite signed measures on it. The mission fixes
Write for the nonnegative functions, for for all , for the nonnegative measures in , and for the probability measures in . Condition (C) requires that every have for some .
A risk function is proper if it never equals and is finite somewhere. The axioms are
The conjugate is , the biconjugate , the dual domain , and the lower semicontinuous hull. In Lean these are pair, PairedSpaces, CondC, IsProper, A1–A4, conj, biconj, dualDom and lscHull in ConvexRiskFn.Dual.
Under condition (C), for proper, lower semicontinuous and convex,
and (i) (A2) holds iff every is nonnegative; (ii) when contains the constant function , (A3) holds iff for all ; (iii) (A4) holds iff for all (2.7).
Under (A1)–(A3), (2.6) holds with ; adding (A4), is the indicator of .
Theorem 2.2 is the unifying statement behind the dual representations of coherent and convex risk measures: one theorem covers bounded measurable functions paired with all finite signed measures, paired with , and weak topologies. Downstream, the paper uses it to describe subdifferentials of risk functions as subsets of , to derive optimality conditions for , and to obtain the risk envelope (2.8) used in distributionally robust optimization.
The result is proved in the paper, assuming Fenchel–Moreau in locally convex spaces as a cited theorem. As far as is known, neither Theorem 2.2 nor Fenchel–Moreau for extended-real functions on a general locally convex space has a machine-checked proof. At the pinned revision Mathlib has geometric Hahn–Banach separation in locally convex spaces but no Fenchel conjugate at all. A formal proof of the goal would yield, in particular, a reusable Fenchel–Moreau theorem for extended-real convex functions under a measure pairing.
The characterizations (i)–(iii) are short once (2.6) is available; the weight sits in (2.6), that is, in Fenchel–Moreau. Its proof separates a point below the epigraph from the closed convex epigraph in , which needs Hahn–Banach in a locally convex space, the identification of the separating functional with a measure in through the compatibility assumption, and a careful case analysis when the separating hyperplane is vertical, a case that occurs because may take the value . The extended-real arithmetic (, ) has to be tracked through every supremum. A finite-dimensional argument does not transfer: is an arbitrary locally convex space, and lower semicontinuity is with respect to its own topology.
is an abstract real vector space with a topology and the instances IsTopologicalAddGroup, ContinuousSMul ℝ, LocallyConvexSpace ℝ (no Hausdorff assumption), mapped injectively and linearly into . is a Submodule ℝ (SignedMeasure Ω). The pairing is the difference of the Bochner integrals against the Jordan parts; integrability against is a field of the structure, so the pairing is never the junk value of a non-integrable integral. The topology of is not modelled, since no statement uses it. Risk functions take values in EReal, and every supremum is an iSup in EReal. The order is pointwise, not almost everywhere. The constant in (A3) is for an element equal to the constant function . Condition (C) is a separate hypothesis, assumed where it is used.
Two statements depart from the page, and both departures are disclosed in their items. Theorem 2.1 carries the extra hypothesis , without which the printed statement is false in infinite dimension; Theorem 2.1 is a cited result, and the goal does not depend on this choice. The indicator-function milestone names the set explicitly instead of "a closed convex subset of ".
The goal mentions neither nor : it is stated about , and alone, and a proof must establish (2.6) from the hypotheses, not assume it. The hypotheses are satisfiable: a one-point with , and meets all of them, including (C) and (A1)–(A4).
Contributions are welcome at every level: Fenchel–Moreau for EReal-valued convex functions on locally convex spaces (reusable well beyond this mission), lemmas about the pairing (linearity, , positivity), and the milestones in the order listed.
The Lasso is the standard estimator for high-dimensional linear regression: from noisy linear measurements of an unknown vector , with possibly much larger than , it minimizes the empirical squared error plus an penalty. Its theoretical guarantees are usually stated as sparsity oracle inequalities: the prediction error of the Lasso is bounded by the best trade-off, over all candidate vectors , between the approximation error of and a term proportional to the number of nonzero components of .
Before this paper, such inequalities for the Lasso carried a leading constant strictly larger than in front of the approximation error. The inequalities of Bunea, Tsybakov and Wegkamp (EJS 2007) and of Bickel, Ritov and Tsybakov (Ann. Statist. 2009, Theorem 6.1) have this form, and the paper notes that sharpness "was not achieved in the previous work on the Lasso" (p. 24). A leading constant larger than means the bound is not informative when the true regression function is far from every sparse linear combination: the inequality then only says that the Lasso is within a constant factor of the best approximation.
Koltchinskii, Lounici and Tsybakov (arXiv:1011.6256v4; Ann. Statist. 39(5), 2011) study nuclear-norm penalized estimation of low-rank matrices in the trace regression model. Their general oracle inequality for a linear subspace of matrices (Theorem 2) has leading constant . Restricted to diagonal matrices with a fixed design, the trace regression model becomes ordinary linear regression and the estimator becomes the Lasso. Section 5.4 of the paper draws the consequence: a sharp (leading constant ) sparsity oracle inequality for the Lasso with Gaussian noise, Theorem 14. This mission formalizes that theorem. The source is the arXiv preprint arXiv:1011.6256v4.
Fix integers and and fixed vectors , the rows of the design matrix . The diagonal elements of the Gram matrix are assumed not larger than . The observations are
with independent random variables, .
For , , and . For , agrees with on and vanishes on . The support of is and the sparsity is its cardinality.
Given , a Lasso estimator is any minimizer
The restricted constant at , with and , is
equal to when the set is empty, and . It is the inverse of a restricted eigenvalue computed at the single support ; the paper obtains it from its matrix quantity for . Finally is the noise vector.
Let with , . With probability at least ,
The event is uniform over all , and the statement holds for every Lasso minimizer.
Theorem 14 gives an oracle inequality for the Lasso whose leading constant is exactly . As a consequence (Corollary 4 of the paper), under the restricted eigenvalue condition RE of Bickel, Ritov and Tsybakov the Lasso's prediction error is at most the best -sparse approximation error plus , which improves the non-sharp inequality of that paper. The bound also shows that the matrix-valued argument of the paper, written for nuclear-norm penalization, specializes cleanly to the vector case; the same argument underlies the matrix completion results of the other missions of this series.
The result is proved in the paper. As far as a search of the platform shows, no formal proof of a sharp oracle inequality for the Lasso exists; the platform has the non-sharp Bickel–Ritov–Tsybakov inequality as an open statement (LassoDantzig.Oracle.theorem_6_1). This mission produces a machine-checked version of the deterministic inequality, of the Gaussian concentration step, and of their combination, with the restricted constant defined exactly as in the paper.
The deterministic part is where the obvious argument fails. The usual Lasso analysis compares the objective at and at a candidate , controls the noise cross term, and rearranges; every version of that argument in the earlier literature loses a multiplicative factor in front of the approximation error , and the factor cannot be pushed to by tuning constants. The sharp bound has to come from a finer use of the optimality of , and the cone constant in is tied to the threshold . Formally, optimality conditions for a nonsmooth convex function on (the subdifferential of ) are infrastructure that has to be in place.
The probabilistic part needs the distribution of a linear combination of independent Gaussians, a Mills-ratio tail bound that is not in Mathlib, and a union bound over coordinates, with the exact constants of the paper.
Vectors are functions Fin p → ℝ, and the design is given by its rows x i : Fin p → ℝ. All statements are in vector form, as the paper itself writes Section 5.4; no matrix library is needed. The Lasso is an argmin predicate, and statements hold for every minimizer; in the goal, is a function of the outcome that is a minimizer at every outcome, and no measurability of is assumed (the bad event is bounded in outer measure).
The restricted constant is formalized through its witnesses: the theorems hold for every in the set whose infimum is . This is equivalent to the infimum, because the bounds are continuous and increasing in . A real-valued infimum would be on an empty set and would make the oracle inequality false, so it is deliberately not used. The infimum over is stated as "for every ", inside the event.
Hypotheses added relative to the page, each disclosed in the item's Formalization Note: (for , and the printed probability divides by zero), , , and measurability of the noise variables. is the paper's standing assumption. The condition is written coordinatewise. In the deterministic milestones the noise is a fixed vector and , which is the paper's for a fixed design and centred noise. No printed slip affects these statements. The constant is kept as printed.
A trivializing formalization would assume the event in the goal, or use a real infimum for ; both are ruled out. Contributions of reusable infrastructure are welcome: the Gaussian tail bound, the law of a weighted sum of independent Gaussians, and the subdifferential of the norm.
The dial-a-ride problem (DARP) asks for minimum-cost vehicle routes that carry users from individual pick-up points to individual drop-off points, subject to vehicle capacities, time windows, route durations and a bound on each user's ride time. It models door-to-door transport for elderly and disabled people, shared taxis and on-demand microtransit. Cordeau (Oper. Res. 54(3), 2006) gave a mixed-integer formulation of the DARP and the first branch-and-cut algorithm for it, and reported that instances with up to 30 users can be solved to optimality in reasonable time. The algorithm's strength comes from families of valid inequalities: linear constraints satisfied by every feasible route plan that cut off fractional points of the linear relaxation. Several of these families were adapted from the precedence-constrained asymmetric TSP (Balas, Fischetti and Pulleyblank 1995; Grötschel and Padberg 1985) and from the pick-up and delivery problem (Ruland and Rodin 1997); others, notably the generalized order-matching inequalities, were new in this paper.
Let be the number of users. Nodes are with pick-up nodes , drop-off nodes , origin depot and destination depot ; user travels from node to node . An instance fixes, for each node , a load , a service duration and a time window ; for each pair of nodes a travel time ; for each vehicle in a finite set a capacity and a maximal route duration ; and a maximal ride time . The standing conditions are , for , and .
A feasible solution gives each vehicle a route through distinct nodes of , start-of-service times and loads such that every node of is visited by exactly one vehicle, and are on the same route with first, and along each travelled arc, the ride time lies in , the route lasts at most , and the time windows and capacity bounds hold at every visited node. These are the constraints (2)–(14) of the paper's model.
The arc variables are when vehicle travels from to , and . For a node set write , , , , and . An inequality in is valid for the DARP when the aggregated arc variables of every feasible solution satisfy it.
Let be distinct users and let satisfy and . Then every feasible solution satisfies
The handle and the teeth are not required to be disjoint from one another beyond , and is arbitrary.
The mission also states the other propositions of §4: the lifted subtour elimination inequalities (33) and (34) (Propositions 1 and 2), the predecessor inequality (30), the two liftings (36) and (37) of the generalized order constraint (Propositions 3 and 4), the redundancy of the strengthening (40) of (39) under (30) for fractional points (Proposition 6), and the infeasible path inequality (41) under the triangle inequality for travel times (Proposition 7).
Valid inequalities are what make branch-and-cut work: each family is added to the linear relaxation by a separation heuristic, and the paper's computational section reports how the bound improves as families are added. Validity is the one property the algorithm cannot check at run time, since a cut that removes a feasible route plan silently returns a suboptimal answer. Remark 2 of the paper observes that (39) is stronger than the TSP comb inequality on the same sets, and Proposition 6 shows that its natural strengthening adds nothing once the predecessor inequalities (30) are present, which tells an implementer which families to separate.
All propositions are proved in the paper, partly in an appendix; none is formalized. A machine-checked development would give a precise route-based model of the DARP that later DARP and pick-up and delivery papers can reuse, and certified validity of the cut families that branch-and-cut codes for these problems separate.
The proofs are short on paper but argue about the shape of routes: "there exists a path connecting all nodes in ", "this path cannot finish at node because of the precedence constraint". Turning a tight subtour count into a single covering path requires knowing that the arcs of a feasible solution inside a subset of form vertex-disjoint paths, which in turn rests on each node of having exactly one predecessor and one successor and on routes containing no cycles. The arithmetic step from tight teeth to the bound on the handle needs the degree identities for every subset of , and counting the arcs leaving needs the distinctness of the users . Reasoning directly with the linear constraints (2)–(14) does not suffice: those constraints alone do not exclude cycles of zero duration.
Nodes are natural numbers, so and appear literally; , , and are Finset.range (2n+2), Icc 1 n, Icc (n+1) (2n) and Icc 1 (2n). All data and arc variables are real-valued, and every right-hand side is computed in . Feasible solutions are route-based: each vehicle has a duplicate-free list of nodes of , and the constraints of the model are imposed along that list. Read literally, the program (1)–(14) admits closed cycles when around a cycle, on which every proposition fails, and imposes (11)–(13) also at nodes a vehicle does not visit; the route encoding follows the paper's verbal definition of the DARP and its proofs, which reason about routes. Precedence ( before ) is a field of the solution, since with zero travel and service times the nonnegativity of ride times does not order the visits. The routing cost plays no role and is omitted. No positivity is assumed for travel or service times.
Added hypotheses, each necessary: sets in the subtour bound and in (30) are nonempty ( gives ); the users of Proposition 5 are distinct; the generalized order constraint (Propositions 3 and 4) has (for it is false); the ordered sets of Propositions 1 and 2 have nodes, the standing assumption of the paragraph that introduces them; Proposition 7 has and a path through distinct nodes. Proposition 6 is the only statement about fractional points: it assumes nonnegativity, no loops, (2), (3) and (30), and drops the remaining constraints of the relaxation, which makes it stronger.
The inequalities are stated for the arc variables of every feasible solution, not for an arbitrary – vector satisfying a few degree constraints; a statement of the latter kind is a different and false theorem. Useful contributions include the path structure of the arcs of a feasible solution inside a subset of , the degree identities, and the milestone proofs, which are reusable for the other propositions.
Principal component analysis estimates the eigenvalues of a population covariance matrix by those of the sample covariance matrix . Before random matrix theory turned to the regime where the dimension grows with the sample size, the classical question was the opposite one: the number of variables is fixed and the number of samples tends to infinity. In that regime almost surely, and the next question is the size and shape of the fluctuations of the sample eigenvalues. When has a repeated eigenvalue, the sample eigenvalues near it do not fluctuate independently: they repel each other, and their joint limit law is that of the eigenvalues of a random Hermitian (or symmetric) matrix. Anderson (1963) derived these limits for real Gaussian samples.
Baik, Ben Arous and Péché (2005) study complex Gaussian samples whose covariance matrix is the identity apart from finitely many "spiked" eigenvalues, and find a phase transition for the largest sample eigenvalue as together. Their Proposition 1.1 is the fixed-dimension counterpart: with fixed and all population eigenvalues equal, fluctuates on the scale with the law of the largest eigenvalue of a Gaussian unitary ensemble (GUE). The paper places it beside its Theorem 1.1(b), where a -fold spike above the critical value gives the same GUE limit when . This mission formalizes Proposition 1.1.
Fix and . A standard complex Gaussian is with independent centred real Gaussians of variance , so . For each , let , , , have independent standard complex Gaussian entries (sampleLaw M k), and let the samples be : mean zero, covariance . The sample covariance matrix is
a Hermitian matrix (sampleCov), and is its largest eigenvalue (largestEig). The general model sampleVec U ℓ G m is specialized to and , because a Hermitian matrix with all eigenvalues equal to is .
Write (vandSq). The finite-GUE distribution (Definition 1.2) is
the distribution function of the largest eigenvalue of a GUE matrix. In Lean these are G k x and Z k.
For every real and every ,
The second statement is in probability.
With , , and :
The proposition identifies the fixed-dimension limit of the top sample eigenvalue under a degenerate population spectrum: the sample eigenvalues near , rescaled by , behave like a GUE spectrum, and like its maximum. For it reduces to the central limit theorem for the sample variance of one complex Gaussian variable, with limit by (29). For general it shows that the GUE limit of the supercritical regime in Theorem 1.1(b) is already present when the dimension does not grow.
The result is proved in the paper (§5, p. 1691) by an exact computation. No machine-checked proof of it, of the complex Wishart eigenvalue density, or of the Gaussian and Laguerre cases of Selberg's integral is known to exist in Mathlib or on the platform. The formalization requires the joint eigenvalue density of a complex Wishart matrix (a Weyl-type integration formula over the unitary group), two Selberg-type integral evaluations, a Stirling asymptotic for products of factorials, and a dominated-convergence argument on . The first three are reusable well beyond this mission.
The limit itself follows from (304) and the constant asymptotics. The hard part is (302): passing from the law of the matrix to the joint law of its eigenvalues. This requires the change of variables with unitary, the Jacobian , and the integration over the unitary group. A direct central limit argument for the entries of gives the Gaussian limit of as a GUE matrix. To get from there to one needs the continuity of the largest eigenvalue in the matrix entries and a matching normalisation, so it is a different route from the paper's. Either route requires spectral facts about Hermitian matrices that Mathlib does not yet package. The Selberg evaluations (27) and (303) are classical but have no short proof: the standard arguments use orthogonal polynomials or an induction with a Dixon–Anderson type integral.
(sampleLaw M k).real of explicit sets.Contributions are welcome on each milestone. Particularly reusable are the complex Wishart eigenvalue density, the Gaussian and Laguerre Selberg integrals, and the measurability and continuity of eigenvalues of Hermitian matrix families.