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?
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.
Markov decision processes assume that the transition law is known exactly. In practice it is estimated from data, and the optimal policy computed for the point estimate can perform badly when the true law differs. 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. The worst case is taken against an adversary (nature) who may choose a law from the set at every step.
For this worst case to be computable by backward induction, the set of path measures of a policy has to decompose epoch by epoch. Garud Iyengar named this property Rectangularity and proved that under it the classical finite horizon theory carries over: a robust Bellman equation holds, and deterministic Markov policies are optimal among all history dependent randomized policies, with state and action sets that may be countably infinite and ambiguity sets that need not be convex (Iyengar, CORC Tech Report TR-2002-07, rev. 2004; published in Math. Oper. Res. 30(2), 2005).
Timeline:
A finite horizon ambiguous Markov decision process (AMDP) has decision epochs , , and a terminal epoch . States lie in a countable set and actions in a countable set . In state at epoch the admissible actions form a nonempty set . For each admissible action , the next state is drawn from some probability measure , where is a nonempty set of probability measures on , the ambiguity set. The decision maker receives when is taken in and the next state is , and at the terminal epoch.
A history at epoch is . A policy assigns to each history a probability measure on . It is deterministic () if every is a point mass, and deterministic Markov () if moreover the chosen action depends on the current state alone. denotes all history dependent randomized policies.
Under Rectangularity (Assumption 1), the set of path measures consistent with is a product of one-epoch sets: nature chooses, for every epoch , every history and every admissible action , a measure , and the path measure is . The robust value of from and the robust value function are
The optimistic values , replace the infimum over by a supremum.
For , depends on only through ; for , ; and
The mission also contains, as a draft theorem that is not a milestone, the per-policy identity of the proof of Theorem 1, eq. (12): for each policy, .
Theorem 2 is the basis of robust dynamic programming in finite horizon: computing an optimal robust policy reduces to backward passes, each a family of one-stage problems . It also justifies restricting attention to deterministic Markov policies, which is what every algorithm in the robust MDP literature computes. Theorem 1 isolates the role of Rectangularity: without it the worst case over path measures does not decompose and the recursion characterizes nothing.
The results are proved on paper; no machine-checked proof is known. The platform holds the finite-state, Markov-controller special case (the Nilim–El Ghaoui RobustMDP series, posed, not proved), whose comparison class is too small to express the claim suffices against . A formal proof here supplies the history dependent policy and adversary machinery on countable spaces that the discounted robust theory and the robust MDP literature reuse.
The obvious argument writes the robust value as an inf–sup over path measures and pushes the infimum inside the expectation epoch by epoch. That step is the content of (12): the infimum of an expectation equals the expectation of an infimum only because nature's continuation choice may depend on the realized action and next state, so near-worst continuations for different branches can be glued into one admissible adversary. Infima need not be attained (the ambiguity sets are arbitrary, the state set countable), so the gluing is an -argument over countably many branches. The supremum over policies needs a matching splicing of -optimal continuation policies (13)–(14). Finally, randomized decision rules must be eliminated (15), which uses Rectangularity again, now per action. Restricting either the policies or the adversary to Markov ones from the start is not allowed: it changes the comparison class and makes the goal circular.
S and one countable action type A serve all epochs; the page's epoch-dependent sets embed into their disjoint union. Epochs are 0-based natural numbers, with terminal epoch M.N and 1 ≤ N.(Fin n → S × A) × S. Probability measures are PMF; as a tsum. The expected reward under a policy and an adversary is computed by backward iterated sums, which is the expectation under the product path measure (3).t < N; the supremum over equals that over the page's because uses only . An adversary chooses for every epoch, history and admissible action.Definitions: AMDP, History, History.extend, IsPolicy, Policy, IsDeterministic, IsDetMarkov, Adversary, Selection, expect, expTail, expectedReward, V, Vstar, Vbar, VbarStar, all in RobustDP.FiniteHorizon. Lemmas about gluing adversaries along history prefixes and about suprema of bounded families indexed by subtypes are reusable. Contributions to any milestone are welcome, in any order; (15) is a one-epoch statement independent of the rest.
A mathematical program with complementarity constraints (MPEC, also called MPCC) is a nonlinear program in which some pairs of constraint functions must be nonnegative with at least one of each pair equal to zero. Such programs model bilevel optimization, Stackelberg games, contact problems in mechanics, and traffic equilibrium design; see Luo, Pang and Ralph, Mathematical Programs with Equilibrium Constraints (Cambridge University Press, 1996). The complementarity constraints make every standard constraint qualification of nonlinear programming fail at every feasible point: neither LICQ nor MFCQ ever holds. Off-the-shelf NLP theory and solvers therefore do not apply directly.
Relaxation methods work around this by replacing the MPEC with a family of ordinary nonlinear programs indexed by a parameter and letting . The oldest of these is the global relaxation of Scholtes (SIAM J. Optim. 11, 2001). The relaxed programs are only useful if they are themselves well posed: a local minimizer of a relaxed program should carry Lagrange multipliers, so that the sequence of KKT points the method computes actually exists. Hoheisel, Kanzow and Schwartz (Preprint 299, Univ. Würzburg, 2010; published in Mathematical Programming) compare five relaxation schemes, prove convergence under weaker MPEC constraint qualifications than before, and ask which standard constraint qualification the relaxed programs satisfy. This mission formalizes their answer for Scholtes' scheme, Theorem 3.2.
A standard nonlinear program (2) on minimizes subject to and for finitely many and . At a feasible , the active set is . A family is positive-linearly dependent if some combination vanishes with and not all coefficients zero. The Mangasarian–Fromovitz constraint qualification (MFCQ) holds at if the gradients are linearly independent and some direction has for every active and for every .
The MPEC (1) minimizes subject to
with continuously differentiable data. At a feasible point the indices of the complementarity pairs split into (), () and (). The tightened program TNLP replaces each pair by equalities on the components that vanish at and a sign constraint on the other. MPEC-MFCQ holds at if standard MFCQ holds for TNLP at .
Scholtes' relaxed program , for , keeps , , , and replaces by . Its feasible set is . Lean notation: the MPEC is MPEC n m p l, TNLP is P.TNLP xs, is P.RS t, and MFCQ of an NLP Q at x is Q.IsMFCQ x.
If is feasible for the MPEC and MPEC-MFCQ holds at , there are a neighbourhood of and such that
The neighbourhood is fixed before and works for every .
Theorem 3.2 says that the relaxed programs inherit a standard constraint qualification from the MPEC. Consequently every local minimizer of near is a KKT point, which is exactly the hypothesis of the convergence theorem for Scholtes' method (Theorem 3.1 of the paper: limits of KKT points of are C-stationary under MPEC-MFCQ). Without it, the convergence theorem could be about sequences that do not exist. The result also replaces the MPEC-LICQ-based regularity results of earlier work by the weaker MPEC-MFCQ.
The theorem is proved in the paper; to our knowledge no part of this theory has been machine-checked. A formal development delivers a reusable layer for nonlinear programming in Lean: positive-linear dependence, MFCQ and its dual characterization, the tightened program of an MPEC and the MPEC constraint qualifications. Sibling missions of this series formalize Theorem 3.1 and the Kadrani–Dussault–Benchakroun relaxation (Theorem 3.5) on the same vocabulary.
The obvious argument is a continuity argument: MFCQ is an open condition, so it should persist near . This fails as stated, because MFCQ for is not a perturbation of MFCQ for TNLP: the two programs have different constraints, and the active set of at changes with and . Near a biactive index , the product constraint can be active, and its gradient tends to zero as . So it cannot be treated as a small perturbation of any gradient in the TNLP family. In addition, the neighbourhood must be uniform in , while the active product constraints depend on . The step that needs care is the regrouping of the multiplier equation of into a combination of TNLP-type gradients, with every coefficient's sign accounted for. The separate step from MPEC-MFCQ to positive-linear independence needs a theorem of the alternative (Motzkin's transposition theorem), which is not in Mathlib in this form.
EuclideanSpace ℝ (Fin n); is the inner product of gradient f x with d. Indices are Fin m (0-based), and are allowed.P.IsC1 on the goal and on milestones 3–5. Milestones 1–2 do not need it.𝓝 xs chosen before .The goal would be trivialized by a weakened MFCQ, for instance one that omits the linear independence of the equality gradients or requires the strict inequality only for some of the active constraints. Such a formalization is ruled out: IsMFCQ requires both conditions, over the full active set of . The neighbourhood must be a genuine element of 𝓝 xs, so an empty is excluded.
Welcome contributions: a proof of Remark 2.2, general lemmas on persistence of positive-linear independence under continuous perturbation, and the final assembly. These lemmas apply to nonlinear programming in general, not only to this mission.
A force whose derivatives decay rapidly can still encode a computation in a particle trajectory. The selected construction makes the observer condition and effectiveness requirements precise. The pinned manuscript supplies the research context.
For each finite deterministic machine and valid input, compilers produce smooth force and velocity fields on nonnegative time and real three-space, with common compact spatial support.
The selected goal is OAI.AlternatingNS.alternating. Its central assertion is
The theorem states that for every positive real viscosity ν computable by rational approximations with error at most 2⁻ⁿ, there exist computable compilers for a force f and velocity U, and one compact set K⊂ℝ³, with the following property for every well-formed finite deterministic Turing machine M and valid finite input w. The compiled programs describe smooth fields f,U on [0,∞)×ℝ³, both spatially supported in K for all nonnegative times, such that every mixed space-time derivative D satisfies sup_{t≥0,x}(1+t+‖x‖)ᴶ‖Df(t,x)‖<∞ and the analogous bound for U, for every nonnegative integer J. Each program supplies rational approximations to all mixed derivatives at rational space-time points with requested error 2⁻ᵏ, effective moduli of continuity on bounded regions, and integer bounds for all these weighted derivative norms. The velocity starts from zero, is divergence-free, and solves the classical forced Navier–Stokes equation ∂ₜU+(U·∇)U=νΔU+f with identically zero pressure; specifically f=∂ₜU+(U·∇)U−νΔU. On every interval [0,T], U is continuous in H² and continuously differentiable in L², and U and its spatial derivative are uniformly bounded in space and time. Moreover, any classical solution (v,p) with the same force and zero initial velocity equals (U,0) pointwise for all nonnegative times, provided on every [0,T] it has v continuous in H², continuously differentiable in L², and uniformly bounded, and p continuous in H¹. Here these Sobolev continuity conditions mean continuous L² representatives of every spatial derivative through the indicated order; time derivatives at zero are taken within [0,∞). Every initial point a has a unique trajectory X(a,t) for t≥0 satisfying X(a,0)=a and ∂ₜX(a,t)=U(t,X(a,t)). Finally, the trajectory starting at (−1,0,0) has strictly positive first coordinate at some nonnegative time if and only if M halts on w, where encountering a missing instruction also counts as halting.
The goal is the alternating-coordinate construction at every positive computable viscosity. It includes Sobolev time regularity, effective bounds, zero initial velocity and the exact observer condition, rather than all three manuscript constructions. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.
The encoding must preserve all weighted derivative bounds and uniqueness in the stated comparison class while recording arbitrarily long computations.
The exact published goal, its hypotheses and its referenced definition blocks specify the requested formalization. The explanatory formula above is a summary; all quantifiers and additional clauses in the linked statement remain required.
The available published material supplies this goal and its necessary definitions. Additional manuscript lemmas are not represented as attached milestones.
adc7f1241b42. Selected goal source.Incompressible transport can implement prescribed geometric operations on coding sheets. The selected statement concerns one such finite transport construction with effective smooth forcing. The pinned manuscript supplies the research context.
Source and target rectangles have rational data and specified positive diagonal ratios. In the formula, D_i(y)=q_i+diag(r_i)(y−p_i), with source and target centers p_i and q_i. Space is represented periodically with period ten, and the viscosity is a positive computable real.
The selected goal is OAI.Solenoidal.sheet_theorem. Its central assertion is
The theorem states that, for any natural number N, any sheet datum D of size N, and any computable real viscosity ν>0, there exist a forcing field f and a velocity field u (each a time-dependent vector field on ℝ³) and a flow map X such that the following hold. Here D consists of N source rectangles and N target rectangles with rational corners, all inside the square [2,3]², with the sources pairwise separated by a positive distance and likewise the targets, together with positive rational ratios in each of two coordinates such that the diagonal affine map from source i to target i, which sends the source center to the target center and scales offsets by the ratios, maps the source rectangle exactly onto the target rectangle. Both f and u are periodic in space with period 10 in every coordinate and are C^∞ in space and time jointly. The forcing f is effective, meaning that all its mixed space-time partial derivatives can be approximated to any rational accuracy by a single fixed partial recursive procedure from computable names of the evaluation point. Moreover f has zero mean over the fundamental cell [0,10)³ at every time, is divergence free, and is 1-periodic in time. The field u is a classical solution on t≥0 of the forced Navier–Stokes equations ∂ₜu + (u·∇)u = −∇p + ν Δu + f with zero pressure, zero initial data, incompressibility and spatial periodicity, so u is a solution driven by f without pressure. Any classical solution v with pressure p for the same f and ν and with zero initial velocity coincides with u, and has p identically zero, for all t≥0. The flow map X satisfies X(0,a)=a and solves the particle-path equation dX/dt=u(t,X) for t≥0, and for each i and each point y of the i-th source rectangle, the time-1 flow image of the sheet point (y₀,y₁,2) agrees modulo the torus ℝ³/(10ℤ)³ with the sheet point at the diagonal-map image of y. Further, u vanishes in a neighborhood of every integer time, the advection term (u·∇)u vanishes everywhere, and both f and u have all their mixed space-time derivatives uniformly bounded by rational bounds computable from the derivative multi-index by a fixed partial recursive procedure. Finally, if N=0 then f and u are identically zero.
The target is the sheet theorem, including its encoded uniqueness statement and zero-advection conditions. Machine-halting detection is not a conclusion of this published goal. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.
The construction must simultaneously enforce smoothness, incompressibility, temporal periodicity, effective bounds and exact transport on every point of each sheet rectangle.
The exact published goal, its hypotheses and its referenced definition blocks specify the requested formalization. The explanatory formula above is a summary; all quantifiers and additional clauses in the linked statement remain required.
The available published material supplies this goal and its necessary definitions. Additional manuscript lemmas are not represented as attached milestones.
adc7f1241b42. Selected goal source.Homogeneous minimizers model possible free-boundary singularities. A nonflat example in seven dimensions supplies one side of the claimed critical-dimension threshold. The pinned manuscript supplies the research context.
The one-phase Bernoulli energy on a ball is the integral of squared weak gradient plus the indicator of positivity. Competitors are nonnegative Sobolev functions with the prescribed H1-zero-boundary difference.
The selected goal is OAI.Bernoulli.nonflat_in_seven. Its central assertion is
The theorem states that there exists a function u: ℝ⁷ → ℝ that is nonnegative almost everywhere, belongs locally to H¹, and is a global minimizer of the one-phase Bernoulli energy E_B(u) = ∫B (|∇u|² + 1{u>0}) dx. Here ∇u is a distributional gradient, and global minimality means that, for every open ball B of positive radius and every nonnegative almost-everywhere Sobolev competitor v ∈ H¹(B) with v − u ∈ H¹₀(B), one has E_B(u) ≤ E_B(v). Membership in H¹₀(B) requires approximation by smooth functions compactly supported in B, with both the functions and their gradients converging in L². The function is nonzero in the sense that it is not equal to zero almost everywhere, and it is homogeneous of degree one: for each real r > 0, u(rx) = r u(x) for almost every x. Nevertheless, it is not flat: there is no unit vector e ∈ ℝ⁷ for which u(x) = max(⟨x,e⟩, 0) almost everywhere. All almost-everywhere statements and integrals use Lebesgue measure.
The selected goal is existence of a nonzero nonflat one-homogeneous global minimizer in dimension seven. Flatness in dimensions at most six and singular-set dimension bounds are not attached conclusions. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.
A stationary cone is insufficient: the example must minimize against all admissible ball competitors and fail every half-space profile.
The exact published goal, its hypotheses and its referenced definition blocks specify the requested formalization. The explanatory formula above is a summary; all quantifiers and additional clauses in the linked statement remain required.
The available published material supplies this goal and its necessary definitions. Additional manuscript lemmas are not represented as attached milestones.
adc7f1241b42. Selected goal source.Negative curvature suggests strong analytic control, but bounded holomorphic coordinates impose a different global condition. The target constructs a complex threefold separating them. The pinned manuscript supplies the research context.
The construction uses the encoded Hartogs domain and a complete Kähler metric with sectional curvature between two negative constants. Holomorphic coordinate obstructions are stated in the published main proposition.
The selected goal is OAI.PinchedHartogs.main_theorem. Its central assertion is
The theorem states that there exist a subset M of ℂ³ (realized as ℂ² × ℂ) and a matrix-valued function g assigning a 3×3 complex matrix to each point, together with real numbers A and B, such that M is open, nonempty and contractible, and g is a Kähler metric on M, meaning g is C^∞ on M, Hermitian at each point (g_ij = conj(g_ji)), positive definite (the Hermitian form of g at u has positive real part for every nonzero u), and satisfies the closedness condition ∂g_kj/∂z_i = ∂g_ij/∂z_k, with ∂ the Wirtinger derivative (1/2)(∂_x − i∂_y). Moreover the metric is geodesically complete on M: for every point p in M and every vector v there is a C^∞ curve γ: ℝ → M with γ(0)=p, γ'(0)=v that satisfies the geodesic equation γ''k + Σ Γ^k{ac} γ'_a γ'_c = 0 for all t, where the Christoffel symbols are built from the inverse of g and the ∂ derivatives of g. The metric is also negatively pinched: 0 < A ≤ B and, for every point of M and every real-linearly independent pair u, v, the sectional curvature, computed from the explicit curvature tensor formula in the source, lies between −B and −A. In addition, M has no bounded coordinates: there is no map F from ℂ³ to ℂ³, holomorphic on a neighbourhood of every point of M and bounded in every component on M, whose complex Jacobian determinant is nonzero at every point of M. Finally, M is not biholomorphic to a bounded domain, that is, there is no bounded open set N with holomorphic maps F on M and G on N, each analytic near the respective set, mapping M into N and N into M, which are mutually inverse.
The selected main theorem requires a nonempty open contractible domain, a geodesically complete Kähler metric with two-sided negative real-sectional pinching, no bounded holomorphic map to complex three-space with everywhere-nonsingular differential, and no biholomorphism to a bounded domain. The controlled potential and metric-transfer statements are attached as supporting milestones. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.
Metric completeness and two-sided negative curvature must coexist with a global obstruction to bounded holomorphic coordinates.
The exact published goal, its hypotheses and its referenced definition blocks specify the requested formalization. The explanatory formula above is a summary; all quantifiers and additional clauses in the linked statement remain required.
Additional published targets are included as separate references:
adc7f1241b42. Selected goal source.Affine maximal graphs satisfy a nonlinear fourth-order geometric equation. The target asks whether completeness forces such a locally uniformly convex graph to be a paraboloid. The pinned manuscript supplies the research context.
The dimension is between three and nine. The domain is nonempty, open and convex, the function is smooth with positive-definite Hessian, and completeness uses intrinsic Euclidean graph length.
The selected goal is OAI.AffineBernstein.affine_bernstein. Its central assertion is
The theorem states that, for every integer dimension 3 ≤ n ≤ 9, a nonempty open convex set Ω ⊆ ℝⁿ and a function u : ℝⁿ → ℝ that is smooth on Ω satisfy the following conclusion under three hypotheses. First, the Hessian H = D²u is positive definite at every point of Ω. Second, u satisfies the affine maximal equation ∑ᵢⱼ Uᵢⱼ ∂ᵢ∂ⱼw = 0 throughout Ω, where U = (det H)H⁻¹ and w = (det H)^{−(n+1)/(n+2)}. Third, the graph is complete for its intrinsic Euclidean path distance: the distance between x and y in Ω is the infimum over C¹ paths γ in Ω joining them of ∫₀¹ √(‖γ′(t)‖² + (Du(γ(t))γ′(t))²) dt, and every Cauchy sequence for this distance has a limit in Ω for the same distance. Then Ω = ℝⁿ and there exist a symmetric positive definite real n × n matrix A, a vector b ∈ ℝⁿ, and c ∈ ℝ such that u(x) = ½xᵀAx + b·x + c for every x ∈ ℝⁿ. Moreover, an invertible affine map of ℝⁿ × ℝ carries the standard paraboloid {(x, ‖x‖²)} onto the graph {(x, u(x)) : x ∈ Ω}.
The goal also gives an invertible affine map from the standard paraboloid to the graph. The wider immersed-hypersurface formulation is not included as a separate target. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.
The domain is not initially assumed to be all of space. Both global domain exhaustion and the quadratic form must follow from the equation and completeness.
The exact published goal, its hypotheses and its referenced definition blocks specify the requested formalization. The explanatory formula above is a summary; all quantifiers and additional clauses in the linked statement remain required.
The available published material supplies this goal and its necessary definitions. Additional manuscript lemmas are not represented as attached milestones.
adc7f1241b42. Selected goal source.Recursive potentials can define tree norms with controlled midpoint behavior. The central question is whether that control forces an asymptotically uniformly convex renorming. The pinned manuscript supplies the research context.
The encoded constructions include root-sum and zero-root completions, finite tree heads, aggregation spaces and variable-exponent coordinate models. Two least nonnegative potential fields determine the norms.
The selected goal is OAI.ComparatorModel.RecursivePotentials.main. Its central assertion is
The theorem states (its proof is admitted with sorry) that the defined proposition MainClaim holds. MainClaim asserts that there exist constructions, over index types in universe 0, of the finite rooted tree head structure, the tree-vector spaces, the zero-root tree-vector spaces, the aggregation-vector spaces, and their l^p-coordinate models, such that eleven statements about completions of finite-support vectors on rooted trees hold simultaneously. These comprise: (1) completion statements saying that the root-sum tree space for the sequence tree and for the joined tree, and the zero-root space for the joined tree, are complete, infinite-dimensional, with continuous coordinates extending the vector coordinates, continuous potential fields P and Q extending the finite-tree ones, norm equal to P+Q at the root (or both P and Q at the root in the zero-root case, where the root coordinate vanishes), and with norm-nonincreasing idempotent coordinate projections onto initial subtrees having finite-dimensional range, closed finite-codimensional tails and approximation of tail elements by vectors vanishing on the head, and that XZero and XJoined are reflexive; (2) a main statement giving the lower bound t^3/128 on the averaged modulus of XSigma and XJoined for 0<t<1, a cubic-type uniform convexity inequality (‖x+z‖+‖x-z‖)/2 ≥ ‖x‖+‖z‖^3/(8(2‖x‖+‖z‖)^2) for x supported on a head and z vanishing there, and that no equivalent norm on XSigma, XZero or XJoined has the AUC property (positive modulus at every positive t); (3) positivity of the averaged modulus of XSigma at every positive radius t; (4) a separation statement for XJoined: for each ε>0 there is η in (0,1), equal to min(1/2, logarithmicGamma(2, ε/16)) when ε≤2, such that if ‖x±z_n‖≤1 for all n and the z_n are pairwise at distance at least ε, then ‖x‖≤1-η; (5) properties of the variable-exponent l^2-sum of height-h tree spaces with exponents 1+1/h, namely completeness, reflexivity, separable dual, a root-sum functional ν (nonnegative, definite, subadditive, absolutely homogeneous) bounded above and below by explicit multiples of the l^p norm, dense finitely supported vectors, and finite-rank projections; (6) a recursive characterization of the l^p-model potentials by least pairs, with ν equal to the root P plus Q; (7) for every equivalent norm A on the variable space, the modulus at lower/upper vanishes; (8) the absence of any equivalent AUC norm there; (9) a sixth-power stability inequality and (10) a cubic stability inequality for admissible heads, with explicit constants; and (11) a weak-tail estimate: if x and a weakly null sequence y_j with ‖y_j‖≥ε, 0<ε≤1, satisfy ‖x±y_j‖≤1, then ‖x‖≤θ(ε)<1.
The published MainClaim is an eleven-part package, not only the displayed midpoint inequality. Its additional completion, separation, stability, weak-tail and no-AUC assertions remain part of the goal. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.
The bundled target must coordinate completion, continuous coordinate maps, finite-head approximations, reflexivity and uniform estimates across several related spaces.
The exact published goal, its hypotheses and its referenced definition blocks specify the requested formalization. The explanatory formula above is a summary; all quantifiers and additional clauses in the linked statement remain required.
The available published material supplies this goal and its necessary definitions. Additional manuscript lemmas are not represented as attached milestones.
adc7f1241b42. Selected goal source.