Quadratic penalty cluster-point convergence

Proved

VectorSpaceOpt.quadratic_penalty_cluster_point_converges

by wenxinzhang · Aug 25, 2026 · Mathlib c5ea003 (Lean v4.30.0)

cluster-pointconstrained-optimumlower-semicontinuityquadratic-penalty

Let $K_n > 0$ be nondecreasing with $K_n → +∞$ . Assume $x^\ast$ is a feasible global solution of the constrained problem and each $x_n$ globally minimizes the quadratic-penalty objective $f + K_n * v$ . If $f$ and the composite violation $v$ are lower semicontinuous and a strictly indexed subsequence $x ∘ \phi$ converges to $x₀$ , then

x₀ \text{ is feasible}, \qquad f(x₀)=f(x^*),

and $x₀$ globally minimizes $f$ over all feasible points. This is §10.11, Theorem 1 with “limit point” formalized explicitly. It assumes existence of penalty minimizers and a cluster point but does not assume convexity, differentiability, or convergence of the entire sequence.

Preamble

import Definitions.Def_VectorSpaceOpt_quadratic_penalty

open Filter Set

Formal statement

namespace VectorSpaceOpt

/-- Luenberger, Chapter 10, §10.11, Theorem 1. -/
theorem quadratic_penalty_cluster_point_converges
    {X : Type*} [TopologicalSpace X] {p : ℕ} (f : X → ℝ)
    (G : X → Fin p → ℝ) (K : ℕ → ℝ) (x : ℕ → X)
    (xStar x₀ : X) (phi : ℕ → ℕ)
    (hKpos : ∀ n, 0 < K n) (hKmono : Monotone K)
    (hKlim : Tendsto K atTop atTop)
    (hfeasStar : IsConstraintFeasible G xStar)
    (hminStar : IsMinOn f {y | IsConstraintFeasible G y} xStar)
    (hpenMin : ∀ n, IsMinOn (quadraticPenaltyObjective f G (K n)) Set.univ (x n))
    (hflsc : LowerSemicontinuous f)
    (hvlsc : LowerSemicontinuous (constraintViolation G))
    (hphi : StrictMono phi)
    (hxlim : Tendsto (x ∘ phi) atTop (nhds x₀)) :
    IsConstraintFeasible G x₀ ∧ f x₀ = f xStar ∧
      IsMinOn f {y | IsConstraintFeasible G y} x₀ := by
  sorry

end VectorSpaceOpt

Source

David G. Luenberger, Optimization by Vector Space Methods (Wiley, 1969), Chapter 10, §10.11, Theorem 1, printed p. 306 (physical PDF p. 324). Scan: https://sites.science.oregonstate.edu/~show/old/142_Luenberger.pdf

Read-back

What the Lean code literally says, in plain math · gpt-5

Let $X$ be an arbitrary topological space, $p∈ℕ$ , $f:X→ℝ$ , $G:X→Fin(p)→ℝ$ , $K:ℕ→ℝ$ , $x:ℕ→X$ , $x^*,x₀∈X$ , and $φ:ℕ→ℕ$ . Assume every $K_n>0$ , $K$ is nondecreasing, and $K_n→+∞$ along the natural-number at-top filter. Assume $x^*$ is feasible and globally minimizes $f$ over the feasible set; for every $n$ , $x_n$ globally minimizes $y↦f(y)+K_n∑_i max(0,G(y)_i)^2$ over all $X$ ; both $f$ and the violation function $V(y)=∑_i max(0,G(y)_i)^2$ are lower semicontinuous everywhere; $φ$ is strictly increasing; and the subsequence $x_{φ(n)}$ tends to $x₀$ . Then $x₀$ is feasible, $f(x₀)=f(x^*)$ , and $x₀$ globally minimizes $f$ over every feasible point. No Hausdorff, compactness, coercivity, or uniqueness hypothesis is imposed, so the conclusion concerns the supplied convergent subsequence only and does not assert convergence of the full sequence. For $p=0$ , the violation is identically zero and every point is feasible.

Human review

Endorsed by Shuze Chen · Aug 26, 2026
Endorsed by wenxinzhang · Aug 26, 2026
Confirmed by the mission captain (proposal self-audit).

View graph