Reference · Signed rationals

rainbow.math.rational.signed.lagrangian-duality

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

Lagrangian duality for general constrained optimization over signed rationals. A constrained program `minimize f x subject to x feasible` is relaxed by moving the constraints into the objective with nonnegative multipliers: L y = f y + penalty y, penalty y = sum_i lambda_i * g_i y. Two facts characterize the relaxation, and both are taken as hypotheses so that no signed multiplication or constraint-list representation has to be postulated here: * `bound` -- the dual value is a lower bound of the Lagrangian everywhere: dual-value <= f y + penalty y for every y. (This is what `dual-value <= inf_y L y` means.) * `slack` -- on the feasible set the penalty is never a bonus: penalty x <= 0. Over a real program this is exactly lambda_i >= 0 together with g_i x <= 0. From these three theorems follow. WEAK DUALITY dual-value <= f x for every feasible x, so every dual value certifies a lower bound on the primal optimum -- the reason a branch-and-bound node may be pruned, and the reason a relaxation is sound. ZERO-GAP OPTIMALITY if some feasible x0 attains the dual value, it is a global primal minimizer. This is the certificate a solver emits: a primal point plus a dual value that match. COMPLEMENTARY SLACKNESS at such a zero-gap pair the penalty vanishes: penalty x0 ~ 0. Every active multiplier sits on an active constraint. This generalizes the nnrat LP duality stack to arbitrary signed objectives: nothing here assumes linearity, only order. Native and axiom-free; chains signed limit uniqueness (add-zero-right, antisymmetry), signed order monotonicity and signed order cancellation on D63.

Depends onmath.rational.signed.limit-uniquenessmath.rational.signed.order-monotonemath.rational.signed.order-cancellation

optimization/signed-lagrangian-weak-duality :
  (f penalty : ℚ → ℚ) (feasible : ℚ → Prop) (dual : ℚ)
  (bound : ∀ (y : ℚ), dual ≤ f y + penalty y)
  (slack : ∀ (y : ℚ), ∀ (member : feasible y), penalty y ≤ 0)
  (x : ℚ) (member : feasible x)
  → dual ≤ f x

optimization/signed-lagrangian-zero-gap-primal-optimal :
  (f penalty : ℚ → ℚ) (feasible : ℚ → Prop) (dual : ℚ)
  (bound : ∀ (y : ℚ), dual ≤ f y + penalty y)
  (slack : ∀ (y : ℚ), ∀ (member : feasible y), penalty y ≤ 0)
  (x0 : ℚ) (x0-member : feasible x0)
  (gap : dual = f x0)
  (x : ℚ) (member : feasible x)
  → f x0 ≤ f x

optimization/signed-lagrangian-complementary-slackness :
  (f penalty : ℚ → ℚ) (feasible : ℚ → Prop) (dual : ℚ)
  (bound : ∀ (y : ℚ), dual ≤ f y + penalty y)
  (slack : ∀ (y : ℚ), ∀ (member : feasible y), penalty y ≤ 0)
  (x0 : ℚ) (x0-member : feasible x0)
  (gap : dual = f x0)
  → penalty x0 = 0