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?
Polynomial optimization asks for the minimum of a polynomial over a set cut out by polynomial inequalities. Lasserre's moment relaxation (Lasserre 2001) replaces the minimization over points by a minimization over probability measures on , and then over linear functionals on polynomials that satisfy semidefinite constraints. The bridge between measures and semidefinite constraints is Putinar's theorem (Putinar 1993): on a compact basic semialgebraic set with an Archimedean description, a linear functional comes from a measure exactly when it is nonnegative on the quadratic module of the constraints.
Many problems of practical size are invariant under a group of linear transformations: permutations of variables, sign changes, rotations of a polygon. Gatermann and Parrilo (2004) showed how such symmetry block-diagonalizes sums-of-squares programs. Riener, Theobald, Jansson Andrén and Lasserre (arXiv:1103.0486, Math. Oper. Res. 2013) carry the reduction to the moment side. Their first step, Theorem 3.2, is a symmetric version of Putinar's theorem: for invariant data it suffices to consider functionals that are themselves invariant, and these are characterized by positivity of symmetrized localizing forms. This mission formalizes that theorem.
Write . Let be a finite subgroup of . A matrix acts on points by and on polynomials by
the linear substitution . A polynomial is -invariant if for every .
Fix and the feasible set
Assumption 2.1 requires to be compact and some polynomial , with sums of squares , to have a compact superlevel set . Put .
A linear map is -linear if for all and all . Its symmetrized localizing forms are
For a Borel measure on , is its image under , and is -invariant if for all . A measure on is one with .
If the are -invariant and Assumption 2.1 holds, then for a -linear :
The result. Theorem 3.2 turns the moment relaxation of a -invariant problem into one over -linear functionals. Such a functional is determined by its values on the invariant ring , so its moment variables are indexed by a basis of invariants instead of all monomials (Example 3.3 of the paper: five variables instead of fifteen for on in degree 2). The block-diagonalized relaxations and the convergence result of §3 (Theorems 3.4–3.7) rest on it.
Formalizing it. The theorem is proved in the paper, modulo Putinar's theorem, which is cited. Neither Putinar's theorem nor any Archimedean Positivstellensatz is in Mathlib or on the platform. A complete formalization therefore needs (i) Putinar's theorem itself, in its dual moment form, and (ii) the determinacy of compactly supported finite measures by polynomial moments in several variables. Both are reusable well beyond this paper: every moment-SOS hierarchy result in the literature cites them.
The group-theoretic steps (milestones 2–4) are finite averaging and change of variables. The weight of the theorem sits in two analytic facts. The first is Putinar's theorem: nonnegativity on the quadratic module is an algebraic condition, and producing a measure from it requires the Archimedean hypothesis of Assumption 2.1 in an essential way; without that hypothesis the statement is false in general. The second is that the measure Putinar's theorem returns has to be shown -invariant. Equality of the polynomial moments of and does not by itself identify two measures; it does so here because both are finite and carried by a compact set, where polynomials are dense in the continuous functions. A further detail: Putinar's theorem is stated for normalized functionals, and Theorem 3.2 is not normalized, so the degenerate case must be shown to force .
Polynomials are MvPolynomial (Fin n) ℝ, points Fin n → ℝ, and a Subgroup (GL (Fin n) ℝ) with a Fintype instance. The action on polynomials is the linear substitution aeval, so is an arbitrary finite matrix group, not only a permutation group. Sums of squares are Mathlib's IsSumSq. "psd" for the symmetric form means for every polynomial , with no degree truncation; () is included. Measures live on the Borel σ-algebra of , is Measure.map along the continuous (hence measurable) map , and "measure on " is .
Committed conventions and disclosed readings:
Trivializing formalizations are ruled out: integrals are taken only against finite measures carried by a compact set, so no statement holds because a Bochner integral of a non-integrable function is ; positivity is through the forms on all of , not replaced by pointwise nonnegativity; and the invariance of is a conclusion of milestone 5, never a hypothesis.
Contributions welcome: Putinar's theorem (milestone 1) and multivariate moment determinacy on compact sets are the reusable infrastructure; the averaging milestones are a natural first entry point.
A proper coloring of a graph assigns colors to its vertices so that adjacent vertices get different colors; the least number of colors that suffices is the chromatic number . The clique number is the size of a largest set of pairwise adjacent vertices, and always. A class of graphs is -bounded if is bounded by a function of on the class. Abstract triangle-free graphs () of arbitrarily large chromatic number have been known since Zykov (1949) and Mycielski (1955), so the question is which geometric classes are -bounded.
For geometric intersection graphs (one vertex per set, an edge for each intersecting pair) the history is as follows.
The same construction disproves Scott's conjecture (1997) that graphs excluding induced subdivisions of a fixed graph are -bounded, as first observed by Fox and Pach.
Points of the plane are pairs . A line segment is a closed set with two distinct endpoints . A family of segments is a finite indexed list of pairwise distinct segments. Its intersection graph has vertex set , and are adjacent exactly when . The family is triangle-free if no three of its segments pairwise intersect, and is the chromatic number of its intersection graph.
The milestones use the paper's auxiliary notions. An axis-aligned rectangle is , with and . For a family inside the open interior of , a probe for is a rectangle sharing the right edge line of such that (i) and ; (ii) no segment meets the left edge of ; (iii) no segment has an endpoint in the closed rectangle ; (iv) the segments meeting are pairwise disjoint. The diagonal runs from the bottom-left corner to the top-right corner of . The sequences are given by , and .
For every integer there is a finite family of distinct line segments in the plane with triangle-free intersection graph and
The goal fixes no size for and no particular construction.
Theorem 1 shows that segment intersection graphs are not -bounded, and it settles negatively the question for every class containing them: intersection graphs of curves crossing at most once (Kratochvíl–Nešetřil), McGuinness's class of arcwise connected sets with connected pairwise intersections, and string graphs in general. Through the Fox–Pach observation it refutes Scott's conjecture on induced subdivisions, a purely graph-theoretic statement. The counts in Lemma 2 give , so the maximum chromatic number of a triangle-free family of segments is (§4 of the paper). The family has the same intersection graph as Burling's boxes.
The theorem is proved on paper; to the best of current knowledge no machine-checked proof exists. The mission produces a Lean 4 statement of the result about actual segments in , a reusable definition of intersection graphs of plane sets, and the paper's probe machinery stated precisely enough to support a full formal proof.
Abstract triangle-free graphs with large chromatic number are easy to build, but almost none of them are intersection graphs of segments, and the standard constructions (Mycielski, Zykov, shift graphs) do not come with a geometric realization. The difficulty is geometric: the construction has to place every new segment so that it meets exactly a prescribed independent set of old segments and nothing else, at every level of a doubly exponential nesting, while keeping finitely many rectangles disjoint and segment endpoints out of them. In a formal development the burden falls on the planar facts the paper treats as evident in one line each: which edges of a rectangle a segment can cross, when two segments must cross, and why the probe conditions survive when families are nested inside one another.
ℝ × ℝ (first coordinate , second ), and segments are Mathlib's closed segment ℝ u v. A family is e : Fin N → (ℝ × ℝ) × (ℝ × ℝ) (endpoint pairs) with seg (e i) the -th segment. "A family of line segments" is read as non-degenerate ((e i).1 ≠ (e i).2) and pairwise distinct (Function.Injective (fun i => seg (e i))).interGraph F : SimpleGraph ι is the intersection graph of an indexed family of plane sets: i ≠ j ∧ (F i ∩ F j).Nonempty. Triangle-free is CliqueFree 3; is Mathlib's chromaticNumber : ℕ∞, and the goal states the literal .Rect = ⟨a, c, b, d⟩ for , with positive area as a separate hypothesis. A probe is stored as and is the closed rectangle ; the interior of is open.sSeq k, pSeq k are , 1-based; every statement assumes (the value at is junk).ncard of the image of those segments.Needed infrastructure: elementary planar geometry of segments and axis-aligned rectangles (membership, edges, crossing of two segments via the intermediate value theorem), affine images of segment families, and finite coloring counts. The segment and intersection-graph definitions are reusable for other questions on geometric intersection graphs. Contributions are welcome on any milestone, in particular a complete proof of the diagonal claim and of the induction step.
Training a model in machine learning usually means minimizing a nonconvex function with first-order methods. Finding a global minimum of a general nonconvex function is NP-hard, so the classical guarantee for gradient descent (GD), , is weaker: with step size it reaches a point with within iterations, independently of the dimension (Nesterov, 1998). Such a point can be a saddle point. For many learning problems (matrix sensing and completion, phase retrieval, dictionary learning, tensor decomposition), every approximate second-order stationary point is an approximate global minimum, so an algorithm that avoids saddle points solves the problem.
Jin, Netrapalli, Ge, Kakade and Jordan (arXiv:1902.04811, J. ACM 2021) show that simple perturbed versions of GD and SGD find approximate second-order stationary points in essentially the number of iterations GD needs for first-order stationarity, up to polylogarithmic factors in the dimension. Their §5 gives a short, self-contained proof for a variant of perturbed GD (Algorithm 4). That proof is the subject of this mission.
Timeline:
Let , , with gradient and Hessian ; is the Euclidean norm on vectors and the spectral norm on matrices. Assumption A: is -gradient Lipschitz, , and -Hessian Lipschitz, . A point is an -second-order stationary point (-SOSP) if
Write and .
Algorithm 4 (Perturbed GD, Variant). With step size , radius , time interval and tolerance , start with . At iteration : if and , replace by with and set ; then . The parameters are those of Eq. (6):
where is a logarithmic factor, and .
For (which equals ) and every with
with probability at least over the perturbations,
The paper writes the count as with .
The result. Theorem 18 says that adding occasional small random perturbations to gradient descent costs only a polylogarithmic factor over the first-order rate and buys second-order stationarity. Combined with the landscape results above, it gives polynomial-time guarantees for gradient methods on those learning problems. Lemma 20, on its own, is a quantitative statement that strict saddle points are unstable under perturbed GD; Lemmas 21 and 22 are reusable tools for any analysis of first-order methods near saddle points.
Formalizing it. The results are proved in the paper; none of them is formalized. A formal development would give machine-checked versions of the descent lemma for Hessian-Lipschitz functions, the improve-or-localize lemma, the coupling argument and the probabilistic escape bound. It would also settle the issue disclosed under Formalization scope.
Lemmas 19 and 21 are short. The difficulty is in Lemma 22 and Lemma 20. The obvious approach, linearizing GD around the saddle and following the unstable eigendirection, fails because the stuck region (starting points that do not escape within steps) has no simple shape once is not quadratic. The coupling argument controls the difference of two runs instead. It needs an induction in which the non-quadratic error term stays below half of the leading term for all steps, with the constants of Eq. (6) used exactly (). Lemma 20 then turns a statement about pairs of points into a measure bound: a set whose every line parallel to meets it in a segment of length at most has volume at most times the -volume of the ball. In Lean this needs Fubini over a rotated coordinate system and measurability of the stuck region. Theorem 18 requires a probabilistic accounting over the whole run, under the product law of the perturbations.
is EuclideanSpace ℝ (Fin d) with . The Hessian is fderiv ℝ (gradient f) x, the derivative of the gradient map, with the operator norm. Statements about use the quadratic form: is "some unit has ", and is " for all ". is normalized Lebesgue measure on the open ball. Algorithm 4 is a deterministic function of the perturbation vectors, which have the product law on . The -th iterate is the point tested at the start of iteration , and "half of its iterations" counts . Probability statements bound the failure event from above.
The paper's is instantiated as the proof does:
A Hessian not tied to , an arbitrary unit vector in place of the bottom eigenvector in Lemma 22, a per-realization or existential statement in place of the product-law probability, or a vacuous would each trivialize the statements; none is used.
Disclosed gap. The proof of Theorem 18 (p. 16) bounds the number of perturbations by applying Lemma 20 at each one. Algorithm 4 also perturbs at points that are already -SOSPs, where Lemma 20 does not apply, and the iterations after such a perturbation are not counted. The goal is posed as printed; a solver who finds it false should report this in the discussion. The milestones do not depend on the gap.
Needed infrastructure: second-order Taylor bounds for Hessian-Lipschitz functions, symmetry of the Hessian and existence of a bottom eigenvector, volumes of Euclidean balls (in Mathlib through ), a Fubini-type slicing bound for sets of bounded width along a direction, and measurability of the GD iterates. The volume-ratio and slicing lemmas are reusable beyond this mission. Proofs of any milestone, and alternative proofs, are welcome.
Wasserstein distributionally robust optimization (DRO) hedges a decision against every probability distribution within a given transport distance of a nominal one, typically the empirical distribution of data. The inner problem, the worst-case loss, is an optimization over an infinite-dimensional set of measures, and every practical use of Wasserstein DRO — tractable reformulations, statistical guarantees, regularization interpretations — rests on a strong duality theorem that replaces it with a one-dimensional minimization over a Lagrange multiplier.
Such duality theorems have been proved under progressively weaker hypotheses:
This mission formalizes the last of these, Theorem 1 of Zhang–Yang–Gao.
Let be a probability space, a measurable loss with , and a measurable transport cost with (Assumption 1). Expectations take values in , and the convention is used for products .
The Kantorovich transport cost between and a probability measure is
where is the set of couplings with marginals and . The worst-case loss is
with for . For let and
is the set of probability measures on with first marginal . A measurable satisfies the interchangeability principle (IP) if is -measurable (measurable for the completion of ) and
The Legendre transform of is .
satisfies (IP) for every if and only if the supremum functions are -measurable and
The minimum is attained. Both sides may be .
The result. Theorem 1 separates Wasserstein DRO duality into two parts. The first, the second display, holds with no regularity at all: the worst-case loss always equals a one-dimensional minimum over of a supremum over couplings with fixed first marginal. The second identifies exactly when that supremum can be moved inside the expectation, which is the form (D) used in applications: (D) holds for all radii if and only if (IP) holds. The question of when Wasserstein DRO has its standard dual becomes a question about measurable selection and measurable projection, which is studied in a companion mission of this series. The duality results of the timeline above become special cases in which (IP) can be verified.
Formalizing it. The results are proved in the paper; none of them has a machine-checked proof. A formalization produces a verified duality theorem at the level of generality of measurable spaces with extended-valued costs, together with a reusable layer: Kantorovich costs with values in , extended-real expectations, and one-dimensional Legendre transforms of extended-real functions.
The proof is short on paper because it delegates to one-dimensional convex analysis: the involution of the Legendre transform on (Rockafellar, Theorem 12.2), applied to . The work is in the extended reals. can be on all of , can be identically , and the costs and products involve . Concavity of on requires mixing near-optimal distributions and couplings, and lower semi-continuity of requires Fatou's lemma for functions bounded below by , not by . The "only if" direction of the goal has to recover (IP) for every from (D), which goes through biconjugation of and the right continuity at of both transforms. A proof that treats every value as finite does not cover the theorem.
The Lean development lives in the namespace ShortWDRODual.Legendre.
ENNReal-valued and curried, c x̂ x, with the nominal point first. The loss is real-valued and measurable.RWPI.SqrtLasso.transportCost (infimum over probability couplings of the lower Lebesgue integral of , in ).ModelRiskOT.Duality.extIntegral, in EReal. This agrees with the paper whenever one part is finite. It assigns to the undefined case , so a law or coupling with an undefined expectation never raises a supremum.EReal, so that for . Reading it as would make every Legendre transform .IsLeast). Concavity, convexity and monotonicity of extended-real functions are stated as explicit inequalities with real weights. Lower semi-continuity "on " is relative to .NullMeasurable. Disclosed reading: in the goal and in the fixed- milestone, the measurability of the supremum functions is stated explicitly next to the duality formula, because the paper's expectation in (D) presupposes it and (IP) contains it. Lemma 2's statement on assumes this measurability for , for the same reason.A complete development needs the one-dimensional Fenchel–Moreau theorem for extended-real functions on , gluing and mixing of couplings with a fixed first marginal, and Fatou's lemma for extIntegral. Each is reusable well beyond this mission. Contributions of any of these as separate lemmas are welcome.
A constraint on a decision requires the distribution of the random vector . In practice that distribution is known only partially: its support, a few moments, or the probability mass of some regions estimated from data. Distributionally robust optimization asks that the constraint hold for every distribution consistent with this information. Wiesemann, Kuhn and Sim (Optimization Online 3757, 2013; Oper. Res. 62(6), 2014) proposed one standardized format for this information. Their format contains, as special cases, many ambiguity sets used earlier: support and moment information (Delage and Ye, 2010), and mean–covariance and directional-deviation information (Goh and Sim, 2010). They then characterized exactly when a worst-case expectation constraint over such a set has a finite conic reformulation. This mission formalizes that characterization: the paper's Theorem 1 and the steps of its proof.
The uncertain parameters are , and an auxiliary random vector may be added to describe structure of . A proper cone is a closed convex cone with and nonempty interior. Write for , and for the dual cone. For indices the confidence sets are
with matrices , vectors and proper cones . The ambiguity set is
where . The paper imposes three conditions:
The distributionally robust constraint (3) is for all .
A set is strictly included in , written , if lies in the interior of . The nesting condition (N) requires that any two distinct confidence sets be strictly nested or disjoint. For each , indexes the confidence sets containing .
Under (C1)–(C3), (N) and the two regularity conditions (S1)–(S2) described below, the constraint (3) holds if and only if there are , and such that, for all and ,
When the are orthants, second-order cones or semidefinite cones, Theorem 1 turns the semi-infinite, measure-valued constraint (3) into a linear, conic-quadratic or semidefinite system of size polynomial in the data. The paper's Theorem 2 shows that when nesting fails, even checking is strongly NP-hard. Theorem 1 is therefore the tractable side of a sharp dividing line. The paper builds its conservative approximation for non-nested sets (Theorem 3) and its lifting results (Section 3) on it.
The result is proved in the paper; nothing here is open. The formalization contributes two things. First, the duality theory for finite moment problems over measures on a compact set, and conic strong duality for strictly feasible sets: neither exists in Mathlib as stated. Second, a corrected statement. As printed, the "only if" direction of Theorem 1 is false, because (C2) does not give the strong duality the proof attributes to it. No machine-checked version of Theorem 1 is known.
The sufficiency half is weak duality: a pointwise inequality on integrated against any . The necessity half needs three facts.
Vectors are Fin n → ℝ, products are Matrix.mulVec and dotProduct, and the outcome space is (Fin nP → ℝ) × (Fin nQ → ℝ) with its Borel -algebra. The index set is Fin (nI + 1), 0-based, with = Fin.last nI. Probabilities are μ.real. Constraint (3) is stated in its "for all " form, so no supremum of reals appears. The scalar and the vector are separate fields.
Every member of is a probability measure with finite first moment, so is a genuine integral and not Lean's default value . The expectation is genuine as well, since grows at most linearly. Hypothesis (C2) keeps nonempty, so (3) cannot hold vacuously. A sorry-free sanity file exhibits two nested intervals for which all hypotheses of the goal hold at once.
Hypotheses added to the paper's, each needed for a true statement:
(S1) also excludes some instances the page allows: or for , and expectation rows that cannot be shifted in every direction by measures on .
The sufficiency milestone drops (C2) and the standing bounds , which only strengthens it.
Needed infrastructure, all reusable: conic duality for closed convex cones, Lagrangian duality for linear programs over finite measures on a compact set, and the extension of a convex inequality from the boundary of a compact set. Contributions of any of these as separate lemmas are welcome.
Lasserre's hierarchy is a sequence of semidefinite relaxations for minimizing a polynomial over a set defined by polynomial equations and inequalities (Lasserre 2001). Under the archimedean condition its optimal values converge to the true minimum, but only asymptotically in general; in practice the hierarchy is often exact at a small relaxation order. J. Nie's paper (arXiv:1206.0319v2, Math. Program. 146 (2014)) explains this gap in two steps. Its Theorem 1.1 shows that finite convergence follows when the classical optimality conditions of nonlinear programming hold at every global minimizer. Its Theorem 1.2, the subject of this mission, shows that those optimality conditions hold at every local minimizer for all input data outside the zero set of finitely many polynomials in the coefficients. Together the two results give finite convergence of Lasserre's hierarchy for generic archimedean problems.
The genericity statement is also of independent interest in nonlinear programming: it says that degenerate local minimizers (failing constraint qualification, strict complementarity or second order sufficiency) are an algebraically exceptional phenomenon for polynomial data of fixed degrees.
Fix variables and write for the real polynomials of degree at most . Problem (1.1) is
with feasible set . For the active set is . At :
The input data are the coefficient vectors of ; a polynomial in the coefficients is a real polynomial evaluated at that vector. The paper's Condition 4.3 lists four families of such polynomials: resultants and discriminants (§2.4) of subsets of the constraints, and the polynomials of (4.6) and of (4.11), which detect a complex projective solution of the homogenised critical-point systems (4.5) and (4.10). Homogenisation is at the nominal degree , with .
For positive degrees there are polynomials in the coefficients such that
The theorem gives the second half of the paper's explanation of finite convergence: combined with Theorem 1.1, Lasserre's hierarchy converges in finitely many steps for all archimedean problems with input outside a proper algebraic subset. Section 5 of the paper derives further consequences, for instance that Marshall's boundary Hessian condition holds on a Zariski open set of data, and that Putinar-type certificates exist generically on the boundary of the cone of nonnegative polynomials. Beyond polynomial optimization, the statement is a precise algebraic form of the folklore that "generic nonlinear programs are nondegenerate".
The result is proved in the paper; no machine-checked version is known. A formalization fixes the exact quantifier structure (the printed statement is vacuous without a nonvanishing clause, and two items of Proposition 4.4 need an extra hypothesis), and builds reusable infrastructure: projective elimination over , homogenisation at a nominal degree, and the bordered-Hessian characterization of second order sufficiency.
The local part (Proposition 4.4, Lemma 4.6, Proposition 4.5) is linear algebra plus first and second order necessary conditions. The global part is not. Proposition 4.1 and 4.2 need the main theorem of elimination theory: the set of coefficient vectors for which a homogeneous (or bihomogeneous) system has a nonzero complex solution is Zariski closed, defined by polynomials in the coefficients. Mathlib has the univariate resultant only. Appendix A, which shows these polynomials do not vanish identically, has to control the homogenised systems both at finite points and at points at infinity (), where only the leading forms of the data are seen. Reasoning over alone does not suffice: the set of data whose real system is solvable is not the zero set of a polynomial.
Polynomials are MvPolynomial (Fin n) ℝ, points are Fin n → ℝ, and gradients and Hessians are formal partial derivatives. Homogenised polynomials have complex coefficients in n + 1 variables, variable 0 being , and homogenisation uses the nominal degree , not the actual degree. CQC is linear independence of an indexed family (repeated gradients count twice). The optimality conditions are bundled: CQC together with one multiplier pair satisfying (1.3), (1.4), (1.5) and (1.7); under CQC the multipliers are unique.
Condition 4.3 is encoded through the defining properties of Res, Δ, and (unsolvability of the corresponding complex projective systems) rather than through the polynomials themselves; since the goal is existential in the polynomials, this is not a weakening. Coefficient variables exist for monomials of every degree, so the goal's nonvanishing clause is asserted at an admissible input: a formal polynomial that is nonzero but vanishes on all admissible data (such as the variable of a monomial of degree ) does not satisfy it. Without that clause the printed theorem would be satisfied by .
Hypotheses added to the page, each disclosed in the statements: in Propositions 4.4 and 4.5 (Condition 4.3's standing assumption; Theorem 1.2 is stated for all , as printed), the nonvanishing clause in Theorem 1.2, and item (a) of Condition 4.3 in Proposition 4.4 ii)–iv) (with item (b) alone, , , , violates CQC). Proposition 4.2's nonsingularity is asserted at all complex critical pairs.
A complete development needs projective elimination theory over (reusable well beyond this mission), multivariate resultants and discriminants as polynomial functions of coefficients, Euler's identity for forms, and genericity facts about critical points of polynomial programs. Contributions to any of these, and direct proofs of the local milestones, are welcome.
An isotropic Gaussian random field is a spatial random quantity whose probability law is unchanged when the sphere is rotated. Such fields model spatially distributed uncertainty when no direction is preferred. The question in this mission is concrete: if a field is simulated by retaining only finitely many spherical harmonic frequencies, how rapidly does the simulation approach the full field? Lang and Schwab study this question while developing regularity, simulation, and stochastic partial differential equation results for isotropic fields on spheres (Lang and Schwab, 2015). Their §5 separates the error in expected spatial energy from the error seen along an individual sample. The latter is the target here.
Let be the unit sphere in and let be surface area measure, with . A point has angular coordinates , where . Spherical harmonics are the normalized complex functions indexed by a degree and an order . They form an orthonormal basis of complex with this unnormalized surface measure. The real factor is the normalized associated Legendre function appearing in for (§2, pp. 4–5).
The angular power spectrum is a nonnegative sequence recording the variance at each harmonic degree. Let and be independent standard normal random variables for the indices that occur below. The centered real field used in §5 is the ordered series
Its Karhunen–Loève truncation retains the outer sum through degree . These are the approximations analyzed and simulated in the paper (§5, p. 25). The norm measures the spatial size of a sample , while takes the th moment of that spatial norm over randomness. Lemma 5.1 relates this explicit series, in law, to an arbitrary centered isotropic Gaussian field with the same angular power spectrum (pp. 23–24).
The goal, Corollary 5.4, assumes , , an integer , and the tail condition for . It asserts almost-sure convergence in spatial and, for each , an eventual samplewise bound (p. 28):
The attack path retains three intermediate statements from §5. The squared mean-square error equals the exact spectral tail (the proof of Proposition 5.2, p. 26). Proposition 5.2 establishes convergence in and the bound
for (p. 25). Theorem 5.3 gives the same exponent for every finite , with a constant depending only on (p. 27). The goal's exponent may approach, but does not include, .
The mean-square estimate controls average approximation error, but it does not itself say whether one sequence of simulated fields converges along almost every outcome. Corollary 5.4 supplies that pathwise assertion and a quantitative rate for each exponent below the spectral threshold. It identifies the resolution needed to make the spatial error small for almost every sample, rather than only on average. The threshold directly links harmonic spectral decay to numerical truncation quality.
The cited results are already proved in the paper; the remaining task is to formalize their statements and proofs for the explicit KL model. The definition layer provides a reusable real representation of normalized spherical harmonics and mixed norms on . A completed proof would also make the transition from Gaussian moment estimates to samplewise convergence available as a machine-checked argument in this setting. No claim is made that these results already have machine-checked proofs.
The spherical harmonics are orthonormal, but an error bound for the full field needs more than termwise estimates. It must control the infinite tail while keeping the harmonic normalization, Gaussian variances, and the surface measure consistent. The passage from an expected error to one bound that eventually holds along almost every sample also requires estimates for arbitrarily high finite moments. A fixed second-moment bound does not yield the full range of exponents in Corollary 5.4. The paper's constant in Proposition 5.2 and the parameter dependence of the constant in Theorem 5.3 therefore matter to the final statement.
Lean uses EuclideanSpace ℝ (Fin 3) for the sphere. Coordinates represent the paper's . volume.toSphere supplies surface measure of mass . Legendre polynomials use Rodrigues' formula; the associated harmonics use Cartesian coordinates through , so they are defined at the poles without choosing an angle there. The field is the limit of the ordered partial sums . A nonconvergent sequence receives Lean's arbitrary limit value, but the theorems concern almost-everywhere convergence and norms, where such exceptional values must be shown irrelevant.
Spatial squared norms and mixed norms are extended nonnegative integrals. This keeps nonintegrable functions from taking a false zero norm. Lean's natural numbers include zero; in the paper is recorded as . Decay is required only above , exactly where the paper requires it. Coefficients that enter the series are measurable, jointly independent, and standard normal. The unused coordinates are zero, as specified in Lemma 5.1; coefficients at invalid indices are unconstrained. The field is the explicit series of p. 25, with Lemma 5.1 supplying the paper's identification in law with any centered isotropic field. In Theorem 5.3 the constant is chosen before the field and probability space, preventing it from depending on a particular spectrum or cutoff. The almost-sure conclusion is a spatial claim, never a pointwise assertion at each sphere point.
The displayed identity on p. 26 omits a square on its left-hand norm, although the neighboring formulas use squared norms. The formal error identity restores the square and the milestone preserves the printed wording. Contributions to the harmonic normalization, exact spectral identity, uniform finite-moment estimates, and the final almost-sure result all fit this mission. The normalizations, the positive cutoff, and the explicit independent Gaussian coefficients rule out vacuous or zero-field encodings.
The hard-core model on a finite graph at fugacity weights each independent set of by . Its normalizing constant, the independence polynomial , is a basic object of statistical physics (a lattice gas with hard-core exclusion) and of combinatorics ( counts independent sets).
The complexity of approximating on graphs of maximum degree is settled for general graphs: below the uniqueness threshold there is a deterministic approximation scheme (Weitz, STOC 2006, doi:10.1145/1132516.1132538), and above it the problem is NP-hard to approximate. On bipartite graphs the picture is different. Approximately counting independent sets of a bipartite graph defines the class #BIS, whose complexity is a major open problem of approximate counting, and Cai, Galanis, Goldberg, Guo, Jerrum, Štefankovič and Vigoda showed that for and the hard-core model on bipartite graphs of maximum degree is #BIS-hard (arXiv:1311.4839).
One route to partial progress is to find natural classes of bipartite graphs on which these #BIS-hard problems become tractable. Helmuth, Perkins and Regts did this for the hard-core model at high fugacity on the torus , using Pirogov–Sinai contour models and the cluster expansion (arXiv:1806.11548). Jenssen, Keevash and Perkins extended the method to abstract polymer models and to all bounded-degree bipartite expanders (arXiv:1807.04804; SIAM J. Comput. 49(4), 2020). This mission formalizes the mathematical core of their Theorem 1.
Let be a finite bipartite graph with vertex classes (odd vertices) and (even vertices), , and maximum degree at most . For a vertex set , the vertex boundary is the set of vertices outside with a neighbour in . For , is a bipartite -expander if
A subset of one class is small if it has at most half as many vertices as that class. The hard-core partition function is
with the independent sets of . A number is an -relative approximation to if .
is the graph on the same vertices in which two distinct vertices are adjacent when their distance in is at most ; a set is -connected when it induces a connected subgraph of . An even polymer is a nonempty, small, -connected set ; odd polymers are defined in . Two polymers are compatible if their distance in exceeds . Each polymer has the weight
and the polymer partition functions are , summed over the families of pairwise compatible even polymers (the empty family included), and likewise. Even polymers describe deviations from the ground state "all odd vertices occupied", and odd polymers from the other ground state.
For , , every bipartite -expander of maximum degree at most on vertices, and every
In the order of the paper's proof: Lemma 18 (every independent set has a small side); the identity ; the size bound for sparse independent sets; Lemma 20 (part 1 of the goal); the weight bound ; the count of at most -connected -sets through a vertex; and inequality (8), .
The two parts of the goal are exactly what Theorem 8 of the paper (adapted from Helmuth, Perkins and Regts) consumes: given a polymer model satisfying the Kotecký–Preiss condition, the truncated cluster expansion of yields an FPTAS and, through self-reducibility, a polynomial-time sampler. Together they give a deterministic approximate counting algorithm for a #BIS-hard problem on a natural graph class, at fugacities far above , the regime in which the problem is hard on general bipartite graphs. The same template (reduction to polymer models around ground states, then Kotecký–Preiss) underlies the paper's results for the Potts model, for random regular bipartite graphs and for proper colourings, and a large later literature on algorithms at low temperature.
The result is proved in the paper; to our knowledge none of it has been machine-checked. A formalization adds a precise treatment of the degenerate cases (see below), a reusable formal definition of abstract polymer models over vertex sets, and the elementary but intricate bijection between compatible polymer families and sparse sets.
Each step is elementary, and the difficulty lies in the bookkeeping. The reduction needs an exact correspondence between families of pairwise compatible polymers and sparse subsets of a class, and an exact double count over independent sets. The quantitative step of Lemma 20 compares the total weight of sparse independent sets, which have at most vertices, with ; the printed last inequality, , follows from only for up to about , and larger forces both classes to have at most nine vertices, a finite range that needs its own argument. The Kotecký–Preiss half needs the count of connected sets in a bounded-degree graph (Lemma 14 of the paper, from Galvin and Kahn), applied to , and a geometric series.
The algorithmic conclusion of Theorem 1 (an FPTAS and a polynomial-time sampling algorithm, with running time ) is not formalized: Mathlib has no machine model and the running times carry unspecified constants. The goal is the mathematics the algorithm rests on: the reduction to two polymer models and the Kotecký–Preiss condition for both. The cluster expansion and Theorem 8 are not part of the mission.
Conventions. The graph is a SimpleGraph V on a finite type, with a Finset V and its complement; bipartiteness is a hypothesis. The fugacity is lam. "" is 2 * #S ≤ #O in . Distances use the extended distance SimpleGraph.edist, so vertices in different components are never close. The Kotecký–Preiss sum ranges over the polymers of the same class incompatible with , including itself. Polymers are capped at half of their own class, not at ; the condition without this cap, or with compatibility in place of incompatibility, would be a different statement.
Two hypotheses differ from the page. Theorem 1 states the threshold as for an absolute constant ; the goal uses the threshold its proof uses (§4.3). The hypothesis is added: on the edgeless graph with one vertex in each class the expansion condition is vacuous, no side of the independent set is small, and Lemma 18 and Lemma 20 fail.
A complete development needs: the bijection between compatible families and sparse sets, Lemma 14 for , and real-power estimates. The polymer-model and graph-power definitions are reusable for the sibling missions of this series. Proofs of individual milestones are welcome independently.
A lookback option pays a function of the running maximum of the underlying asset over the life of the contract. When the prices of European call options of all strikes at the maturity are quoted, the risk-neutral law of the terminal price is known, but the law of the whole path is not. The robust (model-free) superhedging cost of the lookback payoff is the cheapest initial capital that, combined with a static position in the quoted calls and dynamic trading in the underlying, dominates the payoff in every model consistent with .
Hobson (Finance Stoch. 1998) computed this cost for by a pathwise inequality, and identified the extremal model through the Azéma–Yor solution of the Skorokhod embedding problem (Azéma–Yor 1979). Galichon, Henry-Labordère and Touzi (Ann. Appl. Probab. 2014, arXiv:1401.3921) recast model-free bounds as a dual stochastic control problem in which the marginal constraint is penalised by a Lagrange multiplier . Their Theorem 3.1 recovers Hobson's bound for every nondecreasing from that dual, with an explicit optimal multiplier and stopping time. The result is one of the founding examples of martingale optimal transport.
Let be a real Brownian motion with continuous paths and , adapted to a filtration with increments independent of the past, and let for a spot . Write . Let be the set of stopping times for which the stopped process is a uniformly integrable martingale.
The marginal is a probability measure on with finite first moment and mean . Its call prices are . The payoff is with of class and nondecreasing.
For a multiplier and set and . The admissible multipliers are
and the reduced superhedging problem (3.7) is
The barycenter function is for and otherwise. The Hardy–Littlewood transform is the probability measure with
The Azéma–Yor stopping time is , and the candidate multiplier is
that is, the convex function vanishing below that solves the weak ODE (3.21) with .
If and , then
The goal is the paper's theorem for the reduced problem (3.7), in its full two-equality form: the value, its attainment by , and its closed form.
The theorem identifies the model-free price of a lookback payoff as an explicit functional of the call prices, , and exhibits the extremal model (Brownian motion stopped at ) and the optimal static hedge (). It shows that the dual stochastic control formulation is sharp on a nontrivial path-dependent payoff, which is the template for later work on martingale optimal transport with path-dependent costs.
The result has been proved since 2014 (and Hobson's bound since 1998). It has not been formalized. A complete development would provide machine-checked versions of the Azéma–Yor embedding, the law of the maximum at the embedding, a verification theorem for a reflected optimal stopping problem with a nonsmooth obstacle, and the convex-analytic identities linking call prices to second-derivative measures. Each of these is reusable well beyond this paper.
The upper bound requires a verification argument for an optimal stopping problem of the pair with a reflection at the diagonal, where the candidate is only as regular as the convex multiplier : second derivatives are measures and the free boundary solves its ODE only in a relaxed sense. An Itô formula for functions does not apply; an Itô–Tanaka (local time) argument for concave functions of , with the reflection term killed by the Neumann condition, is needed, followed by a localisation that uses uniform integrability and the integrability condition in . The lower bound needs the Azéma–Yor embedding and the law of , neither of which is in Mathlib; the naive appeal to "the embedding exists" does not give the joint law of the stopped value and the maximum.
The Lean development lives in the namespace LookbackMOT.HL and uses Mathlib's IsBrownianReal, IsStoppingTime, stoppedProcess, stoppedValue, Martingale, UniformIntegrable and HasLaw. Committed conventions:
No trivializing reading is available. Payoff expectations are never Bochner integrals (which would be for non-integrable payoffs). lies in and in , so neither the supremum nor the infimum is over an empty set. The predicates for and are satisfiable (witnessed for in a sorry-free check). is only evaluated where a.s. Every division has a positive denominator on the sets that carry mass.
Contributions welcome: the Azéma–Yor embedding and the law of the maximum; an Itô–Tanaka or local-time calculus sufficient for concave functions of Brownian motion and its maximum; the call-price identities of convex analysis; and the analysis of .
Many operational decisions are linear programs whose cost vector is uncertain but partly predictable: shortest-path routing with uncertain travel times, portfolio choice with uncertain returns, shipment planning with uncertain costs. Before deciding, one observes features (traffic, market signals) correlated with the costs . Contextual linear optimization asks for a policy mapping features to decisions that minimizes the conditional expected cost, learned from past data .
Two families of methods compete. Estimate-then-optimize fits a regression of on and plugs it into the optimizer. Empirical risk minimization (ERM) and its "integrated" variants choose a policy directly to minimize the empirical decision cost. A widespread view holds that the integrated approach should win because it targets the decision cost. Hu, Kallus and Mao (arXiv:2011.03030, Management Science 2022) compare the two through their regret rates. Slow, noise-independent rates of order do not separate them. The separation appears under a margin (noise) condition controlling how often the problem is nearly dual-degenerate. This mission formalizes the paper's fast rate for ERM, Theorem 6.
Timeline. Margin conditions for classification go back to Mammen–Tsybakov (1999) and Tsybakov (2004); Massart–Nédélec (2006) obtained the corresponding fast rates for ERM over VC classes. El Balghiti, Elmachtoub, Grigas and Tewari (2019) gave slow generalization bounds for decision-focused losses in terms of the Natarajan dimension. Hu, Kallus and Mao (2020, revised 2021) proved the fast rate for ERM over policy classes of finite Natarajan dimension, a matching lower bound, and a faster rate for estimate-then-optimize.
The decision set is a polytope , nonempty, with on for some ; is its finite set of extreme points. The pair has , and . The optimal set at is .
A policy is a map . A data-driven policy maps a sample of i.i.d. draws to a policy, and its regret is
Given a class of policies, returns a member of minimizing .
The gap is the difference between the best value over suboptimal extreme points and the optimal value, set to when every point of is optimal. Assumption 2 (noise condition) with parameters requires
The Natarajan dimension of is the largest for which there are points and labels such that every pattern of choices between and is realized by some .
If Assumption 2 holds, , has Natarajan dimension at most , and contains an optimal policy , then for a constant depending only on ,
The constant is existential and uniform over all dimensions, polytopes, distributions, classes, and ; the goal fixes no numerical value.
With and :
Theorem 6 shows that the regret of ERM improves from to when the instance is rarely near dual degeneracy. With , the generic case when has a bounded density and is linear, the rate is . Theorem 7 of the same paper (mission 2 of this series) shows that the exponent is optimal for any method that uses only the policy class. Theorem 8 (mission 3) shows that estimate-then-optimize can reach , which is the paper's case against the conventional preference for integrated methods.
The result is proved in the paper; no machine-checked proof is known. Formalizing it adds a checked fast-rate theorem for a decision-focused learning method, a Lean statement of Bousquet's inequality in the form used throughout statistical learning theory, and a localized empirical-process bound for classes of finite Natarajan dimension.
The slow rate follows from uniform convergence of the empirical cost over . This argument cannot give more than : it bounds the deviation of every policy by the same worst-case amount, ignoring that near-optimal policies have small variance. The fast rate needs a variance–mean relation (Lemma 1, which is where the noise condition and the uniqueness assumption enter), a concentration inequality that exploits small variance (Lemma 2), and a localized complexity bound (Lemma 3), combined over shells of the class. Lemma 2 is itself a deep result whose known proofs go through the entropy method. Lemma 3 rests on chaining and on bounding the pseudo-dimension of the excess-loss class by the Natarajan dimension, neither of which is in Mathlib.
All declarations live in the namespace FastCLO.ERM. Conventions:
EuclideanSpace ℝ (Fin k). The polytope is a structure carrying , , , nonemptiness and the bound ; is the cardinality of Set.extremePoints, whose finiteness is a proof obligation, not a hypothesis.Measure.pi of .A statement in which the regret integrated the empirical cost instead of , or in which ERM minimized over a subset of the class, or in which the constant could depend on the instance, would be a different theorem; the Lean statements rule these out by construction.
Needed infrastructure: Bousquet's (or Talagrand's) inequality, symmetrization and Dudley chaining for empirical processes, packing bounds for classes of finite pseudo-dimension, and the Natarajan-to-pseudo-dimension reduction. These are reusable far beyond this mission; contributions of any of them are welcome.
The ferromagnetic Potts model assigns a larger weight to a coloring when more adjacent vertices have the same color. Computing its partition function is an approximate counting problem with connections to statistical physics and counting complexity. For three or more colors, Goldberg and Jerrum established #BIS-hardness of approximation on general graphs, and Galanis, Štefankovič, Vigoda, and Yang refined the hardness result for bounded-degree bipartite graphs Goldberg–Jerrum, Galanis et al.. These results make it useful to identify graph classes where the partition sum can still be approximated efficiently.
Jenssen, Keevash, and Perkins proved that edge expansion supplies such a class at sufficiently large inverse temperature. Their Theorem 3 gives an FPTAS and a polynomial-time sampling algorithm for the -color ferromagnetic Potts model on finite -expanders of maximum degree , when , , , and Jenssen–Keevash–Perkins. This mission records the mathematical reduction and the polymer convergence condition on which their algorithmic conclusion rests.
Let be a finite simple graph, let , and let . A coloring gives each vertex one of colors. Write for the number of edges whose endpoints receive the same color. The Potts partition function at inverse temperature is
For , its edge boundary consists of the edges with exactly one endpoint in . The graph is an -expander if whenever . The maximum-degree assumption means that each vertex has at most neighbors. All logarithms here are natural logarithms.
A color is a strict majority in when . Let be the Potts sum over colorings with that majority, and let . Because two colors cannot each occupy more than half the vertices, these sectors do not overlap. The monochromatic colorings are the model's ground states at positive .
A polymer is a nonempty vertex set for which the induced graph is connected and . Let be all edges with at least one endpoint in . Two polymers are compatible when the distance between every vertex of one and every vertex of the other exceeds one. In particular, overlapping or adjacent polymers are incompatible. With the Potts sum on the induced graph using the other colors, define
The sum includes the empty family. An -relative approximation to means Jenssen–Keevash–Perkins, Definitions 10–11.
The goal is the deterministic core of Theorem 3. For a nonempty -expander with the degree, color, and temperature bounds above, the explicit polymer expression approximates the Potts partition sum:
The error is the composition of the two -relative approximations in Lemmas 12 and 13; the paper does not print it as a separate constant. The same goal also asserts the Kotecký–Preiss condition, with the paper's decay function , for every polymer :
The milestone list follows the source's stated claims: Lemma 12 bounds the contribution outside the strict-majority sectors; Lemma 13 compares one sector with ; the weight bound controls individual polymers; Lemma 14 counts connected induced subgraphs containing a specified vertex; and displayed inequality (5) bounds the resulting per-vertex sum Jenssen–Keevash–Perkins, pp. 13–16.
The reduction makes a Potts partition sum on an expanding graph accessible through a finite polymer model whose weights have controlled decay. The Kotecký–Preiss condition is a quantitative convergence criterion for abstract polymer expansions Kotecký–Preiss. In this setting the two statements provide the mathematical hypotheses used with the algorithmic framework cited by the paper Helmuth–Perkins–Regts. Without the approximation, computing the polymer sum would not give a controlled Potts estimate; without the convergence condition, the cited framework would not apply at the stated temperature threshold.
The paper proves the mathematical and algorithmic results. This mission supplies Lean definitions and compile-checked statements, with proofs still to be formalized. A completed development would give reusable formal accounts of finite Potts sums, strict-majority sectors, graph edge expansion, polymer compatibility and weights, and the connected-set counting bound that the paper cites from Galvin and Kahn Galvin–Kahn.
The tempting approximation is to count only monochromatic colorings. That discards all nearby colorings, whose total weight matters even at low temperature. The polymer model retains connected deviations from a monochromatic coloring, but it also admits collections whose union is larger than half the graph. Controlling the weight of these extra configurations is part of the approximation statement. Separately, the convergence criterion sums over every polymer within distance one of a given polymer. A bound on one weight does not control that sum unless the number of connected vertex sets of each size is also bounded. These are the distinct estimates captured by Lemmas 12–14 and inequality (5) Jenssen–Keevash–Perkins, §3.
The Lean representation uses SimpleGraph V on a finite vertex type. Vertex sets are finite sets, the edge boundary counts each crossing edge once through its orientation from inside to outside, and polymer distance is extended graph distance, so disconnected components are infinitely far apart. Strict-majority colorings use ; expansion and polymers use the non-strict bound . The polymer weight uses the full incident-edge set and the induced Potts sum on colors. The empty compatible family contributes one to .
The vertex set is required to be nonempty in the goal and approximation lemmas: for , the strict-majority sum is zero while the Potts partition sum is one. Lemma 14 states because its printed bound is false for an isolated vertex with . The weight bound states , which is implied by the goal's threshold. These are the only additional domain pins. The stated goal uses the paper's exact , , and ; no free approximation value or freely chosen polymer family can trivialize it.
The algorithm and its running time are out of scope because this Mathlib environment has no machine model for the FPTAS and the paper uses unquantified big-O running times. The goal is the mathematical reduction and Kotecký–Preiss hypothesis consumed by Theorem 8. Contributions that establish the five milestone statements, the color-symmetry identity, or the combination of their bounds are useful; the finite graph and partition-sum definitions are reusable beyond this mission.
A random field on a sphere assigns a random value to every direction. Such fields appear when the underlying data are directional, including spherical models in spatial statistics and geophysics. The covariance of an isotropic field can be recorded by an angular power spectrum: one nonnegative number for each spherical harmonic degree. This changes the sample regularity question into a concrete spectral question. How fast must these numbers decay so that a realization is continuous, and how regular can that realization be? Lang and Schwab, 2015 give a sufficient summability condition and an exact range of Hölder exponents in their Theorem 4.5.
The question matters when a field is evaluated on a mesh or represented by finitely many spherical harmonics. A covariance function can be regular even when the original version of a random field has badly chosen values on null sets. The useful result is therefore the existence of one regular modification: at each fixed sphere point it agrees with the given field almost surely, while its sample paths are regular across the entire sphere. The paper treats this sample path result in §4, separately from its spectral characterization of covariance regularity in §3 and its later simulation and stochastic heat equation results.
Write for the unit sphere. Its geodesic distance is , the length of the shorter great circle arc between and . A random field is a jointly measurable map from a probability space times to the real numbers. A field is Gaussian when every finite collection of its values has a joint Gaussian distribution. Isotropy says that rotating all observation points together does not change that joint distribution. These are the conventions of Definition 2.1 in the paper.
For each degree , let be the Legendre polynomial normalized by , and let be its angular power. The field has a constant mean and covariance determined by :
Because , the same covariance is expressed by the distance kernel for . A modification of means almost surely for each fixed ; it need not agree on one common full measure set at every . The paper's Assumption 4.1, specialized to , asks for finiteness of .
For , the target is Theorem 4.5 of Lang and Schwab:
The same modification serves every eligible exponent. The result leaves the Hölder constant free to depend on the sample and the exponent, as it must.
The four milestones follow the source's statements and its proof order. The Legendre polynomial bounds on p. 16 lead to Lemma 4.2, for and . Lemma 4.3 transfers this to for every positive integer . Theorem 4.4 is a Kolmogorov–Chentsov theorem for any random field on : a moment exponent produces a continuous modification with every Hölder exponent below . The Gaussian and isotropic hypotheses belong to Lemma 4.3 and the goal; they are absent from Theorem 4.4.
The theorem provides a checkable bridge from a harmonic description of a field to sample path behavior. A practitioner can estimate or impose decay of the angular power spectrum, then know that a version of the field admits interpolation on the sphere with any exponent below . The endpoint is not asserted. The moment estimate and the spherical modification theorem can also be reused when studying fields produced by other models; in particular, Theorem 4.4 needs no Gaussian assumption.
The result was proved in the 2015 paper; this mission concerns its machine checked formalization. Mathlib supplies Gaussian process and measure theory interfaces, but the paper's sphere distance, Legendre normalization, angular kernel and spherical version of Kolmogorov–Chentsov must be connected. A platform goal for a Kolmogorov–Chentsov theorem on uses a different index space and hypotheses, so it does not cover the present milestone. The finished development will provide a reusable sphere indexed modification theorem as well as the paper's specific spectral criterion.
A bound on the covariance kernel controls the second moment of field increments, but it does not by itself supply one continuous version with a common pathwise regularity statement. The desired exponent concerns values at uncountably many points, whereas the definition of modification gives an almost sure equality separately at each point. The gap is visible even for simple processes: changing a field at one random location can preserve each fixed point's law while destroying continuity of individual paths. The sphere also carries a two dimensional geodesic metric, so a one dimensional modification theorem indexed by time cannot be substituted without a new argument.
Lean represents as the unit metric sphere in three dimensional Euclidean space. Coordinates have indices for the paper's . All regularity statements use , not the subtype's chord distance. Rodrigues' formula defines , and the kernel is a real infinite sum with its factor . The spectrum is nonnegative and has as part of the field model, matching the finite variance convention used in §2. The covariance formulation allows a nonzero constant mean: Theorem 4.5 does not require centering.
The moment inequalities use extended nonnegative integrals, avoiding a default zero for nonintegrable real integrals. The paper's positive integers are expressed with an explicit because Lean's naturals include zero. Real powers follow the usual convention: the degree zero term of is zero when . On compact , local Hölder continuity gives a global constant for each path and exponent. Exceptional sample paths may be redefined, so the formal conclusion states continuity and Hölder regularity for every sample of the chosen modification. The modification retains pointwise almost sure agreement and measurable evaluations; omitting agreement would make the goal trivial.
Contributions can address Legendre inequalities, covariance and Gaussian moment calculations, and a general Kolmogorov–Chentsov theorem for compact manifolds. The latter is reusable beyond this paper. The auxiliary Legendre and kernel definitions are also available to later spherical field missions.
Stochastic partial differential equations on the sphere model quantities that live on the surface of the Earth or of the sky and are perturbed by spatially correlated noise: temperature anomalies, geophysical fields, fluctuations of the cosmic microwave background. The simplest such model is the stochastic heat equation on the unit sphere with additive isotropic noise. Because the noise is isotropic and the Laplace–Beltrami operator is diagonal in the spherical harmonics, the equation decouples into one scalar Ornstein–Uhlenbeck equation per harmonic, and the solution can be simulated exactly in law by truncating its spherical-harmonic expansion at a degree . The practical question is how fast this spectral truncation converges, in mean square and along a single simulated path.
A. Lang and Ch. Schwab answer this in §7 of Isotropic Gaussian random fields on the sphere: regularity, fast simulation and stochastic partial differential equations (arXiv:1305.1170v3, Ann. Appl. Probab. 25(6), 2015). Their rates are expressed through the decay of the angular power spectrum of the noise, the same quantity that governs the sample regularity and the Karhunen–Loève truncation of isotropic Gaussian random fields in the earlier sections of the paper.
Let be the unit sphere with surface measure (total mass ) and the real square-integrable functions with norm . The spherical harmonics , , , are built from the Legendre polynomials ; the functions , , () form a real orthonormal basis of the degree- harmonics, on which the Laplace–Beltrami operator acts as multiplication by , .
On a probability space let (, , ) be independent real Brownian motions, and let , , be an angular power spectrum. The isotropic -Wiener process is
The stochastic heat equation is
Its solution is with
and the spectral approximation is . The norm measures random fields. The standing assumption of §7 is the decay condition
For every and every , almost surely
The goal fixes no constant; only the exponent enters, so it survives any improvement of the constants below.
Corollary 7.3 is the pathwise convergence rate of the spectral method for the stochastic heat equation on the sphere: a single simulated path of the truncated series is within of the true path in for all large , for any . Combined with the exact-in-law recursion on a time grid (pp. 36–38), it says that the only source of error in simulating this SPDE is the spectral truncation, and that the rate is governed by the decay exponent of the noise spectrum alone, with sufficing (no trace-class condition is needed, thanks to the smoothing of the heat semigroup). The mean-square and estimates of Lemmas 7.1 and 7.2 are the quantitative inputs; the bound for all is what makes a Borel–Cantelli argument possible.
The results are proved in the paper; none of them, nor the stochastic heat equation on the sphere, nor spherical harmonics, has a machine-checked formalization on the platform or in Mathlib. The work here is to formalize the known proof. Two printed statements need correction (see Formalization scope); the milestones state the bounds that the paper's proofs establish.
The obvious argument writes as the tail of the series, splits it into the damped initial condition and the noise, and bounds each. The noise part is a Gaussian random field whose angular power spectrum decays like , so its truncation error is controlled by the corresponding estimates for isotropic Gaussian random fields (Proposition 5.2 and Theorem 5.3 of the paper), which must be re-derived here. Several steps have no current library support: the Wiener integral of a deterministic integrand and its Gaussian law, orthonormality and completeness of the spherical harmonics in , moment equivalence for Gaussian vectors in a Hilbert space (to pass from to all ), and the passage between the pointwise series and its limit. The initial-condition tail decays like but not uniformly as , which is exactly why the printed "uniformly in time" bounds fail and why every statement takes fixed.
Metric.sphere (0 : EuclideanSpace ℝ (Fin 3)) 1 with coordinates indexed (the paper's ); is the measure toSphere of Lebesgue measure, of mass . Spherical harmonics are written in Cartesian form, , which is the paper's function also at the poles. For real the projection is written in the real orthonormal basis.IsBrownianReal processes on , independent as a family of path-valued random variables. The stochastic convolution is defined pathwise as , which equals the Wiener integral almost surely (integration by parts; a.s.). This is the one place where a stochastic integral is replaced by a pathwise expression.An event stream can raise its own future event rate. A Hawkes process models this feedback by adding to a baseline rate the effects of past arrivals. The parameter measuring total excitation can approach its stability boundary, at which long clusters make a fixed time scale an unreliable guide to the observed count. Jaisson and Rosenbaum identify a regime in which observation time and the distance to that boundary balance, leaving a stochastic limit rather than a deterministic average Jaisson and Rosenbaum, 2015. Their theorem gives a precise bridge from an event count with jumps to a continuous square-root diffusion. The paper notes a practical reason for this bridge: intermediate-scale inference can use diffusion methods to estimate the baseline rate and two aggregate kernel parameters, though it cannot recover the entire excitation kernel Jaisson and Rosenbaum, §2.4, p. 10.
For each observation horizon , let count events up to time , with . The process is observed on and has intensity
where is the baseline rate. The integral against is a sum over its unit jumps. The nonnegative kernel has total mass one and finite mean ; its derivative is bounded and integrable. The coefficients satisfy and . Thus is the total mass of , and the model approaches the stability boundary from below. The natural filtration is generated by the observed count. The intensity relation is the identity for conditional expected increments on every interval and every event observable at time Jaisson and Rosenbaum, §2.1, p. 5.
The resolvent collects excitation across repeated generations. Its rescaled density is . The mission uses the paper's additional bound and the balance condition . Here is a fixed limiting parameter, distinct from the time-dependent intensity . The processes to be compared on a common interval are
The main target is Theorem 2.2, p. 10: converges in law in the Skorohod topology on to the unique strong solution, started at zero, of the Cox–Ingersoll–Ross equation
Separately, converges in law in the same path topology to . These are two convergence claims, each on its own path space law. The statement also asserts that the strong solution exists, so convergence to “every solution” cannot hold merely because there are no solutions.
The supporting targets follow the paper's stated results. Lemma 4.1 and Proposition 2.1 identify the resolvent renewal identity and the intensity's resolvent form; both are supporting theorem items. Lemmas 4.2–4.5 give separation and decay estimates for the plus-sign Fourier transforms of and , followed by convergence of to the exponential density . Lemma 4.9 gives a fourth-moment increment bound for the paper's residual process , and Proposition 4.1 states that tends to zero uniformly in probability on . The latter six are source-stated milestones, with their pages and texts recorded separately.
The theorem identifies the scale at which a nearly unstable event model retains random dynamics. It also identifies the diffusion coefficients: the drift relaxes toward at rate , and the noise has coefficient times the square root of the current intensity. The second convergence claim transfers this intensity behavior to accumulated events. Those coefficients make the limit more informative than a statement that merely names a generic continuous process Jaisson and Rosenbaum, Theorem 2.2.
The result is proved in the paper but has no matching published Hawkes formalization in the local Prove2Me index used for this mission. Machine-checked definitions for Brownian motion and strong SDE solutions from the Ethier–Kurtz development are already available and referenced here. The new formal work is the Hawkes model, its path-space convergence, the density estimates, and the limit theorem itself. Formalizing the stated milestones would also leave reusable analytic and probability interfaces for other nearly unstable point-process limits.
Pointwise convergence of an intensity or of finitely many observations does not control its law as a cadlag path. Excitation also couples each event to later events, so a direct independent-increment argument is unavailable. The resolvent has to be controlled at the observation scale, including its high-frequency behavior, while the stochastic remainder has to be controlled uniformly over time. The final limit is a square-root SDE: its coefficient is not globally Lipschitz at zero, and a claim about its law must keep the initial condition and Brownian driver explicit Jaisson and Rosenbaum, §§4.2–4.3.
The horizon is a positive real sequence tending to infinity, as the paper's footnote specifies; is a sequence in tending to one. Each index may have its own probability space. The count is natural-number valued, nondecreasing, right-continuous, starts at zero, and has unit jumps. Its filtration is generated by evaluations of . The intensity identity uses extended nonnegative integrals, avoiding an arbitrary real value for an infinite expectation. The right-continuous intensity includes an event at the current time, so is cadlag. Its predictable left-limit version is available for stochastic integrands. All results use the half-line kernel and ; they never replace it by in the Hawkes process.
Skorohod convergence is represented by a coupling whose cadlag paths approach each other after increasing homeomorphic time changes of . This is the representation form of weak convergence in with the topology. The limit SDE uses the published global strong-solution predicate, then restricts its paths to . Its drift is exactly and diffusion exactly ; Real.sqrt on negative arguments does not affect its nonnegative solution. The renewal theorem item additionally makes the unknown measurable and locally bounded so its real convolution integral has its stated meaning. Fourier denominators exclude zero explicitly, while the zero-frequency bound is stated separately. The density convergence uses an extended nonnegative squared integral, and uniform probability convergence uses an extended supremum. These choices rule out default-zero values, a vacuous Hawkes class, a free limit process, and finite-dimensional convergence in place of path convergence.
The development needs half-line convolution and summable resolvents, natural filtrations and compensated point processes, Fourier bounds, cadlag path laws, and Itô SDEs. The convolution, path-space, and point-process interfaces are suitable for reuse. Contributions should preserve the exact hypotheses, constants, and two distinct convergence conclusions of the source theorem.
The asymmetric traveling salesman problem (ATSP) asks for a shortest closed walk through every vertex of a directed graph whose edge weights need not be symmetric. It models routing with one-way streets, scheduling with sequence-dependent setup times, and many other problems in which the cost of going from to differs from the cost of going back. Its standard linear relaxation, the asymmetric Held–Karp relaxation, is the lower bound used both by exact branch-and-cut codes and by approximation algorithms, and the central question about it is how far it can be from the integer optimum.
Timeline of the approximation ratio and of the integrality gap for ATSP:
The lower bound on the integrality gap remains (Charikar, Goemans and Karloff, 2006).
A digraph has finite vertex and edge sets; each edge has a tail and a head, and parallel edges and loops are allowed. For , and are the edges leaving and entering , and . An ATSP input is a strongly connected digraph with a weight function .
An edge multiset gives each edge a multiplicity ; is the set of vertices it touches. is Eulerian if every vertex has as many outgoing as incoming edges of , a subtour if moreover is connected, and a tour if it is a subtour with . Tours are exactly the closed walks visiting every vertex. The weight of is .
The asymmetric Held–Karp relaxation LP is
and its optimum is the Held–Karp lower bound.
The mission also uses the paper's intermediate objects: laminarly-weighted instances , in which is a laminar family of sets that are tight for a strictly positive feasible , on , and the weight of an edge is ; the value and the lower bound ; Subtour Partition Cover and -lightness; irreducible instances; vertebrate pairs; and quasi-backbones. Each is defined, with the paper's page reference, in the two definition files of the mission.
For every strongly connected digraph with , every and every feasible solution of LP, there is a tour with
This is the statement that the integrality gap of the asymmetric Held–Karp relaxation is at most .
The milestones are the results the paper's §11 combines, in the order it combines them:
The result shows that the asymmetric Held–Karp relaxation approximates ATSP within a constant factor, which settled a question open since the 1980s and made the relaxation a certified lower bound with bounded loss. The structural steps (reduction to laminarly-weighted instances, Subtour Partition Cover, irreducibility and vertebrate pairs) are the framework on which the later improvement to by Traub and Vygen is built.
The theorem is proved; to the best of available knowledge none of it has been formalized in a proof assistant. A complete development would give a machine-checked bound on the integrality gap of a central relaxation in combinatorial optimization, and its intermediate statements are reusable for the improved bounds that follow the same framework.
The obvious approaches do not give a constant. Repeated cycle covers lose a factor at each of logarithmically many rounds. Rounding the LP solution through thin trees needs a spanning tree that is thin in every cut, and only polylogarithmic thinness is known. The paper's route is long: the reduction to laminarly-weighted instances needs an uncrossed dual; the reduction from irreducible to general instances and the one from vertebrate pairs to irreducible instances are recursive, applying the assumed algorithm to instances built by contracting or inducing tight sets, so their hypotheses must hold on all instances and not only on the given one; and the lightness bound for vertebrate pairs (Theorem 10.1) rests on a flow-based construction with careful accounting against the laminar family.
Vertices and edges are finite types; edges carry tail and head maps, so parallel edges (created by contraction) are distinct edges, and loops are allowed and lie in no cut. Edge multisets are functions . Connectivity of a multiset and its components are defined by the reflexive–transitive closure of undirected adjacency along its edges.
Running times are not formalized. Every algorithmic statement is posed in its existential form, as §11 of the paper itself uses it to derive Theorem 11.1: "there is an algorithm returning a tour within " becomes "every instance has a tour within ", and an assumed algorithm becomes a hypothesis quantified over instances on all finite vertex and edge types. The algorithmic constants , , and are therefore not stated; the non-constructive constants , and of §11 are.
The Held–Karp lower bound is never defined as an infimum: comparisons with it are stated for every feasible , equivalently because the LP optimum is attained. Likewise and in the definition of irreducibility are expressed through walks, without an infimum.
Added hypotheses, each disclosed in the item's Formalization Note:
These choices rule out trivializing formalizations: no instance class in a hypothesis is empty (a two-vertex singleton instance is valid, irreducible and vertebrate), admissible partitions exist for every instance, and LP is feasible for every strongly connected input. The goal assumes none of the milestones.
Out of scope: the polynomial running times, §5's merge-procedure lemmas, the constructions of §7, and Corollaries 11.2–11.4 on the path version, which rest on external reductions. Contributions are welcome on every milestone, and on infrastructure that a complete development needs: LP duality and uncrossing for cut LPs, Eulerian multigraphs and their decomposition into closed walks, and circulations with lower bounds (Hoffman's theorem). The platform's proved LP strong duality (SmaleNinth.lp_strong_duality) is a natural starting point for Lemma 2.2.
A Hawkes process is a model for events that make further events more likely for a time. It is used when event times cluster, including transaction arrivals in financial markets. Jaisson and Rosenbaum study what happens when the feedback approaches the threshold at which the usual stable model ceases to have a finite long-run mean intensity. The behavior depends on how fast the observation horizon grows relative to that approach to instability. Their first regime says that, when the horizon grows sufficiently faster, the observed count still becomes deterministic after normalization. The precise result is Theorem 2.1 of Jaisson and Rosenbaum (2015).
The mission concerns that first regime alone. It isolates an statement that controls the whole observed path at once, rather than a count at one fixed time. Later results in the paper use a different balance between the horizon and the feedback parameter and produce stochastic diffusion limits. Those later regimes are separate missions in this series.
For each horizon , let count events through time , starting from . It is observed for on a probability space that may depend on . Its intensity is the nonnegative process
The baseline creates events even before any excitation. At each jump of , the kernel adds an effect that depends on the elapsed time since that event. The intensity property is specified relative to the natural filtration : for and , the expected number of new events on equals the expected integrated intensity on over . This is the defining condition used in §2.1 of the paper.
Assumption 1 fixes a nonnegative measurable kernel of total mass one and finite first moment . Its derivative is bounded and integrable. The horizon-dependent kernel is , with and . Thus approaches the stability boundary. The paper also defines the compensated count and the resolvent , where each convolution uses nonnegative time. These enter the supporting results.
The goal is Theorem 2.1, in the regime . Its assertion is
The supremum is inside the expectation. The time variable runs over the entire unit interval, so this is a statement about the normalized path of the count. The normalizing factor depends on both the horizon and the distance from the stability boundary.
The milestone list consists of the paper's renewal identity (Lemma 4.1), its two representations of the Hawkes mean and centered count, the exact mass of , a pathwise fluctuation bound, the Doob estimate for , and the finite-horizon bound with constant . The final estimate has no asymptotic hypothesis; the goal adds the regime condition and takes its limit. The unnumbered milestones are the displays in §4.1, pp. 14–15, and Lemma 4.1 appears in §4.2, p. 15.
The result identifies a regime in which near instability does not produce macroscopic random fluctuations at the paper's normalization. It supplies a boundary between the familiar deterministic large-horizon behavior of stable Hawkes processes and the diffusion behavior obtained under the paper's other scaling. The theorem controls the largest fluctuation over the whole observation interval, which is stronger than a statement at each fixed or a bound on the supremum of separate variances.
The mathematical result is proved in the paper; the target here is a machine-checked proof of the same result. A completed development would also provide reusable Lean definitions for a simple counting process, its generated filtration, pathwise jump integration, Hawkes intensity, and nonnegative-time convolution resolvent. It would make explicit the maximal inequality and renewal estimates needed for other Hawkes scaling questions. This mission currently poses these statements as open Lean proof obligations; it does not claim the paper's proof is already formalized.
The near-instability parameter tends to one, so estimates for a Hawkes process with a fixed cannot simply be used with a uniform constant. The scale of the mean and the size of the fluctuations both change with . There is also a pathwise issue: the theorem places a supremum over all inside an expectation. A separate estimate for each does not provide the required control of the path maximum.
The point-process side adds another layer. The compensated count is a continuous-time martingale with jumps, and the intensity depends on its own event history. The result therefore needs the correct relation among the natural filtration, the intensity identity, the resolvent, and the martingale maximum. The book-keeping at a jump matters: the cadlag intensity includes the jump at its time, while stochastic compensator integrals use the same process only up to a set of times of Lebesgue measure zero.
The Lean development indexes the paper's implicit horizons as a sequence tending to infinity; the multipliers tend to one, and . Each may use a different probability space. Time is represented by real numbers, with the counting-process conditions applied on nonnegative time and the Hawkes intensity identity applied only through the observation horizon. The count is natural-number valued, right-continuous, nondecreasing, and has unit jumps. The Hawkes intensity is defined by a finite sum over jumps in , and the conditional intensity identity uses extended nonnegative expectations, so an infinite expectation is not silently assigned zero.
The kernel is measurable and nonnegative on , has total mass one and finite first moment, and has an integrable bounded derivative; differentiability at zero is one-sided. The resolvent starts at the first convolution power, not at an identity term. Its mass is taken over positive time. The path supremum and its squared expectation are extended nonnegative quantities. Ordinary real expectations of are retained because their integrability follows from the Hawkes assumptions; the theorem does not assume it separately.
The Hawkes predicate is the paper's natural-filtration intensity condition for . A vacuous process condition, an intensity built from instead of , or a supremum taken outside the expectation would change the target. Contributions to the generic counting-process and resolvent definitions, the renewal identity, the finite-horizon martingale estimates, and the goal theorem are all within scope. The source's p. 14 bound omits an absolute value on the centered count; the Lean milestone states the absolute-value form required by its subsequent squared estimate, while its verbatim field preserves the printed form.
Least-squares regression over a class of functions is the basic problem of statistical learning theory: given an i.i.d. sample from an unknown joint law, select a function in a class whose prediction error is close to the best possible in . The standard analysis of empirical risk minimization (ERM) compares empirical means with true means uniformly over the class, which requires the class and the target to concentrate: bounded functions, or sub-Gaussian tails. Heavy-tailed classes and targets, which arise as soon as the data are not bounded, fall outside that analysis.
S. Mendelson, Learning without Concentration (arXiv:1401.0304, J. ACM 62(3), 2015), showed that concentration is not needed for the lower half of the argument. The only property used for the quadratic part of the loss is a small-ball condition: functions in are not too concentrated near zero. Under that condition, ERM over a closed convex class attains an error governed by two localized complexity parameters, one intrinsic to the class and one measuring its interaction with the noise. The same lower-bound mechanism appears, for random matrices, in Koltchinskii–Mendelson (arXiv:1312.3580); the localized complexity parameters follow Lecué–Mendelson (arXiv:1305.4825).
Let be a probability space and let have joint law on , with and . Let be a closed, convex class of real functions on , and let minimize over . The noise is . Given an i.i.d. sample from , an empirical minimizer minimizes over . Let be independent random signs, independent of the sample, and write .
Fix with and . For every , with probability at least , every empirical minimizer satisfies
The joint law, the class and the target are arbitrary subject to the hypotheses above; no boundedness, moment or tail condition beyond is imposed.
In attack order:
for all with . 9. Display (5.5) (p. 24): a bound on on the sphere extends to outside it (deterministic).
Theorem 3.1 separates the error of ERM into a "low-noise" term , which depends on the class only and matches the realizable rate, and a "high-noise" term , which depends on how the class correlates with the actual noise. Both are computable for heavy-tailed classes: the paper derives from it sharp rates for linear regression with heavy-tailed design and for the persistence problem in (§4). The small-ball lower bound (Theorem 5.4 and (5.3)) is reusable on its own: it gives lower isometry estimates for random matrices with heavy-tailed rows (the setting of Koltchinskii–Mendelson).
The result is proved in the paper. As far as is known, none of it has been machine-checked: there is no formal statement of Theorem 3.1, of the small-ball estimate, or of the localized parameters in Lean. The mission produces the first formal statements of these objects, and a formal proof would also check the constants of the printed argument.
The obvious approach, a uniform law of large numbers for the squared loss over , fails: without concentration, need not be close to uniformly, and an upper estimate is unavailable. The proof needs only a one-sided lower estimate, and the difficulty is to obtain it uniformly over an infinite, unbounded class from the small-ball condition alone, with a probability that is exponential in . A second difficulty is the multiplier term , where the noise may be heavy-tailed and dependent on ; it must be controlled through the random-sign process defining , not through a bound on . The standard tools involved (bounded differences, symmetrization, contraction for Bernoulli processes) are not in Mathlib.
All objects live in one definitions file, LearnNoConc.ERM.Setting. The conventions are:
ν on Ω × ℝ; the law of is ν.map Prod.fst. The sample is a point of Fin N → Ω × ℝ under Measure.pi; is assumed.eLpNorm · 2 μ, valued in . The expectation over random signs is the average over all sign vectors.⨆, ‖·‖ₑ, lower Lebesgue integral), and are -valued infima, so an empty set of admissible radii gives and a vacuous bound, as on the page. Defining inequalities are compared in the extended reals.A formalization in which an infimum over an empty set is , a supremum or an integral of a non-integrable function is truncated to , is an arbitrary element of , or is one chosen minimizer would trivialize or change the statement; all of these are ruled out above.
A complete development needs McDiarmid's bounded differences inequality, Giné–Zinn symmetrization (in expectation and in probability), the Ledoux–Talagrand contraction inequality for Bernoulli processes, and the measurability theory of suprema over separable classes. These are reusable well beyond this mission, and contributions of any of them are welcome, as are proofs of the milestones independently of the goal.
The Volterra square-root model describes a nonnegative, time-dependent state whose present value depends on a weighted history. Ordinary square-root diffusions use a constant kernel and have a Markov state; replacing that kernel by a function of elapsed time allows persistent or singular memory. This matters for the transform formulas used to characterize distributions of such processes. Those formulas depend on a deterministic nonlinear integral equation, and require a solution that exists at every finite time. Abi Jaber, Larsson and Pulido isolate that requirement in Lemma 6.3 of Affine Volterra processes, arXiv:1708.08796v3 (2019).
The paper's Section 6 treats processes in the nonnegative orthant and its Section 7 specializes the framework to a Volterra Heston model. The present mission concerns the deterministic equation behind the Section 6 transform. The stochastic existence theorem and the transform identity are separate results in the same paper. Keeping this mission on the integral equation makes its analytic content usable independently of a chosen probability space.
Fix a finite coordinate set of size . A diagonal kernel consists of real functions for , with the -th entry of the matrix kernel equal to and all off-diagonal entries zero. A resolvent of the first kind for is a nonnegative measure for which the convolution equals one at positive times. The relevant regularity condition, labeled (2.5), requires local square integrability and positive-time translation bounds of order for some . Condition (3.4) requires a kernel to be nonnegative, nonzero, nonincreasing and continuous at positive times. It also requires its resolvent measure to have decreasing interval masses as increases. Each shifted function must satisfy (3.4) for , with its own resolvent. These are the assumptions of Theorem 6.1 and hence of its Lemma 6.3 (pp. 6, 14, 28–29).
Let be a complex row vector and let be a locally integrable complex row function. Let be a real matrix whose off-diagonal entries are nonnegative, and let . The -th square-root Riccati–Volterra equation is
The index selects column : in the paper's notation and the coupling is . The kernel acts only on the -th equation, while couples the coordinates. The coefficient from the stochastic process does not enter this equation (equation (6.3), p. 27).
The goal is the global existence, uniqueness and sign statement of Lemma 6.3. If and , then
For functions defined only up to null sets, the equation, uniqueness and sign conclusion are understood almost everywhere. The goal has no fixed time horizon and no hard-coded kernel: it covers every diagonal kernel satisfying the paper's conditions. The five milestones record the source's analytic support: the shifted resolvent bounds (3.9)–(3.10), the stability lemma C.1, maximal-solution Theorem B.1, global-solution Corollary B.3 and nonnegative-orthant invariance Theorem C.2. Their statements and locations are recorded in the milestone list.
Global solvability makes the square-root transform equation meaningful at any finite horizon. Uniqueness fixes the transform parameter determined by a kernel and forcing function. The nonpositive real part is the sign property needed in the paper's subsequent exponential-affine transform argument for nonnegative states (Theorem 6.1(ii), pp. 28–29). Without a global solution, that argument would only address a time interval before a possible blow-up.
The result is proved in the cited paper; this mission asks for a machine-checked development of that known theorem and its supporting integral-equation results. Its reusable output includes an notion of Volterra solution, the first-kind resolvent hypotheses, maximal lifetime, stability under changes of forcing and kernel, and a comparison statement for diagonal systems. The goal and milestones are presently proof obligations, not claims of existing machine-checked proofs.
Local solvability alone does not control the quadratic term for arbitrarily large time. In particular, a generic local fixed-point theorem can yield a maximal solution whose norm diverges at a finite horizon. Sign information for the real part is also coupled to the imaginary part through that quadratic term; checking each coordinate independently does not establish invariance of the nonpositive half-plane. The analysis has to preserve the kernel's first-kind resolvent conditions and the off-diagonal sign pattern of across the coupled system. Singular kernels allowed by (2.5) prevent replacing the problem with a standard ordinary differential equation.
Time is represented by real numbers and every local condition is restricted to positive bounded intervals. Vectors are functions on Fin d; matrix membership is componentwise. These finite-dimensional norms are equivalent to the Euclidean and operator norms used in the paper. The kernel regularity estimates are Big-O statements as tends to zero through positive values. A first-kind resolvent is a nonnegative measure supported on nonnegative times, with the convolution identity and interval-mass monotonicity stated directly. The convolution at positive time is an interval integral; the bound at zero in (3.10) uses the integral on , while the source describes a right-continuous extension when available.
Solutions are locally square integrable and satisfy their equations almost everywhere. The integrability of each asserted convolution is part of the solution predicate, so the default zero value of a nonintegrable Lean integral cannot create a spurious solution. A maximal lifetime is extended-nonnegative-real valued, allowing infinity, and a finite lifetime requires an infinite extended norm. Sign conditions on locally integrable forcing and on the solution are almost everywhere. Measurable time dependence of the nonlinear drift is made explicit for Theorem B.1 and Corollary B.3, where it is necessary to interpret their integrals. The condition of the square-root process is omitted from the goal because is absent from (6.3).
The development needs Mathlib's Bochner integrals, local predicates, measures, complex arithmetic and asymptotic filters. Proof contributions to the five source milestones and the goal are welcome, including infrastructure for nonconvolution Volterra resolvents where the paper cites earlier literature. The formalization must keep the coefficient , the column index , and every shift .
Kernel ridge regression is a standard nonparametric estimator with optimal statistical guarantees, but it needs the kernel matrix of the data: roughly time and memory. Random features (Rahimi and Recht, NeurIPS 2007) replace the kernel by an average over randomly sampled feature functions, turning the problem into ridge regression in dimension , at cost time and memory. The question is how many features are needed before the statistical accuracy of the exact kernel method is lost.
The first statistical analysis of a random-features estimator (Rahimi and Recht, NeurIPS 2009), for Lipschitz losses over a ball of fixed radius, needs features to reach an bound. Rudi and Rosasco (arXiv:1602.04474, NeurIPS 2017) showed that of order features already give the excess risk that exact kernel ridge regression attains with regularization (Caponnetto and De Vito 2007), assuming only that the best predictor in the reproducing kernel Hilbert space exists.
Let be a separable input space and a probability space. A random feature is a function , continuous in both variables with for some . It defines the kernel
whose reproducing kernel Hilbert space is . Data are drawn i.i.d. from a probability on with almost surely, . The expected risk is , and is a minimizer of over , assumed to exist.
Given features drawn i.i.d. from , independently of the data, the feature map is . With and , the random-features ridge estimator with parameter is
In the Lean development these are kernelOf, featureMap, empCov, empCross, rfWeights, rfEstimator and risk in the namespace RFRidge.Basic.
There are constants , independent of , and , and a threshold such that for every and , with and
features, with probability at least over the data and the features,
The constants are existential: the paper prints them without values, and the values in its appendix are not established by the printed proof. The goal therefore asserts the shape of the bound, which survives any later improvement of the constants.
The proof goes through an analytic decomposition of the excess risk on followed by concentration. The milestones are the results of that proof that are stated as printed:
Theorem 1 shows that, in the basic setting, random features reduce the cost of kernel ridge regression from time and memory to and without losing the minimax-optimal rate. It is the reference result on the statistical cost of random-features approximations, and the same decomposition yields the paper's faster rates under source and capacity conditions (Theorems 2 and 3) and the analysis of data-dependent feature sampling.
To the best of the mission's knowledge, none of these results has a machine-checked proof. Formalizing them requires real infrastructure: integral operators on defined by a kernel with an integral representation, operator inequalities for the continuous functional calculus, and Bernstein inequalities in Hilbert spaces. The Bernstein inequalities and the operator inequalities (Cordes, interpolation, Proposition 8) are reusable well beyond this paper.
The obvious argument controls uniformly and transfers it to the estimator. It needs of order to keep the rate, because a uniform kernel approximation ignores that the estimator only probes through a regularized operator. Getting features requires comparing the integral operators and relative to , in the operator norm weighted by , and this needs fractional powers of operators, operator monotonicity and concentration of random operators. A second subtlety is that the regression function need not lie in the closure of ; Lemma 2 shows that the orthogonal component does not affect any random-features estimator.
All models are posed in Lean 4 with Mathlib. The input space is a separable topological space with its Borel σ-algebra, the feature space is the type W, and is jointly continuous, jointly measurable for the product σ-algebra (an added hypothesis: without second countability it does not follow from continuity), and bounded by everywhere. The RKHS is Mathlib's RKHS ℝ H X ℝ, tied to the kernel by RKHS.kernel H x x' 1 = K x x'. Samples and features are indexed from ; the samples and features have the product law , and is rounded up. "With probability at least " is "the failure event has probability at most ", with and .
Operators: the paper's Hilbert spaces are real, but Mathlib's continuous functional calculus for bounded operators, which defines and , exists only on complex Hilbert spaces. The operator milestones are therefore posed on complex Hilbert spaces, and every inverse or power is the functional calculus of an explicit real function; the real statements follow by complexification. Lemmas 3–5 are stated for abstract positive operators satisfying exactly the relations their proofs use, and add (the range of Assumption 6), without which Lemma 5 is false. Proposition 8 states as a conclusion. Lemma 3 corrects a sign in the exponent of : its display prints where its proof uses ; the printed bound fails for scalar operators.
A trivializing formalization is ruled out: the goal mentions only the estimator, the risk and , never the operators of the proof, and its constants are fixed before and , so they cannot absorb or .
Not included: Theorem 4 (the analytic decomposition), Propositions 5 and 7 (which need Hilbert–Schmidt norms and traces), Lemmas 6–10 and Theorems 5–7 of Appendix A.3–A.4. Contributions of these intermediate results, of a Lean theory of integral operators of kernels, and of Hilbert-space concentration inequalities are welcome.
The projected stochastic subgradient method minimizes an expected loss over a closed convex set : it samples a data point, steps against a sampled subgradient, and projects back onto . For convex its sample complexity has been known for decades, and for smooth nonconvex the stochastic gradient method needs samples to reach gradient norm (Ghadimi–Lan 2013). Many problems in statistical learning and signal processing are neither convex nor smooth — robust phase retrieval, nonlinear regression with an loss, covariance estimation, conditional value-at-risk with smooth losses — but are weakly convex: they become convex after adding a quadratic .
Timeline. Nurminskii (1970s) showed that for weakly convex losses and no constraint the stochastic subgradient method subsequentially converges to a stationary point almost surely, without a rate. Ghadimi and Lan (2013) proved the rate for smooth . Davis and Drusvyatskiy (arXiv:1803.06523, SIAM J. Optim. 2019) proved the first rate for the plain projected stochastic subgradient method on weakly convex problems, measured by the gradient of the Moreau envelope, and for any nonnegative stepsizes. This is Theorem 3.1 of their paper and the goal of this mission.
Work in with the Euclidean norm. Let be nonempty, closed and convex, and let be -weakly convex (): is convex. The problem is
where is on and off .
The subdifferential is the set of with as . For the Moreau envelope and the proximal point of are
Assumption A (stochastic subgradient oracle): on a probability space one can draw i.i.d. samples (A1); there are an open set and a measurable map with for all (A2); and for all (A3).
Algorithm 3.1 with starts at and, for , samples and sets with stepsizes . It returns with drawn from with probability .
For every and any stepsizes with ,
and with , ,
The result. The gradient of the Moreau envelope is a near-stationarity measure: small means that is within of a point with and . Theorem 3.1 therefore gives sample complexity for finding nearly stationary points of nonsmooth nonconvex constrained stochastic problems, matching the smooth case. Estimate (3.3) shows that the Moreau envelope is an approximate Lyapunov function for the method, and it holds for arbitrary nonnegative stepsizes; Theorem 3.4 of the same paper (the proximal extension) needs and a worse constant.
Formalizing it. The result is proved in the paper; no machine-checked version exists. A formalization requires the Fréchet subdifferential of extended-valued functions, the Moreau envelope and its smoothness under weak convexity (Lemma 2.2, which the paper cites as standard rather than proving), and a measure-theoretic treatment of the iterates of a stochastic algorithm on a product probability space. Lemma 2.1 and Lemma 2.2 are reused by the other missions of this series.
The obvious approach — show that decreases in expectation — fails: without smoothness, a subgradient step can increase by an amount of order , not , and no stepsize repairs that. The argument instead tracks the Moreau envelope, which is smooth even though is not; the difficulty moves into (i) Lemma 2.2, the -smoothness of the envelope of a weakly convex function, which is a nontrivial piece of variational analysis, and (ii) the conditional-expectation bookkeeping that turns a one-sample estimate into (3.3) along the random iterates, including the integrability of and , which the paper does not discuss.
EuclideanSpace ℝ (Fin d). An extended-valued function is encoded by its domain and its real values on the domain; is the pair , and is moreauEnv X f lam, a real infimum over . Lemma 2.2 supplies the attainment and differentiability under which this infimum is the paper's envelope.proj constrained by the published nearest-point predicate SpectralProjGrad.Shared.IsProjOnto X proj. It is not the proximal-point predicate of , so that remains meaningful; zero stepsizes are allowed, as in Algorithm 3.1.proj, a stochastic subgradient not tied to by (A2), expectations without integrability, or as a junk-valued infimum would be trivial or false; each is excluded by the statements' hypotheses and conclusions.Proofs of any milestone are welcome; Lemma 2.2 and the product-measure bookkeeping for (3.3) are the reusable parts.
Many platforms match two sides of a market over time: ride-hailing platforms match riders with drivers, blood banks match donated units with patients, organ allocation matches donors with recipients, and retailers pool inventory across fulfilment centres to serve orders from several regions. Demand and supply arrive in several types (locations, blood groups, quality grades), the reward of a match depends on both types, and whatever is not matched today partly waits for tomorrow. A central operational question is which pairs to match first. Static versions of this question go back to the transportation problem and to Monge sequences: Hoffman (1963) characterized the cost matrices for which a fixed greedy order of the arcs solves a transportation problem.
Hu and Zhou (arXiv:1811.07048, published in Manufacturing & Service Operations Management 24(1), 2022) extend this to a stochastic, multi-period setting. They identify conditions on the rewards, the (weak) modified Monge conditions, under which an optimal dynamic policy matches a dominant pair before the neighbouring pairs it dominates. This mission formalizes their main structural result, Theorem 1, and the chain of results it rests on.
There are demand types , supply types , and periods . In period the state is a pair of vectors of available demand and supply. The firm chooses a matching decision , collecting the reward
where the rewards are arbitrary real numbers. The post-matching levels are and , and is feasible if , and . A fraction of unmatched demand and of unmatched supply carries over, and new random quantities arrive. The value function is defined by the dynamic program
with . A matching policy assigns a feasible decision to every period and state; it is optimal if each of these decisions maximizes .
Two neighbouring pairs are compared by the relation . For , means for all , and for all and all ; the relation is defined symmetrically with . The modified Monge condition requires whenever dominates both and ; the paper then writes . For a pair , let be the type- demand left after matching through all pairs that does not dominate, and the analogous supply residual. A decision respects if implies or , and implies or .
Under the modified Monge condition there is a single policy such that, for all and all ,
Theorem 1 replaces the search over all optimal policies, which are state-dependent and generally complex, by a priority structure: whenever dominates a neighbour, the neighbour is matched only once the residual capacity of is exhausted. The paper derives from it the optimality of greedy matching for "perfect" pairs (Proposition 2), the priority order for horizontal (distance-based) and vertical (quality-based) reward structures, and the match-down-to threshold structure of the optimal policy in those models. These results generalize inventory rationing and capacity allocation with upgrading.
The result is proved in the paper, but not completely: the limit argument in the printed proofs of Theorems 1 and 2 ("the quantity transferred converges to zero") is not justified, and Proposition 1 has no printed proof in this version. A machine-checked development would close these gaps and would provide a reusable finite-horizon model with continuous states, concave value functions and an exchange-argument toolkit. No part of this mission is known to be formalized.
The obvious argument starts from an optimal decision and repeatedly applies the transfers of Lemma A.2 and the Monge exchange. Each transfer preserves optimality, but nothing in the printed argument guarantees that the procedure terminates or that its limit has the required property: transfers of different kinds can undo each other's progress, and with equal rewards they can cycle forever. A complete proof has to select the right optimal decision without relying on such an iteration. Before that, the dynamic program itself needs care: the value function is a supremum of an expectation of the next value function, so continuity, concavity, measurability and integrability have to be established together by backward induction, and attainment of the maximum is needed for any optimal policy to exist. Lemma A.1 is a further backward induction in which the multipliers become random and must be averaged.
The Lean development lives in the namespace DynTypeMatching.Priority. Types are Fin m and Fin n; states are Fin m → ℝ, Fin n → ℝ; decisions are Fin m → Fin n → ℝ. Periods are natural numbers with the paper's 1-based indexing, and for . A model Model m n carries , the rewards, , and one arrival law per period on . The paper permits exogenous correlation between periods; its recursion (1) uses per-period laws and does not specify a joint arrival process. The expectation in is over the law of the arrivals entering period .
Every result assumes Model.WellPosed: each arrival law is a probability measure, supported on the nonnegative orthant and integrable, and . Integrability is not stated in the paper, but without it the expectation in (1) is undefined. The value function is a real supremum and the expectation a Bochner integral, so outside the nonnegative orthant, or for non-integrable integrands, Lean returns the junk value 0. All statements therefore quantify over nonnegative states and feasible decisions.
The following hypotheses are added relative to the page, and each is disclosed in the item where it occurs:
Several printed index slips are corrected: the doubled in the Monge exchange, the index ranges in Lemma A.1, and "and" for "or" in the compatibility step.
An optimal decision is defined as a feasible maximizer of over feasible decisions, not through the equation . This rules out a trivializing reading of the goal: a decision that respects the relation but is not optimal (for instance ) does not satisfy it. The goal asserts one policy that is optimal and compatible at the same time.
A complete development needs measurable-function and Bochner-integral calculus on finite-dimensional spaces, concavity and continuity of parametric suprema over polytopes, and compactness arguments for attainment. The model and the exchange lemmas are reusable for later missions on this paper (greedy matching, horizontal and vertical models). Proofs of any milestone are welcome, and so are alternative proofs of the goal.
Bayesian inverse problems for functions — the initial condition of a PDE, a permeability field, a diffusion coefficient — lead to posterior measures on an infinite-dimensional Hilbert space , given by a density with respect to a Gaussian prior . In practice is sampled by Markov chain Monte Carlo on an -dimensional discretisation , and the question that matters is whether the sampler's convergence rate survives the limit . For the standard random-walk Metropolis algorithm it does not (mission III of this series). The preconditioned Crank–Nicolson (pCN) algorithm, whose proposal preserves , was introduced to avoid this (Beskos, Roberts, Stuart and Voss 2008; Cotter, Roberts, Stuart and White 2013).
Hairer, Stuart and Vollmer (2014) prove that pCN has a Wasserstein spectral gap that is uniform in the dimension. Mission I of this series covers their result for globally Lipschitz potentials (Theorem 2.12). This mission covers Theorem 2.14, which needs only that be locally Lipschitz, with a local Lipschitz constant growing slower than any exponential. That class contains potentials of polynomial growth, which arise for nonlinear forward maps.
is a separable real Hilbert space with a centred Gaussian measure , and is an orthonormal basis of eigenvectors of the covariance of . is the span of , and is the image of under the orthogonal projection onto . For a potential the targets are
Fix a step size and put . One pCN step from draws and proposes . The proposal is accepted with probability ; otherwise the chain stays at . Its transition kernel is . The kernel is the same algorithm on with .
Distances between probability measures are Wasserstein lifts of a cost : over couplings of . A kernel is -contracting if implies for a fixed . A set is -small if for all .
The distance of this mission is a weighted path length (3.6). For unit-speed paths from to ,
with () or ().
There are two assumptions. Assumption 2.10 says that for every proposal within distance of the proposal mean is accepted with probability at least , where . Assumption 2.13 says that is -integrable and that for every .
Under Assumption 2.10 with (, ) and Assumption 2.13:
The essential point is that does not depend on .
The paper derives Theorem 2.14 from these, from Lemma 3.2 (Lyapunov functions) and from Proposition 2.6 (the weak Harris theorem of Hairer, Mattingly and Scheutzow 2011). The last two are posed in mission I of this series.
A Wasserstein spectral gap uniform in means that the number of pCN steps needed to reach a given accuracy does not grow with the discretisation level. In §4 of the paper this yields a strong law of large numbers and a central limit theorem for pCN ergodic averages, and, combined with Theorem 2.15, an -spectral gap and mean-square error bounds, all uniform in the dimension. The locally Lipschitz case is the one that covers potentials of polynomial growth.
The result is proved in the paper. It has not been formalized. A formalization would produce a reusable weak-Harris toolkit for Markov kernels on Polish spaces, and a machine-checked account of the path-metric construction, which the paper adapts from Hairer and Majda (2010) and Hairer, Mattingly and Scheutzow (2011). It would also check the paper's proof, whose printed Lemma 3.5 (3) contains a typographical slip in the exponent; the formalized bound is the one the proof derives.
With only locally Lipschitz, no single makes contracting. The probability that exactly one of two coupled chains accepts is controlled by , and far from the origin this exceeds any fixed multiple of . The weighted path distance makes far-out points "close" only when they are very close in norm. But then even the "both accept" move can increase the distance, because the weight changes along the move. Showing that the shrinkage of the proposal mean beats this, while the Gaussian noise term stays integrable uniformly in , is the content of Lemmas 3.5 and 3.6. The order of the choices (, then , then ) is essential.
IsGaussian with mean zero. is a HilbertBasis ℕ whose vectors are pairwise uncorrelated under the covariance bilinear form.Kernel.withDensity. Kernel powers are composition powers, and is Measure.bind.Many stochastic models have a present state that depends on a weighted history of past drift and noise. A stochastic Volterra equation captures this dependence through a kernel : a recent increment and an older increment can enter the current state with different weights. Classical affine diffusions arise from the special constant kernel . For those diffusions, conditional Fourier–Laplace transforms can often be found from finite-dimensional Riccati ordinary differential equations. The paper by Abi Jaber, Larsson and Pulido asks for an analogous transform when the kernel retains memory. Its Theorem 4.3 gives a formula for a continuous affine Volterra process under a stated Riccati–Volterra solution assumption.
The result matters for models in which the history cannot be replaced by the current state alone. The transform characterizes conditional distributions and integrated path functionals in the form used by the paper's later results. The present mission isolates Theorem 4.3 and four of its stated supporting claims. The paper proves these results; the mission seeks machine-checked proofs of their Lean statements.
Fix a positive integer and a deterministic, matrix-valued kernel whose entries are locally square integrable. The Volterra convolution of with a vector function is . Matrix convolutions retain the order of multiplication: .
Let be real symmetric matrices and real column vectors. Their affine covariance and drift are and . The matrix has the as columns. For a complex row , write ; the transpose is ordinary, with no complex conjugation.
An affine Volterra process is a continuous solution of
Here is a -dimensional Brownian motion on a usual stochastic basis, is deterministic, and stays in a state space . The continuous coefficient obeys on , where is positive semidefinite. This is Definition 4.1 and the standing setting of Section 4 of the paper.
The main target is Theorem 4.3. Fix a finite horizon , a complex row , and an integrable complex-row function . Suppose a square-integrable function solves the Riccati–Volterra equation
Define by the stochastic integral and drift in equations (4.4)–(4.5). The theorem identifies with a conditional mean plus a quadratic correction:
It also states that is a local martingale on . If it is a true martingale, then the exponential-affine transform formula is
The milestone list records Lemma 4.2's conditional and unconditional means, the mean Volterra equation stated in the proof of Theorem 4.3, the resolvent commutation claim in the proof of Lemma 4.4, and Lemma 4.4's equivalent Riccati equation. A second-kind resolvent of uses the paper's sign convention for ; the equivalent equation uses .
The conditional transform links a path-dependent stochastic equation to a deterministic nonlinear Volterra equation. It supplies a way to describe the law of a future state together with a linear functional of its past. The conditional-mean milestone separately gives a usable formula for , while the resolvent milestones identify the deterministic kernel relations needed by the transform.
The source provides proofs of these claims. The formalization task is to check their assumptions and equalities against a precise model of Brownian Itô integration, conditional expectation, and matrix convolution. Published Lean definitions for Brownian motion and an Itô integral relation are reused. The affine Volterra process, its Riccati equation, and these theorem statements are drafted here; their proofs remain open.
The conditional payoff involves the entire path before , while generally has no finite-dimensional Markov state. Consequently, the familiar affine-diffusion formula in terms of alone is not the target of Theorem 4.3. Deterministic matrix convolutions are order-sensitive, and the two resolvents of and have different kernels. Stochastic convolutions also have integrands that depend on the terminal time. The passage from fixed-time integral equalities to a continuous local-martingale process requires care about versions and filtration adaptation.
Processes use nonnegative real time, while deterministic kernels and interval integrals use real time. Finite-dimensional conditions are checked componentwise. Kernel and resolvent identities between locally integrable functions hold almost everywhere on positive time. Riccati equations hold almost everywhere on ; stochastic and conditional identities hold almost surely at each fixed time. The local-martingale claim uses the real and imaginary parts of the complex exponential, stopped at .
The process definition includes the Section 4 assumptions on symmetry, covariance positivity, continuity of , deterministic , and the usual stochastic basis. Brownian Itô terms are constrained by the published integral relation. Deterministic drift convolutions require integrable integrands. The theorem asserts integrability of the payoff and of as conclusions, preventing conditional expectation from defaulting to zero. In (4.6) the conditional means enter the -integral through a jointly measurable version in , so that integral cannot default to zero. The dimension is positive, and the theorem does not specialize the kernel to or insert a resolvent assumption into its goal.
A complete development will need reusable results on locally integrable matrix kernels and their resolvents, stochastic Fubini interchange, moment bounds for Volterra solutions, and conditional expectation of the resulting integrals. The moment bound is posed as Lemma 3.1 in the companion existence mission. This draft includes the four listed milestones; Lemmas 2.1 and 2.5 from the source are left for a fuller stochastic Fubini and semimartingale encoding. Contributions that preserve their general hypotheses and conclusions are welcome.
Many problems in statistical learning and signal processing take the form of minimizing an expectation plus a regularizer or constraint , where the only access to is through samples . The classical tool is the stochastic (proximal) subgradient method, which replaces at the current point by a random linear function. Two other methods use richer local approximations: the stochastic proximal point method keeps the whole sampled loss , and the stochastic prox-linear method linearizes only the smooth inner part of a composite loss . In experiments the richer models are markedly less sensitive to the choice of step size.
Davis and Drusvyatskiy (arXiv:1803.06523, SIAM J. Optim. 29(1), 2019) treat all three methods as instances of one scheme, stochastic model-based minimization, in which each step minimizes a sampled one-sided model of plus plus a quadratic penalty. Their main theorem (Theorem 4.3) covers weakly convex problems through the Moreau envelope. This mission formalizes the companion result for the convex setting, Theorem 4.1: when the models lower-bound in expectation without quadratic error and is convex, the expected function gap at a weighted average of the iterates decays like . As the paper notes (p. 22), for the stochastic proximal subgradient method this improves earlier bounds (Cruz 2017; Duchi–Singer 2009) because no subgradient norm of enters the estimate.
Work in with the Euclidean norm. The problem is
where is locally Lipschitz and is closed (its epigraph is closed) with nonempty domain . A function is -weakly convex if is convex; is ordinary convexity.
Assumption B (p. 18) fixes a probability space , an open convex set , real constants , a measurable model on and a measurable such that:
Algorithm 4.1 (p. 19) starts at and, for , samples and sets
The convex setting is and . Write for the step sizes and let be any minimizer of .
For every ,
and with the constant step , ,
The factor in front of is the constant the paper's proof establishes; see Formalization scope.
Theorem 4.1 is the function-value guarantee of the model-based framework. Theorem 4.3 measures progress by the gradient of the Moreau envelope, which is the right quantity for nonconvex problems but says nothing directly about suboptimality; under convexity, Theorem 4.1 gives the familiar rate for the gap itself. It applies to the stochastic proximal point and prox-linear methods as well as to the proximal subgradient method, and §4.2 of the paper uses it for minimizing an expectation of a pointwise maximum of convex functions, such as the conditional value-at-risk. The estimate (4.8) behind it is also the engine of the strongly convex rate (Theorem 4.2, a separate mission of this series).
The result is proved in the paper; nothing in it is open. To our knowledge none of these statements has a machine-checked proof. The formalization contributes a checked version of the one-step estimate (4.8) with its corrected constant, a reusable Lean encoding of Assumption B and of Algorithm 4.1 with extended-valued , and the passage from conditional one-step bounds to expectations over the product measure of the samples.
The argument is short on paper; the work lies in the measure theory the paper leaves implicit. The iterate is an argmin that depends on and on the fresh sample , and the one-step estimate holds only conditionally, with frozen. Turning it into an inequality between unconditional expectations requires measurability of the iterates, independence of from the past, and integrability of and , which the paper takes for granted. The convex function is extended-valued, so the function gap is meaningful only because every iterate and every average lies in .
A naive one-step argument that bounds and separately, each by a Lipschitz constant times , gives the constant in (4.8) and not the printed . The printed constant is false (see below), so the constant cannot be improved simply by tightening that one step.
EuclideanSpace ℝ (Fin d). The extended-valued is a real function together with its domain D; closedness of is closedness of , and convexity is ConvexOn ℝ D. is L and is Lfun.Measure.pi), Fubini–Tonelli over , measurability of the run, Jensen's inequality for a convex function on a convex set, and strong convexity of the subproblem. Proofs of any milestone are welcome, as are a general "conditional one-step bound to expectation over the run" lemma reusable by the other missions of this series.Many problems in statistical learning and signal processing minimize an expectation plus a regularizer or constraint , with access to only through samples . The standard tool is the stochastic (proximal) subgradient method, which replaces at the current point by a random linear function. Two other methods use richer local approximations: the stochastic proximal point method keeps the whole sampled loss , and the stochastic prox-linear method linearizes only the smooth inner map of a composite loss . The richer models are markedly less sensitive to the step size in practice.
Davis and Drusvyatskiy (arXiv:1803.06523, SIAM J. Optim. 29(1), 2019) treat all three methods as instances of one scheme, stochastic model-based minimization: each step minimizes a sampled one-sided model of , plus , plus a quadratic penalty. Their main theorem (Theorem 4.3) concerns weakly convex problems. This mission formalizes the companion result for the strongly convex setting, Theorem 4.2: when the models lower-bound in expectation and is -strongly convex, the expected function gap at a nonuniformly weighted average of the iterates decays like . The weighting is the technique of Schmidt, Le Roux and Bach (2012) for the projected stochastic subgradient method; the paper extends it to the fully proximal, model-based setting (p. 23).
Work in with the Euclidean norm. The problem is
where is locally Lipschitz and is closed (its epigraph is closed) with nonempty domain . A function is -weakly convex if is convex; a negative modulus is -strong convexity.
Assumption B (p. 18) fixes a probability space , an open convex set , real constants , a measurable model on and a measurable such that:
Algorithm 4.1 (p. 19) starts at and, for , samples and sets
The strongly convex setting is and with , run with . Let be any minimizer of .
For every integer ,
together with integrability of the function inside the expectation. The paper prints ; see Formalization scope.
The result. Theorem 4.2 is the rate for a whole family of stochastic methods at once: the stochastic proximal point, prox-linear and proximal subgradient methods all satisfy Assumption B (§4.2 of the paper). The rate is in function values at an explicit averaged point, with explicit constants, and needs neither smoothness of nor bounded subgradients of : the regularizer enters only through the strong convexity of the subproblems. The order is the one Schmidt, Le Roux and Bach obtained for the projected stochastic subgradient method; Theorem 4.2 extends it to models that are not linear and to a general closed .
Formalizing it. The result is proved in the paper; it is not formalized anywhere to our knowledge. Formalizing it pins down the exact constant (the printed one does not follow from the paper's lemmas; see below), the measure-theoretic content of "iterates generated by Algorithm 4.1" (a measurable selection of the argmin, the product measure of the samples, conditional expectation as an integral over one fresh sample) and the integrability that the expectations presuppose. The one-step estimate (4.8) is shared with mission 4 of this series (Theorem 4.1, convex setting); a proof of it serves both.
The telescoping that turns the one-step bound into the rate is elementary once the weights are chosen. The work lies in two places. First, (4.8) itself: it combines the strong convexity of the subproblem, the one-sided accuracy (B2) used in expectation, the Lipschitz bound (B4) at the random point (so the exceptional null set must not depend on that point), Cauchy–Schwarz, and Lemma 4.1. Second, the passage from one step with held fixed to expectations over the whole run: this needs the independence of from (Fubini on the product measure) and integrability of , and along the run, none of which is stated on the page. A natural first attempt, bounding at the average by the average of before checking that the average lies in , is valid only because the weights sum to one and is convex by (B3).
EuclideanSpace ℝ (Fin d). The extended-valued is encoded by its domain D and its real values on D; closedness is closedness of . -strong convexity is -weak convexity: convexity of on D.Measure.pi; expectations are Bochner integrals, and every bounded expectation comes with an integrability conclusion, so a junk value cannot make a bound hold. in (4.8) is the integral over one fresh sample with held fixed.