Feasibility of a penalty cluster point

Proved

VectorSpaceOpt.penalty_cluster_point_feasible

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

cluster-pointfeasibilitylower-semicontinuitysubsequence

Let x₀ be the limit of a subsequence x ∘ phi, where phi is strictly increasing. Suppose the scalar constraint violation v is lower semicontinuous at x₀ and v (x n) tends to zero along the original sequence. Then x₀ is feasible:

∀ i,\; G_i(x₀)≤0.

Lower semicontinuity forces v x₀ ≤ 0, while the finite sum-of-squares definition is nonnegative and vanishes exactly when every positive part is zero. The theorem isolates the feasibility half of §10.11, Theorem 1 and makes the source's phrase “limit point” precise through an explicit convergent subsequence rather than assuming convergence of the full penalty-minimizer sequence.

Preamble

import Definitions.Def_VectorSpaceOpt_quadratic_penalty

open Filter

Formal statement

namespace VectorSpaceOpt

/-- The feasibility half of Luenberger, Chapter 10, §10.11, Theorem 1. -/
theorem penalty_cluster_point_feasible
    {X : Type*} [TopologicalSpace X] {p : ℕ} (G : X → Fin p → ℝ)
    (x : ℕ → X) (x₀ : X) (phi : ℕ → ℕ)
    (hphi : StrictMono phi)
    (hxlim : Tendsto (x ∘ phi) atTop (nhds x₀))
    (hvlsc : LowerSemicontinuousAt (constraintViolation G) x₀)
    (hvlim : Tendsto (fun n => constraintViolation G (x n)) atTop (nhds 0)) :
    IsConstraintFeasible G x₀ := by
  sorry

end VectorSpaceOpt

Source

David G. Luenberger, Optimization by Vector Space Methods (Wiley, 1969), Chapter 10, §10.11, feasibility 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∈ℕ$ , $G:X→Fin(p)→ℝ$ , $x:ℕ→X$ , $x₀∈X$ , and $φ:ℕ→ℕ$ . Assume $φ$ is strictly increasing, the subsequence $x_{φ(n)}$ tends to $x₀$ along the natural-number at-top filter, the function $V(y)=∑_{i:Fin(p)}max(0,G(y)_i)^2$ is lower semicontinuous at $x₀$ , and the full real sequence $V(x_n)$ tends to $0$ . Then $G(x₀)_i≤0$ for every $i:Fin(p)$ . The topology on $X$ need not be Hausdorff and no continuity of $G$ itself is assumed. For $p=0$ , $V$ is identically zero and the feasibility conclusion 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