Vector Space Methods VIII: Fenchel DualityTextbook
## Motivation
Convex duality converts an optimization problem over points into one over linear functionals. It supplies lower bounds, certificates of optimality, and alternative formulations whose geometry can be simpler than the primal problem. In §§7.8–7.12 of David G. Luenberger's [*Optimization by Vector Space Methods*](https://openlibrary.org/books/OL7612943M/Optimization_by_Vector_Space_Methods), this theory is developed for finite-valued convex and concave functions on convex subsets of a real normed space. The capstone is Fenchel duality with restricted domains and an attained continuous-linear-functional dual optimum. This mission preserves that functional-analytic setting rather than reducing the theorem to Euclidean space or silently extending the functions to the whole space.
## Setting
Let $X$ be a real normed space, let $C,D\subseteq X$ be nonempty convex sets, let $f:X\to\mathbb R$ be convex on $C$, and let $g:X\to\mathbb R$ be concave on $D$. For a continuous linear functional $\ell\in X^*$, the **restricted convex conjugate** and **restricted concave conjugate** are
$$
f_C^*(\ell)=\sup_{x\in C}\bigl(\ell(x)-f(x)\bigr),\qquad
g_D^*(\ell)=\inf_{x\in D}\bigl(\ell(x)-g(x)\bigr).
$$
The convex conjugate is admitted into $C^*$ only when its defining set is bounded above; the concave conjugate is admitted into $D^*$ only when its defining set is bounded below. Because $C$ and $D$ are nonempty and the functions are real-valued, these predicates exactly exclude the unwanted infinite endpoint. The Lean definitions use real `sSup` and `sInf`, with boundedness carried explicitly by theorem hypotheses.
The **restricted epigraph** of $(f,C)$ is the set of $(x,r)$ satisfying $x\in C$ and $f(x)\le r$; the restricted hypograph of $(g,D)$ reverses the scalar inequality. Luenberger's qualification requires a common point of the relative interiors of $C$ and $D$, represented by Mathlib's `intrinsicInterior`, and also requires ordinary nonempty interior of at least one of these two graph sets.
## Formalization targets
### Main goal: Fenchel duality
Assume the finite primal value $\mu$ is the greatest lower bound of
$$
\{f(x)-g(x):x\in C\cap D\}.
$$
Prove that some $\ell_0\in C^*\cap D^*$ attains
$$
\mu=g_D^*(\ell_0)-f_C^*(\ell_0)
=\max_{\ell\in C^*\cap D^*}
\bigl(g_D^*(\ell)-f_C^*(\ell)\bigr).
$$
If $x_0$ attains the primal infimum, also prove that $x_0$ attains both conjugate extrema at $\ell_0$: $f_C^*(\ell_0)=\ell_0(x_0)-f(x_0)$ and $g_D^*(\ell_0)=\ell_0(x_0)-g(x_0)$.
### Milestones
The mission records four source milestones. A local minimum of a convex function on its convex domain is global (§7.8, Proposition 1). Convexity of a restricted function is equivalent to convexity of its restricted epigraph (§7.8, Proposition 2). The finite-conjugate domain and the convex conjugate are convex (§7.10, Proposition 1). Finally, a closed restricted epigraph agrees pointwise on $C$ with the continuous-linear biconjugate (§7.10, Proposition 2). Together these statements expose the geometric and conjugacy interfaces on which the capstone depends without turning every paragraph of the chapter into a separate item.
## Significance
The theorem gives an attained dual certificate in an arbitrary real normed space. Equality of primal and dual values eliminates a duality gap, while attainment produces a specific functional that can certify an optimal primal point through simultaneous conjugate equality. The biconjugate milestone is independently useful: it expresses a closed convex function as a supremum of continuous affine minorants on its domain.
Formalizing this material adds a restricted-domain conjugacy API that is not supplied by the existing project artifact named `fenchelConjugate`. That artifact accepts finite-valued functions on a Euclidean space and has no independent convex domain or concave conjugate. Reusing it here would erase hypotheses that are central to Luenberger's theorem. The new definitions remain small, but their exact boundedness contracts make them reusable for later separation, minimax, and Lagrange-duality missions. The theorem is classical; the mission asks for a checked development faithful to the 1969 source and the current Mathlib representation of continuous dual spaces.
## Difficulty
The qualification is not the usual finite-dimensional slogan that relative interiors merely intersect. The source additionally demands that either the restricted epigraph or restricted hypograph have nonempty ordinary interior. Dropping that condition changes the theorem in infinite-dimensional spaces. Replacing `intrinsicInterior` by topological `interior` would also make valid lower-dimensional domains appear empty.
Extended values create another boundary. Real `sSup` and `sInf` are meaningful here only together with nonempty domains and the respective boundedness hypotheses. Treating their default values outside those hypotheses as genuine conjugates would admit false dual candidates. A finite-dimensional conjugate definition avoids neither issue and would prove only a special case. The biconjugate target must quantify over continuous linear functionals, not all algebraic linear maps, because closed epigraph separation is topological. Finally, the dual statement must include actual attainment; proving only equality with a supremum would omit a principal assertion of §7.12.
## Formalization scope
All primal functions are finite-valued real functions. Infinite conjugate values are represented by domain predicates—`BddAbove` for $f_C^*$ and `BddBelow` for $g_D^*$—rather than by changing the public conjugate codomain. The primal finiteness assumption is encoded by a real number $\mu$ together with `IsGLB`, which simultaneously rules out an empty feasible intersection and an infimum of $-\infty$. Epigraph pairs are ordered as $(x,r)$ to match Mathlib conventions, although Luenberger prints the scalar coordinate first.
The ambient space is normed but is not assumed finite-dimensional, reflexive, or complete. Both $C$ and $D$ are explicitly nonempty. The main theorem keeps the common intrinsic-interior condition and the disjunctive ordinary-interior condition verbatim. Contributions may develop separation lemmas, boundedness facts for restricted conjugates, or direct proofs of the milestone statements. A whole-space Euclidean specialization is welcome only as a corollary, not as a replacement for the root. The minimax theorem of §7.13 and extended-real lower-semicontinuous variants are outside this mission.
## Selected references
- David G. Luenberger, *Optimization by Vector Space Methods*, John Wiley & Sons, 1969, Chapter 7, §§7.8–7.12, pp. 191–202. [Open Library record](https://openlibrary.org/books/OL7612943M/Optimization_by_Vector_Space_Methods)
- R. Tyrrell Rockafellar, *Convex Analysis*, Princeton University Press, 1970. [DOI: 10.1515/9781400873173](https://doi.org/10.1515/9781400873173)
7 thms3 active usersReviewed
🏆Completed
Captain: wenxinzhang
Vector Space Methods X: Equality-Constrained Lagrange MultipliersTextbook
## 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](https://sites.science.oregonstate.edu/~show/old/142_Luenberger.pdf) 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
$$
f' + z₀ \circ H' = 0.
$$
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).
4 thms2 active usersReviewed
🏆Completed
Captain: wenxinzhang
Vector Space Methods V: Convex Separation and Distance DualityTextbook
## Motivation
Linear approximation is only one instance of distance minimization. Feasible sets in optimization are typically convex rather than subspaces, so a useful certificate must compare a target point with an entire convex set and must allow an affine offset. Chapter 5 of Luenberger's *Optimization by Vector Space Methods* builds this certificate through geometric forms of the Hahn--Banach theorem, supporting hyperplanes, and separation of convex sets. The resulting minimum-distance theorem expresses the distance from a point to a convex set as an optimal gap measured by a norm-bounded continuous linear functional ([Luenberger, §§5.12--5.13, pp. 130--137](https://sites.science.oregonstate.edu/~show/old/142_Luenberger.pdf)).
This mission advances the series from subspace annihilators to affine separation. It formalizes the Minkowski gauge used by the chapter, three progressively stronger separation statements, and a capstone distance-duality certificate. These results are standard infrastructure for constrained optimization: they turn a geometric exclusion or distance into a scalar inequality that can later become a multiplier or a dual bound.
## Setting
Let $X$ be a **real normed space** and $K\subseteq X$ a nonempty convex set. Convexity is represented by `Convex ℝ K`, and topological interior, closure, and infimum distance use Mathlib's `interior`, `closure`, and `Metric.infDist`. A **continuous affine separator** is described by a continuous linear functional $f:X\toL[\mathbb R]\mathbb R$ and a scalar level $c$. The inequality $f(k)\le c$ for all $k\in K$ places $K$ in one closed half-space.
When a convex set contains zero in its interior, its **Minkowski gauge** is the functional `gauge K`. The source characterizes it by nonnegativity, positive homogeneity, subadditivity, continuity, and the level sets
$$
\{x:g_K(x)\le 1\}=\overline K,
\qquad
\{x:g_K(x)<1\}=\operatorname{int}K.
$$
These properties are bundled into the first milestone, following Lemma 1 of §5.12 ([pp. 131--132](https://sites.science.oregonstate.edu/~show/old/142_Luenberger.pdf)).
For two convex sets $K_1,K_2$, **Eidelheit separation** means finding nonzero $f$ and $c$ with $f(x)\le c\le f(y)$ for $x\in K_1$ and $y\in K_2$. The source assumes that $K_1$ has nonempty interior and that its interior does not meet $K_2$. The Lean statement records the nonemptiness of $K_2$ explicitly, since otherwise nonzero separation is not forced.
## Formalization targets
### Gauge and geometric Hahn--Banach milestones
Formalize the six gauge properties above. Then, for a convex $K$ with nonempty interior and an affine subspace $V$ disjoint from that interior, produce $f\ne0$ and $c$ such that
$$
f(v)=c\quad(v\in V),
\qquad
f(k)<c\quad(k\in\operatorname{int}K).
$$
This is Mazur's geometric Hahn--Banach theorem as stated in §5.12, Theorem 1 ([p. 133](https://sites.science.oregonstate.edu/~show/old/142_Luenberger.pdf)).
### Supporting hyperplanes and convex-set separation
For $x\notin\operatorname{int}K$, formalize a nonzero functional satisfying $f(k)\le f(x)$ for all $k\in K$. Next formalize Eidelheit separation:
$$
f(x)\le c\le f(y)
\quad\text{for all }x\in K_1,\ y\in K_2.
$$
These are Theorems 2 and 3 of §5.12 ([pp. 133--134](https://sites.science.oregonstate.edu/~show/old/142_Luenberger.pdf)).
### Convex minimum-distance duality
Let $x_1$ have positive distance $d$ from $K$. Produce $f$ and a real upper-bound level $c$ with $\|f\|\le1$, $f(k)\le c$ on $K$, and
$$
f(x_1)-c=d.
$$
Every other feasible pair $(g,b)$ must satisfy $g(x_1)-b\le d$. If $x_0\in K$ realizes the distance, require $-f$ to align with $x_0-x_1$. This is the finite real certificate form of §5.13, Theorem 1 ([pp. 136--137](https://sites.science.oregonstate.edu/~show/old/142_Luenberger.pdf)).
## Significance
The capstone is an exact strong-duality statement for distance to a convex set. A feasible pair $(g,b)$ yields a certified lower bound on the distance, and the distinguished pair reaches the primal value. Unlike a nearest-point characterization, it remains meaningful when $K$ is not closed and no minimizing point exists. The conditional alignment clause identifies the equality case when attainment is available.
Formalizing the chapter's progression creates more than one isolated equality. The gauge package links convex geometry to sublinear analysis; Mazur separation handles affine constraints; the supporting-hyperplane and Eidelheit statements provide reusable interfaces for later multiplier rules. The results are known and proved in the 1969 text; the mission's contribution is a coherent machine-checked Lean layer that preserves the source hypotheses and can support later chapters on duality and optimization.
## Difficulty
A direct reuse of subspace distance duality is insufficient because a general convex set is neither closed under subtraction nor described by an annihilator. An affine level $c$ is unavoidable. The common shorthand $\sup_{k\in K} f(k)$ introduces a second problem: $K$ need not be bounded, so a real-valued supremum is not available for an arbitrary functional. The capstone therefore quantifies over a real upper bound $c$ and asserts its optimality through a universal inequality; this records the same finite support value without imposing boundedness absent from the source.
Topological hypotheses also differ across the milestones. Separation uses nonempty interior, whereas the final distance theorem only assumes convexity, nonemptiness, and positive distance. Replacing positive distance by mere exclusion $x_1\notin K$ would be invalid for a nonclosed set. Similarly, requiring closure or compactness would make formalization easier but would lose the theorem's intended infinite-dimensional scope.
## Formalization scope
The mission is restricted to real normed spaces. Sets use `Set X`; affine varieties use `AffineSubspace ℝ X`; separators use `ContinuousLinearMap`. The gauge is Mathlib's existing `gauge`, so no competing definition is introduced. The bundled gauge milestone deliberately includes both level-set identities as well as continuity, positive homogeneity for positive real scalars, subadditivity, and nonnegativity.
The Eidelheit theorem includes `K₂.Nonempty`, an assumption used implicitly by the source's separating conclusion. The capstone includes `K.Nonempty` and `0 < Metric.infDist x₁ K`; it does not assume closedness, boundedness, compactness, or attainment. Its pair $(f,c)$ represents a finite support level, and the universal comparison over all feasible $(g,b)$ rules out a weakened statement in which an arbitrarily loose upper bound could trivialize existence. The optional nearest-point clause uses the exact equality $\|x_0-x_1\|=d$ and fixes the sign of alignment. Contributions may add reusable lemmas on gauges, interiors, affine subspaces, or support bounds, but the public results should remain independent of finite-dimensionality and completeness.
## Selected references
- David G. Luenberger, *Optimization by Vector Space Methods*, John Wiley & Sons, 1969, Chapter 5, §§5.11--5.13, pp. 127--137. [Public scan](https://sites.science.oregonstate.edu/~show/old/142_Luenberger.pdf).
5 thms2 active usersReviewed
🏆Completed
Captain: wenxinzhang
Vector Space Methods VI: Pseudoinverse OperatorsTextbook
## 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](https://sites.science.oregonstate.edu/~show/old/142_Luenberger.pdf)).
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](https://sites.science.oregonstate.edu/~show/old/142_Luenberger.pdf)). Closed range gives the range-kernel identity
$$
\operatorname{range}(A^\dagger)=\ker(A)^\perp,
$$
the Hilbert-space specialization of the closed range theorem used in the chapter ([§6.6, Theorem 2, p. 156](https://sites.science.oregonstate.edu/~show/old/142_Luenberger.pdf)).
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](https://sites.science.oregonstate.edu/~show/old/142_Luenberger.pdf)).
## Formalization targets
### Adjoint and closed-range milestones
Formalize $\|A^\dagger\|=\|A\|$. Under closed range, formalize
$$
\operatorname{range}(A^\dagger)=\ker(A)^\perp.
$$
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
$$
x\text{ minimizes }\|y-Ax\|
\quad\Longleftrightarrow\quad
A^\dagger A x=A^\dagger y,
$$
as in §6.9, Theorem 1 ([p. 160](https://sites.science.oregonstate.edu/~show/old/142_Luenberger.pdf)). 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](https://sites.science.oregonstate.edu/~show/old/142_Luenberger.pdf)). 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
$$
BAB=B,\qquad ABA=A,\qquad (BA)^\dagger=BA.
$$
Also produce pseudoinverses $C$ of $A^\dagger A$ and $D$ of $AA^\dagger$ satisfying
$$
B=CA^\dagger,
\qquad
B=A^\dagger D.
$$
Together with the continuous-linear-map type of $B$, these clauses encode all nine items of §6.11, Proposition 1 ([p. 165](https://sites.science.oregonstate.edu/~show/old/142_Luenberger.pdf)).
## 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](https://sites.science.oregonstate.edu/~show/old/142_Luenberger.pdf).
7 thms2 active usersReviewed
🏆Completed
Captain: wenxinzhang
Vector Space Methods IV: Minimum-Distance DualityTextbook
## 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](https://sites.science.oregonstate.edu/~show/old/142_Luenberger.pdf)).
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
$$
d(x,M)=\inf_{m\in M}\|x-m\|.
$$
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](https://sites.science.oregonstate.edu/~show/old/142_Luenberger.pdf)).
## Formalization targets
### Norm-preserving extension and norming functionals
For a continuous functional $f$ on $M$, formalize an extension $F$ satisfying
$$
F|_M=f,\qquad \|F\|=\|f\|.
$$
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](https://sites.science.oregonstate.edu/~show/old/142_Luenberger.pdf)).
### Closed-subspace double annihilator
For closed $M$, formalize
$$
\{x\in X: \forall f,\ f|_M=0 \Rightarrow f(x)=0\}=M.
$$
This is the concrete set-valued form of Theorem 1 in §5.7 ([p. 118](https://sites.science.oregonstate.edu/~show/old/142_Luenberger.pdf)).
### Minimum-distance duality
For arbitrary $M$ and $x$, produce one functional $f$ with $\|f\|\le 1$, $f|_M=0$, and
$$
f(x)=d(x,M),\qquad
g(x)\le d(x,M)
$$
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
$$
f(x-m_0)=\|f\|\,\|x-m_0\|.
$$
This packages both parts of the minimum-distance theorem in §5.8 ([Theorem 1, pp. 119--120](https://sites.science.oregonstate.edu/~show/old/142_Luenberger.pdf)).
## 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](https://sites.science.oregonstate.edu/~show/old/142_Luenberger.pdf).
4 thms2 active usersReviewed
Captain: ShouqiaoWang
Zhang–Si–Si: Corrected Resonant Almost-Periodic Poincaré–Treshchev PersistenceResearch Paper
## Motivation
The classical persistence problem asks which invariant tori of an integrable Hamiltonian survive a small perturbation. A resonance makes some internal angular frequencies vanish, and an **almost-periodic perturbation** introduces infinitely many additional forcing frequencies. Zhang, Si, and Si state a Poincaré–Treshchev persistence theorem for this combined regime: most lower-dimensional resonant tori associated with nondegenerate relative equilibria persist as infinite-dimensional invariant tori [in Theorem 2.7](https://doi.org/10.3934/dcds.2026043). The formal mission targets that headline result in corrected form. It retains the paper’s nonresonance, spatial-shell, and averaged-critical-point hypotheses, while making explicit the full frequency twist and reduced-frequency parameter chart used later in the paper but absent from the printed theorem statement.
## Setting
Let $n,m>0$ and $d=n+m$. The internal variables are $x\in\mathbb T^d$ and $y\in G\subset\mathbb R^d$, where $G$ is bounded and closed. The external forcing angles and their conjugate actions are $\theta\in\mathbb T^{\mathbb Z}$ and $J\in\ell^1(\mathbb Z;\mathbb R)$. The **suspended Hamiltonian** is
$$
\mathcal H_\epsilon(\theta,J,x,y)=
\sum_{j\in\mathbb Z}\omega_jJ_j+N(y)+\epsilon P(\theta,x,y,\epsilon).
$$
Here $N$ is real analytic near $G$. A primitive rank-$m$ resonance lattice is represented by an integer matrix $K_0=(K_1,K_2)$ with $\det K_0=1$, where the last $m$ columns generate the lattice. The adapted angles are $(\psi,\phi)=K_0^{\mathsf T}x$, with $\psi\in\mathbb T^n$ and $\phi\in\mathbb T^m$. Writing $\nabla N$ for the actual derivative of $N$, define
$$
O(g,G)=\{y\in G:K_2^{\mathsf T}\nabla N(y)=0\},
\qquad \Omega(y)=K_1^{\mathsf T}\nabla N(y).
$$
The **averaged potential** $h_0(\phi,y)$ is the zero external and zero $\psi$ Fourier coefficient of $P$ at $\epsilon=0$. A pair $(\phi,y)$ is associated and nondegenerate when
$$
\nabla_\phi h_0(\phi,y)=0,
\qquad \det D_\phi^2h_0(\phi,y)\ne0.
$$
Let $O_0$ be the subset of $O(g,G)$ admitting such a $\phi$, let $\Omega_0=\Omega(O_0)$, and trim in reduced-frequency coordinates:
$$
\Omega_\xi=\{\eta\in\Omega_0:\operatorname{dist}(\eta,\partial\Omega_0)\ge\xi\},
\qquad O_\xi=O_0\cap\Omega^{-1}(\Omega_\xi).
$$
The perturbation has the paper’s **spatial-shell Fourier expansion** over finite shells $A$ in a spatial structure $\mathcal S$. With
$[A]=1+\sum_{j\in A}\log^{\varrho}(1+|j|)$ for $\varrho>2$, each shell has a uniform analytic Fourier bound $B_A$, and $\sum_AB_Ae^{s[A]}<\infty$ for some $s>0$. Every nonzero admissible finite external mode $k$ satisfies
$$
|\langle k,\omega\rangle|\ge
\frac{\gamma}{\Delta([[k]])\Delta(|k|_1)},
$$
where $\gamma>0$, $[[k]]$ is the minimum shell weight containing its support, and $\Delta$ is a nondecreasing approximation function with $\Delta(0)=1$, $\log\Delta(t)/t\downarrow0$, and $\int_0^\infty\log\Delta(t)t^{-2}\,dt<\infty$.
## Target
Assume that $O_0$ is nonempty. On every sufficiently small trim $O_\xi$, require compactness and positive $n$-dimensional measure in the $\Omega$ chart, injectivity of $D(\nabla N)(y)$, an analytic lower-Lipschitz diffeomorphism $\Omega:O_\xi\to\Omega_\xi$, and nondegeneracy of every averaged critical point retained by the conclusion. Then, for every $0<\xi\le\xi_*$, there are $0<\epsilon_0\le1$, a rate $c(\epsilon)\to0$ as $\epsilon\downarrow0$, and closed measurable nonempty sets $\Lambda_\epsilon\subset O_\xi$ for $0<\epsilon\le\epsilon_0$ such that
$$
\operatorname{vol}_n\bigl(\Omega(O_\xi\setminus\Lambda_\epsilon)\bigr)
\longrightarrow0\qquad(\epsilon\downarrow0).
$$
For every $y\in\Lambda_\epsilon$ and every associated nondegenerate $\phi$, construct a topological embedding
$$
\iota_{\epsilon,y,\phi}:\mathbb T^{\mathbb Z}\times\mathbb T^n
\longrightarrow
(\mathbb T^{\mathbb Z}\times\ell^1)\times
(\mathbb T^d\times\mathbb R^d)
$$
that is analytic almost periodic with the same shell structure, is the image of the standard resonant torus under a local canonical transformation, is $c(\epsilon)$-close to that torus, and is invariant under $\mathcal H_\epsilon$ with rotation vector $(\omega,\Omega(y))$.
## Significance
The result combines three features that are usually separated: a positive-rank internal resonance, an infinite external frequency vector, and persistence for an asymptotically full-measure parameter set. It identifies the surviving object in the full suspended phase, including the external actions, rather than only in the finite internal fibre. The paper contains a proof of its printed theorem; the mission’s open work is a Lean proof of the corrected target. The correction exposes the parameter twist and chart assumptions on which the reduction and measure assertion depend, so a completed formalization would distinguish the theorem’s stated content from hypotheses needed to make that content mathematically controlled.
## Difficulty
Finite-dimensional Diophantine notation does not control infinitely many external modes: admissibility, support weights, and the decay of $\Delta$ must interact without leaving an empty mode class. Resonance also removes $m$ internal frequencies and replaces the original parameter set by a lower-dimensional surface. Its ambient Euclidean boundary is therefore unsuitable for a positive trim, and ordinary ambient volume is unsuitable for the majority statement. Finally, persistence must be expressed simultaneously as an invariant solution of the actual Hamilton equations, an analytic almost-periodic embedding, and a canonical equivalence in the suspended phase; any one of these conditions alone admits objects that do not express the theorem.
## Formalization scope
The Lean representation uses finitely supported integer external modes, a covering spatial structure, the literal shell-indexed norm, complex-neighborhood coefficient analyticity, and a separate absolute-summability guard for every infinite Fourier sum. Unit modes are provably admissible. The averaged potential, its gradient and Hessian, the internal frequency $\nabla N$, the resonant set, and the reduced-frequency map are transparent definitions. Nonemptiness of $O_0$, positive volume of every allowed $\Omega_\xi$, and nonempty $\Lambda_\epsilon$ rule out empty-set and zero-measure trivializations.
The formal target strengthens the printed assumptions only where the source’s reduction requires missing control: $D(\nabla N)$ is injective on the retained trim, and $\Omega$ is an analytic diffeomorphism there with a uniform lower Lipschitz bound. The boundary distance and excluded volume are both taken in the $n$-dimensional reduced-frequency chart. The word “Cantor” is represented by closedness, measurability, nonemptiness, and asymptotically full measure; perfectness and total disconnectedness are not additional targets.
The torus lives in a genuine $\ell^1$ external-action space. Its action component has one weighted-$\ell^1$-valued shell expansion, and the Hamiltonian pairing and external action velocity carry convergence guards. A local conjugacy is a homeomorphism between open neighborhoods, fixes $\theta$, is differentiable along all $\ell^1$ action directions and finitely supported external-angle directions, and preserves $\sum_jd\theta_j\wedge dJ_j+\sum_i dx_i\wedge dy_i$ on those cylinder directions. Reusable contributions include spatial-shell Fourier classes, approximation functions, reduced-manifold measure interfaces, weighted infinite canonical forms, and coordinatewise Hamiltonian invariance.
## Selected references
- Yuan Zhang, Wen Si, and Jianguo Si, *Poincaré–Treshchev Mechanism in Integrable Hamiltonian Systems Under Almost-Periodic Perturbations*, Discrete and Continuous Dynamical Systems **52** (2026), 32–69. [DOI: 10.3934/dcds.2026043](https://doi.org/10.3934/dcds.2026043). Main result: Theorem 2.7, journal p. 39 (PDF p. 8); spatial and nonresonance definitions: Definitions 2.2–2.4 and equations (5)–(7), journal pp. 35–38 (PDF pp. 4–7); reduction exposing the additional twist and parameter-change requirements: Lemma 3.2, journal pp. 41–43 (PDF pp. 10–12).
2 thms1 active userReviewed
🏆Completed
Captain: Shuze Chen
Vector Space Methods IV: Hahn–Banach and Minimum Norm DualityTextbook
## 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.
17 thms1 active userReviewed
🏆Completed
Captain: Shuze Chen
Vector Space Methods II: Gauss–Markov EstimationTextbook
## 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).
8 thms1 active userReviewed
🏆Completed
Captain: Shuze Chen
Vector Space Methods I: Minimum Norm Problems in Hilbert SpaceTextbook
## 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.