Optimization

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

$$P = \{x \mid a_i'x \ge b_i,\ i = 1, \dots, m\}$$

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.

Why stochastic-gradient convergence matters

Training a machine-learning model often means choosing a vector of parameters to minimize an average loss. Evaluating the full gradient can require processing an entire dataset. A stochastic-gradient method instead updates the parameters using a random direction obtained from a smaller amount of information. Its computational appeal raises a mathematical question: which assumptions on those directions and the stepsizes guarantee progress, and what kind of convergence follows?

This mission formalizes the core convergence theory in Section 4 of Bottou, Curtis, and Nocedal, Optimization Methods for Large-Scale Machine Learning. The results distinguish strongly convex objectives, where expected objective error can be controlled, from general smooth objectives, where the guarantee concerns gradients. They also distinguish constant stepsizes, which leave a noise-dependent error bound, from diminishing stepsizes.

Historical timeline

• 1951: Robbins and Monro introduced stochastic approximation for finding a root using noisy observations. Their work is the historical foundation for the stepsize conditions used here; the original root-finding theorem is not a separate target of this mission. Original paper.
• 2016: Bottou, Curtis, and Nocedal released the first version of their survey, organizing stochastic-gradient theory around smoothness and moment assumptions. arXiv record.
• 2018: The revised survey appeared in SIAM Review. This mission fixes arXiv version 3 for stable theorem numbering and PDF page citations. Published article.

The mathematics targeted here is already proved in the literature; the task is its Lean formalization, not a claim that these convergence results are unresolved research conjectures.

Objective, algorithm, and probability model

Let $F:\mathbb R^d\to\mathbb R$ be differentiable with an $L$-Lipschitz gradient, where $L>0$. On a probability space $(\Omega,\mathcal A,\mathbb P)$, let $\mathcal H_k$ contain the history before step $k$. Starting from a deterministic vector $w_0$, the algorithm uses positive deterministic stepsizes $\alpha_k$ and random directions $g_k$ to update

$$w_{k+1}=w_k-\alpha_k g_k.$$

The state $w_k$ is measurable with respect to $\mathcal H_k$; the direction $g_k$ is measurable with respect to $\mathcal H_{k+1}$ and has a finite second moment. Conditional assertions hold almost surely. This uses the adapted-process formulation expressly permitted in footnote 4, PDF p. 22, rather than requiring independent sample seeds. The local index $k=0$ corresponds to the paper's $k=1$. Algorithm 4.1 and footnote 4.

Write $\mathbb E_k$ for conditioning on $\mathcal H_k$. The moment conditions use constants $\mu_G\ge\mu>0$ and $M,M_V\ge0$:

$$\langle\nabla F(w_k),\mathbb E_k g_k\rangle\ge\mu\|\nabla F(w_k)\|^2, \qquad \|\mathbb E_k g_k\|\le\mu_G\|\nabla F(w_k)\|,$$ $$\mathbb E_k\|g_k\|^2-\|\mathbb E_k g_k\|^2 \le M+M_V\|\nabla F(w_k)\|^2.$$

Define $M_G=M_V+\mu_G^2$. The iterates lie almost surely in an open region on which $F\ge F_{\inf}$ for a real lower bound $F_{\inf}$. These are Assumptions 4.1 and 4.3, PDF pp. 23–24, equations (4.6)–(4.9). Source.

Formalization targets

The goal is Theorem 4.10, Section 4.3, PDF p. 33, equations (4.30a)–(4.30b). Suppose

$$\sum_{k=0}^\infty\alpha_k=\infty,\qquad \sum_{k=0}^\infty\alpha_k^2<\infty.$$

For $A_K=\sum_{k=0}^{K-1}\alpha_k$, establish both

$$\exists S\in\mathbb R:\quad \mathbb E\!\left[\sum_{k=0}^{K-1}\alpha_k\|\nabla F(w_k)\|^2\right]\longrightarrow S,$$ $$\frac{1}{A_K}\mathbb E\!\left[\sum_{k=0}^{K-1}\alpha_k\|\nabla F(w_k)\|^2\right] \longrightarrow0.$$

There is no convexity assumption and no restriction that the initial stepsizes already satisfy a small-step bound. Theorem 4.10.

Four milestones capture the surrounding theory. Lemma 4.4 gives the two successive conditional expected-descent inequalities (4.10a)–(4.10b), PDF pp. 24–25. It is a common input to the convergence results. Theorem 4.6 gives a geometric upper bound for strongly convex objectives with a constant stepsize. Theorem 4.7 gives the corresponding $O(1/k)$ bound for $\alpha_k=\beta/(\gamma+k+1)$. These are parallel strongly convex targets, not prerequisites for the nonconvex goal. Theorem 4.8 gives finite-horizon sum and average squared-gradient bounds for general objectives with a constant stepsize. Section 4.

For example, if $c>0$ is the strong-convexity constant, $d\ge1$, and $0<a\le\mu/(LM_G)$, Theorem 4.6 states, with $B=aLM/(2c\mu)$ and $F_*=\inf_xF(x)$,

$$\mathbb E[F(w_k)-F_*]\le B+(1-ac\mu)^k(F(w_0)-F_*-B).$$

The upper bound tends to $B$; this does not assert that the actual expected error tends to $B$. Every milestone retains the paper's constants and all displayed conclusions. Equations (4.13)–(4.14), PDF p. 26.

What a completed formalization provides

The result explains precisely how noise and stepsize interact. The general-objective goal guarantees that the stepsize-weighted expected squared gradients average to zero even when $M>0$. The strongly convex milestones quantify objective error and the effect of initialization. These results concern the stated quantities; they do not assert convergence of iterates, global optimality for a nonconvex objective, or almost-sure convergence. Sections 4.2–4.3.

A completed development would provide reusable Lean results for smooth objective functions, conditional moment bounds, stochastic updates, and expected convergence. The proposed statements are open proof obligations. Compilation establishes that the definitions and statements are well formed, not that their convergence claims have already been proved.

Mathematical and formal difficulties

Finite conditional expectations must be connected to unconditional integrals without relying on total-function defaults. The infinite-horizon result also requires careful handling of a finite initial segment: square summability gives eventually small steps, not a bound at every step. Strong convexity must justify the objective-gap estimates and the properties of the optimum. Treating a descent recurrence as a hypothesis would omit the analytic content that this mission is intended to formalize.

Formalization scope

The model uses real finite-dimensional Euclidean space, Mathlib gradients, filtrations, Bochner conditional expectations, and ordinary real integrals. The probability space is arbitrary; no finite-support or standard-Borel restriction is imposed. Directions have explicit finite second moments, making the finite-expectation convention in the paper visible. Square integrability of iterates and integrability of losses are consequences to establish, not extra model fields.

Strong convexity uses Mathlib's StrongConvexOn, equivalent here to Assumption 4.5's first-order inequality. The optimum is defined as the infimum of the range of $F$, with its finiteness to be derived in the strongly convex branch. That branch requires $d\ge1$: the paper's deduction $c\le L$ implicitly uses a nontrivial space. The nonconvex statements allow $d=0$. Zero noise is allowed. Finite-horizon averages require $K>0$; the value assigned at $K=0$ does not affect an asymptotic limit.

Contributions to the conditional-descent infrastructure and any of the four milestones are welcome. Variance reduction, Newton-type methods, and the remainder of the survey are outside this initial mission.

Selected references

• Léon Bottou, Frank E. Curtis, and Jorge Nocedal. Optimization Methods for Large-Scale Machine Learning. SIAM Review 60(2), 223–311, 2018. arXiv:1606.04838v3; DOI. All page numbers above refer to the 95-page arXiv v3 PDF.
• Herbert Robbins and Sutton Monro. A Stochastic Approximation Method. Annals of Mathematical Statistics 22(3), 400–407, 1951. DOI. Historical background only.

Why control variates matter in federated optimization

Federated optimization trains one model using objectives held by many clients. Performing several local updates between communication rounds saves communication, but clients with different objectives can move in different directions. SCAFFOLD maintains a correction for each client to address this disagreement, including when only some clients participate. Karimireddy et al. establish convergence without a bound on how similar the client objectives are. The relevant result is Theorem III, Section 5, PDF p. 5.

SCAFFOLD: Convergence with Client Sampling concerns that known result's formalization. Its exact targets are finite-round bounds from the Appendix E analysis, covering strongly convex, general convex, and nonconvex objectives. The paper's FedAvg results and its separate quadratic-acceleration theorem are outside this scope.

Setting: local updates and sampled clients

There are $N\ge1$ clients, with differentiable objectives $f_i:\mathbb R^d\to\mathbb R$. The global objective is $f(x)=N^{-1}\sum_i f_i(x)$. Every client gradient is $\beta$-Lipschitz, where $\beta>0$. A stochastic gradient query is conditionally unbiased and has conditional squared-error expectation at most $\sigma^2$, with $\sigma\ge0$. Current queries on different clients are conditionally independent given the full history. These make precise the fresh-oracle interpretation of A4–A5, Appendix B.1, PDF p. 14.

Each of $T\ge1$ rounds selects a uniform subset $A_r$ of $S$ clients, where $1\le S\le N$. Each selected client takes $K\ge1$ local steps. Let $x^r$ be the server model, $c_i^r$ its stored client control variates, and $c^r=N^{-1}\sum_i c_i^r$. With constant local and global step sizes $\eta_l>0$ and $\eta_g\ge1$, a client starts at $y_{i,0}^r=x^r$ and uses

$$y_{i,k+1}^r=y_{i,k}^r-\eta_l\bigl(g_{i,k}^r-c_i^r+c^r\bigr), \qquad x^{r+1}=x^r+\frac{\eta_g}{S}\sum_{i\in A_r}(y_{i,K}^r-x^r).$$

Option II replaces a participating client's control with $K^{-1}\sum_{k=0}^{K-1}g_{i,k}^r$ and retains every other control. These are Algorithm 1, PDF p. 4, and Appendix E, equations (18)–(21), PDF pp. 25–26. Write $h=K\eta_l\eta_g$ for the effective step size.

Formalization targets

Four milestones support a root goal that is the conjunction of the two convergence statements below.

GradientGrowth states, for convex clients and a global minimizer $x^\star$,

$$\frac1N\sum_i\|\nabla f_i(x)-\nabla f_i(x^\star)\|^2 \le2\beta\bigl(f(x)-f(x^\star)\bigr).$$

This is Appendix B.1, equation (9), PDF p. 14. PerturbedStrongConvexity states, for each $\mu$-strongly convex client and $\mu\ge0$,

$$\langle\nabla f_i(x),z-y\rangle\ge f_i(z)-f_i(y) +\frac\mu4\|y-z\|^2-\beta\|z-x\|^2,$$

as in Appendix C, Lemma 5, PDF p. 17.

ConvexFiniteRoundConvergence allows arbitrary deterministic initial controls $c_i^0$. Assume all clients are $\mu$-strongly convex with $\mu\ge0$, including ordinary convexity when $\mu=0$, and fix a minimizer $x^\star$ of $f$. Define

$$C_0=\frac1N\sum_i\|c_i^0-\nabla f_i(x^\star)\|^2, \qquad V_0=\|x^0-x^\star\|^2+\frac{9Nh^2}{S}C_0,$$ $$q=1-\frac{\mu h}{2},\qquad w_r=q^{-(r+1)},\qquad W_T=\sum_{r=0}^{T-1}w_r.$$

For $h\le1/(81\beta)$ and $\mu h\le S/(15N)$, the target is

$$\frac1{W_T}\sum_{r=0}^{T-1}w_r\, \mathbb E\bigl[f(x^r)-f(x^\star)\bigr] \le\frac{V_0}{hW_T} +\frac{12h\sigma^2}{KS}\left(1+\frac S{\eta_g^2}\right).$$

This is a finite-round formulation of Appendix E.1, Lemma 15, PDF p. 30; its $\mu=0$ case is the first bound on PDF p. 31.

NonconvexFiniteRoundConvergence assumes a lower bound $f_\mathrm{lower}$ for $f$ and initializes every client control with $K$ fresh gradients at $x^0$. Put $F_0=f(x^0)-f_\mathrm{lower}$. For $h\le(S/N)^{2/3}/(24\beta)$, establish

$$\frac1T\sum_{r=0}^{T-1}\mathbb E\|\nabla f(x^r)\|^2 \le\frac{14F_0}{hT} +\frac{70\beta h\sigma^2}{KS}\left(1+\frac S{\eta_g^2}\right).$$

This is the explicit finite-round consequence targeted from Appendix E.2, Lemma 19, PDF p. 34, with the initialization specified on PDF pp. 31 and 35. The full-client warm start's communication cost is separate from these $T$ optimization rounds.

What the result establishes

The bounds quantify optimization progress under stochastic gradients, several local steps, and partial participation. They permit arbitrarily different client objectives within the stated smoothness and convexity assumptions. Their output is a weighted random server iterate, represented by its expected loss, or a uniform random server iterate for the squared-gradient guarantee; this follows the output convention in equation (22), PDF p. 26.

The mathematical convergence analysis is published. The open work here is a Lean proof under the explicit stochastic-run model. The proposed statements do not themselves supply a machine-checked convergence proof. A completed development would provide reusable results about sampled finite averages, adaptive gradient queries, and optimization with stored noisy controls.

Where the difficulty lies

Local gradients are evaluated at different client states, and inactive clients retain controls computed in earlier rounds. Consequently, treating the server update as a centralized stochastic-gradient step discards both local disagreement and stale-control error. The challenge is to control these quantities while preserving their dependence on earlier randomness, as reflected in Appendix E.1–E.2, PDF pp. 26–35.

The source also needs careful transcription. The printed Theorem VII nonconvex noise term on PDF p. 25 differs from Lemma 19 in its smoothness and sampling factors, while output indices differ between equation (22) and the finite sum on p. 31. The exact targets above use the proof's finite-round constants and explicit indexing; they do not claim a verbatim formalization of every printed asymptotic rate.

Formalization scope

SCAFFOLD.Space is finite-dimensional real Euclidean space; SCAFFOLD.Problem records differentiable client objectives and smoothness. SCAFFOLD.Run records a standard Borel probability space, full-history filtration, measurable square-integrable iterates and oracle samples, and the concrete updates. Virtual local paths are generated before a fresh uniform size-$S$ subset is sampled, as permitted by the paragraph after equation (22), PDF p. 26.

The conventions include $S=N$, $K=1$, zero noise, and $\mu=0$. The output indices are precisely $0,\ldots,T-1$. Convex initial controls are deterministic; the nonconvex branch uses the specified stochastic warm start. The run definition assumes no descent inequality or convergence conclusion. Contributions should establish the four named propositions and necessary analysis/probability infrastructure while retaining these semantics.

Selected references

• Sai Praneeth Karimireddy, Satyen Kale, Mehryar Mohri, Sashank J. Reddi, Sebastian U. Stich, and Ananda Theertha Suresh, SCAFFOLD: Stochastic Controlled Averaging for Federated Learning, ICML 2020, PMLR 119:5132–5143; arXiv:1910.06378v4, revised 2021. Primary scope: Theorem III, PDF p. 5; A3–A5 and (9), p. 14; Lemma 5, p. 17; Appendix E, pp. 25–35, especially Lemmas 15 and 19.

Motivation

Set cover is the standard worked example of the primal-dual method, and Chapter 2 of Buchbinder's thesis uses it that way: it is where the machinery of §2.1 is first turned on a concrete NP-hard problem. Two analyses appear. The greedy algorithm, analysed by dual fitting, buys the set with the best cost-per-newly-covered-element ratio and charges the price to the elements it covers; the resulting element prices form an infeasible dual that becomes feasible after scaling by $H_n$. The primal-dual algorithm instead raises the price of an uncovered element until some set's constraint goes tight, buys that set, and repeats; the resulting dual is feasible, and each bought set is paid for by elements of frequency at most $f$, giving an $f$-approximation.

Both analyses have the same shape, and it is the shape that matters for the rest of the series: the algorithm never sees the optimum. It maintains a dual solution, and the approximation ratio falls out of comparing the primal it built against the dual it accumulated.

Setting

An instance consists of a finite type $E$ of elements, a finite type $S$ indexing available sets, an assignment $s \mapsto A_s \subseteq E$, and a nonnegative cost $c : S \to \mathbb{R}$. Every element is assumed to lie in at least one available set; the source leaves this implicit, and without it no cover exists and the approximation statements are vacuous. The covering LP and its packing dual are

$$(P)\quad \min \sum_{s} c_s x_s \ \text{ s.t. } \sum_{s : e \in A_s} x_s \ \ge\ 1 \ \ (\forall e \in E), \quad x \ge 0,$$ $$(D)\quad \max \sum_{e} y_e \ \text{ s.t. } \sum_{e \in A_s} y_e \ \le\ c_s \ \ (\forall s \in S), \quad y \ge 0.$$

The frequency of an element is the number of sets containing it, and $f$ denotes the maximum frequency over all elements.

The two standing assumptions — nonnegative costs, and every element lying in some available set — are carried by a bundled SetCoverInstance, not passed as loose hypotheses. Every source-facing statement in the mission takes such an instance and reads those facts off its fields, so none of them can be instantiated at data violating either. The two indicator lemmas are the exceptions and are labelled as generalized assisting results: one has no cost function in scope at all, and the other's hypothesis that a given $C$ covers is strictly stronger than coverability of the family.

Costs are permitted to be zero and the ground type is permitted to be empty. No Nonempty E hypothesis appears anywhere; when $E$ is empty, $f = 0$ and the $f$-approximation bound reads $\mathrm{cost}(C) \le 0$, which the certificate's tightness clause forces to be $0 \le 0$ rather than anything false.

Formalization targets

The results are stated about certificates, not about executable algorithms. This is the central modelling decision of the mission and it is deliberate: the mathematical content of the source's proofs is entirely a statement about the invariants the output satisfies, and separating that from the question of whether a particular procedure produces such output keeps each half provable on its own.

A primal-dual certificate is a pair $(C, y)$ where $C \subseteq S$ covers $E$, $y$ is dual-feasible, and every $s \in C$ has a tight dual constraint, $\sum_{e \in A_s} y_e = c_s$.

Goal — the primal-dual $f$-approximation

For any primal-dual certificate $(C,y)$ and any fractional cover $x$,

$$\sum_{s \in C} c_s \ \le\ f \cdot \sum_{s \in S} c_s x_s .$$

Since this holds against every fractional cover, it holds in particular against an optimal one, so the cover $C$ costs at most $f$ times the fractional optimum and a fortiori at most $f$ times the integral optimum.

The double-counting step

The one substantive step of the goal is split out as its own target: for a primal-dual certificate,

$$\sum_{s \in C} c_s \ \le\ f \cdot \sum_{e \in E} y_e .$$

Tightness rewrites the cover's cost as a double sum over chosen sets and their elements; exchanging the order groups it by element, each charged at most $f$ times. With this and weak duality, the goal is two lines.

The greedy bound

A greedy certificate at ratio $\rho$ is a cover $C$ and a nonnegative $y$ with $\sum_{s \in C} c_s = \sum_{e} y_e$ and $\sum_{e \in A_s} y_e \le \rho\, c_s$ for every $s$. For such a certificate and any fractional cover $x$,

$$\sum_{s \in C} c_s \ \le\ \rho \cdot \sum_{s} c_s x_s .$$

Instantiating $\rho = H_n$ is what recovers the source's greedy guarantee; the harmonic bound itself is already in Mathlib.

Set-cover weak duality and LP attainment

Every dual packing is bounded by every fractional cover, $\sum_e y_e \le \sum_s c_s x_s$; the fractional optimum is at most the integral optimum; and both optima are attained, not merely bounded below. Attainment of the fractional optimum is a genuine linear-programming fact and is the hardest supporting item in the mission.

Significance

This is where the series first converts a dual-feasibility invariant into an approximation ratio on a concrete combinatorial problem, and the two certificate predicates are reused verbatim by the online covering missions later in the series. Set cover approximation has, as far as we can determine, no prior formalization in Mathlib or in any public Lean library: there is no set-cover problem statement, no greedy analysis, and no $f$-approximation result to build on.

Difficulty

The two certificate bounds are finite-summation arguments of moderate length — the work is in a double-counting step that reindexes a sum over chosen sets into a sum over elements, weighted by frequency. Attainment of the fractional optimum is different in kind: it needs a compactness or vertex argument about the covering polytope and is the item most likely to need real work. Zero-cost sets are permitted throughout, so any later algorithm definition that divides by a cost must handle that case explicitly.

Formalization scope

Definitions cover §2.2 of the source, excluding §2.2.2 (randomized rounding), which is deferred to a separate mission because its expected-cost and failure-probability analysis is measure-theoretic and shares no infrastructure with the deterministic results.

Two theorems are not in this mission: that the greedy algorithm produces a greedy certificate, and that the primal-dual algorithm produces a primal-dual certificate. Those require defining the algorithms and proving termination and coverage, and are planned as a second wave. Until that wave lands, the source's Theorems 2.4 and 2.6 should not be described as fully formalized — what this mission establishes is the certificate-to-ratio half of each.

Selected references

• Niv Buchbinder, Designing Competitive Online Algorithms via a Primal-Dual Approach, PhD thesis, Tel Aviv University, 2008, §2.2, pp. 10–14. https://www.tau.ac.il/~nivb/download/phd-thsis.pdf
• Vijay V. Vazirani, Approximation Algorithms, Springer, 2001, Chapters 2 and 15 — the standard treatment of the greedy and primal-dual set-cover analyses.

Motivation

An online algorithm must commit to decisions before it knows the rest of its input, and it is judged by competitive analysis: the ratio between its cost and the cost of an optimal solution computed with full knowledge of the input. A recurring obstacle in this area is that each problem seems to need its own ad hoc potential-function argument. Buchbinder's thesis develops a single method that replaces those arguments — formulate the offline problem as a covering linear program, let the online algorithm raise the dual variables of its packing dual, and read the competitive ratio off the ratio between the primal and dual increments. The same recipe then yields algorithms for online set cover, weighted caching, ad-auction revenue, routing, and load balancing.

This mission formalizes the chapter where the method is introduced on its smallest example, the ski-rental problem. A customer needs skis for an unknown number of days: renting costs $1$ per day and buying costs $B$ once. The customer must decide, each morning, whether to rent again or buy, without knowing how many ski days remain. Despite its size the problem is the canonical rent-or-buy dilemma, and it has two classical tight results: a deterministic $2$-competitive algorithm, and a randomized algorithm whose competitive ratio tends to $e/(e-1)$, due to Karlin, Manasse, McGeoch and Owicki (1994). The primal-dual derivation of both is the content of Chapter 3.

Setting

An instance is a pair $(B, k)$: the purchase price $B$, a positive integer, and the number $k \ge 0$ of ski days, which the online algorithm does not know. An offline solution either buys at once, paying $B$, or rents on every day, paying $k$; so the offline optimum is

$$\mathrm{OPT}(B,k) \;=\; \min(B, k).$$

Chapter 3 casts this as a linear program (Figure 3.1, p. 18). The primal is a covering program with one buy variable $x$ and one rent variable $z_j$ per day $j$:

$$\text{minimize } \; B x + \sum_{j=1}^{k} z_j \quad \text{subject to} \quad x + z_j \ge 1 \ \text{ for each day } j.$$

Its dual is a packing program with one variable $y_j$ per day:

$$\text{maximize } \; \sum_{j=1}^{k} y_j \quad \text{subject to} \quad \sum_{j=1}^{k} y_j \le B, \qquad 0 \le y_j \le 1 .$$

The online structure enters in a single way: a new ski day appends a new covering constraint to the primal and a new variable to the dual, and previously raised primal variables may never be decreased. That monotonicity is what "previous decisions cannot be regretted" means formally.

The fractional primal-dual algorithm maintains $x$, initially $0$. On each new day, while $x < 1$ it sets $z_j \leftarrow 1 - x$, then raises

$$x \;\leftarrow\; x\left(1 + \tfrac{1}{B}\right) + \tfrac{1}{cB},$$

and sets $y_j \leftarrow 1$; once $x$ has reached $1$ it does nothing further. The free parameter $c$ is then pinned to the value that makes $x$ reach exactly $1$ after $B$ days,

$$c \;=\; \left(1 + \tfrac{1}{B}\right)^{B} - 1 .$$

Formalization targets

Goal — the fractional algorithm's competitive ratio at finite $B$

$$B\,x_k + \sum_{j=0}^{k-1} z_j \;\le\; \left(1 + \frac{1}{\left(1 + \frac{1}{B}\right)^{B} - 1}\right) \cdot \min(B, k) \qquad \text{for every } B \ge 1, \ k \ge 0 .$$

The coefficient is the exact finite-$B$ ratio $1 + 1/c$, left in closed form rather than replaced by a constant. This is deliberate: $\left(1+\frac1B\right)^B$ increases to $e$, so $c < e - 1$ and therefore $1 + 1/c > e/(e-1)$ for every finite $B$. A goal asserting $e/(e-1)$-competitiveness at finite $B$ would be false, and a goal asserting some rounded constant would be invalidated by any sharpening. The closed-form coefficient is the weakest statement that is stable under improvement.

Asymptotic companion — where $e/(e-1)$ actually lives

$$\lim_{B \to \infty} \left(1 + \frac{1}{\left(1 + \frac{1}{B}\right)^{B} - 1}\right) \;=\; \frac{e}{e-1} \;\approx\; 1.5819767 .$$

The classical constant is recorded here, as a limit of the coefficient sequence, and nowhere else.

Parallel target — the deterministic algorithm

$$\mathrm{detCost}(B,k) \;\le\; 2 \cdot \min(B,k), \qquad \mathrm{detCost}(B,k) = \begin{cases} k & k < B \\ 2B & k \ge B\end{cases}$$

Chapter 3's other result, independent of the fractional development.

Significance

The ski-rental bounds themselves are classical and tight, and nothing here is mathematically open. What the chapter contributes, and what this mission captures, is the derivation: it is the template instantiated by every later chapter of the thesis, so the artifacts built here — a covering/packing LP pair, its weak-duality instance, a monotone online variable with a closed-form growth law, and the primal-to-dual increment ratio as the source of the competitive factor — are the vocabulary in which the rest of the series will be stated.

On status: the mathematics is proved, published, and standard. It is not, to the best of a search of Mathlib at revision 0df444a, formalized — that revision contains no competitive-analysis or online-algorithm framework, no ski-rental development, and no general linear-programming weak-duality theorem. So the work this mission asks for is formalization of a known proof, not new mathematics, and the reusable output is infrastructure that does not currently exist in the library.

Difficulty

The offline problem is trivial, and a newcomer's first move — prove $\min(B,k)$ is the optimum and stop — solves the wrong problem. The content is entirely in the online constraint. Three specific places where the obvious argument stalls:

The optimum is never observed. The algorithm's cost must be compared against $\min(B,k)$ without $k$ being available to it. The comparison is routed through the dual instead: the dual objective the algorithm accumulates is a lower bound on every feasible primal solution, hence on the optimum, and the algorithm's own primal cost is a fixed multiple of that dual objective.

The growth law is piecewise. The update fires only while $x < 1$. Summing the per-day increments therefore does not telescope uniformly: days before $x$ reaches $1$ contribute $1 + 1/c$ each and later days contribute nothing, and the index at which the switch happens is exactly $B$ — which is a theorem about the recurrence, not an assumption.

The constant is forced, not chosen. $c = (1+1/B)^B - 1$ is not a free tuning parameter; it is the unique value for which the geometric sequence $x_j = \bigl((1+1/B)^j - 1\bigr)/c$ hits $1$ at $j = B$, which is in turn what makes the dual solution feasible ($\sum_j y_j \le B$). Dual feasibility and the choice of $c$ are the same fact.

Formalization scope

Conventions this development commits to. The purchase price is a natural number $B$ with $0 < B$, because Chapter 3 uses $B$ simultaneously as a price, as a day index ("buy skis on the $B$th day"), and as the exponent in $(1+1/B)^B$; costs are real numbers, with $B$ and $k$ coerced. Days are indexed from $0$, so day $j+1$ of the prose is index $j$, and Fin k indexes the $k$ days. Real division is total, so $1/0 = 0$; the hypothesis $0 < B$ is what keeps every reciprocal in the development genuine, and without it $c$ would evaluate to $0$ and the recurrence would collapse to the constant zero sequence. The algorithm's x < 1 guard is part of the formalized definition, not an informal aside: without it the cost would keep growing past day $B$.

A documented discrepancy in the source. The prose on p. 17 relaxes the integer program by letting $x$ and each $z_j$ range over $[0,1]$; Figure 3.1 on p. 18 prints only $x \ge 0$, $z_j \ge 0$. This mission takes the prose version, $0 \le x \le 1$ and $0 \le z_j \le 1$, as the canonical fractional program, and also records the nonnegativity-only region exactly as printed. Two separate theorems establish that both have least value $\min(B,k)$, so the discrepancy is resolved inside the mission rather than silently chosen. Solvers should note which of the two predicates a given statement uses.

Ruling out a trivializing formalization. The offline optimum is defined independently, as $\min(B,k)$, and is not derived from the algorithm's own behaviour; a separate theorem certifies that this value really is the least attainable objective value of the canonical program, so the goal cannot be satisfied by redefining the benchmark. The goal inequality is also tight — both sides are equal to $(1+1/c)$ times the number of days on which $x < 1$ — so it cannot be weakened into vacuity without becoming false.

Infrastructure, and what is reusable. The development needs only Mathlib big operators over Fin k, basic real analysis for the limit, and IsLeast. Two items are explicitly infrastructure rather than ski-rental content: the specialized weak-duality theorem for this covering/packing pair, and the Figure 3.1 optimum. Both are candidates for generalization by the later mission on Chapter 2's general linear-programming duality, and a solver who proves the general form there should expect this instance to be derivable from it rather than duplicated.

Out of scope here. The final paragraph of p. 19 rounds the fractional solution into a randomized algorithm by sampling a threshold $\alpha \in [0,1]$ uniformly and buying on the day whose increment of $x$ contains $\alpha$. That step needs a probability space and an expectation argument, and is deferred to the immediate follow-up mission, Primal-Dual Online Algorithms II: Randomized Rounding for Ski Rental. Contributions here should not anticipate it.

Selected references

• Niv Buchbinder, Designing Competitive Online Algorithms via a Primal-Dual Approach, PhD thesis, Tel Aviv University, 2008. Chapter 3, pp. 17–19. https://www.tau.ac.il/~nivb/download/phd-thsis.pdf
• Niv Buchbinder and Joseph (Seffi) Naor, The Design of Competitive Online Algorithms via a Primal-Dual Approach, Foundations and Trends in Theoretical Computer Science 3(2–3), 2009. https://doi.org/10.1561/0400000024
• Anna R. Karlin, Mark S. Manasse, Lyle A. McGeoch and Susan Owicki, Competitive randomized algorithms for nonuniform problems, Algorithmica 11(6), 1994, 542–571. https://doi.org/10.1007/BF01294260
• Allan Borodin and Ran El-Yaniv, Online Computation and Competitive Analysis, Cambridge University Press, 1998.

Motivation

Quantum algorithms for stochastic optimization are usually presented one paper at a time: a schedule is fixed, a quantum mean estimator is substituted for a classical minibatch, and a new rate is derived from scratch. The derivations are near-identical, and the step that actually differs — the price of one gradient query — is buried inside each proof rather than exposed as a parameter.

This mission publishes a Lean 4 development in which the oracle is a parameter, not an assumption. One rate theorem, instantiated at different oracle contracts and cost models, yields the classical rate, the inexact-gradient rate, and the quantum rate. All constants are explicit; nothing is asymptotic.

The published results it reproduces or corrects:

• Ghadimi--Lan (2013), the $\varepsilon^{-4}$ rate for smooth nonconvex SGD.
• Fang et al., the classical SPIDER variance-reduction schedule and its $\varepsilon^{-3}$ query complexity.
• Sidford--Zhang, Quantum speedups for stochastic optimization (arXiv:2308.01582) — Theorem 6's $\tilde O(\Delta\ell\sigma\sqrt{d}\,\varepsilon^{-3})$ and Theorem 8's $\tilde O(\ell\Delta\sqrt{d\sigma}\,\varepsilon^{-5/2})$, both obtained here from one schedule evaluated at two cost exponents.

Setting

Let $E$ be a real inner-product space, $f:E\to\mathbb{R}$ an objective, and $g:E\to E$ a map supplied as a parameter in place of the gradient. The smoothness hypothesis is the descent-lemma inequality

$$f(y)\;\le\;f(x)+\langle g(x),y-x\rangle+\tfrac{L}{2}\|y-x\|^{2},$$

written $\mathrm{QuadUpper}\,f\,g\,L$; this is exactly what rate proofs consume, and it is implied by a Lipschitz gradient. Write $\Delta_0=f(x_0)-f^{\star}$ for the initial gap, $\varepsilon$ for the target accuracy, $\sigma$ for the gradient-noise scale, $\ell$ for the mean-squared smoothness constant, and $d$ for the ambient dimension.

A cost model converts a target accuracy into a query count as a power law with exponent $p$. Its $p=2$ member is the classical minibatch bill, scaling as $\sigma^{2}/\varepsilon^{2}$; its $p=1$ member is the quantum mean-estimation bill, scaling as $\sigma/\varepsilon$. That single exponent is where classical and quantum part company.

Target

The goal theorem is the exact crossover between the two SPIDER bills. Writing $Q$ and $C$ for the dominant terms of the quantum and classical query totals,

$$Q=\frac{64000\,\ell\Delta\sqrt{d}\sqrt{10\sigma}}{\varepsilon^{2}\sqrt{\varepsilon}},\qquad C=\frac{25\,728\,000\,\ell\Delta\sigma}{\varepsilon^{3}},$$

the target asserts, for $\ell,\Delta,\sigma,\varepsilon>0$ and $d\ge0$,

$$Q<C\quad\Longleftrightarrow\quad d\,\varepsilon<16000\,\sigma .$$

Every supporting rate is also published and proved: the two SPIDER query totals, SPIDER's correctness, the SGD and PL rates, the exact and inexact gradient-descent rates, the two variance-purchase bills, and the two query counts.

Significance

The results. The crossover makes the dimension-versus-accuracy trade-off of quantum stochastic optimization quantitative rather than folkloric. Two readings follow directly: at fixed $d$ the quantum advantage disappears as $\varepsilon\to0$, so the speedup lives at moderate accuracy, not asymptotically; and at fixed $\varepsilon$ the advantage requires $d<16000\sigma/\varepsilon$. Note what cancels — $\ell$, $\Delta$ and the $\varepsilon$-exponent all drop out, leaving only $d\varepsilon$ against $\sigma$.

The formalization. Because the oracle and the cost exponent are parameters, the classical and quantum rates are one theorem evaluated twice rather than two proofs. This mission is unusual in that its frontier is already closed: every node arrives with a machine-checked proof, transplanted from a green build. What it offers the platform is a reusable, fully-proved layer for first-order convergence analysis — function classes, cost models, a one-step descent recursion, accumulation laws including a stopped-time version, and the SPIDER schedule — on which further rates can be built by instantiation.

Difficulty

The apparent difficulty is not where a newcomer expects. Deriving a rate from the one-step recursion is routine telescoping. What is delicate is keeping the constants honest while the oracle varies: a rate proof that quietly assumes an exact gradient, or a global lower bound on $f$, will produce the right-looking exponent from the wrong hypotheses.

Two specific places carry real content. Evaluating an error recursion at a random return time breaks the unconditional variance bound, because conditioning on $\tau=k$ destroys independence; the stopped-time accumulation law is what repairs it. And reproducing a published constant exactly — rather than up to $\tilde O(\cdot)$ — is what certifies that the parametrized machinery has not silently degraded the bound it generalizes.

Formalization scope

Smoothness is QuadUpper on an explicitly supplied g; no differentiability or convexity is assumed anywhere, and the only lower-bound hypothesis is $f^{\star}\le f(x_K)$ at the terminal iterate rather than globally. Cost models are an inductive family with a power-law member, so the classical and quantum instances are $p=2$ and $p=1$ of one definition. Half-integer powers are written with Real.sqrt, so no real exponentiation appears in any statement. Stochastic results use a genuine Filtration and a conditional oracle contract; the tower property is derived, not assumed.

Two honesty notes. Several statements carry hypotheses that Lean marks unused; these are recorded as such in the individual nodes rather than presented as load-bearing. And the library records a discrepancy in Sidford--Zhang's Algorithm 7 parameter block, documented in its own STATUS notes; the formalization follows the corrected parameters.

Selected references

• S. Bubeck-style descent machinery aside, the rates reproduced here are: S. Ghadimi and G. Lan, Stochastic first- and zeroth-order methods for nonconvex stochastic programming, SIAM J. Optim. 23(4) (2013).
• C. Fang, C. J. Li, Z. Lin, T. Zhang, SPIDER: Near-optimal non-convex optimization via stochastic path-integrated differential estimator, NeurIPS 2018.
• A. Sidford and C. Zhang, Quantum speedups for stochastic optimization, arXiv:2308.01582.
• Source development: lean-optrates, github.com/shiy1022/lean-optrates at commit 4c0b8498, Apache-2.0, by Yueheng Shi. The platform copy renames the root namespace OptRates to ShiOptRates; no statement or proof is otherwise altered.

A performance guarantee for a simple replenishment rule

When replenishment takes several periods, an inventory decision commits stock before the demand that will consume it is known. Too much stock incurs holding costs; too little loses sales. An optimal decision can depend on the entire pipeline of outstanding orders. A rule with only two adjustable parameters is easier to implement, but its simplicity alone gives no guarantee on the cost it can incur.

Capped base-stock policies combine an inventory-position target with a maximum order quantity. The class was introduced and analyzed by Xin (2021). The present target is the finite-lead-time guarantee in Linwei Xin's Capped Base-Stock Policies: A 2.33-Approximation, specifically the author-supplied manuscript with source label thm-main. A public listing of the paper identifies the July 17, 2026 working paper; the supplied text is the authoritative version for this formalization.

Demand, stock, and delayed orders

Periods are discrete. Demand is a sequence of independent, identically distributed nonnegative real random variables $D_t$ with finite, strictly positive mean $\mu$. The deterministic lead time is an integer $L\ge1$. Holding and lost-sales rates are $h>0$ and $p>0$.

At the beginning of period $t$, $I_t$ is on-hand inventory and $x_{1,t},\ldots,x_{L,t}$ are outstanding orders, with $x_{1,t}$ due immediately. That arrival is received, an order $q_t\ge0$ is placed, demand is realized, and costs are charged. The new order arrives $L$ periods later. The equations are

$$I_{t+1}=(I_t+x_{1,t}-D_t)^+,\qquad x_{i,t+1}=x_{i+1,t}\ (i<L),\qquad x_{L,t+1}=q_t.$$

Here $u^+=\max\{u,0\}$. Unfilled demand is lost rather than backlogged. With $\ell_t=(D_t-I_t-x_{1,t})^+$, the period cost is $hI_{t+1}+p\ell_t$. Initial inventory and every pipeline coordinate are zero. A nonanticipative policy chooses orders using only information available before the current demand; policies may depend on the entire observed past and on independent private randomization.

For a policy $\pi$, its long-run expected average cost is

$$C(\pi)=\limsup_{T\to\infty}\frac1T\sum_{t=1}^T\mathbb E[hI_{t+1}^\pi+p\ell_t^\pi],\qquad \mathrm{OPT}=\inf_{\pi\in\Pi}C(\pi).$$

The capped rule is $q_t=\min\{(S-I_t-\sum_{i=1}^Lx_{i,t})^+,r\}$ for finite $S,r\ge0$. Write $C^*_{\rm CBS}=\inf_{S,r\ge0}C(\pi_{S,r})$. Ordinary base stock is already included by taking $r=S$; no infinite order cap is required.

Formalization targets

For $0\le r\le\mu$ and $m\ge1$, set

$$I_r^m=\max_{0\le k\le m}\sum_{i=1}^k(r-D_i),\qquad G_m(r,z)=\mathbb E\left[\left(I_r^m+\sum_{i=1}^m(D_i-r)-z\right)^+\right].$$

Empty sums are zero. The lower certificate is

$$\underline C=\inf\{hz+p(\mu-r):0\le r\le\mu,\ z\ge0,\ G_L(r,z)\le L(\mu-r),\ G_{L+1}(r,z)\le(L+1)(\mu-r)\}.$$

The pair $(0,0)$ is feasible. Both horizon constraints are retained. With

$$\kappa_L=1+\frac{4L^2}{(L+1)(3L-1)},$$

the goal is Theorem 1's complete assertion:

$$C^*_{\rm CBS}\le\kappa_L\underline C,\qquad C^*_{\rm CBS}\le\kappa_L\mathrm{OPT}\le\frac73\mathrm{OPT}.$$

The exact rational constant is used; the title's 2.33 is a rounded description. Multiplicative inequalities also make sense when the optimal cost is zero.

Five supporting targets reproduce selected source statements: Proposition 1's lower-certificate bound; Proposition 2's finite-cap cost conclusion; Lemma 2's bound on a consecutive block in the greedy recursion; Proposition 3's ordinary-base-stock cost bound; and Proposition 4's two-branch inequality. The finite-cap and ordinary-base-stock parameters remain exactly $(S,r)=((L+1)r+z,r)$ and $S=(L+1)r+2z$, respectively. Labels accompany the printed numbering so the supplied source is unambiguous.

What completing the mission establishes

The result gives a uniform cost guarantee for this policy class across all positive holding and penalty rates, every positive integer lead time, and arbitrary nonnegative demand laws with finite positive mean. It bounds the infimum of costs over the policy parameters; it does not by itself provide an algorithm for selecting parameters or assert that the infimum is attained. At $L=1$ the displayed coefficient is 2, while its uniform upper bound is $7/3$.

The manuscript supplies mathematical proofs. This mission asks for checked proofs of their formal statements. Compiling the declarations confirms that they are well formed, not that the claims are proved. A completed development would provide reusable delayed-inventory dynamics, measurable history policies, average-cost optimization objects, finite-horizon demand envelopes, and policy-comparison results.

Where the formal work lies

The pipeline carries consequences of past decisions across multiple demand periods. Nonanticipativity and independence must be stated precisely before expectation and convexity arguments can be used. Also, existence of a stationary distribution alone does not identify its expected cost with a long-run cost from an empty initial system. The manuscript invokes stationary results from prior inventory work, including Xin and Goldberg (2016), and uses stationary CBS quantities in intermediate arguments. Their needed hypotheses and connections to the original objective require proof within a complete development.

The two cost bounds depend on both coordinates of a feasible lower-certificate pair. Losing either horizon constraint changes that certificate. Replacing it with an arbitrary scalar lower bound or assuming the policy comparisons would remove substantive parts of the result.

Formalization scope and conventions

Stock, orders, and demand take arbitrary nonnegative real values. Time is represented from zero in the operational model, corresponding to period one in the manuscript. The formal representation uses a canonical probability model with independent demand coordinates and an independent uniform private seed; measurable time-dependent decision functions use only preceding demands and that seed. Connecting arbitrary standard-Borel randomized controls to this canonical realization is a representation obligation. The zero-start optimum ranges over these general history policies, not only stationary or capped policies.

Expected nonnegative costs, their upper limits, and cost infima are represented in the extended nonnegative reals. Thus a policy with infinite expected cost does not acquire a fictitious zero value through a totalized real integral. The finite-horizon envelope expectations use the original integrable demand law. The greedy lemma uses integer-indexed sequences so subtraction of earlier times has no natural-number truncation; its blocks are nonempty, as required to define their maximum.

Definitions contain no unproved facts. In particular, stationarity, convergence from the empty initial state, lower bounds, and upper policy comparisons are not fields assumed by the model. Contributions to these intermediate obligations and to any of the five source targets support the central theorem.

Selected references

• Linwei Xin, Capped Base-Stock Policies: A 2.33-Approximation, working paper, 2026. SSRN listing. Author-supplied LaTeX is authoritative: Theorem 1 (thm-main), Proposition 1 (lemma-lb), Proposition 2 (prop-finite-cap-bound), Lemma 2 (lem-greedy-window), Proposition 3 (prop-base-stock-bound), Proposition 4 (lem-two-branch). Source SHA-256: f353793c255e1ebed5f3ec541037284bd926183e3e5b71941f13e79c2d67cb7a.
• Linwei Xin, Technical Note—Understanding the Performance of Capped Base-Stock Policies in Lost-Sales Inventory Models, Operations Research 69(1), 61–70, 2021. DOI.
• Linwei Xin and David A. Goldberg, Optimality Gap of Constant-Order Policies Decays Exponentially in the Lead Time for Lost Sales Models, Operations Research 64(6), 1556–1565, 2016. DOI.

Motivation

Chapter 5 of Luenberger's Optimization by Vector Space Methods (Wiley, 1969) carries the minimum norm theory of Chapter 3 (Mission I of this series) from Hilbert space to arbitrary real normed spaces. The inner product is gone, so orthogonal projection is no longer available; its role is taken over by the Hahn–Banach theorem, in two classical forms. The extension form generalizes the projection theorem and yields a duality principle equating a minimum norm problem in a space $X$ with a maximization problem in its dual $X^*$; the geometric form (separating hyperplanes) extends that duality from subspaces to convex sets. These duality theorems are the backbone of the optimization theory in the remainder of the book — conjugate functionals (Ch. 7) and Lagrange duality (Ch. 8) both trace back to them.

Setting

Throughout, $X$ is a real normed linear space. A linear functional $f$ on $X$ is bounded if $|f(x)| \le M\|x\|$ for some constant $M$ and all $x$; the least such $M$ is the norm $\|f\|$. The (normed) dual $X^*$ is the space of bounded (equivalently, continuous) linear functionals with this norm; $\langle x, x^*\rangle$ denotes $x^*(x)$. A functional $p : X \to \mathbb{R}$ is sublinear when $p(x+y) \le p(x) + p(y)$ and $p(\alpha x) = \alpha\, p(x)$ for $\alpha > 0$. Vectors $x \in X$ and $x^* \in X^*$ are aligned when $\langle x, x^*\rangle = \|x^*\|\,\|x\|$, and orthogonal when $\langle x, x^*\rangle = 0$; for $S \subseteq X$, the complement $S^\perp \subseteq X^*$ consists of the functionals vanishing on $S$, and for $U \subseteq X^*$, ${}^\perp U \subseteq X$ consists of the vectors annihilated by every member of $U$. A hyperplane is a maximal proper linear variety; closed hyperplanes are the level sets $\{x : \langle x, x^*\rangle = c\}$ of nonzero bounded functionals. The support functional of a convex set $K$ is $h(x^*) = \sup_{k \in K}\, \langle k, x^*\rangle$.

Formalization targets

The goal is §5.13 Theorem 1 (Minimum Norm Duality): if $x_1 \in X$ has distance $d > 0$ from a convex set $K$ with support functional $h$, then

$$d \;=\; \inf_{x \in K} \|x - x_1\| \;=\; \max_{\|x^*\| \le 1}\ \big[\langle x_1, x^*\rangle - h(x^*)\big],$$

the maximum on the right being achieved by some $x_0^*$; and if the infimum is achieved by $x_0 \in K$, then $-x_0^*$ is aligned with $x_0 - x_1$.

The milestones trace the chapter's route there: boundedness $\Leftrightarrow$ continuity (§5.2); the Hahn–Banach theorem in sublinear form (§5.4 Theorem 1) with its norm-preserving extension and norming-functional corollaries; the annihilator identity ${}^\perp(M^\perp) = M$ for closed subspaces (§5.7 Theorem 1); the two subspace duality theorems and the alignment characterization of best approximations (§5.8 — the chapter's principal results); and the geometric form: Mazur's separation theorem, the support theorem, and Eidelheit's separation theorem (§5.12).

Significance

The §5.8 duality theorems are the exact normed-space analogue of the projection theorem: existence transfers to the dual problem (minimum norm problems should be formulated in a dual space to guarantee solutions — the chapter's methodological moral), orthogonality becomes alignment, and infinite-dimensional problems with finitely many constraints reduce to finite-dimensional dual problems. The geometric form underpins all of convex duality.

All results are classical and proved in the source. Mathlib contains the Hahn–Banach extension theorem and point/convex separation theorems, so several milestones are exercises in connecting Luenberger's formulations to existing library lemmas; the two §5.8 duality theorems, the alignment corollary, and the §5.13 convex duality theorem have no direct Mathlib counterpart and are the mission's genuinely new content.

Difficulty

Degenerate cases are the trap throughout. In §5.8 Corollary 1 the "only if" direction fails literally when $M$ is dense and $x \in M$ (then $M^\perp = \{0\}$ and no nonzero aligned functional exists); the formalization therefore carries the hypothesis $x \notin \overline{M}$. In the separation theorems the strict inequality holds only on the interior of the convex set — on the set itself only $\le$ survives — and nonemptiness hypotheses (of the interior, of $K_2$, of the variety) are what make the "nonzero functional" claims true; dropping any of them creates false statements in trivial spaces. In §5.13 the support functional may take the value $+\infty$, so the dual maximum is formalized by two quantified inequalities (the witness achieves $d$; no admissible functional exceeds $d$) rather than by a real-valued supremum. The infimum in the primal problems need not be attained — attainment appears only as a hypothesis in the alignment clauses.

Formalization scope

Real scalars throughout. The dual space is represented concretely as continuous linear maps X →L[ℝ] ℝ, and annihilators are written as explicit quantified conditions rather than named subspaces. Five notions the chapter needs and Mathlib lacks are published as definitions and used by the statements rather than inlined: alignment ($\langle x, x^*\rangle = \|x^*\|\,\|x\|$), the support functional ($h(x^*) = \sup_{k \in K} \langle k, x^*\rangle$, valued in the extended reals since it may be infinite), the total variation of a function on an interval, the normalized space $NBV[a,b]$, and the Riemann–Stieltjes integral (defined relationally, so that no existence claim is built into the definition). The Minkowski functional needed for Mazur's theorem is Mathlib's gauge. Minimum distances are infima ⨅ over coerced sets or submodules; in §5.8 Theorem 2 the dual-side supremum is a real sSup over $\{\langle x, x^*\rangle : x \in M,\ \|x\| \le 1\}$, which is nonempty and bounded. Sublinearity in §5.4 is hypothesized exactly as in the source (subadditivity plus positive homogeneity plus continuity). Linear varieties are parametrized as $x_0 + M$ with $M$ a Submodule ℝ X. No completeness of $X$ is assumed anywhere — the chapter's results are genuinely about normed spaces, and Hahn–Banach needs no completeness. The concrete dual of $C[a,b]$ (§5.5) is in scope, and carries most of the mission's new infrastructure: Mathlib has the property of bounded variation (eVariationOn) but no total-variation norm, no normalized space $NBV[a,b]$, and no Riemann–Stieltjes integral — its StieltjesFunction is the different object of a monotone right-continuous function inducing a Borel measure, and its Riesz–Markov–Kakutani development represents positive functionals on $C_c(X)$ by measures, not bounded functionals on $C[a,b]$ by functions of bounded variation. This mission therefore publishes those notions as definitions and states the representation theorem in both directions. §5.3 (the Riesz–Fréchet theorem, i.e. self-duality of Hilbert space) is the one omission: Mathlib's InnerProductSpace.toDual already provides it. §5.6 (second dual, reflexivity) is definitional and likewise present in Mathlib.

Selected references

• David G. Luenberger, Optimization by Vector Space Methods, John Wiley & Sons, 1969. Chapter 5, pp. 103–142. ISBN 0-471-55359-X.
• H. Hahn, Über lineare Gleichungssysteme in linearen Räumen, J. Reine Angew. Math. 157 (1927), 214–229; S. Banach, Sur les fonctionnelles linéaires II, Studia Math. 1 (1929), 223–239.
• S. Mazur, Über konvexe Mengen in linearen normierten Räumen, Studia Math. 4 (1933), 70–84.

Motivation

Chapter 4 of Luenberger's Optimization by Vector Space Methods (Wiley, 1969) develops linear least-squares estimation as an application of the Hilbert space projection theorem formalized in Mission I of this series. The chapter's centerpiece is the classical Gauss–Markov theorem: among all linear unbiased estimators of an unknown parameter vector from noisy linear measurements, the estimator $(W^\top Q^{-1} W)^{-1} W^\top Q^{-1} y$ has minimum variance — componentwise, not merely in trace. This result is foundational for statistics and econometrics, and its Hilbert-space derivation is the cleanest known.

Setting

Measurements are modeled as $y = W\beta + \varepsilon$, where $y$ is an $m$-dimensional data vector, $W$ a known $m \times n$ matrix ($n < m$) with linearly independent columns, $\beta$ an unknown $n$-dimensional parameter vector, and $\varepsilon$ a random $m$-vector of measurement errors with $E\varepsilon = 0$ and covariance $E[\varepsilon\varepsilon^\top] = Q$, positive definite. A linear estimate is $\hat\beta = Ky$ for a constant $n \times m$ matrix $K$; it is unbiased when $E\hat\beta = \beta$ for every $\beta$, which holds iff $KW = I$. The optimality criterion is the error second moment $E\|\hat\beta - \beta\|^2$, and the book's key observation (p. 85) is that the problem splits into $n$ independent minimum norm problems, one per component, each solvable by the dual approximation theorem of Mission I.

Formally, randomness is carried by an abstract probability space: a measure space $(\Omega, \mu)$ with $\mu$ a probability measure, random vectors as functions $\Omega \to \mathbb{R}^m$ with explicit integrability hypotheses for all first and second moments, and $E[\cdot] = \int \cdot \, d\mu$.

Formalization targets

The goal is §4.4 Theorem 1 (Gauss–Markov): with $K_0 = (W^\top Q^{-1} W)^{-1} W^\top Q^{-1}$,

$$K_0 W = I, \qquad E\big[(K_0 y - \beta)_i^2\big] \le E\big[(K y - \beta)_i^2\big] \quad \text{for every } i \text{ and every } K \text{ with } KW = I,$$

with error covariance

$$E\big[(K_0 y - \beta)(K_0 y - \beta)^\top\big] = (W^\top Q^{-1} W)^{-1}.$$

Milestones: the deterministic least-squares estimate $\hat\beta = (W^\top W)^{-1} W^\top y$ (§4.3 Theorem 1); the book's deterministic reduction — minimize the diagonal entries of $KQK^\top$ subject to $KW = I$ (p. 85); the minimum-variance estimate $\hat\beta = E[\beta y^\top] (E[y y^\top])^{-1} y$ for random $\beta$ (§4.5 Theorem 1); and the information-form identities $RW^\top(WRW^\top + Q)^{-1} = (W^\top Q^{-1}W + R^{-1})^{-1}W^\top Q^{-1}$ and $R - RW^\top(WRW^\top+Q)^{-1}WR = (W^\top Q^{-1}W + R^{-1})^{-1}$ (§4.5 Corollary 2).

Significance

The Gauss–Markov theorem justifies weighted least squares as the optimal linear unbiased procedure and is the standard benchmark against which biased and nonlinear estimators are measured. The minimum-variance estimate of §4.5 is the Bayesian counterpart with prior covariance $R$; the information-form identities connect the two and exhibit Gauss–Markov as the limit $R^{-1} \to 0$. Mission III builds the recursive (Kalman) estimator directly on these results.

All results are classical and proved in the source. Mathlib has mature measure-theoretic integration but, to date, no Gauss–Markov theorem and no linear estimation theory; the matrix milestones (trace reduction, information form) are also absent as stated. The probabilistic statements here are deliberately phrased with elementary integrals of products of real-valued components — no Bochner integration of vector-valued maps — so they are approachable with MeasureTheory.integral alone.

Difficulty

The subtlety is bookkeeping, not depth. Unbiasedness must be encoded as the algebraic constraint $KW = I$ (the book proves the equivalence with $E\hat\beta = \beta$ for all $\beta$); the componentwise variance claim is strictly stronger than the trace claim and requires the per-component minimum norm argument, not a single matrix inequality. Positive definiteness of $Q$ enters through invertibility of $W^\top Q^{-1} W$, which itself needs the linear independence of the columns of $W$ — dropping either hypothesis makes the goal false. In the probabilistic statements every integral needs an integrability hypothesis; the drafts supply integrability of all pairwise products of components, from which integrability of every derived expression follows.

Formalization scope

Random vectors are plain functions Ω → Fin m → ℝ on a MeasurableSpace Ω with a probability measure μ; second moments are hypotheses of the form ∫ ω, ε ω i * ε ω j ∂μ = Q i j with explicit Integrable assumptions; no independence, Gaussianity, or distributional assumptions are used anywhere. Matrices are Matrix (Fin m) (Fin n) ℝ with Mathlib's Matrix.PosDef, nonconstructive inverse ⁻¹, and mulVec. Norms on parameter space are written as explicit finite sums of squares, avoiding any ambiguity between Euclidean and supremum norms on pi types. The estimators under comparison are strictly linear ($\hat\beta = Ky$, no affine offset), exactly as in the source; §4.5's affine extension (its Problem 6) is out of scope.

Selected references

• David G. Luenberger, Optimization by Vector Space Methods, John Wiley & Sons, 1969. Chapter 4, pp. 78–102. ISBN 0-471-55359-X.
• A. C. Aitken, On least squares and linear combination of observations, Proc. Roy. Soc. Edinburgh 55 (1935), 42–48 (the weighted-least-squares form of Gauss–Markov).

Motivation

Luenberger's Optimization by Vector Space Methods (Wiley, 1969) organizes a large part of optimization theory around a single geometric idea: minimum norm problems in inner product spaces, solved by orthogonal projection. Chapter 3 is the technical heart of that program. Its projection theorem and normal equations underlie least-squares data fitting, Fourier approximation, minimum-energy control, and the whole statistical estimation theory of Chapter 4 — which Missions II and III of this series formalize on top of the present one.

Setting

Throughout, spaces are real. A pre-Hilbert space is a real vector space $X$ with an inner product $\langle\cdot,\cdot\rangle$ inducing the norm $\|x\| = \langle x,x\rangle^{1/2}$; a Hilbert space $H$ is a complete pre-Hilbert space. Vectors $x, y$ are orthogonal when $\langle x, y\rangle = 0$; for a subset $S$, the orthogonal complement $S^\perp$ is the set of vectors orthogonal to every element of $S$. Given $y_1,\dots,y_n \in H$, their Gram matrix is $G(y_1,\dots,y_n)_{ij} = \langle y_i, y_j\rangle$ and its determinant $g(y_1,\dots,y_n)$ is the Gram determinant. A linear variety is a translate $x + M$ of a subspace $M$.

Formalization targets

The goal is §3.10 Theorem 2, the dual approximation problem: for linearly independent $y_1,\dots,y_n \in H$ and constants $c_1,\dots,c_n$, among all $x \in H$ satisfying the constraints

$$\langle x, y_i\rangle = c_i, \qquad i = 1,\dots,n,$$

there is a unique vector of minimum norm, and it has the form

$$x_0 = \sum_{i=1}^n \beta_i\, y_i, \qquad \text{where} \qquad \sum_{j=1}^n \beta_j \langle y_j, y_i\rangle = c_i .$$

The milestone list follows the chapter's own development: the projection theorem in its pre-Hilbert form (§3.3 Theorem 1) and classical form (§3.3 Theorem 2), the orthogonal decomposition $H = M \oplus M^\perp$ with $M^{\perp\perp} = M$ (§3.4 Theorem 1), the normal equations and Gram matrices (§3.6), the Gram determinant formula $\delta^2 = g(y_1,\dots,y_n,x)/g(y_1,\dots,y_n)$ for the minimum distance (§3.6 Theorem 1), best approximation by Fourier sums over orthonormal families (§3.7, §3.9), minimum norm over a linear variety (§3.10 Theorem 1), and the extension from subspaces to closed convex sets with its variational inequality characterization (§3.12 Theorem 1).

Significance

The dual approximation theorem converts an infinite-dimensional constrained minimum norm problem into an $n \times n$ linear system — the book's model example of finite reduction, applied there to minimum-energy control of a motor (§3.11) and, in Chapter 4, to every linear estimation problem: least squares, Gauss–Markov, and recursive (Kalman) estimation are all instances of these results in a Hilbert space of random variables.

All results here are classical and proved in the source; the mission's product is a faithful machine-checked development with reusable statements. Mathlib already contains close relatives of several milestones (orthogonal projection onto complete subspaces, Submodule.orthogonal), so part of the work is connecting the book's formulations to that library; the Gram determinant distance formula and the dual approximation theorem itself have no direct Mathlib counterpart.

Difficulty

The individual milestones are standard Hilbert space theory. The care is in the statements, not tricks: the pre-Hilbert version of the projection theorem asserts uniqueness and the orthogonality characterization without existence, while existence requires completeness and closedness — conflating the two versions produces unprovable or vacuous statements. The Gram determinant formula requires the $(n+1) \times (n+1)$ Gram matrix of the extended family $(y_1,\dots,y_n,x)$, where index bookkeeping (Fin.snoc) is easy to get wrong. In §3.12 the variational inequality $\langle x - k_0, k - k_0\rangle \le 0$ replaces the equality characterization valid for subspaces; the inequality direction is a known trap.

Formalization scope

The development commits to: real scalars (the book allows complex; this series does not), an abstract space H : Type with [NormedAddCommGroup H] [InnerProductSpace ℝ H] and [CompleteSpace H] exactly where the source assumes a Hilbert space; subspaces as Submodule ℝ H with explicit IsClosed hypotheses; finite families as Fin n → H; Gram matrices as Matrix (Fin n) (Fin n) ℝ via Matrix.of; minimum distances as infima (⨅) over coerced submodules. Best approximation statements are phrased as explicit inequalities ‖x - m₀‖ ≤ ‖x - m‖ rather than through any projection operator, so they are usable without choosing Mathlib's orthogonalProjection API. Statements deliberately carry no more hypotheses than the source: §3.3 Theorem 1 and the normal equations hold in any real inner product space; completeness appears only where existence is claimed.

Proofs are expected to lean on Mathlib's inner product space library; contributions of reusable bridging lemmas (e.g. between ⨅-formulations and orthogonalProjection) are welcome as child lemmas via proof sketches.

Selected references

• David G. Luenberger, Optimization by Vector Space Methods, John Wiley & Sons, 1969. Chapter 3, pp. 46–77. ISBN 0-471-55359-X.