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.
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?
For a real-analytic function on an open set and a critical point (so ), the Łojasiewicz gradient inequality says that there is an exponent such that stays bounded near . It is the standard tool for proving that bounded gradient trajectories have finite length and converge to a single critical point, and, in its descendants (the Kurdyka–Łojasiewicz property), for proving convergence of the whole iterate sequence of nonconvex descent methods: proximal gradient, alternating minimization, PALM, ADMM. Those algorithmic results all assume a nonsmooth version of the inequality, for functions that may take the value and are not differentiable.
Bolte, Daniilidis and Lewis (SIAM J. Optim. 17 (2007)) supplied that nonsmooth version. This mission formalizes their first main result, Theorem 3.1: the inequality at critical points of subanalytic functions that are continuous on a closed domain.
Timeline.
Write with its Euclidean norm. A function has domain .
Subanalytic sets (Definition 2.1). A set is semianalytic if every point of has a neighbourhood on which with real-analytic on . It is subanalytic if every point of has a neighbourhood such that is the projection onto of a bounded semianalytic subset of , . A function is subanalytic if its graph is subanalytic. Semialgebraic functions, and functions locally built from analytic ones by finitely many algebraic operations, max/min and compositions, are subanalytic.
Subdifferentials (Definition 2.10). The Fréchet subdifferential is the set of with (empty off ). The limiting subdifferential is the set of limits of along with .
Slope and critical points. The nonsmooth slope is , equal to when (equation (4)). The critical set is (Definition 2.11).
Let be subanalytic with closed domain and continuous, and let . Then there is such that
with the conventions and . In division-free form: there are and a neighbourhood of with for all and . The exponent is existential; the goal fixes no value of or .
The result. Theorem 3.1 is the nonsmooth Łojasiewicz inequality at critical points. With the subgradient in place of the gradient, it yields finite length of bounded trajectories of subgradient systems (Section 4 of the paper) and is the template for the Kurdyka–Łojasiewicz property that underlies convergence proofs for proximal and splitting methods on nonconvex, nonsmooth problems (e.g. Attouch–Bolte–Redont–Soubeyran 2010, Bolte–Sabach–Teboulle 2014). Those papers assume the KL property and cite this line of results to know it holds for semialgebraic and subanalytic objectives.
Formalizing it. The theorem is proved; this mission produces a machine-checked proof. To our knowledge no proof assistant has a formal definition of subanalytic sets or of the nonsmooth Łojasiewicz inequality. The definitions layer (semianalytic and subanalytic sets, the slope, the inequality) is reusable by any later formalization of KL-based convergence analyses, and the milestones on Remark 2.12 are general facts about limiting subdifferentials that apply well beyond subanalytic geometry.
The obvious argument restricts and to an analytic curve and compares their Puiseux expansions. That step needs three pieces of subanalytic geometry that no library has: curve selection, the structure of one-variable subanalytic functions (monotonicity and Puiseux expansions), and the fact that the sets built in the proof (sets of points with a subgradient satisfying an inequality, level-wise infima of ) are again subanalytic, which in the paper goes through global subanalyticity and the projection theorem. The second obstacle is that is not smooth: the classical proof differentiates along a curve, while here only Fréchet subgradients are available, and the chain rule along an analytic curve holds only almost everywhere. The constancy of on critical components, equation (6), is itself a nonsmooth Sard-type theorem whose published proof uses stratification. A solver who replaces subanalytic by semialgebraic, or assumes real-valued and , proves a different and much weaker statement.
EuclideanSpace ℝ (Fin n). The function is f : E → EReal with f x ≠ ⊥ for every x. The domain is {x | f x ≠ ⊤}; it is assumed closed, and f is assumed ContinuousOn it.NonconvexSplitting.Shared.IsRegularSubgrad and LimitingSubdiff, which match Definition 2.10 for functions never equal to .AnalyticOnNhd ℝ. The boundedness of the semianalytic set in Definition 2.1(ii) is part of the definition: without it every projection of a semianalytic set would count.LojIneqAt f a θ: one constant and one neighbourhood of , quantified over all limiting subgradients. Under the value never works at a critical point, as under the paper's conventions.Policy gradient methods learn a parameterized policy directly, by stochastic gradient ascent on a scalar performance measure , instead of deriving the policy from learned action values. They are how reinforcement learning handles continuous action spaces, stochastic optimal policies and prior knowledge built into the policy's form, and they underlie REINFORCE (Williams, 1992) and the actor–critic family. Every such method needs an estimate of . The difficulty is that depends on in two ways: through the action choices in each state, and through the distribution of states those choices produce. The second effect depends on the unknown environment dynamics.
The policy gradient theorem (Sutton, McAllester, Singh and Mansour, 2000; Marbach and Tsitsiklis, 2001) gives as an expectation over the on-policy state distribution that involves no derivative of that distribution. Chapter 13 of Sutton and Barto's Reinforcement Learning: An Introduction (2nd ed., 2018) states it as Eq. (13.5), proves it in a box for the episodic case (p. 325) and in a second box for the continuing case (pp. 334–335), and builds REINFORCE, REINFORCE with baseline and actor–critic methods on it. This mission formalizes that chapter's theorem and the identities around it, in the book's own model.
A finite episodic MDP has a finite set of nonterminal states, a terminal state, a finite action set , a finite reward set and dynamics : for each nonterminal and action , a probability distribution over next state and reward . The terminal state is absorbing and pays nothing. Write and for the expected reward.
A differentiable policy parameterization assigns to every and state a distribution over actions, with differentiable. Under the nonterminal states form a substochastic chain with matrix ; . Episodes terminate when for all .
There is no discounting (, p. 324). The state value is the expected total reward from , with ; the action value is the expected total reward after taking in . The episode starts in a fixed state , and the performance is (13.4). The expected number of visits to in an episode is , and the on-policy distribution is (9.3).
In the continuing case there is no terminal state, is the average reward per step (13.15), is the steady-state distribution, and , are differential values, defined from the return (13.17).
If episodes terminate under , then is differentiable at and
with . The book writes and names the constant, the average length of an episode, in words (p. 326). The goal states it.
The theorem turns into a quantity that can be sampled by following the policy: weighting states by is what visiting them under does, and the log form makes the action sum an expectation over . REINFORCE (13.8), REINFORCE with baseline (13.11) and one-step and eligibility-trace actor–critic methods all rest on it, and so does their claim that the expected update is in the direction of the performance gradient (p. 329). The baseline identity is why a learned state value can reduce variance without introducing bias.
The results are proved, in the book and in the literature. What this mission adds is a machine-checked version in the book's model: random episode lengths with , vector parameters , four-argument dynamics, and values defined from expected returns. The platform already has a proved finite-horizon policy gradient theorem (policy_gradient_finite_horizon, with a baseline and log-form companion) for a fixed horizon , a scalar parameter and an expected-reward kernel; it does not cover the book's statement. The mission also makes explicit two points the text leaves informal: that episodes terminate, and what exact constant hides behind "".
The book's proof is a formal manipulation: differentiate the Bellman equation, substitute it into itself, and "unroll" infinitely often. Two steps are not justified on the page. First, it presupposes that exists; with the value is an infinite series whose convergence depends on through termination, so differentiability of at has to be established, and termination is assumed only at . Second, "repeated unrolling" is a limit: after unrollings a remainder is left over, and it vanishes only because . Differentiating the series for term by term is not an alternative shortcut without a uniform bound on the derivatives of .
In the continuing case the corresponding obstacle is the differentiability of the steady-state distribution and of the differential values, which the book's proof uses without comment; here they are part of what is to be proved, from ergodicity at alone.
Option S, with none the single terminal state (several terminal states can be merged, all having value 0). One action type for all states. lives in EuclideanSpace ℝ (Fin d), and is Mathlib's gradient; conclusions are HasGradientAt, so differentiability is asserted, not assumed.Reusable infrastructure: the episodic value layer (substochastic chains, expected visits, termination) is needed by any undiscounted episodic RL result; the soft-max and Gaussian eligibility computations are needed by every policy-gradient algorithm. Proofs of any milestone, and general lemmas on the differentiability of values and stationary distributions of parameterized finite Markov chains, are welcome.
Learning from a finite sample is useful only if changing the sample has a controlled effect on the learned predictor. Uniform stability asks for a bound on the change in loss at every test point when one training example is removed. Bousquet and Elisseeff use this property to obtain generalization bounds for learning algorithms, and identify regularization as a source of stability in methods built from reproducing kernels. The present mission isolates their result for a squared norm penalty in a reproducing kernel Hilbert space (RKHS). It concerns the sensitivity of the optimizer itself, before any probability bound on a random training sample is applied. The result is Theorem 22 of Bousquet and Elisseeff (2002).
Let be an input space, a label space, and a real reproducing kernel Hilbert space of real-valued predictors on . A kernel and a feature representative express the reproducing identity and . Thus . The source assumes that all diagonal kernel values satisfy .
A labeled example is . Its loss under is , where is a real-valued cost. Let be the set of predictions that some element of can produce at some input. The loss is -admissible when is convex for every label and for all and . Here is a nonnegative Lipschitz constant. The definition compares any two attainable predictions, even when they arise at different inputs.
Fix a sample , a deleted index , and a regularization weight . The paper's full and truncated objectives, with squared RKHS norm regularization, are
The factor in both objectives is . Let and be minimizers of these respective objectives over all of . The statements allow any minimizer satisfying the relevant global optimality condition; they do not choose one by an arbitrary fallback rule.
The central target is the explicit deletion stability estimate of Theorem 22. For every test point ,
Its four milestones follow the paper's route through Lemma 20, the point-evaluation inequality (25), and the two quantitative inequalities displayed in the proof of Theorem 22. In particular, the intermediate RKHS distance bound is when . The main theorem uses , so it does not need a choice of sign for . These numerical constants are part of the target, rather than placeholders for unspecified bounds.
The theorem supplies a deterministic, uniform sensitivity estimate for kernel methods trained by squared norm regularization. The bound applies simultaneously to every test example and decreases as either the sample size or the regularization weight increases. It is one of the ingredients that lets the paper apply its earlier stability-to-generalization results to concrete learning procedures. The loss need not be bounded for this theorem; bounding it is a separate question addressed later in the paper.
The result is proved in the source article. This mission asks for a machine-checked version of its exact pairwise claim and the reusable infrastructure around it: the paper's admissibility condition, the two objectives, the general regularizer inequality, and the RKHS evaluation bound. The existing Prove2Me library already has definitions for loss, empirical error, and the RKHS reproducing identity, so the new definitions concentrate on what is specific to these pages. The related replace-one estimate in Mohri, Rostamizadeh and Talwalkar's Foundations of Machine Learning uses a different perturbation and constant; it is not interchangeable with this result.
The two minimizers solve different objectives, and the deleted example appears in only one of them. A comparison of their objective values alone does not directly give a bound on their distance in the Hilbert norm. The source also distinguishes an abstract convex class of functions in Lemma 20 from the full RKHS used in Theorem 22. A proof must keep those domains straight while preserving the precise normalization of the truncated objective. Another delicate point is that the kernel bound controls evaluations through the reproducing identity; a bound on is not by itself a bound on loss unless the admissibility condition is also used.
The Lean model uses an abstract complete real inner product space , an evaluation map , a feature map , and the published IsRKHSOf predicate tying these to . The completeness instance matches the source's Hilbert-space assumption. Samples have type Fin m → X × Y, so an index i : Fin m already forces . Minimization ranges over the entire for Theorem 22 and over the declared convex class for Lemma 20. The objective definitions use the published Loss and EmpiricalError objects. No probability measure or measurability assumption is needed for these deterministic assertions.
There is a printed mismatch that affects what “deletion” means. Theorem 22 names an algorithm defined by equation (26), which, run afresh on points, would normalize its data term by . Lemma 20 and the proof of Theorem 22 instead compare the full objective with equation (20), whose data term uses . The formalized goal states that comparison, with its explicit constant, and records the discrepancy for audit. This excludes the tempting shortcut of treating the two normalizations as identical. The regularizer is the genuine squared norm and the second minimizer is required to minimize the genuine truncated objective; neither a restricted hypothesis ball nor an artificially assumed distance bound enters the goal. Contributions that establish minimizer existence or connect the pairwise bound to an algorithmic selection would extend this core without changing its statement.
Eligibility traces are one of the basic mechanisms of reinforcement learning. A trace is a short-term memory vector with one component per weight. It records which components contributed to recent value estimates, so that an error observed now can be credited to the right components without storing the past. Chapter 12 of Sutton and Barto's Reinforcement Learning: An Introduction (2nd ed., 2018) organizes the topic around two ways of describing an algorithm. A forward view updates each state toward a target built from rewards that arrive later. A backward view makes an update at every step from the current error and the trace.
The chapter proves one exact equivalence between the two views itself, in §12.6: "This is the only equivalence of forward- and backward-views that we explicitly demonstrate in this book" (p. 301). The setting is linear Monte Carlo prediction, and the backward view uses a dutch trace. The same trace appears in true online TD(), whose exact equivalence to the online -return algorithm (van Seijen and Sutton, 2014; van Seijen et al., 2016) the book cites without proof. Of that proof, §12.6 "gives some of the flavor ... but is much simpler" (p. 301).
The older equivalence of §§12.1–12.2 goes back to Sutton (1988). If the weights are held fixed during an episode, the summed updates of TD() with accumulating traces equal the summed updates of the off-line -return algorithm. The book leaves it as Exercises 12.3–12.4.
Fix a dimension , a step size and an episode of length with feature vectors . The episode ends with a single return ("a single reward received at the end of the episode ... and ... no discounting", p. 301). The forward view is the linear gradient Monte Carlo, or LMS, rule (12.13): from an initial ,
Let be the fading matrix. The backward view keeps two vectors that are updated at each step in time without knowledge of . The dutch trace is , . The auxiliary vector is , with .
For the second part, an episode carries states and rewards, and is a differentiable value function with . For one fixed weight vector , define the following, with and :
The left side is the forward view after LMS updates. On the right, and are produced by the incremental recursions above. The goal is about the two algorithms, not only about the closed-form product identity.
The goal says that an -per-step algorithm reproduces the Monte Carlo/LMS result exactly. That algorithm never stores the feature vectors or the intermediate weight vectors. The book draws the conclusion that eligibility traces "are not specific to TD learning at all" (p. 303). The dutch trace in the case is the same object that true online TD() (12.11) uses for general . The fading-matrix products and their incremental forms are therefore the vocabulary of any later formalization of true online TD() and of the online -return algorithm.
Exercises 12.3–12.4 are the fixed-weight equivalence of TD() and the off-line -return algorithm. They are the standard justification for calling TD() an approximation of the -return algorithm. Exercise 12.1 and (12.3) are the identities the rest of the chapter uses to manipulate -returns.
On status: all of these results are known and elementary on paper, and the book prints the derivation of (12.14). To our knowledge none of them has a machine-checked proof, and the platform has no statement about -returns, eligibility traces or TD(). What this mission adds is formal statements with every convention fixed, including one correction to the printed text. It also adds reusable definitions of -step returns, -returns and traces.
The algebra is elementary. The difficulty lies in the conventions, and a careless reading of the page produces a false statement. The book initializes , and taken literally that makes the goal false. The -return is an infinite series, whose tail collapses only because every -step return that reaches past termination equals the full return. That convention has to be built into the definition of , together with the terminal value . Exercises 12.3 and 12.4 are true only when the weights stay fixed. With the algorithms' changing weights the -step returns (12.1) use , and neither identity holds. The boundary indices (, the empty product at , ) must come out right.
Namespace SuttonBartoRL.Traces. Vectors of §12.6 are Fin d → ℝ, matrices Matrix (Fin d) (Fin d) ℝ, and is Matrix.vecMulVec x x. The ordered product fadeProd α x j t is , the identity when . Feature sequences are indexed by ; only enter. is a hypothesis wherever appears. The identities of §12.6 are stated for every real and , a harmless strengthening of the book's positive step size.
For §§12.1–12.2, weights are EuclideanSpace ℝ (Fin d), is Mathlib's gradient, and each is assumed differentiable in Exercise 12.4. An episode is a length , states and rewards. The value at time is . (12.2) is a tsum over of , and , the range the book gives with (12.2). Milestone 5 concludes summability, so the junk value of a divergent tsum cannot make it trivial. Exercises 12.3–12.4 take one weight binder w, used in every return, TD error and gradient. That is the book's fixed- assumption, stated in the binders.
Correction. The printed initialization (p. 302) contradicts the printed definition and (12.14). The counterexample is , , , , , : the forward view gives , while . The mission states the corrected result with , equivalently the same recursion started from . The printed text is kept verbatim in the milestone.
A trivializing formalization is ruled out: the goal is not the closed-form identity with and defined as the products and sums. Those vectors are defined by their -free incremental recursions, and the closed forms are separate milestones.
Out of scope: the equivalence of true online TD() and the online -return algorithm (cited, p. 300), the truncated-return identity (12.10), the error bound (12.8), and all convergence claims. Proofs of the milestones, and reuse of the definitions in later missions on true online TD(), are welcome.
Classical generalization bounds for classifiers, built on the VC dimension, grow with the number of adjustable parameters. For neural networks this is at odds with practice: networks with many more weights than training examples often generalize well. Bartlett's 1998 paper (IEEE Trans. Inform. Theory 44(2), 525–536) explains part of this by measuring a real-valued classifier's confidence. If a hypothesis classifies most training examples correctly with a margin , its misclassification probability is controlled by a scale-sensitive dimension of the class at scale proportional to , not by its VC dimension. Later in the paper this yields bounds for networks with small weights that do not depend on the number of weights.
This mission formalizes the first of the paper's two main technical results, the margin bound of Theorem 2 (p. 527), together with the steps of its proof on pp. 527–528.
The fat-shattering dimension was introduced by Kearns and Schapire (JCSS 1994). Alon, Ben-David, Cesa-Bianchi and Haussler (J. ACM 1997) proved the scale-sensitive Sauer-type covering bound used here (Theorem 5 of the paper). Shawe-Taylor, Bartlett, Williamson and Anthony (IEEE Trans. Inform. Theory 1998) proved the zero-training-error version (Theorem 1 of the paper). Theorem 2 extends it to hypotheses that make margin errors on the training data.
Let be a set and a probability distribution on . The threshold function is for and for . For a real-valued hypothesis on , the misclassification probability is . For a sample drawn independently from and , the margin error estimate is
Let be a class of real functions on . Points are -shattered by if some has the following property: for every sign vector , some satisfies for all . The fat-shattering dimension is the largest such , possibly .
The proof uses the following objects:
Assume , , , and finite with . With probability at least over , every satisfies
A further item, Proposition 8 (p. 529), is the probabilistic device the paper uses to make such bounds uniform over .
Theorem 2 is the bound behind the paper's main message. Corollary 9 makes it uniform over , and Theorem 28 combines it with fat-shattering estimates for networks with bounded weights. Together they show that a network classifying the training data with a large margin generalizes at a rate governed by the size of its weights, not by its number of weights. The same template, a margin error plus a capacity term at scale , underlies later margin analyses of support vector machines and boosting.
All results in this mission are proved in the literature; none is open. None is machine-checked on this platform: the platform has Rademacher-complexity margin bounds, but no statement about fat-shattering dimension or sample covering numbers of real-valued classes. A complete formalization would provide a reusable library of these objects, with their basic inequalities between squashing, quantization, packing and covering. It would also give a checked version of the explicit constants and , which differ from those in later textbook treatments.
The bound is uniform over a possibly uncountable class , so a union bound over hypotheses does not apply. The obvious replacement is a union bound over a cover of . Two steps make it hard:
The quantization steps look routine but carry the factor-of-two losses that produce the constants , and .
The model is in the namespace BartlettNN.Margin.
Bool, read as through pm (true is ). . Samples are functions Fin m → X × Bool, indexed from , with law Measure.pi (fun _ => P). The margin estimate uses the strict inequality , and shattering uses .ℕ∞. A ℕ-valued supremum would be on an unbounded set, so the goal assumes fat H (γ/16) = d with d : ℕ.⊤ when no finite cover exists. and are suprema over all samples, with repetitions allowed. "-separated", which the paper leaves undefined, is read as distance .Real.log, is Real.logb 2, and is Real.exp 1.Measurability. The paper states "we ignore issues of measurability, and assume that all sets considered are measurable" (p. 526). This is made explicit, not removed, through three hypotheses:
Replacing these by countability of would weaken the theorem.
Corrections of the printed text.
Trivializing formalizations, ruled out. The following would each make the statements empty or different, and none is used:
ℕ-valued fat dimension or covering number;Real.sign in place of ;Infrastructure that a complete development needs, and contributions that are welcome:
The covering/packing and fat-shattering lemmas apply beyond this mission. Proofs of individual milestones, or of Theorem 5 in the generality of Alon et al., are useful contributions in their own right.
An airline sells the seats of one flight leg in several fare classes at different prices. Low-fare passengers usually book first, so the airline must decide how many seats to keep back, or protect, for later high-fare passengers. Peter Belobaba's 1987 MIT dissertation introduced the expected marginal seat revenue (EMSR) rule for this decision, and EMSR-type rules became a standard of airline revenue management practice (Talluri and van Ryzin 2004). A protection level is computed from a demand forecast, and forecasts are uncertain. Section 6.2 of the dissertation asks how the protection level moves when its inputs move: the mean of forecast demand, its standard deviation, and the ratio of the two fares. That question decides where forecasting effort pays off, and this mission formalizes the answers the dissertation gives for Gaussian demand.
This is the third mission in a series on the dissertation. The first treats marginal allocation among distinct fare classes, and the second the two-class nested protection level in the discrete model, including its revenue optimality. This mission takes the continuous Gaussian model of Chapter 6 on its own terms.
Let be the number of requests for a fare class, a real random variable with law . For a seat level the tail probability is
and for the fare of the class the expected marginal seat revenue is (Eqs. (6.1)–(6.2)).
There are two classes: class 1 with fare and class 2 with fare , where . Requests for class 1 are Gaussian with estimated mean and estimated standard deviation , written . A real number is an EMSR protection level for class 1 against class 2 when
The standardized level is the value "which has a probability of of being exceeded" by a standard normal variable:
In the Lean development these are tailProb, emsr, gaussianLaw rbar σ, stdNormal, IsProtectionLevel rbar σ f₁ f₂ S and IsStdNormalLevel f₁ f₂ Z, all in the namespace SeatInventory.Gaussian.
For and :
The goal states no numerical constant and no particular fare ratio; it fixes only the shape of the dependence.
The dissertation's constant-coefficient-of-variation form, Eq. (6.13), with , follows from (6.12) by substitution and is not stated separately.
The result gives every Gaussian protection level as a closed form in one standard normal quantile. From it come the three sensitivities that Sect. 6.2 uses to argue for better forecasts. The protection level moves one-for-one with mean demand. The standard deviation moves it in a direction fixed only by whether the discount fare is above or below half the full fare. A higher fare ratio always lowers it. The dissertation uses these facts, and its Figures 6.1 and 6.2, to argue that reducing the estimated standard deviation of demand narrows the range of protection levels a forecast can produce. The same quantile structure is behind Littlewood's rule and the newsvendor critical fractile, so the statements here are the Gaussian specialization of a pattern that recurs throughout revenue management and inventory theory.
All the statements are classical and easy to believe. None of them, to our knowledge, has a machine-checked proof. Mathlib provides the Gaussian law and its affine images, but no standard normal quantile and no statement that a Gaussian tail is a strictly decreasing bijection onto . Formalizing this mission produces both, in a form that can be used again wherever a normal critical fractile appears.
Most of the work is in the existence and uniqueness of the two tail solutions. The tail must be shown continuous, strictly decreasing, and to take every value in . Strictness needs the Gaussian density to be positive everywhere, and existence needs a limit argument at both ends. Monotonicity alone, which holds for every law (Eqs. (6.1)–(6.2)), gives neither, because a general law can have flat stretches and jumps in its tail. The relation then requires transporting the tail of to that of through the affine map , and the sign of requires the symmetry of , namely . Once uniqueness is available, each sensitivity statement follows from these facts. The tempting shortcut of reading as a definition is ruled out below.
gaussianReal rbar (σ^2), parameterised by the variance. Every theorem assumes ; at the law is a Dirac mass and (6.10) has no solution.Useful infrastructure, all reusable: the strict monotonicity, continuity and range of Gaussian tails; the standard normal quantile; and tail transport under affine maps. Contributions of these as separate lemmas are welcome.
Temporal-difference (TD) learning estimates the value of a policy by moving a current estimate toward a target built from observed rewards and from the estimate itself. Chapter 7 of Sutton and Barto's Reinforcement Learning: An Introduction (2nd ed., MIT Press, 2018) interpolates between the two extreme targets of the preceding chapters: the one-step TD target, which uses one reward and then bootstraps, and the Monte Carlo target, which uses every reward until the end of the episode. The intermediate target, the -step return, uses rewards and then bootstraps from the current estimate. The family underlies -step TD, -step Sarsa, the off-policy per-decision methods and the tree-backup algorithm, and it is the introduction to eligibility traces (Chapter 12).
The book justifies the whole family with one inequality, the error reduction property (7.3), p. 144: the expected -step return is closer to the true value than the estimate it bootstraps from, by a factor in the worst state. It is the reason given for calling -step TD methods "sound". The same chapter states, mostly as exercises without solutions, a series of exact identities that rewrite each kind of -step return as a sum of one-step TD errors.
A finite Markov decision process has finite state and action sets , , a finite reward set , and dynamics , the probability of next state and reward after action in state (Eqs. (3.2)–(3.3)). A policy is a probability distribution over actions for each state. Following from produces a random trajectory For a discount factor the state-value function is the expected discounted return (3.12),
Given any function (an estimate of ), the -step return (7.1) is
In an episode that terminates at time it is replaced by the complete return when . The TD error (6.5) is . Off-policy variants use a behavior policy that generates the data, the per-decision ratio , and the return with control variate (7.13), , . The tree-backup return (7.15)–(7.16) uses action values and the expected approximate value (7.8).
For a finite MDP, a policy , , any and every ,
The result. The error reduction property makes the expected -step target a -contraction toward in the sup norm, uniformly over the estimate it starts from. It is the one-line reason the book offers for the soundness of every -step TD method, and the same contraction is what the -return of Chapter 12 averages over . The TD-error identities are the algebra behind implementations that accumulate TD errors instead of storing returns, and behind the forward/backward-view equivalences of Chapter 12. Exercise 7.6 is the unbiasedness of the control-variate return, which is what allows (7.13) to replace plain importance weighting without changing the expected update.
Formalizing it. All results are elementary and well known, but the book gives no proofs: (7.3) is asserted, and the identities are exercises without published solutions. None is formalized on Prove2Me. The mission produces machine-checked versions with every hypothesis explicit (discounting, the fixed estimate, terminal values, coverage), and a trajectory-level expectation for finite MDPs that other chapters of the series can reuse.
The obvious proof of (7.3) is a matrix computation: , and a stochastic matrix does not increase the sup norm. The difficulty lies in the step before it. The left side is an expectation over trajectories, and is an infinite discounted series; neither is a matrix power by definition. Connecting them requires a Chapman–Kolmogorov identity for the finite-trajectory distribution induced by and , the splitting of at time , and summability of the discounted series. Defining the expected -step return as the matrix expression would reduce the goal to the last line and remove its content; that shortcut is ruled out below.
The TD-error identities are telescoping sums, but each has its own boundary: termination inside the steps, the convention that terminal states have value zero, the index at in (7.6), the special case of the tree backup, and ratios with vanishing denominators in (7.13).
Needed infrastructure: finite sums over function types, Chapman–Kolmogorov for the segment distribution, summability of . The trajectory layer is reusable for the importance-sampling and eligibility-trace chapters. Alternative proofs of the goal, and proofs of the undiscounted episodic version as a separate theorem, are welcome.
How many integral points does a polytope contain? The question arises in integer programming, where it measures the size of a feasible set, in combinatorics, where many enumeration problems are lattice-point counts in a polytope (contingency tables, magic squares, flows), in the representation theory of Lie groups, and in the analysis of loop nests in compilers. Counting is #P-hard when the dimension is part of the input, so the natural question is whether the count can be computed in polynomial time when the dimension is fixed.
Timeline:
Points of have real coordinates and . For integral vectors , the rational cone they generate is . The generators are simple if they are linearly independent, and primitive if moreover they form a basis of the lattice .
The index of the cone given by simple generators is the number of integral points in the semi-open parallelepiped . It equals exactly for primitive generators.
The exponential sum of is . Where it converges it has the closed form
and this closed form defines at every regular point, i.e. every with for all .
An integral simplex is with affinely independent . Its supporting cone at a vertex is . A signed decomposition with integers means on all of . The constant term of the Laurent expansion of at is the coefficient of in the expansion of around its pole at .
For and every integral simplex there are, for each vertex , primitive cones and integers with and at most terms. Here is the smallest integer
and is the index of the edge vectors at . Moreover, for every orthogonal to no generator of any ,
where is the constant term at of .
The goal is the reason Barvinok's algorithm is polynomial. For fixed , the number of terms is bounded by a polynomial in , which is polynomial in the input size. Each term is an explicit rational function of inner products (Corollary 4.2). The identity therefore turns lattice-point counting into the evaluation of a short sum. Its consequences include polynomial-time counting for rational polyhedra in fixed dimension, polynomial-time computation of Ehrhart quasi-polynomials, and the theory of short rational generating functions (Barvinok–Woods), which underlies algorithms for parametric integer programming.
The result is proved and classical. As far as known it has not been machine-checked: Mathlib has convex cones, Minkowski's convex body theorem and lattices, but no signed cone decompositions, no generating functions of cones and no Brion identity. The mission produces a formal account of the algorithm's correctness and of the size of its output. Its milestones are statements of independent use: the closed form of cone generating functions, Brion's identity for simplices, and the index-reduction lemma.
The obvious approach is to triangulate the supporting cones into unimodular (primitive) cones. This fails: a cone of index may need about unimodular cones in any triangulation, which is exponential in the input size. The step that makes the count small is signed decomposition. Signed decomposition uses cones that are not contained in , combined with signs , and controls the index through the geometry of numbers rather than through a subdivision of . The second difficulty is that , where the exponential sum equals the count, is a singular point of every . The count is recovered as a constant term of a Laurent expansion, so every identity has to be valid as an identity of meromorphic functions on regular points, and not only where the series converge.
Fin d → ℝ, integral vectors Fin d → ℤ used through their real cast, and is dotProduct. A cone is given by its generator list, because index, parallelepiped and the closed form of depend on the generators. Logarithms are natural, and is the sup norm.An agent learning to control an unknown environment must balance rewards it can collect now against information that improves later decisions. In a finite Markov decision process (MDP), every action changes the distribution of the next state, so a mistaken transition estimate can affect decisions many steps later. Regret measures this loss against a policy that already knows the transition probabilities. The paper of Azar, Osband and Munos gives high-probability regret bounds for two variants of upper confidence bound value iteration (UCBVI) in finite-horizon reinforcement learning. This mission targets its Chernoff–Hoeffding variant, UCBVI-CH, whose bonus depends only on the horizon and the visit count. Theorem 1 improves the paper's cited earlier dependence on the number of states from to in the leading term for sufficiently many interactions. Azar, Osband and Munos, 2017, pp. 2, 4–5.
The paper was released in 2017 alongside work on the attainable dependence of episodic regret on the horizon , state count , action count , and total interaction time . Its second algorithm, UCBVI-BF, uses a variance-dependent bonus and is the subject of the next mission in this series. UCBVI-CH has a simpler bonus and its own explicit bound, making it a distinct mathematical target. Azar, Osband and Munos, 2017, pp. 1–5.
The state set and action set are finite and nonempty, with cardinalities and . A stationary transition kernel gives the probability of moving to state after action in state ; each row is nonnegative and sums to one. The known, deterministic reward lies in . An episode lasts steps. The environment chooses its starting state before episode and may base that choice on earlier episodes. It cannot see the current episode's future random draws. Azar, Osband and Munos, 2017, §2 and Assumption 1, pp. 2–3.
A policy selects an action from the current state and the step number. Its value is the expected sum of rewards from step through step when starting in state . The terminal value is , and is the maximum of over all such policies. Since the state, action and step sets are finite, this maximum is over a finite nonempty policy class. The paper's sentence describing rewards uses a shifted terminal convention; this series follows the reward steps of Algorithms 1–2. Azar, Osband and Munos, 2017, pp. 3–4.
At the start of episode , UCBVI-CH forms visit counts and from earlier completed transitions. On a visited pair it uses the empirical row . Algorithm 2 computes values backward from zero at the terminal step. For a visited pair, is the minimum of the preceding episode's , , and the empirical Bellman value plus Algorithm 3's bonus. For an unvisited pair, . A maximizing action is chosen at every state, including states outside the realized path. Azar, Osband and Munos, 2017, Algorithms 1–3, pp. 3–4.
For episodes and , regret sums the gap . The goal is the paper's printed bound, with its constants:
Algorithm 3 itself uses in its bonus . Both logarithms remain as printed. The probability is over the MDP's next-state draws, for every admissible starting-state rule and every way of breaking ties between maximizing actions. Azar, Osband and Munos, 2017, Algorithm 3, p. 4; Theorem 1, p. 5.
Four milestones retain the source's indexed attack path: the Bernstein bound (9) for the empirical value error, the count-deviation display before (11), Lemma 18 on optimism, and the weighted recursion displayed in the proof of Lemma 3. The last milestone preserves the signed weights that appear before the paper's final simplification. Azar, Osband and Munos, 2017, pp. 17, 20–21, 28.
Theorem 1 gives a finite-sample failure probability with explicit dependence on and . It covers a learner whose initial state can change between episodes, a feature that matters in episodic learning where the experimenter does not fix a single starting distribution. For the regime stated after Theorem 1, the leading rate is . This is a result claimed by the paper; the present Lean declarations are open proof targets, not machine-checked proofs of that claim. Azar, Osband and Munos, 2017, p. 5.
Formalizing the result creates reusable finite objects for adaptive interaction: a constructed probability law on complete paths, empirical transition counts pooled across steps, a policy value defined by its expected reward, and confidence events with their domains stated explicitly. The concentration and optimism milestones can then be investigated independently of the final regret bound. The later UCBVI-BF mission uses the same paper's model with a different bonus. Azar, Osband and Munos, 2017, pp. 3–5, 14–17.
The visit count is random and depends on earlier observations and decisions. A concentration inequality for a predetermined number of samples therefore does not immediately give a statement that holds at every episode start. The algorithm also reuses the previous episode's estimate through a minimum. Any optimism claim must account for this dependence across episodes as well as the backward dependence across steps. In the regret analysis, the terms called martingale differences can have either sign, so replacing a positive weight by a larger common bound can reverse an inequality. These are concrete obstacles to the printed chain of estimates. Azar, Osband and Munos, 2017, pp. 4, 17, 20–21, 28.
States, actions, steps, episodes and complete outcome arrays are finite. Probabilities are finite sums of products of transition rows. The transition-row predicate is a published general definition; this mission defines the paper-specific reward-bounded MDP, policies, UCBVI-CH recursion, and path law on top of it. The starting-state rule can inspect only earlier episodes. Greedy tie-breaking is universally quantified. is a maximum over policies, and the bonus is read only at positive counts. A model that assigns an arbitrary probability law, fixes one starting state, or omits Algorithm 2's minimum does not represent this target. Azar, Osband and Munos, 2017, pp. 2–4.
Lean uses steps and terminal index in place of the paper's algorithmic . The appendix sometimes puts the terminal value at . The weighted recursion therefore runs through the final reward step, rather than ending one step early. Its typical-state threshold is , as required by (34)–(36), whereas Appendix B.1 prints . The proof's correction term dominates its other terms under , which is made explicit in that milestone. The printed (11) loses a factor of two from the count display before it; only the preceding display is a milestone. Lemma 18 is stated under the empirical-model part of the confidence event and , the domain on which its bonus comparison holds. The weighted milestone retains its coefficients because the bracketed martingale terms can be negative. Azar, Osband and Munos, 2017, pp. 14–17, 20–21, 28.
The goal retains Theorem 1's constant . Appendix C.1 cites Lemmas 15 and 18, but the sketch of Lemma 15 does not track that constant explicitly. Formalizing the printed bound may therefore expose a gap in its proof; the mission records the claim without weakening its constants. Contributions establishing or repairing the explicit bound, as well as the four stated milestones and reusable finite concentration results, are within scope. Azar, Osband and Munos, 2017, pp. 5, 27, 29.
Temporal-difference (TD) learning estimates the value of each state of a Markov reward process from observed experience, updating an estimate toward a target built from the next reward and the current estimate of the next state. Monte Carlo (MC) methods instead update toward the full observed return. Both are standard prediction methods in reinforcement learning, and their relationship is a recurring question of the field (Sutton 1988).
When only a finite amount of experience is available, a common practice is to present the same data repeatedly until the estimates stop changing. Chapter 6 of Sutton and Barto's Reinforcement Learning: An Introduction (2nd ed., MIT Press, 2018) uses this setting to explain why TD(0) is often faster: under such batch updating, both methods converge deterministically, but to different answers. Batch MC finds the least-squares fit to the observed returns; batch TD(0) finds the value function of the maximum-likelihood Markov model of the data, the certainty-equivalence estimate. The comparison appears in §6.3, Optimality of TD(0) (pp. 126–128), and is illustrated by Example 6.4, You are the Predictor. The book states these conclusions without proof. This mission formalizes them.
Let be a finite set of nonterminal states and . An episode is a finite sequence with , real rewards , and terminal. A batch is a finite list of episodes. A visit of is an (episode, time ) pair with , and counts all visits (every-visit counting).
A value array is extended by . For a discount rate , the return is and the TD error is .
Batch TD(0) with step size computes the TD(0) increment for every visit in the batch and changes once, by their sum:
Batch constant- MC is the same iteration with the increment .
The maximum-likelihood model of the batch has transition probabilities , where counts the observed transitions from to , and expected rewards equal to the average reward observed on those transitions. With and , the certainty-equivalence estimate is the value function of this Markov reward process,
For every finite batch and every , the series defining converges, and there is such that for all and all initial arrays ,
The limit depends neither on nor on at visited states.
The result explains the empirical observation of Figure 6.2 in the book: batch TD(0) has lower error than batch MC on Markov data, because it computes the certainty-equivalence estimate, while batch MC fits the training returns. It also gives a precise meaning to the claim that TD methods approximate the certainty-equivalence solution with memory linear in the number of states, where computing it directly needs a model of quadratic size and cubic time (p. 128). Identity (6.6) is the starting point of the -step and eligibility-trace methods of later chapters.
The comparison under repeated presentation of a finite training set goes back to Sutton 1988, but the textbook states the conclusions without proof, and no machine-checked version is known to exist. The formalization pins down every hypothesis the text leaves implicit: the step-size threshold, the treatment of unvisited states, every-visit counting, and the undiscounted case.
The fixed-point equation of batch TD(0) is on visited states, with the diagonal of visit counts, and convergence of the iteration requires every eigenvalue of to have positive real part. For this follows from being substochastic. For , the case of Example 6.4, is only substochastic and the naive contraction argument fails: invertibility of must be derived from the structure of the data, since every episode ends in the terminal state. The matrix is not symmetric, so symmetric positive-definiteness arguments do not apply. The same issue makes convergence of the series defining nontrivial at .
An episode is a Lean List (X × ℝ) of transitions , with the terminal state represented by none : Option X; a batch is a list of episodes; states form a Fintype. Values at the terminal state are by definition. The certainty-equivalence estimate is defined from returns as the series , not as the solution of a Bellman equation, and its convergence is part of the goal, not assumed. "Sufficiently small " is an existential threshold quantified before and ; a statement for one fixed , or for some , would be weaker than the book's and is ruled out. Unvisited states receive no increment and keep their initial value; the goal records this rather than claiming convergence to there. The standing assumption includes . Every visit is counted in both the TD increments and the model; mixing first-visit and every-visit counts would make the goal false.
The mission needs only finite sums, matrix powers and limits of real sequences; Mathlib's Matrix and Filter.Tendsto suffice. A lemma that a nonnegative matrix whose rows reach an absorbing mass has spectral radius below one would be reusable beyond this mission, as would a convergence criterion for when is a nonsingular M-matrix. Contributions of either kind, and of the elementary milestones 1–3, are welcome.
In the classical secretary problem a decision maker sees candidates in a uniformly random order and must accept or reject each one on arrival, irrevocably, aiming to accept a valuable one. Its online, random-order structure models hiring, selling an item to sequentially arriving buyers, and posting prices in online markets. Babaioff, Dinitz, Gupta, Immorlica and Talwar (SODA 2009) study the discounted secretary problem, where the reward of a selection depends on when it is made: a candidate accepted late is worth less (or more) by a time-dependent factor, as with a seller whose revenue decays with time, or a firm that loses value the longer a position stays empty.
Timeline of the setting:
There are elements, indexed by . Element has a value , and each time has a discount . The elements arrive in a uniformly random order , a bijection from times to elements: element arrives at time . Selecting the element that arrives at time earns , and an algorithm selects at most one element.
The offline optimum on the order is . It is a random variable, and the benchmark is its expectation
For a real parameter , algorithm selects the first time at which and earns that product; if no time qualifies, it selects nothing and earns . It knows and , sees the values one at a time, and never sees the future of . Its expected value is .
The proof uses three derived objects:
For every , all discounts , all values and every real ,
Taking gives , a -competitive algorithm when the expected optimum is known.
The result. The discounted problem separates sharply by information: a logarithmic gap is unavoidable without prior knowledge, while knowledge of the single number , or of any lower estimate of it, closes the gap to a constant. The algorithm is a fixed posted threshold, so read as a mechanism it is a posted price, which is truthful for single-parameter agents (§1). The paper also notes that when all values are known, can be estimated by sampling (its Lemma A.1), which yields a constant-competitive algorithm in that setting. The companion lower bound (Theorem 4.6) shows that even complete knowledge of the values does not give a ratio better than .
Formalizing it. The result is proved on paper; no machine-checked proof is known. The formalization yields a checked version of the paper's counting argument on permutations (Claim 4.8) and of the tie-breaking step behind Eq. (4.3), and reusable finite random-order bookkeeping: expectations over as averages, threshold stopping rules, and the decomposition of an online algorithm's value by the time and element it selects.
The obvious argument fails when rarely selects. earns at least whenever it selects anything, so . That settles the case and nothing else: the probability of selecting can be tiny while is still large, because the optimum may be concentrated on a few orders with a large product. In that case the bound must come from comparing the algorithm with the optimum pair by pair: every time–element pair with must be realized by on a positive fraction of the orders.
Two points need care in a formal proof:
Neither (4.2) nor the map appears in the statements, so solvers may replace either with any argument they like.
Fin n; the paper's time is the index . An order is π : Equiv.Perm (Fin n), read as time ↦ element, as on p. 3. The instance [NeZero n] encodes , so the maximum over times is a genuine maximum (Finset.sup').Equiv.Perm (Fin n) and on first-hitting times are reusable beyond this mission.In the classical secretary problem a decision maker sees candidates in uniformly random order, learns each candidate's value on arrival, and must accept or reject it on the spot; the goal is to pick a valuable one. A simple sample-then-select rule picks the best candidate with probability at least , so the problem is constant-competitive. The secretary problem is also a model of online mechanism design: a rule that accepts the first agent above a threshold computed from earlier agents is a truthful posted-price mechanism (as the paper notes in §1).
Babaioff, Dinitz, Gupta, Immorlica and Talwar (SODA 2009; authors' version) study the discounted secretary problem, where accepting at time is worth for a known discount function . Discounts model settings where a sale is worth more at some times than at others. The case had been studied before (Rasmussen and Pliska 1976); the paper asks what happens for arbitrary . Its answer has two sides: an -competitive algorithm, and the result of this mission, a lower bound showing that no online algorithm is better than -competitive. So, unlike the classical problem, the discounted problem with a general discount is not constant-competitive.
There are elements with values , and a discount function on the times. The elements arrive in a uniformly random order : element arrives at time . A randomized online stopping rule specifies, for each time and each sequence of values seen so far , a probability of stopping at if it has not stopped yet. Stopping at selects and earns ; the rule selects at most one element and may select none. The rule knows and , but it sees only values, only as they arrive, and it is not told which instance it is facing.
The expected value of is
and the benchmark is the expected offline optimum
which is itself a random variable averaged over the order. is -competitive on an instance when .
The hard family (§4.1.1 of the paper): fix an integer and put , , for , and . The step discount is on the times and on . The instance has elements of value and the rest ; is obtained from by raising of its values to , so has elements of value .
For every integer and every randomized online stopping rule for horizon and the step discount,
That is, no online rule is -competitive on all of .
The result separates the discounted secretary problem from its classical and weighted relatives, which admit constant-competitive algorithms (the paper's Theorem 3.4 and the -competitive classical rule). Together with the paper's upper bound (Theorem 4.4) it pins the competitive ratio for general discounts between and up to constants, and it motivates the paper's known- model (§4.2), where an estimate of restores a constant ratio. The construction is a template for lower bounds against randomized online algorithms in random-order models: geometrically nested instances that a rule cannot tell apart early, played against a discount that punishes waiting.
The theorem is proved in the paper, in about a page. To our knowledge no part of it has a machine-checked proof. This mission produces the formal model of randomized online stopping rules in the random-order discounted setting, a reusable object for the paper's other discounted results (the upper bound, and the lower bound with known values of Theorem 4.6), and a checked version of the lower bound with explicit constants.
The obvious attempt is to fix one instance and show that every rule loses on it. That fails: for any single instance there is a rule tuned to it (a rule that waits exactly as long as that instance warrants). The lower bound has to play the instances against each other. A rule that does well on must commit early, within the first steps, yet the rule cannot distinguish from during those steps except with probability . Making "cannot distinguish" precise is the central step: it needs a coupling of the two runs over the same random order and the same internal randomness, which works only because the rule's decision at time depends on the values observed so far and nothing else. The accounting then has to show that the rule's early earnings on and its late earnings are both small compared with , which uses and that dwarfs .
Fin n, 0-based: index is the paper's time , so the paper's block is the index range . The random order is π : Equiv.Perm (Fin n) read as time element, and every expectation over it is the finite average . Values and discounts are real.StoppingRule n: stopping probabilities indexed by time and the arrival-ordered value sequence, with the non-anticipation condition that depends only on . The theorem quantifies over all such rules, so it covers deterministic and randomized online algorithms that observe values only. A rule may depend on and but not on the instance index.Fin n), and competitiveness is multiplicative, , never a quotient.Fin n (the probability that a set of elements misses the first positions), the coupling of two value sequences that agree on a prefix, and elementary estimates on geometric sums. The rule model and the permutation-counting lemmas are reusable for the paper's other discounted results. Contributions of these supporting lemmas, as well as proofs of the milestones, are welcome.A correlated equilibrium is the equilibrium notion that arises when the players of a game take their actions on the advice of a common randomizing device, each player seeing only his own recommendation. It was introduced by Aumann in 1974 (Aumann 1974). Aumann's 1987 paper (Aumann 1987) gives the simple, finite form of the definition used today (Definition 2.1) and shows that the notion is what Bayesian rationality with a common prior predicts. On the way it records, as Proposition 2.3, the fact that makes correlated equilibrium tractable in practice: for a finite two-person game, the distributions over action pairs that come from correlated equilibria are exactly the solutions of an explicit finite system of linear inequalities.
That characterization is the starting point of the computational theory of correlated equilibria. Because the set is a polyhedron, an optimal correlated equilibrium can be found by linear programming, and no-swap-regret learning dynamics converge to this set (Foster and Vohra 1997; Hart and Mas-Colell 2000). In each of these works the linear-inequality description is taken as the definition; the paper's Proposition 2.3 is the bridge back to the strategic definition.
Player 1 has a finite set of actions and player 2 a finite set . For and , and are the two players' payoffs at the action pair .
A correlated strategy pair is a pair of functions , on a finite probability space : a finite set with nonnegative weights summing to . Chance draws and suggests the action to player . The pair is a correlated equilibrium (Definition 2.1, condition (2.2)) if no player gains by a deviation that depends only on his own suggestion: for every ,
and the analogous inequality holds for player 2 and every .
A distribution is a family with and . The distribution of a correlated strategy pair assigns to the probability . A correlated equilibrium distribution (c.e.d.) is the distribution of some correlated equilibrium on some finite probability space.
In the Lean development these are IsDistribution p, IsProbVec μ, IsCE h₁ h₂ μ f₁ f₂, distr μ f₁ f₂ and IsCED h₁ h₂ p, with h₁ j k and p j k .
For every distribution : is a correlated equilibrium distribution if and only if
A further statement, not a milestone, records the paper's example on p. 5: in the game of chicken (Figure 4) the distribution of Figure 5 is a c.e.d. with expected payoff .
The result. Proposition 2.3 turns an existential statement — there is some probability space and some correlated strategy pair that is an equilibrium and has distribution — into finitely many linear inequalities on alone. Consequently the set of c.e.d.'s is a compact convex polyhedron, membership is decidable by evaluating linear forms, and optimizing a linear objective over it is a linear program. The paper states the two-person case and remarks that "the principle, however, is no different in the general case".
Formalizing it. The proposition is classical and its proof is short; to our knowledge it has no machine-checked proof. The platform already has the linear-inequality (swap) form of correlated equilibrium for two-player games on Fin m × Fin n (Foster–Vohra 1997 missions) and Aumann's 1974 randomizing-structure model, but no statement that connects the strategic definition over arbitrary finite probability spaces with the linear system. This mission supplies that connection, so that results proved about the polyhedron apply to equilibria in Aumann's sense and conversely.
The mathematics is elementary; the care is in the statement. Two points need attention. First, the direction from the inequalities to a c.e.d. requires constructing a probability space and a correlated strategy pair whose distribution is the given ; the c.e.d. notion quantifies over probability spaces, not over distributions. Second, the paper's argument divides by the probability of a suggestion, which may be zero; the conditional formulation (milestone 2) holds only over possible suggestions, while (2.4) and (2.5) quantify over all actions and hold trivially at impossible ones. Deviations must be functions of the player's own suggestion: restricting to constant deviations gives coarse correlated equilibrium, which (2.4)–(2.5) do not characterize, and allowing arbitrary functions of gives a stronger notion.
Two players with finite action types S₁ S₂ : Type* (Fintype, DecidableEq); payoffs h₁ h₂ : S₁ → S₂ → ℝ; distributions p : S₁ → S₂ → ℝ with the sign and sum conditions as an explicit hypothesis of every statement about distributions. Finite probability spaces are finite types Γ : Type with a probability vector μ : Γ → ℝ; deviations are compositions φ ∘ f₁ with φ : S₁ → S₁. The conditional payoffs , use Lean's x / 0 = 0 and are only ever used at possible suggestions. Empty action sets admit no distribution, so the statements are then vacuous, exactly as in the paper.
A trivializing formalization is ruled out: "c.e.d." is the existential notion over finite probability spaces with a genuine probability vector and an equilibrium in the sense of Definition 2.1, not the inequalities themselves or the swap form on .
No infrastructure beyond finite sums and Finset.filter is needed. Contributions welcome: proofs of the milestones, and the -player generalization the paper alludes to.
An orthogonal projection onto a closed subspace is straightforward to describe when that subspace is given directly. It is less straightforward when the subspace is specified as the closed sum of two others: a vector can have contributions from both, and the two component projections generally do not commute. In §12 of Aronszajn's 1950 paper, this problem arises while expressing the reproducing kernel of a sum of two closed subspaces of a reproducing-kernel Hilbert space through their individual kernels. The projection formula is the analytic heart of that calculation. It also gives a series whose finite partial sums can be applied without first describing a basis for the closed sum.
Aronszajn states the result for closed subspaces of a complex Hilbert space of functions. The projection identity itself uses only Hilbert-space geometry; evaluation at a point and the reproducing property enter when the operator formula is translated into a kernel formula later in the section. This mission isolates the projection theorem so that the same formal result can be used both in that kernel calculation and in other settings with two closed subspaces.
Let be a complex Hilbert space and let be closed linear subspaces. The algebraic sum is the set of all with . It need not be closed. Write for its closure and for the intersection. All four subspaces are closed except possibly the algebraic sum itself. Let be the orthogonal projections onto , respectively. Operator products denote composition, with the rightmost factor applied first; is the identity.
The paper writes for , even when is nonzero, and uses a distinct dotted plus for the algebraic sum. These symbols can look like a direct sum in newer notation. Here the definitions of and remove that ambiguity. Aronszajn assumes complex scalars throughout Part I after §1, p. 343; the statements below keep that convention. Neither a topology on an underlying set of functions nor a measure is part of these operator assertions.
The goal is the strong projection series, §12, Eq. (7). For each ,
The sum means that its finite partial sums converge in the norm of for each fixed . No operator-norm limit is claimed. The first term of the sum, at , includes because both zero powers are identity operators.
Three source statements are milestones. Equation (1) is a finite identity that expresses a power of through a partial sum and a power of . The paragraph following Eq. (4) identifies the strong limit of as . The paragraph before Eq. (7) asserts that tends strongly to zero. Together these statements specify the finite and limiting parts of the displayed target. They require no assumption that is zero.
The formula describes the orthogonal projection onto a closed sum in terms of projections onto its two constituents. In Aronszajn's application, an orthogonal projection on a closed subspace determines that subspace's reproducing kernel; therefore the operator expansion supplies a kernel expansion without constructing a basis of the sum. It also makes explicit why an intersection term survives when the subspaces overlap. The result is proved in the 1950 paper; this mission asks for a Lean proof of that known result, with its convergence mode and closure convention made explicit.
A machine-checked development would provide a reusable complex-Hilbert-space statement for alternating projections and closed sums. Mathlib already provides closed submodules and their orthogonal projections, so the new contribution is the finite identity and the strong-limit claims connecting them. The resulting theorem can support the paper's later kernel expression, §12, Eq. (18), once the correspondence between bounded operators and kernels from §11 is available. Equation (18) is outside this mission's target list.
The algebraic sum of two closed subspaces can fail to be closed, so projecting onto it directly would leave the target undefined as a Hilbert-space orthogonal projection. Passing to its closure gives the correct target but does not imply the two projections commute or that their product has a uniform contraction factor. In particular, strong convergence of the powers and of the final series does not generally improve to convergence in operator norm. The later special case in §12, where the intersection is zero and the minimal angle is positive, has a stronger uniform-convergence conclusion; that extra angle condition is absent from Eq. (7).
The finite formula also has four terms per summand whose order matters. Reversing and , beginning the power at rather than , or omitting changes the statement. Even a proof of pointwise convergence of each selected term would not by itself establish the convergence of the bracketed partial sums in the target.
The Lean representation is an arbitrary complex Hilbert space E with two ClosedSubmodule ℂ E objects. Mathlib's Submodule.starProjection supplies and . Two small definitions name as projection onto the join of the closed submodules and as projection onto their meet. The closed-submodule join is the closure of the algebraic sum; the meet is the intersection. These definitions are computed from , not independently quantified projections. The theorem quantifies over every vector and uses Filter.Tendsto along natural-number partial sums, giving norm convergence of the resulting vectors.
The source's ambient class has a reproducing kernel, but no step in Eqs. (1)–(7) uses point evaluations. The formal statements therefore apply to any complex Hilbert space, including the paper's RKHS. The stronger scope is explicit here and does not assert a new kernel identity. The -th Lean partial sum uses indices for the paper's ; it has the same terms and is defined at as . The finite identity is stated only for , as its version is false in general.
Eq. (1) on p. 375 is printed without the opening bracket of the summand (only the closing bracket appears); the formalization reads it as in Eq. (4) on p. 376, where both brackets are printed. There are two printing slips on p. 377: a running sentence drops brackets from the power of , and it prints while discussing the projection . The formalization follows the bracketed expression in Eqs. (1) and (4), using ordinary operator subtraction. The corresponding milestone preserves the printed wording. No assumption from the later angle analysis, especially , is imported into these results. The series is stated through actual partial sums; it is not defined by an arbitrary RKHS chosen to have a desired kernel.
Reinforcement learning methods search for good behaviour by alternating two activities: estimating how good the current behaviour is, and changing the behaviour in the direction those estimates suggest. Sutton and Barto call this pattern generalized policy iteration and use it as the organizing idea of their textbook (Sutton & Barto 2018, §4.6). Its mathematical justification is a single result of Chapter 4, the policy improvement theorem (p. 78): a comparison made one step ahead, at each state separately, certifies that a changed policy is at least as good everywhere. Policy iteration, value iteration, Monte Carlo control with ε-greedy policies (Chapter 5), Sarsa and Q-learning are all motivated by it.
The chapter's results go back to the foundations of dynamic programming: the Bellman optimality equation (Bellman 1957), and policy iteration with its finite termination for discounted finite Markov decision processes (Howard 1960). Standard modern treatments are Puterman 1994, Ch. 6, and Bertsekas 2012, Vol. II, Ch. 1.
A finite Markov decision process has a finite state set , a finite nonempty action set , a finite reward set and dynamics : for each state and action , a probability distribution over the next state and reward (Eqs. (3.2)–(3.3)). A policy gives probabilities of choosing each action in each state; a deterministic policy is a map .
Fix a discount rate . The state-value function of is the expected discounted return
and the action-value function is defined from it by (4.6):
the value of taking once in and following afterwards. A policy is optimal if its value is at least that of every policy at every state, and the optimal value function is . A deterministic policy is greedy with respect to if for all (4.9).
For deterministic policies ,
and at every state where the hypothesis is strict, the conclusion is strict at that same state.
The results. The policy improvement theorem turns a local test into a global guarantee: it is enough to check, state by state, that one step of the new policy followed by the old one does no worse than the old one. Combined with the finiteness of the set of deterministic policies, it yields the finite termination of policy iteration and, with the equality case, the existence of a deterministic optimal policy. The stochastic form is what Chapter 5 invokes for ε-greedy control. Value iteration is the other classical way to compute .
Formalizing them. All of these results are classical and proved in the literature cited above; they are not open. The textbook presents them informally ("we chose not to produce a rigorous formal treatment", p. xiii): the improvement theorem is argued by an unbounded chain of expansions, and the policy evaluation and value iteration convergence claims are stated without proof. The mission makes each claim precise with explicit hypotheses and asks for machine-checked proofs against the book's own model with four-argument dynamics and stochastic policies. Related platform results use different models (cost minimization with deterministic policies in Bertsekas's Dynamic Programming; an expected-reward kernel and an assumed fixed point in Foundations of Machine Learning), and none states the policy improvement theorem itself.
The book's proof expands with (4.6) and reapplies (4.7) indefinitely, ending with "". Made rigorous, the chain is an inequality between truncated returns plus a remainder , and the passage to the limit needs the remainder to vanish and the truncated returns to converge to . Since is defined here as a series of expected rewards under the induced Markov chain, connecting it to the one-step quantities requires first establishing the Bellman equation for from that series. The strictness part does not follow from the weak inequality alone: strictness at one state must be shown to survive the averaging over later states, which requires tracking the contribution of the first step exactly. The policy iteration statement additionally requires handling ties: a greedy step taken from an optimal policy can move to a different optimal policy, so the sequence need not become constant.
All objects live in the namespace SuttonBartoRL.DP. States and actions are finite types, actions nonempty where a maximum is taken; one action set serves all states (footnote 3, p. 48). Rewards form a finite set , and the dynamics are a function whose values off are never used. Policies are stochastic; deterministic policies are embedded as policies that choose one action with probability one.
Committed conventions:
In-place (asynchronous) sweeps (§4.5) and truncated policy iteration are not formalized.
Needed infrastructure: summability of discounted series of bounded expected rewards, the Bellman equation for derived from the return definition, contraction arguments in the sup norm on , and finiteness of the set of deterministic policies. The definitions here duplicate those of the series' Chapter 3 mission and are intended to be merged with them; lemmas about , the Bellman equation and contraction are reusable by every later mission of the series, and contributions of such lemmas are welcome.
A directed polymer in a random environment is a simple random walk whose paths are reweighted by a random field of energies. It is a basic model of disordered statistical mechanics, and in dimension it belongs to the Kardar–Parisi–Zhang (KPZ) universality class: at fixed temperature the free energy fluctuates on the scale and is expected to follow Tracy–Widom laws. Comets and Yoshida (Ann. Probab. 34 (2006)) showed that in dimension every positive inverse temperature lies in the strong disorder regime, where the normalised partition function tends to zero. At the polymer is simply the random walk.
Alberts, Khanin and Quastel (arXiv:1202.4398, Ann. Probab. 42 (2014)) identified the regime in between. If the inverse temperature is scaled as , the partition function neither concentrates nor vanishes: it converges in law to a universal random variable, a Wiener chaos in a space–time white noise. That variable is the solution at time , integrated in space, of the stochastic heat equation with multiplicative noise, whose logarithm is the Hopf–Cole solution of the KPZ equation. The theorem therefore connects discrete polymers to the continuum KPZ equation under weak, -dependent disorder, with no assumption on the environment beyond exponential moments.
The environment is a family of i.i.d. real random variables on a probability space , with mean and variance . Write . The polymer is the symmetric simple random walk on started at , independent of , under the uniform measure on the step sequences. The energy of an -step path is , and the point-to-line partition function is
The modified partition function replaces by : .
On the continuum side, a white noise on is a centred Gaussian family , indexed by the Borel sets of finite Lebesgue measure, with . Its multiple stochastic integrals are continuous linear maps with for pairwise disjoint . Let be the heat kernel and . Put on , with , and zero elsewhere. The Wiener chaos (7) is
The discrete counterpart of is the weighted U-statistic of (29): a sum of products over distinct times, weighted by averages of over space–time rectangles of size .
If, in addition, for all for some , then for every
Under mean zero and variance one alone, .
In the order the proof uses them:
The theorem gives a universal scaling limit for the partition function in a regime where the polymer still moves diffusively but feels the disorder. As a corollary, converges in law, so the fluctuation exponent of the free energy is in this regime. The companion results (point-to-point partition functions, Theorem 2.2) show that the rescaled polymer path measure converges to a continuum directed random polymer. Letting grow then interpolates between Gaussian behaviour and the Tracy–Widom GUE fluctuations of the KPZ class. The U-statistic machinery of Section 4 (discrete chaos expansions in an i.i.d. space–time field converging to multiple Wiener–Itô integrals) applies to other discrete models with polynomial chaos expansions.
The theorem is proved in the paper. To our knowledge it has no machine-checked proof, and Mathlib has no space–time white noise, no multiple Wiener integrals, no Wiener chaos, no Lindeberg–Feller theorem for triangular arrays and no local limit theorem for the simple random walk. A complete formalization would build each of these and check the paper's argument, including two statements that are false as printed (see Formalization scope).
The obvious route is to expand in powers of and pass to the limit term by term. Two steps of that route do not go through as stated. First, the -th term is a degenerate U-statistic of order in the environment. Its convergence to is not a classical central limit theorem: it needs joint control of all orders and a density argument in , and the space–time discretisation must respect the parity of the walk, which is why the rectangles have spatial length . Second, exchanging the limit with the infinite sum over needs bounds on the discrete kernels that are uniform in and summable in . Pointwise convergence from the local limit theorem is not enough. Passing from to also requires a central limit theorem for a triangular array whose law depends on .
The environment is ω : ℕ × ℤ → Ω → ℝ, independent and identically distributed, square integrable, with mean and variance . Times are read. and are explicit averages over the step sequences. The white noise lives on , since only enters (7). is a family of continuous linear maps on characterised by its values on indicators of products of disjoint sets. Every limit theorem quantifies over all white noises and all such families, and a separate item asserts that one exists. and are sums in ; real powers , are Real.rpow; is Mathlib's cgf; convergence in law is TendstoInDistribution.
Normalisation of . The paper's normalisation of multiple integrals is not consistent (§3.2 and the remark on p. 19 differ by ). The formalization follows (7) and the variance computation on p. 6: for supported on , .
Corrected statements. Two milestones are stated in the corrected form that the paper's proof establishes:
Theorem 4.5 and Lemma 4.6 (perturbed environments) are not part of the milestone list. Theorem 4.5 is false as printed: mean zero and a variance tending to do not give a central limit theorem for a triangular array, and the Lindeberg condition named in its proof must be added. Lemma A.1 is stated for the point-to-line kernels only.
Trivializations ruled out. The limit is the chaos (7) built from a genuine white noise and its multiple integrals, not any random variable with a prescribed property. is pinned down by . Every infinite sum comes with a milestone proving its summability, and the partition function averages over all walk paths.
Infrastructure that would be reusable beyond this mission: space–time white noise and multiple Wiener–Itô integrals with their isometry, a Lindeberg–Feller central limit theorem, the local limit theorem for the simple random walk, and the Cramér–Wold device. Contributions of any of these, or of proofs of the milestones in any order, are welcome.
Electricity demand response asks consumers to lower their consumption during price events, when generation is expensive or scarce. Field trials such as the Low Carbon London experiment showed that consumers do react to price signals, but that the reaction is erratic: the average consumption falls while its variability stays high, and a producer that has to follow the load curve in real time pays for that variability. Aïd, Possamaï and Touzi (arXiv:1810.09063; Math. Oper. Res. 2022, doi:10.1287/moor.2021.1201) model this as a continuous-time principal–agent problem in which the consumer (the agent) controls both the level and the volatility of consumption, and the producer (the principal) designs a payment that rewards both.
The paper compares two benchmarks. In the second best, the producer observes only the consumption path and the consumer responds optimally to the contract; this is the subject of the companion mission of this series. In the first best, the producer dictates both the contract and the consumer's effort, subject only to the consumer's participation. The first best is the reference point against which the cost of moral hazard, the information rent, is measured. This mission formalizes the first-best value in closed form, Proposition 3.1 (i) of the paper.
The methodology follows the continuous-time principal–agent literature: Holmström and Milgrom (1987) for exponential utilities and linear contracts, Sannikov (2008) for the dynamic-programming view of the agent's continuation value, and Cvitanić, Possamaï and Touzi (2018) for contracts indexed on both the output and its quadratic variation.
Fix integers (usages for the mean effort and for the volatility effort), cost parameters , , nominal volatilities , effort bounds and , risk aversions , a marginal volatility cost , slopes , a horizon , an initial consumption and a reservation utility .
The consumer chooses a mean effort with values in and a responsiveness effort with values in , at cost
The consumption follows with , in the weak sense: is the canonical process on , and an admissible pair is a progressively measurable control with a probability measure under which starts at and solves the associated martingale problem.
The consumer values consumption by and the producer bears the generation cost ; write . For a payment made at time , the consumer's and the producer's criteria are
A contract is an -measurable with uniform exponential moments (2.5). The first-best value is
The consumer's Hamiltonians are and . Finally , , , and .
Assume . Then
The closed form shows how the first-best value depends on each parameter: on the energy value discrepancy through the mean-effort term, on the volatility cost and the effective risk aversion through the volatility Hamiltonian, and on the reservation utility only through the shift by . It is one half of the paper's information rent (Proposition 3.4), the gap between the first- and second-best values, and it is the benchmark against which the calibrated contracts of the paper's Section 4 are judged.
The result is proved in the paper, partly by appeal to standard stochastic control arguments. To our knowledge it has no machine-checked proof. A formal proof requires a verification theorem for an exponential-utility control problem in the weak formulation, and a risk-sharing argument with a pathwise quadratic-variation term in the contract; both are reusable beyond this paper.
The deterministic parts, Proposition 2.1 and the algebra that turns (A.5) and the value of into the goal, are calculus. The difficulty lies in the two stochastic steps. In (A.5), the producer's optimal payment for a given effort depends on ; it must be realised as a measurable function of the path that is a contract in the sense of (2.5), uniformly over all admissible laws, and the participation constraint must be shown to bind. In Proposition A.3 (i), the upper bound on must hold for every progressively measurable, path-dependent control, not only for Markov feedback controls; the paper invokes "standard stochastic control theory", which has to be made precise for controls of the volatility under a martingale-problem formulation, where no Brownian motion is given in advance.
The canonical space is with the coordinate σ-algebra and the canonical filtration; processes are indexed by . Admissible pairs are given by a martingale problem: almost surely, and both and its square minus are martingales. In the criteria, is replaced by its almost-sure value ; a contract remains any -measurable function of the path. Expectations of utilities are negated lower Lebesgue integrals of exponentials in , and every value is an extended-real supremum with . is read as , with indices in Fin N and Fin d.
The Hamiltonians are defined by their infima, never by their closed forms, so that Proposition 2.1 is not true by definition, and the first-best value is a supremum over the model's own objects, not a variable pinned by hypotheses. Three hypotheses are added to the page: (so ), (so is defined), and, for the goal only, , without which the printed exceeds and contradicts the paper's own proof. Misprints corrected and disclosed in the items: the closed form of in Proposition 2.1 is false for and is replaced by with ; the index range of is ; on p. 28, is and "(A.11)" is (A.6).
The parts (ii)–(iii) of Proposition 3.1, the optimal efforts and the optimal contract, are not stated. Contributions welcome: a verification theorem for controlled martingale problems with bounded coefficients, exponential moment bounds uniform over admissible laws, and a pathwise quadratic variation on the canonical space.
Demand response asks electricity consumers to lower or smooth their consumption when generation is expensive, in exchange for payments. Field trials such as Low Carbon London showed two effects of such incentives: consumers reduce their average consumption, and the variability of their response depends on how much effort they put into it. A producer who cannot observe the consumer's individual usages, only the aggregate consumption path, faces a moral hazard problem: the payment can depend only on what is observed.
Aïd, Possamaï and Touzi (arXiv:1810.09063v3, 2019; Math. Oper. Res. 2022) cast this as a continuous-time principal–agent problem in which the consumer controls both the drift and the volatility of his consumption, and the producer pays for reductions in both. The volatility channel is what makes the problem new: the classical Holmström–Milgrom model (Econometrica 1987) controls only the drift. The paper uses the general reduction of Cvitanić, Possamaï and Touzi (Finance Stoch. 2018) to optimal contracts with volatility control, and obtains the producer's value in closed form up to a scalar minimisation. This mission formalizes that closed form.
Fix integers , cost parameters and , nominal volatilities , effort bounds and , risk aversions , a marginal cost of volatility , marginal energy value and cost with , a horizon , an initial consumption and a reservation utility . Write and .
Consumption. is the canonical process on with its natural filtration . A control is progressively measurable, with (effort to reduce consumption) and (effort to reduce volatility). Under the consumption follows, in the weak sense,
Effort costs per unit time, with and .
Criteria. For a payment at time , the consumer's criterion is and the producer's is with . Contracts are the -measurable with exponential moments of order uniformly over the consumer's responses (2.5). The consumer's value is , and is the set of his optimal responses.
Second best. The producer offers , the consumer responds optimally, ties are broken in the producer's favour, and participation requires :
Hamiltonians. and .
Assume . With , ,
A companion statement, Corollary 3.1 (i), gives the explicit off-peak payment rates and when .
The closed form reduces an infinite-dimensional contracting problem, a supremum over all path-dependent payments and all consumer responses, to a deterministic one-dimensional minimisation at each time. It is the basis of the paper's comparisons: with the first-best value it measures the cost of moral hazard, and its minimiser gives the price of energy and of responsiveness that the optimal contract charges, which the paper calibrates on Low Carbon London data.
The result is proved on paper. No part of it is machine-checked. A complete formalization would give a checked instance of a continuous-time principal–agent theorem with volatility control. It would also fix, in exact terms, the conventions the paper leaves implicit (weak solutions, the effort cap), and the printed misprints that this mission corrects.
The deterministic milestones are calculus on boxes. The goal is not. The upper bound must hold for every -measurable contract, not only for contracts of a convenient form. The step that fails in a direct attempt is the representation of an arbitrary contract: one needs that every inducing an optimal response can be written as , an integral against and driven by the consumer's continuation certainty equivalent. This is the main theorem of Cvitanić–Possamaï–Touzi (2018) and rests on second-order backward SDEs; it has no counterpart in Mathlib. Restricting the supremum to linear or representable contracts at the outset would assume exactly that theorem. The lower bound needs, for the candidate contract, existence of the consumer's optimal response as a weak solution and a verification argument for the producer's HJB equation.
All objects live in the namespace DemandResponse.SecondBest, and all hypotheses are fields of a structure Params. Conventions:
Fin N, Fin d; , are allowed. when (the paper's ).The goal is an equality of extended reals between , defined from the model, and an explicit real number. A formalization that defines over a restricted class of contracts, or with a real-valued supremum that returns on unbounded sets, would trivialize or change it and is not the goal.
Needed infrastructure: continuous-time martingales on the canonical path space (Mathlib has Martingale and progressive measurability), existence of weak solutions with bounded coefficients, a representation theorem for contracts (Cvitanić–Possamaï–Touzi), and a verification theorem for the producer's HJB equation. The weak-formulation layer and the contract representation are reusable for any continuous-time principal–agent model with drift and volatility control. Contributions of any of these pieces, and proofs of the deterministic milestones, are welcome.
Sutton and Barto's Reinforcement Learning: An Introduction (2nd ed., MIT Press, 2018) is the standard introductory text of the field. Its Chapter 3 sets up the model that the rest of Part I works in: the finite Markov decision process (MDP), the value functions of a policy, and the Bellman equations that relate the value of a state to the values of its successors. Section 3.6 then states the fact every planning and control method of the book relies on: in a finite MDP there is an optimal policy, its value is the unique solution of a system of nonlinear equations, and a policy that acts greedily with respect to that solution is optimal. Dynamic programming (Chapter 4), Monte Carlo control (Chapter 5), Sarsa and Q-learning (Chapter 6) are all methods for solving the Bellman optimality equation; their correctness statements presuppose that it has exactly one solution and that it identifies optimal behaviour.
The book is deliberately informal ("we chose not to produce a rigorous formal treatment", p. xiii): §3.6 asserts these facts without proof. The results themselves are classical, going back to Bellman (1957), Howard (1960) and Blackwell (1965); a textbook proof for discounted finite MDPs is in Puterman, Markov Decision Processes (Wiley, 1994), Chapter 6.
A finite MDP has a finite set of states , a finite nonempty set of actions , a finite set of rewards , and dynamics
Eqs. (3.2)–(3.3). From one derives and , Eqs. (3.4)–(3.5).
A policy gives a probability of each action in each state. Fix a discount rate . The return of a reward sequence is (3.8). The state-value function and action-value function of are the expected returns
In the Lean development these are stateValue M γ π s and actionValue M γ π s a, computed as from the transition matrix and the expected reward of the Markov chain the policy induces. A policy is optimal (IsOptimalPolicy) if for every policy and every state . The optimal value functions are
optimalValue and optimalActionValue, with the maximum over all stochastic policies.
For every finite MDP and :
The goal is what turns "find a good policy" into "solve a system of equations". Parts 3 and 4 identify with the unique solution of (3.19), so any procedure that finds a solution of (3.19) has found ; part 5 converts into an optimal policy by a one-step search. Parts 1 and 2 say that the book's definition (3.15) makes sense: a single policy is simultaneously best at every state, so "the optimal value function" is well defined and shared by all optimal policies. Chapter 4's policy iteration and value iteration, and the fixed points of Q-learning, are statements about this equation. Exercises 3.18 and 3.19 are used, by number, in the proof of the policy gradient theorem (p. 325).
The mathematics is classical and proved in many texts; what is missing is a machine-checked version in the book's own model. Platform relatives exist in different models: FoundationsML.ReinforcementLearning.bellman_equations_unique_solution (uniqueness for a fixed policy, with an expected-reward kernel instead of ), BertsekasDP.discounted_main_theorem (cost minimization over deterministic stationary policies), BanditAlgorithm.mdp_discounted_bellman_solution (existence of a solution with a greedy deterministic policy, rewards in ) and FoundationsRL.RLBasics.bellman_optimality (finite horizon). None of them states the book's result: the four-argument dynamics, stochastic policies, the maximum over all of them, uniqueness of the solution of (3.19), and optimality of every policy supported on greedy actions. This mission produces that statement and, with it, a vocabulary of finite-MDP definitions that the later missions of the series reuse.
The book's derivation of (3.19) (p. 63) starts from with a policy that is optimal at every state at once. The existence of such a policy is the substance of the goal, and it does not follow from the definition: (3.15) takes a separate maximum at each state, and a priori the maximizing policy could depend on the state. Uniqueness for (3.19) is likewise not a consequence of linear algebra, as it is for (3.14): the equation is nonlinear because of the maximum. The fixed point must be related to the value of an actual policy, and every policy's value must be bounded above by it.
S and A are finite types with A nonempty (without an action, is undefined). One action set serves every state, as the book's footnote 3 (p. 48) allows. Rewards form a finite set M.R : Finset ℝ and the dynamics are the four-argument M.p s a s' r with the normalization (3.3).MDP, Policy, trans, expReward, policyTrans, policyReward, stateValue, actionValue, optimalValue, optimalActionValue, IsOptimalPolicy) follow the conventions shared by the whole series and are meant to be merged with the finite-MDP layers of the later chapters. Lemmas on summability of the value series, the Bellman operator as a -contraction in the sup norm, and the Markov-chain identities for are welcome as separate contributions.Thompson Sampling (TS) is the oldest heuristic for the stochastic multi-armed bandit problem: it was proposed by Thompson in 1933 (Biometrika 25) and is used in practice for online advertising and recommendation, where it often performs as well as or better than upper-confidence-bound methods (Chapelle and Li, NIPS 2011; Scott 2010). Until 2012 its theoretical guarantees for the frequentist regret were weak: earlier analyses gave only regret in time (Granmo 2010; May, Korda, Lee and Leslie 2011).
Agrawal and Goyal, Analysis of Thompson Sampling for the Multi-armed Bandit Problem (arXiv:1111.1797v3, COLT 2012), gave the first logarithmic finite-time bound on the expected regret of TS. This mission formalizes their two-armed result, Theorem 1. A companion mission covers the -armed bound, Theorem 2.
Timeline. Lai and Robbins (1985) proved that every consistent algorithm has regret at least . Auer, Cesa-Bianchi and Fischer (2002) gave UCB1 with an finite-time bound. Agrawal and Goyal (2012) proved for two-armed TS. Kaufmann, Korda and Munos (ALT 2012) and Agrawal and Goyal (AISTATS 2013) later proved asymptotically optimal bounds for Bernoulli TS.
There are two arms. Arm has a fixed, unknown reward distribution supported in , with mean . Plays of an arm give i.i.d. rewards, independent of the other arm. Arm 1 is the unique optimal arm, , and is the gap.
Thompson Sampling for general stochastic bandits (Algorithm 2 of the paper) keeps, for each arm , a success count and a failure count , both starting at . In each round it
is the number of plays of arm before round . The expected regret in time is
the expectation being over the rewards and the algorithm's randomness.
The analysis uses the Beta cdf , the binomial cdf , and the random variable : the number of independent draws made before one exceeds .
There is an absolute constant such that for every two-armed instance with rewards in and , and every ,
The constant is not fixed numerically: the paper states the theorem in form (footnote 1), and the explicit display it reports on p. 8, , is not the formal claim.
The result. Theorem 1 shows that TS, a randomized Bayesian heuristic with no explicit confidence bonus, has regret logarithmic in on every two-armed instance, matching the order in of the Lai–Robbins lower bound. The proof introduced a way to control the optimal arm's waiting time between plays through the Beta–Binomial duality, and later analyses of TS reuse that device.
Formalizing it. The result is proved on paper and has no machine-checked proof that we know of. The platform's existing TS results concern Gaussian TS (Lattimore and Szepesvári, Ch. 36) and Bayesian regret, which are different algorithms or regret notions. A formalization adds a reusable Lean model of Algorithm 2 on -valued rewards, Beta–Binomial facts (Fact 1, Lemma 1), a binomial-median theorem, and binomial Hoeffding bounds. It also produces a proof with a constant that has been checked, since the printed constants contain an arithmetic slip.
The standard UCB argument does not transfer to TS. For UCB, the optimal arm's index exceeds its mean with high probability however often the arm has been played, because the exploration bonus is deterministic; the analysis then only has to count plays of the suboptimal arm until its own index concentrates, after plays. Under TS the optimal arm's sample is random and, if the arm has been played rarely or its early rewards were poor, it falls below with constant probability. The optimal arm may then wait a long, random time between plays, and the length of that wait depends on the arm's posterior, which in turn depends on how long it has waited. Counting plays of the suboptimal arm with a union bound over rounds, under the assumption that the optimal arm is already concentrated, therefore does not work; controlling these waiting times is the central difficulty and is where the dependence enters.
StochasticBandit 2 (a probability measure on per arm, mean banditArmMean), with the hypothesis that each reward law gives mass to . Lean arm 0 is the paper's arm 1 and Lean arm 1 the paper's arm 2. Lean rounds are indexed from .Online decision makers often have to choose an action before seeing the cost assigned to it. A no-regret algorithm performs almost as well, in total, as the best single action that could have been chosen after the costs were known. In a related repeated-game problem, Blackwell approachability asks a player to keep the average of vector payoffs close to a desired set despite an adversary's choices. These two performance criteria look different: one compares scalar costs to a fixed benchmark, while the other measures a geometric distance. Abernethy, Bartlett, and Hazan establish algorithmic reductions between them, with explicit finite-horizon bounds in their COLT 2011 paper. This mission isolates the direction that turns an approachability algorithm into an online linear optimization algorithm.
The bound matters even when the input algorithm has no known rate. It relates the regret of the resulting online algorithm to the actual distance attained on the corresponding sequence. Any subsequent guarantee on that distance then yields a regret guarantee through the same reduction. The paper also gives the reverse reduction and an application to calibrated forecasting; those are separate missions in this series.
Fix a dimension and a nonempty compact convex decision set . On round , an algorithm selects using only the preceding cost vectors . The adversary then reveals in the Euclidean unit ball . The incurred linear cost is . For a horizon , regret compares these costs with the cost of the best single point of evaluated on all rounds:
The minimum exists because is nonempty and compact. No probabilistic model for the cost sequence is assumed. The round index begins at one, and cannot depend on .
The reduction uses , the maximum norm of a decision. Write for Euclidean concatenation of a scalar and a vector, an element of . The generated cone of a set consists of its nonnegative scalar multiples, . For a set , its polar cone is . This negative-sign convention is fixed throughout the mission.
Algorithm 1 of the paper constructs a vector-payoff game. Its player actions are , its adversary actions are , its payoff and target are
A Blackwell approachability algorithm for this game chooses each from the preceding adversary moves. Its finite-horizon approachability rate on a given sequence is , where distance means the Euclidean distance from a point to a set. The online algorithm created by Algorithm 1 uses precisely the same choices .
The goal is Theorem 16 of the paper. For every admissible history-based algorithm, every sequence of unit-ball costs, and every , it asserts
This is a statement about the rate actually obtained on the chosen cost sequence. It assumes no upper bound on and does not require an oracle call in the statement. Thus it also covers algorithms whose behavior is specified directly rather than through an implementation of the oracle.
The milestone targets are the distance formula of Lemma 13, the conic distance identity in display (8) of Theorem 16's proof, and the existence of a valid halfspace oracle in Lemma 15. Lemma 13 says distance to a nonempty convex cone equals the attained maximum of a linear functional over the polar cone's unit ball. Display (8) specializes this geometry to Algorithm 1's lifted target. Lemma 15 says that every halfspace containing that target admits a player action whose payoff remains in the halfspace against every permitted adversary move. Together these statements specify the geometry and the oracle needed by the reduction.
Theorem 16 gives a numerical transfer rule: a bound on approachability distance for Algorithm 1's game immediately bounds average regret for the same sequence. Its factor depends only on the size of the decision set. This permits comparison of algorithms in a common finite-horizon language, without replacing the online cost sequence by a distribution or an asymptotic limit. The source paper uses this direction as one half of its equivalence between approachability and no-regret learning Abernethy, Bartlett, and Hazan, 2011.
The mathematical results are established in that paper; the goal here is a machine-checked Lean development of their statements and eventually their proofs. The mission also supplies reusable definitions of generated and polar cones, a Euclidean lift, a finite-history online algorithm, and regret over a compact decision set. Lemma 13 is useful outside this reduction whenever distance to a cone is compared with linear functionals on its polar. The proposed theorem items currently carry open proofs, while their statements and definition files are checked for elaboration in the pinned Lean environment.
The main obstacle is the change of viewpoint from a scalar regret comparison to distance from a set of lifted vector payoffs. A direct comparison of individual round costs does not describe that distance. The target is a polar cone in one additional Euclidean dimension, so a faithful account must keep the lift's geometry, the cone's sign convention, and the normalization by aligned. The distance formula also asserts that its maximum is attained. An encoding that merely writes an infimum or supremum with default values can silently make an edge case look valid without representing the paper's claim.
The oracle milestone has a separate quantifier demand. One selected action must work against every adversary move for each halfspace containing the target. It cannot be replaced by a possibly different action for each move, or by a claim only about tangent halfspaces. The theorem includes halfspaces with arbitrary offsets and zero normals because the source oracle accepts any containing halfspace.
Vectors live in EuclideanSpace ℝ (Fin d), and lives in EuclideanSpace ℝ (Fin (d+1)) with the Euclidean norm. The generated cone uses exactly one nonnegative multiple of a point of the generating set, as in Definition 11. The polar uses , the opposite sign from a positive dual-cone convention. Distances are Euclidean point-to-set distances. All arithmetic is over exact real numbers, and the regret minimum ranges over the image of the nonempty compact set .
The statements require because the source payoff divides by . This excludes the degenerate case , in which the source instance is undefined. They require wherever an average is formed. Admissible histories consist of unit-ball adversary moves, and each round's decision belongs to . The dimension may be zero syntactically, but the positive- hypothesis excludes that case in results using Algorithm 1. These conditions keep the bound from being satisfied through Lean's default values for division by zero, distance to an empty set, or infima over empty sets.
The paper's display (8) writes and labels its unit ball with dimension ; the formalization uses the cone of in , matching Algorithm 1. Lemma 12's printed bipolar claim omits closedness; this mission does not use that uncorrected sentence as a milestone. The oracle statement covers all containing halfspaces. Contributions are welcome for the distance identity, the oracle existence result, and the final regret inequality, as well as geometric lemmas supporting those proofs.
Learning an unknown quantum state is expensive. Full quantum state tomography of a -dimensional mixed state to accuracy in trace distance needs on the order of copies of (O'Donnell–Wright 2016; Haah et al. 2017), and this is optimal. For a system of qubits, , so full tomography is out of reach beyond a few dozen qubits.
Often one does not need the whole density matrix, only the behaviour of on a fixed list of tests: acceptance probabilities of verification circuits, expectation values of observables, or the answers a piece of quantum advice gives to a set of questions. Aaronson (arXiv:1711.01053, STOC 2018) named this task shadow tomography and asked whether the number of copies can be polylogarithmic in both the dimension and the number of tests. Measuring each test on separate copies costs copies, which is linear in .
Timeline.
A mixed state of dimension is a Hermitian positive semidefinite matrix with . A two-outcome measurement is a Hermitian matrix with all eigenvalues in . Equivalently, . It accepts with probability .
The state consists of independent copies of . A measurement of with classical output is a POVM: a finite family of positive semidefinite matrices on the -register space with . Outcome occurs with probability . An adaptive procedure that measures the copies one after another is described by one such POVM.
Problem 1 (shadow tomography). Given an unknown and known two-outcome measurements , output numbers with for all , with success probability at least . The output must come from a measurement of , with as small as possible. The measurement may depend on the , but not on .
There is a universal constant such that, for and , Problem 1 is solvable with
copies. This is the last display of the proof (p. 19). The goal fixes no constant, so any improvement of remains consistent with it.
The result. Theorem 2 shows that a state of exponential dimension can be learned "for all practical purposes" on exponentially many tests from polynomially many copies. Applications in the paper include a bound on quantum advice and one-way communication, and implications for quantum money and copy-protection. It also shows that the information needed to predict many measurement outcomes is far smaller than the description of .
Formalizing it. The theorem is proved in the paper, and later work improves its exponents. As far as is known it has not been machine-checked. A complete development formalizes the gentle-measurement toolkit (Lemma 12, Lemma 14, Lemma 15), the amplification of two-outcome measurements on tensor powers, and the postselection argument. These are standard tools of quantum learning theory and quantum complexity with no formal counterpart yet. Lemma 14 and Lemma 15 are reusable beyond this mission.
The naive approach measures the directly on shared copies. A measurement that is likely to reject disturbs the state, so later measurements see a damaged state, and separate copies per measurement cost copies.
The proof needs three ingredients:
The potential argument has to hold for the state after postselection, which is correlated or entangled across registers. Independence-based concentration fails there, which is why the Markov claim, not a Chernoff bound, governs that step. Theorem 13 itself rests on a delicate ancilla-based procedure of Harrow, Lin and Montanaro, and the mission cites it as a milestone without its proof.
WildeQIT.IsDensityOperator (positive semidefinite, trace one).IsEffect E: both and are positive semidefinite.Fin k → n.The multi-armed bandit is the simplest setting in which a learner must trade off exploiting what it knows against exploring what it does not: one situation, actions, and a reward drawn from an unknown distribution each time an action is taken. Chapter 2 of Sutton and Barto's Reinforcement Learning: An Introduction (2nd ed., MIT Press, 2018) uses it to introduce, in the smallest possible setting, ideas that run through the rest of the book: incremental estimation with a step size, the bias introduced by the initial estimate, soft-max policies over learned preferences, and learning by following the gradient of expected reward.
The chapter ends with the gradient bandit algorithm (§2.8), which learns a numerical preference for each action instead of a value estimate. A shaded box on pp. 38–40 shows that its expected update is exactly a gradient-ascent step on the expected reward, so the algorithm is an instance of stochastic gradient ascent. The same argument, a score-function (likelihood-ratio) identity with a baseline, reappears in Chapter 13 as the REINFORCE algorithm and the policy gradient theorem. The bandit case is where the book first carries it out in full.
Actions are . Each action has a reward distribution on with finite mean , the true action value. At each step the learner holds a vector of action preferences and selects action with the soft-max probability
Given , a reward is received. The expected reward is , a smooth function of . With a step size and a baseline , the gradient bandit update (2.12) is
The chapter's estimation sections use a single action's rewards . The sample average after selections is , with an arbitrary initial value . A constant step size updates (2.5). The trace of one , defines the step size (2.8)–(2.9).
For every action , with and ,
that is, the update (2.12) equals the exact gradient-ascent step (2.13) in expected value, for every baseline that does not depend on the selected action.
The result. The identity makes a model-free algorithm, which uses only the sampled action and reward, an unbiased estimator of the gradient of a quantity that depends on the unknown . It therefore places the gradient bandit algorithm within stochastic approximation, where convergence theory for stochastic gradient methods applies. It also explains the role of the baseline: any baseline independent of the action leaves the expected update unchanged, so the choice of baseline can only affect the variance of the update, as Figure 2.5 shows empirically. The estimation milestones make precise two claims the chapter uses repeatedly: sample averages can be maintained incrementally, and constant step sizes produce an exponentially recency-weighted average biased by . Exercise 2.7 removes that bias.
Formalizing it. All of these results are elementary and proved (or left as routine exercises) in the book. None of them is formalized on Prove2Me or, as far as is known, in Mathlib. What this mission adds is a machine-checked version of the book's argument with the reward model and baseline condition stated precisely, and a reusable soft-max layer (definition, partial derivatives, shift invariance) for later missions of this series, in particular the policy gradient theorem of Chapter 13.
The mathematics is beginning calculus, as the book says. The formal difficulty lies elsewhere. The goal is an identity between an expectation over a two-stage random experiment (an action from , then a reward from ) and a partial derivative in one coordinate of a vector-valued parameter. A proof has to justify exchanging the finite sum with the derivative and splitting the reward integral, and it has to use integrability of each . It also needs the fact that the baseline term vanishes because . A scalar-parameter version of the log-sum-exp derivative does not suffice: the book differentiates in one coordinate while all other preferences are held fixed. For Exercise 2.7 the obvious unrolling of (2.6) does not apply directly, because the step size varies with and the book states neither the weights nor the range of .
Fin k. Every statement quantifies over some action, so whenever it has content. Preferences are vectors Fin k → ℝ. The partial derivative in coordinate is the derivative of at . The soft-max derivative milestone is stated with HasDerivAt, so it also asserts differentiability.Integrable identity and mean . The expectation of a function of is . The book's normal-distribution testbed is only an example.In make-to-order production, chemical process industries and other manufacturing settings modelled as projects, activities do not only occupy machines for a while: they also consume intermediate products at their start and deposit products into storage facilities at their completion. Storage is bounded above by a tank or warehouse capacity and below by a safety stock. Resources of this kind are called cumulative resources (or inventory resources, reservoirs in the constraint-programming literature). They were introduced into resource-constrained project scheduling by Neumann and Schwindt (2002), and Chapter 2 of Neumann, Schwindt and Zimmermann, Project Scheduling with Time Windows and Scarce Resources (2nd ed., Springer 2003), develops their theory in §2.12.
A scheduler handling cumulative resources needs a finite combinatorial description of which schedules respect the inventory bounds at every instant, because the time axis is continuous and cannot be checked point by point in a search procedure. Theorem 2.12.4 of the book gives such a description, and it is the basis of the branch-and-bound procedure of Neumann and Schwindt for the problem .
A project consists of activities with , where is the project beginning and the project completion. Activity has an integer duration , with and for the real activities.
For each cumulative resource in a set , every activity has an integer demand . If , activity withdraws units of at its start; if , it deposits units at its completion; means is not used. The demand of the project beginning is the initial stock. Write and . Each resource has a safety stock and a storage capacity .
A schedule is a vector of real start times with and . The active set and the inventory of at time are
The schedule is inventory-feasible if for all and all .
Two standing assumptions of the section are used throughout: (2.12.1) , so the final inventory is admissible; and Remark 2.12.2, .
A nonempty is a -surplus set if , and a -shortage set if . A -surplus set is minimal if no -surplus set arises from by removing a nonempty set of replenishing activities, and none arises by adding a nonempty set of depleting activities. Minimal -shortage sets are defined with the roles of replenishing and depleting activities exchanged. and denote the minimal -surplus and -shortage sets.
A schedule is inventory-feasible if and only if
The theorem turns a constraint over a continuum of time points into finitely many disjunctions, each a choice among precedence relations. An inventory excess caused by a minimal surplus set is removed by a start-to-completion relation (a replenishment is postponed until after a withdrawal starts, equivalently a maximum time lag), and a shortage by a completion-to-start relation . Consequences stated in the book: the feasible region of is a finite union of polyhedra; branching on these relations, organized as pairs of strict orders and reflexive relations, is a complete search scheme; and minimal delaying alternatives for surplus and shortage sets can be enumerated. Because every problem with renewable resources can be rewritten as one with cumulative resources (p. 130), the book also concludes that this union of polyhedra is in general disconnected.
The result is proved in the book (and in Neumann and Schwindt, 2002). To our knowledge it has no machine-checked proof. This mission produces a Lean formalization of the model, of the one-sided minimality notion, and of the two-sided characterization with its supporting lemma.
The combinatorial core is simple to state but easy to state wrongly. The natural first idea, to use inclusion-minimal surplus sets as for renewable resources, gives a different family and a false theorem: the book's minimality allows removing only replenishing activities and adding only depleting ones. The existence lemma needs Remark 2.12.2 to keep at least one replenishing activity in the minimal set, and the sufficiency direction needs (2.12.1) to guarantee a depleting activity outside the minimal set. Both membership conditions of the active set are closed at , so activities that deplete or replenish exactly at the critical instant must be counted on the correct side; a half-open reading changes which schedules are feasible. The initial stock is handled by the same active-set rule as any other demand, which matters for the invariance claim.
Fin (n + 2), activity is Fin.last (n + 1); resources are an arbitrary type K. Demands, safety stocks and capacities are integers (ℤ); start times are reals (ℝ); durations are natural numbers cast to ℝ.TotalDemandWithinBounds, BoundsStraddleZero) wherever the book's proofs use them. Surplus and shortage sets are nonempty by definition, and minimality uses proper inclusions.Reusable parts: the cumulative-resource model and inventory profile, which later missions on continuous cumulative resources (§2.12.2) or on the NP-completeness of (Theorem 2.12.1) can build on. Contributions welcome: proofs of the lemmas, of either half of the theorem, and finite-sum lemmas about Finset.filter that the proofs need.
The smallest enclosing ball problem asks, for finitely many points , for a ball of the smallest radius that contains all of them. It appears in clustering, in collision detection and bounding-volume hierarchies, in facility location (placing one service point so that the farthest client is as close as possible), and in the analysis of geometric algorithms. Sylvester posed the planar version in 1857; Megiddo (1983) gave a linear-time algorithm in fixed dimension, and Welzl (1991) a simple randomized one.
This mission formalizes Section 8.7 of Matoušek and Gärtner, Understanding and Using Linear Programming (Springer, 2007), which uses the problem to introduce convex programming. Unlike the geometric problems of the book's Chapter 2, the smallest ball cannot be written as a linear program. The section shows instead that it is a convex quadratic program, derives the Karush–Kuhn–Tucker (KKT) conditions for convex programs in equational form from the duality theorem of linear programming, and uses them to prove that the smallest enclosing ball exists and is unique. It is the book's bridge from linear to convex optimization.
A function is convex if for all and . A convex program in equational form is
with a real matrix with columns , and convex. A vector is feasible if and componentwise, and optimal if it is feasible and for every feasible . For differentiable , is the row vector of partial derivatives, so is a scalar.
For points , write and let be the matrix whose th column is . The program studied is
A ball is a closed Euclidean ball . The ball is the unique smallest enclosing ball of a set if , , every ball containing has radius at least , and every ball containing of radius at most has center .
For points , the objective of (8.15) is convex, and
The result. Theorem 8.7.4 gives existence and uniqueness of the smallest enclosing ball together with an explicit certificate: the center is a convex combination of the input points, the squared radius is the negated optimum value, and the points with lie on the boundary. It reduces the geometric problem to a convex quadratic program, for which interior-point and simplex-type solvers exist, and it is the basis of the combinatorial characterization "the center lies in the convex hull of the boundary points" used by Welzl-type algorithms. Proposition 8.7.2 is the KKT theorem for equational-form convex programs; it holds without any constraint qualification because the constraints are linear.
Formalizing it. All results here are classical and proved in the book; none is open. The mission produces machine-checked statements and, when solved, proofs of: the first-order optimality criterion for convex functions on convex sets in ; the equational-form KKT theorem derived from LP duality; the boundary characterization of unique smallest enclosing balls; and existence and uniqueness of the smallest enclosing ball in every dimension. Mathlib has first-order necessary conditions at local minima and general convexity theory, but no KKT theorem for linearly constrained convex programs in this form and no smallest-enclosing-ball theory.
Existence of an optimum and convexity of are routine. For the KKT conditions, the necessary direction needs multipliers, which do not come from calculus alone: the obvious Lagrange-multiplier argument handles only equality constraints and says nothing about the sign pattern forced by . For the goal, a solver must connect three layers — the gradient of a quadratic form in matrix notation, the multiplier conditions, and the Euclidean geometry of distances to — and uniqueness of the ball does not follow from uniqueness of the optimizer , which in general is not unique (repeated or cospherical points). The statement quantifies over all optimal and asserts that they all yield the same center.
Fin n → ℝ, so the book's indices become . Points of are EuclideanSpace ℝ (Fin d), so and are Euclidean. The matrix is Matrix (Fin d) (Fin n) ℝ.ContDiff ℝ 1 f. Convexity is ConvexOn ℝ Set.univ f.Fin n → ℝ, LP duality for the pair (maximize , , ) / (minimize , ), compactness of the standard simplex, and elementary Euclidean geometry. The first-order criterion and the KKT theorem are reusable beyond this mission; proofs through any route are welcome.