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?
Fake accounts (purchased followers, likes and engagement) are a large part of influencer marketing on social media, and platforms say they invest in detecting and removing them. Huang and Liu (Management Science 71(10), 2025) model this market as a signaling game. An influencer of unknown quality buys fake followers to look popular, consumers decide whether to follow, an advertiser pays for the real followers it expects, and the platform, which takes a share of the advertising revenue, chooses how much antifake effort to spend. A practical question for regulators and platform designers follows: does a platform that maximizes profit have any reason to fight fake accounts? This mission formalizes the paper's answer for the purely profit-driven platform: it does not.
The model draws on the signaling literature, in particular the undefeated equilibrium refinement of Mailath, Okuno-Fujiwara and Postlewaite (1993), and is close to the welfare analysis of social-learning manipulation in Chen and Papanastasiou (Management Science 67(11), 2021).
An influencer is of type (probability ) or , with content quality , and . A fraction of consumers (social media literacy) are informed and know the type. The platform picks an effort . With technology level and base price , a fake account costs (1), and following costs a consumer (2), with .
Informed followers of a -type number (8). Uninformed consumers see the early follower count and follow in number (9). The real followers are (10). An uninformed advertiser expects (11). From the -type's side, the advertiser pays for real followers (12). Under a pooling equilibrium both types show the same count and the posterior is . Under a separating equilibrium (costly or natural) the posterior is at the -type's count and at the -type's.
With advertising revenue per real consumer and platform share , the platform's profit under equilibrium type is (6)
where averages (12) over the type. Two thresholds, (13) and (16), with and , select the equilibrium (Proposition 1). If and the equilibrium is pooling. Otherwise it is costly separating for and naturally separating beyond. The equilibrium profit is .
A purely profit-driven platform ( in the objective of (3)) optimally chooses zero antifake effort, and zero is the unique optimum.
Proposition 4(a) separates two motives for antifake effort. Effort harms a profit-maximizing platform twice: it raises the consumers' following cost, which lowers participation and revenue, and it costs . Pooling, in which low-quality influencers successfully mimic high-quality ones, also earns more revenue than separation, because uninformed consumers follow an average influencer more readily than the average of the two types. So any antifake effort a platform makes must come from its concern for consumer welfare (Proposition 4(b)), not from advertising profit. That is the paper's argument for external pressure or regulation.
The result is proved in the paper's Online Appendix. This mission formalizes the main-text claims behind it: the threshold ordering, Lemma 7, the concavity argument and Lemma 8, together with the goal. To our knowledge none of these has a machine-checked proof. The definitions of the follower and profit model are reusable for the companion mission on the influencer's defensive purchasing (Proposition 3).
The obvious argument is "effort only costs, so choose zero". It is incomplete, because effort changes which equilibrium is played, and the equilibrium profit is discontinuous at and . Comparing profits across regimes needs two facts. First, pooling revenue dominates separating revenue at the same effort, a strict-convexity (Jensen) inequality for applied to the uninformed followers through (11)–(12). Second, the thresholds are ordered, , which uses the explicit . The bookkeeping of (10)–(12), where the advertiser's expectation is nested inside the type-average, has to be unfolded exactly. The boundary case falls under Proposition 1(a), so zero effort then induces costly separation, not pooling.
Parameters form a Lean structure with ASCII field names (mu, lamI, lamP, rho, l, qH, qL, c0, c1, tau, p0, gamma). A Standing predicate records the ranges: ; with ; ; ; ; ; . is unconstrained, and Assumption 3 () is a separate hypothesis, used only in Lemma 8(a). The model's expectations are the closed forms (8)–(12); no probability space is built. Follower formulas are untruncated, as in the paper. Assumptions 1–2 depend on , are never stated for a range of , and are not needed, so they are not imposed.
The equilibrium regime map is Proposition 1 taken as a definition: the belief systems, the undefeated refinement and the proofs of Lemmas 1–4 are in the Online Appendix, which this mission does not use. The regime test is " and " for pooling, which matches Proposition 1(a) at . Lemma 7 is stated on all of , a superset of each regime's range. The two separating profits are the same function, because real followers depend only on the information revealed. The concavity milestone assumes , without which both sides are equal.
The goal is about the equilibrium profit computed from (6) and (8)–(12). It is not about abstract regime profits with Lemmas 7–8 as hypotheses, and pooling revenue is not defined by substituting into a single-type formula, which would hide the Jensen step. Consumer welfare is not formalized: its formula is not in the main text, so Proposition 4(b) and Table 3 are out of scope. Contributions welcome: proofs of the milestones and the goal, and a formalization of the signaling game behind Proposition 1.
Video-game consoles, streaming services, ride-hailing apps and payment systems are sold in markets where the value of a product grows with the number of people who use it. In the classical analysis of such markets every consumer buys exactly one of the competing products (singlehoming). Under that assumption, a stronger network effect intensifies price competition in Hotelling models of incompatible products, so equilibrium prices fall (Farrell and Saloner, 1992; Shy, 2001); Katz and Shapiro (1985) find the same under Cournot competition. In practice many consumers own both a PlayStation and an Xbox, or subscribe to several streaming services (multihoming).
Foros, Kind and Stähler (Management Science, 2025; SNF Working Paper 16/21, 2021) let consumers choose endogenously whether to buy one good or both. Their Proposition 1 shows that the classical conclusion reverses once some consumers multihome: near the point without network effects, a stronger network effect raises each firm's demand, price and profit, even when the firms differ in size. This mission formalizes that proposition together with the computations on which the paper rests it.
Two firms are located at the ends of a Hotelling line of unit length, along which a unit mass of consumers is uniformly distributed. A consumer at distance from firm pays a mismatch cost , with . Good has exclusive features worth and shared features worth ; buying good also yields a network benefit , where is the strength of the network effect and is the expected number of buyers of good . Throughout, (Assumption 1 (i) of the paper), and denotes the rival of .
When some consumers buy both goods and expectations are fulfilled (), the paper derives the demand for good at prices :
Maximizing the profit (marginal costs are zero) gives the reaction function
and solving the two reaction functions gives the candidate prices
At these prices the output of good is , the number of singlehomers of good (consumers who buy only ) is , the number of multihomers is , and firm 's profit is . All of these are functions of for fixed . In Lean they are demandM, reactM, priceM, outM, singleM, multiM and profitM in the namespace Multihoming.Local, each taking its parameters in the order .
Partial multihoming means that some consumers buy both goods and some buy only one of each: , , . At this is exactly , and .
Assume and , , . Then there is such that, for each ,
The goal fixes no constant and no size of the neighbourhood: it asserts the direction of every effect near , for asymmetric firms.
The result separates two regimes that the classical theory does not distinguish. Under singlehoming, network effects are a force for competition and lower prices; under partial multihoming, a small network effect makes prices strategic complements (each firm's reaction function slopes upward in the rival's price) and raises the prices, outputs and profits of both firms. This is the paper's explanation for why firms facing multihoming consumers may welcome network effects, and it is the starting point of the paper's later analysis of symmetric firms, of the thresholds on exclusive content, and of mergers.
The proposition is proved in the paper by a short computation: differentiating closed forms at . To our knowledge none of it has been machine-checked. A formal proof would confirm the closed forms (16), (19), (20), the derivative signs (22) and footnote 15, and would upgrade the paper's derivative-at-a-point argument to monotonicity on an explicit interval. The formalization also records a printed slip: the second constant of (22) is printed as , while the value implied by (16) and (17) is . The sign, and so Proposition 1, is unaffected.
Each identity is a rational-function computation with up to quartic denominators, which is tedious but routine once the denominators are known to be nonzero. The substantive step is from a derivative at one point to monotonicity on an interval. The paper computes one-sided derivatives at . To conclude strict monotonicity on , one needs the derivatives to keep their sign on a neighbourhood, which requires continuity of the derivative of each of eight functions (four quantities for each of two firms) and a common . The price claim has no printed derivative at all. A further subtlety is that the profit derivative at is positive only because , which is not a hypothesis but follows from .
HasDerivAt, StrictMonoOn). Lemmas turning a positive continuous derivative on an interval into strict monotonicity are reusable. Proofs of the milestones and of the goal are welcome, as are proofs that derive the goal from the milestones.Short selling is never free. To sell a share short, an investor borrows it from a holder and pays that holder a lending fee, and the size of these fees has been documented empirically for decades (D'Avolio 2002; Duffie, Gârleanu and Pedersen 2002). Most equilibrium models of asset pricing either forbid short sales or take the fee as exogenous. Evgeniou, Hugonnier and Prieto build a continuous-time general-equilibrium economy where the fee is determined jointly with prices: investors disagree about expected dividend growth, the pessimist wants to short, the optimist owns the shares, and the cost of shorting clears the securities lending market. The paper uses the model to explain how a positive shorting cost can coexist with apparent mispricing, as in the 3Com/Palm spin-off.
In the special case of a single risky asset (the market portfolio), the equilibrium reduces to a pair of algebraic equations for the shorting cost and the lending yield at each state, and the paper solves them in closed form (Proposition 3). This mission formalizes that closed form and its comparative statics in the belief gap.
At a fixed state of the economy, three numbers describe the environment:
Short selling is active only when the optimist holds a large enough share of consumption, namely on the shorting region , where
Two unknowns are determined in equilibrium: the shorting cost , the flow rate a short seller pays per unit of position, and the lending yield , the flow rate a lender receives per unit of shares held. The paper shows (p. 27) that with one risky asset they satisfy
The proof of Proposition 3 works with the per-volatility yield and the quadratic
In Lean these objects are costOne σ δ s, yieldOne σ δ s, IsOneAssetSystem σ δ s Φ Γ and gQuad σ Δ s γ, all in the namespace CostlyShort.OneAsset.
For and : for every and every , the pair solves (29)–(30) if and only if
and both (31) and (32), as functions of , are non-decreasing and convex on and strictly increasing for .
A companion statement, not a milestone, formalizes the limits on p. 29: as , and .
Proposition 3 is the only fully explicit equilibrium of the paper. It gives the level of the shorting cost and of the lending yield as functions of disagreement and of the wealth distribution, and its monotonicity in is the model's prediction that short interest and lending fees rise with the dispersion of beliefs, which the paper checks against analysts' forecast dispersion (Table 1). Convexity says the effect accelerates with disagreement. The two-asset case of §4.2 has no closed form and is solved numerically; the one-asset formulas are its benchmark.
The result is proved in the paper, but the proof of the comparative statics is omitted ("We omit the details", p. 50), and the selection of the positive root is asserted ("it is clear"). A formal development supplies the omitted differentiation argument, including convexity across the kink at the boundary of the shorting region, and checks the paper's algebra. No part of this paper has a machine-checked proof.
The algebra of milestones 1, 4 and 5 is mechanical but involves a square root and several divisions, whose signs must be tracked throughout. The substantive step is the comparative statics. Monotonicity and convexity of in need the derivative of a square-root expression on the open region, and then a separate argument at the kink: both functions vanish identically for , so convexity on requires the one-sided derivative at to be non-negative, which is a computation rather than a consequence of convexity on each piece. For the paper's route is indirect: with , and composition of a non-decreasing convex with a non-decreasing convex . Differentiating (32) directly is possible but heavier.
Everything is pointwise in real numbers. The continuous-time economy of §2 (Brownian dividends, portfolio choice, the derivation of (29)–(30) from the equilibrium conditions (16), (20), (21)) is the paper's motivation and is not formalized; Proposition 3 is stated relative to (29)–(30), which is exactly where the paper's proof begins. Conventions committed to:
A trivializing formalization is ruled out: stating only that (31)–(32) satisfy (29)–(30), or convexity only on the open shorting region, would be strictly weaker than the paper and is not the goal.
Needed infrastructure is Mathlib's real analysis: Real.sqrt, deriv, MonotoneOn, ConvexOn, and convexity of compositions. Proofs of any milestone are welcome independently. Facts about convexity of a function that vanishes up to a point and is convex beyond it are reusable outside this mission.
A life assurance pays a contingent lump sum under a policy-defined event, rather than a sequence of survivor-contingent instalments. A benefit paid at the end of the policy year of death has a different value from one paid immediately on death. A pure endowment pays instead when the insured survives to maturity, while an endowment assurance combines cover for death before maturity with a maturity payment to survivors. For these products, the event partition, contractual recipient and payment instant must be explicit before an expected present value is calculated.
Promislow (2015, Chapter 5, sections 5.1–5.8) derives a general annual insurance–annuity relationship from benefit vectors. Dickson, Hardy and Waters (2020, Chapter 4) develops the corresponding conventional life insurance factors. The mission makes the death, survival and maturity events visible as actual random cashflows, then derives the classical identities without taking the desired identities as assumptions.
Let the lifetime-state variable take values . For , state represents death during the policy year whose start is anniversary and whose end is anniversary . State represents survival at the model's right-censoring anniversary. Nonnegative probabilities satisfy . The anniversary survival probability is , for . The annual discount factor satisfies , and all values are expressed at policy commencement, time zero.
For an amount schedule in money per death claim, the random present value of a death benefit payable at the end of the death year is
A temporary assurance of duration includes deaths in policy years . A deferred term assurance adds a waiting period and covers deaths in years . A pure endowment is triggered by and pays at time . The term and maturity components are disjoint for . The specific settlement recipient can be identified contractually; if recipient survival or eligibility changes the payment event, that condition requires an additional model variable.
The foundational result is a reconciliation between the expectation of the realised random present value and a separate valuation made from the probability of death in each covered policy year. For a unit sum assured, both routes must produce an actuarial value from exactly the same state law. The analogous pure-endowment reconciliation averages realised survivor payments and independently discounts the survival tail.
The next result establishes the endowment decomposition from disjoint actual payment events, including the zero-term boundary and a terminal survivor who must not receive a fictitious death claim. The year-end-of-death benefit and the maturity benefit are valued separately. Their combination is then reconciled with a survival-contingent annuity paid in advance at anniversaries .
Writing for the annual effective discount rate, the central finite relationship for unit death and maturity benefits is
Here includes deaths before maturity and settlement at the following policy-year end. The maturity mass captures those alive at . The formula is derived by telescoping discounted survival decrements. When the horizon is right-censored, a whole-horizon death-only assurance omits terminal survivors and requires a residual term. A familiar whole-life identity without that term needs certain death by the terminal horizon or an expressly defined terminal benefit.
The source also defines arithmetic increasing and decreasing insured amounts, geometric escalation and minimum-benefit floors. It constructs the second moment of the actual claim present value by squaring its realised value and compares it to a separate squared-benefit death-mass sum. Distinct death years are mutually exclusive, so mixed claim terms vanish. A variance is meaningful only with a normalised, nonnegative probability law. Additional families cover insurance-term extensions, the split of a deferred term, exact commutation recursions and benefit or discount ordering.
The principal capstone starts with a single finite lifetime law and one annual discount basis. It simultaneously derives the death-claim expectation, the pure-endowment expectation, the disjoint endowment decomposition, the finite insurance–annuity conservation identity and the independent second-moment formula. The conservation equation is the substantive conclusion rather than a restated hypothesis. Each item remains an open theorem statement until a valid Prove2Me proof is separately accepted.
The additional model uses an actual real future lifetime T with a specified probability measure μ supported on nonnegative times. It does not infer a continuous death-time distribution from annual mortality probabilities. At nonnegative maturity n, death in 0≤T<n triggers an immediately paid claim. Death at T=n instead belongs to the pure-endowment event T≥n, even if the probability law has an atom there.
At constant force of interest δ, put U=min(T,n). A continuously paid unit annuity has realised present value Y=(1−exp(−δU))/δ when δ≠0, and Y=U when δ=0. An immediate death benefit or maturity benefit pays exp(−δU) under exactly one of the two events. Therefore its pathwise conservation law is
Taking expectations under the same μ produces the distinct continuous insurance–annuity identity
Fractional-time results specify m>0 annual instalment periods, each ending at (r+1)/m. A death in [r/m,(r+1)/m) is payable at the following subperiod end, without ambiguity at exact grid instants. At nonnegative force, immediate payment is at least as valuable as m-thly payment, which is at least as valuable as year-end payment. Supporting results cover cashflow moments, settlement lag, escalation and UDD-versus-constant-force survival. The annual–continuous bridge equates year-end claim values under matched policy-year death masses.
This event-level basis, grounded in the insurance benefit conventions of Dickson, Hardy and Waters (2020, Chapter 4), supports analyses of death-in-service benefits, death-in-deferment cover, pension-scheme lump sums, term life protection and survival maturity benefits. It also makes transparent why the expected value of a lump-sum death claim can be represented using an annuity schedule only after the schedules and discounting are related mathematically. The annuity correspondence reflects an exact payment-mass identity, and a denominator used for recurring premiums needs strict positivity before division.
These reusable cashflow models can support future dependent-beneficiary and pension-scheme guarantees, but true survivor entitlement requires an additional joint-life state.
Careful classification at anniversaries is essential. In the annual model, a death allocated to the policy year following maturity cannot generate both the pre-maturity death benefit and the maturity benefit. Terminal censoring distinguishes survival observed at the end of a finite table from guaranteed eventual death. The conservation identity should remain valid at zero interest and zero term; when no covered deaths occur, its insurance component must vanish. Later death-year payments also make valuation sensitive to the chosen discount factor.
Death-claim second moments require exclusive event indicators, not independence. The capstones derive values from cashflows rather than commutation-table definitions. These constraints exclude vacuous premises and cosmetic equalities.
The private formal development contains two distinct models: a finite annual right-censored K-model with discount factor v and an actual real-lifetime T-model with exponential discounting at force δ. The annual root remains the main theorem, while the continuous insurance–annuity result is a separate supporting capstone. Targeted Mathlib imports encode a probability measure, real claim instants, fractional settlement and cashflow moments.
The classical actuarial identities are already established in the literature. The Draft contains 119 open theorem statements, including seven explicitly formulated reusable root-support lemmas, with no accepted mission proofs. Pinned-revision private Lean checks have verified 85 distinct theorem statements, including the complete 12-conjunct finite annual root, distribution-level insurance–annuity conservation and the annual–continuous settlement bridge. These are private compiler diagnostics, not accepted proofs of published mission targets.
Annual discount d=1−v differs from continuous force δ. The fractional branch models UDD and finite constant-force survival and bridges half-year survival to the payment grid. General-duration inequalities, death-time density valuation, select tables, dependent-survivor eligibility and infinite-horizon convergence remain open. A time-dependent recipient multiplier does not establish joint-life entitlement.
Flatly Foliated Relativity (FFR) is a theory of gravity introduced by Bray, Hamm, Hirsch, Wheeler and Zhang (arXiv:1911.00967, 2019) that sits between special and general relativity. It keeps the Einstein–Hilbert action of general relativity (GR) but restricts it to spacetimes that are foliated by flat Euclidean spaces (Assumption 1 of the paper): "matter curves spacetime, but not space". The authors motivate this by the observed spatial flatness of the local universe. Since gravitational waves are excluded, FFR is proposed as an approximation of GR whose metric equations are much more tractable. It still contains the big bang (FLRW spacetimes with ), accelerated expansion and the exterior Schwarzschild spacetime.
One headline feature of the theory is how a positive cosmological constant (Assumption 2) shapes it. For the paper shows that the FFR metric equations are elliptic on every slice, that the mean curvature of the foliation gives a geometric arrow of time, and that there is exactly one vacuum solution among solutions that are spherically symmetric at infinity. For uniqueness fails, and for existence fails. This mission formalizes Sections 3.2–5 of the paper, which contain these statements.
All FFR equations live on a single flat slice , with no time derivatives, so the formalization works on with coordinates . The spacetime metric is
where is the lapse and is a one-form on , identified with a vector field through the flat metric. Matter enters through the energy density and the momentum density . Writing , and for the flat Laplacian (summation over repeated indices), the FFR equations (34)–(35) are
Substituting with gives the elliptic form (39)–(41), with unknowns . Here :
together with the requirement at infinity. Vacuum means and . When , the paper fixes the time orientation by the arrow-of-time convention (Convention 1). A pair is spherically symmetric at infinity if it is spherically symmetric on for some . Two vacuum solutions count as the same if they differ by an overall positive constant factor, which corresponds to rescaling .
For , the pair , is a smooth vacuum solution that is spherically symmetric at infinity. Every smooth vacuum solution with and that is spherically symmetric at infinity has the form
Theorem 2 (equivalence with the elliptic form), Theorem 3 (arrow of time), Theorem 4 (ellipticity inequality), Lemma 1 (symmetrization), identity (82)–(83), Theorem 5 (uniqueness for the elliptic form under approximate spherical symmetry), Lemma 2 (: many vacua) and Lemma 3 (: no vacuum).
Corollary 2 is the fourth claim of the paper's main result (Theorem 1). It is the precise sense in which FFR with is rigid, in contrast to GR, which has many vacuum solutions that are spherically symmetric at infinity (gravitational waves). Together with Lemmas 2 and 3, it singles out the sign of as the parameter that controls existence and uniqueness. The intermediate results are of independent use. Theorem 2 lets the elliptic system replace the original one, Theorem 4 is the ellipticity statement behind the existence question posed in the paper (Question 1), and Lemma 1 is a symmetrization inequality for the -Hessian operator .
These are paper proofs. No machine-checked version of any of them is known to the proposer. The mission asks for a complete formal proof of the goal and the milestones in Lean 4 with Mathlib.
The algebra is elementary. The difficulty is analytic. The uniqueness arguments rest on maximum principles for the elliptic equations (41) and (45) on all of under conditions at infinity, on Liouville-type arguments for harmonic functions, and on a Newtonian-potential representation (convolution with the Green's function of ) used to show . Lemma 1 needs averaging over rotations (spherical symmetrization), Jensen's inequality and a characterization of its equality case. Theorem 5 then needs a divergence-theorem argument on large balls that is controlled only by the approximate symmetry hypothesis. Mathlib provides the divergence theorem on boxes and some harmonic-function theory, but no ready-made maximum principle for second-order elliptic operators with variable coefficients on .
EuclideanSpace ℝ (Fin 3). One-forms are vector fields , and the paper's is written w in Lean. Partial derivatives are fderiv applied to the standard basis vectors. Because fderiv returns at non-differentiable points, every statement assumes smoothness (ContDiff ℝ ∞) of all fields, as the paper does.volume.toSphere. "Approximately spherically symmetric at " is read as: is bounded and uniformly as , using operator norms.Mass–energy equivalence is the relationship between mass and energy in a system's rest frame: the two differ only by the constant factor , the square of the speed of light,
It was proposed as a general principle by Albert Einstein in 1905 ("Does the inertia of a body depend upon its energy-content?") as a consequence of special relativity, and it underlies nuclear and particle physics: the mass defect of a nucleus measures its binding energy, and the energy released in fission or annihilation is accounted for by the change in rest mass.
Timeline. Electromagnetic-mass relations of the form were considered in the late 1800s and by Poincaré (1900) and Hasenöhrl (1904). Einstein (1905) derived the relativistic kinetic energy and stated that a body emitting energy as radiation loses mass . Planck, Stark, Lewis–Tolman and Lorentz (1907–1914) rewrote the relation in its modern forms, and von Laue (1911) gave a proof from the stress–energy tensor. This mission follows the Wikipedia article Mass–energy equivalence.
Velocities and momenta are vectors in with Euclidean norm . Fix a speed of light . A body of rest mass moving with velocity , , has
For a finite system of free particles the invariant mass is , the total energy over in the centre-of-momentum frame (zero total momentum). A Lorentz boost with speed along the first axis sends to , .
It contains as the case .
The energy–momentum relation is the kinematic identity behind relativistic energy bookkeeping: rest energy, kinetic energy, invariant-mass reconstruction and the frame independence of rest mass all follow from it. The low-speed expansion makes precise in what sense Newtonian mechanics is the limit of relativity. The composite-system statements formalize why, in relativity, mass is neither additive nor separately conserved while energy and momentum are conserved.
All results are classical and established in the physics literature. The mission produces machine-checked versions of these kinematic facts in a reusable -vector setting with an explicit speed of light.
Most single-particle statements are algebraic once the square roots are controlled; the work lies in handling the square-root and division conventions of a total formal language. The power-series milestone requires the binomial series of , and the asymptotic milestones require Taylor-type bounds near . The non-additivity milestone is a reverse triangle inequality for future-pointing timelike four-vectors, including its equality case, which does not reduce to a one-line computation.
Lean uses EuclideanSpace ℝ (Fin 3) for , with explicit (no natural units). All definitions are total functions: for and , so every theorem assumes and ; rest masses are assumed non-negative. Massless particles cannot be described by velocity-based quantities ( is undefined at ), so milestone 3 is phrased directly in terms of an energy–momentum pair. Only boosts along the first axis are formalized. Systems are finite and free (no interaction potential). Historical derivations (Einstein 1905, Rohrlich 1990) and the nuclear-physics applications are not formalized.
Robust control repeatedly meets linear matrix inequalities that must hold for every value of an unknown, norm-bounded matrix. A typical instance is
where collects model uncertainty or noise. Such a condition quantifies over infinitely many matrices and cannot be checked directly. Petersen's lemma (Petersen and Hollot, Automatica 1986; Petersen, Systems & Control Letters 1987) replaces it by a single inequality in one scalar multiplier . The lemma is a standard tool in the design of quadratically stabilizing controllers for uncertain systems, and it was recently used for controller design from noisy data (Bisoffi, De Persis and Tesi, arXiv:2109.12175).
H. J. van Waarde, M. K. Camlibel, J. Eising and H. L. Trentelman (arXiv:2203.12959v3, 2023; SIAM J. Control Optim.) develop a theory of quadratic matrix inequalities (QMIs) and prove matrix versions of the S-lemma. In §4.5.3 they show that both the strict and the non-strict Petersen lemma follow from their matrix S-lemmas (Theorems 4.10 and 4.7) by a suitable choice of the two quadratic forms. This mission formalizes that derivation.
Timeline. Petersen and Hollot (1986) and Petersen (1987) state the lemma for stabilization of uncertain linear systems. Bisoffi, De Persis and Tesi (arXiv 2021) use strict and non-strict versions for data-driven stabilization. van Waarde, Camlibel, Eising and Trentelman (2023, Proposition 4.16) recover both versions from matrix S-lemmas.
All matrices are real. For a symmetric matrix , () means positive semidefinite (definite), and means ; the notation includes symmetry. is the Moore–Penrose pseudo-inverse and the positive semidefinite square root of .
Quadratic matrix inequalities. A symmetric is partitioned into blocks (), , , (). Its solution sets are
and is defined in the same way with . The generalized Schur complement is , and the class consists of the with , and .
Petersen's data. Fix symmetric, , with , and . The uncertainty set is . Display (4.17) defines
In this proposition the letters of the QMI section become , so .
(a) The robust strict inequality holds if and only if a single multiplier exists:
(b) If , and , the same equivalence holds with in place of on both sides.
The result itself. Petersen's lemma converts a semi-infinite family of matrix inequalities into one inequality that is jointly an LMI after a Schur complement. In controller synthesis this makes robust quadratic stabilization against norm-bounded uncertainty a convex feasibility problem. The derivation in this paper places the lemma inside a general theory: Petersen's lemma becomes the special case of the matrix S-lemmas for the pair of (4.17), and the hypotheses , , of the non-strict version become exactly the Slater condition of Theorem 4.7.
Formalizing it. All results here are proved in the paper. None of them, and no matrix S-lemma, has a machine-checked proof on this platform. The mission produces formal statements and proofs of Petersen's lemma in both forms, of the contraction factorization Lemma A.1, and of the strict and non-strict matrix S-lemmas, which are reused by the data-driven stabilization results of the same paper (Theorems 5.1 and 5.3).
The "if" directions are routine: a multiplier certificate yields the robust inequality by completing a square. The difficulty is the converse, which needs a lossless S-lemma for matrix-valued quadratic forms. The scalar S-lemma rests on the convexity of the joint range of two quadratic forms (Dines' theorem). It does not apply directly to matrix inequalities, and the reduction of Section 4.2 from the matrix case to the vector case is the main obstacle. A second, smaller obstacle is the non-strict case: an equivalence with is false without a Slater-type condition, and the formal statement has to carry , and exactly where the paper does. Petersen's lemma does not follow from a pointwise choice of . The quantifier over must first become a QMI in , which is what Lemma A.1 provides.
Matrices are Mathlib Matrix over ℝ. In the goal the sizes are Fin n, Fin p, Fin q. In the S-lemmas the two block index types are arbitrary finite types, and a partitioned matrix is a matrix over the sum type. is (−X).PosDef and is (−X).PosSemidef; both include symmetry, as the paper's notation does. is (F̄ − FᵀF).PosSemidef. The multiplier is required positive, so is the true inverse. The pseudo-inverse is the unique matrix satisfying the four Penrose conditions, selected by Hilbert's ε, and the square root is Mathlib's CFC.sqrt under the scoped matrix order. "At least one positive eigenvalue" refers to the eigenvalues of the symmetric matrix . "Full column rank" is B.rank = q.
Two choices differ from a literal transcription, and both are disclosed in the items. The strict "Moreover" of Lemma A.1 carries no rank hypothesis, because already forces full column rank. The Schur step includes its non-strict analogue, which the paper uses implicitly ("the proof of statement (b) is analogous").
A trivializing formalization is excluded. The quantifier in the goal ranges over every with , not over a fixed or over . Part (b)'s extra hypotheses are not added to part (a), and the sanity instance , , satisfies every hypothesis and both multiplier conditions at .
A complete development needs: Loewner-order calculus and Schur complements for block matrices; Moore–Penrose pseudo-inverse identities; positive semidefinite square roots; the scalar S-lemma (Dines' theorem); and the reduction from matrix to vector QMIs. The S-lemmas and Lemma A.1 are reusable well beyond this mission. Proofs of any milestone, and of the auxiliary results of §4.1–4.2 (Lemmas 4.1–4.5, Theorem 4.6) as supporting theorems, are welcome.
Quadratic matrix inequalities (QMIs) describe sets of matrices rather than sets of vectors. They appear whenever an unknown matrix is constrained by a quadratic bound: in robust control, where an uncertain block of a system is only known to lie in a norm ball or a sector, and in data-driven control, where the system matrices of a linear system are unknown and the measured data, corrupted by noise satisfying a quadratic bound, only pin them down to a set defined by a QMI.
H. J. van Waarde, M. K. Camlibel, J. Eising and H. L. Trentelman (arXiv:2203.12959, SIAM J. Control Optim. 2023) develop a systematic theory of such sets, culminating in matrix versions of the S-lemma and of Finsler's lemma and in data-based stabilization tests. Before any of that can be used, one has to know when the set of matrices satisfying a QMI is nonempty, convex, bounded, has interior points, or contains strict and boundary solutions. Section 3.1 of the paper answers these questions in terms of the blocks of the matrix defining the QMI. This mission formalizes that section, Theorem 3.2, together with the Schur complement identities (3.2)–(3.4) on which it rests.
All matrices are real. Fix integers . For a matrix , the Moore–Penrose pseudo-inverse is the unique matrix with
is the set of symmetric matrices; for , and mean positive semidefinite and positive definite, , the negative versions, and means (the Loewner order).
A matrix is always partitioned as
For the QMI is
with solution set . Replacing by or gives the sets of strict solutions and of solutions of the quadratic matrix equation. The generalized Schur complement is
and the class (equation (3.5) of the paper) consists of the with
In Lean these are pinv, qmiForm, ZSet, ZPlus, ZZero, schur and InPi in the namespace QuadMatIneq.Basic.
For :
For with and :
Theorem 3.2 turns geometric questions about a set of matrices into finite checks on the blocks of : semidefiniteness, definiteness, vanishing and a rank comparison. In the data-driven setting of the paper, (after transposition) is the set of noise samples, and hence of systems, consistent with the data; part (b) decides when that set is compact, part (c) when it has interior, and (a) guarantees convexity, which is what allows linear matrix inequalities to be used over it. The identities (3.2)–(3.4) are used throughout the rest of the paper, in the matrix S-lemma, the matrix Finsler lemma and the parametrization of solution sets.
The result and its proof appear in the paper; this mission produces machine-checked versions. Mathlib has the Schur complement for invertible blocks and positive semidefiniteness, but no Moore–Penrose pseudo-inverse for matrices and nothing on QMI solution sets. To the knowledge of this mission no formalization of these statements exists.
The obvious argument is the classical Schur complement, which requires to be invertible. Here is only negative semidefinite, and the singular case is exactly where the interesting behaviour lives: the solution set is unbounded precisely when has a kernel, and gives the whole space. Working with the pseudo-inverse requires the range and kernel identities of for a symmetric matrix and the kernel inclusion at every step. Part (c) needs a topological argument about the interior in , and part (e) needs a factorization of one positive semidefinite matrix through another of possibly different size, which is a rank argument rather than an identity.
toBlocks₁₁, …, toBlocks₂₂. Nothing assumes except part (b).Classical.epsilon over the four Penrose conditions. Since a solution exists and is unique, this is the pseudo-inverse and not a default value; the total inverse A⁻¹, which is on singular matrices, is not used anywhere.PosSemidef and PosDef, which include symmetry, matching the paper's convention that definiteness is only asserted for symmetric matrices. is IsHermitian.Infrastructure needed and reusable beyond this mission: the existence and uniqueness of the matrix pseudo-inverse with its basic identities (, is the orthogonal projector onto the range), and the generalized Schur complement identities. Contributions of these as separate lemmas are welcome.
Learning dynamics in games describe how players who repeatedly interact adjust their strategies from observed payoffs. A central question is whether such dynamics lead to Nash equilibrium. For the replicator dynamics, the canonical model of evolutionary game theory, the answer is negative in general: in Matching Pennies and in generic zero-sum games with a unique interior equilibrium, replicator trajectories cycle forever. A classical positive result survives: if a replicator trajectory of a 2-player game stays a bounded distance away from the boundary of the strategy space, its time average converges to the Nash set (Hofbauer and Sigmund, 1998, Ch. 7).
Mertikopoulos and Sandholm (arXiv:1407.6267v2; Math. Oper. Res. 41(4), 2016) study a broad family of continuous-time learning dynamics, regularized reinforcement learning: each player aggregates payoffs into scores and plays the mixed strategy that maximizes score minus a strongly convex penalty function. The family contains the replicator dynamics (entropic penalty) and the projection dynamics (quadratic penalty). For non-steep penalties, trajectories can enter and leave the boundary of the strategy space infinitely often, so the classical "stay away from the boundary" criterion is no longer natural. Section 6 of the paper replaces it with a condition on scores and derives convergence of time averages in zero-sum games with an interior equilibrium.
A 2-player finite game has players , finite pure strategy sets , and payoff functions on pure profiles. A mixed strategy is a probability vector on ; is the set of mixed profiles and the expected payoff (2.1). The payoff vector of player is , the payoff of the pure strategy against the opponent's mixed strategy (2.2). A profile is a Nash equilibrium if no player gains by a unilateral deviation to another mixed strategy; it is interior if for every and . The game is zero-sum if .
On the simplex of a finite set, a penalty function (Definition 2.1) is continuous on , smooth on the relative interior of every face, and -strongly convex for some :
No steepness is required. The choice map is (Definition 2.2), the convex conjugate is (C.1), and the Fenchel coupling is (C.10).
Each player has its own penalty function . An orbit of (RL) is a pair of trajectories , , of score vectors and mixed profiles with
The time average of the orbit is .
If is a 2-player zero-sum game with an interior Nash equilibrium, then for every orbit of (RL),
The statement fixes no rate and no particular penalty function: it holds for every choice of .
The result. Proposition 6.2 shows that the time-average convergence known for the replicator dynamics in zero-sum games is a property of the whole class of regularized reinforcement learning schemes, including those whose trajectories hit the boundary of the strategy space infinitely often, such as the projection dynamics. Time-averaged play of no-regret-type dynamics in zero-sum games is the continuous-time counterpart of the standard argument that averaged learning computes minimax strategies. Theorem 6.1 isolates the mechanism for general 2-player games: bounded score differences suffice, with no zero-sum assumption.
Formalizing it. The results are proved in the paper; none has a machine-checked proof. A complete formalization produces reusable components: differentiability of the conjugate of a strongly convex function on the simplex (a Danskin-type statement), the Fenchel-coupling identity along the dynamics, and a conservation law for zero-sum games. These are the building blocks of many analyses of mirror-descent and follow-the-regularized-leader dynamics.
The first idea, comparing itself with the equilibrium, fails: need not converge, and for non-steep penalties it does not stay in the interior, so the Kullback–Leibler argument used for the replicator dynamics is unavailable. The conserved quantity is a function of the scores , not of , and turning its boundedness into control of score differences requires the asymptotic behaviour of the choice map when some scores diverge. The second difficulty is analytic: is not differentiable at the boundary of , yet must be differentiable everywhere on the score space, with derivative , for the chain rule along (RL) to apply. Finally, the passage from score differences to the time average uses that is linear in the single opponent's strategy, which is specific to two players.
Fin 2, strategy types A k are finite, payoffs are real functions on pure profiles; mixed profiles, expected payoffs and mixed Nash equilibria come from the published agt_games vocabulary (AGT.IsMixedNash). Zero-sum is for every pure profile; interiority is .IsPenalty h K is Definition 2.1 with strong convexity in the Euclidean norm; since is existential the class does not depend on the norm. Steepness is not assumed. Each player has its own .IsChoice h y x (maximizer of over ), never a chosen argmax. An orbit is IsRLOrbit u h y x: for , and , a right derivative at . This differential form is equivalent to the integral form (RL) because is continuous along an orbit.Metric.infDist in the sup metric on profiles. For Theorem 6.1, which has no equilibrium among its hypotheses, the conclusion also asserts that the Nash set is nonempty, because the distance to the empty set is in Lean.Contributions are welcome on any milestone; Proposition C.1 and Proposition A.1(iii) are self-contained convex-analysis statements about a single penalty function.
A variational inequality asks for a point of a convex set at which a vector field points "inward" against every feasible direction. It is the common form of convex minimization (with a gradient), of saddle-point problems (with the monotone operator of a convex–concave function), of Nash equilibria of convex games, of complementarity problems and of traffic and economic equilibria. Iterative methods that use only evaluations of and projections onto the feasible set are the methods of choice when the problem is large, because each step is cheap.
The classical such method, the projected gradient iteration , does not converge for merely monotone . Korpelevich's extragradient method (1976) does, at the price of two projections and two evaluations of per step, and it is known to converge R-linearly under strong monotonicity (Tseng 1995, reference [19] of the paper). Popov (1980), Tseng (2000) and Censor–Gibali–Reich (2011) reduced the number of projections or evaluations. Yu. Malitsky's projected reflected gradient method (arXiv:1502.04968, SIAM J. Optim. 25(1), 2015, doi:10.1137/14097238X) uses one projection and one evaluation of per step, evaluating at the reflected point instead of at . This mission formalizes the paper's second main result: under strong monotonicity the method keeps the R-linear rate of the extragradient method.
Let be a real Hilbert space with inner product and norm , let be closed and convex, and let . The metric projection is the unique point of nearest to . The variational inequality (1.1) is
with solution set . The paper's standing assumptions for this result are
Algorithm 3.1 chooses and a step and iterates
The Lean development names these objects proj, solSet, IsStronglyMonotoneMap, IsLipschitzMap and IsPRGRun in the namespace ProjReflGrad.Linear.
Under (C1), (C2*), (C3) and , every run of Algorithm 3.1 converges to the solution of (1.1) at least R-linearly:
The goal fixes neither nor ; the proof produces them from , and , but the theorem asserts only the shape of the rate.
In attack order:
The result. Theorem 3.3 shows that halving the per-step cost of the extragradient method does not cost the linear rate under strong monotonicity. For strongly monotone problems (strongly convex minimization, strongly convex–strongly concave saddle points, strictly monotone games with a quadratic margin) the method therefore reaches accuracy in iterations with one projection each, which matters when projecting onto dominates the cost. The two-step recursion (3.9) and Lemma 2.8 are also a reusable template: the same mechanism gives linear rates for other methods with a memory of one past iterate.
Formalizing it. The theorem is proved in the paper; nothing here is open. No machine-checked proof of it, or of its lemmas, is on the platform. A formal proof needs the projection inequality in a general real Hilbert space, a careful account of the reflected iterate, and a rigorous version of Lemma 2.8, whose printed proof leaves the range of and the positivity of implicit. The deliverable is a checked R-linear rate for a one-projection method in infinite dimension.
The natural first attempt, a contraction (Q-linear convergence), is not what the paper proves and is not available: the reflected point depends on , so the error at step is controlled only by the errors at steps and , together with auxiliary terms and . Strong monotonicity is applied at , not at , and can be smaller than ; the lower bound may even be negative. The step range is exactly what keeps the coefficients of the Lipschitz error terms below the gain from the projection inequality, and the resulting two-step recursion needs Lemma 2.8, with its choice of and , to yield a geometric bound.
[CompleteSpace H]); it is never specialized to .LipschitzWith, whose constant admits ). (C1) stays in the goal: it is the paper's assumption and its only source of .VectorSpaceOpt.min_distance_convex_set, included as a reference. Contributions welcome: proofs of the milestones in any order; Lemma 2.8 and the identity of milestone 2 are self-contained.Many problems in optimization, game theory and mechanics come down to a variational inequality: find a point of a convex set at which a given vector field points "inward" against every feasible direction. Constrained convex minimization (where the field is a gradient), saddle-point problems (where it is the gradient of a convex–concave function with one sign flipped), Nash equilibria of convex games and complementarity problems are all of this form. In large-scale and infinite-dimensional settings the methods of choice are projection methods, which use only evaluations of the field and projections onto the feasible set.
The plain projected gradient iteration does not converge for merely monotone fields: on a rotation field in the plane it spirals outward for every step size. Korpelevich's extragradient method (1976) repairs this with two field evaluations and two projections per iteration. Later methods (Tseng's forward–backward–forward method, 2000; the subgradient extragradient method of Censor, Gibali and Reich, 2011) reduce the number of projections to one, but still need two evaluations of the field.
Yu. Malitsky's paper (arXiv:1502.04968, SIAM J. Optim. 25(1), 2015, doi:10.1137/14097238X) introduces the projected reflected gradient method, which uses one projection and one field evaluation per iteration, evaluated at a "reflected" point, and proves that it converges weakly under the same assumptions as the extragradient method. This mission formalizes that convergence theorem, Theorem 3.2 of the paper.
Let be a real Hilbert space with inner product and norm . Let be closed and convex, and let be a mapping. For , the metric projection is the unique point of nearest to (it exists when is nonempty). The variational inequality (1.1) asks for with
and denotes its solution set. The standing assumptions are:
Algorithm 3.1 (projected reflected gradient method). Fix a step size and a starting point , and iterate
The point is the reflection of through . A sequence converges weakly to , written , if for every .
Under (C1)–(C3), for and every run of Algorithm 3.1 there is with
In the order the proof uses them:
Companion items, not milestones: the defined projection is the metric projection (so runs of Algorithm 3.1 exist from every starting point), Remark 2.1 ( is closed and convex), and the characterization of as the zeros of the projected residual (§3, p. 4).
The result. Theorem 3.2 shows that a monotone Lipschitz variational inequality in Hilbert space can be solved by an iteration costing one projection and one evaluation of per step, the minimum for a projection method, with no knowledge beyond the Lipschitz constant. This halves the cost of each iteration relative to the extragradient method when evaluating is expensive, and keeps the cost of projections at one when projecting onto is expensive. The method and its analysis became the basis for several later algorithms, including the adaptive variant in §4 of the same paper and the golden ratio algorithm of Malitsky (2020).
Formalizing it. The theorem is proved in the paper; no machine-checked proof is known to exist. The formal development needs, beyond the main argument, a usable library of facts about projections onto closed convex sets in Hilbert space, weak convergence of sequences (boundedness of weakly convergent sequences, weak sequential compactness of bounded sets) and Opial's property. These are reused by every weak-convergence proof for splitting and projection methods, and several companion missions of this series and of related papers rely on the same facts.
The naive Lyapunov function is not monotone along the iteration: because is evaluated at the reflected point rather than at , the cross terms do not cancel as they do for the extragradient method. The quantity that does decrease (milestones 3–4) carries extra terms, and the step bound is what the decrease requires. As a consequence, itself is not known to converge, so the standard Opial lemma ("if converges for every and all weak cluster points lie in , then converges weakly") does not apply directly; the uniqueness of the weak cluster point has to be argued with the perturbed quantity and Opial's inequality. In infinite dimension, the weak cluster point step also needs weak sequential compactness of bounded sets, which is not norm compactness.
[CompleteSpace H] in every statement that needs completeness; it is never specialised to , where weak and norm convergence coincide.Contributions welcome: proofs of the milestones in any order; general Hilbert-space lemmas (boundedness of weakly convergent sequences via the uniform boundedness principle, weak sequential compactness of bounded sets, Opial's inequality) are useful well beyond this mission.
Many engineered and natural systems are networks of identical dynamical units coupled through a directed interaction graph: arrays of oscillators, power grids, sensor and multi-agent networks, gene regulatory circuits. A basic control question for such a network is how to force every unit onto a prescribed reference trajectory (an equilibrium, a periodic orbit or a chaotic solution of a single unit) by acting on only a few of them. Applying a feedback controller to a small fraction of the vertices and letting the coupling spread its effect is called pinning control. It was introduced for scale-free networks by Wang and Chen (2002), shown to work with a single controller on undirected networks by Chen, Liu and Lu (2007), and turned into checkable criteria for undirected networks by Yu, Chen and Lü (2009).
Directed networks are harder. Earlier criteria for directed networks (Zhou, Lu and Lü 2008; Song and Cao 2010) were stated through the symmetric part of the coupling matrix, which may have eigenvalues with positive real part even when the network synchronizes, so they lose the structural information of the graph. Yu, Chen, Lü and Kurths (SIAM J. Control Optim., 2013) replaced the standard quadratic Lyapunov function by one weighted with the positive left null vector of the coupling matrix. This mission formalizes their main criterion for strongly connected networks (§3 of the paper) together with the matrix-theoretic lemmas it rests on (§2).
The network has vertices with states . A coupling matrix has for ( means a connection from vertex to vertex ) and zero row sums, . The network is strongly connected if any vertex can be reached from any other by a directed path; is irreducible if no simultaneous permutation of rows and columns brings it to block lower-triangular form with square diagonal blocks of sizes and , . The in-degree of vertex is .
Each vertex runs the dynamics for a continuously differentiable . A reference trajectory solves . With coupling strength , inner coupling matrix and control gains (vertex is pinned when ), the controlled network is
It is globally synchronized if for every , every reference trajectory and every solution. The vector field satisfies Assumption 1 if, for a constant matrix ,
For positive weights put , and .
Let satisfy Assumption 1 with symmetric, let be a strongly connected coupling matrix, and let be positive with having zero row sums (the weights of Lemma 2.12). If
then the controlled network is globally synchronized.
The path to the goal follows the paper: Lemma 2.5 (irreducible strongly connected), Lemma 2.9 ( for nonnegative with constant row sums), Lemma 2.8 (Perron–Frobenius, already on the platform), Lemma 2.11 (a positive vector with ), Lemma 2.12 (the weights ), and the derivative estimate (3.4) for , :
Lemma 2.7, Lemma 2.10, and, under the paper's standing assumptions (, ) with positive definite: Corollary 3.2 (the condition suffices), Corollary 3.3 (i) (an explicit coupling threshold ), and Corollary 3.4 (the necessary conditions at pinned and at unpinned vertices).
The criterion reduces global synchronization of an -dimensional nonlinear system to one linear matrix inequality in the data , and the corollaries reduce it further to an inequality and to explicit bounds. Corollary 3.4 turns this into a pinning rule: vertices whose in-degree is below must be controlled. Weighting by the left null vector of is the device that later work on directed consensus and pinning reuses; Lemmas 2.11 and 2.12 isolate it as a statement about Metzler matrices.
The paper's results are proved on paper; none of them has a machine-checked proof that this mission is aware of. A formalization adds three things: a corrected statement of Theorem 3.1 (see the scope section), a Lean library of directed-network matrix facts (irreducibility in the permutation form, its equivalence with strong connectivity, positive left null vectors, the weighted symmetrization ), and a reusable Lyapunov argument for linearly coupled networks with Kronecker-structured quadratic forms.
The obvious first idea, the unweighted Lyapunov function , produces the symmetric part of , which for a directed network need not be negative semidefinite; this is exactly the defect of earlier criteria. The weights must come from a positive left null vector of , whose existence is a Perron–Frobenius statement that needs irreducibility, hence the graph–matrix equivalence of Lemma 2.5. The analytic part needs a derivative of along solutions on , the conversion of a sum over vertices into a Kronecker quadratic form, and the passage from a negative definite form to convergence of every error component. On the Mathlib side, irreducibility in the paper's permutation sense, spectral radius through characteristic roots, and largest eigenvalues of symmetric matrices all have to be connected to existing API.
States are Fin n → ℝ and matrices are indexed by Fin N, Fin n and, for Kronecker products, by pairs (i, a) with ; the stacked error uses the same order. Convergence (2.7) is stated with the neighbourhood filter of in , which does not depend on the norm. Derivatives are taken within . Pinning is encoded by instead of the paper's reordering of the first vertices. "" is positive definiteness of (Mathlib PosDef, which includes symmetry); every matrix compared with is symmetric by construction. of a symmetric matrix is the least with for all ; is the largest modulus of a complex characteristic root. Global synchronization quantifies over every reference solution and every network solution; existence of solutions is not asserted.
Added hypotheses, each disclosed in the item: in Theorem 3.1 and (3.4), because the printed theorem allows any and is then false (a directed 3-cycle with satisfies (3.2) but its error grows); in Corollary 3.4; at least one pinned vertex in Corollary 3.3 (i); in Lemma 2.10. The weights are not arbitrary: Theorem 3.1 and the corollaries require to have zero row sums, which for a coupling matrix is equivalent to . Assuming the derivative bound (3.4), negative definiteness of or decay of in the goal would trivialize it and is excluded.
The mission needs: graph reachability for matrices with nonnegative off-diagonal entries; Perron–Frobenius for irreducible nonnegative matrices (referenced from the platform); Gershgorin-type bounds; Kronecker products and positive definiteness; and calculus of quadratic forms along solutions. The matrix lemmas (2.5, 2.7, 2.9–2.12) are reusable beyond this mission. Proofs of any item, and alternative proofs of the milestones, are welcome. Corollary 3.3 (ii) is not posed.
A chance constraint asks that an uncertain constraint hold with high probability: a decision is acceptable if the loss it incurs is nonpositive with probability at least . Chance constraints appear in portfolio selection, power-system dispatch, inventory control and engineering design, wherever an occasional violation is tolerable but a frequent one is not. Two obstacles stand in the way of using them. The distribution of is rarely known exactly, and even when it is, the feasible set of a chance constraint is in general nonconvex and hard to compute.
Distributionally robust chance constraints address the first obstacle by requiring the constraint to hold for every distribution consistent with the available information. Zymler, Kuhn and Rustem (Math. Program. 137, 2013) take that information to be the mean and the covariance of . The standard way around the second obstacle is to replace the probability by the Conditional Value-at-Risk (CVaR) of Rockafellar and Uryasev (J. Risk 2, 2000): a nonpositive CVaR implies the chance constraint, and the worst-case CVaR over a moment set can be computed by semidefinite programming. The approximation is conservative, and the question this mission formalizes is when it loses nothing.
Timeline. Isii (Ann. Inst. Statist. Math. 12, 1960) established strong duality for moment problems, the basis of generalized Chebyshev bounds; Calafiore, Topcu and El Ghaoui (Systems & Control Letters 58, 2009) gave the semidefinite form of the worst-case probability of a set under mean and covariance information that the paper uses as Lemma A.2. El Ghaoui, Oks and Oustry (Oper. Res. 51, 2003) computed the worst-case Value-at-Risk of a portfolio under mean and covariance information. Calafiore and El Ghaoui (J. Optim. Theory Appl. 130, 2006) showed that a distributionally robust individual chance constraint with a loss affine in is a second-order cone constraint. Zymler, Kuhn and Rustem (2013) showed that the worst-case CVaR approximation is exact for every continuous loss that is concave or quadratic in (Theorem 2.2), which is the goal of this mission, and extended the approach to joint chance constraints (the companion mission II).
Let be a random vector in . Fix a mean vector and a covariance matrix with (positive definite). The moment set is the set of all probability distributions on with finite second moments, and . The second-order moment matrix is
and is the trace scalar product.
Fix a tolerance and a loss . Write . The CVaR of under is
and the worst-case CVaR is its supremum over . The distributionally robust individual chance constraint is . The worst-case Value-at-Risk is
A loss is quadratic if , with no sign condition on .
For a continuous loss that is either concave or (possibly nonconcave) quadratic in ,
The implication from left to right holds for every loss; the content of the theorem is the converse.
The theorem says that for concave and for quadratic losses the worst-case CVaR constraint, which is a linear matrix inequality in the decision through (20), describes exactly the feasible set of the distributionally robust chance constraint. Its affine special case (Corollary 2.1 of the paper) gives an exact semidefinite representation of robust individual chance constraints with affine dependence on the uncertainty, the case most used in robust portfolio and engineering models. The same equality between worst-case CVaR and worst-case VaR is the starting point of the paper's treatment of joint chance constraints, where an exact representation is obtained by optimizing over scaling parameters (mission II). The quadratic case covers losses such as portfolio variance terms or quadratic constraint functions, which are neither convex nor concave in general.
The results are proved in the paper, but parts of the argument are sketches. Lemmas A.1 and A.2 are strong duality theorems for moment problems that the paper cites from Isii and from Calafiore et al. rather than proves, and the interchange of supremum and infimum in the worst-case CVaR is justified by a citation to a stochastic saddle-point theorem. To our knowledge none of these results has a machine-checked proof. A formalization produces a checked moment-duality theorem with given mean and covariance, a nonlinear Farkas lemma, and a complete proof of the exactness theorem.
The direction from the worst-case CVaR constraint to the chance constraint is elementary. The converse cannot be obtained distribution by distribution: for a single distribution the CVaR is strictly larger than the VaR in general, and for a convex piecewise-linear loss the worst-case equivalence fails (Example 2.1 of the paper). The identity therefore depends on the specific moment set and the specific loss classes, and passes through two infinite-dimensional dualities. The moment set is not compact in the weak topology, since mass can escape to infinity while the first two moments stay fixed, so the minimax interchange in the worst-case CVaR does not follow from a standard compact minimax theorem. Lemmas A.1 and A.2 are stated for an arbitrary measurable function and an arbitrary Borel set; their strong duality uses in an essential way. Finally, the semi-infinite constraint "for all with " involves a strict inequality on a nonconvex set, and turning it into a matrix inequality is where concavity or quadraticity of enters.
Fin k → ℝ; matrices in are indexed by Fin k ⊕ Unit with the extra coordinate last, so that is liftQuad M ξ. is built from the published ConvexOptimization.symQuadBlock.MomentDRO.Conf.HasSecondMoments, meanVec, covMat). It is not restricted to discrete laws, densities or a support set.A complete development needs moment-problem duality on , a convex Farkas lemma, and the S-procedure (already proved on the platform). The first two are reusable beyond this mission, in particular by mission II, which uses Lemmas A.1 and A.2 verbatim. Proofs of any milestone are welcome independently.
An online classifier must predict a label before learning the correct answer. Its errors matter directly: a low numerical loss is useful only if it controls the number of wrong predictions. Chapter 8 of Orabona's textbook examines this connection for linear classification, where a vector of weights produces a score by taking an inner product with the incoming example. The Perceptron is a particularly spare example: it changes its weights only after a mistake, and it needs no learning rate or chosen comparator. This makes its guarantee a useful point of contact between classification mistakes and the convex losses used elsewhere in online optimization.
Theorem 8.2 compares the Perceptron's mistake count with a whole family of comparator losses, indexed by a real exponent . The theorem is a known result in the book, not an unsolved conjecture. The mission concerns a faithful Lean statement and, subsequently, its machine-checked proof. The distinction matters because other Perceptron bounds on the platform address batch separability, multiclass prediction, or a hinge loss only on update rounds; those results do not state this theorem with its constants and quantifiers.
Fix a dimension and a sequence of feature vectors with binary labels , for rounds . The Perceptron begins at . At round it predicts , where . It records a mistake when and, on exactly those rounds, adds to its weights. Write and . A zero score is a mistake even though it is not a strict sign disagreement.
For a score , a label , and a real power , the hinge-power loss is . A fixed competitor has cumulative loss . The loss is zero when gives every example the correct sign with margin at least one. The book assumes the input vectors obey ; is a nonnegative radius. The sequence is arbitrary, so the result includes examples chosen with knowledge of earlier predictions.
The goal is Theorem 8.2, p. 144 of Orabona. For every and every real ,
All constants and the full family of powers are part of the target. For a competitor with , choosing yields the finite mistake bound , as the book explains on p. 144. For a nonseparable sequence, the same statement measures mistakes relative to the competitor's nonzero loss.
The milestone list follows the book's named ingredients: Lemma 4.29 converts an implicit square-root inequality into an explicit one; the constant-step clause of Theorem 2.13 gives the linear-loss gradient bound; and displays (8.4) and (8.5) relate the Perceptron updates to the comparator and to the hinge loss. Theorem 2.13 is stated in the linear, whole-space case used on p. 145. The printed (8.4) has an invalid extra term on its left; the milestone retains the printed text for provenance, while the Lean statement gives the valid comparator inequality used by (8.5). The correction is described in the item and moderation notes.
The guarantee answers a practical question about a simple online rule: how many classification errors can it make when a fixed linear predictor has small convex loss? The answer has explicit dependence on the feature radius, comparator norm, loss exponent, and comparator loss. It contains the separable margin case and also applies when no comparator classifies every example with margin one. The quantifier over all permits a later analyst to choose a competitor after seeing the sequence without changing the algorithm or the theorem.
A complete formalization would provide a reusable account of a deterministic online classifier, its exact zero-score convention, and the passage from update counts to a family of hinge losses. The local Lean declarations currently compile as statements with proof placeholders; compilation does not establish the mathematical inequalities. A proof of the goal and milestones remains to be supplied and checked. In particular, the correction to (8.4) should be made explicit in any downstream development so that later results never depend on the false printed left side.
The mistake count is discontinuous in the prediction score, while the competitor is measured by a smooth family of convex surrogates. A direct comparison of their per-round losses does not give the theorem's constants. The update rule also depends on its own current score, so its condition must be tied to the weight sequence generated by earlier rounds. Treating the update indicators as free variables, or counting only rounds with a strictly negative score, changes the statement.
The book's proof passes through an implicit inequality involving . That relation alone is weaker than the displayed goal until its constants and nonnegative domains are handled precisely. Real powers require special attention at a zero hinge value. The printed (8.4) introduces an additional difficulty: with and two one-dimensional examples , carrying positive labels, its left side is positive while its right side is zero. The valid comparator inequality has to be distinguished from that printed display.
Lean uses EuclideanSpace ℝ (Fin d) for , its Euclidean inner product and norm, and sequences indexed by natural numbers with active rounds . Index zero carries no data requirement. A total recursive definition fixes and every later Perceptron update. Mathlib's Real.sign supplies ; an indicator records both a wrong sign and a zero score. The comparator loss uses a maximum with zero before taking a real power. No probability space is needed because Algorithm 8.2 is deterministic.
The Lean theorems explicitly require binary labels on the active rounds, for the goal, , and . They allow , , and ; the formulas remain meaningful in these cases. The set in the book's theorem is omitted because the assertion uses only the given feature sequence and its norm bound. The constant-step milestone requires because its formula divides by . The definitions include a mistake count, hinge-power loss, cumulative comparator loss, and the fixed algorithm; the theorem layer can reuse Mathlib's inner-product and real-analysis results. Contributions toward these statements, the algebraic milestone, or the full theorem proof are in scope. A run that can skip a zero-score update or whose iterates are chosen independently of the recursion is outside this mission.
Phase recovery asks to reconstruct a complex signal from the moduli of linear measurements, , where is known. The problem arises in X-ray crystallography, diffraction imaging and microscopy, where detectors record intensities but not phases (Shechtman et al., 2015). Since the map is not linear, the problem is non-convex, and a line of work since 2011 replaces it by semidefinite programs over Hermitian matrices.
Two such relaxations are compared in this mission. PhaseLift (Candès, Strohmer and Voroninski, 2013) lifts to and asks for a positive semidefinite with ; its trace-free version is called Weak PhaseLift. PhaseCut (Waldspurger, d'Aspremont and Mallat, 2015) separates amplitude and phase, with , and relaxes the resulting complex MaxCut-type problem to a semidefinite program in a Hermitian matrix with unit diagonal. In the noiseless case the two relaxations are equivalent (Corollary 4.3 of that paper). This mission formalizes the paper's comparison of the two in the presence of noise: Theorem 4.7 and the two lemmas of Appendix A behind it.
Write for the Hermitian complex matrices and for the positive semidefinite ones. Let be the orthogonal projector onto the range , with the Moore–Penrose pseudoinverse. Define the face
the affine section , and the trace-norm distance , where .
After rescaling, PhaseCut minimizes over with . By Lemma 4.1 this objective equals for , so PhaseCut is the projection problem
Weak PhaseLift, as solved by first-order methods with an distance (), is the projection problem in the other direction,
Both aim at a point of ; PhaseCut starts from , Weak PhaseLift from .
Noise enters through with . With the Frobenius norm of a matrix and the Euclidean norm of a vector, an algorithm is -stable at (Definition 4.5) if, for every close enough to zero, every minimizer of its problem satisfies
For , , and :
The constant is the paper's. The paper remarks that any would do, but that variant is printed without proof and is not a target.
The theorem says that PhaseCut is "almost as stable as" Weak PhaseLift: any stability guarantee proved for the lifted relaxation, such as the noisy recovery bounds of Candès and Li for Gaussian measurements (Candès and Li, 2014), carries over to PhaseCut with a constant of the same order. This justifies using PhaseCut, whose block-coordinate algorithms are cheap, with the stability theory developed for PhaseLift. The paper notes that the converse transfer does not seem to hold.
The result is proved in the paper. No part of it has a machine-checked proof that we know of. Formalizing it means proving the trace-norm identity of Lemma 4.1, which needs a Hölder-type bound for an orthogonal projector , the matrix Cauchy–Schwarz estimates of Appendix A, and the contradiction argument of Theorem 4.7, all for complex Hermitian matrices and an arbitrary, possibly non-injective, .
The obvious argument transports a PhaseCut minimizer to a Weak PhaseLift minimizer, but is in general not in , and its compression is not in for the same noise. Two estimates are needed at once: the distance between and , and the size of the new noise vector . Both rest on bounding by the squared noise, which uses the optimality of in (13) against a specific competitor, and on Lemma 4.1, whose printed proof is incomplete: the matrix it calls the projection of onto is not the trace-norm projection in general, so the identity requires a separate lower bound.
Matrices are Matrix (Fin n) (Fin p) ℂ, and signals are vectors Fin p → ℂ. is the matrix of Mathlib's orthogonal projection onto LinearMap.range (toEuclideanLin A); no pseudoinverse is built. The trace norm is the published definition WildeQIT.traceNorm (), and is a real infimum over a nonempty set bounded below by . Frobenius and Euclidean norms are written out as square roots of sums of squares. Diagonal entries and traces of Hermitian matrices are read through their real parts. Lemma 4.1 is stated in , so it also asserts that the trace is real. "Close enough to zero" is , and stability quantifies every minimizer for every small noise.
The formal statements depart from the print in three places:
The case is not excluded; there the hypothesis on Weak PhaseLift fails, as the paper notes. The milestones keep only the hypotheses their proofs use, listed in each statement.
A trivializing formalization would define the minimizer predicates so that no matrix satisfies them, or quantify the noise before . Here (13) and (14) both have minimizers (checked for ), and precedes the noise.
Needed infrastructure: the trace norm and its duality with the operator norm on Hermitian matrices, compressions by orthogonal projectors, and Cauchy–Schwarz for positive semidefinite forms. These are reusable for other trace-norm and semidefinite-relaxation missions. Proofs of the milestones in any order are welcome, as are proofs of the general facts as separate lemmas.
In online convex optimization, a learner selects a point before seeing the current loss. A useful guarantee compares the learner's accumulated loss with that of a single fixed point chosen in hindsight. A step size chosen from a preannounced bound on all future gradients can be wasteful when the realized gradients are small. Chapter 4 of Orabona's online learning text studies step sizes determined from the gradients observed so far. Its adaptive online subgradient descent bound uses the actual sum of squared subgradient norms, without requiring that sum in advance (Theorem 4.14, p. 40).
The chapter then asks for a more informative guarantee when the losses have small values at a good competitor. For self-bounded losses, a small loss at a point limits the size of its subgradients. Theorem 4.30 on p. 45 turns that relation into a bound in terms of the competitor's cumulative loss. This is useful for problems such as the squared hinge loss discussed immediately after the theorem: if one feasible comparator has zero loss on every round, the regret bound becomes independent of the number of rounds. These are known textbook results. The goal here is a machine-checked formulation and, eventually, a proof of the stated constants.
Fix a finite horizon and a nonempty, closed, convex decision set . Its Euclidean diameter is at most : every satisfy . In round , the learner plays and receives a convex loss . The loss sequence is arbitrary. A subgradient of at satisfies for every . The regret against a fixed competitor is
The learner uses projected online subgradient descent. After observing , it sets
when . If , the algorithm leaves . Here is a Euclidean nearest point in . The current gradient appears in the sum defining because the update is made after that gradient is observed. The initial point is any member of , and every admissible choice of subgradient is allowed.
A loss is -self-bounded on when it is bounded below, has a subgradient at each point of , and every subgradient at every satisfies
The infimum is over the whole ambient space. The target theorem additionally assumes that each loss is nonnegative everywhere. The in these formulas is nonnegative. These conventions follow Definition 4.26 and Theorem 4.30 of the pinned preprint.
The first milestone is Theorem 4.14. Under the setting above, for every ,
This bound depends on the gradient sequence encountered by the algorithm. The printed theorem also equates this expression with a minimum over constant positive step sizes. At zero accumulated gradient energy that minimum is an unattained infimum, so the formal milestone states the regret inequality in every case and the identity with the minimum only when the accumulated squared gradient norm is positive.
The goal is Theorem 4.30. If every loss is nonnegative, convex, and -self-bounded on , then for every fixed ,
The target includes the intermediate displayed bound on p. 45 and Lemma 4.29 as milestones. Their statements capture the passage from a regret bound involving the learner's cumulative loss to one involving the competitor's cumulative loss. The constants and are those printed in the theorem; the goal does not replace them with asymptotic notation.
Theorem 4.14 provides a guarantee without supplying a gradient bound or the horizon-dependent sum of squared gradients to the learner. Theorem 4.30 sharpens the interpretation when the losses are self-bounded: for a comparator with , the regret is at most . For larger comparator losses, the bound changes continuously with their accumulated value. The guarantee holds against each competitor, not merely one selected by an infimum over .
A formal development would make the algorithm's timing, its zero-gradient branch, the ambient-space infimum, and the exact numerical constants explicit. These details are reusable in later analyses of adaptive step sizes and small-loss bounds. The proposal contains open Lean theorem statements and a compiled definitions file; it does not claim that these results already have machine-checked proofs in this mission. The metric projection relation is reused from an existing published definition, and the intended work is proving the open statements and developing their supporting inequalities.
A fixed step size can be selected after looking at all gradients, but that selection does not define an online update. The adaptive step size must use only gradients observed through the current round. The zero-gradient case needs an explicit update rule because its displayed quotient has a zero denominator on an all-zero prefix. These issues already appear in the first milestone.
For the goal, the self-bounded inequality controls subgradient norms using loss at the learner's own points. Substituting that control into the gradient bound yields a right-hand side containing , although the desired statement is expressed using . The intermediate estimate on p. 45 is therefore implicit. The square-root inequality of Lemma 4.29 supplies the separate arithmetic statement needed to express the final result with the printed constants. A direct substitution that treats the learner's loss as the competitor's loss would not justify the theorem.
The Lean carrier is EuclideanSpace ℝ (Fin d), including dimension zero; the theorem remains valid there. Rounds are indexed from one, with index zero unused, and sums range over Finset.Icc 1 T. The loss functions are real-valued on the whole Euclidean space. The book permits extended-real losses that take outside their domain; this formalization addresses the real-valued case. Full-space subgradients retain the source's definition. Convexity and nonnegativity hold on the whole Euclidean space, and self-boundedness holds at every feasible point, for each round through .
The adaptive run is a relation covering every legal selection of subgradients and projections. It requires the update after every nonzero gradient and the unchanged point after a zero gradient. The closed, convex, nonempty set assumptions ensure that Euclidean projection is meaningful. The diameter condition is written as for all feasible , so it also covers any valid upper bound on the diameter. Self-boundedness uses the real infimum of the full range of each loss, together with boundedness below; global nonnegativity in the goal guarantees that condition. The explicit and conditions prevent boundary values from silently changing the meaning of a quotient or a square root.
The goal must hold for every comparator and every admissible run. A definition that checks self-boundedness only at , or permits arbitrary next decisions, would lose the algorithmic guarantee. The reusable components are the regret and gradient-energy definitions, the adaptive run relation, the self-boundedness predicate, and the scalar inequality in Lemma 4.29. Contributions that establish the projection analysis and the three listed milestones directly support the goal.
In online learning, a decision is made before the loss for that round is revealed. The learner cannot optimize a known objective once and use its minimizer forever: the sequence of objectives may be arbitrary. A basic performance measure is regret, the learner's total loss minus the loss of one fixed decision chosen with hindsight. A regret bound that grows more slowly than the number of rounds shows that the learner's average excess loss vanishes. Orabona's introduction develops this measure and derives a bound for projected online gradient descent without requiring advance knowledge of the loss sequence (Orabona, Chapter 1 and Theorem 2.13).
The result is useful because it separates the geometry of the feasible set from the size of the gradients seen during play. It also supports step sizes that change with time, which matters when a learner adjusts its updates as more rounds pass. The exact endpoint term in the theorem records information that would be discarded by a coarser regret estimate (Orabona, Theorem 2.13 and the discussion on p. 14).
Let be a nonempty closed convex set in a real inner-product space. At round , the learner chooses , receives a differentiable convex loss function , and incurs . For a fixed competitor , the book's regret is
The competitor stays fixed through all rounds; it is not the best separate decision for each round. The losses may differ on every round, and their sequence is arbitrary (Orabona, p. 2).
A metric projection is a point of nearest to in Euclidean distance. Convexity makes the projection single valued when is nonempty and closed. Projected online gradient descent, Algorithm 2.1, starts from an arbitrary , chooses positive step sizes , forms , and sets
The projection keeps the next decision feasible even when the unconstrained gradient step leaves (Orabona, Algorithm 2.1, p. 12). The first-order optimality condition of Theorem 2.8, the projection inequality of Proposition 2.11, and the one-round inequality of Lemma 2.12 are the numbered milestones leading to the main statement. Lemma 2.31 records the parallel one-round statement for subgradients (Orabona, pp. 11–13, 19).
For of finite diameter , positive nonincreasing step sizes, and any , the main target is the complete first inequality of Theorem 2.13:
The negative terminal term is part of the target. The constant-step clause of the same theorem is a separate companion item. If on every round, it states
This clause has no finite-diameter hypothesis, so it applies on unbounded feasible sets as well (Orabona, Theorem 2.13, p. 13).
The theorem gives a deterministic guarantee against every fixed feasible competitor, for every loss sequence and every valid run of the algorithm. It exposes the cumulative effect of the gradient magnitudes and the step sizes. Its constant-step form uses the distance from the initial decision to the comparator rather than the diameter of the whole set. The bound is therefore informative on some unbounded sets where the diameter term has no finite value (Orabona, Theorem 2.13 and p. 14).
This is a known textbook theorem, not an open conjecture. The mission asks for machine-checked proofs of the source statements in a reusable Lean interface: a fixed-comparator regret definition, a finite-horizon run predicate, and the projection and one-step results. The published metric-projection predicate is reused, while the one-based regret and run definitions are specific to this book's convention.
An immediate attempt to sum the one-round estimate leaves squared-distance terms with different coefficients when the step size varies. They do not cancel as they would with a fixed coefficient. The theorem's monotonicity condition on the step sizes and the finite diameter of are what make a uniform bound possible; omitting either changes the first displayed claim. Keeping the final negative squared-distance term also requires more care than proving only the weaker bound obtained by dropping it. On the nonsmooth side, an arbitrary vector cannot replace a subgradient: its defining inequality supplies the link between a loss difference and the linearized direction (Orabona, Lemmas 2.12 and 2.31, Theorem 2.13).
Lean uses a complete real inner-product space, covering the book's and using only the geometry needed by this chapter. Time remains one based: round zero is unused, sums run from through , and the output after the last round is . The horizon satisfies , so the last step size and the terminal iterate are part of an actual run. The run predicate requires a gradient and a metric projection at every round through ; it does not select a favorable projection after seeing the comparator. The theorem requires each loss to be convex and differentiable on an open neighborhood containing , as in Algorithm 2.1.
The diameter in the main target is Mathlib's real Metric.diam V, with boundedness imposed so that it is the finite supremum in the book. The constant-step clause has no boundedness requirement. The projection relation is the published OnlineConvexOpt.FirstOrder.IsMetricProjection: it includes membership in and minimal distance to the point being projected. Thus, the update cannot be satisfied by an arbitrary point of . Every regret claim quantifies over a comparator ; extending the quantifier outside would assert a different result.
For Lemma 2.31, losses are real valued on , and the stated subgradient inequality is relative to . The book defines a full-space subgradient for an extended-real-valued function; every such subgradient gives the relative inequality used here. This is the precise convention for that milestone and is disclosed in its item description. Contributions that establish the projection inequality, the single-round inequalities, and either complete form of Theorem 2.13 fit the mission. The regret and run definitions can be reused in later deterministic online optimization results, while the projection predicate is already shared with another textbook development.
When the players of a game repeatedly adjust their strategies with no-regret learning algorithms, the empirical distribution of play converges to a coarse correlated equilibrium, and in smooth games the average social welfare approaches the price-of-anarchy guarantee of the game (Roughgarden 2009). For generic no-regret algorithms such as Hedge the convergence rate is , because each player's regret after rounds is of order in the worst case, against an adversary.
Other players are not adversaries: they are also learning, and their strategies change slowly. Syrgkanis, Agarwal, Luo and Schapire (NIPS 2015, arXiv:1507.00407v5) identify a property of learning algorithms, regret bounded by variation in utilities (RVU), under which this predictability can be exploited in general multi-player games, and show that a natural class of algorithms has it. This mission formalizes their first main consequence: if every player uses optimistic follow the regularized leader (OFTRL), the sum of all players' regrets stays bounded by a constant independent of , so the average welfare converges at rate .
Timeline. Rakhlin and Sridharan (COLT 2013; NIPS 2013) introduced optimistic mirror descent and showed convergence to the minimax value in two-player zero-sum games when both players use it. Syrgkanis et al. (2015) extend the fast-rate phenomenon to general -player games and arbitrary no-regret algorithms with the RVU property (Theorem 4), and establish RVU for OFTRL (Proposition 7), giving Corollary 8.
A game has players. Each player has a finite strategy set with , and a utility for each pure profile . A mixed strategy is a point of the probability simplex , and a mixed profile induces the product distribution on pure profiles.
The game is played for rounds. At round each player picks and then observes the utility vector with entries
so that is the expected utility of player at round . The regret of player is
The primal norm is and its dual is . A regularizer is 1-strongly convex if for all , and denotes a bound on its range, on . Optimistic FTRL with step size and predictors plays and, for ,
With one-step recency bias, : the algorithm bets that the next utility vector equals the last one.
An algorithm has the RVU property with constants , if for every utility sequence
If every player runs OFTRL with and , , then for every
A companion statement, Proposition 2 (p. 3), turns a regret bound into a welfare bound in a -smooth game: .
Corollary 8 says that uncoupled learning dynamics, in which each player sees only its own utility vectors, can keep the total regret of all players bounded by a constant in an arbitrary finite game. By Proposition 2 this gives convergence of the average welfare to the price-of-anarchy bound in smooth games, against for generic no-regret algorithms. The RVU framework has since become a standard tool in the analysis of optimistic learning in games, and Theorem 4 decouples the game-level argument from the choice of algorithm.
The paper's proofs are in its supplementary material (App. A and C). None of the results here has a machine-checked proof to our knowledge. A complete formalization produces a reusable layer: utility vectors of mixed profiles, total-variation subadditivity for finite product distributions, and the regret analysis of optimistic FTRL under an -strongly convex regularizer.
The game-level step (Theorem 4) is short once display (2) is available, but (2) itself, subadditivity of total variation over products of finite distributions, is not available in Mathlib in this form.
The core is the single-player analysis. Theorem 19 and Lemma 20 compare the iterates with the leader sequence, an object the algorithm never computes, and both rest on the quadratic-growth fact that a maximizer of a -strongly concave function satisfies . Footnote 3's midpoint inequality does not give the constant in a single application; it has to be upgraded to the standard form of strong convexity first.
Players are Fin n, strategies Fin d; time keeps the paper's indices with and . is the utility vector against , the formula of p. 2 at , which the paper uses but never writes. Mixed profiles and expectations come from the published definition agt_games. is defined explicitly and is Mathlib's sup norm. Regret and are never written as suprema: a bound on is stated for every profile of comparators in , and is any upper bound on the range of every regularizer.
Added hypotheses, each disclosed in its statement:
Theorem 19, Lemma 20 and Proposition 7 are stated for ; the paper allows any norm.
OFTRL is an argmax predicate, so the goal holds for every trajectory the dynamics can produce, not for a chosen one. It is not the entropic closed form (Optimistic Hedge). The utility bound is kept, since the game-level statements are false without it. A sanity file shows that satisfies the strong-convexity hypothesis and that OFTRL runs exist, so the hypotheses are satisfiable.
Contributions are welcome for each milestone. The quadratic-growth lemma for midpoint strongly convex continuous functions on the simplex and the total-variation bound for products are reusable beyond this mission.
Training a model by stochastic gradients on a constrained or regularized loss is a stochastic composite problem: a smooth expected loss, observed only through noisy gradients, plus a simple non-smooth term such as a constraint set or an penalty. For convex losses, accelerated stochastic approximation methods attain the optimal rates (Lan 2012; Ghadimi & Lan 2012). For nonconvex losses, the available guarantees came from randomized stochastic gradient methods (Ghadimi & Lan 2013) and their mini-batch proximal versions (Ghadimi, Lan & Zhang 2016), which are not optimal when the problem happens to be convex.
Ghadimi and Lan (arXiv:1310.3787v1, 2013; Math. Program. 156, 2016) gave one accelerated scheme covering both cases. This mission formalizes its most general result, Theorem 4 (§3.2): the randomized stochastic accelerated gradient (RSAG) method with mini-batches, on a composite objective whose smooth part may be nonconvex and whose gradients are noisy.
Work in with the Euclidean norm. The problem (1.3) is
where is differentiable with -Lipschitz gradient and may be nonconvex, is convex and differentiable with -Lipschitz gradient, , and is a convex, possibly non-smooth function with bounded domain (for instance the indicator of a convex compact set, or that indicator plus ).
The prox map (2.37) is for , and the gradient mapping (2.38) is . With , a small certifies approximate stationarity. Assumption 2 asks for with for all and .
Gradients come from a stochastic oracle: queried at , it returns for a random sample . Assumption 1 asks that the output be unbiased, , with variance at most .
Algorithm 4 takes , for , , batch sizes , starts from , and for sets
With and (2.6), the output is , where is drawn independently of the oracle with
Fix , assume for
let be an optimal solution and . Then
and, if ,
The expectations are over and all samples. The goal keeps general step sizes and batch sizes; Corollaries 4 and 5 (explicit policies) are left for follow-up work.
In the order of the proof: Lemma 4 ( is 1-Lipschitz); the mini-batch variance bound (3.28) and its consequence (3.29) for the gradient mapping; Lemma 1, (2.16) and Lemma 5, the two-sided bound ; the three-point inequalities (3.32)–(3.33) and their combination (3.34); the descent bound (2.46) (already proved on the platform) and (2.47); the one-step and summed inequalities of p. 22; the iterate bound (2.52); the summed inequality at ; and the expected bound (3.35).
The result. Theorem 4 covers stochastic composite problems whether or not is convex, with one step-size policy. Under Corollary 4's policy and batch sizes it gives a sample complexity for that improves the dependence on over mini-batch proximal stochastic gradient [Ghadimi, Lan & Zhang 2016], and when it recovers the optimal rate for convex stochastic composite optimization. Its proof is a template for later variance-controlled accelerated methods: a weighted Lyapunov argument in which nonconvexity enters only through and noise only through the martingale and variance terms.
Formalizing it. The result has been proved and refereed since 2016. As far as is known, no proof assistant has a formalization of it, and the platform has no accelerated stochastic method with a nonconvex guarantee. A complete development gives machine-checked versions of the mini-batch variance bound for martingale-difference noise, the Lipschitz property of the gradient mapping, the proximal three-point inequality on a convex domain, and the composite accelerated analysis with noise. Each of these can be reused in other stochastic proximal methods.
Copying the deterministic composite proof (Theorem 2) fails in two places. First, the deterministic step bounds through the decrease , but here is computed from , so this decrease measures the stochastic gradient mapping. Passing back to the exact one costs an extra variance term, which is why the constant is 8 rather than 2. Second, the noise appears in two ways. The linear term vanishes only in expectation, and only because is fixed before the batch is drawn. The quadratic terms need the variance of an average of dependent samples, which is only when the samples within a batch are conditionally unbiased given the earlier ones. A pathwise argument cannot remove either term, and an unconditional reading of Assumption 1 does not give the second.
EuclideanSpace ℝ (Fin n) (the published GhadimiLan.RSG.E). Smoothness of and is the platform's ConvexOptAlg.SmoothGD.IsBetaSmooth. , and are given with the identities , , .K with finite values X and ConvexOn ℝ K X; the prox map is a function P with the minimizer hypothesis IsProxMap K X P. A real-valued on all of is excluded: it makes Assumption 2 unsatisfiable and the goal vacuous. So is a free P with no minimizer property.GhadimiLan.RSG.AssumptionA1 along these query points: conditional unbiasedness given a filtration of the earlier calls, and conditional variance bound . This conditional form is what the paper's proof uses, and the i.i.d. setting satisfies it. The oracle is jointly measurable. The variance bound (3.28) is a milestone and is never assumed.Contributions welcome: proofs of any milestone. Lemma 4, (3.28) and the three-point inequality are self-contained and reusable. Also welcome: the measurability of the iterates, and Corollaries 4–5 as follow-up statements.
Reinforcement learning with large or continuous state spaces is done in practice with function approximation: the agent represents value functions in a low-dimensional parametric family instead of a table indexed by states. For tabular Markov decision processes, regret bounds of order have been known since the work on UCRL and UCBVI, but they scale with the number of states and actions and say nothing when is infinite. Before 2019, provable guarantees for function approximation either needed a simulator, assumed deterministic transitions, or had regret exponential in the horizon.
Jin, Yang, Wang and Jordan, Provably Efficient Reinforcement Learning with Linear Function Approximation (arXiv:1907.05388, COLT 2020), identified a model, the linear MDP, in which an optimistic version of least-squares value iteration has regret polynomial in the feature dimension and the horizon and independent of and . The model and the algorithm, LSVI-UCB, became a standard reference point for the theory of RL with function approximation.
Timeline:
An episodic MDP has a measurable state space , a finite action set , a horizon , transition kernels and deterministic rewards for steps . A policy chooses an action at each state and step. Its value functions satisfy the Bellman equation , , , where ; the optimal values , satisfy the same recursion with a maximum over actions.
The MDP is linear (Assumption A) with feature map if and for each step there are signed measures and a vector with
and , .
In each episode an adversary chooses the initial state ; the agent then plays steps, the next state being drawn from . LSVI-UCB (Algorithm 1) computes, backwards over , the Gram matrix of the past features , the ridge-regression weight for the targets , and the optimistic estimate
and then plays greedily with respect to . Its policy in episode is , and the regret is
There are absolute constants such that for every linear MDP, every and every run of LSVI-UCB with and , ,
The milestones follow Appendix B of the paper: linearity of (Proposition 2.3) and the weight bounds (Lemmas B.1, B.2, with Lemma D.1); the covering bound for the value class (Lemma D.6, with the Euclidean-ball covering of Lemma D.5); the uniform self-normalized concentration (Lemma D.4, with Theorem D.3) and the good event (Lemma B.3); the error propagation (Lemma B.4), optimism (Lemma B.5) and the recursion (Lemma B.6); and the bonus-sum bound (17)–(18), with Lemma D.2. Lemma D.2, Theorem D.3 and Lemma D.5 are already on the platform and are referenced.
A companion statement, not a milestone, formalizes Proposition 5.1 (§5): on a finite state space with non-degenerate features, if the Bellman operators of (8) map linear action-value functions to linear ones for every policy, then is linear in .
The theorem shows that exploration with function approximation can be sample-efficient without a simulator: the regret depends on the intrinsic dimension of the features and polynomially on , not on the size of the state space. Its analysis, a uniform concentration bound over a data-dependent class of value functions combined with optimism, is the template for a large later literature: misspecified and low-rank MDPs, kernel and neural function approximation, and reward-free exploration.
The result has a published proof, but no machine-checked one. A formalization supplies the measure-theoretic episodic MDP on a general state space, an interaction protocol with adaptive initial states, the LSVI-UCB algorithm, and a checked chain from self-normalized martingale bounds to the regret theorem. The formal statements also record two points where the printed paper is imprecise: the normalization of the measures (see Formalization scope) and the existential reading of the weights in Lemma B.1.
The regression targets depend on all past data through . The self-normalized bound for vector-valued martingales (Theorem D.3) therefore cannot be applied to them directly: the natural first idea, conditioning on the past and treating as fixed, fails because is not measurable with respect to the past at the time is drawn. The concentration must hold uniformly over a function class, which requires a covering-number bound for a class parametrized by vectors and matrices (Lemma D.6) and a union bound in the right scale.
A second difficulty is formal: the probabilistic protocol mixes an adversary, a learning algorithm reading its own past outputs, and transition kernels on a general measurable space, and the martingale argument (Azuma–Hoeffding over the steps) needs every object to be measurable with respect to the right σ-algebra.
Retailers that carry a limited range of products often know something about a customer before choosing which of those products to display. The customized assortment problem asks which products to carry when the displayed assortment may be tailored to the arriving customer's type. This separates the first-stage capacity decision from the later offer decision. El Housni and Topaloglu study the problem under a mixture of multinomial logit choice models and develop an approximation framework for it in their SSRN paper. This mission isolates their structural guarantee for Augmented Greedy, Theorem 4.2 of the PDF version dated 7 December 2021. The theorem identifies the revenue recovered from customer types whose optimal personalized offers agree with a chosen product subset.
The paper contrasts this setting with ordinary assortment optimization, where every type sees the same products. Its later approximation results use the structural guarantee here as a component. The classical comparison is the cardinality-constrained greedy bound for monotone submodular functions, associated with Nemhauser, Wolsey and Fisher (1978). The paper's Appendix B gives an instance in which the customized revenue function lacks global submodularity, so that classical result does not apply directly. El Housni and Topaloglu, §§4 and App. B.
Let be a finite product set. Product has positive revenue , and products are indexed with . Let be customer types. A type- customer arrives with probability , with , and assigns each product a nonnegative preference weight . The no-purchase option has weight one. Offering an assortment to that customer gives MNL expected revenue
If the retailer initially carries only , it can still choose the best offer to each customer type. Thus . For , write , and abbreviate . The first-stage capacity is ; an optimal solution of CAP maximizes among sets with at most products. These definitions and the standing data assumptions are stated in §2 and §4 of the paper.
For each product , the prefix contains products at least as early in the revenue ordering. Greedy starts at the empty set, repeatedly adds an available product that maximizes the new objective value, and stops at cardinality or when the prefix is exhausted. Augmented Greedy runs Greedy on for each , using , and returns whichever candidate has the greatest value. Both stages may break ties arbitrarily. El Housni and Topaloglu, §4.1.
For type , use the optimal personalized assortment , characterized by Lemma E.1. A type is complete with respect to when ; let collect these types. The threshold choice matters because zero-weight products can be present in other optimal offers without helping a customer. El Housni and Topaloglu, Definition 4.1 and App. E.
For every , , with , and every output of Augmented Greedy on ,
This is the mission goal, the structural performance statement of Theorem 4.2, p. 11. It does not assert a constant-factor approximation to all of CAP: it identifies the contribution from complete customer types.
The milestone list follows the results used with this bound: monotonicity of from Appendix C; the MNL threshold assortment of Lemma E.1; submodularity of on from Lemma 4.3; and the cited Greedy guarantee for a nonnegative monotone submodular objective. The greedy milestone compares its output against every feasible set of cardinality at most .
The theorem says that one algorithmic output captures a fixed fraction of the benchmark supplied by complete types, despite the absence of global submodularity of . It connects the local behavior of truncated type revenues to the full customized assortment objective. The paper uses this result in the development of later algorithms; without it, the standard submodular greedy theorem gives no immediate conclusion for CAP. El Housni and Topaloglu, §§4–5.
The mathematical results are proved in the 2021 paper. The formalization work here is to give machine-checkable statements for the objective, the algorithm with all its legal tie choices, and the four supporting targets, then supply proofs. The MNL revenue formula is already available as a published platform definition; the local CAP and algorithm definitions specify the extra model needed by this theorem. A completed development could also support later CAP missions that use the same threshold and submodularity properties.
The tempting argument applies the classical greedy guarantee directly to , since increases when more products are carried. Appendix B of the paper shows that this fails: even for one customer type, need not be submodular. Restricting the ground set to a revenue prefix and truncating each at that prefix's revenue level changes the submodularity question, but the final guarantee must still concern the untruncated objective. The threshold condition in the definition of is what makes that comparison meaningful. El Housni and Topaloglu, App. B, Lemma 4.3 and Theorem 4.2.
Products and types are Fin n and Fin m; their zero-based Lean indices correspond to the paper's indices plus one. Assortments and type groups are finite sets. The model assumes , , , , and decreasing revenue order. The no-purchase weight is exactly one. CAP and personalized revenue use maxima over nonempty finite powersets, so empty input sets have their intended value rather than an arbitrary real supremum. The theorem keeps the source's optimality assumption on , even though its particular inequality uses less.
The Greedy predicate describes each successive maximizer and the exact stopping rule. Augmented Greedy requires a Greedy output at every prefix and an -maximizing choice among them. Thus the output is constrained by the printed algorithm, and the statement covers every tie-break. The type- assortment is defined from by the Lemma E.1 threshold, rather than supplied as a free set. These choices rule out a size-only output condition, an arbitrarily chosen , a vacuous run predicate, and real supremum defaults. The target includes the corner cases , , and , where its right side is zero. Arrival probabilities summing to one force ; Augmented Greedy has an output only when at least one product exists.
The reusable parts are the MNL threshold characterization, finite-set submodularity and the general Greedy bound. Contributions toward those lemmas, the paper's case analysis for Lemma 4.3, and the final structural theorem are in scope. Runtime claims, the paper's later logarithmic approximation theorems and its computational experiments are outside this mission.
Computing an approximate Nash equilibrium of a two-player game is one of the central questions of algorithmic game theory. For a constant approximation , the algorithm of Lipton, Markakis and Mehta runs in quasi-polynomial time , and for a long time it was unknown whether polynomial time is possible. A. Rubinstein, Settling the Complexity of Computing Approximate Two-Player Nash Equilibria (FOCS 2016, arXiv:1606.04550), proved that, assuming an exponential-time hypothesis for PPAD, quasi-polynomial time is also necessary.
The proof is a chain of reductions. Its middle links produce multiplayer games in which only most players are approximately best-responding (the WeakNash notions of Babichenko, Papadimitriou and Rubinstein, Can Almost Everybody be Almost Happy?, ITCS 2016). Its last link turns a bipartite multiplayer game into a two-player game. Section 8.1 of the paper sits between the two: it shows that the weaker mixed-response notion of WeakNash can be converted into the stronger support-based notion, with a loss of only a square root in the approximation. This mission formalizes that step, Lemma 8.1, together with the intermediate claims of its proof.
Timeline. Daskalakis, Goldberg and Papadimitriou (SIAM J. Comput. 2009, doi:10.1137/070699652) introduced the trimming argument (their Lemma 4.28 and Claim 6) for exact-all-players -approximate equilibria of general games. Babichenko–Papadimitriou–Rubinstein (2016) introduced -WeakNash. Rubinstein (2016) adapted the trimming argument to WeakNash of bipartite polymatrix games, where the constant no longer grows with the number of players.
A finite game has a finite set of players , a finite action set for each player , and utilities on action profiles. A mixed strategy is a probability vector on ; a mixed profile is one mixed strategy per player, drawn independently. For an action , is the expected utility of when plays and the others play , and .
A polymatrix game is one in which each pair of players plays a two-player subgame, each player uses one action in all of its subgames, and its utility is the sum of its subgame payoffs. In a complete bipartite polymatrix game the players form two sides , with , ; every plays a bimatrix subgame against every , and same-side pairs play nothing. Lemma 8.1 assumes the payoffs of -vertices lie in and those of -vertices in , so every utility lies in .
The trimmed profile with parameter : every player that plays -optimally in drops the actions with , whose total mass is , and renormalises, on the kept actions; every other player keeps .
For a complete bipartite polymatrix game with the payoff ranges above, , and an -WeakNash , the trimmed profile with satisfies
The result. Lemma 8.1 is the link that allows the hardness of WeakNash, the notion the PPAD-hardness argument naturally produces, to be transferred to the support-based notion used by the two-player reduction of Section 8.2 (Lemma 8.3, via Althöfer's games). The polynomial loss and the unchanged are what keep the final constant approximation constant. The same trimming technique, with constants that do not depend on the number of players, applies to any polymatrix game with normalised payoffs.
Formalizing it. The result is proved on paper; it is not formalized anywhere. The published platform items DGPNash.WellSupported.* formalize the Daskalakis–Goldberg–Papadimitriou version, which assumes every player is -optimal and has a constant growing with the number of players; this mission produces the WeakNash and polymatrix version and a reusable vocabulary of WeakNash notions (Definitions 2.5–2.9) for the rest of the paper.
The obvious argument applies the trimming of Daskalakis–Goldberg–Papadimitriou to every player, and it fails in two places. First, only a -fraction of players are -optimal; for the others the trimmed mass can equal , so the renormalisation is undefined and those players cannot be trimmed, while their neighbours' payoffs still depend on them. Second, the general bound on how much a payoff moves when the other players' strategies move grows with the number of players, which would make the final constant depend on and ; Lemma 8.1 has no such dependence, and the payoff normalisation , is what must absorb it. The constant of milestone 4 is tight enough that the page's own displayed chain, which ends at , does not reach it directly.
VA ⊕ VB; action sets are finite types S i; subgame payoffs are PA v w (for against ) and PB w v. The general polymatrix payoff (Definition 2.9) sums over ; the bipartite instance sets same-side subgames to zero.agt_games bundle. is DGPNash.NashMap.purePayoff; , and the trim formula are maxPurePayoff, trimMass, trim of DGPNash_WellSupported_Equilibria.The bare existence of some -Well-Supported WeakNash is a consequence of Nash's theorem and does not use ; the goal therefore names the specific trimmed profile computed from .
Contributions welcome: proofs of the milestones; general lemmas expressing of a polymatrix game as a bilinear sum and the multilinearity of expected payoffs, which are reusable for the rest of the paper.
Many problems in statistics, signal processing and machine learning have the form "smooth loss plus simple non-smooth term": a differentiable data-fit term together with a constraint set or a sparsity-inducing penalty such as the norm. When the loss is convex, Nesterov's accelerated gradient (AG) method and its proximal variants are known to be optimal among first-order methods: after iterations the optimality gap is , against for plain proximal gradient (Nesterov 1983, reference [24] of the paper; Beck & Teboulle 2009). When the loss is nonconvex, the classical accelerated schemes come with no convergence guarantee at all, and practitioners must choose between a method that is fast on convex problems and one that is guaranteed to make progress on nonconvex ones.
Ghadimi and Lan (arXiv:1310.3787v1, 2013; Math. Program. 156, 2016) proposed a single AG scheme that does both. This mission formalizes their result for composite problems (§2.2, Theorem 2), where the smooth part is split into a possibly nonconvex piece with Lipschitz constant and a convex piece, and a non-smooth convex term is handled through a proximal step. The theorem shows that one aggressive step-size policy, the one that is optimal in the convex case, still drives a stationarity measure to zero when the smooth part is nonconvex.
Work in with the Euclidean norm. The problem (1.3) is
where:
The prox map (2.37) is
and the gradient mapping (2.38) is . With it reduces to when , and a small certifies approximate stationarity of (1.3). Assumption 2 asks for a constant with for all and ; it holds whenever is proper, closed, convex with bounded domain (Lemma 2).
Algorithm 2 takes step sizes with , for , , , starts from , and for sets
The weights are , (2.6).
Fix and assume, for ,
Let be an optimal solution of (1.3). Then
and, if ,
The goal is stated for general step sizes, so it does not hard-code the constants of a particular policy; Corollary 2 (the policy , , ) is a specialization left for follow-up work.
In the order of the proof: Lemma 1 (unrolling a -weighted recursion) and (2.16); the identity (2.42) linking to ; Lemma 5, the two-sided bound ; the descent bound (2.46) (already proved on the platform); the one-step inequalities (2.47)–(2.51); the summed inequality after (2.51); and the bounds (2.52)–(2.53).
The result. Theorem 2 gives a uniform treatment of convex and nonconvex composite problems. The same step sizes yield the optimal optimality gap when is affine, and a bound on the gradient mapping when is nonconvex. Under Corollary 2's policy that bound gives an iteration count of for , which depends on the Lipschitz constant of the convex part more mildly than projected gradient does. The proof template (a weighted Lyapunov argument in which the nonconvexity appears only through ) recurs in later stochastic and variance-reduced accelerated methods, including the paper's own Theorem 4.
Formalizing it. The result has been proved and refereed since 2016. As far as is known it has not been formalized in any proof assistant, and the platform holds no accelerated method with a nonconvex guarantee. A complete development would give a machine-checked proximal three-point inequality for convex functions on a convex domain, a checked composite AG analysis, and a checked version of Lemma 5. These are reusable pieces for any accelerated proximal method.
The obvious route is to copy the convex analysis of accelerated methods. It breaks at the convexity step: the bound needs convexity of , which is now available only up to -quadratic errors. Those errors involve and , which do not telescope and are not controlled by the usual potential; without some a priori bound on the iterates they can grow with . A formal proof also has to track the extended-valued carefully, since its convexity is used only at points of its domain, and the first iteration, where is not a prox output.
EuclideanSpace ℝ (Fin n). Smoothness of and is the platform's ConvexOptAlg.SmoothGD.IsBetaSmooth (differentiable with an explicit gradient map, Lipschitz gradient, nonnegative constant). and are written as and .K and its finite values X : E n → ℝ on K, with ConvexOn ℝ K X. Points outside K never enter: is compared only on K, is optimal over K, and (2.48)–(2.51) quantify over . A real-valued on all of is ruled out, because Assumption 2 is then unsatisfiable ( as ) and the goal would hold vacuously.P x y c with the hypothesis IsProxMap K X P: for every , P x y c ∈ K and it minimizes the prox objective over K. Without this minimizer hypothesis the three-point inequalities and the goal are false, so it cannot be dropped.Finset.inf' over . Conditions (2.9)–(2.10) are imposed for , and is written .Contributions welcome: proofs of any milestone. The three-point inequality (2.48)–(2.49) and Lemma 5 are self-contained and reusable. Also welcome: a proof of Lemma 2 (bounded domain implies Assumption 2), and Corollary 2 as a follow-up statement.
Many problems in machine learning and signal processing minimize a smooth loss plus a simple non-smooth regularizer: -regularized least squares, group-sparse regression, and constrained problems written with an indicator function. The standard algorithm for this composite form is the proximal-gradient method, a gradient step on the smooth part followed by a proximal step on the regularizer. Its classical linear convergence guarantee needs the smooth part to be strongly convex, a hypothesis that fails for -regularized least squares with fewer observations than variables and for most problems of interest without explicit regularization.
For smooth problems the Polyak–Łojasiewicz (PL) inequality gives a linear rate for gradient descent without convexity (Polyak 1963). Karimi, Nutini and Schmidt (arXiv:1608.04636, ECML PKDD 2016) propose a generalization to the composite setting, the proximal-PL inequality, under which the proximal-gradient method converges linearly with a one-paragraph proof. They show that it contains the PL case, the strongly convex case, and convex objectives with quadratic growth, and that it is equivalent to the Kurdyka–Łojasiewicz inequality (Bolte, Nguyen, Peypouquet, Suter 2017) and to the proximal error bound used earlier by Luo, Tseng and Drusvyatskiy–Lewis.
Timeline:
Let and consider problem (11),
The function is differentiable with an -Lipschitz gradient, with . The function is convex. has a minimizer , and .
For a base point and a parameter , the proximal model is
and the paper's measure of non-stationarity is
satisfies the proximal-PL inequality with modulus if
When is constant, and (12) is the PL inequality.
The proximal-gradient method with step size starts at an arbitrary and sets
The proximal residual function of Appendix E is .
Under the hypotheses above,
Theorem 5 gives a global linear rate for the proximal-gradient method under a hypothesis that does not require strong convexity, or convexity of . Through the classes of Section 4.1 it covers -regularized least squares, the composite strongly convex case, and convex composite problems with quadratic growth. The quantity also drives the analysis of proximal coordinate descent (Theorem 6, mission VI of this series), and Lemma 1 is what lets the sufficient conditions of Appendix F, which hold with for , be used in (12).
The results are proved in the paper; none of them has a machine-checked proof that this mission knows of. The work here is to formalize the known proofs, including the properties of and that the paper uses without stating: the minimum in (13) exists, and the value is finite.
The proof of Theorem 5 is short; the difficulty sits in the objects. is defined through a minimum over of a function involving a non-smooth convex , so every step that replaces the minimum by its value at a particular point needs the minimum to be finite and attained. The paper never states these facts, and they fail for an arbitrary : for and the model is unbounded below and the minimum in (13) does not exist. The monotonicity of in its second argument (Lemma 1) rests on the convexity inequality of , and Appendix F item 4 relies on the projection onto the solution set, whose existence depends on that set being closed, convex and non-empty.
EuclideanSpace ℝ (Fin d), is Mathlib's gradient f, and the Lipschitz hypothesis is written literally, ‖gradient f x - gradient f y‖ ≤ L * ‖x - y‖, with 0 < L.xstar with F xstar ≤ F y for all y; is f xstar + g xstar, never a free real.ConvexOn ℝ Set.univ g). Indicator functions of convex sets, which the paper lists among its examples, take the value and are outside this formalization; the formulas (13)–(15) subtract values of , which is undefined at .ShiOptRates.PolyakLojasiewicz (the paper's (3) multiplied by 2), and (2) is the published ShiOptRates.QuadUpper.Quadratic growth is stated with the distance to the solution set, , which equals for the projection the paper uses. Appendix F item 3 (Hoffman's bound with an unspecified constant ) and the equivalences of Appendix G are not included.
Contributions of every kind are welcome: proofs of the milestones, of the companion lemmas, and reusable facts about (finiteness, attainment, continuity in ) that other proximal-method missions can import.
Accelerated gradient (AG) methods go back to Nesterov (1983), who showed that a first-order method with a momentum-like extrapolation reaches an -optimal value of a smooth convex function in iterations, against for gradient descent, and that this rate is optimal among first-order methods. Many objectives met in practice (training losses, nonconvex penalties, problems with unknown convexity) are smooth but not convex. For those, gradient descent is known to drive the gradient norm to zero, with , while the classical AG method has no convergence guarantee at all.
Saeed Ghadimi and Guanghui Lan (arXiv:1310.3787v1, 2013; Mathematical Programming 156, 2016) modified the AG method with a third step size and proved that one algorithm handles both cases: on a smooth nonconvex problem it has the gradient-descent rate for , and when the problem turns out to be convex it keeps Nesterov's optimal rate for the optimality gap. This mission formalizes that result, Theorem 1 of the paper, and its proof path in §2.1.
Let be differentiable with Lipschitz gradient: there is with
and bounded from below, with (problem (1.1)). need not be convex.
Algorithm 1 (AG). The inputs are a starting point and step sizes , , with , for , and . Set and, for ,
One gradient is evaluated per iteration, at the middle point ; takes a long step and the aggregated point a short step . With the method reduces to gradient descent, with to a variant of Nesterov's method.
The weights are , (), and for a horizon and
Fix .
a) If for , then
b) If is convex with a minimizer , and for one has and , then
The theorem leaves the step-size policy open: any sequences meeting the conditions are covered, and the rates of Corollary 1 ( in part a, for the gap in part b) follow by substitution.
The milestones follow the proof in §2.1: the quadratic bound (2.1); Lemma 1, which unrolls the recursion ; the nonconvex chain (2.13), (2.15), the identity for , (2.16), (2.17), (2.18) and (2.19); and the convex chain (2.20)–(2.25).
The result. Theorem 1 is the first convergence guarantee for an accelerated gradient method on nonconvex smooth problems. It shows that acceleration costs nothing in the nonconvex case (the same rate for the squared gradient norm as gradient descent) while keeping the optimal gap when the function is convex, so a user need not know in advance which case holds. The same analysis is the template for the composite and stochastic results of the paper (Theorems 2–4) and for the later literature on accelerated methods for nonconvex optimization.
Formalizing it. The theorem is proved on paper; it is not known to have a machine-checked proof. The mission produces a Lean definition of the AG run with its three step sizes, a formal Lemma 1 (a reusable tool for any Nesterov-type analysis), and the two chains of estimates with all constants explicit. These pieces are reused by the composite and stochastic missions of the same paper.
The standard analysis of Nesterov's method is an estimate-sequence or potential argument that relies on convexity at every step: it bounds below by a linearization. Without convexity that lower bound fails, and the potential need not decrease. Part a) instead tracks the decrease of along the sequence, where gradients are evaluated at a different point ; the error this creates is governed by the gap , which accumulates all past gradients with weights . Controlling that accumulated term, and showing it is absorbed by the condition with depending on the horizon , is the delicate step. Part b) needs the monotonicity (2.10) to turn a weighted telescoping sum into a single initial-distance term.
EuclideanSpace ℝ (Fin n). The gradient is an explicit map g, tied to by the published predicate ConvexOptAlg.SmoothGD.IsBetaSmooth Ψ g LΨ (differentiable with gradient , and (1.2)); as in (1.2). The quadratic bound (2.1) is the published, proved ConvexOptAlg.SmoothGD.lemma_3_4.agRun, with xSeq, xagSeq, xmdSeq), computed by (2.2)–(2.4) from ; indices are 1-based as in the paper. , so . is C LΨ α β lam N k and depends on .BddBelow (Set.range Ψ) and is ⨅ x, Ψ x. The minimum over is Finset.inf' over Finset.Icc 1 N with . Convexity is ConvexOn ℝ Set.univ Ψ; is any global minimizer.Welcome contributions: proofs of Lemma 1 and of the algebraic milestones (the identity before (2.16), (2.16), (2.17), (2.22), (2.25)), which are independent of ; then the descent chains; then Theorem 1.