Optimality of a feasible penalty cluster point

Proved

VectorSpaceOpt.penalty_cluster_point_optimal

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

cluster-pointglobal-minimumlower-semicontinuityoptimality

Let a subsequence of x n converge to a feasible point x₀, and let f be lower semicontinuous at x₀. Assume a feasible point xStar globally minimizes f on the constraint set and that f (x n) ≤ f xStar for every n. Then

f(x₀)=f(x^*)

and x₀ is itself a global constrained minimizer. This is the optimality half of the cluster-point argument on p. 306. It cleanly separates the lower-semicontinuous objective limit from feasibility recovery, and it states feasibility of both reference and limit points explicitly because Mathlib's IsMinOn predicate alone does not include set membership.

Preamble

import Definitions.Def_VectorSpaceOpt_quadratic_penalty

open Filter Set

Formal statement

namespace VectorSpaceOpt

/-- The optimality half of Luenberger, Chapter 10, §10.11, Theorem 1. -/
theorem penalty_cluster_point_optimal
    {X : Type*} [TopologicalSpace X] {p : ℕ} (f : X → ℝ)
    (G : X → Fin p → ℝ) (x : ℕ → X) (xStar x₀ : X) (phi : ℕ → ℕ)
    (hphi : StrictMono phi)
    (hxlim : Tendsto (x ∘ phi) atTop (nhds x₀))
    (hflsc : LowerSemicontinuousAt f x₀)
    (hupper : ∀ n, f (x n) ≤ f xStar)
    (hfeasStar : IsConstraintFeasible G xStar)
    (hminStar : IsMinOn f {y | IsConstraintFeasible G y} xStar)
    (hfeas₀ : 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, optimality part of 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)→ℝ$ , $x:ℕ→X$ , $x^*,x₀∈X$ , and $φ:ℕ→ℕ$ . Assume $φ$ is strictly increasing, $x_{φ(n)}$ tends to $x₀$ , $f$ is lower semicontinuous at $x₀$ , and $f(x_n)≤f(x^*)$ for every $n$ . Assume $G(x^*)_i≤0$ for every $i$ , $f(x^*)≤f(y)$ for every feasible $y$ with all $G(y)_i≤0$ , and $x₀$ itself is feasible. Then $f(x₀)=f(x^*)$ , and $f(x₀)≤f(y)$ for every feasible $y$ . No member $x_n$ is assumed feasible, and no relation to penalty parameters or penalized minimization is present in this theorem. The space need not be Hausdorff; for $p=0$ , 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