Vector Space Methods XIII: Conjugate-Gradient ConvergenceTextbook
## Motivation
The [conjugate-gradient method in Luenberger's Chapter 10](https://sites.science.oregonstate.edu/~show/old/142_Luenberger.pdf) is one of the most enduring consequences of Hilbert-space geometry in numerical optimization. For a bounded self-adjoint coercive operator, it solves the quadratic first-order equation `Q x = b` using only operator applications, inner products, and a short recurrence. Luenberger develops the method from steepest descent and conjugate directions, then proves convergence in a general real Hilbert space rather than only for finite matrices. This mission formalizes that full setting. It also repairs a practical omission in the printed recursion: division formulas are undefined after exact convergence, so the formal algorithm explicitly stops and stutters once its search direction is zero.
## Setting
Let `H` be a **complete real inner-product space** and `Q : H →L[ℝ] H` a bounded **self-adjoint operator**. Constants `m` and `M` satisfy `0 < m ≤ M` and
$$
m\lVert x\rVert^2 \le \langle x,Qx\rangle
\le M\lVert x\rVert^2
$$
for every `x`. The first inequality is **coercivity**; together with self-adjointness it supplies the positive `Q`-energy. For a right-hand side `b` and initial point `x₀`, the initial residual and direction are both `b - Q x₀`. A **conjugate-gradient state** records the current iterate, residual, and direction. If the direction is nonzero, the next state uses Luenberger's `alpha` and `beta` ratios. If the direction is zero, `conjugateGradientStep` returns the same state, so every natural-number iterate is total and all denominators occur only on the active branch.
## Formalization targets
The root theorem `VectorSpaceOpt.conjugate_gradient_converges` states that there is a unique `xStar` satisfying `Q xStar = b` and that the iterate component of the guarded conjugate-gradient state tends to `xStar` in norm. Four milestones provide reusable structure. `coercive_selfadjoint_bijective` establishes existence and uniqueness for `Q x = b` from bounded self-adjoint coercivity. `conjugate_directions_converge` formalizes §10.6, Theorem 1: a complete sequence of nonzero pairwise `Q`-orthogonal directions produces residuals orthogonal to every earlier direction and iterates converging to the solution. `cg_directions_conjugate_until_stop` records the §10.8 invariants only before the explicit stopping time. `cg_energy_contraction` captures the uniform energy reduction factor derived from the bounds `m` and `M`.
The total algorithm is represented by `conjugateGradientIterate`, and its error functional is
$$
E(x)=\langle x-x^*,Q(x-x^*)\rangle.
$$
These definitions are proposed as mission-owned reusable objects in the shared `VectorSpaceOpt` namespace.
## Significance
The mission gives a coordinate-free verification target for an algorithm usually presented through arrays and matrices. Its theorem applies directly to finite-dimensional symmetric positive-definite systems but also retains Luenberger's infinite-dimensional perspective. The guarded recursion is suitable for later executable specializations and makes exact termination a first-class semantic event. The coercivity and conjugate-directions milestones can be reused for Galerkin methods, preconditioned variants, and other Krylov algorithms, while the energy estimate provides a natural connection to condition-number convergence rates.
Unlike a matrix-only formalization, the Hilbert-space theorem cleanly separates the geometric reason for convergence from any storage representation. It therefore complements Mathlib's existing operator and orthogonality libraries and can serve as a specification against which finite implementations are later verified.
It also preserves the book's unifying theme: optimization algorithms arise from the geometry of carefully chosen inner products rather than from coordinate manipulation alone.
## Difficulty
The difficulty is medium to high. Algebraic invariants of the three-term recurrence involve several interacting orthogonality relations and require strict control of nonzero denominators. Infinite-dimensional convergence additionally uses density of the closed span of directions and comparison of the `Q`-energy with the ambient norm. The theorem must move between self-adjoint continuous linear maps, scalar inner products, filters on sequences, and function iteration. Exact termination creates a case split that informal accounts routinely ignore; the formal statement must show that the zero-direction branch is stable and already represents the solution.
## Formalization scope
The proposal follows §10.6 and §10.8, pp. 291–296, and uses Chapter 10, Problem 10 on p. 309 for the coercive-invertibility dependency. All assumptions on `Q`, `m`, and `M` that §10.8 inherits from the preceding sections are repeated explicitly. The conjugate-directions milestone explicitly assumes every direction is nonzero and that the closed span of the directions is the whole Hilbert space. The conjugate-gradient invariants are asserted only for iterations before a zero direction occurs. Once it occurs, the state stutters by definition; the proposal never relies on Lean's totalized value for `0 / 0`.
Luenberger's §10.7, Theorem 1 is not included as a literal milestone. As printed, its orthogonalization-of-moments statement omits self-adjointness of the auxiliary operator relative to the `Q` inner product and omits the linear-independence/nonbreakdown conditions needed to keep denominators nonzero. The mission instead isolates the `Q`-conjugacy invariant directly from §10.8. It does not claim finite-dimensional termination within `dim H` steps, floating-point stability, preconditioning, a sharp Chebyshev condition-number rate, or computability of equality tests on arbitrary Hilbert spaces.
## Selected references
- David G. Luenberger, *Optimization by Vector Space Methods*, Wiley, 1969, Chapter 10, §10.6, Theorem 1, pp. 291–292; §10.8, Theorem 1, pp. 294–296; Problem 10, p. 309. Scan: https://sites.science.oregonstate.edu/~show/old/142_Luenberger.pdf
- Lean community, *Mathlib documentation*, continuously updated: https://leanprover-community.github.io/mathlib4_docs/ (real inner-product spaces, continuous linear maps, coercivity, closed spans, orthogonality, and filter convergence).
Vector Space Methods XIV: Quadratic Penalty ConvergenceTextbook
## Motivation
[Quadratic exterior penalties in Luenberger's §10.11](https://sites.science.oregonstate.edu/~show/old/142_Luenberger.pdf) replace a constrained problem by a sequence of unconstrained minimizations. The method is simple enough to state in a few lines, yet Luenberger's convergence theorem is strikingly general: no convexity, differentiability, or convergence of the full minimizer sequence is required. If penalty weights increase to infinity and a subsequence of exact penalty minimizers converges, lower semicontinuity alone makes its limit feasible and optimal. This mission isolates that robust primal convergence result as a tractable companion to the more analytic conjugate-gradient and optimal-control missions. It offers a clean formalization target with direct relevance to nonlinear programming and approximation schemes.
## Setting
Let `X` be a **topological space**, `f : X → ℝ`, and `G : X → (Fin p → ℝ)`. **Feasibility** means `G x i ≤ 0` for every component. Define the **positive part** componentwise and the **squared violation** by
$$
G_i^+(x)=\max(0,G_i(x)), \qquad
v(x)=\sum_i (G_i^+(x))^2.
$$
For a positive weight `K`, the penalty objective is `f x + K * v x`. A sequence `K n` is positive, nondecreasing, and tends to `+∞`. The constrained problem is assumed to have a minimizer `xStar`, and for each `n` an exact global minimizer `x n` of the corresponding penalty objective is supplied. A limit point is represented explicitly by a strictly increasing index map `phi` for which `x ∘ phi` tends to `x₀`.
## Formalization targets
The root `VectorSpaceOpt.quadratic_penalty_cluster_point_converges` formalizes §10.11, Theorem 1. Assuming lower semicontinuity of `f` and `v`, it concludes that every stated subsequential limit `x₀` is feasible, has the same objective value as `xStar`, and globally minimizes `f` over the feasible set.
Three milestones split the exact source content into reusable statements. `quadratic_penalty_basic_estimates` is §10.11, Lemma 1: the attained penalty values are nondecreasing, are bounded above by `f xStar`, and the stronger weighted violation `K n * v (x n)` tends to zero. `penalty_cluster_point_feasible` combines convergence of violations with lower semicontinuity at a subsequential limit to recover all component inequalities. `penalty_cluster_point_optimal` combines lower semicontinuity of `f`, the uniform upper bound `f (x n) ≤ f xStar`, feasibility of the limit, and optimality of `xStar` to identify the limiting objective value and global constrained optimality.
## Significance
The theorem captures the essential consistency guarantee behind one of the most widely used constraint-handling methods. Its assumptions separate optimization existence from convergence: minimizers of each auxiliary problem and at least one cluster point are assumed, while the theorem identifies what any such cluster point must be. The componentwise positive-part and violation definitions are reusable for augmented Lagrangians, exact penalties, barrier comparisons, and finite inequality systems. The basic-estimates lemma is particularly useful because it requires neither topology nor continuity and exposes a quantitative fact stronger than mere feasibility residual convergence.
Because the proof target is stated over an arbitrary topological space, the mission also clarifies which parts of penalty convergence are genuinely metric and which depend only on order, finite nonnegative sums, and lower semicontinuity. This abstraction is faithful to the source's vector-space viewpoint.
## Difficulty
The mission has moderate difficulty and relatively low infrastructure risk. The main analytic interfaces are lower semicontinuity along a convergent subsequence and real filter convergence to both zero and infinity. The basic estimates require reasoning simultaneously about minimizers for changing objectives, monotonicity of the weights, and the asymptotic product `K n * v (x n)`. The cluster-point theorem must extract componentwise feasibility from a finite sum of nonnegative squares without assuming continuity of `G`. Lean's `IsMinOn` does not itself assert membership in the feasible set, so feasibility of the known constrained minimizer is included separately rather than hidden in prose.
## Formalization scope
The proposal covers the primal part of §10.11: Lemma 1 on p. 305 and Theorem 1 on p. 306. It makes “limit point” precise through a strictly monotone subsequence, avoiding any assumption that the full sequence converges. The weight sequence may have repeated values because the source only needs it to be nondecreasing, but every weight is positive and the sequence tends to `atTop`. Lower semicontinuity is required for `f` and the composite violation `v`, exactly as in the book; continuity or componentwise lower semicontinuity of `G` is not substituted. Existence of `xStar` and of every penalty minimizer is assumed rather than derived from compactness or coercivity.
The mission does not include §10.11, Lemma 2 or Theorem 2 on dual multipliers. Those results add convexity and continuity assumptions and naturally require careful treatment of an extended-real dual functional. It also does not address approximate minimizers, rates, boundedness of the sequence, existence of cluster points, equality constraints beyond their encoding as paired inequalities, or finite exactness. Keeping those extensions separate preserves the unusually weak hypotheses and clear conclusion of the cited primal theorem.
## Selected references
- David G. Luenberger, *Optimization by Vector Space Methods*, Wiley, 1969, Chapter 10, §10.11, Lemma 1 and Theorem 1, pp. 305–306. Scan: https://sites.science.oregonstate.edu/~show/old/142_Luenberger.pdf
- Lean community, *Mathlib documentation*, continuously updated: https://leanprover-community.github.io/mathlib4_docs/ (lower semicontinuity, finite sums, `Fin`-indexed vectors, subsequences, global minima on sets, and filter convergence).
Vector Space Methods XI: Generalized Kuhn–Tucker ConditionsTextbook
## Motivation
[Luenberger's generalized Kuhn–Tucker theorem](https://sites.science.oregonstate.edu/~show/old/142_Luenberger.pdf) turns inequality-constrained optimization into an order-theoretic statement on normed vector spaces. Instead of listing scalar inequalities, it lets a convex cone `P` define positivity in a target space `Z`; one condition `G x ≤ₚ 0` can therefore represent finite, infinite, or function-valued families of constraints. At a regular local minimizer, a positive continuous functional on `Z` simultaneously provides stationarity and complementary slackness. This mission is a separate capstone because the cone-separation argument is conceptually independent of the equality-constrained theorem and because Mathlib currently lacks this general cone-valued KKT result.
## Setting
Let `X` and `Z` be **real normed spaces**, `P : ConvexCone ℝ Z`, `f : X → ℝ`, and `G : X → Z`. The **cone order** is `coneLE P z₁ z₂`, meaning `z₂ - z₁ ∈ P`; strict inequality uses the topological interior of the **convex cone** `P`. The cone is assumed to have nonempty interior. At `x₀`, both `f` and `G` possess linear **Gâteaux derivatives** represented by continuous linear maps `f'` and `G'`. The source's **regularity condition** requires feasibility together with a direction `h` for which `G x₀ + G' h` lies strictly below zero in the cone order.
The point `x₀` is a local, not global, minimizer of `f` on `{x | coneLE P (G x) 0}`. The resulting multiplier `z₀ : Z →L[ℝ] ℝ` is positive on `P`. This mission reuses the previously published `VectorSpaceOpt.coneLE` and `VectorSpaceOpt.dualPositive` definitions from the global Lagrange-duality mission; it deliberately does not introduce equivalent duplicate constants.
## Formalization targets
The root theorem is `VectorSpaceOpt.generalized_kuhn_tucker`, corresponding to §9.4, Theorem 1. It produces `z₀` such that
$$
z₀(P) \subseteq [0,\infty), \qquad
f' + z₀ \circ G' = 0, \qquad
z₀(Gx₀)=0.
$$
Three milestones expose the exact logical interfaces of the source theorem. `kkt_no_strict_linearized_descent` says local minimality and feasibility exclude a direction that strictly decreases `f'` while making the linearized constraint strictly feasible. `kkt_linearized_separator` packages the separation step: nonintersection of the strict descent system, cone regularity, and nonempty cone interior yield a positive continuous multiplier with both KKT conclusions. `kkt_complementary_slackness` isolates the algebraic extraction of stationarity and complementarity from the separating inequality valid for every direction. The items use the shared namespace `VectorSpaceOpt` and list dependencies in this order.
## Significance
This mission generalizes the standard finite-dimensional KKT rule without choosing coordinates or reducing cone constraints to components. It provides a reusable basis for semi-infinite optimization, ordered Banach-space problems, and state constraints expressed in function spaces. The multiplier positivity predicate connects directly to the dual cone used in the earlier global duality mission, while complementarity links local differential theory to primal–dual optimality. A successful formalization would also close a conspicuous gap in general-purpose optimization infrastructure: cone-valued KKT conditions are referenced often but rarely available as a theorem with all topological hypotheses exposed.
The statement is also a useful stress test for compositional textbook formalization. It deliberately shares its order and dual-positivity vocabulary with an earlier mission, so subsequent results can consume one stable API instead of translating among locally invented conventions.
## Difficulty
The main challenge is functional-analytic separation. The relevant convex set mixes objective descent and strict cone feasibility, and the separating functional must be normalized so that its objective component is nonzero. Regularity rules out an abnormal separator and nonempty cone interior controls the sign of the `Z` component. The Gâteaux assumptions are directional rather than full Fréchet differentiability, so local contradiction statements must use only the one-dimensional expansions actually supplied. Lean also requires careful sign discipline: feasibility is encoded as `0 - G x ∈ P`, while positivity is evaluated on elements of `P`. Small convention errors would reverse the dual cone or the stationarity equation.
## Formalization scope
The source says that `X` is a vector space, but its definition of Gâteaux differentiation and its local perturbation argument require a norm and topology. The proposal therefore makes both `X` and `Z` normed real spaces and represents derivatives by continuous linear maps. It keeps Luenberger's cone assumptions: convexity and nonempty interior are explicit; pointedness and closedness are not added because the printed separation argument does not need them. The optimality hypothesis is faithfully local through `IsLocalMinOn`. Feasibility is included in `IsConeRegularAt`, and the no-descent milestone states it separately.
This is proposed as “Vector Space Methods XI” and depends on the earlier global Lagrange-duality mission, proposed as “Vector Space Methods IX,” for `coneLE` and `dualPositive`; the missions should be submitted in numerical order. The proposal does not cover equality constraints, second-order KKT conditions, multiplier uniqueness, constraint qualifications other than Luenberger's strict linearized feasibility condition, or sufficient conditions based on convexity. It also does not specialize to a finite list of scalar inequalities. These omissions preserve the exact role and scale of §9.4.
## Selected references
- David G. Luenberger, *Optimization by Vector Space Methods*, Wiley, 1969, Chapter 9, §9.4, regular-point definition and Theorem 1, pp. 248–250. Scan: https://sites.science.oregonstate.edu/~show/old/142_Luenberger.pdf
- Lean community, *Mathlib documentation*, continuously updated: https://leanprover-community.github.io/mathlib4_docs/ (convex cones, continuous linear functionals, topological interiors, differential calculus, local extrema, and geometric separation).
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).
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).
Vector Space Methods IX: Global Lagrange DualityTextbook
## Motivation
Many convex programs impose inequalities valued in a vector space: componentwise inequalities, positive-semidefinite constraints, and families of ordered resource constraints are all instances of one cone order. Chapter 8 of David G. Luenberger's [*Optimization by Vector Space Methods*](https://openlibrary.org/books/OL7612943M/Optimization_by_Vector_Space_Methods) develops a global theory for this setting. A perturbation of the constraint produces a convex value function, continuous linear functionals positive on the ordering cone become Lagrange multipliers, and a strict-feasibility condition yields an attained dual optimum. This mission formalizes the progression in §§8.2–8.6, culminating in the book's Lagrange Duality Theorem.
## Setting
Let $X$ and $Z$ be real normed spaces, let $\Omega\subseteq X$ be a nonempty convex set, and let $P\subseteq Z$ be a **convex cone**. The cone induces the relation
$$
z_1\le_P z_2\quad\Longleftrightarrow\quad z_2-z_1\in P.
$$
A continuous linear functional $z^*\in Z^*$ is **dual-positive** when $z^*(p)\ge0$ for every $p\in P$. A map $G:X\to Z$ is **cone-convex on $\Omega$** when its value at a convex combination is below the corresponding convex combination of its values in this cone order. The primal program is
$$
\mu=\inf\{f(x):x\in\Omega,\ G(x)\le_P0\},
$$
where $f$ is real-valued and convex on $\Omega$.
For a multiplier $z^*$, the **Lagrangian** and its possibly infinite dual value are
$$
L(x,z^*)=f(x)+z^*(G(x)),\qquad
\phi(z^*)=\inf_{x\in\Omega}L(x,z^*).
$$
The perturbed primal value $\omega(z)$ replaces the zero right-hand side by $G(x)\le_P z$. Lean represents $\omega$ and $\phi$ in `EReal`, so infeasible perturbations have value $+\infty$ and objectives unbounded below can have value $-\infty$ without arbitrary defaults.
## Formalization targets
### Main goal: Lagrange duality
Assume $P$ has nonempty interior, the primal value $\mu$ is finite, and there is a **strictly feasible point** $x_s\in\Omega$ with
$$
-G(x_s)\in\operatorname{int}P.
$$
Prove that a dual-positive $z_0^*$ exists and attains
$$
\mu=\phi(z_0^*)=
\max_{z^*\ \text{dual-positive}}\phi(z^*).
$$
If $x_0$ attains the primal infimum, also prove complementarity $z_0^*(G(x_0))=0$ and that $x_0$ minimizes $L(\,·\,,z_0^*)$ over $\Omega$.
### Milestones
Five source milestones delimit the reusable theory. A closed convex cone is recovered from all dual-positive inequalities (§8.2, Proposition 1). The finite-height epigraph of the extended perturbation value is convex, and that value is antitone in the cone order (§8.3, Propositions 1–2). A Lagrangian saddle point is sufficient for primal feasibility and optimality when the cone is closed (§8.4, Theorem 2). Finally, multipliers for two perturbed right-hand sides bound the change in optimal objective value from both sides (§8.5, Theorem 1). The root then states §8.6, Theorem 1 rather than duplicating the equivalent multiplier theorem from §8.3.
## Significance
The capstone provides both equality of optimal values and an attained multiplier. It applies to a single vector inequality, so finite systems of scalar inequalities and matrix-cone constraints fit the same statement once their ordering cones are supplied. Complementarity and Lagrangian minimization turn a primal optimizer and multiplier into a certificate. The sensitivity milestone additionally gives quantitative information about how the optimum changes when the constraint right-hand side moves.
Formalization produces a reusable cone-order layer independent of coordinate choices. `coneLE`, `dualPositive`, and `ConeConvexOn` can support later Kuhn–Tucker, vector optimization, and conic programming developments. The `EReal` value functions preserve infeasibility and unboundedness, two cases that a real-valued `sInf` encoding would collapse. This is a formalization mission for a classical theorem, not a claim that the underlying duality result is open.
## Difficulty
The theorem's strict-feasibility condition is load-bearing. Feasibility $-G(x)\in P$ cannot replace interior feasibility, and nonempty interior of $P$ alone does not supply a Slater point. Equality constraints also cannot be converted into pairs of inequalities while retaining strict feasibility; Luenberger explicitly warns about this after the theorem.
The cone assumptions differ across milestones. The main strong-duality theorem does not require $P$ to be closed or pointed, whereas the bipolar and saddle-sufficiency statements require closedness. Using Mathlib's stronger `ProperCone` everywhere would silently add both topological and order hypotheses and shrink the theorem. Another tempting simplification is to make both value functions real. That loses the empty feasible set and unbounded dual subproblem, precisely the boundary cases used when comparing perturbations. The saddle inequalities must also have the correct orientation: the multiplier coordinate is maximized and the primal coordinate is minimized.
## Formalization scope
The mission uses `ConvexCone ℝ Z` with a custom induced relation; it deliberately does not assume a lattice order on $Z$. Multipliers are continuous linear maps $Z\to\mathbb R$. The root assumes a real finite optimum through `IsGLB` and a real witness $\mu$, while `lagrangeDualValue` and `perturbationValue` retain `EReal` codomains. The strict condition is written as membership of $-G(x_s)$ in `interior P`, exactly matching $G(x_s)<_P0$.
No finite-dimensionality, reflexivity, completeness, closedness, or pointedness is added to the root. Closedness appears only where the source uses cone separation to recover primal feasibility. The sensitivity item assumes the two candidate points are feasible, their multipliers are dual-positive and complementary, and each point minimizes its shifted Lagrangian; these hypotheses spell out “solutions and corresponding multipliers” without relying on informal terminology.
Contributions may formalize cone separation, perturbation-value geometry, saddle certificates, or strong duality. Finite-dimensional orthant and positive-semidefinite specializations are useful corollaries but do not replace the general goal. Local multiplier rules, equality constraints, differentiable Kuhn–Tucker conditions, and Chapter 9's local theory remain outside this mission.
## Selected references
- David G. Luenberger, *Optimization by Vector Space Methods*, John Wiley & Sons, 1969, Chapter 8, §§8.2–8.6, pp. 214–225. [Open Library record](https://openlibrary.org/books/OL7612943M/Optimization_by_Vector_Space_Methods)
- Stephen Boyd and Lieven Vandenberghe, *Convex Optimization*, Cambridge University Press, 2004, Chapter 5. [Official book page](https://web.stanford.edu/~boyd/cvxbook/)
Asymmetric Hashing Square Bound: omega < 2.3747Research Paper
AI generated, I think it's correct
## Motivation
The **matrix-multiplication exponent** measures the asymptotic arithmetic cost of multiplying square matrices. A bound $\omega<c$ means that, over the field under consideration, $n\times n$ matrices can be multiplied in $O(n^{c+\varepsilon})$ field operations for every $\varepsilon>0$. Matrix multiplication is a central benchmark in algebraic complexity and a basic subroutine in linear algebra, graph algorithms, and symbolic computation.
The Coppersmith--Winograd tensor and the laser method produced the strongest bounds on $\omega$ for several decades. The 1990 tensor-square analysis gave $\omega<2.375477$. Later analyses of larger powers improved the numerical bound, but they organized their recursion through values assigned independently to constituent tensors. Duan, Wu, and Zhou identified a loss in that organization: several fine constituents that can coexist inside one coarse block may be counted as though they had to be selected independently. Their asymmetric-hashing framework partially compensates for this **combination loss**. The paper's full second-power specialization improves the best bound obtainable from the square of the Coppersmith--Winograd tensor to $\omega<2.374631$; see Section 6.3 and its parameter Table 2 in [Duan--Wu--Zhou](https://arxiv.org/abs/2210.10173).
This mission isolates that second-power result. It is smaller than the paper's record-setting eighth-power calculation, but it contains the genuinely new asymmetric-hashing and hole-repair mechanisms in their first complete form. It therefore provides a focused bridge from the existing formalization of the classical $2.375477$ square analysis to later combination-loss methods.
## Setting
For a field $K$, the **matrix-multiplication tensor**
$$
\langle a,b,c\rangle_K
=\sum_{i<a}\sum_{j<b}\sum_{k<c}
x_{ij}\otimes y_{jk}\otimes z_{ki}
$$
encodes multiplication of an $a\times b$ matrix by a $b\times c$ matrix. A restriction applies one linear map to each tensor leg, while a degeneration permits polynomial families of such maps and takes their first nonzero coefficient. A degeneration from the diagonal tensor $I_r$ gives a border-rank upper bound of $r$.
The **Coppersmith--Winograd tensor** with parameter $q$ is
$$
CW_q=
\sum_{i=1}^{q}
(x_i y_i z_0+x_i y_0z_i+x_0y_i z_i)
+x_0y_0z_{q+1}+x_0y_{q+1}z_0+x_{q+1}y_0z_0.
$$
It has border rank at most $q+2$. Its coordinate partition has six supported types, and the square $CW_q^{\otimes2}$ has fifteen coarse constituent types $(i,j,k)$ with $i+j+k=4$. A large tensor power contains many blocks with prescribed joint and marginal type distributions. The **laser method** retains blocks whose variables are disjoint and interprets their direct sum through Schönhage's asymptotic sum inequality.
Duan--Wu--Zhou refine this organization by also retaining a split distribution for the fine indices inside each coarse constituent. Coarse $X$- and $Y$-blocks are made unique, while compatible coarse triples may initially share a $Z$-block. The resulting partially damaged constituent tensors are described as broken copies of a standard-form tensor. The formal target uses $q=6$, the full Section 6 construction, and the paper's released second-power parameters.
## Formalization targets
### Goal: the full second-power asymmetric-hashing bound
For every field $K$,
$$
\operatorname{matMulExp}(K)<\frac{23747}{10000}=2.3747.
$$
The source reports the stronger numerical endpoint $2.374631$, so the displayed rational inequality has strict slack. The Lean declaration has exactly the same field quantification and uses exactly the same `matMulExp` definition as the existing Coppersmith--Winograd $2.376$ mission; only the theorem name and rational endpoint change.
### Source-level milestones
The mission first isolates the available-block shuffling interface extracted from Definitions 5.3--5.5 and Claims 5.8--5.10, then formalizes the finite covering core of the Hole Lemma 5.6. The subsequent tensor realization by zeroing and identification, the multiple-copy Corollary 5.11, the compatibility-rate identity of Lemma 6.7, the probabilistic part of Claim 6.8, and the global restricted-splitting value inequality in Equation (25) remain visible structural leaves rather than being hidden inside scalar assumptions. The numerical milestone instantiates Equation (25) with the exact $q=6$ data of Section 6.3 and Table 2 and checks a strict value surplus at $\tau=23747/30000$. The structural proof must also make explicit the conversion from the paper's six-symmetrized value to a direct `HasTauValueAtLeast` witness for the mode-symmetric CW square. The final bridge applies the existing tau-value/rank machinery and transfers the Strassen-preorder exponent bound to `matMulExp`.
## Significance
The mathematical result gives the first improvement over the classical Coppersmith--Winograd number while continuing to use only the tensor square. It separates improvement of the tensor analysis from improvement obtained merely by moving to a much higher tensor power. The same standard-form and restricted-splitting language is then reused by the paper's higher-power algorithm, which reports $\omega<2.371866$.
For formalization, the mission adds reusable infrastructure for nested tensor partitions. Existing CW-square work records coarse support types and actual matrix-multiplication restrictions. This mission extends that layer with fine split distributions, compatibility between levels, broken-block bookkeeping, and repair of holes without replacing tensor statements by unverified scalar values. Those definitions are prerequisites for later asymmetric-hashing, complete-split, and more-asymmetry analyses.
The bound is known mathematically and was published at FOCS 2023. The open work is a machine-checked reconstruction. The underlying CW tensor, border-rank certificate, canonical tensor-square grading, Salem--Spencer sets, direct-sum tau-value notion, asymptotic sum inequality, and exponent equivalence already exist on Prove2Me. The new frontier is the cross-level combination-loss analysis and its exact numerical specialization.
## Difficulty
The central difficulty is that coarse and fine decompositions cannot be optimized independently. Two coarse triples may share a $Z$-block, and a fine $Z$-block can be useful for one triple, compatible with several, or removed by a collision. Counting all locally valuable fine constituents therefore does not certify a direct sum. Conversely, requiring every coarse $Z$-block to be unique discards precisely the combinations that produce the improvement.
The Hole Lemma must also preserve the actual tensor. A broken copy lacks some fine variable blocks; combining several such copies is useful only when a degeneration covers every required block with controlled loss and does not duplicate monomials. On the numerical side, the same-marginal maximum-entropy term and restricted-splitting values must be bounded with certified real inequalities. Floating-point output from MATLAB is evidence for a witness, not a Lean proof.
## Formalization scope
The mission uses the existing `TensorObj`, `MMObj`, restriction, degeneration, asymptotic-rank, `HasTauValueAtLeast`, `matMulExp_strassen`, and `matMulExp` declarations in environment `777aaa61dcd2a1258d2b4962dbe983ede4d23b2e`. Top-level results quantify over an arbitrary field. Finite supports and block indices are represented by finite types; probability and split distributions are nonnegative real functions of total mass one; entropy and numerical optimization live in the reals.
The formalization is restricted to $CW_6^{\otimes2}$ for the capstone, although generic definitions and source lemmas may quantify over levels and finite index types. A valid proof must connect scalar rate inequalities to witnessed restrictions or degenerations yielding direct sums of concrete matrix-multiplication tensors. A constant-valued surrogate for the restricted-splitting value, a hypothesis that already assumes the desired exponent bound, or a certificate definition containing its own conclusion is outside scope.
Contributions are welcome for standard-form tensor encodings, finite permutation arguments, hole repair, type and split counting, entropy maximization certificates, certified logarithm and power inequalities, and the final tau-value/rank assembly. Statements should identify the corresponding definition, lemma, claim, equation, or table in the source.
## Selected references
- Ran Duan, Hongxun Wu, and Renfei Zhou, *Faster Matrix Multiplication via Asymmetric Hashing*, 64th IEEE Symposium on Foundations of Computer Science (FOCS), 2023. [arXiv:2210.10173](https://arxiv.org/abs/2210.10173) and [released verification code](https://osf.io/dta6p/).
- Don Cop persmith and Shmuel Winograd, *Matrix Multiplication via Arithmetic Progressions*, Journal of Symbolic Computation 9, 1990, pp. 251--280. [DOI 10.1016/S0747-7171(08)80013-2](https://doi.org/10.1016/S0747-7171(08)80013-2).
- Arnold Schönhage, *Partial and Total Matrix Multiplication*, SIAM Journal on Computing 10(3), 1981, pp. 434--455. [DOI 10.1137/0210032](https://doi.org/10.1137/0210032).
Vector Space Methods VII: Euler–Lagrange EquationsTextbook
## Motivation
The calculus of variations replaces optimization over finitely many coordinates by optimization over paths. Its necessary conditions underlie geodesics, minimum-energy curves, classical mechanics, and many optimal-control models. Chapter 7 of David G. Luenberger's [*Optimization by Vector Space Methods*](https://openlibrary.org/books/OL7612943M/Optimization_by_Vector_Space_Methods) presents this transition as an application of differentiation in normed vector spaces: a local extremum first forces every directional derivative to vanish, and the resulting integral identity forces a differential equation along the optimizing path. This mission formalizes the scalar, fixed-endpoint version in §§7.4–7.5. The target is intentionally the theorem actually isolated by the source, not a stronger modern Sobolev-space variant.
## Setting
Fix real numbers $a<b$. A **$C^1$ path on the segment** is represented in Lean by two functions, $x,\dot x:\mathbb R\to\mathbb R$. Both are continuous on $[a,b]$, and $x$ has derivative $\dot x(t)$ at every $t\in(a,b)$. Ordinary two-sided derivatives are not demanded at $a$ or $b$; this makes the formal endpoint convention match the one-sided role of endpoints in a closed interval.
Let $L(y,v,t)$ be a scalar Lagrangian. Along a candidate path, write
$$
L_x(t)=\frac{\partial L}{\partial y}(x(t),\dot x(t),t),\qquad
L_v(t)=\frac{\partial L}{\partial v}(x(t),\dot x(t),t).
$$
The Lean statement records these partial derivatives with `HasDerivAt` and assumes that $L_x$ and $L_v$ are continuous on $[a,b]$. A **fixed-endpoint variation** is another $C^1$ pair $(h,\dot h)$ with $h(a)=h(b)=0$. The first variation already computed from the action is
$$
\delta J(x;h)=\int_a^b\bigl(L_x(t)h(t)+L_v(t)\dot h(t)\bigr)\,dt.
$$
The main theorem begins from the stationarity identity $\delta J(x;h)=0$ for every such variation. It does not claim that the complete passage from a local extremum in Luenberger's $C^1$ norm to this integral formula has already been bundled into the root statement.
## Formalization targets
### Main goal: Euler–Lagrange equation
From the computed first-variation identity, prove that
$$
\frac{d}{dt}L_v(t)=L_x(t)\qquad(t\in(a,b)).
$$
The conclusion is expressed as `HasDerivAt Lv (Lx t) t`, so it asserts both differentiability of $L_v$ and the equality of its derivative with $L_x$. This is equation (2) and the conclusion reached on printed pages 180–181.
### Milestones
The first milestone formalizes §7.4, Theorem 1: a local minimum or maximum of a real functional has zero derivative along every direction whenever that scalar directional derivative exists. The remaining milestones are the three fixed-endpoint fundamental lemmas from §7.5. They respectively show that a continuous coefficient annihilating all variations is zero, that a continuous coefficient annihilating all variation derivatives is constant, and that an identity involving both $h$ and $\dot h$ forces the second coefficient to have derivative equal to the first. These are stated with the same $C^1$ variation class used by the goal.
## Significance
The result turns an infinite family of scalar integral equalities into a pointwise differential equation. Once available, the same interface can support standard variational examples by supplying a concrete $L$, its two partial derivatives, and a stationary path. It also provides the analytic core needed before treating natural boundary conditions, vector-valued paths, higher derivatives, or weak Euler–Lagrange equations.
The formalization adds reusable interval-sensitive infrastructure. In particular, `IsC1OnSegment` separates a path from its chosen continuous derivative and avoids silently imposing derivatives outside the optimization interval. The three fundamental lemmas are useful independently of the named Euler–Lagrange theorem: they are test-function principles for interval integrals and can serve later missions involving integration by parts or weak formulations. The mathematics is classical and proved in the cited text; the open work is a machine-checked Lean development of these exact statements in the pinned Mathlib environment.
## Difficulty
The source argument uses informal phrases such as “arbitrary $C^1$ function vanishing at the endpoints” and treats endpoint differentiation according to standard calculus convention. In Lean, those phrases must determine a precise domain, derivative witness, continuity requirement, and interval-integral orientation. Replacing $C^1$ variations by merely continuous functions would change Lemmas 2 and 3, while requiring `HasDerivAt` at the endpoints would add a hypothesis not present in the book.
Another tempting shortcut is to assume from the outset that $L_v$ is differentiable and then use integration by parts. That would trivialize the central regularity conclusion of Lemma 3: the book derives differentiability of $L_v$ from stationarity and continuity. The root therefore assumes only continuity of the two coefficient functions and concludes a `HasDerivAt` assertion on the open interval. Conversely, constructing the first variation from a local extremum of the action requires a separate differentiation-under-the-integral development and a topology on bundled $C^1$ paths; it is not hidden inside the main goal.
## Formalization scope
The scalar field, path values, time variable, and action values are all real. The interval is nondegenerate through the explicit hypothesis $a<b$. Integrals use Mathlib's oriented interval integral, but all principal statements are made in the forward orientation. Paths and variations are total functions on $\mathbb R$ whose relevant regularity is restricted to $[a,b]$. The Lagrangian is finite-valued. No measurability or integrability premise is omitted: continuity of the coefficient and variation factors on the compact interval supplies the intended finite integrals.
The goal starts from an already computed first-variation identity. Contributions connecting a genuine local extremum of the action in the norm $\max|x|+\max|\dot x|$ to that identity are welcome as a strengthening, but they must not be advertised as part of the present root theorem. Other welcome contributions include reusable continuous test-function constructions and endpoint-aware interval integration lemmas. Sobolev paths, vector-valued state spaces, free endpoints, and weak derivatives are outside this mission and should be proposed separately rather than obtained by weakening the stated hypotheses until the result becomes vacuous.
## Selected references
- David G. Luenberger, *Optimization by Vector Space Methods*, John Wiley & Sons, 1969, Chapter 7, §§7.4–7.5, pp. 178–181; definition of $D[a,b]$ on p. 23. [Open Library record](https://openlibrary.org/books/OL7612943M/Optimization_by_Vector_Space_Methods)
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).
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).
Vector Space Methods III: Recursive EstimationTextbook
## Motivation
The final sections of Chapter 4 of Luenberger's *Optimization by Vector Space Methods* (Wiley, 1969) derive the **discrete-time Kalman filter** (§4.7 Theorem 1, attributed to Kalman 1960) purely from Hilbert space geometry: the optimal estimate of a linearly evolving random state is an orthogonal projection onto the span of past measurements, and the projection updates recursively as measurements arrive. This derivation — no Gaussian assumptions, no density calculations — is a canonical application of the projection theorem formalized in Mission I and the estimation theory of Mission II.
## Setting
Following §4.2 and §4.7 of the source, all random variables have zero mean and finite second moments, and are treated as elements of a **Hilbert space of random variables**: an abstract real inner product space $H$ in which the inner product of two random variables is their correlation, $\langle a, b\rangle = E[ab]$. Random $n$-vectors are families $\mathrm{Fin}\ n \to H$; two random variables are **uncorrelated** iff they are orthogonal in $H$; the **covariance matrix** of a zero-mean random vector $x$ is the Gram matrix $\langle x_i, x_j\rangle$. A **white** process $u$ satisfies $E[u(k)u(l)^\top] = Q(k)\,\delta_{kl}$.
The **dynamic model** (§4.7) consists of a state process and measurements
$$x(k+1) = \Phi(k)\,x(k) + u(k), \qquad v(k) = M(k)\,x(k) + w(k), \qquad k = 0, 1, 2, \dots$$
with known matrices $\Phi(k) \in \mathbb{R}^{n\times n}$, $M(k) \in \mathbb{R}^{m\times n}$, white noises $u, w$ with covariances $Q(k)$, $R(k)$ ($R(k)$ positive definite), mutually uncorrelated and uncorrelated with the initial state $x(0)$. The estimate $\hat x(k+1 \mid k)$ is the projection of each component of $x(k+1)$ onto the subspace spanned by the components of $v(0), \dots, v(k)$.
## Formalization targets
The goal is §4.7 Theorem 1: the estimates generated by the recursion
$$\hat x(k+1 \mid k) = \Phi(k) P(k) M^\top(k)\big[M(k)P(k)M^\top(k) + R(k)\big]^{-1}\big(v(k) - M(k)\hat x(k \mid k-1)\big) + \Phi(k)\, \hat x(k \mid k-1)$$
$$P(k+1) = \Phi(k) P(k)\big\{I - M^\top(k)[M(k)P(k)M^\top(k) + R(k)]^{-1} M(k) P(k)\big\}\Phi^\top(k) + Q(k),$$
started from $\hat x(0 \mid -1) = 0$ and $P(0) = \operatorname{cov} x(0)$, are the linear minimum-variance estimates: each $\hat x(k \mid k-1)$ lies in the span of past measurement components, its error is orthogonal to all past measurements, and its error covariance is $P(k)$.
Milestones: orthogonality of the **innovation** $v(k) - M(k)\hat x(k\mid k-1)$ to the past-data subspace, and the single-step **updating formula** (§4.6 Example 1) — given a prior projection with error covariance $R$ and new data $y = W\beta + \varepsilon$, the updated projection is $\hat\beta + RW^\top(WRW^\top + Q)^{-1}(y - W\hat\beta)$ with error covariance $R - RW^\top(WRW^\top+Q)^{-1}WR$.
## Significance
The Kalman filter is among the most used algorithms in engineering — navigation, tracking, control, time-series analysis — and this mission gives it a machine-checked correctness statement at the natural level of generality: linear minimum-variance optimality over arbitrary zero-mean second-order processes, with no Gaussian hypothesis. Mathlib currently has no Kalman filter and no linear filtering theory. The abstract Hilbert-space formulation also makes the development directly reusable: the update milestone is a general two-stage projection lemma independent of the dynamic model.
## Difficulty
The recursion couples two invariants that must be established simultaneously by induction: the geometric one (the error is orthogonal to the growing measurement subspace, and the estimate lies in it) and the algebraic one (the error Gram matrix equals $P(k)$). Whiteness enters precisely through the index inequalities — $u(k)$ and $w(k)$ are orthogonal to everything generated by $x(0), u(0..k{-}1), w(0..k{-}1)$ — and an off-by-one in these ranges silently breaks the induction. Invertibility of $M(k)P(k)M^\top(k) + R(k)$ must be derived, not assumed: $P(k)$ is positive semidefinite as a Gram matrix and $R(k)$ is positive definite. The naive approach of expanding all projections over a concrete probability space adds measure-theoretic overhead the abstract formulation avoids entirely.
## Formalization scope
The Hilbert space of random variables is an abstract `H : Type` with `[NormedAddCommGroup H] [InnerProductSpace ℝ H]`; **zero means are implicit** in this representation (§4.7 assumes all variables zero-mean), so expectations never appear — only inner products. Matrix-vector actions on random vectors are written componentwise as `∑ j, A i j • x j`. Processes are indexed by `ℕ`, with `x̂(0 | -1)` rendered as `xh 0 = 0` and covariances as explicit Gram identities. Whiteness and uncorrelatedness are hypotheses on inner products with `if k = l then _ else 0`. The span of past data at time $k$ is `Submodule.span ℝ {a | ∃ l < k, ∃ j, a = v l j}`. The recursion defining `xh` and `P` is supplied as hypotheses, so the goal asserts exactly the optimality and covariance claims of the source theorem. Statements deliberately avoid Mathlib's `orthogonalProjection`; the projection property is asserted by membership plus orthogonality, which characterizes it uniquely.
## Selected references
- David G. Luenberger, *Optimization by Vector Space Methods*, John Wiley & Sons, 1969. §4.6–4.7, pp. 90–97. ISBN 0-471-55359-X.
- R. E. Kalman, *A new approach to linear filtering and prediction problems*, J. Basic Eng. 82 (1960), 35–45. https://doi.org/10.1115/1.3662552
Markov Chains and Mixing Times XIII: Coupling from the PastTextbook
## Motivation
Every sampling guarantee in this series so far is approximate: run the chain for $t_{\mathrm{mix}}(\varepsilon)$ steps and the output is within $\varepsilon$ of stationarity. In 1996 Propp and Wilson showed that, astonishingly, one can often sample *exactly* from the stationary distribution of a chain — with no error at all and no knowledge of the mixing time — by running the chain not forward from the present but **from the past**. Their algorithm, **coupling from the past** (CFTP), drives all states simultaneously with the same sequence of random update maps drawn from times $-1,-2,-3,\dots$; as soon as the composed map from some time $-t$ collapses the entire state space to a single value, that value is an exact sample from $\pi$. Chapter 22 of Levin–Peres–Wilmer, *Markov Chains and Mixing Times* (AMS, 2009; the chapter is by Propp and Wilson themselves) presents the algorithm, the monotone shortcut that makes it practical for huge state spaces, and the proof of exactness. This mission — the final one of the series — formalizes that correctness proof.
## Setting
Throughout, $P$ is a chain on a finite state space $V$ with stationary distribution $\pi$. A **random mapping representation** of $P$ is a probability distribution $\nu$ on update functions $f:V\to V$ that reproduces the transition probabilities in one step:
$$\nu\{f: f(x)=y\}\;=\;P(x,y)\qquad\text{for all }x,y.$$
Sampling $f\sim\nu$ and applying it to the current state is exactly one $P$-step — simultaneously from every possible current state.
CFTP draws i.i.d. maps $f_{-1},f_{-2},\dots\sim\nu$ indexed by *past* times and composes them **forward from the past up to time zero**:
$$F^0_{-t}\;=\;f_{-1}\circ f_{-2}\circ\cdots\circ f_{-t}.$$
Note the order: extending the horizon deeper into the past prepends new randomness *inside* the composition, while the maps near time $0$ stay fixed — this is the crucial asymmetry between running from the past and running into the future. The composition has **coalesced** when $F^0_{-t}$ is a constant map — all starting states have been funneled to one common value — and the algorithm outputs that value. In the **monotone** variant, $V$ carries a partial order with a bottom state $\hat0$ and a top state $\hat1$ and every update map is monotone; then it suffices to track the two extreme trajectories.
## Formalization targets
### Goal
Correctness of coupling from the past (Propp–Wilson; §22.2–22.3), the capstone of the series: if $\nu$ is a random mapping representation of $P$, $\pi$ is stationary for $P$, and coalescence is almost sure, then for every state $y$ the probability that the CFTP composition has coalesced to the value $y$ within $t$ steps from the past tends, as $t\to\infty$, to exactly $\pi(y)$ — the output of the algorithm is an *exact* sample from the stationary distribution, with no mixing-time error term.
### Milestones
- **Proposition 1.5 / §22.3** — every finite Markov chain has a random mapping representation: a suitable $\nu$ always exists.
- **Coalescence (§22.3)** — if some finite composition of update maps collapses the state space with positive probability, then coalescence is almost sure: the probability that $F^0_{-t}$ is not yet constant tends to $0$ as $t\to\infty$.
- **Monotone CFTP (§22.2)** — if the state space has a bottom $\hat0$ and a top $\hat1$ and every update map is monotone, then the composition is constant as soon as it merely identifies $\hat0$ and $\hat1$: checking two trajectories certifies coalescence of all of them.
## Significance
*The results.* CFTP is one of the most striking algorithmic ideas probability has produced: a Las Vegas algorithm whose output distribution is *exactly* $\pi$, side-stepping every mixing-time estimate of the previous twelve missions. The monotone shortcut is what made it explode in practice — for the Ising model of Mission IX the $2^n$ trajectories collapse to two, and Propp–Wilson famously drew exact Ising samples on large grids at the critical temperature. CFTP remains the foundation of exact-simulation methods across statistical physics, spatial statistics, and randomized algorithms.
*Formalizing it.* The correctness argument is short but famously slippery — the standard pitfall (running the coupling *into the future* yields a biased sample) is precisely a statement about the order of composition, which a formal proof pins down mercilessly. Nothing about exact sampling exists in any proof-assistant library. Formalized CFTP correctness is a fitting keystone: it consumes the random-map representation (Chapter 1), stationarity (Mission I), and the almost-sure-coalescence analysis, and certifies the algorithm practitioners actually run.
## Difficulty
The whole content lies in managing the composition order and the limiting argument without measure theory. The probability space at horizon $t$ is the finite product of $t$ copies of $\nu$ (tuples of update maps, weighted by products); the key observation — for fixed $t$, the law of $F^0_{-t}$ applied to any fixed start equals the law of $t$ forward steps — is a finite re-indexing argument. Exactness then follows from a sandwich: on the event of coalescence by time $t$, the output equals $F^0_{-t}(x)$ for *every* $x$; choosing the start according to $\pi$ shows the output law differs from $\pi$ by at most the non-coalescence probability, and the hypothesis drives that to zero. Formalizing this needs care at exactly the point where informal proofs wave: the event "coalesced by $-t$" is *increasing* in $t$ because the maps near zero are shared between horizons — the tuple encoding must make this monotonicity provable. The coalescence milestone is a geometric-trials argument (independent blocks each collapse with probability bounded below), and the monotone milestone is an induction showing monotonicity of compositions plus the squeeze between the extreme trajectories. All randomness is finite products of a finite distribution; limits are limits of explicit real sequences.
## Formalization scope
Update-map distributions are functions $(V\to V)\to\mathbb R$ with the distribution predicate of Mission I; the random-map representation condition is a finite-sum identity. The composition $F^0_{-t}$ is encoded by a tuple $F:\mathrm{Fin}\,t\to(V\to V)$ with $F(i)$ the map used at time $-(i{+}1)$, folded so that the *last* entry applies first — the from-the-past order. Coalescence probabilities and output probabilities are finite sums over tuples of products of $\nu$-weights; "coalescence is almost sure" is the statement that the non-coalescence probability tends to $0$, and the goal's conclusion is a limit of real sequences (`Filter.Tendsto`), not a measure-theoretic almost-sure statement. The monotone milestone is stated abstractly for any finite partial order with `OrderBot` and `OrderTop` and any tuple of monotone maps — reusable beyond CFTP. No measure theory, filtrations, or i.i.d. infrastructure is required anywhere.
## Selected references
- D. A. Levin, Y. Peres, E. L. Wilmer, *Markov Chains and Mixing Times*, American Mathematical Society, 2009 (Chapter 22, by J. G. Propp and D. B. Wilson). https://documents.epfl.ch/groups/i/ip/ipg/www/2013-2014/Random_Walks/markovmixing.pdf
- J. G. Propp, D. B. Wilson, *Exact sampling with coupled Markov chains and applications to statistical mechanics*, Random Structures Algorithms 9 (1996). https://doi.org/10.1002/(SICI)1098-2418(199608/09)9:1/2<223::AID-RSA14>3.0.CO;2-O
- D. B. Wilson, *How to couple from the past using a read-once source of randomness*, Random Structures Algorithms 16 (2000). https://doi.org/10.1002/(SICI)1098-2418(200003)16:2<85::AID-RSA1>3.0.CO;2-H
Modern A/B tests must infer *lifetime* treatment effects — e.g. customer lifetime value under a new feature — from short-horizon experiment data. Chen, Simchi-Levi and Wang (arXiv:2407.19618) model the experiment as a Markov decision process and exploit a structural fact of many practical interventions: the treatment is *local*, modifying the system at a single crucial state only. This mission formalizes the core asymptotic theory of the paper: for **any** differentiable estimator built from the experiment's transition and reward statistics, *information sharing* — pooling across test arms the samples collected away from the treated state — keeps the estimator asymptotically normal with the same asymptotic bias and never increases its asymptotic variance (Theorem 9), and is asymptotically efficient among unbiased estimators (Theorem 5). The route runs through a Markov chain central limit theorem with the asymptotic variance identified as the autocovariance series, and the linearization/delta method for functionals of chain statistics.
Markov Chains and Mixing Times II: The Convergence TheoremTextbook
## Motivation
The first mission of this series established that an irreducible finite Markov chain has a unique stationary distribution $\pi$. The present mission, covering Chapters 3–4 of Levin–Peres–Wilmer, *Markov Chains and Mixing Times* (AMS, 2009), answers the two questions that make that fact useful. First, the *inverse* problem of sampling: given a target distribution $\pi$ — uniform over proper colorings, a Gibbs measure, a posterior — how does one build a chain whose stationary distribution is $\pi$? The Metropolis and Glauber constructions of Chapter 3 are the universal answers, and they are the engine of Markov chain Monte Carlo across statistical physics, Bayesian statistics, and approximate counting. Second, the *convergence* question: in what sense, and how fast, does an irreducible aperiodic chain approach $\pi$? Chapter 4 introduces the total variation distance, proves the Convergence Theorem — geometric convergence to stationarity — and defines the mixing time, the parameter the entire remainder of the book estimates.
## Setting
All chains live on a finite state space $V$ and are presented by row-stochastic matrices, with the definitions of Mission I. The **total variation distance** between distributions $\mu$ and $\nu$ is
$$\|\mu-\nu\|_{\mathrm{TV}} = \max_{A\subseteq V}\,|\mu(A)-\nu(A)|,$$
the maximal discrepancy over events. A **coupling** of $\mu$ and $\nu$ is a distribution on $V\times V$ whose marginals are $\mu$ and $\nu$. For a chain $P$ with stationary $\pi$ one sets
$$d(t)=\max_x \|P^t(x,\cdot)-\pi\|_{\mathrm{TV}},\qquad \bar d(t)=\max_{x,y}\|P^t(x,\cdot)-P^t(y,\cdot)\|_{\mathrm{TV}},$$
and the **mixing time** is $t_{\mathrm{mix}}(\varepsilon)=\min\{t : d(t)\le\varepsilon\}$, with $t_{\mathrm{mix}}=t_{\mathrm{mix}}(1/4)$.
The **Metropolis chain** for a target $\pi$ and a symmetric proposal chain $\Psi$ accepts a proposed move $x\to y$ with probability $1\wedge \pi(y)/\pi(x)$; a general (not necessarily symmetric) base chain is handled by the ratio $\bigl(\pi(y)\Psi(y,x)\bigr)/\bigl(\pi(x)\Psi(x,y)\bigr)\wedge 1$. The **Glauber dynamics** for a distribution $\pi$ on configurations $V^{\text{sites}}$ picks a uniform site and re-samples its value from $\pi$ conditioned on the rest.
## Formalization targets
### Goal
$$\text{$P$ irreducible and aperiodic}\;\Longrightarrow\;\exists\,\alpha\in(0,1),\ C>0:\quad d(t)\le C\alpha^{t}.$$
This is Theorem 4.9, the Convergence Theorem. It asserts only the geometric shape of convergence, leaving all quantitative rates to later missions, which is why it is the goal.
### Milestones
The milestones are the chapter's working parts: stationarity and reversibility of the Metropolis chain for symmetric and general base chains (§3.2, Exercise 3.1), stationarity and reversibility of the Glauber dynamics (§3.3, Exercise 3.2); the three characterizations of total variation distance — the half-$\ell^1$ formula (Proposition 4.2 with Remark 4.3), the supremum over $[-1,1]$-bounded test functions (Proposition 4.5), and the coupling characterization with an optimal coupling attaining it (Proposition 4.7 with Remark 4.8); the comparison $d\le\bar d\le 2d$ (Lemma 4.11) and submultiplicativity $\bar d(s+t)\le\bar d(s)\bar d(t)$ (Lemma 4.12); the standard mixing-time consequences $d(\ell\, t_{\mathrm{mix}}(\varepsilon))\le(2\varepsilon)^\ell$ and $t_{\mathrm{mix}}(\varepsilon)\le\lceil\log_2\varepsilon^{-1}\rceil\, t_{\mathrm{mix}}$ (§4.5); and the equality of distance to stationarity for a group walk and its inverse walk (Lemma 4.13 and Corollary 4.14).
## Significance
*The results.* The Convergence Theorem is the qualitative foundation on which quantitative mixing theory stands: it guarantees that $t_{\mathrm{mix}}(\varepsilon)$ is finite, so every bound in Missions III–XIII is a bound on a well-defined quantity. The TV characterizations are used constantly — the coupling characterization is the engine of Mission III, the half-$\ell^1$ formula of every explicit computation. The Metropolis and Glauber stationarity results justify the chains analyzed in Missions III (colorings, hardcore), VIII (path coupling) and IX (Ising). Submultiplicativity of $\bar d$ is what makes $t_{\mathrm{mix}}$ a meaningful single number.
*Formalizing them.* None of this exists in Mathlib: there is no total variation distance for finitely supported distributions, no coupling theory, no mixing time, no MCMC correctness statement. The definition layer published here (TV distance, $d$, $\bar d$, $t_{\mathrm{mix}}$, couplings, Metropolis, Glauber) is imported by every subsequent mission of the series.
## Difficulty
The tempting proof of Theorem 4.9 via spectral decomposition fails twice: it needs reversibility, which the theorem does not assume, and spectral machinery that arrives only in Mission VII. The book's proof is the Doeblin decomposition: by Proposition 1.7 some power satisfies $P^r(x,y)\ge\delta\pi(y)$, so $P^r=(1-\theta)\Pi+\theta Q$ with $\Pi$ the rank-one matrix of rows $\pi$, and induction gives $P^{rk}=(1-\theta^k)\Pi+\theta^kQ^k$. The formal work is matrix algebra with careful bookkeeping of the remainder chain $Q$, plus the monotonicity of $d$ needed to interpolate between multiples of $r$. For Proposition 4.7 the delicate half is *constructing* the optimal coupling: mass $\mu\wedge\nu$ on the diagonal and the normalized product of the positive parts off it, with the degenerate case $\mu=\nu$ handled separately. The Glauber stationarity statement must be phrased with care because configurations outside the support of $\pi$ have junk rows; the formalization asserts stochasticity only at supported configurations, and detailed balance globally.
## Formalization scope
Total variation distance is *defined* as the supremum over events, $\bigsqcup_{A}\,|\mu(A)-\nu(A)|$ over `Finset V`, exactly as in (4.1); the half-$\ell^1$ formula is a milestone, not the definition. The mixing time is `sInf` of the set $\{t : d(t)\le\varepsilon\}$ in $\mathbb N$ (junk value $0$ if empty — impossible under the goal theorem). Couplings are distributions on the product with prescribed marginals; no probability-space machinery is used. The mixing-time inequalities are stated with the integer-rounding slack made explicit (e.g. $\lceil\log_2\varepsilon^{-1}\rceil$ via `Nat.ceil` of a real logarithm) so that no statement is true only "up to rounding". The Metropolis definitions use total real division, so the hypotheses require $\pi>0$ pointwise; this matches the book, which divides by $\pi(x)$ throughout.
Welcome contributions beyond the milestones: `simp` lemmas for `tvDist`, monotonicity of $d$ and $\bar d$ in $t$, and triangle-inequality infrastructure — all reused by Missions III–XIII.
## Selected references
- D. A. Levin, Y. Peres, E. L. Wilmer, *Markov Chains and Mixing Times*, American Mathematical Society, 2009. https://documents.epfl.ch/groups/i/ip/ipg/www/2013-2014/Random_Walks/markovmixing.pdf
- N. Metropolis, A. Rosenbluth, M. Rosenbluth, A. Teller, E. Teller, *Equation of state calculations by fast computing machines*, J. Chem. Phys. 21 (1953). https://doi.org/10.1063/1.1699114
- W. Doeblin, *Exposé de la théorie des chaînes simples constantes de Markov à un nombre fini d'états*, Rev. Math. Union Interbalkan. 2 (1938).
Primal-Dual Online Load Balancing on Unrelated MachinesTextbook
## The model
Fix $m \ge 1$ **machines** and $n$ **jobs** arriving one at a time in the order $0, \dots, n-1$. Job $i$ carries a whole vector of nonnegative **loads** $\tilde p(i,j)$, one per machine, with no assumed relationship between the entries — the same job may be cheap on one machine and unplaceable on another. This is the **unrelated machines** model. When job $i$ arrives its load vector becomes visible, and the algorithm must commit it to a single machine immediately and **irrevocably**, knowing nothing about the jobs still to come. A machine's load is the sum of $\tilde p(i,j)$ over the jobs assigned to it.
The setting formalized here is one **normalized phase**: loads are already scaled by a guessed makespan, so machine $j$ counts as **eligible** for job $i$ exactly when $\tilde p(i,j) \le 1$. The phase is allowed to give up rather than assign badly — it **fails** if an arriving job has no eligible machine, or if an internal weight grows past $1$.
## The algorithm and the guarantee
The algorithm keeps a **weight** $x(j)$ per machine, initialized to $1/(2m)$. Job $i$ goes to the eligible machine $\ell$ minimizing $\tilde p(i,\ell)\, x(\ell)$; that machine's weight is then scaled by $1 + \tilde p(i,\ell)/2$, so a machine becomes exponentially unattractive as it fills. The weights are the primal variables of the covering LP
$$\min \sum_j x(j) + \sum_i z(i) \quad \text{s.t.} \quad \tilde p(i,j)\,x(j) + z(i) \ge 1 \ \text{ for every eligible pair } (i,j),$$
and each assignment raises one dual variable $y(i,\ell)$ to $1$. The guarantee follows from weak duality rather than a bespoke potential argument, which is the point of the primal-dual method.
The goal theorem states that if the dual admits a feasible solution putting unit total mass on every job — the certificate that the guessed makespan was large enough — then the phase does not fail, every job is assigned, and every machine ends with load
$$\sum_{i \,\text{assigned to}\, j} \tilde p(i,j) \ \le\ \frac{\ln(3m)}{\ln(3/2)}.$$
The source states this as $O(\log m)$; the explicit constant is what its proof yields.
Note that the load bound alone is not the theorem: it holds vacuously when the phase assigns nothing, and the milestones state it that way deliberately. The content is the conjunction of *succeeded*, *assigns all*, and the bound.
## Scope
The **doubling wrapper** — guess a makespan, run a phase, double the guess and restart on failure — is what turns this phase into an $O(\log m)$-competitive online algorithm. It is outside this mission; the guarantee proved here is the conditional single-phase statement. The milestones break the argument into weak duality for finite LPs, the load bound, primal feasibility at each prefix, the primal objective identity, and the failure certificate.
## Source
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, Chapter 8, pp. 193–196 (Theorem 8.1). [PDF](https://www.tau.ac.il/~nivb/download/pd-survey.pdf) · [doi:10.1561/0400000024](https://doi.org/10.1561/0400000024)
Hefferon Linear Algebra V: Jordan Canonical FormTextbook
Chapter Five of Jim Hefferon's *Linear Algebra* is one long search for a canonical form for matrix similarity, and Theorem IV.2.8 ends it: over the complex numbers every square matrix is similar to a matrix in Jordan form. That is the goal theorem of this mission and the capstone of the book. Mathlib carries the generalized eigenspace decomposition but has no Jordan canonical form, so this is a genuine target rather than a wrapper around an existing lemma; the Jordan block and the block-diagonal Jordan matrix are supplied as a mission definition. The milestones are the three results the proof is assembled from: diagonalizability as the existence of an eigenbasis, Cayley-Hamilton, and the canonical form of a nilpotent map, which is Jordan form applied to $t - \lambda$ on each generalized eigenspace.
Introduction to Linear Optimization VI: Farkas' Lemma and Separating HyperplanesTextbook
When is a system of linear constraints infeasible? Sections 4.6-4.7 of Bertsimas-Tsitsiklis answer with the archetypal theorem of the alternative. The capstone is Farkas' lemma (Theorem 4.6): for an $m \times n$ matrix $A$ and $b \in \mathbb{R}^m$, exactly one of the following holds — (a) some $x \ge 0$ satisfies $Ax = b$, or (b) some $p$ satisfies $p'A \ge 0'$ and $p'b < 0$; such a $p$ is a certificate of infeasibility, geometrically a hyperplane separating $b$ from the cone of the columns of $A$. The mission also carries the cone-membership restatement (Corollary 4.3), the inequality form (Theorem 4.7: every solution of $Ax \le b$ satisfies $c'x \le d$ iff some $p \ge 0$ has $p'A = c'$ and $p'b \le d$), and the application to asset pricing (Theorem 4.8: a market's prices admit no arbitrage iff there is a nonnegative state-price vector $q$ with $p_i = \sum_s q_s r_{si}$). The book proves Farkas' lemma from LP strong duality; Section 4.7 then reverses the arrow from first principles: every polyhedron is closed (Theorem 4.9), Weierstrass' theorem (Theorem 4.10, already in Mathlib), and the separating hyperplane theorem (Theorem 4.11: for nonempty closed convex $S$ and $x^* \notin S$ there exists $c$ with $c'x^* < c'x$ for all $x \in S$), from which Farkas' lemma — and hence the duality theorem itself — follows geometrically.
Introduction to Linear Optimization V: Duality TheoryTextbook
Every linear programming problem has a shadow. To the primal $\min c'x$ we associate the dual $\max p'b$, whose variables price the primal constraints: one dual variable per primal constraint and one dual constraint per primal variable, with signs governed by the correspondence of Table 4.1. This mission formalizes §4.1–4.5 of Bertsimas–Tsitsiklis: the dual of a general-form linear program, the involution "the dual of the dual is the primal" (Theorem 4.1), and weak duality $p'b \le c'x$ for any primal-feasible $x$ and dual-feasible $p$ (Theorem 4.3) with its two corollaries — an unbounded primal forces an infeasible dual (Corollary 4.1), and feasible $x, p$ with $p'b = c'x$ are automatically both optimal (Corollary 4.2). The goal theorem is strong duality (Theorem 4.4): if a linear programming problem has an optimal solution, so does its dual, and the respective optimal costs are equal — proved in the book by running the simplex method with the lexicographic pivoting rule of Mission IV on a standard-form transform. The statement is deliberately the book's attainment form: by Table 4.2 the primal and the dual can be simultaneously infeasible (Example 4.5), so an unguarded equality of optimal values is false. The mission closes with complementary slackness (Theorem 4.5): feasible $x$ and $p$ are simultaneously optimal if and only if $p_i(a_i'x - b_i) = 0$ for all $i$ and $(c_j - p'A_j)x_j = 0$ for all $j$ — the certificate structure behind the dual simplex method and every LP optimality check.
Hefferon Linear Algebra III: Maps, Representation and Change of BasisTextbook
Chapter Three of Jim Hefferon's *Linear Algebra* is about maps between spaces and how matrices represent them. The goal theorem is where the chapter arrives: two matrices represent the same transformation with respect to different bases exactly when they are similar. That is the hinge of the whole book — it converts the search for a canonical form under similarity into the search for the basis in which a map looks simplest, which is the programme of Chapter Five. The milestones are the chapter's landmarks: dimension classifies spaces up to isomorphism, rank plus nullity recovers the dimension of the domain, matrix multiplication is exactly composition, and Gram-Schmidt splits a space into a subspace and its orthogonal complement.
Hefferon Linear Algebra II: Dimension and RankTextbook
Chapter Two of Jim Hefferon's *Linear Algebra* builds the vector space vocabulary — spanning, independence, basis — and turns it into a theory of dimension. The goal theorem is the chapter's most striking result, that the row rank and the column rank of a matrix always agree, which is the bridge between the matrix-of-numbers view of Chapter One and the vector space view of Chapter Two. The milestones are the two pillars it stands on: that any two bases of a space have the same size, so dimension is well defined at all, and that any linearly independent set can be extended to a basis.
Introduction to Linear Optimization III: Fourier–Motzkin Elimination and Projections of PolyhedraTextbook
Is the shadow of a polyhedron again a polyhedron? §2.8 of Bertsimas–Tsitsiklis answers this with perhaps the oldest method for solving linear programming problems: Fourier–Motzkin elimination. Given $P = \{x \in \mathbb{R}^n \mid \sum_{j=1}^n a_{ij}x_j \ge b_i,\ i = 1, \dots, m\}$, one sorts the constraints by the sign of the coefficient of $x_n$ — rewriting them as $x_n \ge d_i + \mathbf{f}_i'\bar{x}$, $d_j + \mathbf{f}_j'\bar{x} \ge x_n$, or $0 \ge d_k + \mathbf{f}_k'\bar{x}$ — and forms the polyhedron $Q \subset \mathbb{R}^{n-1}$ whose constraints are all pairwise combinations $d_j + \mathbf{f}_j'\bar{x} \ge d_i + \mathbf{f}_i'\bar{x}$ together with the constraints not involving $x_n$. The capstone, Theorem 2.10, states that $Q$ is exactly the projection $\Pi_{n-1}(P)$ of $P$ onto its first $n-1$ coordinates: a value of $x_n$ can be interpolated if and only if every lower bound is below every upper bound. Though hopeless as an algorithm (the number of constraints can grow exponentially), elimination has powerful theoretical corollaries, all formalized here: projections $\Pi_k(P)$ of polyhedra are polyhedra (Corollary 2.4), the image of a polyhedron under any linear mapping is a polyhedron (Corollary 2.5), and the convex hull of finitely many vectors is a polyhedron (Corollary 2.6) — the first half of the finite-basis picture completed by the resolution theorem of Mission VII.
Hefferon Linear Algebra I: Gauss's Method and the Solution SetTextbook
Chapter One of Jim Hefferon's *Linear Algebra* develops Gauss's method and asks what row reduction actually preserves. The answer arrives as the Linear Combination Lemma: row operations change the rows of a matrix but never the subspace those rows span, and that invariant is complete. The goal theorem is that completeness — two matrices are row equivalent exactly when they have the same row space — which is what makes reduced echelon form a genuine canonical form. The milestones are the two results the chapter builds on the way: that row operations leave a system's solution set alone, and that a solution set is always one particular solution translated by the solutions of the associated homogeneous system.
Introduction to Linear Optimization II: Existence and Optimality of Extreme PointsTextbook
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.
Bandit feedback is only one point on a spectrum: a learner might see more than its own loss (full information) or less (a spam filter never learns what happened to mail it deleted). Chapter 37 of Lattimore–Szepesvári studies finite adversarial games $G = (\mathcal{L}, \Phi)$ where the loss matrix and the feedback matrix are decoupled. The goal theorem is the celebrated classification theorem: every finite partial-monitoring game has minimax regret exactly $0$, $\Theta(\sqrt{n})$, $\Theta(n^{2/3})$ or $\Omega(n)$ — determined by two purely combinatorial conditions, global and local observability, on the game's neighbourhood structure. A single geometric dichotomy thus governs the price of information in every online decision problem with finite actions and feedback.
Bandit Algorithms XII: Follow-the-Regularised-Leader and Mirror DescentTextbook
Beneath Exp3, Exp4 and their relatives lies one algorithm: minimize past losses plus a convex regularizer. Chapters 26–28 of Lattimore–Szepesvári develop this unifying view. For a Legendre potential $F$ with Bregman divergence $D_F$, both mirror descent and follow-the-regularised-leader satisfy the master bound $R_n(a) \le \frac{F(a) - F(a_1)}{\eta} + \frac{1}{\eta}\sum_t D_F(a_t, \tilde a_{t+1})$; the negentropy potential on the simplex recovers Exp3 exactly. The goal theorem is the payoff for adversarial *linear* bandits: FTRL on the unit ball with the self-concordant-flavoured potential $F(a) = -\log(1-\|a\|) - \|a\|$ achieves $R_n \le 2\sqrt{3nd\log n}$ — improving the $\sqrt{d}$ factor over the Exp3-style approach of Chapter 27 and matching the $\Omega(d\sqrt{n})$ lower bound of Mission XI up to logarithms.