Basic quadratic-penalty estimates

Proved

VectorSpaceOpt.quadratic_penalty_basic_estimates

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

global-minimizermonotonicitypenalty-methodweighted-violation

Let positive weights $K_n$ be nondecreasing and tend to infinity. Suppose $x^\ast$ is a feasible global minimizer of $f$ , and for every $n$ , $x_n$ globally minimizes $f + K_n * v$ . Then the attained penalty values are nondecreasing, every one is at most $f(x^\ast)$ , and the stronger weighted residual vanishes:

K_n v(x_n) → 0.

No topology, continuity, convergence, or convexity is assumed. This is exactly §10.11, Lemma 1, including its part 3 rather than the weaker consequence $v (x_n) → 0$ . The result supplies all numerical bounds consumed by the cluster-point theorem and can be reused for penalty sequences in any underlying decision type.

Preamble

import Definitions.Def_VectorSpaceOpt_quadratic_penalty

open Filter Set

Formal statement

namespace VectorSpaceOpt

/-- Luenberger, Chapter 10, §10.11, Lemma 1. -/
theorem quadratic_penalty_basic_estimates
    {X : Type*} {p : ℕ} (f : X → ℝ) (G : X → Fin p → ℝ)
    (K : ℕ → ℝ) (x : ℕ → X) (xStar : X)
    (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)) :
    Monotone (fun n => quadraticPenaltyObjective f G (K n) (x n)) ∧
      (∀ n, quadraticPenaltyObjective f G (K n) (x n) ≤ f xStar) ∧
      Tendsto (fun n => K n * constraintViolation G (x n)) atTop (nhds 0) := by
  sorry

end VectorSpaceOpt

Source

David G. Luenberger, Optimization by Vector Space Methods (Wiley, 1969), Chapter 10, §10.11, Lemma 1, printed p. 305 (physical PDF p. 323). 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 type, $p∈ℕ$ , $f:X→ℝ$ , $G:X→Fin(p)→ℝ$ , $K:ℕ→ℝ$ , $x:ℕ→X$ , and $x^*∈X$ . Assume $K_n>0$ for every $n$ , $K$ is nondecreasing, and $K_n$ tends to $+∞$ along the natural-number at-top filter, meaning it is eventually above every real bound. Assume $x^*$ is feasible, so $G(x^*)_i≤0$ for every $i$ , and globally minimizes $f$ over every feasible point. Assume also that, for every $n$ , $x_n$ globally minimizes over all $X$ the function $y↦f(y)+K_n∑_i max(0,G(y)_i)^2$ . Then the attained penalized values $f(x_n)+K_nV(x_n)$ form a nondecreasing sequence; each is at most $f(x^*)$ ; and the real sequence $K_nV(x_n)$ tends to $0$ , where $V(y)=∑_i max(0,G(y)_i)^2$ . The conclusion does not explicitly assert convergence of $x_n$ or of $V(x_n)$ itself. No topology on $X$ is assumed. For $p=0$ , $V≡0$ and feasibility is vacuous.

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