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?
The index theorem says that among several Markov reward processes, of which one may be advanced at each decision time, the right one to advance is the one of greatest Gittins index. Chapter 4 of Gittins, Glazebrook and Weber, Multi-armed Bandit Allocation Indices (2nd ed., doi:10.1002/9780470980033), asks how far this extends when the constituents are not reward processes but decision processes, each with its own controls: a research project that can be run in several ways, a job that can be processed at different speeds, a sampling process that may be stopped and exploited. A family of such superprocesses requires two choices at every decision time, which superprocess to continue and with which control, and an index policy in the sense of Chapter 2 need not be optimal (Example 4.1). Whittle (1980) identified the condition under which it is: Condition D, that when a superprocess is played against a standard bandit process paying a constant rent, the control one should apply to it does not depend on the rent. Under that condition the index theorem survives (Theorem 4.3), the index is characterized (Note 4.2), stoppable bandit processes with improving stopping options satisfy the condition (Lemma 4.4), and the chapter adds two results about indices themselves: any index that works for all bandit processes is a strictly increasing function of the Gittins index (Theorem 4.8), and a policy that is within of the index policy loses at most (Theorem 4.18).
A decision process on a countable state space has in each state a nonempty finite set of controls; applying yields the reward and moves the state by . Adding the freeze control, which leaves the state unchanged and yields nothing, makes a superprocess . Operating under a feasible deterministic stationary Markov policy (that is, ) gives an ordinary bandit process , and the superprocess index is
with the Gittins index of the Bandit Algorithms model. A simple family of alternative superprocesses (SFAS) is superprocesses on a common ; at each decision time exactly one is continued, with a control from its control set, the others being frozen, and rewards are discounted by . A policy is a Markov kernel per decision time from the history to the pair (superprocess, control); it is optimal if it is feasible and attains the supremum of the discounted payoff over feasible policies from every initial state-vector, and it is an index policy if it always continues a superprocess and control of maximal .
Condition D. Let be a standard bandit process with parameter (one state, reward ). satisfies Condition D if there is a function such that, for every and for which it is optimal in the family to select in state , it is optimal to apply the control . A stoppable bandit process is a bandit process with a stop control that makes it behave as a standard bandit process with parameter ; its stopping option is improving if is almost surely nondecreasing in process time.
For a decision process with bounded rewards and a Condition-D control , every index policy with respect to that applies to the superprocess it continues is optimal for the family of superprocesses:
Note 4.2 (under Condition D, is selected in iff , and at a control is optimal iff ; the printed equivalence fails for ); Lemma 4.4 (Condition D for stoppable bandit processes with improving stopping options); Theorem 4.8 (an index for the bandit processes with discount factor is strictly increasing in ); Theorem 4.18 (the -index bound, for the discrete-time index).
Theorem 4.3 is the widest form in which the index theorem holds without further structure, and Condition D is exactly the right hypothesis: it says the superprocess has a canonical control, and once it does the family reduces to a family of bandit processes and the prevailing-charge argument goes through. Lemma 4.4 gives the model where the condition is known to hold, a research project that may be exploited at any time; the buyer's problem of Bergman and Bather is the case where it fails. Theorem 4.8 explains why every index theorem in the book is about the Gittins index: any function that orders bandit processes optimally must order them as does. Theorem 4.18 is the quantitative version of the index theorem that heuristics and computations rely on.
Nothing here is machine-checked. The mission builds the first controlled multi-armed model on the platform, a run law for families of decision processes with an explicit feasibility constraint, and states Whittle's condition as a property of the two-member family, which is how the literature uses it. Theorems 4.8 and 4.18 are statements about the existing Bandit Algorithms model and are usable by any later work on that model.
The obvious attack on Theorem 4.3, "replace each superprocess by the bandit process for its Condition-D policy and apply the index theorem", is the second half of the book's proof; the first half is to show that an optimal policy never gains by applying a control other than to a superprocess it continues, and that uses the prevailing-stake accounting of §4.3 with the other superprocesses treated as one bandit process, plus the observation that the class of policies deviating at most times is -exhaustive. Both halves require the whole run law of the family to be related to the run laws of its constituents, which is where a formalization spends its effort. Note 4.2 is short on the page but needs the optimal-stopping characterization of Chapter 2 for the bandit process under charge . Theorem 4.8 is elementary given the value of under a freezing rule, , but that identity is itself a computation on the run law. Theorem 4.18 has no proof in the book (Glazebrook 1982c); the natural route is the prevailing-charge upper bound with the charges perturbed by .
Decision processes carry their control sets as finsets with a nonemptiness proof and their kernels as Markov kernels; the state space is countable with measurable singletons (so stationary kernels and control-dependent maps are measurable without side conditions) and the control type is finite with measurable singletons. The family's run law is built decision time by decision time as the Bandit Algorithms model builds markovBanditMeasure, with the policy's kernel producing the pair (superprocess, control). Feasibility is an almost-sure condition on the policy kernel, and optimality is the book's: feasible, and the supremum from every initial state-vector. The superprocess index is a real supremum over feasible stationary policies with , bounded by the reward bound and nonempty for ; for an unavailable it is a default value that no index policy consults. Condition D is stated on the family on , where the standard state has every control available, all equivalent. A stoppable bandit process is the decision process with control type Bool. Theorem 4.8 quantifies over index functions defined on every measurable state space and takes as hypothesis only what its proof uses, optimality of -index policies for the families . Theorem 4.18 is on the -armed Bandit Algorithms model with and the bound : the book's is in continuous-time index units, times the discrete-time index used here, and read with the discrete index it is false for . Theorem 4.3's index policy applies the Condition-D control to the superprocess it continues, as the book's proof does; an index policy that breaks ties among controls otherwise need not be optimal.
Trivializing readings are excluded: index policies must be feasible, optimality is required from every initial state, and Condition D is a statement about optimal policies of a genuine two-member family, not about a chosen policy. Welcome contributions: the relation between the family's run law and the constituents' chain laws, the freezing-rule value identity behind Theorem 4.8, and the prevailing-stake accounting of §4.3.
Chapter 3 of Gittins, Glazebrook and Weber, Multi-armed Bandit Allocation Indices (2nd ed., doi:10.1002/9780470980033), asks which of the assumptions behind the index theorem can be dropped and which cannot, using the simplest bandit processes there are: jobs, which pay a single reward when they complete. Along the way it settles three questions that matter on their own. When identical machines run in parallel, which schedule of deterministic jobs minimizes the total completion time (Baker's theorem), and what does the equal-ratio case look like (Theorem 3.3)? When an object is hidden in one of several boxes and each search costs money and may fail, in what order should the boxes be searched (Blackwell's search-index theorem, Theorem 3.6)? And when two bandit processes discount at different rates, is there still an index policy (Nash's Theorem 3.4)? The search theorem is the chapter's example of what the index machinery yields once undiscounted criteria are admitted through the limit ; the scheduling results are the source of the counterexamples that show a second machine breaks the index structure.
Jobs on parallel machines. There are jobs with service times and weights , and identical machines. A schedule assigns each job a machine and a position in that machine's processing order; each machine processes its jobs consecutively. The completion time of a job is the total service time of the jobs on its machine up to and including it; the flow time is and the weighted flow time . The load of a machine is the total service time assigned to it, and is its excess over the average . The SPT list schedule sorts the jobs by increasing service time and deals them out cyclically to the machines. The level of a job is its position counted from the end of its machine's schedule.
The search problem (Problem 3). A stationary object is hidden in one of boxes, in box with probability . A search of box costs and finds the object with probability if it is there. A search policy is a sequence of boxes; after unsuccessful searches of box the posterior probability that the object is there is proportional to , and the search index of the box is , the current probability of finding the object per unit cost. The expected cost of a policy is .
Two discount factors. Bandit process (state space , kernel , reward ) discounts at rate and at rate ; a reward obtained at time is worth or times its face value according to which process produced it. The cross indices are and with the roles exchanged: each is computed from one process's stopping times but with the other's discount factor in the denominator. The book prints the denominator as and compares with at every time; both are corrected here (see the Theorem 3.4 item), since the printed rule is not optimal. The family is the two-armed Markov bandit of the Bandit Algorithms model on the disjoint union .
For prior probabilities summing to one, detection probabilities and costs , a search policy is optimal if and only if at every step it searches a box of maximal current index :
Theorem 3.3, as the identity when ; Theorem 3.4 in discrete time and corrected, that a policy selecting, at time , when and when attains the supremum of the bandit-dependently discounted payoff; Theorem 3.7, that SPT minimizes the flow time on machines and that the optimal schedules are exactly those placing the -th block of longest jobs at level from the end, for some order of the equal jobs.
Theorem 3.6 is the classical solution of the discrete search problem (Blackwell, reported by Matula 1964; Kadane 1969): the greedy rule in probability-per-cost is optimal, and every optimal policy is of that form. The book derives it from the index theorem through an auxiliary family of bandit processes (Problem 3A) and the undiscounted limit (Corollary 3.5), which is why it sits in this chapter; as a statement it is elementary and self-contained, and it is the template for the tax problems and Klimov's model of Chapter 4. Theorem 3.7 and Theorem 3.3 are the positive results about parallel machines that survive the loss of the index structure; Theorem 3.4 shows the index theorem's shape persisting under bandit-dependent discounting, with two twists: each index depends on the other process's discount factor, which is exactly why it does not extend to three processes, and the comparison at time weighs the indices by and , so the rule is not stationary in the states. The printed statement misses the second twist and misnormalizes the first; two one-state bandits paying () and () are best played and then forever, which no stationary rule does.
None of these is machine-checked. Formalizing them gives the platform an optimality theorem for an infinite-horizon search process with an explicit index characterization in both directions, the standard parallel-machine flow-time results with a precise uniqueness clause, and a first statement on the Bandit Algorithms two-armed model with unequal discounting.
For Theorem 3.6 the obvious route, comparing two adjacent searches, gives only that interchanging a pair in the wrong index order lowers the cost; turning that into optimality over all infinite sequences needs that an optimal policy exists (costs are bounded below by zero and the index policy has finite cost), that a policy neglecting a box of positive prior has infinite cost, and that any first deviation from the index rule can be improved by moving a later search forward, which requires tracking how the not-found probability changes along the whole tail. The converse direction is the same interchange run backwards, and the tie case must be handled so that the equivalence is exact. Theorem 3.7's first part follows from writing the flow time as with the level and applying a rearrangement inequality over the multiset of levels, but the multiset of levels itself depends on how many jobs each machine gets, so balancing the machine counts is part of the argument; the uniqueness clause needs both that the multiset is forced and that the pairing of levels with service times is forced by strict monotonicity. Theorem 3.4 is the hardest: the book's proof changes the time scale of each process so that the two share a discount factor, which produces a semi-Markov family, and applies the index theorem there; in discrete time on the Markov model one needs either a discrete analogue of that argument or a direct prevailing-charge proof with two charge scales.
Schedules are assignments of machines and positions with distinct positions on a machine, without idling; the flow-time quantities are finite sums over Fin n. The SPT schedule is defined by the ascending rank of a job (ties broken by index) and carries its own injectivity proof. The search cost is a series in of nonnegative terms, so no summability hypothesis is needed and "infinite cost" is literal; the index is stated unnormalized, , which orders the boxes exactly as the posterior index does. The two-discount family uses the platform's MarkovBanditPolicy 2 (S_A ⊕ S_B) and markovBanditMeasure with the kernel that moves an -state by and a -state by ; the payoff is the round-by-round series , absolutely summable for bounded rewards, and the policy condition is imposed at histories whose current states have the right types (all reachable histories do). Hypotheses: , service times positive; , , , ; countable state spaces, bounded rewards, .
Trivializing readings are excluded: the search "iff" is over all sequences, not a finite horizon; the uniqueness clause is stated in full, with ties resolved by any ranking of the equal jobs; the cross indices are suprema over positive stopping times (denominators at least one), and the two-discount rule weighs the indices by , . Welcome contributions: the rearrangement and level-count lemmas for schedules, the interchange lemma for the search cost, and a discrete prevailing-charge argument for Theorem 3.4.
Every data-driven decision problem faces the same trap. A decision-maker estimates a risk functional from a nominal distribution built from training samples, then optimizes a loss function against instead of the unknown true distribution . Because the optimizer adapts to the noise in , the in-sample risk of the optimizer systematically understates its true, out-of-sample risk — a phenomenon Smith and Winkler named the optimizer's curse (Smith & Winkler, Management Science, 2006). The remedy explored here is to hedge against a whole neighborhood of plausible distributions around , rather than trusting the point estimate. Kuhn, Mohajerin Esfahani, Nguyen and Shafieezadeh-Abadeh's INFORMS TutORials chapter (2019) develops this neighborhood using the Wasserstein distance, and the present mission formalizes its foundational duality theory: the machinery every later result in the chapter (finite-sample guarantees, elliptical tractability, regularization) builds on.
Fix a norm on a finite-dimensional real vector space (representing ). For , the type- Wasserstein distance between two Borel probability measures on is
where is the set of couplings of and — joint probability measures on whose marginals are and . The optimal can be read as a transportation plan moving one pile of dirt () into another () at minimum cost, which is why is also called the earth mover's distance; the underlying linear program was formalized by Kantorovich (1942) after Monge's 1781 original.
Given training samples , the empirical distribution is . Centered at , the Wasserstein ambiguity set of radius is
where is a closed set known to contain the support of the true distribution. The worst-case risk of a loss function is
and minimizing it over a class of admissible loss functions is a distributionally robust optimization problem. measures the estimation error one insures against; a larger ambiguity set gives a more conservative (and more expensive) guarantee.
This is the Lagrangian dual of the worst-case risk evaluation problem, with the multiplier of the Wasserstein constraint : it converts a supremum over an infinite-dimensional space of measures into a one-dimensional minimization of the Moreau-Yosida regularization . Every tractability result later in the chapter (finite convex reformulations, SDP relaxations) specializes this duality by choosing a loss class for which is computable.
These identify as a linear program's strong dual (Theorem 1) and, for , specialize it to the Kantorovich-Rubinstein form (Theorem 2), which is what lets the worst-case-risk analysis reason about Lipschitz loss functions directly.
These are the tractable, easily-computed bracket that Theorems 7 and 10 later show is tight in important special cases.
Theorem 5's inequality becomes exact under convexity — the cleanest closing corollary of the duality theory, obtained from Theorem 7 by evaluating the Moreau-Yosida regularization of a convex function explicitly.
Theorem 7 is the hinge on which the entire computational program of Wasserstein distributionally robust optimization turns: every tractable reformulation in the source chapter (piecewise-concave losses via conic duality, quadratic losses via semidefinite programming, the shrinkage-estimator connection) is obtained by substituting a specific loss class into the right-hand side of Theorem 7 and showing the resulting Moreau-Yosida regularization is computable. Kuhn et al. themselves derive it as a corollary of Blanchet & Murthy (2019) and Gao & Kleywegt (2016) for the empirical case, generalized to Polish spaces by Blanchet & Murthy and Gao & Kleywegt independently — the paper cites [12] and [37] for the general statement. Formalizing it is what makes every later, more computational result in the chapter — the ones a solver is more likely to reach for next — rest on a mechanically verified foundation rather than a citation chain.
Status. The mathematical result is well established (multiple independent published proofs cited above); nothing here is open research. What this mission contributes is the first machine-checked formal statement of the duality theorem and its supporting dual representations (Theorems 1, 2, 5, 6, 10) on the Prove2Me platform — none of Wp's dual representation, the Wasserstein ambiguity set, or the worst-case risk functional exist there prior to this mission (see Formalization scope).
The obvious proof strategy — write down the Lagrangian of the semi-infinite program (6), swap the order of the outer supremum over and the inner minimization over the multiplier , and invoke ordinary Lagrangian strong duality — fails because (6) is an infinite- dimensional linear program over measures, not a finite convex program: there is no compact feasible set or Slater point in a form that ordinary finite-dimensional duality applies to directly. The actual proof goes through the dual representation of the Wasserstein distance itself (Theorem 1, which is why it is a prerequisite milestone), reformulating the constraint via its own dual variables and swapping the resulting sup-inf using minimax theorems for semi-infinite programs, not ordinary Lagrangian duality for finite programs.
is a generic finite-dimensional real normed space (NormedAddCommGroup, NormedSpace ℝ,
Borel-measurable), representing with the paper's arbitrary fixed norm as a
parameter rather than fixing the Euclidean norm. A coupling is formalized directly via
MeasureTheory.Measure.map: π.map Prod.fst = Q ∧ π.map Prod.snd = Q'. Constrained
infima/suprema (over couplings, over the ambiguity set, over Lipschitz test functions, over
perturbation matrices) use Mathlib's guarded-binder idiom ⨅ x (_ : P x), f x, which
correctly returns (resp. ) outside the feasible set rather than a finite junk
value.
Two deliberate, disclosed conventions keep the extremal-value definitions faithful without
extended-real integration machinery, both recorded in MODERATION_NOTES.md:
worstCaseRisk and the dual representations (Theorems 1, 2) are valued in EReal,
not ℝ, so an unbounded supremum is recorded as rather than collapsed to
Mathlib's real-valued junk value 0 on an unbounded family.BoundedContinuousFunction E ℝ), narrower than the paper's
general upper-semicontinuous, -integrable loss class (Assumption
1). This keeps a finite real
number for every nonempty , so the right-hand side's Bochner integral is well-posed;
the milestones (Theorems 5, 6, 10) keep the more general real-valued (not necessarily
bounded) loss class, since their statements do not require evaluating a pointwise
supremum over .Ξ is required closed in Theorems 5, 6 and 7, matching the paper's own standing
assumption (p. 6: "we let be a closed set that is known to
contain the support of ") for the whole worst-case-risk framework, which is used
silently in the paper wherever a theorem takes as an argument but was not carried
into these theorems' own hypothesis lists in an earlier draft.ambiguitySet uses for
), which the paper's framework presupposes for the nominal
distribution throughout §2. Combined with bounded, this makes bounded
on the full-measure set (above by unconditionally, below by
itself via for ), which is what makes the right-hand side's integral
genuinely well-posed rather than liable to Mathlib's non-integrable junk value .There is no trivializing formalization risk from a vacuous hypothesis: Ξ.Nonempty and
0 < N are both required exactly where the paper's own indexing and support assumptions
require them, and every extremal value uses the extended-real convention above rather than a
convention that would make an inequality vacuously true.
No definition in this mission exists on the platform prior to this series (GET /theorems?q=Wasserstein, q=Kantorovich, q=optimal transport, q=coupling return only
unrelated discrete/finite-type constructions); all seven definitions and six theorems are
drafted fresh. WassersteinDRO.Duality.wassersteinDistance, .ambiguitySet and
.worstCaseRisk are the substrate every later mission in this five-part series (Gelbrich
tractability, finite-sample guarantees, regularization, shrinkage estimation) either imports
directly or redefines locally per the series' reuse rule.
An initial value problem , , is the standard way a law of motion, a growth model or a circuit equation is written down, and only a small minority of such problems can be integrated in closed form. Single-step methods advance the solution by small increments: Euler's method takes the tangent line at the current point, and the higher-order Runge-Kutta schemes refine the same idea. What justifies them is a pair of theorems: that the problem has a unique solution at all, and that the computed polygon approaches that solution as the step size decreases.
This mission is the seventh in a series formalizing the lecture notes Métodos Numéricos by Sergio Roberto de Freitas (UFMS, 2000). It covers Chapter 9, Métodos Numéricos para EDO's, up to the convergence of Euler's method.
Consider the initial value problem
with defined on a rectangle .
Picard's method replaces the differential equation by the integral equation and iterates it:
With , and , the source states the bound on , where is the exact solution.
Euler's method with step produces , . Its local error is per step and its global error .
The goal theorem is the global error statement: for an initial value problem whose exact solution is twice continuously differentiable on and whose right-hand side is Lipschitz in there, there is a constant such that for every step size and every grid point ,
This is the precise form of the source's assertion .
The milestones are the results the chapter states on the way: local existence and uniqueness for the initial value problem under a Lipschitz condition in (Teorema 9.4.1), the Picard error bound, the convergence of the Picard iterates to the solution, and the one-step Taylor identity behind Euler's method.
The global error bound is what makes Euler's method a method rather than a heuristic: it converts an arbitrary choice of step size into a guaranteed accuracy, and it exhibits the characteristic loss of one order between the local error and the global error that recurs for every single-step scheme. The existence and uniqueness theorem is the prerequisite for all of it — without uniqueness there is no well-defined object for the numerical solution to approximate — and the Picard iteration is both the constructive proof of that theorem and a method in its own right.
The global error proof has to handle the interaction of two error sources: the local truncation error at each step and the amplification of previous errors by the Lipschitz constant, which gives the discrete Gronwall recursion . Carrying that recursion to the closed-form bound, and doing it uniformly in , is the core of the mission. The Picard bound requires the iterates to remain inside the rectangle so that the hypotheses on continue to apply — that is what the choice is for — and an induction on with the factorial denominator.
The unknown is a real function of a real variable and is a function of two real variables. A solution is a function satisfying and having derivative at every point of the relevant interval. The Lipschitz condition in the second variable is stated explicitly, , in place of the source's hypothesis that is bounded; for the global-error goal it is assumed for all real and all in the interval, and in the Picard milestones only inside the rectangle. Uniqueness is stated as agreement of any two solutions on the interval, not as uniqueness of a function on all of , since a solution is unconstrained outside the interval. Euler's iterates and the Picard iterates are explicit recursive definitions; the Picard integral is the interval integral, which is total, so no integrability side condition appears in the definition. The constant in the goal is asserted to exist and to be positive, uniformly over step sizes in ; the restriction merely normalizes the range of steps considered.
Chapter 2's tail bounds mostly rest on moment-generating-function control, obtained either directly (sub-Gaussianity) or through explicit combinatorial arguments (Hoeffding, bounded differences). The entropic method offers a different, more structural route: bound a specific information-theoretic quantity — the -entropy of — and convert that bound mechanically into a tail bound via a short ODE argument (the Herbst argument). This method's real payoff appears once it is combined with the tensorization property of entropy across independent coordinates, which is what lets it handle Lipschitz functions of many independent variables — including cases, such as separately convex functions, that elude the purely martingale-based techniques of Chapter 2. This mission formalizes the entropic method's two foundational entropy-to-tail conversions and its central Lipschitz-concentration application, following Wainwright, High-Dimensional Statistics: A Non-Asymptotic Viewpoint (Cambridge University Press, 2019), Chapter 3.
For (), , the -entropy of a nonnegative random variable is (Eqs. (3.1)-(3.2)). Writing for the moment generating function of , the entropy of has the explicit form (Eq. (3.3)).
A function is separately convex if, for each coordinate , the univariate function obtained by fixing every coordinate but the -th is convex — strictly weaker than joint convexity of itself. is -Lipschitz with respect to the Euclidean norm if for all .
Let be independent, each supported on , and separately convex and -Lipschitz. Then for all ,
If for all ( or ), then for all — the basic entropy-to-sub-Gaussian-tail conversion.
The sub-exponential analogue: if for , then on the same range.
Propositions 3.2 and 3.3 are the two basic entropy-to-tail conversions the entire chapter's entropic method rests on — every subsequent Lipschitz-concentration result in the chapter (including Theorem 3.4 and the more advanced Theorem 3.24) is obtained by first establishing an entropy bound of one of these two forms and then invoking the corresponding proposition. Theorem 3.4 is itself the direct analogue, for independent bounded variables, of Chapter 2's Gaussian Lipschitz concentration (Theorem 2.26) — but crucially requires the extra hypothesis of separate convexity, which the Gaussian case does not need and which cannot be dropped in general.
Formalizing it. No faithful prior art exists on the platform. The one candidate flagged in
BRIEF.md, Talagrand.lipschitz_concentration, was read in full: it is a weighted-Hamming-
distance concentration bound for functions on a finite-alphabet product space Fin n → α,
proved via Talagrand's convex-distance method — a different underlying space (finite alphabet
vs. real-valued bounded coordinates) and a different Lipschitz norm (weighted Hamming vs.
Euclidean) from Theorem 3.4, and not reused here. A search for "log-Sobolev" and "Herbst" turned
up bousquet_herbst_cgf_le_phi_via_herbst/bousquet_herbst_cgf_le_phi_double_integration: these
are abstract calculus lemmas about a generic function satisfying an ODE-type growth
condition (), concluding — a genuinely different statement
shape from Proposition 3.2/3.3's entropy-to-CGF conversions (which conclude a quadratic, not
exponential, bound on ), and not a faithful match. All
three theorems here are drafted as open goals (:= by sorry).
The naive approach to Theorem 3.4 — try to adapt the bounded-differences (martingale) method of Chapter 2 directly — fails, because the bounded-differences method needs to have small coordinatewise oscillation in an absolute sense, while separate convexity alone gives no such uniform bound (a separately convex function can vary arbitrarily fast within the interior of its domain, only its slope is controlled by the Lipschitz condition). The entropic method sidesteps this by working with the -entropy of directly: entropy has a tensorization property across independent coordinates (not itself part of this mission, but what the entropic method's proof of Theorem 3.4 uses) that reduces a multivariate entropy bound to a sum of "one coordinate at a time" contributions, each of which convexity and the Lipschitz condition jointly control — a route with no analogue in the bounded-differences approach.
Separate convexity and Euclidean-Lipschitzness are both restated locally in this chapter's own
sub-namespace (HighDimStat.Concentration), per this book series' rule against importing
another chapter's draft definitions, even though Chapter 2 already defines an
IsLLipschitz for the same Euclidean condition. φ_X'(\lambda)$ (Proposition 3.3) is realized via Mathlib's deriv, a legitimate way to state a hypothesis on a derivative without separately proving differentiability, appropriate at the draft-statement stage. Explicit Integrable`
hypotheses guard the Bochner integral's junk value on non-integrable functions throughout (trap
2), not literal in the book's own propositions but implied by what "the entropy exists" (an explicit qualifier the book itself makes when introducing Eq. (3.2)) means.
Goal substitution, disclosed. BRIEF.md recommends Theorem 3.24 (the two-sided, jointly
convex analogue) as the primary goal, but explicitly names Theorem 3.4 as a fallback "if 3.24's
dependence on the unnumbered transportation-cost inequality (Eq. 3.73, attributed to Samson)
proves too heavy to state faithfully in the time available." Theorem 3.24's proof route depends
on Theorem 3.19 (a general "transportation cost implies concentration" result for an abstract
metric measure space, itself needing a from-scratch formalization of the transportation-cost
inequality (3.58) and the concentration function ) plus the
unproven-in-chapter Eq. (3.73). Building this full stack faithfully was judged to exceed this
chunk's time budget; Theorem 3.4 is drafted instead, using this mission's own budget on
Propositions 3.2 and 3.3 (the two most load-bearing entropy-to-tail conversions of the chapter)
rather than the heavier transportation-cost machinery. Theorem 3.19, Theorem 3.24, and Eq.
(3.73) are all out of scope for this mission and named here as natural follow-on work.
Many estimation problems are naturally posed over matrices rather than vectors: recommender
systems (Netflix-style matrix completion), multivariate regression with correlated responses,
vector autoregressive time series, and phase retrieval all reduce to estimating an unknown
matrix that is low-rank, or well approximated by one. A rank constraint alone makes
the natural least-squares estimator non-convex and generally intractable; replacing it with the
nuclear norm — the sum of the matrix's singular values, the tightest convex surrogate for rank
— yields a tractable semidefinite program. Wainwright's High-Dimensional Statistics (2019),
Chapter 10, shows that this substitution costs nothing statistically: nuclear-norm-regularized
least squares achieves error rates matching what one could hope for even knowing the rank in
advance, by specializing Chapter 9's general decomposable-regularizer framework (mission
09-decomposability) directly to the nuclear norm.
For matrices , the trace inner product is (Eq. 10.1), inducing the Frobenius norm . Given design matrices and responses , the observation operator and its adjoint (Eqs. 10.2-10.3) are the matrix analogs of a vector design matrix and its transpose. The nuclear norm (Eq. 10.5) — the sum of singular values — is a decomposable regularizer (in the sense of Chapter 9) with respect to the subspace pair spanned by the top singular vectors of any target matrix, and its dual norm (Table 9.1) is the -operator (spectral) norm . The estimator under study is nuclear-norm-regularized least squares,
with user-chosen.
Suppose satisfies the restricted strong convexity condition (10.17), for all , with , . Conditioned on the good event , any optimal satisfies, for any with ,
Under the alternative -curvature condition (10.20) (a curvature bound on the gradient map rather than the Taylor error), with : conditioned on , any optimal satisfies — an operator-norm bound the book notes is, in conjunction with the cone-like constraint (10.15), strictly stronger than Proposition 10.6's Frobenius-norm bound.
Proposition 10.6 is this chapter's direct payoff from Chapter 9's general machinery: it shows
that the deterministic backbone of the Lasso's guarantee (mission 07-sparse-linear) extends
essentially verbatim to the matrix setting, with the sparsity level replaced by the target
rank and the ambient dimension replaced by — exactly the "degrees of freedom"
scaling one would predict by counting the parameters needed to specify a rank- matrix. Every
one of the chapter's later corollaries (matrix compressed sensing, multivariate regression,
matrix completion) is obtained by verifying the restricted strong convexity condition (10.17)
holds with high probability for a specific random design, then reading the rate directly off
Proposition 10.6 — the same two-step recipe Chapter 9's own Theorem 9.19 established abstractly.
Proposition 10.7's operator-norm bound is what subsequently controls the individual singular
values of the estimation error, needed for exact-rank-recovery guarantees.
Both results are direct specializations of Chapter 9's general oracle inequalities (Theorem
9.19 and Theorem 9.24 respectively) to the nuclear norm as regularizer and the Frobenius/operator
norm pair, so their formalization difficulty lies almost entirely in getting the matrix-specific
objects right rather than in new proof machinery: the nuclear norm requires an actual notion of
singular values (realized via the eigenvalues of the Gram matrix , using
Mathlib's Hermitian-matrix spectral theorem), the operator norm requires the correct rectangular
generalization of the symmetric-matrix Rayleigh-quotient characterization used in mission
08-pca, and the restricted-strong-convexity and curvature conditions must be instantiated
against the correctly-adjointed observation operator . A further subtlety is
keeping Proposition 10.6's Frobenius-norm conclusion and Proposition 10.7's operator-norm
conclusion cleanly distinct — the book itself warns against conflating the norms used across
different chapters of Part II (the vector -norm of chunks 07-sparse-linear/08-pca
versus the matrix Frobenius and operator norms here).
Scope cut, disclosed here and in STATUS.md. BRIEF.md recommends Corollary 10.10 (the
sample-complexity bound for the -Gaussian random matrix ensemble) as the goal theorem.
Corollary 10.10 is a genuinely probabilistic statement — it asserts a bound holding "with
probability at least " over i.i.d. draws of design matrices from a
-Gaussian ensemble (Theorem 10.8's own high-probability restricted-strong-convexity
certification for that ensemble) — and formalizing it faithfully would require a genuine
multivariate-Gaussian-measure infrastructure on matrix space (a probability space, an i.i.d.
sequence of -covariance-structured Gaussian matrices, and Mathlib's measure-theoretic
probability API) that is disproportionate to this mission's time budget, and orthogonal to what
Chapter 10 itself contributes (the chapter's own text stresses that Propositions 10.6 and 10.7
are the chapter's deterministic core, with probability entering only in Section 10.3's
ensemble-specific certification — precisely mirroring chunk 09-decomposability's own
"Theorem 9.19 is actually a deterministic result" framing). This mission instead takes
Proposition 10.6 as its goal — explicitly named in BRIEF.md's own candidate list as "the
nuclear-norm oracle inequality, an explicit corollary of Theorem 9.19" — the natural, tractable,
still highly citable deterministic title result of Section 10.2, together with its companion
Proposition 10.7. Theorem 10.8 (the -Gaussian ensemble's RSC certification), Corollary
10.9 (noiseless exact recovery) and Corollary 10.10 itself are left for a future mission with a
dedicated probability-theory budget. The cone-like constraint (Eq. 10.15) — whose own faithful
statement requires the same explicit subspace-pair machinery
() chunk 09-decomposability built for the
general theory — is similarly left out, since Propositions 10.6 and 10.7's own numbered
statements never expose these subspaces directly (only their proofs do, via instantiating
Theorem 9.19/9.24). singularValues and nuclearNorm are noncomputable, defined via
Mathlib's Hermitian-matrix eigenvalue spectral theorem; c0 ≥ 0 and λn > 0 are made explicit,
matching this book's running conventions for RSC tolerance constants and regularization weights
(see MODERATION_NOTES.md).
Linear methods like SVMs work only when the classes are linearly separable, but most real data is not. Chapter 6 shows how to get non-linear decision boundaries for free: replace the input space's inner product with a kernel that implicitly computes an inner product in a (possibly very high- or infinite-dimensional) feature space, without ever explicitly computing the feature mapping. This works for any positive definite symmetric (PDS) kernel — and the chapter's central theorem shows that such a kernel always induces a genuine Hilbert space (the reproducing kernel Hilbert space, RKHS) in which the kernel is literally an inner product. The chapter's capstone, the representer theorem, then shows that a broad class of optimization problems over this (possibly infinite-dimensional) Hilbert space always has a solution expressible as a finite linear combination of kernel evaluations at the training points — turning an infinite-dimensional problem into a finite, -dimensional one.
A kernel is PDS (Definition 6.3) if for every finite sample , the Gram matrix is symmetric positive semidefinite. Theorem 6.8 shows every PDS kernel is an inner product in some Hilbert space (the RKHS), which further has the reproducing property for every — evaluating at a point is itself an inner product with the kernel section at that point. Theorem 6.10 shows PDS kernels are closed under sum, product, tensor product, pointwise limit, and power-series composition, letting complex kernels (Gaussian, and many others) be built from simple ones (polynomial kernels) without re-verifying positive-semidefiniteness from scratch. Section 6.3's representer theorem (Theorem 6.11) then considers minimizing, over , an objective that depends on only through its norm and its values at fixed points.
Theorem 6.8 (RKHS existence, milestone). For a PDS kernel , there exist a Hilbert space and with , and has the reproducing property for all , .
Theorem 6.10 (closure properties, milestone). PDS kernels are closed under sum, product, tensor product, pointwise limit, and power-series composition with non-negative coefficients.
Theorem 6.11 — the mission's goal. For any non-decreasing and any loss , admits a solution ; if is increasing, every solution has this form.
Theorem 6.11 is the chapter's payoff and one of the most widely used structural results in
kernel methods: it explains, in one general statement covering SVMs, kernel ridge regression,
Gaussian process MAP estimation and many other algorithms simultaneously, why the dual
(finite, -coefficient) formulation always suffices — the RKHS's infinite dimensionality
never has to be confronted directly. Theorem 6.8 is the structural fact the whole chapter (and
every later kernelized algorithm in the book, chapters 9-11, 15) depends on: without it, "PDS
kernel" would be a purely combinatorial condition on Gram matrices with no guarantee it
corresponds to any actual inner product. No prior art on the Prove2Me platform is faithful to
any of this chapter's content: GET /theorems?q=Representer theorem and q=reproducing kernel return no faithful match (one unrelated hit concerns a Gaussian-measure reproducing
kernel in a different, probabilistic context, not this chapter's PDS-kernel/RKHS
construction). All six items are drafted fresh.
Theorem 6.8's proof is a genuine construction: define as finite linear combinations of kernel sections , define an inner product on using itself, verify it is well-defined (independent of the representation), positive semidefinite (via the PDS hypothesis), and — via the Cauchy-Schwarz-for-PDS-kernels lemma (Lemma 6.7) — actually positive definite, then complete to a genuine Hilbert space in which it is dense, and finally extend the reproducing property from the dense subspace to all of by a continuity argument. This is substantial analysis, not a restatement. Theorem 6.11's proof uses the orthogonal decomposition (where ) and the reproducing property to show the orthogonal component never helps and, when is strictly increasing, strictly hurts — a short argument, but one that depends essentially on Theorem 6.8's reproducing property holding for the specific constructed, not just any Hilbert space with the kernel as its inner product.
IsPDS uses the book's own second SPSD characterization (c^T K c ≥ 0 for every finite sample
and coefficient vector c) rather than the non-negative-eigenvalues characterization, avoiding
spectral theory for a Prop-valued definition; the book states the two are equivalent.
IsRKHSOf and IsMinimizer are formalization scaffolding, not book-numbered definitions:
IsRKHSOf packages Theorem 6.8's own two displayed equations (6.8, 6.9) as a reusable
predicate shared between Theorem 6.8 (its conclusion) and Theorem 6.11 (its "H its
corresponding RKHS" hypothesis), using an explicit evaluation map ev : H → X → ℝ to stand in
for "elements of H are functions on X," since Mathlib's abstract Hilbert spaces are not
themselves spaces of functions; IsMinimizer packages argmin. Both X in Theorem 6.8's
existential and Theorem 6.11's ambient type are plain Type rather than Type*, avoiding
universe-polymorphic quantification over the constructed Hilbert space's own type — a harmless
simplification, since every application in this book instantiates X at a concrete, small
type (typically or a finite set). Theorem 6.11's loss codomain ℝ ∪ {+∞} is
WithTop ℝ, not EReal (which would also admit -∞, an unstated generalization the book's
own display does not license, since EReal's ⊤+⊥=⊥ collapse is a genuine faithfulness risk
the book's own L:\mathbb R^m\to\mathbb R\cup\{+\infty\} avoids by construction). WithTop ℝ
on its own does not avoid every collapse, though: an unconstrained L may be the constant
function ⊤ (a legal instance of ℝ∪\{+\infty\}), forcing the objective identically ⊤ and
every point to vacuously minimize it, which would make the theorem's second conjunct false. An
added hypothesis, ∃ h₀, F h₀ ≠ ⊤, makes explicit the book's own implicit assumption that the
objective is finite somewhere — see the Formalization scope note below. Theorem 6.11's two
clauses are otherwise kept exactly as distinct as the book states them: existence needs only
Monotone G (non-decreasing); "any solution has this form" needs StrictMono G (increasing)
as an added hypothesis on the second conjunct only — per this chunk's own BRIEF.md, the crux
of the theorem, and the trap this mission is most careful to avoid collapsing. Theorem 6.10's
five closure clauses are stated as one conjunction (matching the book's single theorem, not
five separate items); the power-series clause keeps the book's own radius-of-convergence
domain restriction and adds an explicit summability hypothesis guarding the ∑' term.
Not formalized: Theorem 6.2 (Mercer's condition) — not needed by the goal's own proof chain
(it is an equivalent characterization of PDS mentioned before the RKHS construction, not a
premise Theorem 6.8's or 6.11's proof invokes) and its own hypotheses (compact , continuous , an eigenfunction expansion of a compact self-adjoint integral
operator) are real analytic content this mission's budget does not include; Lemma 6.7
(Cauchy-Schwarz for PDS kernels) and Lemma 6.9 (normalized PDS kernels) — supporting lemmas for
Theorem 6.8's proof, not independently numbered results the goal cites; Theorem 6.12/Corollary
6.13 (Rademacher complexity/margin bounds for kernel-based hypotheses) — the chapter's optional
further milestone, connecting to chunks 03/05's machinery, cut for budget; §6.5-6.8
(sequence kernels, weighted transducers, rational kernels, Bochner's theorem, approximate
feature maps) — explicitly out of scope per this chunk's own BRIEF.md, a distinct,
applications-heavy topic.
A Markov decision process (MDP) chooses a decision in every period of a dynamic system whose state evolves stochastically in response to the decision, so as to maximize expected discounted return. Firms use this model for inventory, pricing, and advertising decisions that respond to a randomly evolving demand state; engineers use it for maintaining or replacing equipment that degrades stochastically. A recurring practical question is qualitative rather than numerical: does the optimal decision increase with the state — should a firm price higher after a period of strong sales, or replace a machine sooner the worse its observed condition — without having to solve the dynamic program numerically for every instance of the model? Topkis's Chapter 3, Section 3.9 (Topkis, Supermodularity and Complementarity, 2011, building on Topkis [1968]) answers this by isolating the lattice-theoretic structure — supermodularity of the return function and of the transition law — under which monotone optimal policies are guaranteed on structural grounds alone. A closely related but logically independent question was studied earlier by Lehmann [1955], who characterized when a family of distributions is stochastically increasing in a parameter; Topkis generalizes Lehmann's characterization to any property of the parameter dependence whose defining set of functions forms a closed convex cone, of which stochastic monotonicity, supermodularity, and convexity are three instances (Theorem 3.9.1, Corollary 3.9.1). Serfozo [1976] independently develops related conditions for partially observed Markov decision processes, and Amir [1996] and Amir, Mirman, and Perkins [1991] give analogous monotonicity results for other classes of dynamic programming models.
Fix a finite planning horizon of periods, . In period the state ranges over a set ; given state , the decision is restricted to a finite, nonempty set (finiteness guarantees that an optimal decision always exists — no continuity or compactness argument is used). Write for the set of admissible (decision, state) pairs in period . The (bounded) expected net return of choosing decision in state , period , is . A discount rate gives , the value in period of one unit of return in period . Given decision , state , and period , the state of period is drawn from a distribution on .
The optimal-value function (present value of acting optimally from state , period , onward) and the decision-value function (present value of choosing in state , period , then acting optimally thereafter) are defined by backward induction from period :
A subset of a Euclidean space is increasing if it is upward closed under the coordinatewise
order. A family of distributions indexed by a parameter is
stochastically increasing on if the probability of every increasing set
is a monotone (non-decreasing) function of on ; when is a sublattice, the family is
stochastically supermodular on if that same probability is a supermodular function of
on . A real-valued function on a lattice is supermodular on a set if
for all
— the mission series' shared notion, defined once in chunk 02-monotonicity and
reused here as Supermodularity.Monotonicity.SupermodularOn.
together with the existence of a greatest and a least optimal decision at every state, each increasing in the state, in every period — under the hypotheses that is a sublattice of , is expanding in , is increasing in (on sections) and jointly supermodular in , and is stochastically increasing in (on sections) and stochastically jointly supermodular in , for every period .
This is the weakest of the targets that is still worth stating on its own: it packages four related conclusions (parts (a)–(d) of Theorem 3.9.2) that share one hypothesis set, rather than isolating just the headline monotone-decision claim, because the book's own proof derives all four together and a solver attacking part (c) or (d) needs part (a) and (b) established first.
The result gives a purely structural sufficient condition — no smoothness, convexity of the decision set, or specific functional form — for monotone comparative statics in dynamic optimization: whenever the one-period return and the state transition are individually monotone and jointly supermodular in (decision, state), so is the whole multi-period value function, and so are the optimal decisions. Textbook applications include optimal advertising that decreases with prior-period sales, optimal pricing that increases with prior-period sales, and optimal maintenance of a deteriorating system, none of which need to be re-derived from scratch once the structural hypotheses are checked for the specific return and transition functions at hand.
Formalizing it contributes a genuinely new layer to the mission series and, per the paper's own
triage (substrate.md), to the platform's application of Mathlib's probability-kernel
infrastructure: a finite-horizon MDP with a Lebesgue–Stieltjes-style transition law and its
associated stochastic-dominance vocabulary (stochastically increasing / stochastically
supermodular families of distributions) did not previously exist on the platform or in this
mission series, and both are reusable beyond this mission by any future formalization of dynamic
programming under uncertainty. The proof itself is not open — Topkis [2011] (unchanged from the
1968/1998 original) gives a complete, elementary backward-induction argument — so what this mission
produces is the formalization of a known, structurally distinctive proof technique, not a new
mathematical result.
The naive argument — "supermodularity of plus supermodularity of the transition kernel obviously gives supermodularity of " — breaks exactly at the integral: supermodularity of is a statement about the whole family of distributions, not about a single number, so "the transition is jointly supermodular" has to be unpacked into "the probability of every increasing set is jointly supermodular in " before it says anything about for a specific function . Corollary 3.9.1(b) is exactly the step that licenses this unpacking, and it is not free: it needs Theorem 3.9.1's closed-convex-cone argument (approximating from below by increasing step functions and invoking monotone convergence), not a pointwise argument on and separately. A second place the naive argument fails is at the constraint sets: because only grows with rather than being fixed, monotonicity of (Lemma 3.9.4) needs its own induction combining that growth with monotonicity of — supermodularity of alone does not hand you monotonicity of the arg max without it.
States and decisions are represented as Fin m → ℝ and Fin n → ℝ (finite-dimensional Euclidean
coordinate spaces with the coordinatewise/product order, matching the book's own restriction to
and — no abstract lattice is used where the book itself specializes).
Distributions are represented as MeasureTheory.Measure on the relevant coordinate space, with
IsProbabilityMeasure supplied explicitly wherever a stochastic-dominance hypothesis is used (the
probability of a set is read off as (μ S).toReal, which is only faithful to when
μ is a probability measure — an unconstrained arbitrary measure would let .toReal collapse an
infinite value to and make the hypothesis trivially satisfiable, a formalization this mission
rules out). Integrands h are required integrable against every measure in the family wherever an
integral is asserted to lie in a set V, since the Bochner integral of a non-integrable function is
definitionally 0 in Lean/Mathlib and would otherwise make Theorem 3.9.1 and Corollary 3.9.1(b)
trivially true. Decision sets are finite (Finset, not merely a bounded or compact
Set) and required nonempty exactly where the book assumes it: this finiteness, not any
compactness or semicontinuity argument, is what guarantees an optimal decision exists, and dropping
it would silently substitute Chapter 2's compactness-based existence machinery for the different
argument this section actually uses. The optimal-value and decision-value functions are
represented as any functions satisfying the two backward-recursion equations that define them,
rather than being constructed by explicit backward recursion in Lean; since the equations determine
uniquely from and , this is a faithful reading of "define by (3.9.1)
and (3.9.2)," not a weakening of the theorem. The goal's part (c) is stated using the mission
series' InducedSetOrder (the Veinott/strong set order, chunk 01-lattices) and part (d) as the
existence of two selection functions (greatest, least optimal decision), each monotone in the
state — matching the book's "there is a greatest (least) optimal decision ... and this greatest
(least) optimal decision is increasing in ." The infinite-horizon stationary extension that the
book gives immediately after Theorem 3.9.2 (relying on an unproved citation to Blackwell [1965]) is
out of scope for this mission.
Reusable infrastructure: the StochasticallyIncreasingOn/StochasticallySupermodularOn
definitions are parametric in the ambient preorder/lattice and in the measure's target dimension,
so a future mission on stochastic convexity (Corollary 3.9.1(c), not formalized here) or on
Topkis's §3.10 stochastic inventory model (which explicitly depends on §3.9, per the book's own
reading-order note) can reuse them without modification. Contributions extending this mission to
the infinite-horizon case, or completing Corollary 3.9.1's monotonicity and convexity halves, are
welcome.
Random matrices with independent entries appear whenever a system is measured through many noisy, roughly independent channels: shot noise in a sensor array, edges in an Erdős–Rényi-type random graph, or the design matrix of a linear model with independent covariates. A basic question about any such matrix is how far it can stretch a vector — its operator norm — since this single number controls the stability of every linear statistic computed from : least-squares estimates, spectral clustering, covariance estimation, and random projections all reduce, at some point, to bounding .
The theory traces to Marchenko and Pastur's 1967 asymptotic law for the spectrum of large random matrices, and to Bai and Yin's 1988 almost-sure limit for matrices with i.i.d. mean-zero, unit-variance entries. Those results are asymptotic: they say what happens as the dimension , for a fixed matrix shape. The result formalized here, Theorem 4.4.5 of Vershynin's High-Dimensional Probability (2018) (DOI 10.1017/9781108231596), belongs to the more recent non-asymptotic strand of the theory: it gives an explicit, dimension-free bound that holds at every fixed , with an explicit failure probability — the form of statement needed for finite-sample guarantees in statistics and data science, rather than limiting behavior.
Let be an real matrix. Equip and with the Euclidean norm ; acts as a linear map . Its operator norm (§4.1.2) is
the largest factor by which can stretch a unit vector; equivalently, the largest singular value of .
A real random variable is sub-gaussian with the mission's own convention (matching the
Orlicz norm this series already carries as a published definition,
HighDimProb.Concentration.subgaussianNorm) if
Bounded random variables and Gaussians are sub-gaussian; a Bernoulli() variable and a -valued coin flip both qualify, which is why the theorem below directly covers random matrices with i.i.d. Rademacher or Gaussian entries as special cases.
The mission's proof technique is the ε-net argument, developed in §4.2 and used nowhere before this chapter of the book: a metric space , a subset , and give rise to an ε-net — a finite set such that every point of is within of some point of — and a covering number , the smallest cardinality of such a net. The technique reduces a statement that must hold uniformly over an infinite (compact) set to a statement about finitely many points, paid for by a union bound whose cost is controlled by the covering number.
for any random matrix with independent, mean-zero, sub-gaussian entries and . This is the weakest stable form of the bound — it fixes no numerical value for , only its existence and absoluteness (independence from , , , ), so later refinements of the constant do not invalidate it.
The result itself. The bound is sharp up to the constant: for entries of unit variance, for large (the book's Exercise 4.4.7), so no non-asymptotic bound of this shape can be improved beyond constants. It is the entry point to the rest of the book's random matrix theory: Corollary 4.4.8 specializes it to symmetric matrices, and it underlies the community-detection (§4.5) and covariance-estimation (§4.7) applications later in the same chapter, neither of which is part of this mission.
Formalizing it. The theorem is a classical, fully proved result; nothing about its truth is
open. What this mission contributes is a machine-checked formal statement — together with the
two pieces of chapter infrastructure its own textbook proof names by number (Corollary 4.2.13,
Exercise 4.4.3(a)) — and a third, self-contained application of the same covering-number
machinery (Theorem 4.3.5) that exercises the shared IsEpsNet/coveringNumber definitions on a
different metric space (the Hamming cube), independently of the Euclidean case. Mathlib and the
Prove2Me platform currently have no ε-net, covering-number, or packing-number infrastructure
(checked by q=random matrix, q=operator norm, q=covering number, q=net on the platform,
and by filename search in Mathlib): this mission is the first to introduce it, restated inside
its own namespace since it is not otherwise available to build on.
The obvious first approach is to bound directly by union-bounding a concentration inequality over the sphere . This fails outright: is
infinite (indeed uncountable) for , so no union bound over its points can converge — the
naive approach gives . The ε-net argument is the fix, but
it is not just "discretize and hope": the reduction from the sphere to a finite net
(quadratic_form_on_net, Exercise 4.4.3(a)) loses a multiplicative factor
that must be tracked, and the net's cardinality (covering_numbers_of_euclidean_ball_and_sphere,
Corollary 4.2.13) is exponential in the dimension ( at ) — so the
per-point tail probability from Hoeffding-type concentration must itself decay fast enough
(quadratically in the exponent) to survive multiplying by many points. Getting the
union bound to close requires choosing the threshold in the tail bound proportionally to
, not to alone — the term is exactly what pays for
the net's exponential size.
is represented as Ω → Matrix (Fin m) (Fin n) ℝ; its entries A ω i j are the individual
real random variables. Independence of the entries is iIndepFun over the index type
Fin m × Fin n; mean-zero is the vanishing of each entry's Bochner integral. The operator norm
is the norm of the associated continuous linear map between EuclideanSpace ℝ (Fin n) and
EuclideanSpace ℝ (Fin m) (matrixOpNorm, every linear map between finite-dimensional normed
spaces being automatically continuous), matching the book's maxₓ∈Sⁿ⁻¹ ‖Ax‖₂ exactly. The
sub-gaussian norm reuses this series' own published definition,
HighDimProb.Concentration.subgaussianNorm, rather than a re-derivation. Covering numbers
(coveringNumber) are restricted to finite (Finset) ε-nets, the only kind this chapter uses;
this is a deliberate restriction, not a general-purpose covering-number formalization, and is
disclosed as such. A hard-coded numeral for , or an unquantified "with high probability" in
place of the explicit failure probability , would each trivialize the statement and
is ruled out: is existentially bound ahead of every other quantifier, and is a free
parameter with its own explicit bound, exactly as the book states it.
Definitions reusable beyond this mission: IsEpsNet and coveringNumber are stated for a
general PseudoMetricSpace and apply unchanged to any later chapter's covering-number needs
(e.g. Chapter 8's VC-dimension covering numbers), though per this series' rule that drafts cannot
import drafts, a later chunk would restate rather than import them until this mission is
published. matrixOpNorm is likewise chapter-agnostic. Contributions completing the sorry
proofs of any of the four theorem items are welcome and independent of one another; the covering
number and net-reduction items (covering_numbers_of_euclidean_ball_and_sphere,
quadratic_form_on_net) are the standard prerequisites for the goal's own volumetric/ε-net
proof.
Every method in Chapters 2-4 of this series solves a projection or proximal subproblem at every step — a Euclidean projection, or a Bregman-divergence prox-mapping — which can itself be as hard as the original problem when is a complicated feasible set (a spectrahedron, a flow polytope, a matroid base polytope). The conditional gradient method (Frank & Wolfe, 1956) sidesteps this entirely: instead of a projection, each step calls a linear optimization (LO) oracle — minimize a linear function over — which is frequently far cheaper (over a spectrahedron, this reduces to a single eigenvector computation; over many combinatorial polytopes, to a greedy algorithm). This is the origin of the modern "projection-free" family of optimization methods widely used at the scale where projections are the bottleneck.
Fix a nonempty compact convex set in a real normed space and a convex with -Lipschitz gradient (Eq. (7.1.4)): . The classic conditional gradient (CndG) method, Algorithm 7.1, sets , , and for : calls the LO oracle , then sets for a stepsize , either the fixed schedule (Eq. (7.1.9)) or exact line search (Eq. (7.1.10)).
Section 7.1.1.2 extends this to bilinear saddle-point problems, where itself is the (generally nonsmooth) function (Eq. (7.1.5)) for a compact convex and linear operator . Since is nonsmooth, the method is applied instead to a family of smooth approximations built from a strongly convex on (Eq. (7.1.21)-(7.1.23)), with the smoothing parameter allowed to vary across iterations rather than being fixed in advance.
Every constant here is exactly the book's; the goal theorem's bound is left in terms of the actual step distances , not a diameter-based simplification (see Difficulty).
This mission formalizes the founding convergence result of the entire projection-free family (Frank-Wolfe methods), which has become central to large-scale machine learning precisely because its per-iteration cost can be orders of magnitude below that of a projection-based method on structured feasible sets. Theorem 7.1's specific form — a rate depending on the realized step distances rather than a fixed diameter — is also the more informative, tighter statement (the book's own remarks show it recovers the classical diameter-based complexity as a corollary, but also explains why the rate can be much better in practice when the iterates settle near an extreme point).
No result matching conditional gradient / Frank-Wolfe methods exists on the platform as of
2026-09-18 (q=Frank-Wolfe and q=conditional gradient both return zero hits — see Prior art
in MODERATION_NOTES.md).
The chief formalization difficulty is representing "with the stepsize policy in (7.1.9) or
(7.1.10)" faithfully without either restricting to one policy (weaker than the book's stated
theorem) or introducing an awkward disjunction of two separate algorithm definitions. The book's
own proof resolves this by a single observation used for both policies at once: for the point the fixed schedule would have
produced — trivially by equality under (7.1.9), or because is chosen to minimize over
the entire line segment under (7.1.10), of which is one point. This mission's
hyk_le hypothesis states exactly this shared consequence, which is genuinely what the proof
uses and genuinely covers both policies, rather than picking one arbitrarily.
A second difficulty is not collapsing into a diameter bound inside the milestone itself — the book's own remarks perform that substitution as a separate, weaker corollary (Eq. (7.1.19)) after stating Theorem 7.1 in its sharper form; folding the substitution into the goal statement itself would silently prove a different, weaker theorem.
conditional_gradient_rate and saddle_point_cndg_rate state the LO oracle's exactness
(x k ∈ Argmin_{z∈X}⟨fGrad(y(k-1)),z⟩) as a pointwise hypothesis rather than deriving it from
IsCompact X via an existence lemma — matching the pointwise-hypothesis convention this series
uses throughout for argmin-defined algorithmic steps (chunk 03-deterministic's mirror-descent
updates, chunk 04-stochastic's stochastic mirror-descent update). X compact convex is still
included as a hypothesis, matching the book's own standing assumption on the problem class, even
though it is not itself needed to derive the stated conclusion from the other hypotheses.
smoothed_objective_monotone and saddle_point_cndg_rate realize / via sSup of the
image of under the pointwise saddle-point objective, matching the book's own max_{y∈Y}{...}
definition (Eq. (7.1.5), (7.1.23)) directly rather than introducing a separate Def_ file for a
"bilinear saddle-point objective" structure — no other item in this mission reuses that
definition verbatim, so per this series' convention (no shared substrate bundled into a structure
unless reused), it is inlined at each use.
A trivializing formalization this mission rules out: stating the LO oracle via an
-approximate minimizer ((fGrad (y(k-1))) (x k) ≤ (fGrad (y(k-1))) z + ε for some
ε) rather than an exact one — this is explicitly a different, weaker algorithm the book does not
analyze in Theorem 7.1/7.2 (the book studies approximate LO oracles separately, later in the
chapter, not selected here).
Left out of scope, for time: Theorem 7.7 (the matching lower complexity bound for LO-oracle
methods, Eq. (7.1.60)) — formalizing it faithfully requires first modeling the abstract class of
"LCP methods" (any algorithm restricted to LO-oracle calls) as a universally-quantified object,
a substantially different and more involved formalization task than the two upper-bound
convergence theorems selected here; named per Hard Rule 7 rather than approximated. The
d(x)=\sum x_i\log x_i entropy-smoothing remark and the primal/primal-dual averaging CndG
variants (§7.1.2, not covered by this mission's page range) are likewise not attempted.
Empirical-risk-minimization objectives in machine learning are finite sums: , one smooth term per training example (or per worker, in a distributed setting), plus a simple nonsmooth regularizer . Chapter 4's basic stochastic mirror descent handles this by sampling a single random component gradient as an unbiased estimator of — but that estimator's variance is a constant throughout the algorithm, which caps the achievable convergence rate. Variance-reduced mirror descent asks a sharper question: can an unbiased finite-sum gradient estimator be built whose variance itself vanishes as the algorithm approaches the optimum? The answer — periodic full-gradient snapshots combined with single-component corrections — is the SVRG-style idea this mission formalizes in Lan's general-norm mirror-descent framework, with an explicit, sampling-distribution-dependent constant rather than a generic .
Fix a closed convex set in a real normed space , and the finite-sum composite problem (Eq. (5.3.1)), where is the average of smooth convex component functions, each with -Lipschitz gradient (), and is a simple, possibly nondifferentiable convex function. is possibly -strongly convex, (Eq. (5.3.2)); this mission's goal takes (§5.3.1, "Smooth Problems Without Strong Convexity"). A fixed probability distribution on the component indices governs the algorithm's random sampling, and
is the section's key aggregate smoothness constant (Eq. (5.3.4)), replacing the plain average wherever component-wise variance enters the analysis. Variance-reduced mirror descent (Algorithm 5.6) is a multi-epoch method: each epoch of length recomputes a full gradient at a snapshot point , then runs inner iterations using the estimator and the mirror-descent-with-composite-term update , where is the Bregman divergence of a fixed distance-generating function, exactly as in Chapters 3-4.
With , , and the doubling epoch schedule , (Eq. (5.3.17)),
for every epoch count , where is the weighted average of the epoch snapshots (Eq. (5.3.16)).
Every constant is exactly the book's: 's own sampling-distribution-dependent definition (never specialized to uniform ), and Corollary 5.8's explicit , , — not a generic — are all taken verbatim.
This is the series' first genuinely finite-sum result: unlike Chapters 3-4's single abstract objective , here is structurally a named average of component functions, and the sampling distribution over those components is a first-class free parameter of both the algorithm and the analysis (not fixed to uniform sampling) — itself depends on this choice, and a formalization that hard-codes would understate what Lemma 5.12's own proof needs. Getting Theorem 5.6/Corollary 5.8 right also requires keeping two nested indices straight: inner iterations within an epoch, and outer epoch counts , with the convergence bound stated in terms of the epoch count alone — and keeping the two "gap" quantities (an objective-value gap) and (a Bregman-divergence gap) distinct throughout, since they enter Corollary 5.8's final bound with different explicit coefficients ( vs. ) and neither generically bounds the other.
No result on the platform models a finite-sum objective with named component functions
sampled by a general index distribution , a variance-reduction snapshot/anchor point, or
this specific SVRG-style estimator, as of 2026-09-18 (q=finite sum, q=variance reduction,
q=SVRG, q=component function, q=variance reduced gradient, q=mirror descent finite sum —
see Prior art below).
The central difficulty is Theorem 5.6's own epoch-weight sequence : the book defines
explicitly only for (Eq. (5.3.14)), yet the
displayed sums in (5.3.15)-(5.3.16) run from . A 2026-09-19 revision found
that this, combined with the epoch snapshot being constrained only by membership in
and not tied to the algorithm's own dynamics, made the originally drafted statements false,
not merely incomplete: an adversarial, unboundedly-large-, -independent
together with violates the stated conclusion. The fix restores the connection via an
auxiliary epoch-boundary sequence and the per-epoch progress inequality Theorem 5.6's own proof
derives from Lemma 5.14 (see epoch_convergence_bound's hepoch hypothesis), and resolves
by extending (5.3.14)'s domain to via a fixed "epoch 0" length — w_1 is no longer
left free beyond positivity. finite_sum_variance_reduced_rate instantiates
concretely, reproducing the arithmetic Corollary 5.8's own proof is internally consistent with
(, matching the closed form ) — this was
previously only a documented-but-unresolved observation, not yet a stated hypothesis.
All five items are stated over a general real normed space [NormedAddCommGroup E] [NormedSpace ℝ E], matching the mirror-descent chunks' general-norm convention (never specialized to Euclidean
space or squared distance) — is a free two-point function throughout, and each ,
, are continuous linear functionals E →L[ℝ] ℝ, whose Mathlib operator norm
supplies the dual norm with no separate definition needed. This is the trivializing
formalization this mission rules out: hard-coding (uniform sampling) or (Euclidean Bregman divergence) would understate both 's dependence on the sampling
distribution (the whole point of Lemma 5.12's bound) and the general-norm apparatus the rest of
this book series shares.
Ψ(x_0)-Ψ(x^*) and V(x_0,x^*) are kept as two syntactically distinct terms throughout — never
conflated or bounded one by the other — matching Corollary 5.8's own two separate coefficients.
Corollary 5.8's own explicit constants (, , ) are stated verbatim rather
than left as an unspecified , per Hard Rule 6.
Left out of scope, for time: the gradient-computation-count complexity bound (Eq. (5.3.19), an
statement about total oracle calls, not a convergence-rate inequality on ) and
§5.3.2's strongly-convex case (Theorem 5.7, a geometric-decay bound
under ) are natural continuations reusing this mission's variance_reduced_progress_bound
milestone, not attempted here.
q=finite sum, q=variance reduction, q=SVRG, q=component function, q=variance reduced gradient, and q=mirror descent finite sum were all searched on 2026-09-18. The only
topically-adjacent hit across all six queries is ShiOptRates.Stochastic.variance_purchase_ classical ("Classical variance reduction is cost-neutral..."), which models plain minibatch SGD
on a smooth objective with an i.i.d.-noise oracle characterized by a single scalar variance
and a minibatch-size trade-off — no finite-sum structure with named component
functions, no sampling distribution , no snapshot/anchor point , and a
different question (cost-neutrality of minibatch size vs. this mission's convergence rate for a
fixed variance-reduction scheme). Not reused; every item in this mission is drafted fresh.
Gradient descent's convergence rate for a general smooth convex problem is in the function-value gap; Nemirovski and Yudin (1983) proved that no first-order method can do better than is achievable, and Nesterov (1983, 1988, 2004) constructed the first method attaining it — the accelerated (or "fast") gradient method. For thirty years this was the standard route to -rate solvers in convex optimization, and the technique underlies essentially every modern accelerated first-order method used at scale in machine learning (accelerated SGD, momentum methods, Nesterov-style extensions of Adam). The two building blocks this mission formalizes on the way there — subgradient descent (Polyak, 1960s) and mirror descent (Nemirovski & Yudin, 1983) — are themselves the default tools whenever the objective is nonsmooth or the constraint set's natural geometry is not Euclidean (e.g. the probability simplex, where mirror descent with the entropic distance-generating function beats projected subgradient descent by a factor).
Fix a nonempty closed convex set (in Lean: a normed real vector space , X : Set E) and a
convex ; write and for an arbitrary
minimizer. The projected-subgradient update is for a subgradient and stepsize
. Its generalization, mirror descent, replaces the Euclidean proximal term with a
Bregman divergence built from a
1-strongly-convex distance-generating function with respect to a general norm
(dual norm ): ,
where is now a continuous linear functional (a subgradient in the dual space, since the
norm need not come from an inner product). Choosing recovers and the plain subgradient update as a special case.
The accelerated gradient method additionally assumes has -Lipschitz gradient () and is -generalized-strongly-convex w.r.t. ( for ), and tracks three coupled sequences from :
With , and :
Every constant here is exactly the book's; no milestone hides an behind an unspecified absolute constant.
The chain culminates in an explicit, non-asymptotic certificate for accelerated gradient descent — the theoretically optimal rate for smooth convex minimization by a first-order method (matching the Nemirovski–Yudin lower bound, not re-derived here). Formalizing it forces every implicit convention in a standard optimization-course derivation to become explicit: which of the three sequences a given quantity refers to, exactly which inequality (3.3.7)-(3.3.9) each specific stepsize schedule needs to satisfy, and the precise index range over which the chapter's own stated hypotheses actually get used in its own proof (see Difficulty below).
None of these six results (or their strongly-convex counterpart, Theorem 3.7, left for future
work — see Formalization scope) has a machine-checked proof on Prove2Me. The one theorem with
the same name as this mission's subject, BanditAlgorithm.mirror_descent_regret_bound
(Lattimore & Szepesvári, Theorem 28.4), is a different object: an online, adversarial regret
bound against a changing sequence of loss vectors , not an offline function-value gap for a
single fixed ; not reused. Likewise OnlineConvexOpt.FirstOrder.online_gradient_descent_regret
(Hazan) and OnlineConvexOpt.ConvexBasics.constrained_gd_well_conditioned_convergence are,
respectively, an online-regret bound and a plain-gradient-descent (non-accelerated) linear-rate
result — checked and confirmed not reusable per the mission brief.
The three-point inequalities (Lemmas 3.1/3.4) are routine consequences of a strongly-convex minimizer's optimality condition. The real difficulty is bookkeeping across three coupled sequences in the accelerated method: a formalization using only and (dropping , the point at which the gradient is actually evaluated) is not Lan's algorithm and proves either a false or a different bound — is what lets the method use a gradient computed at a point between and , which is exactly the extrapolation step that makes acceleration work.
A second, subtler difficulty is that Theorem 3.6's own stated hypothesis — "(3.3.15) for any " — is not quite what its proof uses. Telescoping Proposition 3.1's per-step bound via (3.3.15) requires the previous step's constants ; at these would be , values the recursion (3.3.4)-(3.3.6) never defines (it only ever uses for ). The book's own proof, read closely, invokes (3.3.15) only for , with handled directly by Proposition 3.1's conclusion connecting to the given base data . Formalizing the literal hypothesis range would either be unstatable (no exist) or vacuous (adding unused ghost parameters); this mission states the range the proof actually needs.
Chapter 3's own §3.1/§3.2 split (Euclidean vs. general norm) is preserved rather than collapsed:
subgradient_iterate_three_point/subgradient_descent_bound are stated over a real inner
product space with the vector subgradient and the Euclidean norm, exactly matching
§3.1; mirror_iterate_three_point/mirror_descent_bound and the two accelerated-method
milestones are stated over a general real normed space [NormedAddCommGroup E] [NormedSpace ℝ E], with subgradients as continuous linear functionals E →L[ℝ] ℝ (whose Mathlib operator norm
is already the dual norm , needing no separate definition) and the Bregman
divergence left as a free two-point function — but, following a
2026-09-19 revision, no longer a totally free function. V is now required to satisfy the two
facts (3.2.2)/(3.2.3)/(3.2.6) actually establish and every downstream proof (Lemma 3.4, Theorem
3.5, Proposition 3.1, Theorem 3.6) uses: nonnegativity ( for ) and the
three-point/cosine identity ,
the latter made explicit via an added parameter dV : E → E → (E →L[ℝ] ℝ) read as "the gradient
of at ." Without these two hypotheses the five items that use an abstract V
(mirror_iterate_three_point, mirror_descent_bound, accelerated_one_step_recursion,
accelerated_gradient_recursion_bound, accelerated_gradient_rate) are false as stated — a
constant V satisfies the bare pointwise-minimality hypotheses while violating the conclusion, as
two worked counterexamples confirmed. This mission does not derive V/dV from an explicit
distance-generating function (the heavier, fully book-literal route (3.2.1)-(3.2.2) would);
it takes the two facts the proofs actually consume as hypotheses directly, which is lighter and
sufficient. Satisfiability is witnessed by the Euclidean case already in §3.1:
, , , exactly how
subgradient_iterate_three_point/subgradient_descent_bound already handle the Euclidean
special case. A trivializing formalization this mission rules out: specializing to the
Euclidean squared distance in mirror_iterate_three_point/mirror_descent_bound would make
those two milestones restatements of the §3.1 Euclidean results rather than genuine
generalizations, exactly the pitfall the chapter brief flags.
Every argmin-defined iterate ( in each of the three update rules) is represented by
its defining pointwise-minimality property rather than by an IsMinOn/argmin term, so no
existence or uniqueness lemma for the underlying minimization problem is needed anywhere in this
mission — matching how the book's own proofs use these updates (via their first-order optimality
condition, never via an explicit formula for the minimizer).
Left out of scope, for time: Theorem 3.7 (the strongly-convex, linear-rate
companion to Theorem 3.6, sharing Proposition 3.1 as its own base lemma) and Corollary 3.5 (the
composite-objective extension ). Both are natural continuations reusing this
mission's accelerated_one_step_recursion; a later mission or an amendment to this one could add
them as additional milestones/goals without touching what is here.
Every algorithm in the first three chapters of Foster and Rakhlin's Foundations of Reinforcement Learning and Interactive Decision Making — ε-Greedy and UCB for the multi-armed bandit, Inverse Gap Weighting and SquareCB for contextual bandits — is a special case of the same two-step recipe: estimate a model of the world with an online regression oracle, then convert the estimate into a decision that trades exploration against exploitation. Chapter 4 asks whether this recipe can be made generic: given any structured decision-making problem, specified only by a function class and a decision space , is there a single quantity that governs the best achievable regret, the way governs the multi-armed bandit and governs the linear bandit? The chapter's answer is the Decision-Estimation Coefficient (DEC), introduced by Foster, Kakade, Qian, and Rakhlin [40] as a complexity measure that both upper- and lower-bounds achievable regret for a general decision-making protocol, unifying results that were previously proved from scratch, case by case, for each structured setting. This mission formalizes the chapter's central upper bound (Proposition 13) together with the machinery that makes it computable in two concrete cases — the multi-armed bandit (Proposition 14) and the linear bandit (Propositions 16–17).
Fix a finite decision space and a class of candidate mean-reward functions, with a ground-truth (realizability). Over rounds, at each round the learner observes an estimate produced by an online regression oracle, plays a decision distribution (possibly depending on and the history), and the regret is
where . The oracle's cumulative estimation error is assumed bounded: with probability at least (Definition 7). Writing , the DEC game value at a reference model and scale is the min-max quantity
and the DEC of itself is . The Estimation-to-Decisions (E2D) algorithm plays, at each round, a certifying (i.e. attaining or beating) the value of this min-max game at .
with probability at least , for any exploration parameter . This is the weakest stable statement the chapter proves about E2D: it holds for an arbitrary function class and an arbitrary regression oracle, with no structural assumption on beyond realizability, and the chapter's later sections instantiate it rather than strengthen it.
The Decision-Estimation Coefficient is, in the book's own words, "the main result" of this line of work: Foster, Kakade, Qian, and Rakhlin [40] show it is not merely an upper bound but (in a suitable localized form, developed further in Chapter 6) a tight characterization of the minimax regret for structured bandits and, more generally, for the interactive decision-making protocol the rest of the book studies. Proposition 13 is the mechanism that makes this useful in practice: it reduces regret analysis for a new structured problem to a single, purely convex-analytic computation of , in place of a bespoke exploration argument. Propositions 14–17 are the demonstration that this reduction is not vacuous — they recompute, via the DEC alone, the two rates (multi-armed and linear bandit) that earlier chapters of the book derived by direct, setting-specific arguments, and the match is exact. Formalizing this chapter therefore captures the book's unifying abstraction itself, not just one more instance of it. No formalization of the Decision-Estimation Coefficient, in any form, currently exists on the platform (see Formalization scope).
The obvious formalization mistake is to state Proposition 13's conclusion with left as an unconstrained free real-number parameter satisfying only the inequality the theorem asserts — a formalization under which the "theorem" would be a triviality about an arbitrary real number, since nothing about the actual min-max game would ever be checked. The chapter's content is precisely the opposite: that this specific minimax quantity can be computed (Proposition 14) or bounded via a concrete strategy (Proposition 17), and — as Chapter 6 shows for a lower bound outside this chunk's scope — that no smaller quantity would do. A second difficulty is proof-theoretic rather than notational: the book's own proof of Proposition 13 bounds regret by an unconstrained supremum over all reference functions , and only identifies this with the official, -restricted of Eq. (4.16) via Proposition 24 — a fact stated on p. 80, outside this chapter's numbered range, whose own proof the book defers to an exercise. A formalization that quietly imports Proposition 24 to close this gap would rest the goal theorem on an unverified fact; this mission instead states the hypothesis the book's own text uses to motivate restricting to in the first place (online estimation algorithms produce ), so the goal is faithful to what is actually established within the chapter's own pages.
Every item fixes a finite decision space (Fin A, Fin n, or a generic Fintype S)
and states the DEC as the literal sInf-of-sSup transcription of the min-max game
(Eqs. (4.15)–(4.16)), never as an opaque bound — this is the trivializing
formalization the chunk's own reading of the chapter rules out (see Difficulty).
piStar : (S → ℝ) → S is a hypothesized global maximizer selector throughout,
constrained to be a genuine argmax only on the function class in scope (F or
Set.univ), matching how the book treats as a fixed but arbitrary
tie-breaking choice. The goal theorem (Proposition 13) adds the explicit hypothesis
hfhat : ∀ t, fhat t ∈ convexHull ℝ F, replacing an appeal to the out-of-range
Proposition 24 (see Difficulty); this is the one place this mission's statement is not
a line-by-line transcription of the book's own displayed proof steps, and it is
recorded here and in MODERATION_NOTES.md. Proposition 14's and Proposition 17's
are replaced by the explicit constants the book's own proofs establish
( exactly, and respectively — the latter obtained
by summing the three terms the proof of Proposition 17 isolates). Proposition 14's
Lean statement splits the book's single equality into an upper bound on the literal decGf, a lower bound restricted
to full-support distributions, and IGW's own exact game value, because the book's
min over the whole simplex is not provable as a literal Lean equality: a
distribution with a zero-weight arm makes the inner supremum genuinely unbounded, and
Lean's total Real.sSup returns a junk value smaller than there
(caught in moderation, MODERATION_NOTES.md); the three-conjunct statement recovers
exactly the book's real content without asserting that false literal equality. Lemma 9
is restated
inside FoundationsRL.Structured rather than imported from the Chapter 2 mission,
since draft items across chunks cannot import one another; its source citation still
points to its original location (p. 32). Proposition 16 is not drafted: the
platform's existing BanditAlgorithm.kiefer_wolfowitz_equivalence (Lattimore &
Szepesvári, Theorem 21.1) states the identical existence claim — compact set with
full-dimensional span, a design with G-value at most — as one clause of a larger
equivalence, and is reused as a reference item rather than redrafted. Proposition 22
(primal/dual DEC equivalence, §4.4) is deliberately excluded: the book states it "under
mild regularity conditions" it does not pin down in the statement itself, which is
exactly the kind of unquantified hypothesis this series' faithfulness standard
excludes from a goal or milestone. Contributions extending this mission with Chapter
6's lower bound (matching from below, establishing tightness)
or with a formalization of Proposition 24 itself (removing this mission's hfhat
hypothesis) are welcome.
Two-stage stochastic linear programming with recourse models a decision made before uncertainty resolves (the first-stage variables ) followed by a corrective decision made after (the second-stage, or recourse, variables ). Solving such a program means minimizing , where is the expected cost of the best recourse action given -- an object defined only implicitly, as the value of an embedded linear program that must be solved (or bounded) for every realization of the uncertain data. Before any algorithm for this problem can be justified -- the L-shaped method, stochastic decomposition, scenario decomposition, all developed in later chapters of Birge & Louveaux, Introduction to Stochastic Programming (Springer, 2011) -- one needs to know that is well-behaved enough to optimize over at all: that the feasible region is closed and convex, that itself is a finite, Lipschitz, convex function on it, that an optimal solution is actually attained rather than only approached in the limit, and finally what an optimality condition for the resulting nonsmooth convex program even looks like. This mission formalizes exactly that foundational layer, Chapter 3, Section 3.1 of the book.
Fix natural numbers and a finite scenario count . A two-stage recourse instance consists of first-stage data , , , a fixed recourse matrix , and, for each scenario , a cost vector , a right-hand side , a technology matrix , and a probability with (Eq. (1.1)). The first-stage feasible region is .
For a fixed and scenario , the second-stage value is
(Eq. (1.6)), taken as an extended real: if no feasible exists, if the inner program is unbounded below. The expected recourse value is (Eq. (1.3)), combined so that -- the book's own convention (p. 109): infeasibility in one scenario is treated as fatal even if another scenario is unboundedly favorable. The second-stage feasibility set is , and the deterministic-equivalent objective is (Eq. (1.2)). For with finite, the subdifferential is the set of satisfying for every (p. 115).
A simple-recourse instance is the special case : the recourse cost splits as , and decomposes componentwise via the closed form of Eq. (1.9)-(1.10) using the (left- and right-limit) distribution functions of each .
given that (1.2) has a finite optimal value. This is the KKT-style necessary and sufficient optimality condition for the two-stage recourse LP, and the weakest of the mission's targets in the sense that everything else supports it: convexity and finiteness of (Theorem 6) are what make the left-to-right implication meaningful, closedness/convexity of (Theorem 5) makes the feasible region well-posed, and attainment (Theorem 8) is what makes " is optimal" a statement about a point that exists rather than an infimum that may not be reached.
Theorem 9 is the hinge on which the rest of the book's algorithmic chapters turn. The L-shaped method (Chapter 5) is a cutting-plane scheme whose cuts are literally elements of ; stochastic decomposition and sampling-based methods use the same subdifferential structure with estimated cuts; the differentiable specialization (Eq. (1.14), ) underlies nonlinear-programming approaches to the smooth case. None of this is meaningful without first knowing is convex, finite where it needs to be, and that a minimizer exists to characterize. Formalizing this mission's four milestones from the actual definition of as an embedded linear program's value -- rather than assuming these properties -- is exactly the content the book itself proves (or, for Theorem 6, explicitly cites to Wets [1972] and Kall [1976] rather than proving); this mission asks for genuine Lean proofs of Theorems 5, 8, 9 and Corollary 10 from the LP structure of , and records Theorem 6 as a stated (not re-derived) input, matching the book's own presentation.
The obvious shortcut is to treat as an opaque convex function and apply a textbook convex-KKT
theorem off the shelf. This fails to capture what Theorem 9 actually is: a statement about the
specific function , built from finitely many parametric linear programs, each of which can be infeasible
() or unbounded () depending on . Convexity of
must come from convexity of the value function of a parametric LP in its right-hand side
(the book's Theorem 2 argument: a convex combination of optimal solutions at two right-hand
sides is feasible, hence suboptimal, at the combined right-hand side) -- not from an assumed
hypothesis. Handling correctly is a second, easy-to-miss source of error: the book
fixes an explicit, non-default convention ( dominates ) for combining
per-scenario values, the opposite of the convention Mathlib's own extended-real arithmetic uses,
so any formalization that reaches for EReal's built-in addition to aggregate silently
states a different theorem. Theorem 8's attainment condition is a genuine existence result, not
an automatic consequence of convexity: continuity alone does not give attainment on an unbounded
feasible region, and the book's own counterexample (Eq. (1.11), a negative-exponential tail with
infimum attained by no finite ) shows the boundedness/recession hypotheses are load-bearing.
The scenario set is modeled as Fin K, a finite discrete random variable, matching Section
3.1b's development; under this model " has finite second moments" (the standing hypothesis
of Theorems 4-11 in the general, possibly-continuous case) holds automatically and so does not
appear as a separate hypothesis anywhere in this mission. Q(x,\xi_k) is defined as an EReal
via sInf of the second-stage LP's feasible objective values -- sInf of the empty set is
⊤, and of a set unbounded below is ⊥ -- and is genuinely derived from that inner
minimization rather than assumed convex; this rules out the chapter's trivializing
formalization, which the paper-level triage explicitly warns against: taking Q(x) as an
opaque convex-function hypothesis instead of deriving its properties from the inner LP's
structure. Aggregating the per-scenario values into uses a bespoke bookAdd operation
implementing the book's stated convention , since Mathlib's EReal
addition is defined with the opposite convention (). is
the ordinary subgradient-inequality set for this extended-real-valued function.
Theorem 8's condition (b) is stated with the book's own quantifier structure: the threshold
and the recession value depend on the point and direction exactly as
written, with no strengthening. Theorem 6(a)'s Lipschitz bound is stated, not derived -- the book
itself cites it to Wets [1972] and Kall [1976] without proof -- so a faithful Lean proof of that
milestone is expected to remain out of scope for this mission. Corollary 10 similarly takes the
closed form of from Eq. (1.10) as a hypothesis on an abstract , matching how
the book itself uses (1.10) as an already-established fact rather than re-deriving it from the
second-stage LP in the corollary's own proof. Theorem 11's subdifferential-decomposition result
() is deliberately left out of
this mission's scope: it is not needed by Theorem 9's own proof, and its normal-cone term would
require relatively-complete-recourse machinery this mission does not otherwise need. No prior-art
match was found on the platform: VectorSpaceOpt.fenchel_duality and the Luenberger-derived
VectorSpaceOpt.generalized_kuhn_tucker / kkt_complementary_slackness family use a
differentiable (Gateaux-derivative) or conjugate-function KKT model over general normed spaces,
not this chapter's finite-dimensional, possibly-nondifferentiable subgradient formulation over
the specific polyhedral set , so none is a faithful match and all items here are original
drafts.
Chapter 7 of Walter Rudin's Principles of Mathematical Analysis (3rd edition, McGraw-Hill, 1976) asks when a limit of functions inherits the properties of its members. Pointwise convergence preserves almost nothing: Rudin's opening examples give continuous with discontinuous limit, and sequences where . Uniform convergence is the hypothesis that repairs this, and the chapter's second half asks the converse question — which functions arise as uniform limits from a given family — answered by the Stone–Weierstrass theorem (Theorem 7.32): an algebra of continuous real functions on a compact set that separates points and vanishes nowhere is uniformly dense in all continuous functions there.
The classical Weierstrass approximation theorem (7.26) — polynomials are dense in — is the special case that made the general theorem worth proving, and is used in Chapter 8 for Fourier series and in Chapter 11 for the density of continuous functions in .
This mission is the seventh in a series formalizing Rudin Chapters 1–11; it uses the compactness results of Mission II, the continuity results of Mission IV and the Riemann–Stieltjes integral of Mission VI.
A sequence converges uniformly to on if for every there is with for all and all — the same for every point. A family is equicontinuous on if a single serves all its members in the definition of uniform continuity; it is pointwise bounded if each orbit is bounded, and uniformly bounded if one bound works for all and all .
A set of real functions is an algebra if it is closed under addition, multiplication and multiplication by real scalars; it separates points on if for in some has ; it vanishes at no point of if for each some has . The uniform closure of on is the set of uniform limits on of sequences from .
Let be compact and let be an algebra of real continuous functions on which separates points on and vanishes at no point of . Then
every continuous real function on is a uniform limit on of members of .
Uniform convergence is the standard hypothesis under which limits commute with continuity, integration and (with an extra condition) differentiation, and Theorems 7.11, 7.12, 7.16 and 7.17 are used throughout the rest of the book; Chapter 8 in particular builds the exponential, trigonometric and Gamma functions as uniform limits and differentiates them term by term on the strength of 7.17. Theorem 7.18 shows how weak pointwise differentiability is as a consequence of continuity: a uniform limit of piecewise-linear functions can fail to be differentiable anywhere. Arzelà–Ascoli is the compactness criterion for families of functions, and it is the standard route to existence theorems for differential and integral equations.
Stone–Weierstrass is the structural theorem of the chapter: it replaces the combinatorial Bernstein-polynomial proof of Weierstrass's theorem with a statement about algebras of functions, applicable to trigonometric polynomials, polynomials in several variables, and Lipschitz algebras alike.
Mathlib contains a Stone–Weierstrass theorem for subalgebras of C(X, ℝ) on compact Hausdorff
spaces, and a version of Arzelà–Ascoli. This mission states the results in Rudin's terms — plain
sets of functions on a compact subset of a metric space, uniform closure defined by
sequences — so that they can be used together with the Riemann–Stieltjes integral built in
Mission VI, which is not part of the library.
Stone–Weierstrass is the one theorem in this mission whose proof is genuinely structural: from the algebra one first produces as a uniform limit of polynomials in (which needs the polynomial approximation of on and so cannot be circular with Theorem 7.26), then maxima and minima of pairs, then functions matching prescribed values at two points, and only then the local-to-global patching over a finite subcover. Each step is short; keeping the uniform closure a lattice and an algebra simultaneously is the bookkeeping burden.
Two hypotheses are easy to lose and both are necessary: an algebra that vanishes at a point cannot approximate functions that do not, and one that fails to separate two points cannot approximate functions that distinguish them.
Conventions fixed by this mission:
TendstoUniformlyOn … atTop; complex-valued sequences are
used where Rudin allows complex values.Rudin.IsFunctionAlgebra, Rudin.SeparatesPointsOn, Rudin.VanishesAtNoPointOn,
Rudin.UniformClosureOn, defined for sets of functions X → ℝ and a compact subset K.
The goal's conclusion is membership in the uniform closure, i.e. the existence of an
approximating sequence from the algebra.Rudin.EquicontinuousOn,
Rudin.PointwiseBoundedOn, Rudin.UniformlyBoundedOn, stated with explicit and
as in Definitions 7.19 and 7.22.The discrete-time Riccati equation is the central object of linear-quadratic optimal control — the design equation behind LQR/LQG controllers in every modern control stack. Proposition 4.4.1 of Bertsekas, Dynamic Programming and Optimal Control, Vol. I (3rd ed., 2005, §4.1) packages its asymptotic theory: under controllability and observability the Riccati iteration converges to the unique positive semidefinite solution of the algebraic Riccati equation and the resulting closed loop is stable. Alongside it, Lemma 4.2.1 of §4.2 develops K-convexity, the analytical engine behind Scarf's optimality of inventory policies — a foundational result of operations research. Neither the Riccati asymptotics nor K-convexity exists in Mathlib.
Matrices , , , . The Riccati operator (BertsekasRiccatiMap)
is controllable if has rank (BertsekasControllablePair); is observable if is controllable (BertsekasObservablePair). Separately, is -convex (BertsekasKConvex, Def. 4.2.1) if for all , , .
with — BertsekasDP.riccati_convergence_stability (goal). Milestones: Lemma 4.2.1(a)–(d) (kconvex_of_convex, kconvex_combination, kconvex_expectation, kconvex_sS_structure), culminating in the structure theorem for continuous coercive -convex functions.
The Riccati result is the mathematical license behind steady-state LQR design: it guarantees the design equation has one meaningful solution, that iterating the finite-horizon recursion finds it, and that the resulting feedback is stabilizing. Formally it would seed a Mathlib-adjacent theory of matrix fixed-point iterations, positive semidefinite order, and spectral-radius stability. The K-convexity milestones are self-contained real analysis, each of independent reuse value for inventory theory; part (d) is the engine of -policy optimality. All results are classical and proved in the book; the formal work is new.
The Riccati proof interleaves monotonicity of on the psd cone, boundedness from controllability (a steering argument), positivity from observability, and stability extracted from the fixed-point identity via a Lyapunov argument — several pieces of matrix analysis (psd order, congruence, Schur-type manipulations, spectral radius vs. convergence of powers) that must be built or located in Mathlib. The naive route of diagonalizing fails: nothing is symmetric about . For Lemma 4.2.1(d), the difficulty is that is not convex: the minimizer structure must come from the K-convexity inequality applied at carefully chosen points, plus continuity and coercivity.
Real matrices over Fin n; Matrix.PosSemidef/PosDef; matrix inverse is Mathlib's total inverse (zero on singular input — harmless here since along the relevant iterates, which the proof must establish); convergence in the entrywise topology; eigenvalues via spectrum ℂ of the complexified matrix, all strictly inside the unit circle. Rank-based controllability exactly as Def. 4.1.1. K-convexity is stated for all real ; note is forced whenever it is satisfiable (), and the expectation milestone is stated for finitely supported disturbances (integrability automatic).
The Pontryagin Minimum (Maximum) Principle is the fundamental necessary condition of optimal control, in continuous use since 1956 across aerospace guidance, robotics, and mathematical economics. Chapter 3 of Bertsekas, Dynamic Programming and Optimal Control, Vol. I (3rd ed., 2005) develops it from the dynamic programming side: the HJB sufficiency theorem (Prop. 3.2.1), an envelope lemma (Lemma 3.3.1), the Minimum Principle itself (Prop. 3.3.1), and its discrete-time counterpart (Prop. 3.3.2). Mathlib's optimal-control coverage is currently near zero — no HJB equation, no adjoint equations, no maximum principle — which makes this the mission with the largest gap between textbook maturity and formal coverage in the series.
Minimize, over admissible pairs, the cost
with continuously differentiable (BertsekasCTModel). Admissible controls are piecewise continuous on — formalized as: bounded image and continuous off a finite set (BertsekasPiecewiseContinuousOn) — and state trajectories are continuous, satisfying the ODE off a finite set (BertsekasCTAdmissibleFrom, parametrized by an arbitrary start ). The Hamiltonian is (BertsekasHamiltonian).
For an optimal admissible pair : there exist an adjoint and a constant with
away from finitely many times — BertsekasDP.pontryagin_minimum_principle (goal). Milestones: Prop. 3.2.1 (hjb_sufficiency_of_continuous), Lemma 3.3.1 (envelope_gradient_lemma), Prop. 3.3.2 (discrete_minimum_principle).
The HJB milestone carries the hypotheses that and are jointly continuous — the consequence of the §3.1 standing assumptions that its proof uses. An earlier version without any regularity hypothesis was disproved: with a discontinuous running cost the cost integrand need not be integrable, and the library's integral of a non-integrable function is .
The Minimum Principle converts an infinite-dimensional optimization into a two-point boundary value problem — the basis of shooting methods and of every "bang-bang" analysis. None of it exists in Mathlib; even the HJB verification theorem would be new. The discrete-time milestone is self-contained multivariable calculus and gives early value; the envelope lemma is reusable well beyond control theory. The results are classical (Pontryagin et al. 1962; the book's Chapter 3); the formal proof of Prop. 3.3.1 will need an honest variational argument — the book's own HJB-based derivation is explicitly informal.
For the goal: the classical proofs go through needle variations and a separation argument, or through regularity of the value function — neither is in Mathlib. The book's derivation assumes differentiability of the optimal value function, which is not a hypothesis of the statement; a formal proof must either supply a rigorous variational argument or add intermediate lemmas as new platform problems (sketching is encouraged). For the HJB milestone, the work is differentiating along a trajectory that satisfies the ODE only off a finite set, then integrating.
States and controls in EuclideanSpace ℝ (Fin n) / (Fin m); gradients in Mathlib's gradient; the ODE and adjoint via HasDerivAt off a finite exceptional set; costs via intervalIntegral. Piecewise continuity includes boundedness of the image, so the cost integrand of an admissible pair is genuinely integrable — the junk-value escape (non-integrable integrand ⇒ integral 0) is closed. Fixed initial state, fixed terminal time, free terminal state; time-independent dynamics (so the Hamiltonian is constant, per the book's remark that time-varying systems lose constancy). is an arbitrary set — no compactness or convexity is assumed in the goal.
Pontryagin's principle as presented by Luenberger is the decisive necessary condition in continuous-time optimal control. It converts an optimization over functions into a pointwise comparison of a Hamiltonian, coupled to the original state equation and a backward costate equation. Luenberger derives the minimum-Hamiltonian convention from vector-space multiplier ideas and a first-order comparison principle. Formalization is especially valuable here because the printed theorem contains a standard but consequential regularity oversight: it asserts a condition at every time even though controls are only piecewise continuous and the cost is an integral. This mission preserves the intended theorem while replacing that false pointwise claim by the mathematically canonical almost-everywhere statement.
Fix t₀ < t₁, a finite-dimensional Euclidean state space OCState n, a Euclidean control space OCControl m, and a permitted-control set Omega. A state-control pair (x,u) is admissible when x t₀ = xInit, the state is absolutely continuous on the interval, the control is almost everywhere strongly measurable and lies in Omega almost everywhere, the differential equation x' = F(x,u) holds almost everywhere in the interior, and the running cost is interval integrable. An optimal pair globally minimizes the interval integral among all admissible pairs.
The dynamics F and running cost ell are continuous jointly in state and control and continuously differentiable in the state variable. Their state derivatives Fx and ellx vary continuously. A global Lipschitz estimate controls changes of F in both state and control. Because an a.e. measurable control need not be bounded, the optimal control is explicitly assumed to have an a.e. norm bound on the compact interval, matching the boundedness inherited from the source's piecewise-continuous model. The operator-valued paths Fx (x₀ t) (u₀ t) and ellx (x₀ t) (u₀ t) are also assumed interval integrable along the optimum. Together these hypotheses provide the measure-theoretic regularity needed for the adjoint and state perturbations. The Hamiltonian uses Luenberger's minimum convention,
The root VectorSpaceOpt.pontryagin_minimum_principle asserts the existence of an absolutely continuous costate lambda with terminal value lambda t₁ = 0. Almost everywhere it satisfies the weak inner-product form of
and almost everywhere on the control interval it satisfies
Two milestones capture source dependencies. control_state_lipschitz_estimate is the Grönwall stability estimate used on p. 263 to control the state response by the integral distance between controls; it explicitly assumes interval integrability of both the state-difference norm and the control-difference norm, so Mathlib's totalized integral cannot hide a nonintegrable input. adjoint_lagrangian_comparison formalizes §9.6, Proposition 1: under an implicit state equation, differentiability in the state, Lipschitz dependence of the state solution, and an adjoint identity, the objective difference agrees with a frozen-state Lagrangian difference up to an explicit filter-level little-o remainder.
This is the flagship analytic mission of the continuation. It connects finite-dimensional differential calculus, Bochner integration, absolute continuity, ODE constraints, adjoints, and localized control variations in one reusable theorem. The definitions form a minimal control framework that can support terminal costs, endpoint constraints, and alternative maximum-principle conventions later. The corrected a.e. conclusion also demonstrates a central benefit of formalization: informal conventions about representatives of controls and isolated time values must be resolved before a theorem can be accepted.
The weak inner-product adjoint equation avoids introducing a coordinate transpose and remains invariant under the Euclidean-space representation. That choice makes the result immediately reusable in later vector-space treatments of transversality and endpoint multipliers.
The difficulty is very high. Mathlib supplies finite-dimensional calculus, interval integration, absolute continuity, measure-theoretic almost-everywhere statements, and Grönwall tools, but not an assembled Pontryagin framework. The mission must coordinate a state-solution stability estimate, state differentiability of the dynamics and cost, existence and regularity of the backward costate, and Hamiltonian comparison against arbitrary admissible values. The control is measurable rather than globally continuous, so every pointwise expression must be placed under an a.e. quantifier where appropriate. The proposition milestone additionally requires a precise little-o interface instead of an unnamed asymptotic remainder.
The proposal covers §9.6, Proposition 1 and Theorem 1, with the regularity inherited from the surrounding discussion made explicit. Both the optimal state and the costate are absolutely continuous. Admissible controls are a.e. strongly measurable, which is a broader measure-theoretic proxy for the source's piecewise-continuous controls and is compatible with integral objectives; the root additionally requires the optimal control to be essentially norm bounded on Icc t₀ t₁, restoring the compact-interval boundedness used by the source. The maps F, ell, Fx, and ellx are jointly continuous; state derivatives are supplied by HasFDerivAt; a uniform Lipschitz bound is stated; and both derivative coefficients along the optimal path are interval integrable. The separate Grönwall milestone requires its state and control norm differences to be interval integrable. The interval is required to have positive length.
There is a documented source erratum. The sentence on printed p. 263 states Hamiltonian minimality for every t, while the proof on p. 264 chooses a neighborhood on which a purported strict violation persists. That step requires continuity at the selected time. Moreover, changing a piecewise-continuous control at a single isolated time changes neither its a.e. class, the state equation, nor the integral cost. Therefore no condition can be forced at an arbitrary jump value. The Lean root uses an a.e. conclusion on Icc t₀ t₁; an alternative source-faithful repair would assert the inequality at every continuity point of u₀. The mission does not claim existence of an optimal pair, compactness of Omega, endpoint constraints, nonsmooth dynamics, or a sufficiency theorem.
AI generated but i think correct. I think the milestones make it really annoying but the central theorem looks correct.
The matrix-multiplication exponent measures the asymptotic number of field operations needed to multiply two square matrices. A bound means that, for every , two matrices can be multiplied using arithmetic operations. Matrix multiplication is a central benchmark in algebraic complexity and a primitive for many algorithms in linear algebra, graph theory, and symbolic computation.
After Strassen showed that , a sequence of tensor constructions reduced the exponent further. Schönhage's asymptotic sum inequality made it possible to exploit simultaneous matrix products rather than a single square product. In 1990, Don Coppersmith and Shmuel Winograd combined an explicit low-border-rank tensor with a block extraction argument based on Salem--Spencer sets. Their basic analysis gave ; coupling the random weights in the tensor square sharpened this to , hence the exact rational consequence .
This mission formalizes that historical Coppersmith--Winograd result. It follows the source tensor and its actual block restrictions, while excluding placeholder “laser values” that are not backed by extracted direct sums of matrix-multiplication tensors.
For a field , an order-three tensor is represented by three finite-dimensional -vector spaces and an element of their tensor product. The matrix-multiplication tensor
encodes multiplication of an matrix by a matrix. A restriction applies one linear map to each tensor leg. A degeneration permits those maps to depend polynomially on a formal parameter and selects their first nonzero coefficient. Thus a degeneration from the diagonal tensor is a border-rank certificate .
The Coppersmith--Winograd tensor with parameter is
It has border rank at most . Its coordinates carry three classes, indexed by , and its six nonzero block types are
The first three blocks are matrix-multiplication tensors with dimensions , , and ; the other three are scalar products. Tensor powers therefore contain many typed rectangular matrix products. The laser method selects a large family with disjoint coordinate blocks and applies Schönhage's asymptotic sum inequality to all surviving products simultaneously.
For every field ,
The Lean goal has the same quantified proposition and the same matMulExp definition as the existing Schönhage-bound mission; only the theorem identifier and rational endpoint change.
The development records the characteristic-free order-three degeneration
and the exact matrix-product dimensions associated with every supported type sequence in . These statements identify the algebraic input before any asymptotic counting is used.
For , the tensor-square grading and the coupled-weight pruning must produce the direct sums and asymptotic inequality stated in Section 8 and in the coupled-constituent lemma on journal pp. 270--272. The final numerical milestone certifies the rational endpoint from exact inequalities, rather than treating the decimal as a proof object.
The result was the strongest matrix-multiplication bound for roughly two decades and introduced the tensor family that underlies the classical laser-method line of work. A formal proof supplies a checked bridge from an explicit border-rank identity to an exponent bound whose combinatorial extraction is substantially more delicate than the earlier Schönhage examples.
The formalization also produces reusable infrastructure. The order-three CW degeneration is an explicit polynomial-family test case over arbitrary fields. The six block identifications and type-count formulas can be reused in analyses of tensor powers. A faithful extraction predicate, stated through actual restrictions to direct sums of MMObj tensors, separates sound laser arguments from formulas that count incompatible or coordinate-sharing blocks as independent.
The mathematical bound is known. The open work is its machine-checked reconstruction in Lean. The border-rank theorem, per-type matrix-product restriction layer, tensor-square support invariant, balanced block calculation, Salem--Spencer set theorem, and exact numerical endpoint are already proved. The unrestricted value/rank bridge, the coupled-constituent extraction, and the full Section 8 auxiliary inequality remain the substantive frontier.
The main difficulty is not expanding or evaluating a decimal logarithm. A tensor power contains exponentially many typed terms, but most share variables. They cannot all be placed in a direct sum, and counting all joint type sequences overestimates the usable matrix products. The source hashes coordinate blocks into a large progression-free set and prunes collisions so that the surviving blocks are genuinely independent.
The improvement adds a second layer. It begins with , regroups variables into five classes, couples weights that were independent in the simpler analysis, and estimates a nontrivial central block by a further extraction. A formal proof must track the direction of every restriction, the exact multiplicities of all block types, and the loss introduced by pruning. Replacing exponential surviving-block counts by a polynomial number of blocks, or using joint entropy without the marginal compatibility constraints, changes the mathematical claim and is outside the mission.
The mission uses the existing TensorObj, MMObj, TensorObj.Restrict, Degenerates, tensorAsymptoticRank, matMulExp, and matMulExp_strassen declarations in the Mathlib environment pinned by the earlier matrix-multiplication mission. Tensor dimensions and type counts are natural numbers; exponent and optimization inequalities are real-valued. All top-level bounds quantify over an arbitrary field, matching the integral polynomial identities used by the construction.
Laser statements must exhibit, directly or through a faithful reusable predicate, restrictions from a tensor power to a finite direct sum of concrete matrix-multiplication tensors. The number and dimensions of the summands remain part of the witness. A constant-valued “laser functional,” a vacuous witness hypothesis, or a capacity definition that discards the exponential number of surviving blocks does not satisfy the mission.
Welcome contributions include restriction composition lemmas, tensor-power block equivalences, multinomial and entropy estimates with all marginal constraints, formal Salem--Spencer pruning, exact real-inequality certificates, and the coupled central-block value lemma. Every milestone should cite the corresponding equation, table, or lemma in the primary paper.
The whole series so far lived in discrete time on finite state spaces. Chapters 20–21 of Levin–Peres–Wilmer, Markov Chains and Mixing Times (AMS, 2009) lift both restrictions. Running the jumps of a chain at the arrivals of a rate-one Poisson clock produces the continuous-time chain, whose transition semigroup — the heat kernel — converges to stationarity for every irreducible chain, with no aperiodicity hypothesis: continuous time washes out periodicity. On countable state spaces, existence of a stationary distribution is no longer automatic, and the trichotomy of transience, null recurrence, and positive recurrence replaces it; the convergence theorem survives exactly on the positive-recurrent class. The chapter's crown jewel — and this mission's goal — is Pólya's theorem: simple random walk on the lattice is recurrent in dimensions one and two and transient in dimension three and higher. "A drunk man will find his way home, but a drunk bird may get lost forever."
Continuous time (Ch. 20). For a finite chain , the heat kernel at time is defined by Poissonization,
the law at time of a walk taking -steps at Poisson arrival times ( as a matrix exponential). With , the continuous distance and mixing time are and . The lazy version of a discrete chain is ; from Mission VII, the spectral gap is with the largest eigenvalue . The product chain on a product of coordinate spaces picks a uniform coordinate and updates it by that coordinate's chain.
Countable state spaces (Ch. 21). A chain on a countable state space is a function with nonnegative entries and rows summing to one (as convergent series); -step probabilities are defined recursively, and trajectory probabilities are countable sums of path weights. The first return time to is ; a state is recurrent when (tails tend to zero), positive recurrent when moreover (tails summable), and null recurrent when recurrent but not positive recurrent. A stationary distribution is a nonnegative summing to one with (as convergent series). Simple random walk on steps from to one of its nearest neighbours uniformly at random.
Pólya's theorem (§21.2, Examples 21.8–21.9), the capstone of Chapters 20–21:
The results. Theorem 20.1 explains why laziness and aperiodicity pervade the discrete theory — periodicity is an artifact of the discrete clock. The product-chain theorem 20.7 is the cleanest instance of the paradigm (independent coordinates mix in relaxation time ) and the template for the hypercube cutoff of Mission XI. Chapter 21's trichotomy is the backbone of applied Markov chain theory — queueing, branching, renewal — and Kac's lemma with the convergence theorem 21.14 is the standard equipment of any probability course. Pólya's theorem is one of the most celebrated results of twentieth-century probability, the birth of the random-walk-in-dimension- paradigm.
Formalizing them. Mathlib has no continuous-time Markov chains, no Poissonization, and no recurrence/transience theory (its PMF random walks stop far short). The countable-state layer built here — summable stationary equations, tail-sum return times, the recurrence dichotomy — is the missing infrastructure for formalized applied probability; Pólya's theorem is a famous target in its own right, and the half has never been formalized in any assistant to our knowledge.
The heat kernel is an infinite series of matrices: convergence (dominated by the Poisson weights), the semigroup property, and the interchange of the series with matrix products and limits must all be established by hand over tsum. Theorem 20.1 avoids aperiodicity by the number-theoretic fact that the Poisson distribution smears over residue classes — formally, the continuous chain is automatically aperiodic because for . The product-chain bounds need the machinery of Mission VII applied coordinatewise and a careful union bound; the lower bound is a Gaussian-free second-moment argument. On the countable side, everything is series bookkeeping in the absence of Fintype: the recurrence dichotomy is a generating-function (renewal) identity handled through partial sums; Kac's lemma is a mass-transport double-count over trajectories; and Theorem 21.14 needs an aperiodicity-based coupling on a countable product space, the technical summit of the mission. Pólya's theorem itself combines a local central-limit-type estimate for the return probabilities (, obtained by Stirling in and by a comparison argument in higher dimension) with the dichotomy of Proposition 21.3.
Chapter 20 lives on finite state spaces: the heat kernel is a tsum over of Poisson weights times matrix powers (summability is provable, not assumed), continuous distance is a supremum over states, and the continuous mixing time is an sInf over nonnegative reals (junk if the set were empty — excluded under the theorems' hypotheses). Discrete-vs-continuous comparison (Theorem 20.3) is stated with eventual thresholds (), matching the book's asymptotic phrasing. Chapter 21 lives on a Countable type: stochasticity and stationarity are HasSum statements, -step powers are defined recursively with tsum convolutions, return-time tails are countable sums of path weights over finite horizons, and recurrence/positive recurrence are the tail-limit and tail-summability conditions above — measure theory never enters. Pólya's theorem is stated for the origin of with the walk defined by nearest-neighbour steps; the and halves are separate conjuncts of one statement.
How fast does a Markov chain forget its starting point? For a reversible chain the complete answer is coded in the eigenvalues of its transition matrix: the largest eigenvalue is always , and the size of the gap between and the rest of the spectrum is the chain's fundamental time constant — a large gap means fast mixing, a small gap means slow mixing. Chapters 12–13 of Levin–Peres–Wilmer, Markov Chains and Mixing Times (AMS, 2009) develop this spectral theory and culminate in the discrete Cheeger inequality of Jerrum–Sinclair and Lawler–Sokal, which says that the spectral gap (an analytic quantity, defined below) and the bottleneck constant (a geometric quantity from Mission IV, also recalled below) control each other:
A chain mixes rapidly exactly when its state space has no bottleneck. This inequality is the backbone of the Markov-chain approach to approximate counting and of spectral graph theory at large; alongside it the chapters provide Wilson's method — the sharpest general technique for mixing-time lower bounds — and the comparison machinery that transfers spectral estimates between chains.
All chains live on a finite state space . A chain with transition matrix and stationary distribution is reversible when the detailed balance equations hold; reversibility is the standing assumption of both chapters. The yardsticks of the series are the total variation distance , the worst-case distance to stationarity , and the mixing time , with ; we write .
The spectral vocabulary: an eigenfunction of is a nonzero with , where ; the number is then an eigenvalue. Out of the spectrum one forms
Functions on carry the weighted inner product — the geometry, denoted , in which a reversible is self-adjoint — and the Dirichlet form
the average squared variation of along the chain's transitions. Finally, from Mission IV: the bottleneck ratio of a set of states is , the conditional probability at stationarity of escaping in one step, and the bottleneck constant is .
Theorem 13.14, the discrete Cheeger inequality: for a reversible irreducible chain,
The results. Theorems 12.3–12.4 sandwich the mixing time between and — the fundamental equivalence of spectral and mixing estimates for reversible chains, prerequisite for the cutoff criterion of Mission XI. The Cheeger inequality converts isoperimetry into spectral bounds; it is the mathematical core of the Jerrum–Sinclair program of polynomial-time approximate counting, and its graph version underlies expander theory. Wilson's method produced the sharp lower bounds for adjacent transpositions and hypercube-type chains; the comparison lemma is the engine behind the shuffle bounds cited in Mission V (§16.1).
Formalizing them. Mathlib has the spectral theorem for symmetric matrices but nothing connecting spectra to Markov chains: no spectral gap, no relaxation time, no Dirichlet forms, no Cheeger inequality in any form. A formalized discrete Cheeger inequality would be a landmark reusable well outside this series (spectral graph theory, expanders); the eigenvalue and Rayleigh-quotient layer built here is what Missions IX (tree relaxation, block dynamics) and XI (cutoff criterion) consume.
Everything routes through one change of basis: conjugating by the diagonal matrix with entries produces a matrix that is symmetric precisely because the chain is reversible, so Mathlib's spectral theorem applies — but transporting the resulting eigenbasis back to , keeping track of orthonormality with respect to the weighted inner product, is a genuine formal-linear-algebra project; nothing about it is deep, all of it is fussy. The definitions of and as suprema over the set of non-unit eigenvalues (finite, and nonempty once ) must be reconciled with the eigenbasis enumeration before any variational argument runs. The upper half of Cheeger is direct from the variational characterization — test it on the indicator function of a bottleneck set , recentred to have mean zero; the lower half is the hard half: the standard proof takes an optimal , decomposes it over its level sets , and applies Cauchy–Schwarz twice, and formalizing that level-set sweep is the main effort of the mission. Wilson's method needs a supermartingale-style iteration of the eigenfunction estimate; its constants are exact, so the inequalities cannot be rounded.
Eigenvalues are defined by real eigenvectors (); for reversible chains this captures the whole spectrum, and all statements assume reversibility wherever the book does. and are suprema of explicit sets of reals; on a one-point space these sets are empty and the supremum takes a junk value, so the affected statements carry the explicit hypothesis , matching the book's implicit assumption of a non-degenerate chain. with total inverse. Theorem 12.3 carries an explicit absorbing the rounding of a real-valued bound to an integer time. The cycle eigenvalue statement exhibits eigenvalues (existence of eigenfunctions); completeness of that list is not asserted. The variational characterization asserts both the minimization identity and its attainment, so it can be used in either direction.
Welcome contributions: the symmetrization API (conjugation by ), Rayleigh-quotient lemmas, level-set (layer-cake) infrastructure — all reused by Missions IX and XI.
Missions II–III produce upper bounds on mixing times. Whether such a bound is sharp is a different question: an bound on a chain that actually mixes in steps hides the truth. Chapter 7 of Levin–Peres–Wilmer, Markov Chains and Mixing Times (AMS, 2009) develops the standard toolkit of lower bounds: the counting and diameter bounds (a chain cannot spread faster than its transition graph allows), the bottleneck ratio (a chain cannot mix faster than it crosses its worst cut), and distinguishing statistics (a chain is far from stationarity as long as some statistic separates from by several standard deviations). The bottleneck bound — closely related to the conductance of the chain and, via Mission VII, to the Cheeger inequality — is the single most important obstruction result in the subject: it is how slow mixing (torpid mixing of Ising at low temperature, in Mission IX) is proved.
For a chain with stationary distribution , the edge measure is , the bottleneck ratio of a set of states is
and the bottleneck ratio of the chain is . The maximal one-step out-degree is ; the diameter is measured in the graph joining when . For a statistic and distribution , and are the finite-sum expectation and variance, and denotes the pushforward of under .
This is Theorem 7.3, the bottleneck-ratio lower bound, the chapter's central theorem.
The counting bound for chains with uniform stationary distribution (§7.1.1, display (7.2)); the diameter bound: any two states satisfy for (§7.1.2, display (7.3)); Proposition 7.8 (a statistic separating means by standard deviations forces ); Lemma 7.9 (projection under a statistic does not increase TV distance); Proposition 7.13 (the lazy hypercube walk satisfies ); and Proposition 7.14 (the top-to-random shuffle needs shuffles, matching the upper bound of Mission III).
The results. Together with Mission III this pins the top-to-random shuffle at — the first sharp mixing result of the series, and the prototype of the cutoff phenomenon formalized in Mission XI. Proposition 7.13 similarly matches the hypercube upper bound and feeds the cutoff analysis. The bottleneck bound is used in Mission IX to prove exponentially slow mixing of the mean-field Ising model at low temperature, and its two-sided refinement is the Cheeger inequality of Mission VII.
Formalizing them. Mathlib has no notion of conductance/bottleneck ratio of a chain, no distinguishing-statistic method, and no mixing-time lower bound of any kind. The pushforward and variance infrastructure over finitely supported distributions is elementary but new, and reusable wherever second-moment methods appear (Wilson's method in Mission VII).
The bottleneck theorem's proof is short but exact: it hinges on the identity for conditioned on , followed by a telescoping estimate of ; the formal cost is manipulating conditioned measures and one-sided TV sums (Remark 4.3 from Mission II). For Proposition 7.8, the second-moment argument runs through Chebyshev on both distributions plus optimization of a threshold — the constants are exact, not asymptotic, so the formal inequalities must be done carefully. Proposition 7.13 requires the binomial mean/variance computation for Hamming weight under both and , including the negative-correlation bound for unrefreshed coordinates. The naive route to a lower bound — "the chain has not left a small set, so it is far from " — is precisely the counting bound and is too weak for the sharp results; the statistics method is what closes the gap.
is an infimum over the subtype of nonempty sets with ; on a one-point space this subtype is empty and the infimum takes a junk value, making the goal trivially true there (the bound carries content only for , as in the book). The counting bound divides by with total division ( gives a trivially true statement). The diameter bound is stated for arbitrary pairs of states through SimpleGraph.dist of the transition graph, which subsumes the book's diameter formulation. Propositions 7.13 and 7.14 are stated for all integer times (resp. ), using monotonicity of instead of evaluating at a real-valued time — this avoids floor artifacts while keeping the book's content. Proposition 7.14 quantifies " large, then large" exactly as the book's iterated limit.
Welcome contributions: monotonicity of in ; conditioned-measure lemmas; variance API for distExp/distVar.
The Convergence Theorem of Mission II says an irreducible aperiodic chain mixes geometrically, but with constants coming from a crude Doeblin decomposition — useless for actual chains, whose state spaces are exponentially large. Chapters 5–6 of Levin–Peres–Wilmer, Markov Chains and Mixing Times (AMS, 2009) develop the two classic probabilistic techniques that give useful upper bounds: coupling — run two copies of the chain jointly so that they meet quickly, and read a TV bound off the meeting time — and strong stationary times — random times at which the chain is exactly stationary, independent of the time. The flagship application is the top-to-random shuffle: repeatedly take the top card of a deck of cards and reinsert it at a uniform position; the deck is well mixed after shuffles, with error at most .
A Markovian coupling of a chain (with the stay-together convention (5.2)) is a chain on pairs whose coordinate marginals are both and which moves diagonal states to diagonal states. The coupling time is the hitting time of the diagonal; its tails are expressed with the trajectory calculus of Mission I.
A randomized stopping time is presented by its stopping rule: for each time and trajectory prefix , a number , the conditional probability of stopping at given the trajectory so far and no earlier stop. A strong stationary time for the chain started at is an almost surely finite such with
i.e. independent of . The separation distance is .
The mission also fixes the concrete chains it bounds: the lazy walk on the discrete torus , the Metropolis chain on proper -colorings of a graph, the Glauber dynamics of the hardcore model with fugacity , and the top-to-random shuffle on decks of cards (states are arrangements, i.e. permutations; position is the top).
Let ,
for the top-to-random shuffle on cards — display (6.16) of the book, the chapter's flagship bound, proved by combining the strong stationary time with the coupon collector tail of Mission I.
Theorem 5.2 and Corollary 5.3 (the coupling bound: , hence ); Theorem 5.5 ( for the lazy torus walk); Theorem 5.7 (Metropolis colorings, : mixing in ); Theorem 5.8 (hardcore Glauber, : mixing in ); Proposition 6.1 with Example 6.7 ( is a strong stationary time); Lemma 6.11 (); Lemma 6.13 (); Proposition 6.10 ().
The results. The coupling bound is the single most used upper-bound technique in the subject: Missions VIII (path coupling), IX (Ising) and XI (cutoff examples) all instantiate it. Strong stationary times and separation distance return in Mission XI (separation cutoff) and underlie perfect sampling in Mission XIII. The three concrete bounds (torus, colorings, hardcore) are the standard first applications and give the first polynomial mixing results of the series; the colorings and hardcore chains are the objects of intense ongoing research on sampling thresholds.
Formalizing them. Nothing here exists in Mathlib. The novel infrastructure is the stopping-rule formalization of randomized stopping times over trajectory prefixes — measure-theory-free, but expressive enough for the strong stationarity identity — and the Markovian-coupling predicate on pair chains. Both are reused later in the series (Matthews method, cutoff, CFTP).
The coupling bound itself is short once Proposition 4.7 (Mission II) is available; the work is in the applications. For the torus, the coordinatewise coupling requires assembling one-dimensional couplings and bounding the coupling time by a sum of one-dimensional meeting times — the formal bookkeeping of "couple coordinate by coordinate" is the real cost, and the constant absorbs it. For Theorem 5.7 and 5.8 the argument is a grand coupling over all colorings/configurations simultaneously; the formal statements quantify only over the resulting bound, but a solver must build the coupling. For Proposition 6.1, the crux is the induction "given cards under the original bottom card, all orders are equally likely" — an exchangeability argument that must be carried through the stopping-rule encoding. Lemma 6.11 is where the definition of strong stationarity does its work; the naive attempt to prove Proposition 6.10 directly from the coupling characterization fails, which is exactly why separation distance is introduced.
Couplings of chains are transition matrices on with marginal conditions stated row by row; the stay-together convention is part of the predicate, matching (5.2). Stopping rules take the trajectory prefix (which includes the starting state), so times "depending on the starting position" are covered; strong stationarity packages the stopping rule bounds, almost-sure finiteness (), and the product identity. The colorings chain lives on the subtype of proper colorings; the hardcore chain is the Glauber dynamics of Mission II restricted to the subtype of hardcore configurations (transitions never leave it). Mixing-time upper bounds carry an explicit for integer rounding where the book's real-valued display would otherwise be false for the integer-valued . The torus statement fixes ; for near the display is false as stated in the book.
Welcome contributions: interface lemmas between setAvoidTailProb of the pair chain and the two coordinates; the taboo-matrix form of coupling-time tails; exchangeability infrastructure for the deck chains (reused in Mission V).
Two quadratic functions can be compared losslessly. The S-procedure says that, when the constraint is strictly feasible, the implication
holds if and only if a single nonnegative multiplier certifies it as a matrix inequality, for some . It is a cornerstone of control theory, trust-region methods and robust optimization, and a rare case in which a nonconvex problem has zero duality gap. The route runs through the theory this mission builds from Boyd & Vandenberghe §5.8–5.9 and Appendix B: strong alternatives for convex inequality systems, cone-program strong duality under a generalized Slater condition, semidefinite programming duality, the LMI theorems of alternatives, and the hidden convexity of the joint range of two quadratic forms.
Log-concave functions are the meeting point of convex analysis and probability: densities of Gaussian, exponential, uniform and Wishart distributions are all log-concave, and countless facts of applied probability flow from one structural theorem — integrating out variables preserves log-concavity. This mission builds the convex-analysis spine of Boyd & Vandenberghe's Convex Optimization (Chapters 2–3) — separation and supporting hyperplanes, dual cones, the first- and second-order differential characterizations of convexity, Fenchel conjugacy — and climbs to Prékopa's theorem via the Prékopa–Leindler inequality, a landmark of Brunn–Minkowski theory absent from Mathlib.