Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
A chance-constrained program minimizes a cost over decisions subject to the requirement that a random constraint holds with probability at least : , where collects constraint functions and is a risk level. Such constraints model reliability requirements in power systems, finance and engineering design. They are hard to handle numerically: the probability is rarely available in closed form, its sample estimate is a step function of , and the feasible region is in general nonconvex.
Peña-Ordieres, Luedtke and Wächter (arXiv:1905.07377v2; SIAM J. Optim. 30(3), 2020, DOI 10.1137/19M1261985) replace the probability by a smoothed sample quantile, which turns the chance constraint into a single smooth nonlinear constraint, and solve the resulting problem with a trust-region method built on an exact penalty, in the spirit of the SQP method for regular nonlinear programs (Nocedal and Wright). This mission formalizes the analytic core of that method: the smoothed quantile is well defined and has a bounded, Lipschitz gradient, and the piecewise quadratic model used to compute trust-region steps agrees with the penalty function up to second order.
Fix . The smoothed indicator equals on , on , and a strictly decreasing function in between, chosen so that is differentiable (equation (2.2)). The concrete choice is the quartic kernel (2.6),
which makes twice continuously differentiable.
Fix a sample of the random vector. For , the smoothed -quantile is the number solving
It is applied to the vector with entries , and the smoothed sample problem requires .
With deterministic constraints and a penalty parameter , the exact penalty function is
The trust-region step at minimizes the model
where is a symmetric matrix, and .
If and have Lipschitz gradients, each is -Lipschitz with -Lipschitz gradient, is the quartic kernel and , then for fixed there is a constant with
The constant is not specified, so the goal survives any sharpening of the estimate.
Proposition 5.3 is the hypothesis under which the trust-region convergence theory of Conn, Gould and Toint (cited as Theorem 5.4, from their Theorem 11.2.5) applies: it guarantees that the method of §5 converges to stationary points of . Combined with the exact-penalty result of Curtis and Overton (cited as Theorem 5.2), which says that for large enough local minimizers of the smoothed problem are local minimizers of , this justifies solving the smoothed chance-constrained problem by minimizing . Proposition 4.1 is independently useful: it says that the smoothed quantile can be handed to any smooth nonlinear solver as a constraint with a bounded, Lipschitz gradient.
The results are proved in the paper. None of them has a machine-checked proof that this mission is aware of. A formalization would also settle two points the printed proofs leave thin: the uniform lower bound on the denominator in Proposition 4.1, which the paper asserts without argument, and the existence part of Lemma 2.1, whose printed proof argues only uniqueness.
The model error splits into three parts. The and parts are standard Taylor estimates. The quantile part is the substance. First, is defined only implicitly, so its differentiability needs the implicit function theorem, and its gradient bound needs a lower bound on that is uniform over all , not just pointwise. The pointwise statement is easy: some sample lies strictly inside the smoothing window. The uniform statement needs a quantitative version of that fact, which uses the fractional part of . Second, is a maximum of smooth functions and is not differentiable, so the model linearizes each before taking the maximum; one has to show this costs only , uniformly in .
All objects are defined in one module, SmoothCCP.PenaltyModel.Setting. Decisions and directions live in EuclideanSpace ℝ (Fin n), so gradients and are inner products. is a self-adjoint continuous linear operator and is its operator norm. Sample values are a fixed list ξs : Fin N → Ξ; this mission involves no probability. is a function on Fin N → ℝ (sup norm), defined as the least root of (2.3) via sInf. Its gradient is the Fréchet derivative. is deriv of the smoothed indicator, which is differentiable for the quartic kernel, including at . The maximum over uses Finset.sup' and needs (the paper's §5 has ). The Euclidean norm on appears explicitly only in milestone 5, where it is written to match the printed factor .
Standing hypotheses: , , , and . From Proposition 4.1 on, is the quartic kernel. Three readings are disclosed in the goal's statement. The Lipschitz hypotheses (5.4)–(5.5) are assumed on all of and per component , because the conclusion ranges over all . The quartic kernel and are assumed because the proof uses Proposition 4.1. The constant is quantified after all data and and before , , .
is the paper's quantile, defined from (2.3), not a function assumed to satisfy it. A statement in which the uniform constant may depend on , or , or in which (2.3) has no root, would be trivial and is excluded.
A complete development needs the implicit function theorem for (Mathlib's HasStrictFDerivAt.implicitFunction or a one-dimensional argument), first-order Taylor bounds for functions with Lipschitz gradients, and elementary facts about the quartic kernel. The Taylor bounds and the facts about maxima of linearizations are reusable beyond this mission. Proofs of any milestone are welcome independently.
A chance-constrained program asks for a decision that satisfies uncertain constraints with high probability rather than surely:
Such models appear in power-system operation, portfolio selection, chemical-process and reservoir management, and other settings where requiring the constraints for every realization is too conservative (Nemirovski–Shapiro 2006; the paper's introduction lists applications). The probability is rarely available in closed form, and when the distribution of is only accessible through samples, the feasible set of the empirical counterpart is a union of polyhedral-like pieces: it is non-smooth and non-convex, and the empirical quantile introduces many spurious local minima (Peña-Ordieres, Luedtke, Wächter 2020, §2).
Peña-Ordieres, Luedtke and Wächter replace the indicator inside the empirical probability by a smooth kernel with bandwidth , which turns the sample constraint into a differentiable one suitable for nonlinear programming solvers. This mission formalizes the paper's consistency result: as the sample size grows and the bandwidth shrinks, jointly, the optimal values and optimal solutions of the smoothed sample problem converge to those of the true problem with probability one.
Timeline. Consistency of sample approximations of chance constraints with the plain empirical cdf goes back to Pagnoncelli, Ahmed, Shapiro 2009 (reference [36] of the paper; its Propositions 2.1 and 2.2). Luedtke–Ahmed 2008 gave finite-sample feasibility guarantees for the same empirical approximation. Convergence with respect to a smoothing parameter alone was studied by Geletu, Hoffmann, Klöppel and Li (SIAM J. Optim. 27, 2017), Hong, Yang, Zhang 2011 and Hu, Hong and Zhang (IIE Trans. 45, 2013) (references [15], [25], [26] of the paper). Peña-Ordieres–Luedtke–Wächter 2020 (SIAM J. Optim. 30(3)) treat both parameters simultaneously; Theorem 3.5 of the preprint arXiv:1905.07377v2 is the result posed here.
Decisions are vectors restricted to a closed set . The random data takes values in a measurable space with law . The constraints are aggregated into one scalar function , and the risk level is .
The standing assumptions are: Assumption 3.1, for each the random variable has a continuous distribution; Assumption 3.2, is Carathéodory, i.e. is measurable for each and is continuous for almost every ; Assumption 3.3, some optimal solution of (1.1) is a limit of points with .
If is compact, is continuous and Assumptions 3.1–3.3 hold, then with probability one, as and jointly,
Theorem 3.5 justifies solving the smooth problem (2.4) in place of (1.1): with enough samples and a small enough bandwidth, global solutions of the surrogate approximate global solutions of the chance-constrained program, and the optimal values agree in the limit. Unlike earlier results it controls the two approximation errors, sampling and smoothing, at once, so no order of limits has to be chosen in practice. It is the asymptotic counterpart of the paper's finite-sample feasibility bound (Theorem 3.13) and the theoretical basis for the trust-region method of §5.
The result is proved in the paper, with two steps imported from Shapiro–Dentcheva–Ruszczyński, second edition (a uniform law of large numbers, Theorem 7.53, and a convergence-of-expectations result, Theorem 4.91) and the deviation statement deferred to Theorem 5.3 there. None of these results, and no consistency theorem for sample approximations of chance constraints, is machine-checked on Prove2Me or, as far as is known, elsewhere. A formal proof requires writing the imported steps out for the specific integrands of this problem and completing the solution-set argument the paper leaves to the reference.
The pointwise statements are routine; the uniformity is not. The integrand converges, as , to the indicator , which is discontinuous in wherever . A uniform law of large numbers for a family that degenerates into indicators needs the no-atom Assumption 3.1 at every point of , not only at the limit. Moreover, the smoothing functions for different are unrelated, so the family is not continuous in , and a Glivenko–Cantelli argument over a joint parameter cannot be applied directly. The convergence of solution sets needs, in addition, that the limit of feasible points of (2.4) is feasible for (1.1), which uses the continuity of on ; that continuity again rests on Assumptions 3.1 and 3.2.
Fin n → ℝ with the sup norm. Assumption 3.3 is stated for every radius, so the norm choice does not change it.ξ : ℕ → Ω → Ξ of measurable, independent maps on a probability space, each with law ; uses the first draws.atTop ×ˢ 𝓝[>] 0 on , with because needs it; one null set serves every conclusion of a statement.The definitions layer (Γ_ε, admissibility, , , , , the shifted sample sets (3.2)) is shared with the companion mission on finite-sample feasibility. A uniform law of large numbers for almost-surely continuous, bounded integrands on a compact parameter set, and convergence of optimal values under uniform convergence of constraint functions, are reusable beyond this mission; contributions of either as standalone lemmas are welcome.
How many edges can a graph have if it contains no long cycle? This Turán-type question for the circumference goes back to Erdős and Gallai (1959), who showed that an -vertex graph with circumference has at most edges. For 2-connected graphs the answer is exact and the extremal graphs are known, so the natural next question is stability: what does a graph look like when its edge count is just below the extremal value? Such statements are the standard input for exact results via the stability method, and for counting and spectral variants of the original problem.
Timeline.
All graphs are finite and simple, with vertex set . The circumference is the length (number of edges) of a longest cycle. is 2-connected if it has at least three vertices and stays connected after deleting any one vertex. is the minimum degree and the number of edges.
For , the graph is a clique together with further vertices, each joined to the same vertices of the clique. It has vertices, minimum degree , circumference , and
edges. The graph is the union of a clique and cliques , any two of the cliques sharing the same two vertices. The families and consist of graphs on (resp. ) with a clique of size , stable and complete to . In every vertex of has exactly two neighbours, the same and . In , carries a star forest whose stars all attach to the same two vertices in a prescribed way.
The proof works with the -closure of a cycle . It is obtained by replacing by its -closure, which repeatedly joins non-adjacent pairs of whose degree sum is at least . A cycle is locally maximal if every longer cycle uses at least three edges between and the rest of the graph.
Let and let be 2-connected on vertices with and circumference , . If
then , or , or (, odd, and is a subgraph of a member of ), or ( and ).
For a longest cycle , the same hypotheses give one of four alternatives. Either ; or ; or the alternative holds; or and .
The milestones follow the paper's proof.
The theorem describes every 2-connected graph whose edge count comes within one step of Woodall's extremal bound in either parameter. At it recovers the theorem of Füredi, Kostochka, Luo and Verstraëte exactly. At it refines the Li–Ning / Füredi–Kostochka–Luo stability theorem for non-Hamiltonian 2-connected graphs. It also gives Corollary 1.8 for 3-connected graphs, where only the two graphs remain. Theorem 1.9 goes further and identifies the extremal configurations exactly, up to the closure.
On the formal side, Mathlib has walks, cycles, Hamiltonian paths and cycles, clique numbers and graph embeddings. It has no circumference theory, no Bondy–Chvátal closure, no Hamiltonian-connectedness and none of the classical extremal results the proof cites (Dirac, Bondy, Chvátal, Erdős–Gallai, Fan). No result of this mission is known to have a machine-checked proof. The mission asks for the paper's proof, or any other proof, of the goal; for its refinement, Theorem 1.9; and for the closure and attachment lemmas on the way.
The obvious approach is to delete a low-degree vertex and induct, as in the classical proofs of Erdős–Gallai type bounds. It does not reach stability. Deleting a vertex can destroy 2-connectivity, and the extremal family changes with : the threshold moves with the minimum degree, and the new graph appears only for .
The edges inside are the hard part. A longest cycle gives no direct control over . The paper's route needs two non-trivial reductions:
After that, Lemma 4.2 is four pages of degree-sequence casework, and Lemma 4.4 is a ten-claim structural argument.
Vertices are Fin n and graphs are Mathlib SimpleGraphs. Further conventions:
⊑, a subgraph up to relabelling), and "" or "" is a graph isomorphism.Added hypothesis: in Theorems 1.7, 1.9, 4.1 and Lemma 4.4. As printed, the theorems claim every , but they fail at : a member of with is 2-connected, has circumference and edges, yet lies in neither nor . also divides by . Lemma 4.3 has no minimum-degree hypothesis and is stated for every .
Trivializations ruled out.
Infrastructure. A complete development needs:
All of these are reusable well beyond this mission, and contributions of any of them are welcome. Theorem 1.12 is also the goal of the companion mission on the stability of Bondy's theorem.
Mean field games describe large populations of agents who interact symmetrically: every agent sees the same average of all the others. Many populations interact instead along a network, where each agent responds only to its neighbours. Lacker and Soret (arXiv:2005.14102v2, 2021; Math. Oper. Res. 2022) study a linear-quadratic stochastic differential game on a finite graph that is simple enough to solve explicitly on every vertex-transitive graph, and then ask what happens to the equilibrium as the graph grows. The question is the network analogue of the classical convergence problem for mean field games: does the -player equilibrium have a limit, and does that limit depend on the graph only through a small amount of information?
The answer of the paper is that the limit is governed by the empirical eigenvalue distribution of the graph Laplacian. Dense graph sequences (degrees tending to infinity) all have the same limit, the mean field game; sparse ones (bounded degrees) have limits that depend on the graph, through its spectrum. This mission formalizes that large-graph limit theorem, Theorem 2.6 of the paper. Mission I of the series formalizes the explicit equilibrium on a fixed transitive graph (Theorem 2.5), on which this mission builds.
Let be a finite simple graph on vertex set with adjacency matrix and degree matrix . Its Laplacian is . is transitive if every vertex can be mapped to every other one by a graph automorphism; such a graph is regular, of degree , and is then symmetric with eigenvalues . The empirical eigenvalue distribution is .
Fix a horizon , a volatility and a weight . Player controls the state
driven by independent Brownian motions, with Markovian feedback controls , and pays
On a transitive graph without isolated vertices, Theorem 2.5 gives an explicit Nash equilibrium: with and the solution of , on , the feedback is with . The resulting equilibrium state process is Gaussian, and the value is .
For a probability measure define , so that .
Let be finite transitive graphs without isolated vertices, , with , and suppose weakly for a probability measure . Then (1) the ODE , has a unique solution on ; (2) for every vertex sequence and ,
(3) the empirical measure converges weakly in probability to ; (4)
The milestones are the statements the paper's proof (§3, §6, §7.1) relies on: the stability of in (Proposition 3.2, last sentence); the finite-graph variance formula (2.7); monotonicity and concavity of (Proposition 3.3, first sentence); correlation decay (Proposition 2.12) for distinct vertices; the relation between degrees and the spectral limit (Lemma 7.1); the Gaussian Poincaré bound (7.3) and the concentration (7.1) of the empirical measure; and the spectral form (2.9) of the value.
Theorem 2.6 reduces the large-population behaviour of a network game to one spectral object. For complete graphs and the limit is the mean field game; for sparse sequences such as cycles, tori, or random regular graphs, is a non-degenerate measure and the limiting variance and value differ from the mean field ones. The theorem thereby gives a quantitative criterion for when a mean field approximation of a network game is accurate, and it shows propagation of chaos in both regimes: in the dense case because interactions are weak, in the sparse case because typical players are far apart in the graph.
The result is proved in the paper; none of it has been machine-checked. A complete formalization requires a Lean account of Gaussian laws of linear SDEs with additive noise, of weak convergence of spectral measures of graph Laplacians, and of a Gaussian Poincaré inequality, none of which is currently in Mathlib in the needed form. Each of these is reusable well beyond this mission.
Parts (2) and (4) follow from the finite-graph formulas once uniformly, but that convergence requires stability of a nonlinear ODE whose vector field is defined through the spectral measure, uniformly over a class of measures. The harder step is (3). Convergence of one player's law does not imply convergence of the empirical measure: the players are correlated, and on sparse graphs every player has a bounded number of strong neighbours, so the correlations do not vanish uniformly. Bounding them requires an estimate that decays in the graph distance and in the degree, and combining it with the growth of graph balls, which is controlled differently in the dense and in the sparse regime. The usual mean field route is closed: unless the graph is complete, the state vector is not exchangeable, so propagation-of-chaos arguments based on exchangeability do not apply.
The Lean development lives in namespace GraphLQGame.Asymptotics.
Fin n; a graph sequence is G : ∀ k, SimpleGraph (Fin (N k)) with .lapMatrix. is built from the real roots of the characteristic polynomial of , with multiplicity.gaussianReal 0 V.toNNReal; .The goal quantifies over every solution , and every equilibrium state process, and also asserts that the graph ODE solutions and the state processes exist, so it cannot be discharged vacuously. Proposition 2.12 is stated for distinct vertices: as printed, (2.17) is also claimed for , where it fails on complete graphs of large degree; the off-diagonal case is the one the proof of Theorem 2.6 uses. Theorem 2.5 (mission I) is not restated here; a solver proves what is needed of it.
Contributions are welcome at every level: Gaussian laws of linear SDEs, spectral measures of graph matrices, ODE stability, a Gaussian Poincaré inequality, and the milestones themselves.
Mean field games (MFGs) describe the limit of symmetric stochastic differential games as the number of players tends to infinity, when every player interacts with the empirical distribution of all the others. Their main practical use is the converse direction: an equilibrium of the limiting game supplies a simple, decentralized control that is an approximate Nash equilibrium of the game with finitely many players. For the complete graph, where everybody interacts with everybody, this is classical, with the standard rate (Carmona and Delarue, Probabilistic Theory of Mean Field Games, Vol. II, §6.1; Huang, Malhamé and Caines 2006, Theorem 12), as recalled on p. 10 of the paper.
Many interacting systems are not complete graphs: players see only their neighbours in a network. The question is then how dense the network must be for the mean field approximation to remain valid. Lacker and Soret (arXiv:2005.14102v2) answer it exactly for a linear-quadratic "flocking" game, where explicit computations are possible. This mission formalizes their Theorem 2.11, which applies to every finite graph, with no transitivity or regularity assumed.
Let be a finite simple graph on the vertex set ; means and are adjacent and is the number of neighbours of . Fix a horizon , a volatility and a cost weight . Each player controls a real state through
where are independent standard Brownian motions and . A Markovian control is a Borel function of time and the full state , of linear growth. The cost of player under a profile is
and for an isolated vertex: each player wants to end near the average of its neighbours at minimal quadratic effort. For a vector , a profile is a Markovian -Nash equilibrium if no player can lower its cost by more than by switching unilaterally to another control , written .
The mean-field control is
each player looks only at its own state, as if its neighbours' average were frozen at its mean.
Define if and if , and with the minimal degree ,
Then, with zero initial states, the state equation for has a solution, and
The result. Theorem 2.11 gives an explicit threshold for the mean field approximation on networks: along any sequence of graphs whose minimal degree diverges, the decentralized control is an -Nash equilibrium with , and the vector form says more: if the average of over vertices tends to zero, the per-player errors vanish on average (the paper's (2.16)). The rate quantifies how the accuracy of the approximation depends on denseness. In the same paper, transitive graphs whose degrees stay bounded lead to equilibria that do not agree with the mean field one, so a denseness condition cannot be dropped.
Formalizing it. The theorem is proved in the paper; to our knowledge no part of it is machine-checked. A formal development needs, beyond the statement, a verification argument for a one-dimensional linear-quadratic control problem with additive noise, Gaussian computations for linear SDEs driven by Brownian motion, and the comparison of costs between the equilibrium system and a system with one deviating player. The one-player result (Lemma 7.2) and the Gaussian facts of (7.7) are reusable well beyond this mission.
The obvious argument compares a deviating player with an isolated player and treats the neighbour average as noise independent of the deviation. Two things stand in the way. The cost of player couples its terminal state with the neighbours' average through a cross term , and the deviation may look at the neighbours' states, so the cross term does not vanish; it has to be bounded through the size of the deviation's energy. And an arbitrary deviation has no a priori energy bound: one is available only for deviations that do at least as well as the zero control, which is why the argument passes through a (near-)optimal deviation. Lemma 7.2 itself requires a verification theorem over all progressively measurable controls, not only feedback ones.
The Lean development lives in the namespace GraphLQGame.DenseApprox and uses the shared encoding of this series:
Fin n (the paper's become ), the state space is EthierKurtz.SDEState n, and is any SimpleGraph (Fin n); isolated vertices are allowed;A formalization in which is compared only with deviations depending on the player's own state, or in which the costs are Bochner integrals that vanish when not integrable, would be trivially or wrongly satisfied; both are ruled out by the encoding above.
Welcome contributions: the verification argument for Lemma 7.2, the Gaussian law of linear SDEs with additive noise, and proofs of the three steps. Related missions in this series: I (an explicit Nash equilibrium on transitive graphs) and II (large-graph limits).
The circumference of a graph is the length of a longest cycle. Extremal graph theory asks how many edges force a long cycle. The Erdős–Gallai theorem (1959) states that every -vertex graph has at most edges. Bondy (1971) strengthened it by counting only the edges near a longest cycle: if is a longest cycle of length , the number of edges with at most one endpoint in is at most , and at most when is 2-connected. Since spans at most edges, this implies the Erdős–Gallai bound.
A stability result complements an extremal one: a graph close to the extremal bound must be close in structure to the extremal graphs. Jie Ma and Bo Ning (Combinatorica, 2020; arXiv:1708.00704) proved stability versions of Kopylov's edge theorem for 2-connected graphs of given circumference and of Bondy's theorem above. This mission formalizes their stability version of Bondy's theorem, Theorem 1.12. In the paper it is also one of the two halves of the proof of the main stability theorem; the other half is a separate mission in this series.
Timeline (as recorded in §1 of the paper). Dirac (1952): every 2-connected graph has . Erdős and Gallai (1959): . Bondy (1971): the bound on edges with at most one endpoint on a longest cycle, and the degree theorem stated here as Theorem 2.1. Woodall (1976): for 2-connected with circumference . Kopylov (1977): for 2-connected with circumference ; another proof by Fan, Lv and Wang (2004). Fan (1990): an improved version of Bondy's bound for 2-connected graphs, and average-degree bounds on long paths. Füredi, Kostochka and Verstraëte (2016): stability for Kopylov's theorem when ; Füredi, Kostochka, Luo and Verstraëte (2018): the complete stability version, with the families , . Ma and Ning (2017 preprint, 2020): the results of this mission.
All graphs are finite and simple, on the vertex set . A path or cycle of length has edges. A graph is 2-connected if it has at least three vertices, is connected, and remains connected after deleting any one vertex. A cycle is a longest cycle if no cycle of has more edges; is its vertex set and its length.
For a longest cycle , write for the number of edges with at most one endpoint in . A vertex is an isolated vertex of if and every neighbour of lies on ; is its number of neighbours on .
The extremal graphs are:
means that is isomorphic to a subgraph of .
Let be 2-connected on vertices and a longest cycle of length with . If
then , or is odd and is a subgraph of a member of .
In every one of the vertices off a longest cycle sends edges to the cycle, so Bondy's bound is attained. Theorem 1.12 says that exceeding already leaves only three structures: a subgraph of , or for odd a subgraph of a member of or . In the paper it is one of the two cases of the proof of the main stability theorem (Theorem 1.9): a graph with many edges and a longest cycle has either many edges with at most one endpoint on , handled here, or many edges inside , handled by the closure argument of the companion mission.
The result is proved in the paper; none of it, nor Bondy's or Fan's theorems, is formalized on the platform or in Mathlib. The mission produces machine-checked statements of the goal, of the cited tools (Bondy's Theorem 2.1, Fan's Theorem 2.2, Lemma 2.3), and of the steps Theorems 3.1, 3.2 and Lemma 3.3, together with reusable definitions of 2-connectivity, longest cycles and the extremal families.
The obvious approach counts edges at the vertices off : each such vertex has at most neighbours on , since otherwise two consecutive cycle vertices would let the cycle be extended. This bound is far from enough. The edge count also includes edges between vertices off , and components of can be large, 2-connected, and attached to in complicated ways. The bound has to be beaten by every such configuration at once, and Theorem 3.2 states exceptional small cycle lengths for which the analysis does not close. A second difficulty is the passage from one vertex of degree to a global description of : in the odd case, the structure of every component of has to be determined, which is where the families and appear.
Graphs are SimpleGraph (Fin n) with decidable adjacency. A cycle is a closed walk C : G.Walk u u with C.IsCycle; its length is C.length and its vertex set C.support.toFinset. "Longest cycle" is the predicate that every cycle of is at most as long as ; no supremum of cycle lengths is used. 2-connectivity is: at least three vertices, connected, and connected after deleting any one vertex. It is stated for an arbitrary finite vertex type so that it applies to the induced subgraph in Lemma 2.3. The edge count off is the number of edges with an endpoint outside , and is natural-number division; under the stated bounds every natural-number subtraction is exact.
is defined on fixed labels (clique , hubs ), and "" is a graph embedding G ⊑ W. Membership in and are predicates on labelled graphs, closed under relabelling, and " is a subgraph of a member" is G ≤ H for some member . No hypothesis is added to any statement. Fan's Theorem 2.2 is stated without its equality characterization.
Trivializing formalizations are ruled out explicitly: the alternative " is odd and …" is a conjunction, never an implication; the circumference is never a junk supremum; containment in is up to isomorphism, never ≤ on fixed labels; and 2-connectivity excludes and disconnected graphs.
The definitions are reusable for any work on circumference, longest cycles and Bondy–Erdős–Gallai-type problems. Contributions of proofs of the cited tools (Bondy's and Fan's theorems) are especially welcome, as is a proof of Erdős–Gallai's edge theorem, which the proof of Theorem 3.2 uses and which is posed elsewhere on the platform.
Distributionally robust stochastic optimization (DRSO) chooses a decision to minimize the worst expected loss over an ambiguity set of probability distributions, instead of the expectation under one estimated distribution. When is a ball around a nominal distribution (often the empirical distribution of data) in the Wasserstein distance, the set contains distributions with supports different from that of , and the worst case is driven by how far mass can be moved and how fast the loss grows along the way. This makes Wasserstein balls a standard choice in data-driven optimization, statistical learning and operations research.
The inner problem, a supremum over an infinite-dimensional set of measures, is not directly computable. Gao and Kleywegt (arXiv:1604.02199v3) show that it equals a minimization over a single scalar multiplier, for an arbitrary Polish space and nominal distribution and a merely measurable loss.
Timeline. Esfahani and Kuhn (2018, doi:10.1007/s10107-017-1172-1) proved a strong duality for and empirical on , giving finite convex reformulations for piecewise-affine losses. Blanchet and Murthy (2019, doi:10.1287/moor.2018.0936) proved duality for general optimal transport costs on Polish spaces under upper semicontinuity of the loss, with a dual over pairs . Gao and Kleywegt's result, first posted in 2016 and published in Mathematics of Operations Research (2023, doi:10.1287/moor.2022.1275), covers every order , every nominal and every measurable loss with finite growth rate, with a dual in one variable.
Let be a Polish space (complete, separable metric) with its Borel -algebra, the Borel probability measures, and . The decision variable is suppressed: is a Borel measurable loss with for a fixed nominal distribution .
The Wasserstein distance of order is given by
The primal value is the worst-case expectation over the Wasserstein ball,
The regularization operator is , the dual objective is , and the dual value is . The growth rate of is
with if no qualifies. The lemmas also use the near-optimal distances and , the limits as of the largest and smallest over -minimizers of .
In Lean these objects are DRSOWass.Duality.wassPow, vP, Phi, dualObj, vD, growthRate, DUpper, DLower.
If , then
This is the printed theorem: an equality of values together with finiteness. It fixes no constant and needs no regularity of beyond measurability and integrability.
The result. Strong duality turns the worst-case expectation over a Wasserstein ball into a convex problem in one scalar, , where is a Moreau–Yosida-type regularization of . For finite-supported this yields finite-dimensional reformulations of DRSO; the paper derives from it the structure of worst-case distributions (Corollaries 1 and 2) and applications to two-stage problems, point processes and Gaussian nominal distributions. The growth rate separates the finite case (this theorem) from the case (Proposition 2).
Formalizing it. The theorem is proved in the paper; to the best of current knowledge none of it is machine-checked. The mission produces a formal statement of the duality on general Polish spaces, together with reusable pieces: extended-valued integrals, the regularization operator and its one-sided derivatives, measurable selection on Polish spaces, and push-forward constructions of near-optimal measures. Formal proofs of Lemma 3 also give measurable-selection tools that Mathlib does not yet provide in this form.
Weak duality is a one-line Lagrangian argument. The difficulty is attainment from the primal side: one must construct, for every , a distribution in the ball whose expectation is within of . A worst-case distribution need not exist (when mass escapes to infinity), so a compactness argument on fails; and is only measurable, so the infimum defining cannot be reduced to a countable one, and the measurability of and of near-optimal transport maps needs projection and measurable-selection theorems for analytic sets. The case analysis on whether the dual minimizer exceeds is forced by the possible non-differentiability of at .
MetricSpace, CompleteSpace, SecondCountableTopology and BorelSpace instances; is a probability measure; is dist ξ ζ ^ p with real .RWPI.SqrtLasso.transportCost with cost , an infimum over probability couplings in ; is written .ModelRiskOT.Duality.extIntegral, in (with ). , , , are EReal-valued; , , are ENNReal-valued, so is representable and the empty infimum is .A complete development needs couplings and gluing in Mathlib's measure theory, the measurable projection theorem and a measurable selection theorem on Polish spaces, and one-sided derivatives of concave extended-valued functions; the first three are reusable well beyond this mission. Proofs of any milestone, alternative proofs of the goal (e.g. through the Blanchet–Murthy dual), and the companion result Proposition 2 () are welcome.
A recurring question in revenue management with strategic consumers is whether a seller gains from price commitment. When customers are forward-looking, a seller who announces its whole price path in advance (pre-announced pricing) removes the customers' incentive to wait for a markdown the seller would otherwise be tempted to give; a seller who keeps the freedom to set later prices after observing the market (responsive pricing) cannot credibly promise not to cut prices. In the classical models without learning, commitment is valuable: Aviv and Pazgal (2008) find that announced pricing extracts more profit than contingent pricing from forward-looking customers, and Besanko and Winston (1990) analyse the responsive monopolist facing rational consumers.
Papanastasiou and Savva (Management Science, 2017) add social learning (SL): early buyers post product reviews, and the customers still in the market update their beliefs about the product's quality before deciding whether to buy later. The reviews create an informational reason to wait, and they also give the responsive seller something to respond to. This mission formalizes the paper's §7, which asks whether commitment remains valuable once learning is present, and its answer: for impatient consumers it is not.
A monopolist sells over two periods to a continuum of consumers of mass one. Consumer has a preference , uniform on . Mean product quality is unknown; consumers share the prior , and reviews carry noise of variance . The SL parameter is . Consumers discount second-period utility by ; the firm does not discount; the unit cost is .
If a mass of consumers buys in period 1, the posterior mean that the remaining consumers see is, before the reviews arrive, distributed as
the pre-posterior law (Lemma 1); when it is the point mass at . A remaining consumer of type who buys in period 2 at price gets .
The optimal values and are the suprema of expected profit over all prices and all equilibria. In Lean these are preValue P and respValue P for a parameter record P : Params, and P.withδc d is the same model with discount factor ; "absence of SL" is P.noSL, the same model with .
In the presence of SL there is a threshold such that
with , and fixed on both sides. The threshold is not specified; only its positivity is claimed.
Without SL (), both values are finite and
strictly positive for .
The two propositions together reverse a standard prediction. Without learning, commitment weakly dominates (Proposition 7, consistent with Aviv and Pazgal 2008). With learning and impatient consumers, flexibility strictly dominates (Proposition 8): the value of reacting to reviews outweighs the cost of being unable to commit. The paper's numerical study (Figure 4) suggests that the threshold equals one for moderate , so that responsive pricing wins for every discount factor; that numerical claim is not a theorem of the paper and is not posed here.
The results are proved in the paper; to the best of current knowledge none of them has a machine-checked proof. Formalizing them requires a rigorous treatment of a continuum purchasing game whose equilibrium is defined through a Gaussian law whose variance depends on the equilibrium itself, the subgame-perfect second-period pricing rule, and the continuity of optimal values in a parameter.
The comparison at is elementary in spirit: myopic consumers buy early exactly when , so the two regimes produce the same reviews for the same , and the responsive firm can only do better state by state. Turning this into a strict inequality between two suprema requires a uniform gap, not just a pointwise one, because the paper's argument assumes an optimal pre-announced plan exists.
The step that extends the result to is the paper's appeal to the Maximum Theorem. It needs the expected profit to be jointly continuous in the prices and in over a compact set of relevant plans. But the expected profit depends on through the equilibrium threshold, which is defined implicitly by an indifference equation whose Gaussian kernel itself depends on the threshold (equations (3) and (9)), and equilibria are sets of types, not numbers. Continuity of the optimal value therefore requires continuity and uniqueness of these implicit thresholds, and a reduction of both suprema to compact sets of prices.
The model is one shared definition module (SLPricing.Compare.Model), plus the formula (6) as p2Star. Conventions it commits to:
Added hypotheses, disclosed in each item: in the two threshold milestones; for the uniqueness clause of Lemma 3. Proposition 7's "higher" is stated as the proof states it: non-negative gap on , strict on .
The comparison is meaningful only because the responsive firm cannot commit. Enlarging the responsive regime to arbitrary second-period rules, or defining either optimal value as a real supremum (whose junk value is on unbounded sets), would make the goal trivial or empty; both are excluded by the definitions. Hard-wiring the thresholds , or the price (6) into the definitions would make the milestones definitional; they are theorems here.
A complete development needs: Gaussian expectations of piecewise-linear functions of and their continuity in the variance; the implicit-function argument for the thresholds; a Maximum Theorem (Berge) for the optimal values. The Gaussian convex-order and Maximum-Theorem pieces are reusable well beyond this mission, and contributions of them as separate theorems are welcome.
Most business-to-business sales are not paid in cash on delivery. The supplier lets the buyer pay later, which is trade credit, and often offers a discount for paying early. In the classic "2/10 net 30" the buyer gets 2% off for paying within 10 days and otherwise owes the full price in 30 days. Trade credit is a major source of short-term finance for firms. Empirical work documents both forms of contract: net terms, with one price and no discount, and two-part terms, with an early-payment discount. The discounts are large, and they vary a lot from one buyer to another (Petersen and Rajan 1997; Klapper, Laeven and Rajan 2012). The implied interest rate on a forgone discount is often far above a bank loan's. This raises two questions: why do cash-poor buyers use trade credit at all, and when should a supplier offer a discount?
Yang and Birge (Management Science 2018) answer this in a supplier–retailer model with a financially constrained retailer, who can finance inventory with a bank loan, with trade credit, or with both. Their answer is risk sharing. Trade credit is repaid out of realized sales, so the supplier bears part of the demand risk. She can therefore induce a larger order than a price-only contract does. The model builds on the selling-to-the-newsvendor model of Lariviere and Porteus (2001), and it complements the supplier-versus-bank analysis of Kouvelis and Zhao (2012). This mission formalizes the paper's main result on the structure of the optimal contract.
A retailer buys a single good from a supplier at unit cost and sells it at unit price . Demand is random with density on . Its distribution function is , the complementary distribution function is , the failure rate is , and the generalized failure rate is . Demand has an increasing failure rate (IFR). The retailer has cash .
The supplier offers a cash price and a credit price , with . The early-payment discount is . If the retailer's cash does not cover his cash purchases, he borrows from a competitive bank. The bank loan is senior to trade credit. A bank and a supplier recovering a defaulted claim lose fractions and of what they recover, with .
Default is described by two thresholds. The bank-loan default threshold is the demand below which the bank is not repaid in full, and it equals the amount owed to the bank. The trade-credit default threshold is the demand below which the supplier is not repaid in full. The retailer uses a bank loan iff , and uses trade credit iff .
The paper shows (p. 13) that the supplier's problem can be written in the thresholds alone. Let
The retailer orders , the prices are and , and the discount is . The supplier's expected profit is
She maximizes over a domain of thresholds. A maximizer is an optimal trade credit contract. Net terms correspond to , which is . Two-part terms correspond to .
For every optimal contract :
If , or if is sufficiently large, then and (net terms, no bank loan). If and is sufficiently small, then
"Sufficiently large" and "sufficiently small" are existential thresholds on that depend on the data , not on the contract.
They are listed in the order the proof uses them:
Proposition 3 is the paper's prediction about inventory financing portfolios. Once the supplier sets the terms, a retailer who needs external financing always uses trade credit. Early-payment discounts appear only when supplier default is costly and the retailer is cash-poor. A discount is then the supplier's way of moving part of the financing to the bank. The paper uses this to explain why discounts go to small, risky buyers, as observed by Klapper et al. (2012). The comparative statics of §5 (Propositions 4–6) are built on the same reduced problem.
The result is proved on paper but has not been formalized. The appendix lemmas it rests on (C.4, C.7, C.8, C.9) are stated without proof ("available upon request"). A machine-checked development would therefore settle whether these lemmas hold on the domain where the paper uses them. It would also produce a reusable library: IFR demand with failure rates, the bank-loan pricing kernel , and the implicit order quantity .
The order quantity is defined implicitly, as the smaller root of a unimodal equation, and the paper's arguments differentiate through it with the implicit function theorem. Every derivative of therefore involves , which blows up at the edge of where . The density is only assumed continuous, so and need not be differentiable when . Monotonicity and concavity have to be argued from the integral forms, or under a smoothness assumption the paper does not state.
The obvious argument for "sufficiently large " also fails. It perturbs the optimum at just below , but there the domain shrinks to a sliver near , and the derivative of in at can be negative. For exponential demand it tends to as . The proof's claim that there is not part of the theorem. Part 1 for general is reduced to through Proposition 6, which requires comparing optima over domains that themselves depend on .
All objects live in TradeCredit.Terms.Model.
Demand. Demand is a density that is continuous on , positive on , zero on , integrable with total mass , and has a weakly increasing failure rate on . is the interval integral of from . The normalizations are and . The parameters satisfy , and .
Domain. is the printed set of Corollary 3 ( and ) plus two pinned constraints: (that is, ) and . These are the image under (11) of §3.1's , which the printed omits.
Statements. is the infimum of the nonnegative roots. "The optimal contract" means every maximizer of on . Existence of a maximizer is not asserted; the paper does not prove it. Monotonicity is weak, and concavity is Mathlib's ConcaveOn on the sections of . Proposition 6 is stated by comparing attained values with .
Not in scope. The retailer's best response (Proposition 1) and the bijection between thresholds and contracts are not formalized. The goal is about the paper's own reduced problem. Lemma 1's first-order conditions are not a milestone: as printed they fail at a corner optimum , and they need , which is not defined under a merely continuous density.
Ruling out trivialization. The large- clause quantifies over with . For the domain has no point with and every "for every optimal contract" statement holds vacuously, so a large- clause that reached only those values would be empty.
Welcome contributions. Lemmas on IFR densities (positivity of , finiteness of the mean, monotonicity of and existence of ), the root structure of , and boundedness of on are reusable beyond this paper.
Source. The source PDF is the authors' accepted manuscript (LBS Research Online, eprint 801). All page numbers are the manuscript's.
A firm launching a new experience good does not know how good the product is, and neither do its customers. Early buyers post reviews, and customers who wait learn from them: this is social learning (SL). Forward-looking customers anticipate this and may delay their purchase until reviews are available, which cuts into the firm's early sales. Papanastasiou and Savva (Management Science 2017) ask whether SL helps or hurts a monopolist facing such strategic consumers.
This mission formalizes their answer for responsive pricing, where the firm cannot commit to a second-period price and instead sets it after observing the reviews. Without learning, this is the classical price-skimming game of Besanko and Winston (1990), in which a firm without commitment power is hurt by consumer patience. With learning, two effects compete: reviews make the second-period market more informative (an informational effect the firm can exploit by repricing), and the option to learn makes waiting more attractive (a behavioral effect that hurts the firm).
A monopolist sells over two periods at unit cost to a unit mass of consumers with preference types uniform on . The mean quality is unknown, with prior , and reviews are noisy with variance ; the SL influence parameter is . Consumers discount second-period utility by ; the firm does not discount.
If a set of types buys in period 1, its mass is the mass of reviews, and the posterior mean , seen from period 1, has the pre-posterior law (Lemma 1 and Definition 1 of the paper). In period 2 the remaining types value the product at .
Under responsive pricing the firm sets ; consumers decide whether to buy now or wait; reviews realize ; the firm sets to maximize the second-period profit
An equilibrium after is a measurable buyer set and a measurable rule that is optimal at every , such that every type in weakly prefers to the discounted expected value of waiting, and every type outside weakly prefers waiting. The firm's expected profit is , and is its supremum over all and all equilibria. The benchmark "absence of SL" ( in the paper) is the same model at , where with certainty.
The thresholds are left unspecified; the statement asserts only that SL raises the optimal profit near both ends of the patience range.
The result shows that the benefit of reviews to a firm that reprices dynamically, previously established for non-strategic consumers, survives when consumers strategically wait for information. It is one half of the paper's comparison between commitment and responsiveness: under SL the firm's flexibility to react to reviews becomes valuable, which reverses the classical ranking of pre-announced over responsive pricing.
The paper proves the result on paper only. This mission produces a machine-checked model of a two-period game with a continuum of consumers, Bayesian learning and subgame-perfect pricing, and machine-checked versions of the equilibrium characterizations. The paper's numerical evidence that the result holds for all is not part of the goal.
The first-period threshold is defined implicitly: in (7) the law of has a variance that depends on the threshold itself, and the second-period price inside the integral is a piecewise function of both. Existence, uniqueness and the comparison with the benchmark all go through this fixed-point equation.
The endpoint relies on Proposition 5(i), that inducing adoption inertia is strictly suboptimal. At the alternative price used in the printed proof yields exactly the inertia profit, so this endpoint is not settled by the page's witness. Passing from the two endpoints to the thresholds requires continuity of an optimal value taken over an unbounded price set and over implicitly defined equilibria; the paper cites the Maximum Theorem, whose hypotheses must be established.
Everything lives in namespace SLPricing.Resp. The model file is shared, verbatim, with the two other missions of this series. Conventions:
EReal over all real prices and all their equilibria, so neither an empty nor an unbounded family produces a junk value. Defining as the profit at a closed-form price, or the benchmark by dropping the second period, would make the goal circular; the formalization does neither.Hypotheses added or restricted relative to the page, each disclosed in its item:
Contributions welcome: Gaussian integral estimates for (7), the second-period optimization of Lemma 3, a witness against inertia at , and a continuity argument for optimal values over parametrized equilibria, which is reusable for the series' other missions.
DC programming is the minimization of a function that is a difference of two convex functions. The class contains every function on a compact convex set and most nonconvex models of sparse learning, clustering, combinatorial relaxations and robust optimization, and its standard method, the DC Algorithm (DCA), replaces by its affine minorant at the current iterate and solves a convex program at each step. DCA was introduced by Pham Dinh Tao in 1985 and developed jointly with Le Thi Hoai An from 1994 on (Pham Dinh & Le Thi 1998); the survey of Le Thi & Pham Dinh 2018 collects thirty years of that work.
DCA is guaranteed to reach critical or strongly critical points, notions that depend on the chosen decomposition , while a decomposition-free notion, directional (d-)stationarity of itself, is what a user of a nonconvex model usually wants. Ahn, Pang & Xin 2017 warned that DC criticality can be much weaker than d-stationarity. Theorem 1 of the 2018 survey (p. 9) states when the two coincide. Its proof is omitted in the paper ("can be easily deduced … It is omitted here").
Let with the canonical inner product . Functions take values in . The effective domain of is , and is the set of proper, lower semicontinuous, convex functions .
The standard DC program is
with the convention , and is assumed finite. Finiteness of forces , so .
The subdifferential of at is
A point is strongly critical for if .
The directional derivative of at in direction is . For convex it equals . A point is d-stationary for if for every . The support function of is , with . Finally, is the relative interior of , its interior inside the affine hull .
For ,
Part (iii) is the goal because it is the equivalence the paper uses to justify DCA, stated under a hypothesis symmetric in and ; (vi) is the more general companion.
The theorem connects the output of DCA with a stationarity notion intrinsic to . Without it, the strong criticality certified by DCA would be a property of a decomposition rather than of the problem, and different decompositions of the same could certify different points. With it, at points in the relative interiors of the domains, every strongly critical point is d-stationary, and conversely no d-stationary point is missed by the criticality test.
Parts (i) and (ii) are stated in the paper without proof, and so is the rest of Theorem 1; none of it has a machine-checked proof. The mission produces a formal statement of all six parts with the extended-real conventions made explicit. Three of the printed parts are false as stated without the nonemptiness of ; the formal versions add that hypothesis and record a counterexample for each, so the formalization also corrects the printed statement.
The obvious argument writes and reads off both directions from . Two steps of it fail. First, the difference can be or , and the limit defining need not be the difference of the limits; the nonemptiness of is exactly what rules out the first case. Second, passing from "" to "" needs to equal the support function of , which holds in the relative interior of but fails on its relative boundary, where need not be lower semicontinuous. The relative interior, not the interior, is essential: the domains may be lower-dimensional.
is EuclideanSpace ℝ (Fin n), and every function maps into EReal. The published definitions TaoAnDCA.GlobalOpt.Setting supply (effDom), the DC objective with (dcSub), the subdifferential (subdiff) and (primalValue); is the published IsProperClosedConvex. Every statement carries the standing assumptions of Theorem 1 as binders: , and . The mission's definitions are:
convDirDeriv: the convex directional derivative by the paper's infimum formula, in EReal;HasDirDerivE: the predicate that the one-sided limit along exists in EReal and equals a given value;IsDStationary: and, for every direction, the limit exists and is ;IsStronglyCritical: both and ;supportFn: the extended-real support function, on .The relative interior is Mathlib's intrinsicInterior ℝ, the affine hull is affineSpan ℝ. The subgradient inequality has the standard sign; display (1) of the paper prints the opposite sign, a slip. The only hypothesis added to the page is , in parts (i), (ii) first sentence and (iv), each of which is false without it; parts (ii) second sentence, (iii), (v) and (vi) are stated as printed.
The statement admits trivializing formalizations, which this one rules out. Strong criticality without the nonemptiness of is vacuous wherever . A d-stationarity defined through limUnder, a real-valued derivative, or "every limit is nonnegative" holds vacuously where the limit does not exist. And written in raw EReal would give .
A complete development needs the monotonicity of convex difference quotients in EReal, limit arithmetic for extended reals, and the formula for at points of (Rockafellar 1970, Theorem 23.4), together with the nonemptiness of there. These results on extended-real convex functions are reusable well beyond DC programming, and contributions of them as separate theorems are welcome.
How far is a graph from being regular? Several numerical irregularity measures answer this question, and spectral graph theory supplies a natural one. For a graph with vertices and edges, the largest eigenvalue of the adjacency matrix is always at least the average degree , with equality exactly when is regular. The difference is therefore a measure of irregularity; it was studied by Bell (1992) alongside the variance of the degrees, and it is one of several such measures, with Albertson's and Nikiforov's degree deviation among the others. The measures are incomparable in general, and one way to understand what each gauges is to determine its extremal graphs.
A basic extremal question asks which graphs are the most irregular. Among all graphs the question is uninteresting, because isolated vertices lower without lowering . Among connected graphs it is a genuine optimization problem. Using the variable neighbourhood search system AutoGraphiX, Aouchiche, Bell, Cvetković, Hansen, Rowlinson, Simić and Stevanović (2008) found that the maximizers of over connected graphs on vertices are always pineapple graphs, a clique with pendant vertices hanging from one clique vertex, and they conjectured that this holds for every (Aouchiche et al., European J. Oper. Res. 2008).
Timeline:
This mission formalizes Section 4 of Tait and Tobin.
All graphs are finite and simple; an -vertex graph has vertex set . The spectral radius is the largest eigenvalue of the adjacency matrix of , the published platform definition specRad. The average degree is , a real number.
A connected graph on vertices is a maximizer of (Lean: IsIrregMax G) if
The pineapple (Lean: pineapple p q) has vertices: the first form a complete graph , and each of the other vertices is a pendant vertex, adjacent only to the clique vertex . Stars () and complete graphs () are degenerate pineapples.
The lemmas of the mission speak about the leading eigenvector of a maximizer : a vector with , all entries positive, normalized so that its largest entry is . Such a vector exists by the Perron–Frobenius theorem because is connected. denotes a vertex with , the degree of , and the neighbourhood of . Some statements carry a small parameter , fixed before .
The clique size is left free. The optimal value is determined by Aouchiche et al. by optimizing a cubic polynomial over pineapples; Tait and Tobin cite it and do not prove it, so it is not part of the goal.
The result. Theorem 21 identifies the most spectrally irregular connected graphs for large , confirming a conjecture that came from computer search and that had resisted the usual graph-transformation arguments. Combined with the cited optimization over pineapples, it gives the exact maximum of over connected -vertex graphs for large , which in turn bounds by plus an explicit term for every connected graph. The intermediate statements, notably Lemma 19 which converts products of Perron entries into adjacency, are reusable in other spectral extremal problems over connected graphs.
Formalizing it. The theorem is proved on paper for large ; no machine-checked proof of it, or of Hong's inequality, is known. The formalization must make every "for sufficiently large" and every explicit, and it repairs two statements that are false as printed (see Formalization scope). A small- verification, or a proof for all , would be further contributions.
The obvious approach is local improvement: given a non-pineapple, move an edge and show that increases. Each move changes both terms, by amounts of order and respectively, and these are comparable; neither the sign of the change nor connectivity of the modified graph is under control without first knowing the global structure. The proof therefore needs the whole chain of asymptotic estimates: the size of and , a second vertex of nearly maximal entry, the norm of the Perron vector, and only then the adjacency rules of Lemma 19. Every edge deletion must also keep the graph connected, since the maximum ranges over connected graphs.
Fin n; graphs are SimpleGraph (Fin n) with classical decidability. is the published WangKangXue.SpectralTuran.specRad, the largest eigenvalue of G.adjMatrix ℝ. is avgDeg G = 2 · #edges / n in .IsIrregMax); dropping connectivity changes the problem.v with (G.adjMatrix ℝ).mulVec v = specRad G • v, all entries positive, all entries at most , and a vertex x with v x = 1. It is never quantified existentially.∃ N, ∀ n ≥ N. Constants from and "a constant not depending on " are existentially quantified before , and . In Lemma 18, inequality (11) and Lemma 19 the proof works for every , which is universally quantified; Proposition 20 needs small and is stated for .G ≃g pineapple p q with . The pineapple is defined by its edges, clique plus pendants at one vertex; it is not defined by any property that the proof establishes, and the clique size is not pinned.The stochastic linear quadratic (LQ) optimal control problem asks to steer a linear stochastic differential equation by a control so as to minimize a quadratic cost. It is the basic model of stochastic control: Wonham studied it in 1968 (Wonham 1968), and it is the model on which feedback design, mean-field control and LQ differential games are built (Yong–Zhou 1999).
Classically the cost weights are assumed nonnegative and the control weight uniformly positive definite, the standard conditions (1.4). Under them the Riccati equation has a unique solution and the optimal control is a linear state feedback. A stochastic problem can however be well posed when is indefinite, because the diffusion term also penalizes the control.
Timeline:
A probability space carries a standard one-dimensional Brownian motion . Its natural filtration, augmented by the -null sets, is . Fix a horizon and deterministic coefficients , , weights , , (functions of time) and . The admissible controls are the -progressively measurable processes with . The state from the initial pair solves
and the cost is
Standing assumptions (H1)–(H2): , , , , , on , and square-integrability of the random terms . No sign condition is imposed on , or . The homogeneous problem (SLQ) sets ; its cost is .
The map is uniformly convex if, for some ,
With and , the Riccati equation is
with the Moore–Penrose pseudoinverse. A solution is strongly regular if a.e. for some (4.10).
The goal fixes no constant: the on each side is existential.
Companion items: Remark 4.6 (the same bounds ), the well-posedness of the state equation and the cost (Sun–Yong 2014, Proposition 2.1), and Proposition 3.5 (the standard conditions (1.4) imply uniform convexity).
Theorem 4.5 gives a checkable sufficient condition for the classical structure of LQ control: under (4.2) the Riccati equation has a solution whose gain matrix is uniformly positive definite, so the optimal control is a state feedback with an invertible gain. It covers indefinite weights, and Proposition 3.5 shows that it contains the classical case (1.4). Combined with Sun–Yong's equivalence it yields Corollary 4.7, the feedback representation of the open-loop optimal control, which later missions of this series use.
The results are proved in the paper. As far as is known they have no machine-checked proof. Formalizing them requires stochastic calculus for controlled SDEs (Itô's formula for quadratic forms of a state process) linked to matrix ODE theory. The definitions this mission fixes (the LQ problem, the Riccati and Lyapunov equations with a pseudoinverse) can be reused by the other missions of the series and by any stochastic LQ formalization.
The direction (ii) ⇒ (i) is a completion of squares followed by Lemma 2.3. Lemma 2.3 is not obvious: it asserts a bounded inverse for an operator defined through an SDE.
The direction (i) ⇒ (ii) is the hard one. The obvious approach would solve (4.6) directly, but (4.6) is nonlinear and its coefficient may be singular. No sign condition gives a priori bounds. The paper instead builds a policy-iteration sequence of linear Lyapunov equations. The difficulty is to show that every iterate keeps , so that the next gain is defined, and stays bounded below. These bounds come from the cost functional (Proposition 4.4), not from the matrix equation. Uniform convergence of the iterates then needs integrable estimates under the weak integrability of (H1).
IsStdBrownian (Mathlib's IsBrownianReal per coordinate, published module Peng1990.SMP.Stochastic). is augmentedFiltration (published ReflectedBSDE.Existence.Setting).state_wellposed poses existence, uniqueness and integrability of the cost. Expectations are Bochner integrals, and is the Euclidean .EReal infimum over admissible controls.HarmonicGames.Decomposition.pinv. Where the paper prints ((4.19), p. 2290) Lean's matrix inverse is used; it is invertible there by .Ruling out trivial forms. Uniform convexity is not defined through the operator of (3.8), and strong regularity includes the integral Riccati equation. A formalization that drops the Riccati equation, or reads uniform convexity off a matrix condition, is a different theorem. No positivity of , or is assumed anywhere except in Proposition 3.5, whose hypothesis (1.4) is exactly that.
Contributions welcome: Itô's formula for with a (or absolutely continuous) matrix ; existence and uniqueness for linear SDEs with coefficients; existence and uniqueness for linear matrix ODEs; the Penrose identities for pinv.
Linear–quadratic (LQ) optimal control is the basic test case of stochastic control: a linear stochastic differential equation, a quadratic cost, and an optimal control that one expects to be a linear feedback of the state computed from a Riccati equation. In the indefinite stochastic case the weighting matrices , , carry no sign condition. The cost can then be convex without being uniformly convex, an optimal control may fail to exist although the value is finite, and the Riccati equation may have no solution of the kind the classical theory needs.
Sun, Li and Yong (SIAM J. Control Optim. 54 (2016) 2274–2308) separate finiteness, convexity, open-loop solvability and closed-loop solvability for this problem. This mission covers their Section 6. Under uniform convexity the optimal control is the Riccati feedback of Corollary 4.7. Section 6 removes uniform convexity: it regularizes the control weight to , takes the Riccati feedback control of each regularized problem, and shows that open-loop solvability of the original problem is exactly the convergence of along some sequence .
Timeline. Chen, Li and Zhou (SIAM J. Control Optim. 36 (1998)) introduced indefinite stochastic LQ problems. Ait Rami, Moore and Zhou (SIAM J. Control Optim. 40 (2002)) introduced the generalized Riccati equation with a pseudoinverse. Sun and Yong (SIAM J. Control Optim. 52 (2014)) characterized closed-loop solvability by regular solutions of that equation. In 2016 Sun, Li and Yong characterized uniform convexity by strongly regular solutions and open-loop solvability by the regularized feedback sequence treated here.
Fix a horizon and a probability space carrying a one-dimensional standard Brownian motion , with the augmented natural filtration of . For an initial pair and an admissible control , an -progressively measurable -valued process with , the state solves
The cost is
The coefficients and are deterministic, are random, and the integrability conditions are (H1)–(H2). The value function is . A control is open-loop optimal at if for every . Problem (SLQ) is the case , with cost .
For let be the strongly regular solution of the Riccati equation (5.7),
where for some and . Let be the adapted solution of the linear backward equation (4.11) for these data, and put
With the solution of the closed-loop system , , the regularized feedback sequence is
is a Hilbert space with inner product ; weak and strong convergence of controls refer to it.
Assume (H1)–(H2) and that is convex. For the following are equivalent:
and every weak or strong limit of such a subsequence is an open-loop optimal control at . The goal assumes convexity, not uniform convexity, and no finiteness.
Two further statements follow the goal: open-loop solvability is equivalent to (p. 2303), and Proposition 6.4: if , the Riccati equation (4.6) has a regular solution and Problem (SLQ) is closed-loop solvable.
Theorem 6.1 gives a minimizing sequence computed from Riccati and backward equations whenever the problem is finite. Theorem 6.2 turns it into a test for open-loop solvability that needs no uniform convexity and no regular solution of the original Riccati equation. When an optimal control exists, it is recovered as the limit of feedback controls. Proposition 6.4 converts a bound on the gains into closed-loop solvability of the homogeneous problem. Section 7 of the paper shows that open-loop solvability does not imply closed-loop solvability, so a criterion phrased directly in open-loop terms is needed.
All of these results are proved in the paper. None of them, nor the solution theory of stochastic LQ problems they rest on, had a machine-checked proof on Prove2Me or in Mathlib as of October 2026. A formal development needs the well-posedness of linear SDEs and BSDEs with integrable coefficients, the Riccati theory of Section 4, and the Hilbert-space structure of the space of admissible controls. Those parts are reusable for any stochastic LQ problem.
The obvious approach takes any minimizing sequence and extracts a weakly convergent subsequence. That fails without uniform convexity: a minimizing sequence need not be bounded, and boundedness is exactly what open-loop solvability provides in (6.7). The converse direction needs the limit of the regularized costs to identify the value, which requires both the minimizing property of (Theorem 6.1) and weak lower semicontinuity of . That in turn rests on convexity being transported from to through Corollary 3.4 and the zero extension. Upgrading weak to strong convergence uses the norm bound (6.7) with the limit itself as the optimal control. Every step depends on Corollary 4.7, the Riccati representation of the optimal control of the regularized problem, whose proof requires the theory of Section 4.
The probability basis is a probability space with a one-dimensional standard Brownian motion and its augmented natural filtration. Vectors are Fin k → ℝ and matrices Matrix (Fin k) (Fin l) ℝ. Time is ℝ≥0, and is the Euclidean dot product u ⬝ᵥ u. (H1)–(H2) are standing assumptions, with entrywise conditions on the matrix coefficients. The state from is a strong solution of the published SDE notion Peng1990.SMP.SolvesSDE whose coefficients are switched on at ; it has a.s. continuous paths and . The cost is evaluated along a chosen solution, which is unique. is an infimum in the extended reals. Limits in are taken as . "A subsequence" is a sequence with , and the limit control is required to be admissible. The backward equations use the published Peng1990.SMP.SolvesBSDE, and the pseudoinverse in (4.6) and (4.11) is the published HarmonicGames.Decomposition.pinv.
Theorem 6.1 prints the term in its backward equation. The equation (4.11) that its proof uses through Corollary 4.7 has , and the formalization uses (4.11). Corollary 3.4 is stated without its item (vi), which involves an operator that the paper quotes from another source.
The families , and are hypotheses pinned by their equations for every . The sequence is therefore the Riccati feedback sequence (6.2), never an arbitrary minimizing sequence or an arbitrary family of -optimal controls; with such a family the implication (ii) ⇒ (i) would be a different theorem.
Contributions are welcome at every level: the solution theory of linear SDEs and BSDEs, Itô's formula for quadratic forms, Riccati and Lyapunov equations in integral form, weak compactness in , and the milestones themselves.
Linear–quadratic (LQ) optimal control is the basic test case of stochastic control: a linear stochastic differential equation, a quadratic cost, and a value function that one expects to be a quadratic form in the initial state. In the indefinite stochastic case the weighting matrices , , carry no sign condition, and the classical picture breaks down. Without a sign condition the infimum of the cost can be . Before one can ask whether an optimal control exists, one has to ask whether the problem is finite, i.e. whether its value function stays above .
Sun, Li and Yong (SIAM J. Control Optim. 54 (2016) 2274–2308) separate the notions of finiteness, convexity, open-loop and closed-loop solvability for this problem. This mission covers their Section 5. Section 5 characterizes finiteness of the homogeneous problem by a family of regularized Riccati equations, and Example 5.2 shows that convexity of the cost alone is not enough.
Timeline. Chen, Li and Zhou (SIAM J. Control Optim. 36 (1998)) introduced indefinite stochastic LQ problems. Ait Rami, Moore and Zhou (SIAM J. Control Optim. 40 (2002)) introduced the generalized Riccati equation with a pseudoinverse. Sun and Yong (SIAM J. Control Optim. 52 (2014)) characterized closed-loop solvability by regular solutions of that equation. In 2016 Sun, Li and Yong characterized uniform convexity by strongly regular solutions, and finiteness by the limit of the regularized solutions treated here.
Fix a horizon and a probability space carrying a one-dimensional standard Brownian motion , with the augmented natural filtration of . For an initial pair and an admissible control , an -progressively measurable -valued process with , the state solves
The cost is
The coefficients and are deterministic, and are random; the integrability conditions are (H1)–(H2). The value function is . Problem (SLQ) is the case ; its cost and value are and . The problem is finite at if for all , and finite if this holds for every .
Write and . The regularized Riccati equation (5.7) is
A solution is strongly regular if a.e. for some . Further, solves the Lyapunov equation (3.2), , , and solves , . The comparison function is
Assume (H1)–(H2) and (5.6): for all . For every , let be the strongly regular solution of (5.7). Then
In this case exists for every , and
In particular, finiteness at implies finiteness.
Theorem 5.6 states the converse of Remark 4.8. Theorem 5.7 gives six equivalent conditions when and . Example 5.2 is a problem whose cost is convex but which is not finite. Corollary 5.4 gives a Lyapunov-type sufficient condition for finiteness.
The result. Theorem 5.3 turns finiteness, a statement about an infimum over an infinite-dimensional space of controls, into a lower bound on a one-parameter family of matrices. Each matrix in the family solves a well-posed Riccati equation. The theorem also says that the value function of a finite homogeneous problem is a quadratic form whose matrix is the monotone limit of . It shows that this limit satisfies the regularity condition (5.10) and sits between two explicit bounds. Section 6 of the paper builds on the same regularization to construct minimizing sequences. Theorem 5.7 shows that in the case , , finiteness already forces unique closed-loop solvability.
Formalizing it. The result has been proved on paper since 2016; nothing in this mission is open mathematics. As far as is known, no part of indefinite stochastic LQ theory has been machine-checked, and Lean/Mathlib has no stochastic LQ problem, no matrix Riccati equation and no fundamental-matrix theory for time-varying linear ODEs. The mission produces faithful statements of the theorem, its proof steps and its companions on top of a reusable problem layer, as targets for complete formal proofs.
The naive argument fails at the interchange of the limit with the infimum over controls. Monotonicity in gives a limit directly. The reverse inequality needs near-optimal controls whose norm may blow up, so it has to be organized carefully. The sufficiency direction needs more than the bound at . Finiteness at later times is recovered through the comparison function , which combines the fundamental matrix with the Lyapunov solution . Example 5.2 rules out the tempting shortcut: under (5.6) the cost is convex, yet for all . Every step also rests on stochastic calculus (Itô's formula for , well-posedness of the state equation) and on the representation of the value through the Riccati equation (Theorems 4.3 and 4.5, cited here).
The problem layer is shared by the four missions of this series: SLQSolv.Finite.Setting and SLQSolv.Finite.Riccati. It builds on the published Itô-calculus and SDE layer Peng1990.SMP.Stochastic, the augmented Brownian filtration of ReflectedBSDE.Existence.Setting, and the Moore–Penrose pseudoinverse HarmonicGames.Decomposition.pinv. The layer commits to these conventions:
ℝ≥0, vectors are Fin k → ℝ, and is the dot product ;EReal, so is ⊥ and finiteness is ⊥ < V;PosSemidef of the difference), and conditions on matrix coefficients are entrywise;A formalization in which "bounded from below" allows to depend on , or in which finiteness is checked on at a fixed control rather than on , would trivialize the theorem and is excluded.
A complete development needs several pieces, all reusable beyond this mission:
Contributions to any of them are welcome.
Online reviews let consumers learn about a new product from the experience of earlier buyers. For a firm selling to strategic consumers, who time their purchases, this social learning (SL) cuts two ways. Reviews reveal quality, which can raise second-period demand; but a consumer who expects reviews also has a new reason to wait, and every consumer who waits writes no review. Papanastasiou and Savva (Management Science 63(4), 2017) build a two-period model in which both forces are endogenous and ask whether a monopolist that commits to its prices in advance is better or worse off when consumers learn from one another.
The benchmark without learning is the classical intertemporal pricing problem with strategic consumers (Landsberger and Meilijson, 1985), whose optimal pre-announced plan is a decreasing price path. This mission formalizes the paper's answer for pre-announced pricing: its Proposition 3.
A unit mass of consumers has preference types uniform on . A product of unknown mean quality is sold over two periods. Buying in period gives type the utility , where is the consumers' discount factor and the perceived quality. The firm has unit cost and does not discount.
Everyone shares the prior . Individual quality perceptions are , and is the SL influence parameter. If a mass buys in period 1 and posts reviews, the posterior mean is , where is the average rating. Seen from period 1, is random, with the pre-posterior law
Under pre-announced pricing the firm commits to a plan . Consumers then play a purchasing game. A set of early buyers is an equilibrium if every type in weakly prefers buying now, and , and every other type weakly prefers to wait. Here has the pre-posterior law for . In period 2 the remaining types buy iff . The firm's expected profit is
and the optimal pre-announced profit is its supremum over all plans and all their equilibria. Absence of SL is the same model at , where .
For there are thresholds and such that
Proposition 3 says that social learning helps the firm at both ends of the patience range. For myopic consumers this is the informational effect alone. For patient consumers it holds even though learning makes them strictly more inclined to wait (Lemma 2) and the committed price cannot react to the reviews. The paper's numerical experiments found no intermediate at which learning hurts, but the theorem asserts only the two ends. The result underlies the managerial conclusions of the paper: firms gain from encouraging reviews even when consumers are strategic.
The result is proved in the paper; nothing in the model has been machine-checked before. A formal proof would check the equilibrium analysis of a continuum purchasing game with an endogenous information externality. Its intermediate results also serve the paper's two other missions: responsive pricing, and the comparison of responsive with pre-announced pricing. These are the Normal convex-order monotonicity (Lemma 5), the implicit threshold equation (Lemma 2), the no-SL benchmark (Proposition 1) and a Maximum-Theorem continuity statement.
The equilibrium threshold solves an equation whose Normal kernel has a variance that depends on itself. Existence, uniqueness and monotonicity are not closed-form computations.
The endpoint is the delicate one. There learning makes waiting most attractive, and the strict gain over the no-SL optimum must come from a plan that still induces a positive mass of early buyers.
Continuity of in is a Maximum-Theorem argument for a supremum over an unbounded set of prices whose objective passes through an implicit equilibrium. Compactness of the relevant price set has to be established, not assumed.
Every statement is taken over the standing assumptions , , , , with firm discount factor and pure strategies. Further conventions:
The witness used in the printed proof of Proposition 2(i) does not settle the case .
A complete development needs Gaussian expectations of hinge functions and their monotonicity in the variance (strict convex order), an implicit-equation argument for the threshold, and a version of Berge's Maximum Theorem. The Gaussian lemmas and the no-SL benchmark are reusable across the series. Contributions to any milestone are welcome.
A forward–backward stochastic differential equation (FBSDE) couples a forward diffusion with a backward equation for a pair whose terminal value depends on . Such systems arise from the stochastic maximum principle, from option pricing with large investors, and from stochastic differential games. Whether an FBSDE with Lipschitz coefficients has a unique solution on an arbitrary horizon is a classical question: small-time solvability is easy, but global solvability can fail even for linear equations.
J. Ma, Z. Wu, D. Zhang and J. Zhang, On well-posedness of forward–backward SDEs—a unified approach (arXiv:1110.4658v2, Ann. Appl. Probab. 25 (2015)), reduce well-posedness to the existence of bounded solutions of two deterministic dominating ordinary differential equations, obtained from the difference quotients of the coefficients. For linear FBSDEs with constant coefficients the two dominating ODEs coincide, and the authors give sharp criteria for global solvability. This mission formalizes the criterion in the case , where the dominating ODE has a rational right-hand side with a pole.
Earlier global results for coupled FBSDEs rested on the four-step scheme (Ma–Protter–Yong 1994) or on monotonicity conditions (Hu–Peng 1995); §7.4 of the paper compares the dominating-ODE approach with these methods.
The linear FBSDE (4.1) with constant coefficients is determined by nine reals and a terminal slope . Its dominating function is (3.9),
defined for . When it can be rewritten as (5.8),
for constants . The dominating ODE (5.3) is the backward integral equation
The paper needs a solution satisfying (5.9): both and are bounded on . Since , this forces (Remark 5.5).
The comparison tool is Lemma 5.1. For measurable it gives a unique solution of lying between a sub-solution and a super-solution of perturbed equations (5.2).
For and , the ODE (5.3) has a solution satisfying (5.9) for every if and only if one of the following holds:
The limit alternatives in cases 3 and 4 are not printed in the paper. Without them the equivalence is false. Take , , , all other coefficients , and . Then , and satisfies (5.9) on every horizon, yet none of the printed cases holds. The gap is in the Appendix (p. 48): it asserts that is positive on the closed interval when , which fails when the polynomial part vanishes at the pole. A companion item records the counterexample.
The milestones follow the paper's proof:
In the paper, Theorem 5.6 is the sharp solvability criterion for linear FBSDEs with constant coefficients and . The paper describes these sharp conditions as setting the "limits" for the solvability of general FBSDEs, and the nonlinear Theorems 5.9–5.11 and the main well-posedness Theorem 7.4 are modelled on them. Because the criterion is an equivalence, it also says when no regular decoupling field can be built from the dominating ODE, whatever the horizon.
The result is proved in the paper, but the printed statement is not correct as an equivalence (see above). The mission states and asks for a corrected version, a machine-checked counterexample to the printed one, and formal versions of each step of the proof. The deterministic parts (comparison for backward integral equations, finite-time blow-up of scalar autonomous ODEs, pole-reaching for rational vector fields) are basic real analysis with no current Lean library. They are reusable well beyond FBSDEs. No part of this paper has a machine-checked proof.
Each sufficiency case is an a priori bound: a comparison with a constant or explicitly solvable equation keeps the solution in a fixed interval away from the pole. The difficulty is on the necessity side, where three kinds of failure must be excluded:
The obvious argument for the last case, " is bounded below by a positive constant up to the pole", is exactly what fails when tends to at the pole. There the solution approaches the pole only asymptotically, and the right criterion is the corrected one above. A second subtlety is that is only locally Lipschitz off the pole, so comparison must be carried out on a band in which the solution provably stays.
Time is real, with and . The coefficients form a record Coeffs of nine reals, and Coeffs.F is (3.9) verbatim. A solution on is a function such that, for every , the integrand is integrable on and ; values outside are irrelevant. Condition (5.9) is a uniform bound on together with for some . "For arbitrary " is a universal quantifier over outside the existential.
Lean's conventions are total, so several trivializing formalizations are ruled out explicitly:
Coeffs.F a junk value at the pole. No statement evaluates there: every zero point, bound and limit in the statements lives strictly on one side of .The constants of (5.8) enter the necessity milestones only through the decomposition hypothesis, never through a formula.
The development needs a Picard–Lindelöf or comparison argument for backward scalar integral equations with locally Lipschitz right-hand sides, monotonicity of autonomous scalar solutions, and the intermediate value theorem. Contributions of a general comparison lemma for scalar integral equations would serve this mission and both other missions of the series.
Liouville quantum gravity describes random surfaces whose area measure is formally , where is a Gaussian free field (GFF). Schramm–Loewner evolution (SLE) describes random fractal curves that arise as scaling limits of interfaces in critical lattice models. Sheffield's paper Conformal weldings of random surfaces: SLE and the quantum gravity zipper (arXiv:1012.4797, Ann. Probab. 44 (2016), DOI 10.1214/15-AOP1055) shows that the two theories fit together: SLE curves are the interfaces obtained by conformally welding independent quantum surfaces along their boundaries.
The starting point of that program is a coupling between the reverse Loewner flow and the free boundary GFF (Theorem 1.2 of the paper): zipping up the upper half-plane by a reverse SLE map, and changing coordinates by the rule of Liouville quantum gravity, does not change the law of the field. This mission formalizes that theorem and the calculations of §4.1 that prove it.
Timeline. Couplings of forward SLE with the GFF go back to Schramm–Sheffield for (arXiv:1008.2447) and to Dubédat for general (arXiv:0712.3018). The reverse coupling with the free boundary GFF and the factor is Sheffield's (2010 preprint, published 2016); it underlies the later mating-of-trees theory of Duplantier–Miller–Sheffield (arXiv:1409.7055).
Let . A test function is a smooth, compactly supported real function with support in ; it has mean zero if . For a function write .
The free boundary Green's function is , and the energy of two test functions is
A free boundary GFF is a random modulo-additive-constant distribution: for every family of mean-zero test functions , the vector is a centred Gaussian vector with covariance . Pairings with test functions of nonzero mean are not defined.
Fix and a standard Brownian motion , and put . The reverse Loewner flow is , where for each
the pathwise form of . Write and
The fraktur are deterministic functionals of the flow. Finally , , and .
For every , with independent of ,
that is, the pairing vectors with every finite family of mean-zero test functions have the same law. Here .
The result. Theorem 1.2 says that the free boundary quantum surface is invariant in law under zipping up by an independent reverse SLE for a fixed time. It is the stationarity statement behind the quantum gravity zipper: Theorems 1.3–1.4 and 1.8 of the paper (the welding of boundary arcs of equal quantum length, treated in the companion mission) start from it, and the subsequent theory of quantum wedges, quantum cones and mating of trees uses it as a basic tool. It also gives an alternate way to sample the field: first sample (hence the curve), then sample an independent GFF, and form .
Formalizing it. The theorem is proved in the literature, and the paper itself regards several steps as standard (Proposition 3.1 is cited to [She07]). No part of it has a machine-checked proof. A complete development would give Lean its first Gaussian free field, its first reverse Loewner flow, and martingale statements for SLE functionals; the deterministic Loewner calculus of milestones 1–4 is useful independently of the probabilistic part.
The time derivatives in milestones 1–3 are routine once the flow is known to be holomorphic in , and milestone 4 follows from them. The obstacle is upgrading local martingales to martingales and exchanging the stochastic dynamics with integration in . Itô's formula gives that is a continuous local martingale; that it is a true martingale needs the bound of milestone 4, which shows that it is a Brownian motion run for a time at most a constant times . Passing from points to and to (4.2) needs integrability of uniformly on the support of and a Fubini argument. Mathlib has neither Itô calculus nor quadratic variation, so these steps need either a stochastic-calculus library or a direct argument. The final step (milestones 9–10) needs the Cramér–Wold device for an infinite-dimensional Gaussian field and the change of variables .
𝓓(ℍ, ℝ); integrals are Bochner integrals for Lebesgue measure on and .multivariateGaussian 0 (E(ρ_i,ρ_j)) laws for every mean-zero family. Every statement pairs only with mean-zero test functions.IsBrownianReal, taken with every path continuous and every coordinate measurable; martingales are with respect to its natural filtration and hold for all .Incidence bounds count how often points can lie on lines, planes or other simple objects. Over the reals the model result is the Szemerédi–Trotter theorem for points and lines in the plane (Szemerédi–Trotter 1983). Its proofs use the order or topology of (cuttings, crossing numbers, polynomial partitioning), so they say nothing over finite fields or fields of positive characteristic. These are the settings that matter for the sum–product problem in and for the finite-field versions of Erdős-type distance problems, where the absence of an incidence theorem was long the bottleneck.
M. Rudnev, On the number of incidences between points and planes in three dimensions (Combinatorica 38 (2018), doi:10.1007/s00493-016-3329-6), proves a point–plane incidence bound in valid over every field of characteristic , with a constraint only in terms of the characteristic. It became the standard tool for sum–product estimates in positive characteristic: for example, Roche-Newton, Rudnev and Shkredov and Stevens and de Zeeuw build their bounds on it.
Timeline:
Let be a field and the projective three-space over . A point and a plane are both nonzero vectors of up to scaling. The point lies on the plane, , when . A line of is a 2-dimensional subspace of . For finite sets of points and of planes, the incidence count is
The collinearity parameter is the largest number of planes of that contain a common line.
The proof works in the space of lines of . The line through and has Plücker vector , . These vectors fill the Klein quadric . A point defines its α-plane (the lines through ) and a plane its β-plane (the lines in ), both projective planes inside . Cutting with a hyperplane that is not tangent to it gives a three-quadric , and every α- and β-plane meets in a line.
There are absolute constants such that for every field of characteristic , every set of points and every set of planes in , with when has positive characteristic ,
In characteristic there is no constraint on .
The proof decomposes as: point–plane incidences in equal line–line incidences between two families of mutually skew lines in (Lemma 9), and those are bounded by
where now counts lines of in a three-dimensional section of . The supporting milestones are: the incidence criterion (9) for Plücker vectors, the intersection pattern of α- and β-planes, Lemma 6 on sections of , the generic projection from to , the existence of a low-degree vanishing polynomial, the bound of zeros on a line, and Salmon's theorem (Theorem 2) on surfaces with many lines.
Theorem 3 gives the incidence bound with no assumption on the field beyond characteristic. The paper shows that its main term is sharp in positive characteristic under the constraint alone (Remark 4), and that the bound is tight for , (§6.2). It yields the paper's applications (distinct bilinear products of a planar point set over , and a pinned Erdős distance bound in positive characteristic), and it is the incidence input to sum–product estimates over such as .
The theorem is proved and published; it is not open. As far as is known, neither it nor its ingredients (the Klein correspondence in Plücker coordinates, the Guth–Katz polynomial argument over an arbitrary field, Salmon's theorem) has a machine-checked proof. This mission's statements give a formal target for the whole chain. Several milestones (the Plücker incidence criterion, the vanishing polynomial, zeros on a line, the generic projection) are standard facts of projective geometry over arbitrary fields that are useful well beyond this paper.
The obvious route, cell decomposition by polynomial partitioning as over , fails over a general field: there is no ordering, so no cells. The Guth–Katz algebraic argument survives, but in it needs the hypothesis that few lines are concurrent, which point–plane arrangements violate. Rudnev's way out is to move the problem into the three-quadric . There the two line families are skew within themselves, and the collinearity parameter becomes a count of lines in a three-dimensional section of .
The hard step is Theorem 12. It needs the polynomial method over an arbitrary field together with Salmon's theorem on flecnodal surfaces. That theorem holds in characteristic only for degree , which is the source of the constraint . It also needs a structure theory of ruled surfaces to rule out many incidences inside non-quadric ruled components. Salmon's theorem alone has no formal proof anywhere.
Points and planes of are elements of Mathlib's ℙ F (Fin 4 → F). Finite sets of them are Finsets of projective classes, so they contain distinct points and planes. Incidence is Projectivization.orthogonal. Lines of , and are 2-dimensional subspaces. Two lines meet when their intersection is a nonzero subspace, and they are skew when it is zero. Plücker vectors are indexed in the order . A hyperplane of is given by its covector , and "not tangent to " is . A three-subspace of is a 4-dimensional subspace of .
Committed conventions:
Type. Bounds are stated in , and Salmon's threshold is computed in .Trivializing formalizations are excluded:
Finsets that would count one point twice are not used;A complete development needs Plücker coordinates and the Klein correspondence over arbitrary fields, homogeneous polynomials on and their zero sets, irreducible factorization, Salmon's theorem, and the Guth–Katz induction. Lemma 8 of the paper (generators of ruled surfaces as curves in ) is not posed. Proofs of any milestone are welcome, as are proofs of the projective-geometry milestones as standalone Mathlib-style lemmas.
In Wasserstein distributionally robust optimization (DRO) a decision is evaluated against the worst distribution within an optimal-transport ball around a nominal distribution . For a Wasserstein distance of finite order , the ball constrains an average transport cost. The case is different. The -Wasserstein distance constrains the largest distance any unit of mass travels, so it describes perturbations in which every sample may move, but only within a fixed radius. This is the perturbation model of adversarial training (Sinha, Namkoong and Duchi 2018) and of distributionally robust chance constraints (Xie 2021).
Zhang, Yang and Gao (arXiv:2205.00362v4, §5.1) generalize to an arbitrary cost , the maximum transport cost . They show (Theorem 2) that on a Polish space with a continuous cost the worst-case loss is a nominal expectation of a local supremum. Their Theorem 1 covers finite-order costs. Its proof does not reach this case, because is not an integral of the cost, and a separate argument is needed.
Timeline. Strong duality for finite-order Wasserstein DRO was proved for empirical on convex subsets of by Mohajerin Esfahani and Kuhn (2018). On Polish spaces it was proved for a lower semicontinuous cost and an upper semicontinuous loss by Blanchet and Murthy (2019), and for a power of a metric by Gao and Kleywegt (2023). For distributionally robust chance constraints, Xie (2021) treated the 1-Wasserstein distance on a totally bounded Polish space. Yang and Gao (2022, Optimization Online) obtained the -Wasserstein chance-constraint reformulation on normed spaces. Zhang, Yang and Gao (arXiv 2022, v4 2024) state the -Wasserstein and maximum-transport-cost duality for a continuous cost on a Polish space (Theorem 2 and Example 7).
Let be a Polish space (complete, separable, metrizable) with its Borel -algebra , and let be a probability measure on , the nominal distribution. A cost is a continuous function with , written with the nominal point first. A loss is a measurable with . Expectations take values in .
For probability measures let be their couplings: the probability measures on with marginals and . The maximum transport cost and its robust loss are
For a metric , . The Legendre transform of is , and is the soft-penalty counterpart .
The proof uses the interchangeability principle (IP). A measurable satisfies (IP) if is -measurable and
where is the set of probability measures on with first marginal . It also uses the measurable projection (Proj) and measurable selection (Sel) conditions of §3 of the paper.
For every and every ,
The result. Theorem 2 turns an optimization over probability measures into one expectation under of a deterministic local problem. Each nominal point is replaced by the worst point of its -ball. For an empirical this is a finite sum of local maximizations. This is the reformulation used for -Wasserstein adversarial training and for distributionally robust chance constraints. Example 7 of the paper derives from it, for , the robust chance constraint on a Polish space. The theorem needs no convexity, no semicontinuity of and no finiteness of the support of .
Formalizing it. The result is proved on paper; no machine-checked proof exists. A formal proof requires measurable projection and selection on Polish spaces, which Mathlib has only in part (analytic sets, Lusin separation). It also needs Prokhorov compactness for couplings and essential suprema under weak convergence. The milestones isolate these, so each can be attacked separately and reused.
The obvious argument restricts to deterministic transport plans with . This argument has two gaps. First, the maximizing map must be measurable, and the local supremum is in general only universally measurable, not Borel. Measurable projection and selection theorems for analytic sets are therefore needed, and the expectation must be read against the completion of . Second, the constraint is an infimum over couplings, and an infimum need not be attained. Without attainment one only obtains an inequality. Attainment is where Polishness of and continuity of enter, and continuity cannot be dropped. Remark 5 of the paper gives a discontinuous metric cost on for which the identity fails.
[TopologicalSpace X] [PolishSpace X] [MeasurableSpace X] [BorelSpace X].ModelRiskOT.Duality.extIntegral, with lower Lebesgue integrals in EReal. It agrees with the paper whenever one part is finite and gives for . For the universally measurable integrand of the goal it is the completed integral. The Bochner integral is not used.essSup of , so .EReal, so for . The Legendre transform ranges over all real .EReal.NullMeasurable.The goal is stated only through , , the Legendre transform and the local supremum. (IP), (Proj) and (Sel) appear only in milestones, so no hypothesis of the goal assumes the duality it asserts. The robust loss is not defined through an ENNReal comparison either, which would make the ball at negative radii coincide with the ball at radius .
A complete development needs the following:
Contributions to any of these layers are welcome independently.
A forward–backward stochastic differential equation (FBSDE) couples a forward SDE, solved from an initial state, with a backward SDE, solved from a terminal condition that depends on the forward state. Such systems arise from the stochastic maximum principle, from quasilinear parabolic PDEs through Feynman–Kac formulas, and in mathematical finance. Whenever a control problem or a market model is solved through its first-order conditions, a fully coupled FBSDE appears, and the question is whether it has a unique solution.
The history has a recurring gap: each method covers a different regime, and none handles coefficients that are random, fully coupled, and have a forward diffusion depending on the martingale integrand , over an arbitrary horizon.
Fix a horizon and a probability space carrying a one-dimensional Brownian motion , with its natural filtration augmented by the null sets. All processes are real valued. The FBSDE (1.1) is
for , with . The coefficients depend on and on . Assumption 2.1 asks that they be progressively measurable for fixed , that be finite, and that they be Lipschitz in with a common constant , uniformly in . Solutions are sought in the space of progressively measurable with .
A decoupling field (Definition 2.2) is a random field with such that, on every short interval and from every square-integrable initial state, the FBSDE with terminal map is uniquely solvable and its solution satisfies .
The difference quotients (3.1) of the coefficients — in the variables () and for — enter the scalar function
and its essential supremum and infimum over all quotients give the dominating ODEs (3.13): and , with the bounds of .
Fix with , , (5.13). There are and , depending only on , and , such that whenever Assumption 2.1 holds and the quotients satisfy one of the nine conditions of Cases I–III ((5.14); (5.15)–(5.18); (5.19)–(5.22)), uniformly in the quotient arguments, then (i) the FBSDE has a decoupling field whose quotient obeys the bound assumed of with replaced by , and (ii) for every there is a unique solution in , with
A companion statement, Corollary 7.5, gives well-posedness over under the sign conditions (7.5) or (7.6), with no smallness constant.
The theorem replaces structural assumptions (small horizon, monotonicity, deterministic coefficients, independent of ) by conditions that can be read off the coefficients through a scalar ODE. It covers random coefficients and a forward diffusion that depends on , the case in which the classical Riccati-type obstruction appears, and it recovers the earlier sufficient conditions as special cases (§7.4 of the paper). The decoupling field produced in (i) is uniformly Lipschitz, which is the input to the comparison and stability results of §8 and to numerical schemes based on .
The result is proved in the paper; nothing here is open mathematically. None of it is formalized: there is no machine-checked existence theory for coupled FBSDEs in any proof assistant this mission is aware of. A complete development would be the first formal well-posedness theorem for a fully coupled FBSDE, and the milestones — the ODE comparison lemma, the small-time theory, and the patching argument of Theorem 2.3 — are each self-contained.
The obvious approach is a contraction argument on . It works only when is small, because the Lipschitz constant of the solution map grows with the coupling; iterating it over a partition requires a terminal condition whose Lipschitz constant does not deteriorate from one subinterval to the next. Controlling that constant is the whole problem. Its spatial derivative satisfies a backward stochastic Riccati equation with quadratic growth in both and and a singularity where ; such equations need not have bounded solutions, and the standard comparison theory for quadratic BSDEs does not apply off the region where the generator is Lipschitz. A second difficulty is the small-time theory itself: when depends on , even a linear FBSDE with constant coefficients is well posed on short intervals only if (Theorem 7.1 of the paper), so in Cases II and III, where and are large, the contraction argument does not apply even for small .
The development reuses the platform's Peng1990.SMP.Stochastic (standard Brownian motion, , the Itô integral IsItoIntegral) and the augmented Brownian filtration of ReflectedBSDE.Existence.Setting. Time is , time integrals are over real intervals, and the stochastic integral is for an Itô integral process of .
Committed conventions:
The constants , and are chosen before the probability space and the coefficients. A formalization that places them after the coefficients, integrates without integrability, divides at the pole , uses a real-valued essential supremum of an unbounded family, or states uniqueness without a solution class would make the statements vacuous or false; none of these is used.
Contributions are welcome on every milestone. The ODE layer (Lemma 5.1 and the a priori bounds of Theorems 5.9–5.11) needs only real analysis and is a natural first target. The stochastic layer needs Itô-integral facts (linearity, restriction to subintervals, the Burkholder–Davis–Gundy and Doob inequalities in ) and the Lipschitz BSDE theory; these are reusable well beyond this mission.
Deciding whether a real polynomial is non-negative on is NP-hard already for quartics, and the standard computational substitute is to ask whether it is a sum of squares (SOS) of polynomials, which is a semidefinite feasibility problem. The two notions agree only in three cases, determined by Hilbert in 1888: univariate polynomials, quadratic forms, and ternary quartic forms (equivalently, polynomials of degree at most 4 in two variables). Outside those cases there are non-negative polynomials that are not SOS, among them symmetric ones: Choi and Lam exhibited a symmetric quartic form in four variables that is non-negative but not SOS.
Many polynomial optimization problems are symmetric, invariant under permutations of the variables. Riener, Theobald, Jansson Andrén and Lasserre (arXiv:1103.0486, Math. Oper. Res. 2013) study how symmetry reduces the size of SDP relaxations. Their §5 uses the degree principle, introduced by Timofte (2003) and refined by Riener (2012), to replace one symmetric problem in variables by finitely many problems in few variables. For symmetric quartics this yields an exact SOS certificate of non-negativity in every dimension: Theorem 5.5, the goal of this mission.
Timeline:
Let . A polynomial is symmetric if for every permutation ; its degree is the total degree. A polynomial is a sum of squares if for some polynomials in the same variables.
For symmetric put
and let be the set of points with at most distinct components.
An -partition of is a vector of positive, non-increasing integers with ; denotes the set of all of them. For ,
and . For the partitions are with , ; there are of them.
For and a symmetric of degree ,
with the set of 2-partitions of .
Theorem 5.5 turns non-negativity of a symmetric quartic in any number of variables into semidefinite feasibility problems of fixed size, one per 2-partition, each in two variables. This is a certificate scheme that is exact, in contrast with the SOS relaxation in variables, which fails for the Choi–Lam quartic. Proposition 5.1 and (5.1) are the general mechanism behind it, and they apply to any symmetric problem whose degrees are small relative to : they underlie the reduced relaxation hierarchy of Theorem 5.2 of the same paper.
All four milestones and the goal are proved results in the literature; the work is formalization. As far as a search of the platform shows, neither the degree principle nor Hilbert's ternary quartic theorem has a machine-checked statement on Prove2Me, and Mathlib has the vocabulary (MvPolynomial.IsSymmetric, IsSumSq) but neither theorem. Hilbert's theorem is a classical result of real algebraic geometry that is reusable far beyond this mission, for example in any SOS-exactness argument in low dimension.
The obvious route to the goal is to apply Hilbert's theorem to each , and that is the whole printed proof; it gives only the direction "non-negative implies every is SOS". The converse, "every SOS implies non-negative", is not a consequence of Hilbert's theorem: it says that a symmetric quartic attains its infimum, if anywhere, on points with at most two distinct coordinate values, which is the degree principle with . The paper quotes the degree principle from Riener's earlier work without proof, and it is not available in Mathlib.
Hilbert's theorem itself is the hardest item. It is a statement about all non-negative quartic forms in three variables, with no symmetry to exploit, and every known proof needs substantial real algebraic geometry beyond what Mathlib provides; it is not a computation on a Gram matrix.
Polynomials are MvPolynomial (Fin n) ℝ; evaluation is MvPolynomial.eval; degree is totalDegree; symmetric is MvPolynomial.IsSymmetric; sum of squares is Mathlib's IsSumSq in the relevant polynomial ring (the empty sum is allowed, as on the page). An -partition is encoded by its block map , required to be monotone, surjective and with non-increasing fibre sizes; this is in bijection with the page's , and is the substitution . Infima in Proposition 5.1 and (5.1) are taken in EReal, so empty feasible sets give and unbounded problems give ; no extended-real arithmetic is used.
Disclosed additions and readings, each forced by the page:
Ruled out: replacing "sum of squares" by non-negativity of (which would make the goal Proposition 5.1 alone), real-valued infima (which are on empty or unbounded sets), or arbitrary maps in place of 2-partitions.
Welcome contributions: Hilbert's theorem on ternary quartics in any standard form; homogenization and dehomogenization lemmas for MvPolynomial and IsSumSq; the degree principle, first for (the case the goal needs) and then with constraints.
In many operational problems the decision is taken after observing covariates (weather, calendar, prices) that carry information about an uncertain quantity (demand, yield, return). The target is the conditional stochastic program: minimize over a feasible set . Kannan, Bayraksan and Luedtke (Math. Program. 2023) approach it in two steps: fit a regression model of on , then use the regression residuals as scenarios of the uncertainty at the new covariate . Their earlier work (Kannan, Bayraksan, Luedtke, arXiv:2207.13554) analysed the sample average approximation built in this way (ER-SAA). The 2023 paper wraps the same scenarios in a distributionally robust problem, to protect against the small-sample error of the regression and of the residuals.
This mission formalizes the paper's rate of convergence for a family of ambiguity sets that contains sample robust optimization and reweighting (φ-divergence, CVaR) sets as special cases.
Responses follow , with regression function and error of law . A known nonempty closed convex set contains the range of , with orthogonal projection . From data , with , one computes a regression estimate and residuals . At a covariate realization the scenarios are .
The true problem (3) is with , and the full-information SAA objective (4) is .
The unified ambiguity family of §5 has two radii. is the radius of balls around each scenario. is a set of probability vectors that shrinks to the uniform weights. The worst-case expected cost over the distributions with and is the ER-DRO objective
and the ER-DRO problem (8) is , with optimal solution . Taking gives sample robust optimization; taking gives ambiguity sets with the same support as the empirical residual distribution. The intermediate objective reweights the true scenarios.
Assume the following:
Then
Theorem 17 shows that robustifying the residuals-based SAA costs nothing in rate. With the ER-DRO estimators converge at the rate of the ER-SAA estimators, which is set by the regression step: for OLS or Lasso, and for kernel regression or random forests. It covers in one statement sample-robust sets, φ-divergence sets and CVaR sets around the residual scenarios. It is the template for the paper's mean-rate analogue (Theorem 18) and for the consistency results (Proposition 15, Theorem 16), which reuse Lemma 14.
The result is proved in the paper; nothing in it is machine-checked. The mission produces checked versions of the decomposition (12) and of each step. It also produces a reusable predicate, a statement of a functional CLT in through Mathlib's convergence in distribution, and the passage from a uniform objective rate to rates for the optimal value and the out-of-sample cost.
The paper's proof is short, but each line hides a step. The obvious bound on the regression term uses the plain average . Under a reweighting that average is no longer what appears, and controlling needs the factor , which stays bounded only because of the rate in Assumption 12.
The full-information term needs tightness of from convergence in distribution in . That is a continuous-mapping and Portmanteau argument on a function space, not on .
All suprema over may be infinite for individual data realizations, and the probabilities of the events involved need not be measurable. Arithmetic with (sums, products with , comparing rates ) must be carried out with these in mind.
Carriers are the Euclidean spaces , , . The data are random variables on a probability space , and sample is i : Fin n. The covariate is fixed, and the paper's "for a.e. " assumptions are hypotheses at that . No i.i.d. assumption is made. is a nonempty subset of the probability simplex. The limit clause of (9) concerns the family in the radius at fixed ; Theorem 17 does not use it, so it is omitted. Assumption 12 is printed as an equality for every , which cannot hold at (there ), so it is required for all large . is defined by the explicit formula of p. 20, which the paper states equals the worst-case expectation over . and a true minimizer are taken as given selections of minimizers; the paper's standing assumptions guarantee they exist.
means: for every there are and with for all , for -valued . Every supremum over is computed in , so an unbounded family is never read as . Convergence in distribution is Mathlib's TendstoInDistribution for the Borel -algebra on .
The sample-robust balls are centred at the projected residual scenarios, not at the true scenarios . Centring them at the true scenarios would make the regression term vanish and the goal close to the full-information result.
A complete development needs the Cauchy–Schwarz steps of Appendix A.6 and the nonexpansiveness of the projection onto a closed convex set (inequality (6)). It also needs a calculus of , tightness of norms under convergence in distribution in , and the passage from uniform objective rates to optimal-value rates. The calculus and the tightness lemma are reusable beyond this paper. Contributions proving any milestone, or general lemmas as separate theorems, are welcome.
Designing a network that survives the failure of any single link is a basic problem of network design: given a graph whose links can be bought, choose as few links as possible so that the chosen subgraph still connects all vertices after any one of its links is removed. This is the minimum 2-edge-connected spanning subgraph problem (2ECSS). It is NP-hard, since the 2-edge-connected spanning subgraphs with edges are exactly the Hamiltonian circuits, and it is a relaxation of the graphic travelling salesman problem: every tour of a 2-edge-connected graph yields a 2ECSS with at most as many edges.
Timeline of approximation ratios for unweighted 2ECSS:
A graph has finite vertex and edge sets; every edge has two distinct ends, and parallel edges are allowed. For , is the set of edges with exactly one end in , and for we write . An edge set is 2-edge-connected spanning (a 2ECSS of ) if is connected and stays connected after the deletion of any single edge of ; is 2-edge-connected if is.
The cut relaxation of 2ECSS is
Every 2ECSS crosses every cut at least twice, so , the minimum size of a 2-edge-connected spanning multi-subgraph.
An ear-decomposition of starts from a single vertex and adds ears : paths whose two ends, or circuits whose one vertex, lie on the earlier ears, and whose other (internal) vertices are new. The ears partition . An ear of length is even if is even, nontrivial if , and short if . A nontrivial ear is pendant if no nontrivial ear has an end among its internal vertices; denotes the number of pendant ears. is the minimum number of even ears over all ear-decompositions, and .
An ear-decomposition is nice if it has even ears, all its short ears are pendant, and internal vertices of different short ears are non-adjacent. The internal vertex sets of its short ears avoiding a set form an eardrum . An earmuff chooses, for some , a path with for each so that the union of their edges is a forest. is the largest such , and .
For every 2-edge-connected graph there is a 2ECSS with
The theorem gives a polynomial-time -approximation for unweighted 2ECSS. Because it compares with rather than with the optimum, it also bounds the integrality ratio of the cut relaxation on unweighted instances by (the paper's Corollary 31). The two lower bounds and and the construction of Theorem 24 are shared with the paper's result for graphic TSP and its result for connected--joins, so the milestones of this mission are also steps toward those results.
The theorem is proved in the paper, and to the best of current knowledge none of it is machine-checked: there is no formal development of ear-decompositions, of Frank's even-ear parameter , or of 2ECSS approximation in Mathlib or on Prove2Me. The work here is formalizing the known proofs. Theorems 7 and 19 rest on classical results that are absent from Mathlib: Frank's theorem on ear-decompositions and the Edmonds–Johnson/Lovász packing of -cuts.
The arithmetic of the final step is short: and . The difficulty lies in the lower bounds and in the decomposition. A natural first idea is to bound every nontrivial ear by its internal vertices. This fails for 3-ears, whose three edges cover only two new vertices, and the paper handles them by making all short ears pendant and pairwise non-adjacent and then re-choosing them as a maximum earmuff. That step needs a matroid-intersection or forest-representative min-max theorem (Theorem 18), which in turn yields . The bound needs Frank's characterization of through minimum -joins together with the half-integral packing of -cuts. None of this machinery exists formally yet.
Every definition is local to the namespace NicerEars.TwoEC. Reusable beyond this mission:
Contributions are welcome on any milestone. Especially valuable are Frank's Theorem 7, the -cut packing behind Theorem 19, and the basic fact that a graph with an ear-decomposition is 2-edge-connected.
Wasserstein distributionally robust optimization (DRO) replaces the expected loss under a nominal distribution (typically an empirical distribution) by the worst expected loss over all distributions within a given optimal-transport distance of . Its tractability rests on a strong duality theorem that turns a supremum over distributions into a one-dimensional minimization over a multiplier of an expectation under alone. Such duality results were proved under successively weaker hypotheses: for finitely supported on by Mohajerin Esfahani and Kuhn (2018), on Polish spaces with lower semicontinuous costs and upper semicontinuous losses by Blanchet and Murthy (2019), and on Polish spaces with general nominal distributions by Gao and Kleywegt (2023). Zhang, Yang and Gao (arXiv:2205.00362v4, 2024) show that, on an arbitrary probability space, strong duality holds exactly when the integrand satisfies an interchangeability principle (IP) between expectation and supremum. That reduces every duality question to verifying (IP).
This mission formalizes the paper's Proposition 2, which verifies (IP) for the most common choice of cost, the -th power of a metric, under minimal hypotheses on and on the loss. The paper uses it for distributionally robust Markov decision processes on Borel spaces, where value functions are only measurable for a completed -algebra.
Let be a metric space and its Borel -algebra. Let be a probability measure on that is tight: for every there is a compact with . Write for the completion of under ; a function is -measurable if it is -measurable.
Expectations take values in the extended reals : .
Let be -measurable with , let and , and define
Let be the set of probability measures on whose first marginal is . The function satisfies (IP) if is -measurable and
No constant is fixed; the statement holds for every and every , including , where may be .
Combined with Theorem 1 of the same paper, Proposition 2 yields strong duality for -Wasserstein DRO on any metric space with a tight nominal distribution, in particular on every Polish space and every Borel subset of one, without semicontinuity of the loss. Allowing to be merely -measurable is what makes the duality applicable recursively in dynamic programming, where each stage's value function is lower semianalytic rather than Borel.
The result is proved in the paper, with the case left to the reader. No machine-checked proof of it, or of any Wasserstein DRO duality theorem at this generality, is known to exist. A formalization would supply the omitted case and pin down the measure-theoretic conventions (extended-valued expectations, completed -algebras) that the paper treats briefly.
The inequality "" is pointwise. The reverse inequality requires a near-optimal coupling, i.e. a measurable near-maximizer of . A general measurable selection theorem is not available: is not assumed Polish and is not assumed Borel, so the projection and selection theorems behind Polish-space duality do not apply. The approximation must also control the expectation of a possibly unbounded , where integrals take extended values and must be avoided.
[MetricSpace X] [MeasurableSpace X] [BorelSpace X]; is a probability measure with IsTightMeasureSet {Phat} (Mathlib's tightness).NullMeasurable f Phat. A Borel-measurable would be a strictly weaker theorem and is ruled out.ModelRiskOT.Duality.extIntegral: in EReal with lower Lebesgue integrals and . The Bochner integral, which returns on non-integrable functions, is not used. Because need not be -measurable, the page leaves undefined for a general coupling; the lower-integral reading is adopted, and stays on as printed.X × NullMeasurableSpace X Phat, with the completion on the second factor.Contributions welcome: lemmas on lower Lebesgue integrals of null-measurable functions under push-forward measures, and tightness-based approximation arguments, both reusable beyond this mission.