Optimization

Motivation

A network of resistors solves an optimization problem. Nobody tells the electrons what to do; each one moves under a purely local rule, and the current distribution that emerges minimizes energy dissipation over all distributions satisfying Kirchhoff's node law. Add a wire and the network can only become easier to traverse. This is the encouraging case, and Chapter 4 of Frank Kelly and Elena Yudovina's Stochastic Networks (Cambridge University Press, 2014) opens with it.

Road traffic is the discouraging case. Drivers also follow a local rule — take the fastest route — and the pattern that emerges is again characterized by an optimization problem, but not the one anyone wants solved. Braess's paradox is the sharp form of the discrepancy: in a small road network carrying six cars per unit time, every route takes 83 time units at equilibrium; open an extra road, and at the new equilibrium every route takes 92. Building road capacity made everyone slower. The difference from the electrical case is that a driver's choice imposes a delay on everyone else sharing the road and the driver does not pay for it, and correcting that — pricing the externality — is how a decentralized rule can be made to produce good global behaviour. That idea recurs in Chapters 7 and 8 of the book as the basis of Internet congestion control.

Setting

The network is a set $\mathcal{J}$ of $J$ directed links. A route $r$ is a subset of links, and $\mathcal{R}$ is the set of $R$ routes under consideration — not necessarily all physically possible ones. The link-route incidence matrix $A$ has $A_{jr}=1$ when $j \in r$ and $A_{jr}=0$ otherwise. Writing $x_r$ for the flow on route $r$, the flow on link $j$ is

Each link has a delay function $D_j(y_j)$, continuous and increasing in the flow on that link, and the delay along a route is the sum of the delays of its links, $\sum_j D_j(y_j)A_{jr}$. Drivers care only about getting from origin to destination: $\mathcal{S}$ is the set of source–destination pairs, each route $r$ serves exactly one of them, written $s(r)$, and the flow requirement between pair $\sigma$ is $f_\sigma$.

A routing pattern is stable when no driver has an incentive to switch. Definition 4.2 makes this precise: a Wardrop equilibrium is a feasible vector of route flows $x$ such that

Every route actually carrying traffic is a shortest route, in delay, for the traffic it carries.

Formalization targets

Goal — Theorem 4.3, a Wardrop equilibrium exists

The goal asserts existence only, for an arbitrary network, arbitrary route set and arbitrary continuous increasing delay functions. It fixes no uniqueness claim, because the equilibrium flows need not be unique even though the link loads are, and no efficiency claim, because Braess's paradox is precisely the statement that the equilibrium is not efficient.

Supporting levels

Kirchhoff's node law as the equations satisfied by the expected reward in the random-walk game of section 4.1; the two Braess networks of Figures 4.4a and 4.4b, with their equilibrium delays $83$ and $92$; convexity of $\int_0^{y}D(u)\,du$ for increasing $D$; the optimization characterization that makes the goal reachable — a minimizer of $\sum_j\int_0^{y_j}D_j(u)\,du$ over the feasible flows is a Wardrop equilibrium; and the exact externality decomposition of the queueing network of section 4.3.1.

Significance

The result itself. Theorem 4.3 is what makes the Wardrop equilibrium a usable object: a traffic model that could fail to have an equilibrium would be describing nothing. Its proof does more than establish existence — it identifies the equilibrium as the solution of a specific convex program, minimizing $\sum_j\int_0^{y_j}D_j(u)\,du$. That function is not the total delay $\sum_j y_jD_j(y_j)$, and the gap between the two is exactly Braess's paradox: selfish routing optimizes the wrong objective. Once the two objectives are written side by side, the fix is readable off them, and it is the fix used in practice — a toll on link $j$ equal to $y_jD_j'(y_j)$, the marginal delay a driver imposes on everyone else, makes the selfish objective coincide with the social one. Section 4.3 then carries the same accounting into queueing and loss networks, where the derivative of the mean cost splits into a term for the delay a customer suffers and a term for the knock-on cost it inflicts.

Formalizing it. Nothing here is open; Wardrop stated the principle in 1952 and Beckmann, McGuire and Winsten gave the optimization formulation in 1956. What the mission produces is a machine-checked model of selfish routing — incidence matrix, link flows, delay functions, the equilibrium condition — and a formal record of Braess's paradox as a concrete pair of networks rather than a story. Mathlib has no traffic or congestion-game theory.

Difficulty

Existence is not a fixed-point argument in the obvious variable: the best-response map of the routing game is not continuous, since a small change in flows can flip which route is shortest and move all the traffic. The book's route is to replace the equilibrium condition by the stationarity conditions of a convex program on a compact feasible set, where existence is routine and the content is the translation. The translation is where the care is needed, and it is stated here as a separate milestone: the first-order conditions say the Lagrange multiplier $\lambda_{s(r)}$ equals the route delay on routes carrying traffic and is a lower bound on the others, which is Definition 4.2 restated.

The subtlety worth naming in advance is that "increasing" is doing real work in two different places. It makes $\int_0^{y}D(u)\,du$ convex, which is what makes the program tractable; and it is what makes each $D_j(y_j)$ interpretable as a price. Neither convexity of $D_j$ itself nor strict monotonicity is needed, and assuming them would be assuming more than the book does.

Formalization scope

Links, routes and source–destination pairs are indexed by finite types. The incidence matrix is real-valued with entries constrained to be $0$ or $1$, matching the book's definition in this chapter (unlike Chapter 3, which allows general non-negative integers). The map from routes to source–destination pairs is given as a function $s$ rather than as the matrix $H$, which is exactly the book's statement that each column of $H$ sums to $1$.

Delay functions are total functions $\mathbb{R}\to\mathbb{R}$, continuous and monotone. This excludes the vertical asymptote that Figure 4.5 permits — a link with a finite capacity at which delay blows up — and that restriction is recorded here rather than left implicit. The equilibrium condition is stated as the inequality "$\text{delay on } r \le \text{delay on } r'$ for every $r'$ serving the same pair", which is Definition 4.2 with the minimum written out; the two are equivalent because $r$ itself serves $s(r)$, and the inequality form avoids having to produce a minimum over a possibly empty set.

The goal is not vacuous: the feasibility hypotheses ($f_\sigma\ge0$, and each source–destination pair served by at least one route) are exactly what makes the feasible set non-empty, and without them the existence claim would be false rather than trivial.

Contributions welcome beyond the listed items: uniqueness of the equilibrium link loads $y$; the marginal-cost toll that aligns the selfish and social optima; Rayleigh monotonicity (Exercise 4.3, that effective resistance does not decrease when a resistance is increased); the price of anarchy for affine delays; and Theorem 4.6 on the derivatives of the loss-network rate of return with respect to offered traffic and capacity.

Selected references

• Frank Kelly and Elena Yudovina, Stochastic Networks, Cambridge University Press, 2014, Chapter 4 (pp. 85–107); Definition 4.2, Theorem 4.3, sections 4.1–4.3. DOI 10.1017/cbo9781139565363
• J. G. Wardrop, Some theoretical aspects of road traffic research, Proceedings of the Institution of Civil Engineers 1 (1952), 325–362. DOI 10.1680/ipeds.1952.11259
• M. Beckmann, C. B. McGuire and C. B. Winsten, Studies in the Economics of Transportation, Yale University Press, 1956.
• D. Braess, Über ein Paradoxon aus der Verkehrsplanung, Unternehmensforschung 12 (1968), 258–268. DOI 10.1007/BF01918335
• Peter Doyle and J. Laurie Snell, Random Walks and Electric Networks, Mathematical Association of America, 1984. arXiv:math/0001057
• R. G. Gallager, A minimum delay routing algorithm using distributed computation, IEEE Transactions on Communications 25 (1977), 73–85. DOI 10.1109/TCOM.1977.1093711

Motivation

Many results in economics and operations research reduce to a single question: does a system of interacting, mutually reinforcing choices settle at an equilibrium? A firm choosing input levels that are complements, a Cournot duopoly whose best responses move together, a matching market where agents' preferences reinforce assortative pairings — each is a fixed-point problem, but classical fixed-point theory (Brouwer, Kakutani) asks for convexity and continuity that these problems rarely have. Tarski's fixed point theorem [1955] showed that order, not topology, suffices: every increasing (monotone) self-map of a nonempty complete lattice has a fixed point, and the fixed points themselves form a nonempty complete lattice, with no continuity or convexity assumed at all. Zhou [1994] extended this from single-valued functions to set-valued correspondences, which is what is needed once "best response" becomes "the (possibly non-unique) set of optimizers." This mission formalizes Zhou's theorem (Topkis's Theorem 2.5.1) together with its parametric extension (Theorem 2.5.2), the two capstones of the lattice-theoretic toolkit that the rest of Topkis's monograph — and, within this series, its mission on supermodular games (Supermodularity and Complementarity V) — builds on directly.

Setting

A lattice $(X, \preceq)$ is a partially ordered set in which every pair of elements $x, y$ has a join $x \vee y$ (least upper bound) and a meet $x \wedge y$ (greatest lower bound). $X$ is a complete lattice if every subset (not just every pair) has a supremum and an infimum in $X$; a nonempty complete lattice always has a greatest element $\top$ and a least element $\bot$.

To compare sets of points — not just points — Topkis defines the induced set ordering $\sqsubseteq$: for $A, B \subseteq X$, $A \sqsubseteq B$ holds when every $a \in A$ and $b \in B$ satisfy $a \wedge b \in A$ and $a \vee b \in B$. Restricted to singletons, $\{a\} \sqsubseteq \{b\}$ says exactly $a \preceq b$, so $\sqsubseteq$ is the natural extension of $\preceq$ from points to sets, and it is the order with respect to which set-valued maps (correspondences) $Y : X \to \mathcal{P}(X)$ are called increasing: $x \preceq x'$ implies $Y(x) \sqsubseteq Y(x')$.

A subset $S \subseteq X$ is a sublattice if it is closed under the binary join and meet of $X$. $S$ is subcomplete if, more strongly, the supremum and infimum in $X$ of every nonempty subset of $S$ exist and lie in $S$ — so a subcomplete sublattice is itself a complete lattice under the order it inherits. A point $x \in X$ is a fixed point of a correspondence $Y$ if $x \in Y(x)$.

Formalization targets

Goal — Theorem 2.5.1 (Zhou's fixed point theorem)

Let $X$ be a nonempty complete lattice and $Y : X \to \mathcal{P}(X)$ an increasing correspondence with $Y(x)$ subcomplete for every $x$. Then:

and the set of fixed points of $Y$, under its inherited order, is itself a nonempty complete lattice.

Theorem 2.5.2 (the parametric extension)

Let $T$ be a partially ordered set and $Y(x,t)$ a jointly increasing, subcomplete-valued correspondence on $X \times T$. Then for each $t$ the greatest and least fixed points $g(t)$, $l(t)$ of $Y(\cdot, t)$ exist and are increasing functions of $t$; under the further hypothesis that $\sup Y(x',t') \prec \inf Y(x',t'')$ whenever $t' \prec t''$, both become strictly increasing in $t$. This is the theorem that gives comparative statics their bite: it says an equilibrium moves monotonically — even strictly — as a parameter of the underlying system changes.

Two supporting results are formalized as milestones because Theorem 2.5.1's own proof invokes them directly: Lemma 2.4.2 (supremum and infimum are monotone under $\sqsubseteq$, whenever they exist) and Theorem 2.4.2 (an intersection of increasing correspondences, if it stays nonempty, is itself increasing).

Significance

The result itself. Tarski–Zhou is the order-theoretic alternative to Brouwer–Kakutani: where the latter needs a convex, compact strategy space and a continuous map, Tarski–Zhou needs only a lattice order and monotonicity, and it delivers something Brouwer–Kakutani does not — a greatest and a least fixed point, with an explicit order-theoretic formula for each, and the guarantee that the whole fixed-point set is a complete lattice in its own right. This is exactly the machinery behind existence proofs for supermodular games (Topkis's own Theorem 4.2.1, where the fixed points of the best-response correspondence are the pure-strategy Nash equilibria) and behind monotone comparative statics more broadly (Milgrom–Roberts [1994], of which Theorem 2.5.2 is a strict generalization to correspondences).

Formalizing it. Mathlib already has Tarski's theorem for single-valued monotone functions (OrderHom.lfp/gfp, fixedPoints.completeLattice, Knaster–Tarski). Nothing in Mathlib currently proves it for set-valued correspondences: this mission is a genuine strengthening of existing formalized mathematics, not a restatement of it, and it introduces the induced set ordering and subcompleteness — reused throughout the rest of this book's mission series — for the first time.

Difficulty

The natural first idea — "apply Knaster–Tarski to some selection function built from $Y$" — fails because there is no canonical way to select a single point from each $Y(x)$ that remains monotone without already knowing the theorem: an arbitrary selection from an increasing correspondence need not itself be increasing (this is exactly the subtlety Topkis's Theorem 2.4.3 addresses only for correspondences with a greatest/least element). The real argument instead builds the candidate fixed point directly as a supremum over an auxiliary set $\{x : Y(x) \cap [x,\infty) \neq \emptyset\}$ and establishes it is a fixed point using the monotonicity lemma (Lemma 2.4.2) at each step — no selection is ever made. A second subtlety is that the fixed-point set is not, in general, a sublattice of $X$: Topkis's Example 2.5.1 exhibits an increasing self-map of $[0,3]^2 \subset \mathbb{R}^2$ whose four fixed points are not closed under $\vee$/$\wedge$. Part (b)'s claim that the fixed points form their own complete lattice must therefore be proved without ever assuming, or implying, that ambient joins and meets of fixed points are again fixed points.

Formalization scope

$X$ is formalized as an abstract CompleteLattice, not ℝⁿ — the theorem is genuinely about order, and specializing to $ℝⁿ$ would hide exactly the generality Zhou's result adds over finite-dimensional fixed-point theorems. The induced set ordering InducedSetOrder and the predicate Subcomplete are defined once in this mission and reused by every later mission in the series that reasons about correspondences ordered by $\sqsubseteq$. A formalization that replaced the correspondence $Y$ by a single-valued function would trivialize the mission into a restatement of Mathlib's existing Knaster–Tarski theorem; the set-valued, subcomplete-ranged correspondence is not an optional generality but the entire content being added. Part (b) of Theorem 2.5.1 is formalized as a completeness statement about the induced order on the fixed-point set itself — not as a claim that the fixed-point set is closed under $X$'s ambient join and meet, which Example 2.5.1 refutes. "Partially ordered set" throughout is Lean's PartialOrder, matching the book's own usage in Chapter 2.

Selected references

• Tarski, A., A lattice-theoretical fixpoint theorem and its applications, Pacific Journal of Mathematics 5(2), 1955, pp. 285–309. https://doi.org/10.2140/pjm.1955.5.285
• Zhou, L., The set of Nash equilibria of a supermodular game is a complete lattice, Games and Economic Behavior 7(2), 1994, pp. 295–300. https://doi.org/10.1006/game.1994.1051
• Milgrom, P. and Roberts, J., Comparing equilibria, American Economic Review 84(3), 1994, pp. 441–459. https://www.jstor.org/stable/2118061
• Topkis, D. M., Supermodularity and Complementarity, Princeton University Press, 2011 (DOI 10.1515/9781400822539), Chapter 2, §2.2–2.5.

Motivation

Two-stage stochastic programs with recourse require evaluating $Q(x) = \mathbb E_\xi[Q(x,\xi)]$, the expected value of a recourse function, at every candidate first-stage decision $x$. When $\xi$ is high-dimensional or continuously distributed, this expectation is a multivariate integral of a piecewise-linear, generally nondifferentiable integrand, and classical quadrature rules — built for smooth integrands in low dimension — do not apply (Birge & Louveaux, §8.1). What does apply is convexity: $Q(x,\cdot)$ is convex whenever the recourse problem is a linear program in $\xi$, and convexity alone is enough to sandwich $\mathbb E_\xi[Q(x,\xi)]$ between two computable discrete approximations. This chapter develops that sandwich, and it is the standard device used throughout the stochastic-programming literature to bound and iteratively refine the recourse function: the lower bound goes back to Jensen [1906]; the upper bound is due to Edmundson [1956] and Madansky [1959], with the mean-consistent LP refinement due to Madansky [1960] and Gassmann & Ziemba [1986]. Refinements of both bounds appear in Huang, Ziemba & Ben-Tal [1977], Kall & Stoyan [1982] and Frauendorfer [1988].

Setting

Fix a probability space $(\Omega, \mathcal F, P)$ and an integrand $g : D \times \Xi \to \mathbb R$, where $\Xi \subseteq E$ is the (convex, closed) support of a random vector $\xi : \Omega \to \Xi$ and $E$ is a real vector space (in the recourse application, $g(x,\cdot) = Q(x,\cdot)$ and $D$ is the first-stage feasible region). Write $\mathbb E(g(x)) = \mathbb E_\xi[g(x,\xi)] = \int_\Xi g(x,\xi)\, P(d\xi)$.

A partition of $\Xi$ into $\nu$ measurable blocks $S^\nu = \{S_1,\dots,S_\nu\}$ determines, for each block, its probability $p_l = P[\xi \in S_l]$ and its conditional mean $\xi^l = \mathbb E[\xi \mid S_l]$. Equivalently — and this is the convention this mission's Lean development uses — the blocks may be taken directly on the sample space as the pulled-back sets $S_l = \xi^{-1}(\text{region}_l) \subseteq \Omega$, with $p_l = P(S_l)$ and $\xi^l = p_l^{-1}\int_{S_l}\xi\,dP$ the Bochner integral average of $\xi$ over the block; the two descriptions coincide.

Formalization targets

Goal — Chapter 8, Theorem 1 (Jensen lower bound), p. 346

This is the sharpest statement the chapter proves for the lower bound: it holds for every finite measurable partition, with no assumption beyond convexity of $g(x,\cdot)$ and integrability.

Chapter 8, Theorem 2 (Edmundson-Madansky upper bound), pp. 347-348

For $\Xi$ compact, let $\mathrm{ext}\,\Xi$ be the extreme points of $\mathrm{co}\,\Xi$, carrying the Borel field of all its subsets. If, for every $\xi \in \Xi$, $\varphi(\xi,\cdot)$ is a probability measure on $\mathrm{ext}\,\Xi$ with barycenter $\xi$ (i.e. $\int_{\mathrm{ext}\,\Xi} e\,\varphi(\xi,de) = \xi$) and $\omega \mapsto \varphi(\xi(\omega), A)$ is measurable for every $A$, then

Together the two targets give the chapter's headline sandwich: for convex $g(x,\cdot)$, the finite-partition Jensen value and the Edmundson-Madansky value bracket the true expectation, and refining the partition (resp. the disintegration) tightens both sides toward it.

Significance

The Jensen bound is the workhorse of discrete-distribution approximation in stochastic programming: it is what makes $Q^\nu(x) = \sum_l p_l Q(x,\xi^l)$ a valid, refinable lower-approximation of the true recourse function, and it underlies the partition-refinement schemes (§8.2, following Birge & Wets [1986] and Frauendorfer & Kall [1988]) used inside the $L$-shaped method and separable-programming solvers described later in the chapter (§8.3). The Edmundson-Madansky bound is its indispensable upper counterpart: without it there is no certificate of how far a lower approximation can be from the truth, and the mean-consistent LP refinement (eq. 2.9, not part of this mission) reduces to a moment-problem computation over $\lambda$. Both bounds are, to date, unformalized: the platform holds no theorem matching either a finite-partition conditional-Jensen inequality or an extreme-point disintegration bound (searched GET /theorems?q=... for "Jensen", "conditional expectation", "Edmundson Madansky", "partition convex" — no relevant hits), so this mission is a first formalization of both, not a reformulation of existing platform content. Mathlib supplies the raw convexity substrate this mission is built from — finite Jensen (Analysis/Convex/Jensen.lean) and, critically, the set-average integral Jensen inequality (ConvexOn.map_set_average_le in Analysis/Convex/Integral.lean), exactly the per-block step the book's proof of Theorem 1 performs — but no existing lemma assembles these into the partitioned, conditional-mean statement the book actually states.

Difficulty

The obvious shortcut is to prove "convex functions lie above their tangent line" and stop — this captures no partition structure at all and is not the theorem the book states (the theorem is about $\Sigma_l p_l g(x,\xi^l)$, a sum over blocks, not a single linearization). The real content is bookkeeping across the partition: writing $\mathbb E(g(x))$ as $\sum_l P(S_l)\,\mathbb E[g(x,\xi)\mid S_l]$ (an exact identity, no convexity needed), then applying ordinary Jensen inside each block to replace $\mathbb E[g(x,\xi)\mid S_l]$ by $g(x,\xi^l)$ from below — the inequality only enters at the second step, once per block. Proving this in Lean means correctly discharging, for every block, the side conditions Mathlib's integral-Jensen lemma needs (closedness of $\Xi$, continuity of $g(x,\cdot)$ on $\Xi$, integrability on the block) and then summing the $\nu$ per-block inequalities against weights $p_l$ that themselves depend on the partition — an easy step to get wrong by, e.g., letting $\xi^l$ be an arbitrary point of $S_l$ rather than exactly its conditional mean, which understates what Jensen actually forces. Theorem 2 additionally requires setting up the disintegration $\lambda$ correctly: $\lambda$ is a probability measure defined as an integral of the kernel-like family $\varphi$ against $P\circ\xi^{-1}$, and both the barycenter condition on $\varphi$ and the measurability of $\omega \mapsto \varphi(\xi(\omega),A)$ are load-bearing — dropping either makes $\lambda$ ill-defined or the bound's proof inapplicable.

Formalization scope

$\Xi \subseteq E$ for $E$ a complete real normed vector space (NormedAddCommGroup E, NormedSpace ℝ E, CompleteSpace E); no finite-dimensionality is assumed since neither theorem's proof needs it. The parameter $x$ ranges over an arbitrary type $\alpha$ with $D \subseteq \alpha$, and $g$ is left as a bare function α → E → ℝ, matching the book's level of abstraction (the recourse LP's own data $A,b,c,q,W,T,h$ is never used in either proof).

The partition is formalized directly on the sample space $\Omega$ (a Partition structure: pairwise-disjoint measurable blocks covering $\Omega$, each of positive measure) rather than on $\Xi$, per the equivalence noted under Setting; $\xi^l$ is defined as the Bochner-integral average $p_l^{-1}\int_{S_l}\xi\,dP$, so it is forced to be the conditional mean and cannot be weakened to an arbitrary sample point of the block — the change the chunk brief flags as the main faithfulness trap for this chapter.

Two explicit hypotheses are added beyond the book's own statement of Theorem 1, both needed by Mathlib's integral-Jensen lemma rather than narrowings of the mathematical content: ContinuousOn (g x) Ξ (finite-dimensional convex functions are automatically continuous on the interior of their domain, which is what the book implicitly relies on; stated explicitly since $E$ is not assumed finite-dimensional) and integrability of $\xi$ and of $g(x,\xi(\cdot))$ (needed for $\mathbb E(g(x))$ and each $\xi^l$ to be well-defined). For Theorem 2, the disintegrating family $\varphi$ is E → Measure Ext for an abstract type Ext (standing for $\mathrm{ext}\,\Xi$) with the discrete MeasurableSpace (every subset measurable, matching the book's "Borel field ... the collection of all subsets"), mapped into $E$ by an embedding toE whose range is exactly (convexHull ℝ Ξ).extremePoints ℝ; the measure $\lambda$ (named μExt in the Lean code, since λ is a reserved keyword) is a hypothesis satisfying its defining equation (2.6) rather than constructed, since constructing a measure from a set function is a separate, book-external piece of measure theory the chapter's own proof does not perform either — it simply asserts $\lambda$ is the probability measure with that value on every set.

A trivializing formalization is ruled out explicitly: a version that lets $\xi^l$ range over an arbitrary point of $S_l$, or that proves only the ordinary (unconditional) Jensen inequality without ever introducing the partition, states something strictly weaker than the book and is not what is formalized here.

Both draft theorems end in := by sorry; a full Lean proof of Theorem 1 combines Mathlib's ConvexOn.map_set_average_le applied per block with the exact decomposition of $\int_\Omega$ into $\sum_l \int_{S_l}$ over the partition's disjoint, covering blocks. Reusable beyond this mission: the Partition structure and its weight/condMean accessors generalize to any chapter needing a finite measurable partition with conditional means (this book's later approximation schemes, §8.2-8.5 and Chapter 10, all build on the same device). Contributions solving either theorem, or formalizing the partition-refinement monotonicity $\mathbb E(g(x)) \ge \mathbb E^{\nu+1}(g(x)) \ge \mathbb E^\nu(g(x))$ (eq. 2.3, not part of this mission's milestone list since it is not itself a numbered theorem) as a follow-up, are welcome.

Selected references

• J.R. Birge, F. Louveaux, Introduction to Stochastic Programming, 2nd ed., Springer Series in Operations Research and Financial Engineering, Springer, 2011. https://doi.org/10.1007/978-1-4614-0237-4
• J.L.W.V. Jensen, Sur les fonctions convexes et les inégalités entre les valeurs moyennes, Acta Mathematica 30 (1906), 175-193. https://doi.org/10.1007/BF02418571
• H.P. Edmundson, Bounds on the expectation of a convex function of a random variable, The RAND Corporation, Paper 982, 1956.
• A. Madansky, Bounds on the expectation of a convex function of a multivariate random variable, Annals of Mathematical Statistics 30 (1959), 743-746. https://doi.org/10.1214/aoms/1177706207
• A. Madansky, Inequalities for stochastic linear programming problems, Management Science 6 (1960), 197-204. https://doi.org/10.1287/mnsc.6.2.197
• H.I. Gassmann, W.T. Ziemba, A tight upper bound for the expectation of a convex function of a multivariate random variable, Mathematical Programming Study 27 (1986), 39-53. https://doi.org/10.1007/BFb0121114
• J.R. Birge, R.J-B. Wets, Designing approximation schemes for stochastic optimization problems, in particular for stochastic programs with recourse, Mathematical Programming Study 27 (1986), 54-102. https://doi.org/10.1007/BFb0121122

Motivation

Every stochastic program is, in practice, compared against a shortcut. A decision maker facing genuine uncertainty is tempted either to replace the random data by its mean and solve one deterministic problem, or to imagine that perfect information about the future were available and solve a separate deterministic problem per scenario. Both temptations have precise answers: the expected value of perfect information (EVPI) measures how much a decision maker should be willing to pay for a perfect forecast, and the value of the stochastic solution (VSS) measures the cost of ignoring uncertainty altogether by solving the mean-value problem. Both concepts originate in decision analysis — EVPI traces to Raiffa and Schlaifer (1961) — and were brought into stochastic programming by Madansky (1960), who proved the first chain of inequalities relating the wait-and-see value, the recourse value and the expected-value-solution's cost. Birge and Louveaux, Introduction to Stochastic Programming, 2nd ed. (Springer, 2011), Chapter 4, gives the standard modern treatment, including a refined family of bounds — built from pairs subproblems against a chosen reference scenario — that sharpen VSS beyond the original mean-scenario comparison. This mission formalizes that chapter's capstone: the five-quantity, four-inequality chain that pins VSS between two computable optimal values.

Setting

Fix a two-stage stochastic program with fixed recourse: a finite family of K scenarios $\xi_1,\dots,\xi_K$ in $\mathbb R^d$, each occurring with probability $p_k \ge 0$, $\sum_k p_k = 1$; a first-stage feasible set $K_1 \subseteq \mathbb R^{n_1}$; and, for every first-stage decision $x \in \mathbb R^{n_1}$ and every scenario $\xi \in \mathbb R^d$, a scenario cost $z(x,\xi)$ — the optimal value of $c^Tx + \min\{q^Ty \mid Wy = h(\xi) - Tx,\ y \ge 0\}$. By convention $z(x,\xi) = +\infty$ when $x$ has no feasible second-stage recourse under $\xi$, and $z(x,\xi) = -\infty$ when the second-stage program is unbounded below.

From $z$, five basic quantities are defined (Birge & Louveaux §4.1–§4.2):

• The recourse problem's value, $RP = \min_{x \in K_1} \mathbb E_\xi\, z(x,\xi)$ — the best a decision maker can do without foreknowledge of $\xi$ (the "here-and-now" solution).
• The wait-and-see value, $WS = \mathbb E_\xi\big[\min_{x \in K_1} z(x,\xi)\big]$ — the average cost if $\xi$ were revealed before choosing $x$.
• The expected value of perfect information, $EVPI = RP - WS$.
• The expected value problem's solution $\bar x(\bar\xi)$, optimal for the deterministic problem at the mean scenario $\bar\xi = \mathbb E(\xi)$; its recourse cost, the expected result of using the EV solution, is $EEV = \mathbb E_\xi\, z(\bar x(\bar\xi), \xi)$.
• The value of the stochastic solution, $VSS = EEV - RP$ — the extra cost of implementing the mean-scenario decision instead of solving the recourse problem.

Section 4.6 refines VSS by replacing the mean scenario with an arbitrary reference scenario $\xi^r$ (not necessarily one of the $K$ possible scenarios, e.g. a worst case), with assumed probability $p_r = P(\xi=\xi^r)$:

• $\bar x^r$, optimal for $\min_{x\in K_1} z(x,\xi^r)$, gives the expected value of the reference-scenario solution, $EVRS = \mathbb E_\xi\, z(\bar x^r,\xi)$, and the generalized $VSS = EVRS - RP$.
• For each scenario $\xi^k$, the pairs subproblem of $\xi^r$ and $\xi^k$ treats them as a two-point distribution with weights $p_r$ and $1-p_r$: its optimal value is $\min_{x\in K_1}\big[p_r\,z(x,\xi^r) + (1-p_r)\,z(x,\xi^k)\big]$, attained at some $\bar x^k$. Averaging these optimal values over $k$ (rescaled by $1/(1-p_r)$) gives the sum of pairs expected values, $SPEV$. Taking, instead, the smallest full expected cost $\mathbb E_\xi\,z(\bar x^k,\xi)$ among the $K{+}1$ candidate solutions $\{\bar x^1,\dots,\bar x^K,\bar x^r\}$ gives the expectation of pairs expected value, $EPEV$.

Formalization targets

Goal — Chapter 4, Theorem 9 (p. 174)

Four links, each with independent content: nonnegativity of the leftmost gap, then two genuine inequalities (from the pairs-subproblem comparisons of Propositions 7 and 8), then the identity $VSS = EVRS - RP$ folded against $RP \ge WS$'s reverse-direction cousin. This is the weakest statement that keeps all five quantities distinct — stating only the outer bound $0 \le VSS \le EVRS-WS$ would erase exactly the refinement (via pairs subproblems) that makes the chapter's method useful.

Supporting propositions (milestones, in attack order)

• Proposition 1 (p. 166): $WS \le RP \le EEV$.
• Proposition 5(a) (pp. 167–168): $0 \le EVPI$ and $0 \le VSS$ (mean-scenario form), for any stochastic program.
• Proposition 7 (p. 173): $WS \le SPEV \le RP$.
• Proposition 8 (p. 174): $RP \le EPEV \le EVRS$.

Significance

The chain gives a decision maker two computable, non-obvious bounds on VSS — a quantity that is otherwise expensive to pin down exactly, since $RP$ itself already requires solving the full recourse problem. $EVRS - EPEV$ and $EVRS - SPEV$ are both computable from $K+1$ (or $K$) two-scenario LPs, far cheaper than the full $K$-scenario recourse problem, so Theorem 9 turns an expensive exact quantity into a pair of cheap certified bounds. Formalizing it fixes, once and for all, the exact hypotheses and quantifier structure of Madansky's original inequality (Proposition 1) together with the later pairs-subproblem refinement (Propositions 6–8, Birge 1982), often cited informally as "the VSS bounds" without distinguishing $EEV$, $EVRS$, $EPEV$ and $SPEV$. No part of this chain is on Mathlib or Formalpedia today (checked by concept query, not title); this is a first, from-scratch treatment of two-stage recourse value-of-information theory as formal objects.

Difficulty

The obvious first idea — collapse $RP$, $WS$, $EV$, $EEV$, $EVRS$, $EPEV$, $SPEV$ to one "the optimal value of the LP" and prove a single inequality — throws away the entire content of the chapter. Each quantity restricts the minimization to a different feasible object: $RP$ minimizes jointly over $x$; $WS$ swaps the order of $\min$ and $\mathbb E$; $EEV$/$EVRS$ evaluate one fixed $x$ under every scenario; $SPEV$ and $EPEV$ each minimize over a family of pairs subproblems rather than the full $K$-scenario problem. The chain's proof (Propositions 7–8) depends on this precisely: Proposition 7's lower bound uses that each pairs-subproblem-optimal $(\bar x^k,\bar y^k)$ is feasible (not necessarily optimal) for the single-scenario problem at $\xi^r$, and its upper bound uses that the recourse-optimal $(x^*, y^*(\xi^r), y^*(\xi^k))$ is feasible (not necessarily optimal) for the pairs subproblem — a feasible-but-not-optimal argument in each direction, not a direct comparison of objective values. Losing track of which solution is fixed and which is optimized destroys the argument entirely.

Formalization scope

An Instance bundles the finite scenario set (Fin K, probabilities p : Fin K → ℝ with p ≥ 0, ∑ p = 1, scenarios xi : Fin K → (Fin d → ℝ)), the first-stage feasible set K1 : Set (Fin n1 → ℝ), and the scenario cost z : (Fin n1 → ℝ) → (Fin d → ℝ) → EReal, using the extended reals to carry the book's own +∞/−∞ conventions for infeasibility and unboundedness rather than silently restricting to a finite-valued special case (a genuine risk of trivialization here, since Example 2 of the chapter exhibits $EEV = +\infty$). All optimal values (RP, WS, EV, EVPI, EEV, VSS, EVRS, generalized VSS, SPEV, EPEV) are defined directly from z, matching the book's own level of abstraction in this chapter (which never unfolds z into the underlying LP's $A,b,c,q,W,T,h$ data — those appear only in Chapter 3). Because EEV, the mean-scenario VSS, EVRS, the generalized VSS, and EPEV are each defined relative to an optimal solution of some sub-problem — the book itself only ever says "let $\bar x(\bar\xi)$ denote some optimal solution" — every theorem using them states that solution and its optimality as explicit hypotheses (x ∈ K1 and z x … = ⨅ …), never baking it into a Classical.choiced value; this keeps the quantifier structure faithful to the book's own "let ... be an optimal solution" phrasing. Proposition 5's part (b) — the upper bound $EVPI \le EEV-EV$, $VSS \le EEV-EV$ "for stochastic programs with fixed recourse matrix and fixed objective coefficients" — needs a different scope: that hypothesis is a structural property of the underlying LP data ($W$, $c$, $q$ fixed across scenarios) invisible once $z$ is abstracted away as above, and pinning it down would require modeling the LP's $A,b,c,q,W,T,h(\xi)$ data explicitly (as Chapter 3's mission does for its convexity theorem). That part is out of scope here and is not needed for Theorem 9's own chain, which rests only on Proposition 5(a).

Collapsing any two of $RP$, $WS$, $EV$, $EEV$, $EVRS$, $EPEV$, $SPEV$ to a single "value of the LP" — the trivialization this book-wide series flags for Chapter 4 — is ruled out by construction: each is its own definition over its own feasible object, and Theorem 9's statement names all five quantities in the chain rather than only its outer bound. The two occurrences of "VSS" in the chapter (the original mean-scenario $EEV-RP$ of §4.2, and the reference-scenario $EVRS-RP$ generalization of §4.6, used only in Theorem 9) are likewise kept as two distinct definitions rather than conflated under one name.

Every addition and subtraction between EReal values in this mission — inside expect, WS, EVPI, VSS, EVRS's appearance in VSSRef, the pair sum inside pairsValue, the sum inside SPEV, and all four differences in Theorem 9's own chain — uses three explicit operations, badd/bsub/bsum, that implement the book's own convention (p. 164) that +∞ (infeasibility) dominates, i.e. (+∞)+(−∞)=+∞, rather than Mathlib's native EReal addition, whose ⊤+⊥=⊥ would make VSS ≥ 0 (Proposition 5(a)) and the goal's own leftmost inequality false whenever a witness solution is infeasible in a positive-probability scenario — exactly the situation of the book's own Example 2 (pp. 174-175). The reference scenario's probability $p_r=\Pr(\xi=\xi^r)$ (p. 172) is likewise not a free parameter but a definition, refProb, computed from the instance itself as $\sum_{k:\,\xi^k=\xi^r}p_k$; SPEV's sum is correspondingly restricted to the scenarios other than the reference scenario ($\xi^k\ne\xi^r$), matching the book's own proof of Proposition 7, which uses $\sum_{k\ne r}p_k=1-p_r$. The single hypothesis refProb I xir < 1 on Propositions 7, 8 and the goal says that some other scenario remains possible, which the book's own $(1-p_r)^{-1}$ factor presupposes.

Reusable beyond this mission: the Instance definition and the RP/WS/EV quantities are the natural base for any later chapter of this series that needs the two-stage recourse value (e.g. Chapter 3's convexity mission, Chapter 5's L-shaped method); contributions extending this Instance to the full LP data of the underlying two-stage program, or adding Proposition 5(b) and Proposition 2's Jensen-inequality argument on top of it, are welcome.

Selected references

• J.R. Birge and F. Louveaux, Introduction to Stochastic Programming, 2nd ed., Springer Series in Operations Research and Financial Engineering, 2011, Chapter 4. DOI: 10.1007/978-1-4614-0237-4
• A. Madansky, "Inequalities for Stochastic Linear Programming Problems", Management Science 6(2), 1960, 197–204.
• H. Raiffa and R. Schlaifer, Applied Statistical Decision Theory, Harvard Business School, 1961.
• J.R. Birge, "The Value of the Stochastic Solution in Stochastic Linear Programs with Fixed Recourse", Mathematical Programming 24(1), 1982, 314–325.

Motivation

When exact dynamic programming is intractable, practice runs on approximations: one-step and multistep lookahead with a cost-to-go surrogate, open-loop feedback control, and rollout — the algorithm that improved backgammon programs and became a conceptual ancestor of Monte-Carlo tree search and modern policy improvement schemes. Chapter 6 of Bertsekas, Dynamic Programming and Optimal Control, Vol. I (3rd ed., 2005) gives the basic guarantees: performance bounds for limited lookahead (Props. 6.3.1–6.3.2), superiority of open-loop feedback control over open-loop control (Prop. 6.2.1), and the cost-improvement theory of rollout on discrete deterministic problems (Props. 6.4.1–6.4.3). These are the theorems that make "approximate DP" more than a heuristic.

Setting

Two frameworks. For the stochastic bounds (§6.2–6.3): the basic finite-horizon model of Mission I of this series (BertsekasDPModel), its policy cost recursion, and the open-loop cost of a fixed control sequence (BertsekasDPOpenLoopCost). For rollout (§6.4.1): a graph search problem — a finite digraph with destination set and terminal costs $g(i)$ on destinations (BertsekasGraphSearch); a base heuristic $\mathcal{H}$ producing from every node a path to a destination (BertsekasBaseHeuristic), with projection $p(i)$ and heuristic cost $H(i) = g(p(i))$; the rollout algorithm $R\mathcal{H}$ repeatedly moves to a neighbor $j$ minimizing $H(j)$ (BertsekasIsRolloutRun). $\mathcal{H}$ is sequentially consistent if its paths have the tail property (Def. 6.4.1), sequentially improving if $\min_{j \in N(i)} H(j) \le H(i)$ (Def. 6.4.2).

Target

For sequentially improving $\mathcal{H}$ and any terminating rollout run $(i_1, \dots, i_{\bar m})$:

— BertsekasDP.rollout_sequential_improvement (goal, Prop. 6.4.2). Milestones: Props. 6.4.1 (termination under sequential consistency with the book's tie-breaking), 6.4.3 (exact cost identity via the defects $\delta_i$), 6.3.1, 6.3.2 (lookahead bounds), 6.2.1 (OLFC).

Significance

Prop. 6.4.2 is the "rollout never hurts" theorem — the formal warrant for policy improvement by simulation, with Prop. 6.3.1 its stochastic counterpart (via Example 6.3.1 the rollout of any policy improves that policy). Prop. 6.3.2 is the robustness version that quantifies the cost of inexact minimization, used for CEC bounds. Formalizing the chapter yields a reusable graph-search + base-heuristic vocabulary and connects it to the Mission I stochastic model. Everything here is proved in the book; the formal versions are new.

Difficulty

The rollout proofs are elementary but exact: the min formula (6.37) requires tracking the running minimum along the run, and the IsLeast membership half forces identifying which neighbor value is attained. Termination under sequential consistency (6.4.1) is the delicate one — it fails without the tie-breaking convention (the book gives a cycling counterexample), so the formal statement carries the convention explicitly and the proof must extract a termination measure from "strict decreases are finitely many, plateaus shorten the heuristic path". The stochastic bounds are clean backward inductions over the Mission I recursion.

Formalization scope

Graph search: finite node type, arcs as ordered pairs, vertex costs only (no arc costs — the book's reduction absorbs them into destination costs); heuristic paths as lists; rollout runs as lists (finite, complete runs) except 6.4.1, where the run is an infinite sequence absorbed at destinations so that termination is a genuine claim. Ties in neighbor selection are allowed everywhere except where 6.4.1's convention pins them. Stochastic side: state-independent constraint sets for OLFC (as in §6.2); restricted lookahead sets $\bar U_k(x) \subseteq U_k(x)$ per Eq. (6.19); all statements at the level of the Mission I model.

Selected references

• D. P. Bertsekas, Dynamic Programming and Optimal Control, Vol. I, 3rd ed., Athena Scientific, 2005. (§6.2–6.4.) http://www.athenasc.com/dpbook.html
• G. Tesauro, G. R. Galperin, On-line policy improvement using Monte-Carlo search, NIPS 1996. https://papers.nips.cc/paper/1302
• D. P. Bertsekas, J. N. Tsitsiklis, C. Wu, Rollout algorithms for combinatorial optimization, J. Heuristics 3 (1997), 245–262. https://doi.org/10.1023/A:1009635226865

Motivation

In 1956 Kelly answered a question that looks like gambling and is really about information: if a channel gives you a noisy advance signal about a sequence of bets, how much is that signal worth? His answer was that the maximum exponential rate of growth of a gambler's capital equals the rate of transmission over the channel -- so information rate and capital growth rate are the same quantity in different units. The betting fraction that achieves it is now called the Kelly criterion, and it is the basis of a large practical literature on position sizing.

The result is short, entirely explicit, and has no analytic subtleties -- which makes it a good formalization target and a surprising gap: the platform currently has fifteen missions on bandit algorithms and none on optimal growth.

Setting

This mission formalizes the simplest case of Kelly's Section 4: an even-money bet with no track take, won independently with probability p and lost with probability q = 1 - p. A gambler stakes a fixed fraction l of current wealth on each bet, so wealth is multiplied by 1 + l on a win and 1 - l on a loss. The exponential rate of growth is

Kelly shows this is maximised at l = p - q, with maximum value 1 + p log p + q log q in bits. We state G in nats (natural logarithm), so the maximum carries an additive log 2; dividing by log 2 recovers Kelly's bit-valued form, which is exactly 1 - H(p) for the binary entropy H. The maximiser is unaffected by the choice of base.

What is being asked

The goal theorem is that l = 2p - 1 maximises G over the admissible range (-1, 1) when the bet is favourable (p > 1/2). Milestones supply the maximum value (Kelly's information-rate identity), the admissibility of the maximiser, and the concavity that makes the first-order condition sufficient.

Source

J. L. Kelly Jr., A New Interpretation of Information Rate, Bell System Technical Journal 35 (1956) 917-926, Section 4 ("the simplest case"). The growth-rate expression and the maximiser l = p - q are stated there; the maximum value in bits is Kelly's eq. for G_max.

The identity and maximiser were checked numerically before drafting: for p = 0.55, 0.6, 0.7, 0.9 the claimed maximum matches log 2 + p log p + q log q to six decimals, and a grid search over (-1, 1) at 1e-5 resolution returns 2p - 1 in every case.

Motivation

Dynamic programming is the backbone of stochastic optimal control, operations research, and reinforcement learning. Its cornerstone — that the backward recursion of Bellman computes the optimal cost of a finite-horizon stochastic control problem — is stated as Proposition 1.3.1 of Bertsekas, Dynamic Programming and Optimal Control, Vol. I (3rd ed., Athena Scientific, 2005), the standard graduate text on the subject. Every convergence result for value iteration, every performance bound for approximate DP, and every correctness proof for a planning algorithm ultimately leans on this proposition. A machine-checked version of it — over a clean, reusable model of the basic problem — is the natural foundation stone for formalized control theory and RL theory alike.

Setting

The basic problem (§1.2 of the book): a discrete-time system

with state $x_k \in S$, control $u_k$ constrained to a finite nonempty set $U_k(x_k) \subseteq C$, and disturbance $w_k$ drawn from a finite space $W$ with conditional probabilities $p_k(w \mid x_k, u_k)$. A policy is a sequence $\pi = \{\mu_0, \mu_1, \dots\}$ of feedback maps $\mu_k : S \to C$; it is admissible if $\mu_k(x) \in U_k(x)$ everywhere. Its expected cost from $x_0$ is

In the Lean development these are BertsekasDPModel, BertsekasDPPolicyCost (backward recursion on remaining stages), and the DP recursion BertsekasDPValue:

Section 1.6 of the book develops the minimax variant, where the disturbance is chosen antagonistically from a finite membership set $W_k(x,u)$; the mission mirrors it with BertsekasMinimaxDPModel, BertsekasMinimaxPolicyCost, BertsekasMinimaxValue.

Target

formalized as BertsekasDP.dp_algorithm_optimality: the DP value at the horizon is an IsLeast of the set of admissible policy costs. Milestones: the min–max interchange Lemma 1.6.1 (minimax_selection_interchange) and the minimax DP validity (minimax_dp_algorithm).

Significance

The proposition itself is the license to compute optimal policies stage by stage; downstream, Missions VI and VII of this series (lookahead bounds, infinite-horizon theory) consume exactly this model and recursion. Formalizing it produces the reusable model of the basic problem — the shared vocabulary for the whole series. The result is classical and proved in the book; the contribution here is a machine-checked proof over a model faithful to the book's, with the measurable-selection subtleties deliberately avoided by finiteness (see scope).

Difficulty

The proof is a backward induction, but the standard informal argument ("interchange expectation and minimization") must be carried out honestly: the induction hypothesis is about all states simultaneously, the minimizing control must be selected as a function of the state (choice over a finite set), and the policy-cost recursion must be related to the value recursion stage by stage. The minimax milestone needs the interchange lemma with its $> -\infty$ proviso — the classic trap is losing that hypothesis and asserting a false unconditioned interchange.

Formalization scope

Finite disturbance space (Fintype W), finite nonempty control-constraint sets (Finset, inf'), arbitrary (possibly infinite) state space; expectations are finite weighted sums, probabilities are required to be distributions only at admissible controls. Stage data are total functions on $\mathbb{N}$; only stages $0,\dots,N-1$ matter. Policies are deterministic Markov feedback maps — for this class the book's result is exactly recovered. The trivializing risks (empty constraint sets, junk beyond horizon) are ruled out by the nonemptiness field and by evaluating at exactly $N$ remaining stages. Lemma 1.6.1 is stated in the extended reals over arbitrary types with the book's finiteness-of-infimum proviso.

Selected references

• D. P. Bertsekas, Dynamic Programming and Optimal Control, Vol. I, 3rd ed., Athena Scientific, 2005. ISBN 1-886529-26-4. (Prop. 1.3.1, §1.2–1.3, §1.6.) http://www.athenasc.com/dpbook.html
• R. Bellman, Dynamic Programming, Princeton University Press, 1957.

Motivation

The conjugate-gradient method in Luenberger's Chapter 10 is one of the most enduring consequences of Hilbert-space geometry in numerical optimization. For a bounded self-adjoint coercive operator, it solves the quadratic first-order equation Q x = b using only operator applications, inner products, and a short recurrence. Luenberger develops the method from steepest descent and conjugate directions, then proves convergence in a general real Hilbert space rather than only for finite matrices. This mission formalizes that full setting. It also repairs a practical omission in the printed recursion: division formulas are undefined after exact convergence, so the formal algorithm explicitly stops and stutters once its search direction is zero.

Setting

Let H be a complete real inner-product space and Q : H →L[ℝ] H a bounded self-adjoint operator. Constants m and M satisfy 0 < m ≤ M and

for every x. The first inequality is coercivity; together with self-adjointness it supplies the positive Q-energy. For a right-hand side b and initial point x₀, the initial residual and direction are both b - Q x₀. A conjugate-gradient state records the current iterate, residual, and direction. If the direction is nonzero, the next state uses Luenberger's alpha and beta ratios. If the direction is zero, conjugateGradientStep returns the same state, so every natural-number iterate is total and all denominators occur only on the active branch.

Formalization targets

The root theorem VectorSpaceOpt.conjugate_gradient_converges states that there is a unique xStar satisfying Q xStar = b and that the iterate component of the guarded conjugate-gradient state tends to xStar in norm. Four milestones provide reusable structure. coercive_selfadjoint_bijective establishes existence and uniqueness for Q x = b from bounded self-adjoint coercivity. conjugate_directions_converge formalizes §10.6, Theorem 1: a complete sequence of nonzero pairwise Q-orthogonal directions produces residuals orthogonal to every earlier direction and iterates converging to the solution. cg_directions_conjugate_until_stop records the §10.8 invariants only before the explicit stopping time. cg_energy_contraction captures the uniform energy reduction factor derived from the bounds m and M.

The total algorithm is represented by conjugateGradientIterate, and its error functional is

These definitions are proposed as mission-owned reusable objects in the shared VectorSpaceOpt namespace.

Significance

The mission gives a coordinate-free verification target for an algorithm usually presented through arrays and matrices. Its theorem applies directly to finite-dimensional symmetric positive-definite systems but also retains Luenberger's infinite-dimensional perspective. The guarded recursion is suitable for later executable specializations and makes exact termination a first-class semantic event. The coercivity and conjugate-directions milestones can be reused for Galerkin methods, preconditioned variants, and other Krylov algorithms, while the energy estimate provides a natural connection to condition-number convergence rates.

Unlike a matrix-only formalization, the Hilbert-space theorem cleanly separates the geometric reason for convergence from any storage representation. It therefore complements Mathlib's existing operator and orthogonality libraries and can serve as a specification against which finite implementations are later verified. It also preserves the book's unifying theme: optimization algorithms arise from the geometry of carefully chosen inner products rather than from coordinate manipulation alone.

Difficulty

The difficulty is medium to high. Algebraic invariants of the three-term recurrence involve several interacting orthogonality relations and require strict control of nonzero denominators. Infinite-dimensional convergence additionally uses density of the closed span of directions and comparison of the Q-energy with the ambient norm. The theorem must move between self-adjoint continuous linear maps, scalar inner products, filters on sequences, and function iteration. Exact termination creates a case split that informal accounts routinely ignore; the formal statement must show that the zero-direction branch is stable and already represents the solution.

Formalization scope

The proposal follows §10.6 and §10.8, pp. 291–296, and uses Chapter 10, Problem 10 on p. 309 for the coercive-invertibility dependency. All assumptions on Q, m, and M that §10.8 inherits from the preceding sections are repeated explicitly. The conjugate-directions milestone explicitly assumes every direction is nonzero and that the closed span of the directions is the whole Hilbert space. The conjugate-gradient invariants are asserted only for iterations before a zero direction occurs. Once it occurs, the state stutters by definition; the proposal never relies on Lean's totalized value for 0 / 0.

Luenberger's §10.7, Theorem 1 is not included as a literal milestone. As printed, its orthogonalization-of-moments statement omits self-adjointness of the auxiliary operator relative to the Q inner product and omits the linear-independence/nonbreakdown conditions needed to keep denominators nonzero. The mission instead isolates the Q-conjugacy invariant directly from §10.8. It does not claim finite-dimensional termination within dim H steps, floating-point stability, preconditioning, a sharp Chebyshev condition-number rate, or computability of equality tests on arbitrary Hilbert spaces.

Selected references

• David G. Luenberger, Optimization by Vector Space Methods, Wiley, 1969, Chapter 10, §10.6, Theorem 1, pp. 291–292; §10.8, Theorem 1, pp. 294–296; Problem 10, p. 309. Scan: https://sites.science.oregonstate.edu/~show/old/142_Luenberger.pdf
• Lean community, Mathlib documentation, continuously updated: https://leanprover-community.github.io/mathlib4_docs/ (real inner-product spaces, continuous linear maps, coercivity, closed spans, orthogonality, and filter convergence).

Motivation

Quadratic exterior penalties in Luenberger's §10.11 replace a constrained problem by a sequence of unconstrained minimizations. The method is simple enough to state in a few lines, yet Luenberger's convergence theorem is strikingly general: no convexity, differentiability, or convergence of the full minimizer sequence is required. If penalty weights increase to infinity and a subsequence of exact penalty minimizers converges, lower semicontinuity alone makes its limit feasible and optimal. This mission isolates that robust primal convergence result as a tractable companion to the more analytic conjugate-gradient and optimal-control missions. It offers a clean formalization target with direct relevance to nonlinear programming and approximation schemes.

Setting

Let X be a topological space, f : X → ℝ, and G : X → (Fin p → ℝ). Feasibility means G x i ≤ 0 for every component. Define the positive part componentwise and the squared violation by

For a positive weight K, the penalty objective is f x + K * v x. A sequence K n is positive, nondecreasing, and tends to +∞. The constrained problem is assumed to have a minimizer xStar, and for each n an exact global minimizer x n of the corresponding penalty objective is supplied. A limit point is represented explicitly by a strictly increasing index map phi for which x ∘ phi tends to x₀.

Formalization targets

The root VectorSpaceOpt.quadratic_penalty_cluster_point_converges formalizes §10.11, Theorem 1. Assuming lower semicontinuity of f and v, it concludes that every stated subsequential limit x₀ is feasible, has the same objective value as xStar, and globally minimizes f over the feasible set.

Three milestones split the exact source content into reusable statements. quadratic_penalty_basic_estimates is §10.11, Lemma 1: the attained penalty values are nondecreasing, are bounded above by f xStar, and the stronger weighted violation K n * v (x n) tends to zero. penalty_cluster_point_feasible combines convergence of violations with lower semicontinuity at a subsequential limit to recover all component inequalities. penalty_cluster_point_optimal combines lower semicontinuity of f, the uniform upper bound f (x n) ≤ f xStar, feasibility of the limit, and optimality of xStar to identify the limiting objective value and global constrained optimality.

Significance

The theorem captures the essential consistency guarantee behind one of the most widely used constraint-handling methods. Its assumptions separate optimization existence from convergence: minimizers of each auxiliary problem and at least one cluster point are assumed, while the theorem identifies what any such cluster point must be. The componentwise positive-part and violation definitions are reusable for augmented Lagrangians, exact penalties, barrier comparisons, and finite inequality systems. The basic-estimates lemma is particularly useful because it requires neither topology nor continuity and exposes a quantitative fact stronger than mere feasibility residual convergence.

Because the proof target is stated over an arbitrary topological space, the mission also clarifies which parts of penalty convergence are genuinely metric and which depend only on order, finite nonnegative sums, and lower semicontinuity. This abstraction is faithful to the source's vector-space viewpoint.

Difficulty

The mission has moderate difficulty and relatively low infrastructure risk. The main analytic interfaces are lower semicontinuity along a convergent subsequence and real filter convergence to both zero and infinity. The basic estimates require reasoning simultaneously about minimizers for changing objectives, monotonicity of the weights, and the asymptotic product K n * v (x n). The cluster-point theorem must extract componentwise feasibility from a finite sum of nonnegative squares without assuming continuity of G. Lean's IsMinOn does not itself assert membership in the feasible set, so feasibility of the known constrained minimizer is included separately rather than hidden in prose.

Formalization scope

The proposal covers the primal part of §10.11: Lemma 1 on p. 305 and Theorem 1 on p. 306. It makes “limit point” precise through a strictly monotone subsequence, avoiding any assumption that the full sequence converges. The weight sequence may have repeated values because the source only needs it to be nondecreasing, but every weight is positive and the sequence tends to atTop. Lower semicontinuity is required for f and the composite violation v, exactly as in the book; continuity or componentwise lower semicontinuity of G is not substituted. Existence of xStar and of every penalty minimizer is assumed rather than derived from compactness or coercivity.

The mission does not include §10.11, Lemma 2 or Theorem 2 on dual multipliers. Those results add convexity and continuity assumptions and naturally require careful treatment of an extended-real dual functional. It also does not address approximate minimizers, rates, boundedness of the sequence, existence of cluster points, equality constraints beyond their encoding as paired inequalities, or finite exactness. Keeping those extensions separate preserves the unusually weak hypotheses and clear conclusion of the cited primal theorem.

Selected references

• David G. Luenberger, Optimization by Vector Space Methods, Wiley, 1969, Chapter 10, §10.11, Lemma 1 and Theorem 1, pp. 305–306. Scan: https://sites.science.oregonstate.edu/~show/old/142_Luenberger.pdf
• Lean community, Mathlib documentation, continuously updated: https://leanprover-community.github.io/mathlib4_docs/ (lower semicontinuity, finite sums, Fin-indexed vectors, subsequences, global minima on sets, and filter convergence).

Motivation

Luenberger's generalized Kuhn–Tucker theorem turns inequality-constrained optimization into an order-theoretic statement on normed vector spaces. Instead of listing scalar inequalities, it lets a convex cone P define positivity in a target space Z; one condition G x ≤ₚ 0 can therefore represent finite, infinite, or function-valued families of constraints. At a regular local minimizer, a positive continuous functional on Z simultaneously provides stationarity and complementary slackness. This mission is a separate capstone because the cone-separation argument is conceptually independent of the equality-constrained theorem and because Mathlib currently lacks this general cone-valued KKT result.

Setting

Let X and Z be real normed spaces, P : ConvexCone ℝ Z, f : X → ℝ, and G : X → Z. The cone order is coneLE P z₁ z₂, meaning z₂ - z₁ ∈ P; strict inequality uses the topological interior of the convex cone P. The cone is assumed to have nonempty interior. At x₀, both f and G possess linear Gâteaux derivatives represented by continuous linear maps f' and G'. The source's regularity condition requires feasibility together with a direction h for which G x₀ + G' h lies strictly below zero in the cone order.

The point x₀ is a local, not global, minimizer of f on {x | coneLE P (G x) 0}. The resulting multiplier z₀ : Z →L[ℝ] ℝ is positive on P. This mission reuses the previously published VectorSpaceOpt.coneLE and VectorSpaceOpt.dualPositive definitions from the global Lagrange-duality mission; it deliberately does not introduce equivalent duplicate constants.

Formalization targets

The root theorem is VectorSpaceOpt.generalized_kuhn_tucker, corresponding to §9.4, Theorem 1. It produces z₀ such that

Three milestones expose the exact logical interfaces of the source theorem. kkt_no_strict_linearized_descent says local minimality and feasibility exclude a direction that strictly decreases f' while making the linearized constraint strictly feasible. kkt_linearized_separator packages the separation step: nonintersection of the strict descent system, cone regularity, and nonempty cone interior yield a positive continuous multiplier with both KKT conclusions. kkt_complementary_slackness isolates the algebraic extraction of stationarity and complementarity from the separating inequality valid for every direction. The items use the shared namespace VectorSpaceOpt and list dependencies in this order.

Significance

This mission generalizes the standard finite-dimensional KKT rule without choosing coordinates or reducing cone constraints to components. It provides a reusable basis for semi-infinite optimization, ordered Banach-space problems, and state constraints expressed in function spaces. The multiplier positivity predicate connects directly to the dual cone used in the earlier global duality mission, while complementarity links local differential theory to primal–dual optimality. A successful formalization would also close a conspicuous gap in general-purpose optimization infrastructure: cone-valued KKT conditions are referenced often but rarely available as a theorem with all topological hypotheses exposed.

The statement is also a useful stress test for compositional textbook formalization. It deliberately shares its order and dual-positivity vocabulary with an earlier mission, so subsequent results can consume one stable API instead of translating among locally invented conventions.

Difficulty

The main challenge is functional-analytic separation. The relevant convex set mixes objective descent and strict cone feasibility, and the separating functional must be normalized so that its objective component is nonzero. Regularity rules out an abnormal separator and nonempty cone interior controls the sign of the Z component. The Gâteaux assumptions are directional rather than full Fréchet differentiability, so local contradiction statements must use only the one-dimensional expansions actually supplied. Lean also requires careful sign discipline: feasibility is encoded as 0 - G x ∈ P, while positivity is evaluated on elements of P. Small convention errors would reverse the dual cone or the stationarity equation.

Formalization scope

The source says that X is a vector space, but its definition of Gâteaux differentiation and its local perturbation argument require a norm and topology. The proposal therefore makes both X and Z normed real spaces and represents derivatives by continuous linear maps. It keeps Luenberger's cone assumptions: convexity and nonempty interior are explicit; pointedness and closedness are not added because the printed separation argument does not need them. The optimality hypothesis is faithfully local through IsLocalMinOn. Feasibility is included in IsConeRegularAt, and the no-descent milestone states it separately.

This is proposed as “Vector Space Methods XI” and depends on the earlier global Lagrange-duality mission, proposed as “Vector Space Methods IX,” for coneLE and dualPositive; the missions should be submitted in numerical order. The proposal does not cover equality constraints, second-order KKT conditions, multiplier uniqueness, constraint qualifications other than Luenberger's strict linearized feasibility condition, or sufficient conditions based on convexity. It also does not specialize to a finite list of scalar inequalities. These omissions preserve the exact role and scale of §9.4.

Selected references

• David G. Luenberger, Optimization by Vector Space Methods, Wiley, 1969, Chapter 9, §9.4, regular-point definition and Theorem 1, pp. 248–250. Scan: https://sites.science.oregonstate.edu/~show/old/142_Luenberger.pdf
• Lean community, Mathlib documentation, continuously updated: https://leanprover-community.github.io/mathlib4_docs/ (convex cones, continuous linear functionals, topological interiors, differential calculus, local extrema, and geometric separation).

Motivation

Equality-constrained optimization is the point where the geometric language of vector spaces becomes an operational calculus. In finite dimensions, the familiar rule says that the gradient of an objective at a regular constrained optimum is a linear combination of the constraint gradients. Luenberger's Chapter 9 replaces coordinate gradients by continuous linear maps between Banach spaces and identifies the genuinely important hypothesis: the derivative of the constraint map is onto. The resulting theorem covers constraints with infinitely many degrees of freedom and prepares the functional-analytic form of optimal control. This mission formalizes the local theorem rather than a finite-dimensional specialization. It also records the generalized inverse theorem that makes regular level sets locally rich enough to test every tangent direction.

Setting

Let X and Z be real Banach spaces, U ⊆ X an open set, f : X → ℝ an objective, and H : X → Z an equality-constraint map. The distinguished point x₀ lies in U and satisfies H x₀ = 0. Both maps are continuously Fréchet differentiable on U; their derivatives at x₀ are named f' and H'. A regular point is one at which H' : X →L[ℝ] Z is surjective. Local optimality is expressed relative to the actual feasible set {x | x ∈ U ∧ H x = 0}, and may be either a local minimum or a local maximum. Multipliers live in the continuous dual Z →L[ℝ] ℝ, never in an untopologized algebraic dual.

The mission also treats a map T : X → Y between Banach spaces. Surjectivity of its derivative at x₀ yields local metric surjectivity: sufficiently nearby target points possess preimages in U, with displacement controlled linearly by their distance from T x₀. This is the Lyusternik–Graves form of the generalized inverse theorem, not the ordinary inverse theorem requiring a bijective derivative.

Formalization targets

The main target is VectorSpaceOpt.equality_lagrange_multiplier, the exact regular equality-multiplier theorem from §9.3. Its conclusion is the existence of a continuous linear functional z₀ satisfying

Three source-aligned milestones organize the mission. First, generalized_inverse_function formalizes §9.2, Theorem 1: an onto derivative gives constants ε > 0 and K ≥ 0 so every y with dist y (T x₀) < ε has a preimage x ∈ U obeying T x = y and ‖x - x₀‖ ≤ K ‖y - T x₀‖. Second, constrained_extremum_tangent_stationary states that f' h = 0 for every h in the kernel of H' at a regular local extremum. Third, abnormal_lagrange_multiplier records Luenberger's closed-range corollary: without surjectivity there is a nonzero pair (r₀,z₀) satisfying r₀ • f' + z₀ ∘ H' = 0.

Significance

This theorem is the Banach-space bridge between unconstrained differentiation and multiplier theory. It isolates the quotient-space geometry behind the multiplier rule and supplies an interface reusable in variational problems, PDE-constrained optimization, and smooth optimal control. The abnormal alternative matters independently: it represents the degeneracy that later appears in Fritz John conditions and endpoint-constrained control. Formalizing the quantitative generalized inverse statement also contributes infrastructure with uses beyond optimization, including nonlinear solvability, metric regularity, and perturbation estimates.

Difficulty

The mission is mathematically compact but technically demanding. The hard object is local surjectivity from an onto, noninjective derivative. Its natural linear model passes through the Banach quotient by the kernel and the open mapping theorem, while the nonlinear statement must preserve the open domain and a quantitative norm estimate. At the multiplier stage, a functional defined on the range of H' must be shown well-defined, bounded, and represented as a continuous functional on Z. Lean must also reconcile ContDiffOn, pointwise Fréchet derivatives, kernels and ranges of continuous linear maps, and filter-based local extrema. These are substantial analytic interfaces even though the final equation is short.

Formalization scope

The proposal follows printed pp. 240–244. All domain, completeness, differentiability, feasibility, and locality hypotheses that are inherited implicitly in the prose are explicit in the Lean statements. The primary theorem assumes surjectivity and therefore produces a normalized multiplier with coefficient one on the objective. The abnormal milestone assumes only that Set.range H' is closed and explicitly requires the pair (r₀,z₀) to be nonzero. No finite-dimensionality, choice of coordinates, second-order condition, constraint qualification weaker than surjectivity, or sufficiency theorem is claimed.

Boundary cases are intentional. The zero constraint space is allowed and reduces the conclusion to ordinary stationarity. A local maximum is covered alongside a local minimum because the tangent argument is symmetric. The generalized inverse target explicitly returns a preimage inside U; it does not silently rely on extending T outside its domain. The mission does not identify the feasible level set with a manifold or claim uniqueness of a multiplier. Those are natural later developments but are not statements in the cited pages.

Selected references

• David G. Luenberger, Optimization by Vector Space Methods, Wiley, 1969, Chapter 9, §9.2, Theorem 1, pp. 240–242; §9.3, Lemma 1, Theorem 1, and Corollary 1, pp. 242–244. Scan: https://sites.science.oregonstate.edu/~show/old/142_Luenberger.pdf
• Lean community, Mathlib documentation, continuously updated: https://leanprover-community.github.io/mathlib4_docs/ (Fréchet derivatives, local extrema, continuous linear maps, Banach quotients, and Lagrange multipliers).

Motivation

The calculus of variations replaces optimization over finitely many coordinates by optimization over paths. Its necessary conditions underlie geodesics, minimum-energy curves, classical mechanics, and many optimal-control models. Chapter 7 of David G. Luenberger's Optimization by Vector Space Methods presents this transition as an application of differentiation in normed vector spaces: a local extremum first forces every directional derivative to vanish, and the resulting integral identity forces a differential equation along the optimizing path. This mission formalizes the scalar, fixed-endpoint version in §§7.4–7.5. The target is intentionally the theorem actually isolated by the source, not a stronger modern Sobolev-space variant.

Setting

Fix real numbers $a<b$. A $C^1$ path on the segment is represented in Lean by two functions, $x,\dot x:\mathbb R\to\mathbb R$. Both are continuous on $[a,b]$, and $x$ has derivative $\dot x(t)$ at every $t\in(a,b)$. Ordinary two-sided derivatives are not demanded at $a$ or $b$; this makes the formal endpoint convention match the one-sided role of endpoints in a closed interval.

Let $L(y,v,t)$ be a scalar Lagrangian. Along a candidate path, write

The Lean statement records these partial derivatives with HasDerivAt and assumes that $L_x$ and $L_v$ are continuous on $[a,b]$. A fixed-endpoint variation is another $C^1$ pair $(h,\dot h)$ with $h(a)=h(b)=0$. The first variation already computed from the action is

The main theorem begins from the stationarity identity $\delta J(x;h)=0$ for every such variation. It does not claim that the complete passage from a local extremum in Luenberger's $C^1$ norm to this integral formula has already been bundled into the root statement.

Formalization targets

Main goal: Euler–Lagrange equation

From the computed first-variation identity, prove that

The conclusion is expressed as HasDerivAt Lv (Lx t) t, so it asserts both differentiability of $L_v$ and the equality of its derivative with $L_x$. This is equation (2) and the conclusion reached on printed pages 180–181.

Milestones

The first milestone formalizes §7.4, Theorem 1: a local minimum or maximum of a real functional has zero derivative along every direction whenever that scalar directional derivative exists. The remaining milestones are the three fixed-endpoint fundamental lemmas from §7.5. They respectively show that a continuous coefficient annihilating all variations is zero, that a continuous coefficient annihilating all variation derivatives is constant, and that an identity involving both $h$ and $\dot h$ forces the second coefficient to have derivative equal to the first. These are stated with the same $C^1$ variation class used by the goal.

Significance

The result turns an infinite family of scalar integral equalities into a pointwise differential equation. Once available, the same interface can support standard variational examples by supplying a concrete $L$, its two partial derivatives, and a stationary path. It also provides the analytic core needed before treating natural boundary conditions, vector-valued paths, higher derivatives, or weak Euler–Lagrange equations.

The formalization adds reusable interval-sensitive infrastructure. In particular, IsC1OnSegment separates a path from its chosen continuous derivative and avoids silently imposing derivatives outside the optimization interval. The three fundamental lemmas are useful independently of the named Euler–Lagrange theorem: they are test-function principles for interval integrals and can serve later missions involving integration by parts or weak formulations. The mathematics is classical and proved in the cited text; the open work is a machine-checked Lean development of these exact statements in the pinned Mathlib environment.

Difficulty

The source argument uses informal phrases such as “arbitrary $C^1$ function vanishing at the endpoints” and treats endpoint differentiation according to standard calculus convention. In Lean, those phrases must determine a precise domain, derivative witness, continuity requirement, and interval-integral orientation. Replacing $C^1$ variations by merely continuous functions would change Lemmas 2 and 3, while requiring HasDerivAt at the endpoints would add a hypothesis not present in the book.

Another tempting shortcut is to assume from the outset that $L_v$ is differentiable and then use integration by parts. That would trivialize the central regularity conclusion of Lemma 3: the book derives differentiability of $L_v$ from stationarity and continuity. The root therefore assumes only continuity of the two coefficient functions and concludes a HasDerivAt assertion on the open interval. Conversely, constructing the first variation from a local extremum of the action requires a separate differentiation-under-the-integral development and a topology on bundled $C^1$ paths; it is not hidden inside the main goal.

Formalization scope

The scalar field, path values, time variable, and action values are all real. The interval is nondegenerate through the explicit hypothesis $a<b$. Integrals use Mathlib's oriented interval integral, but all principal statements are made in the forward orientation. Paths and variations are total functions on $\mathbb R$ whose relevant regularity is restricted to $[a,b]$. The Lagrangian is finite-valued. No measurability or integrability premise is omitted: continuity of the coefficient and variation factors on the compact interval supplies the intended finite integrals.

The goal starts from an already computed first-variation identity. Contributions connecting a genuine local extremum of the action in the norm $\max|x|+\max|\dot x|$ to that identity are welcome as a strengthening, but they must not be advertised as part of the present root theorem. Other welcome contributions include reusable continuous test-function constructions and endpoint-aware interval integration lemmas. Sobolev paths, vector-valued state spaces, free endpoints, and weak derivatives are outside this mission and should be proposed separately rather than obtained by weakening the stated hypotheses until the result becomes vacuous.

Selected references

• David G. Luenberger, Optimization by Vector Space Methods, John Wiley & Sons, 1969, Chapter 7, §§7.4–7.5, pp. 178–181; definition of $D[a,b]$ on p. 23. Open Library record

Motivation

Linear equations between Hilbert spaces need not have unique solutions and may not even be exactly solvable for a given right-hand side. Least squares selects a vector with the smallest residual; when several such vectors exist, minimum norm selects one canonical representative. Luenberger packages this two-stage optimization into the pseudoinverse of a continuous linear operator with closed range. The construction unifies exact equations, approximation, normal equations, and orthogonal projections, while retaining a bounded linear operator suitable for subsequent optimization methods (Luenberger, §§6.9--6.11, pp. 159--165).

This mission continues the series into Chapter 6. Its capstone formalizes the structural identities of the pseudoinverse, including involution, compatibility with adjoints, reflexive inverse laws, self-adjoint projection products, and factorizations through the normal operators. Earlier milestones establish the adjoint facts and minimum-norm characterizations on which that operator calculus depends.

Setting

Let $G$ and $H$ be real Hilbert spaces, represented in Lean by complete real inner-product spaces, and let $A:G\toL[\mathbb R]H$ be a continuous linear map whose range is closed. The Hilbert adjoint is written $A^\dagger$ in the Lean statements and is Mathlib's adjoint continuous linear map. It is characterized by the inner-product relation and satisfies $\|A^\dagger\|=\|A\|$ (Luenberger, §6.5, Theorem 1, p. 151). Closed range gives the range-kernel identity

the Hilbert-space specialization of the closed range theorem used in the chapter (§6.6, Theorem 2, p. 156).

For $y\in H$, a vector $x\in G$ is a least-squares solution when $\|Ax-y\|$ is no larger than $\|Az-y\|$ for every $z$. A least-squares solution is minimum norm when its norm is no larger than that of every other least-squares solution. A continuous linear map $B:H\toL[\mathbb R]G$ satisfies VectorSpaceOpt.IsPseudoinverse A B when, for every $y$, $By$ has both properties. This predicate is the mission's one lightweight definition, directly encoding the definition in §6.11 (pp. 163--164).

Formalization targets

Adjoint and closed-range milestones

Formalize $\|A^\dagger\|=\|A\|$. Under closed range, formalize

These record §6.5, Theorem 1 and the Hilbert form of §6.6, Theorem 2.

Normal equations and minimum-norm solutions

Formalize the least-squares equivalence

as in §6.9, Theorem 1 (p. 160). For solvable $Ax=y$ and closed-range $A$, characterize the minimum-norm solution by $x=A^\dagger z$ with $AA^\dagger z=y$, following §6.10, Theorem 1 (pp. 161--162). Finally, formalize existence and uniqueness of a continuous linear $B$ satisfying IsPseudoinverse A B.

Pseudoinverse identities

Given such a $B$, formalize that $A$ is the pseudoinverse of $B$, that $B^\dagger$ is the pseudoinverse of $A^\dagger$, and that

Also produce pseudoinverses $C$ of $A^\dagger A$ and $D$ of $AA^\dagger$ satisfying

Together with the continuous-linear-map type of $B$, these clauses encode all nine items of §6.11, Proposition 1 (p. 165).

Significance

The pseudoinverse turns a possibly inconsistent or underdetermined equation into a canonical bounded linear solution operator. The normal equations connect residual minimization with the self-adjoint operator $A^\dagger A$; the minimum-norm theorem selects the component orthogonal to the kernel. The capstone identities show that the construction behaves like an inverse on the effective ranges and that $BA$ is self-adjoint, while the two factorizations reduce pseudoinverse questions to the normal operators.

The underlying results are proved in Luenberger's text. Their Lean formalization supplies a reusable predicate for minimum-norm least squares and an operator-level API linking adjoints, kernels, ranges, composition, and optimization characterizations. This bridges the earlier missions on minimum norm and estimation with later chapters that use normal operators and generalized inverses. It also records explicitly which conclusions require closed range, preventing accidental use of a bounded pseudoinverse where only an unbounded generalized inverse could exist.

Difficulty

Pointwise existence of a best residual is not enough. The selected minimum-norm solutions must collectively form a linear bounded map, and closed range is the hypothesis that makes this global operator well behaved. Without closed range, least-squares minimizers may fail to exist and the inverse on the effective range need not be bounded. A formulation that chooses an arbitrary minimizer for each target would therefore miss the main analytic content.

Several notationally similar operations must also remain distinct. The book writes a star for the adjoint and a superscript dagger-like symbol for the pseudoinverse; Mathlib's displayed dagger denotes the Hilbert adjoint. The mission consequently names the generalized inverse through IsPseudoinverse instead of overloading dagger notation. Orthogonal complements apply to submodules, compositions must retain their source and target spaces, and each factorization involves a different normal operator. These typing constraints expose domain/codomain mistakes that paper notation suppresses.

Formalization scope

The mission uses real Hilbert spaces only: NormedAddCommGroup, InnerProductSpace ℝ, and CompleteSpace. Operators are ContinuousLinearMap, composition is ∘L, the Hilbert adjoint is Mathlib's †, and the closed-range assumption is IsClosed (A.range : Set H). The orthogonal complement in the range theorem is the submodule A.kerᗮ.

IsPseudoinverse A B requires two pointwise inequalities for every target: B y minimizes residual norm among all inputs, then minimizes norm among all residual minimizers. The second clause cannot be dropped or weakened to exact solutions, because it is what makes the choice canonical for inconsistent as well as underdetermined systems. The minimum-norm-solution milestone states y ∈ A.range explicitly; the source treats solvability as part of speaking about a solution. The capstone accepts a continuous linear $B$ satisfying the predicate, so linearity and boundedness are represented by its type, corresponding to the first two items of Proposition 1. Contributions may add reusable lemmas about adjoints, orthogonal complements, closed range, normal equations, or uniqueness of optimizers, but must preserve the closed-range and completeness assumptions in the public operator theorems.

Selected references

• David G. Luenberger, Optimization by Vector Space Methods, John Wiley & Sons, 1969, Chapter 6, especially §§6.5--6.11, pp. 151--165. Public scan.

Motivation

Best approximation asks how closely a point can be represented by a prescribed linear model. In a Hilbert space, orthogonality turns this into a geometric projection problem. A general normed space has no inner product and may have no nearest point, so the corresponding certificate must live in the continuous dual rather than in the original space. Chapter 5 of Luenberger's Optimization by Vector Space Methods develops exactly this passage from geometry to duality: the Hahn--Banach theorem supplies continuous linear functionals that detect norms, separate points from closed subspaces, and certify an infimum distance even when that distance is not attained (Luenberger, §§5.4--5.8, pp. 111--120).

This mission continues the book's vector-space formalization series at the point where minimum-norm arguments cease to be specifically Hilbertian. Its capstone identifies the distance from a point to a linear subspace with the largest value at that point among all norm-at-most-one continuous linear functionals annihilating the subspace. The statement is a prototype for dual certificates throughout approximation theory and convex optimization.

Setting

Let $X$ be a real normed space and let $M$ be a linear subspace. In Lean, $M$ is represented by Submodule ℝ X; no topological closure assumption is imposed on the capstone. A continuous linear functional is an element $f : X \toL[\mathbb R] \mathbb R$, with operator norm $\|f\|$. It annihilates $M$ when $f(m)=0$ for every $m\in M$. The set of all such functionals is the annihilator $M^\perp$ in the book's terminology.

For $x\in X$, the infimum distance to $M$ is

The Lean target uses Metric.infDist x (M : Set X). Since every submodule contains zero, the underlying set is nonempty and this extended geometric notion is an ordinary nonnegative real number here. A functional $f$ is aligned with a vector $v$ when $f(v)=\|f\|\,\|v\|$. Alignment is the normed-space replacement for the familiar inner-product equality associated with a projection direction.

Two auxiliary dual notions are also formalized. A norm-preserving Hahn--Banach extension takes a functional on a subspace and extends it to all of $X$ without changing its norm. A norming functional for $x$ is a nonzero functional aligned with $x$. Finally, for closed $M$, the preannihilator of its annihilator is exactly $M$: the functionals vanishing on $M$ distinguish every point outside it (Luenberger, §§5.4 and 5.7, pp. 112--118).

Formalization targets

Norm-preserving extension and norming functionals

For a continuous functional $f$ on $M$, formalize an extension $F$ satisfying

For nontrivial $X$ and every $x\in X$, formalize the existence of a nonzero $f$ with $f(x)=\|f\|\,\|x\|$. These are Corollaries 1 and 2 of §5.4 (pp. 112--113).

Closed-subspace double annihilator

For closed $M$, formalize

This is the concrete set-valued form of Theorem 1 in §5.7 (p. 118).

Minimum-distance duality

For arbitrary $M$ and $x$, produce one functional $f$ with $\|f\|\le 1$, $f|_M=0$, and

for every other $g$ of norm at most one annihilating $M$. Thus $f$ realizes the dual maximum. If a best approximant $m_0\in M$ exists, the same certificate also satisfies

This packages both parts of the minimum-distance theorem in §5.8 (Theorem 1, pp. 119--120).

Significance

The capstone gives an exact lower-bound certificate for an infinite-dimensional approximation problem. Every feasible dual functional supplies the inequality $g(x)\le d(x,M)$, while the distinguished functional reaches equality. Consequently, the primal infimum is identified without assuming reflexivity, strict convexity, finite dimension, closedness of $M$, or existence of a nearest point. When a nearest point does exist, alignment records the equality case of the norm estimate and links the dual certificate back to the geometry of the residual.

The source result is classical and proved in the book; the open work here is its machine-checked Lean formalization in the same namespace as the earlier vector-space missions. The reusable output includes norm-controlled extension infrastructure, norming functionals, a concrete double-annihilator theorem, and a certificate form of distance duality suitable for later convex-separation and constrained-optimization missions.

Difficulty

The obvious Hilbert-space formulation fails because a normed space has no canonical orthogonal complement and a minimizing element of $M$ need not exist. Replacing the minimum by Metric.infDist avoids an unjustified attainment assumption, but the desired dual maximizer must still be an actual continuous functional, not merely a limiting family. Norm control is essential: an algebraic separator without continuity cannot serve as a bounded dual certificate.

There are also degenerate cases that informal notation can hide. The distance may be zero even when $x\notin M$ if $M$ is not closed, and then the zero functional is the correct capstone witness. Conversely, the book's assertion that a norming functional is nonzero requires a nontrivial ambient space. The formal statements must handle these cases without silently strengthening the main theorem to closed subspaces or positive distance.

Formalization scope

All spaces and functionals are real, matching the chapter and avoiding extra complex-scalar conjugation conventions. The ambient object uses Mathlib's NormedAddCommGroup, NormedSpace, Submodule, and ContinuousLinearMap; completeness is not assumed because the cited Hahn--Banach consequences do not require it. The distance is exactly Metric.infDist, and annihilation is written pointwise rather than by introducing a new annihilator definition. This keeps the capstone self-contained while the double-annihilator milestone states the same construction explicitly as a set.

No claim is made that a best approximant exists. The alignment clause is conditional on an element already satisfying the global minimum property. No closedness assumption may be added to the capstone, since the zero-distance/nonclosed case is part of the source theorem's generality. The norming-functional milestone alone assumes [Nontrivial X]; this prevents a vacuous encoding of “nonzero functional” on the zero space. Contributions may establish the four stated theorems and any generally useful lemmas about restrictions, quotient norms, annihilation, or Metric.infDist, provided the public statements retain these conventions.

Selected references

• David G. Luenberger, Optimization by Vector Space Methods, John Wiley & Sons, 1969, Chapter 5, especially §§5.4, 5.7, and 5.8, pp. 111--120. Public scan.

When is a system of linear constraints infeasible? Sections 4.6-4.7 of Bertsimas-Tsitsiklis answer with the archetypal theorem of the alternative. The capstone is Farkas' lemma (Theorem 4.6): for an $m \times n$ matrix $A$ and $b \in \mathbb{R}^m$, exactly one of the following holds — (a) some $x \ge 0$ satisfies $Ax = b$, or (b) some $p$ satisfies $p'A \ge 0'$ and $p'b < 0$; such a $p$ is a certificate of infeasibility, geometrically a hyperplane separating $b$ from the cone of the columns of $A$. The mission also carries the cone-membership restatement (Corollary 4.3), the inequality form (Theorem 4.7: every solution of $Ax \le b$ satisfies $c'x \le d$ iff some $p \ge 0$ has $p'A = c'$ and $p'b \le d$), and the application to asset pricing (Theorem 4.8: a market's prices admit no arbitrage iff there is a nonnegative state-price vector $q$ with $p_i = \sum_s q_s r_{si}$). The book proves Farkas' lemma from LP strong duality; Section 4.7 then reverses the arrow from first principles: every polyhedron is closed (Theorem 4.9), Weierstrass' theorem (Theorem 4.10, already in Mathlib), and the separating hyperplane theorem (Theorem 4.11: for nonempty closed convex $S$ and $x^* \notin S$ there exists $c$ with $c'x^* < c'x$ for all $x \in S$), from which Farkas' lemma — and hence the duality theorem itself — follows geometrically.

Is the shadow of a polyhedron again a polyhedron? §2.8 of Bertsimas–Tsitsiklis answers this with perhaps the oldest method for solving linear programming problems: Fourier–Motzkin elimination. Given $P = \{x \in \mathbb{R}^n \mid \sum_{j=1}^n a_{ij}x_j \ge b_i,\ i = 1, \dots, m\}$, one sorts the constraints by the sign of the coefficient of $x_n$ — rewriting them as $x_n \ge d_i + \mathbf{f}_i'\bar{x}$, $d_j + \mathbf{f}_j'\bar{x} \ge x_n$, or $0 \ge d_k + \mathbf{f}_k'\bar{x}$ — and forms the polyhedron $Q \subset \mathbb{R}^{n-1}$ whose constraints are all pairwise combinations $d_j + \mathbf{f}_j'\bar{x} \ge d_i + \mathbf{f}_i'\bar{x}$ together with the constraints not involving $x_n$. The capstone, Theorem 2.10, states that $Q$ is exactly the projection $\Pi_{n-1}(P)$ of $P$ onto its first $n-1$ coordinates: a value of $x_n$ can be interpolated if and only if every lower bound is below every upper bound. Though hopeless as an algorithm (the number of constraints can grow exponentially), elimination has powerful theoretical corollaries, all formalized here: projections $\Pi_k(P)$ of polyhedra are polyhedra (Corollary 2.4), the image of a polyhedron under any linear mapping is a polyhedron (Corollary 2.5), and the convex hull of finitely many vectors is a polyhedron (Corollary 2.6) — the first half of the finite-basis picture completed by the resolution theorem of Mission VII.

Where should one look for the optimum of a linear programming problem? Chapter 1 of Bertsimas–Tsitsiklis suggests that optima "tend to occur at corners" of the feasible polyhedron; §§2.5–2.6 turn this intuition into theorems. Not every polyhedron has a corner — a halfspace in $\mathbb{R}^n$ ($n > 1$) has none — and the exact dividing line is the presence of an infinite line: a nonempty polyhedron

has an extreme point if and only if it does not contain a line, if and only if $n$ of the vectors $a_1, \dots, a_m$ are linearly independent (Theorem 2.6). In particular every nonempty bounded polyhedron and every nonempty standard-form polyhedron has a basic feasible solution (Corollary 2.2). The capstone, Theorem 2.8, is the sharpest form of the corner principle: if $P$ has at least one extreme point, then for any cost vector $c$ either the optimal cost is $-\infty$, or there is an extreme point of $P$ that is optimal — existence of an optimal solution comes for free once the cost is bounded below. Its companion Theorem 2.7 places an optimal extreme point under the weaker assumption that an optimal solution exists, and Corollary 2.3 — the fundamental theorem of linear programming — concludes that every feasible LP either has optimal cost $-\infty$ or attains an optimal solution, in stark contrast with nonlinear problems such as minimizing $1/x$ over $x \ge 1$. These results license the extreme-point search that the simplex method (Mission IV) performs.