Reference · Signed rationals

rainbow.math.rational.signed.lp-scaling-bound

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

Transport a bound between formal D^2/D-scaled objectives to original sums. A positive rational D is cancelled three times, avoiding an assumed positive representation of D^3. No endpoint-equivalence premise is assumed. This is an objective inequality theorem, not a feasibility or host-code theorem.

Depends onmath.rational.signed.scale-reflectionmath.rational.signed.map-sum-scale

signed/scale-positive-cube-reflects-order :
  (ap adp : ℕ) (left right : ℚ)
  (ordered : signed/scale (nnrat/make (data/succ ap) adp · nnrat/make (data/succ ap) adp · nnrat/make (data/succ ap) adp) left ≤ signed/scale (nnrat/make (data/succ ap) adp · nnrat/make (data/succ ap) adp · nnrat/make (data/succ ap) adp) right)
  → left ≤ right

signed/lp-scaled-objectives-bound.{u} :
  (A : Type u) (ap adp : ℕ) (margins plan capacities prices : A → ℚ)
  (columns rows : List A)
  (scaled-bound : Σ i∈columns, signed/scale (nnrat/make (data/succ ap) adp · nnrat/make (data/succ ap) adp) (margins i) · signed/scale (nnrat/make (data/succ ap) adp) (plan i) ≤ Σ i∈rows, signed/scale (nnrat/make (data/succ ap) adp · nnrat/make (data/succ ap) adp) (capacities i) · signed/scale (nnrat/make (data/succ ap) adp) (prices i))
  → Σ i∈columns, margins i · plan i ≤ Σ i∈rows, capacities i · prices i