Reference · Signed rationals

rainbow.math.rational.signed.kkt-sufficiency

Signed rationalssrc/rainbow/math/rational/signed/kkt_sufficiency.clj0 definitions, 3 theorems

KKT sufficiency: a stationary, feasible, complementary point is a global optimum of a convex program. The Karush-Kuhn-Tucker conditions at a candidate `x0` are, in this presentation: STATIONARITY the Lagrangian L y = f y + penalty y has a supporting linear certificate at x0 that holds for every y (not only feasible y): L x0 + linear y <= L y, with 0 <= linear y. FEASIBILITY x0 is feasible, and the penalty is nonpositive on the feasible set (dual feasibility, lambda >= 0, plus constraint satisfaction). COMPLEMENTARITY penalty x0 ~ 0. The conclusion is global primal optimality: f x0 <= f x for every feasible x. No local search, no derivative calculus, no convexity of the feasible set is used -- only the order laws. The proof is exactly the composition of the two preceding modules. The first-order theorem turns stationarity into `x0 minimizes the Lagrangian globally`, which is precisely the hypothesis Lagrangian weak duality needs; weak duality then bounds every feasible objective value below by L x0, and complementarity rewrites L x0 as f x0. Native and axiom-free; chains signed convex optimality and signed Lagrangian duality on D63.

Depends onmath.rational.signed.convex-optimalitymath.rational.signed.lagrangian-duality

signed/add-left-respects-equivalence :
  (a b c : ℚ)
  (same : a = b)
  → c + a = c + b

optimization/signed-stationary-minimizes-lagrangian :
  (f penalty linear : ℚ → ℚ) (x0 : ℚ)
  (stationarity : ∀ (y : ℚ), f x0 + penalty x0 + linear y ≤ f y + penalty y)
  (variational : ∀ (y : ℚ), 0 ≤ linear y)
  (y : ℚ)
  → f x0 + penalty x0 ≤ f y + penalty y

optimization/signed-kkt-sufficiency :
  (f penalty linear : ℚ → ℚ) (feasible : ℚ → Prop) (x0 : ℚ)
  (stationarity : ∀ (y : ℚ), f x0 + penalty x0 + linear y ≤ f y + penalty y)
  (variational : ∀ (y : ℚ), 0 ≤ linear y)
  (slack : ∀ (y : ℚ), ∀ (member : feasible y), penalty y ≤ 0)
  (x0-member : feasible x0)
  (complementary : penalty x0 = 0)
  (x : ℚ) (member : feasible x)
  → f x0 ≤ f x