Reference · Signed rationals

rainbow.math.rational.signed.constrained-duality

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

Lagrangian duality with a CONCRETE penalty: an explicit finite constraint system with explicit multipliers. `rainbow.math.rational.signed.lagrangian-duality` proves weak duality, zero-gap optimality and complementary slackness from an abstract `penalty` function together with the hypothesis that the penalty is nonpositive on the feasible set. That hypothesis is the only thing standing between those theorems and an ordinary constrained program. Here it is discharged. Given an index type A, multipliers `lambda : A -> signed`, constraint functions `g : A -> signed -> signed` and an index list, the penalty is the finite sum penalty x = sum_i lambda_i * g_i x and `optimization/signed-constraint-penalty-nonpositive` derives its nonpositivity from the two ordinary side conditions of a Lagrangian relaxation: 0 <= lambda_i (dual feasibility, nonnegative multipliers) g_i x <= 0 (primal feasibility, satisfied constraints) termwise by the multiplicative sign rule, then through the sum by `signed/map-sum-nonpositive`. Composing gives optimization/signed-constrained-weak-duality optimization/signed-constrained-zero-gap-optimal -- weak duality and the primal optimality certificate for a genuine finite constraint system, with no abstract penalty left in the statement. Native and axiom-free; chains the signed finite-sum, multiplicative sign-rule and Lagrangian duality modules on D63.

Depends onmath.rational.signed.list-summath.rational.signed.multiply-ordermath.rational.signed.lagrangian-duality

optimization/signed-constraint-penalty-nonpositive.{u} :
  (A : Type u) (lambda : A → ℚ) (g : A → ℚ → ℚ) (idx : List A)
  (nonnegative : ∀ (i : A), 0 ≤ lambda i)
  (x : ℚ)
  (satisfied : ∀ (i : A), g i x ≤ 0)
  → Σ i∈idx, lambda i · g i x ≤ 0

optimization/signed-constrained-weak-duality.{u} :
  (A : Type u) (f : ℚ → ℚ) (lambda : A → ℚ) (g : A → ℚ → ℚ) (idx : List A)
  (feasible : ℚ → Prop) (dual : ℚ)
  (bound : ∀ (y : ℚ), dual ≤ f y + Σ i∈idx, lambda i · g i y)
  (nonnegative : ∀ (i : A), 0 ≤ lambda i)
  (satisfied : ∀ (y : ℚ), ∀ (member : feasible y), ∀ (i : A), g i y ≤ 0)
  (x : ℚ) (member : feasible x)
  → dual ≤ f x

optimization/signed-constrained-zero-gap-optimal.{u} :
  (A : Type u) (f : ℚ → ℚ) (lambda : A → ℚ) (g : A → ℚ → ℚ) (idx : List A)
  (feasible : ℚ → Prop) (dual : ℚ)
  (bound : ∀ (y : ℚ), dual ≤ f y + Σ i∈idx, lambda i · g i y)
  (nonnegative : ∀ (i : A), 0 ≤ lambda i)
  (satisfied : ∀ (y : ℚ), ∀ (member : feasible y), ∀ (i : A), g i y ≤ 0)
  (x0 : ℚ) (x0-member : feasible x0)
  (gap : dual = f x0)
  (x : ℚ) (member : feasible x)
  → f x0 ≤ f x