Reference · Signed rationals

rainbow.math.rational.signed.lp-equality-row

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

Formal equality-row expansion into two signed inequality rows. Generic in the carrier, coefficient/value maps and finite index list. This proves the mathematical row relation, not host array append or free-price split.

Depends onmath.rational.signed.lp-objective-negate

signed/lp-equality-row-expand.{u} :
  (A : Type u) (a x : A → ℚ) (xs : List A) (b : ℚ)
  (same : Σ i∈xs, a i · x i = b)
  → proposition/conjunction (Σ i∈xs, a i · x i ≤ b) (Σ i∈xs, (fun i₁ => signed/negate (a i₁)) i · x i ≤ signed/negate b)

signed/lp-equality-row-contract.{u} :
  (A : Type u) (a x : A → ℚ) (xs : List A) (b : ℚ)
  (rows : proposition/conjunction (Σ i∈xs, a i · x i ≤ b) (Σ i∈xs, (fun i₁ => signed/negate (a i₁)) i · x i ≤ signed/negate b))
  → Σ i∈xs, a i · x i = b

signed/lp-equality-row-expansion-equivalence.{u} :
  (A : Type u) (a x : A → ℚ) (xs : List A) (b : ℚ)
  → proposition/equivalence (Σ i∈xs, a i · x i = b) (conjunction)
  where conjunction := proposition/conjunction (Σ i∈xs, a i · x i ≤ b) (Σ i∈xs, (fun i₁ => signed/negate (a i₁)) i · x i ≤ signed/negate b)