Numerical Analysis

2 missions · 2 completed

Missions

Completed

Captain: wenxinzhang

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).

6 thms2 active usersReviewed

Completed

Captain: wenxinzhang

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).

5 thms2 active usersReviewed