Reference · Signed rationals

rainbow.math.rational.signed.map-sum-scale

Signed rationalssrc/rainbow/math/rational/signed/map_sum_scale.clj0 definitions, 4 theorems

Nonnegative-rational scaling of signed indexed sums and bilinear objectives. Produces the endpoint equivalences for formal LP D^2/D scaling, including empty and repeated-index lists. Host-language input transformation is not identified with this formal expression without a separate correspondence.

Depends onmath.rational.signed.map-sum-algebramath.rational.signed.scale-additive

signed/map-sum-nnrat-scale.{u} :
  (A : Type u) (c : ℚ≥0) (mapping : A → ℚ) (xs : List A)
  → Σ i∈xs, signed/scale c (mapping i) = signed/scale c (Σ j∈xs, mapping j)

signed/multiply-scaled-factors :
  (a b : ℚ≥0) (x y : ℚ)
  → signed/scale a x · signed/scale b y = signed/scale (a · b) (x · y)

signed/map-sum-biscaled-products.{u} :
  (A : Type u) (a b : ℚ≥0) (left right : A → ℚ) (xs : List A)
  → Σ i∈xs, (fun i₁ => signed/scale a (left i₁)) i · (fun i₁ => signed/scale b (right i₁)) i = signed/scale (a · b) (Σ i∈xs, left i · right i)

signed/lp-objective-cubic-scale.{u} :
  (A : Type u) (d : ℚ≥0) (coefficients values : A → ℚ) (indices : List A)
  → Σ i∈indices, (fun i₁ => signed/scale (d · d) (coefficients i₁)) i · (fun i₁ => signed/scale d (values i₁)) i = signed/scale (d · d · d) (Σ i∈indices, coefficients i · values i)