Finite inequality violation and quadratic penalty

Definition

VectorSpaceOpt_quadratic_penalty

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

definitioninequality-constraintpenalty-functionpositive-part

For a finite constraint vector z : Fin p → ℝ, positivePartVector z has component max 0 (z i). Given G : X → Fin p → ℝ, the scalar violation and feasibility predicates are

v(x)=∑_i (\max(0,G_i(x)))^2, \qquad x \text{ feasible }⇔ ∀i,\;G_i(x)≤0.

The quadratic exterior-penalty objective at weight K is f x + K * v x. These definitions exactly encode Luenberger's G⁺(x)·G⁺(x) for finite inequality systems and provide a reusable, nonnegative real-valued residual. They do not assume continuity, differentiability, convexity, or a norm on the decision type, allowing the algebraic estimates and later topological cluster-point arguments to share one interface.

Definition code

import Mathlib

open scoped BigOperators

namespace VectorSpaceOpt

/-- The componentwise positive part used to encode inequality violations. -/
def positivePartVector {p : ℕ} (z : Fin p → ℝ) : Fin p → ℝ :=
  fun i => max 0 (z i)

/-- The squared Euclidean violation of the inequalities `G x ≤ 0`. -/
def constraintViolation {X : Type*} {p : ℕ} (G : X → Fin p → ℝ) (x : X) : ℝ :=
  ∑ i, (positivePartVector (G x) i) ^ 2

/-- Feasibility for a finite family of scalar inequality constraints. -/
def IsConstraintFeasible {X : Type*} {p : ℕ} (G : X → Fin p → ℝ) (x : X) : Prop :=
  ∀ i, G x i ≤ 0

/-- The quadratic exterior-penalty objective `f(x) + K ‖G⁺(x)‖²`. -/
def quadraticPenaltyObjective {X : Type*} {p : ℕ}
    (f : X → ℝ) (G : X → Fin p → ℝ) (K : ℝ) (x : X) : ℝ :=
  f x + K * constraintViolation G x

end VectorSpaceOpt

Source

David G. Luenberger, Optimization by Vector Space Methods (Wiley, 1969), Chapter 10, §10.11, inequality-penalty definitions, printed p. 304 (physical PDF p. 322). Scan: https://sites.science.oregonstate.edu/~show/old/142_Luenberger.pdf

Read-back

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

positivePartVector. For any natural $p$ and vector $z:Fin(p)→ℝ$ , this is the vector whose $i$ th component is $max(0,z_i)$ . When $p=0$ it is the unique function on the empty index type.

constraintViolation. For any type $X$ , natural $p$ , constraint map $G:X→Fin(p)→ℝ$ , and $x∈X$ , this is the finite sum $∑_{i:Fin(p)}max(0,G(x)_i)^2$ . It is always nonnegative; for $p=0$ the empty sum is $0$ for every $x$ .

IsConstraintFeasible. For such $G$ and $x$ , feasibility means $G(x)_i≤0$ for every $i:Fin(p)$ . For $p=0$ this universal statement is vacuous, so every $x$ is feasible.

quadraticPenaltyObjective. For arbitrary $f:X→ℝ$ , $G$ , real $K$ , and $x$ , the value is $f(x)+K·∑_i max(0,G(x)_i)^2$ . The definition allows any real $K$ , including zero and negative values; positivity is imposed only by theorem hypotheses that explicitly state it.

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