Reference · Signed rationals

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

Signed rationalssrc/rainbow/math/rational/signed/lp_equality_row_transport.clj0 definitions, 2 theorems

Generic feasibility transport from an original equality to certified actual positive/negative row maps and RHS entries. All candidates, arbitrary finite index lists; no sign, distinctness or nonemptiness assumptions.

Depends onmath.rational.signed.lp-equality-rowmath.rational.signed.multiply-ring

signed/lp-actual-equality-row-equivalence.{u} :
  (A : Type u) (original positive negative : A → ℚ) (indices : List A)
  (rhs positive-rhs negative-rhs : ℚ)
  (positive-same : ∀ (i : A), positive i = original i)
  (negative-same : ∀ (i : A), negative i = signed/negate (original i))
  (positive-rhs-same : positive-rhs = rhs)
  (negative-rhs-same : negative-rhs = signed/negate rhs)
  (candidate : A → ℚ)
  → proposition/equivalence (Σ i∈indices, original i · candidate i = rhs) (conjunction)
  where conjunction := proposition/conjunction (Σ i∈indices, positive i · candidate i ≤ positive-rhs) (Σ i∈indices, negative i · candidate i ≤ negative-rhs)

signed/lp-actual-inequality-row-equivalence.{u} :
  (A : Type u) (original actual : A → ℚ) (indices : List A) (rhs actual-rhs : ℚ)
  (same : ∀ (i : A), actual i = original i)
  (rhs-same : actual-rhs = rhs)
  (candidate : A → ℚ)
  → proposition/equivalence (Σ i∈indices, original i · candidate i ≤ rhs) (Σ i∈indices, actual i · candidate i ≤ actual-rhs)