Reference · Signed rationals

rainbow.math.rational.signed.lp-objective-negate

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

Generic finite-sum negation and formal LP minimization sense transport. Covers arbitrary carriers and finite lists, including empty/repeated indices. Does not identify a host mapv-negation with the formal mapping without evidence.

Depends onmath.rational.signed.map-sum-algebramath.rational.nnrat.ringmath.rational.signed.equivalence-lawsmath.rational.signed.negate-additivemath.rational.signed.deviation-rowsmath.rational.signed.order-respects

signed/map-sum-negate.{u} :
  (A : Type u) (m : A → ℚ) (xs : List A)
  → Σ i∈xs, signed/negate (m i) = signed/negate (Σ j∈xs, m j)

signed/lp-objective-negate.{u} :
  (A : Type u) (c x : A → ℚ) (xs : List A)
  → Σ i∈xs, (fun i₁ => signed/negate (c i₁)) i · x i = signed/negate (Σ i∈xs, c i · x i)

signed/lp-negated-objective-bound-to-lower.{u} :
  (A : Type u) (c x : A → ℚ) (xs : List A) (lower : ℚ)
  (ordered : Σ i∈xs, (fun i₁ => signed/negate (c i₁)) i · x i ≤ signed/negate lower)
  → lower ≤ Σ i∈xs, c i · x i