Prove2Me

Local cone-optimization vocabulary

Definition
VectorSpaceOpt_cone_optimization

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

constraint-qualificationconvex-conedefinitiongateaux-derivative

For normed real spaces, HasGateauxDerivAt F F' x means that every affine line t ↦ F (x + t h) is differentiable at zero with derivative F' h. For a convex cone P, coneLT P z₁ z₂ means that z₂ - z₁ lies in the topological interior of P. Finally, IsConeRegularAt P G G' x combines feasibility with a strict linearized-feasibility direction:

Gx≤p0∧∃h,  Gx+G′h<p0.Gx ≤ₚ 0 \quad∧\quad ∃h,\; Gx+G'h <ₚ 0.

These definitions expose exactly the differentiability and regular-point notions used in §9.4. The file imports, rather than redefines, the earlier mission's coneLE and dualPositive constants so multiplier and order conventions remain shared across the series.

Definition code
import Mathlib
import Definitions.Def_VectorSpaceOpt_coneLE
import Definitions.Def_VectorSpaceOpt_dualPositive

open Set Filter

namespace VectorSpaceOpt

/-- A linear Gâteaux derivative, expressed by differentiating every affine line. -/
def HasGateauxDerivAt
    {X Y : Type*} [NormedAddCommGroup X] [NormedSpace ℝ X]
    [NormedAddCommGroup Y] [NormedSpace ℝ Y]
    (F : X → Y) (F' : X →L[ℝ] Y) (x : X) : Prop :=
  ∀ h : X, HasDerivAt (fun t : ℝ => F (x + t • h)) (F' h) 0

/-- Strict cone order, using the topological interior of the positive cone. -/
def coneLT
    {Z : Type*} [NormedAddCommGroup Z] [NormedSpace ℝ Z]
    (P : ConvexCone ℝ Z) (x y : Z) : Prop :=
  y - x ∈ interior (P : Set Z)

/-- Luenberger's regularity condition for the inequality `G x ≤ 0`. -/
def IsConeRegularAt
    {X Z : Type*} [NormedAddCommGroup X] [NormedSpace ℝ X]
    [NormedAddCommGroup Z] [NormedSpace ℝ Z]
    (P : ConvexCone ℝ Z) (G : X → Z) (G' : X →L[ℝ] Z) (x : X) : Prop :=
  coneLE P (G x) 0 ∧ ∃ h : X, coneLT P (G x + G' h) 0

end VectorSpaceOpt
Source
David G. Luenberger, Optimization by Vector Space Methods (Wiley, 1969), Chapter 9, §9.4, regular-point definition and surrounding notation, printed pp. 248–249 (physical PDF pp. 266–267). Scan: https://sites.science.oregonstate.edu/~show/old/142_Luenberger.pdf
Read-back

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

HasGateauxDerivAt. For real normed spaces X,YX,Y, a map F:X→YF:X→Y, a continuous real-linear map F′:X→YF':X→Y, and a point x∈Xx∈X, this means that for every direction h∈Xh∈X, the one-variable curve t↦F(x+th)t↦F(x+th) has derivative F′hF'h at the real parameter t=0t=0. The quantification is over every direction, including h=0h=0; completeness and continuity of F′F' as a function of the base point are not additional hypotheses.

coneLT. For a convex cone PP in a real normed space ZZ, the strict relation x<Pyx<_{P}y is defined to mean y−x∈interior(P)y-x∈interior(P), where the interior is taken in the topology of ZZ. Thus it can be empty, in which case no strict comparison holds.

IsConeRegularAt. For real normed spaces X,ZX,Z, a convex cone P⊆ZP⊆Z, a map G:X→ZG:X→Z, a continuous real-linear G′:X→ZG':X→Z, and x∈Xx∈X, regularity means both that G(x)≤P0G(x)≤_{P}0—equivalently, under the imported cone order, −G(x)∈P-G(x)∈P—and that there exists h∈Xh∈X for which G(x)+G′h<P0G(x)+G'h<_{P}0, meaning −(G(x)+G′h)∈interior(P)-(G(x)+G'h)∈interior(P). This is an existential condition on one direction and includes feasibility as a separate conjunct.

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