Reference · Signed rationals

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

Signed rationalssrc/rainbow/math/rational/signed/map_sum_algebra.clj0 definitions, 7 theorems

Algebra of signed finite sums: congruence, splitting, and the weighted bound. signed/add-respects-equivalence : a~a' -> b~b' -> a+b ~ a'+b' signed/add-four-reorder : (a+b)+(c+d) ~ (a+c)+(b+d) signed/map-sum-respects-equivalence : pointwise ~ lifts to the sum signed/map-sum-zero : a sum of zeros ~ 0 signed/map-sum-add : sum of (f+g) ~ sum f + sum g signed/weighted-sum-monotone : nonnegative weights preserve <= Signed addition, like nnrat addition, is associative and commutative only up to equivalence -- (a+b)+c and a+(b+c) are different Grothendieck pairs -- so every regrouping law here is stated with `signed/equivalent` and the two reorderings are proved componentwise from `nnrat/add-four-reorder`. `signed/weighted-sum-monotone` is the headline: with nonnegative weights, termwise domination survives weighting and summation. That is the signed analogue of `nnrat/weighted-sum-monotone`, and it is what bounds a signed objective by a signed dual expression -- the leg of any linear-programming or expectation bound whose data may be negative. It is only reachable now that `signed/multiply-left-monotone` exists to scale a single term. Native and axiom-free; chains signed finite sums and signed multiplicative monotonicity on D63.

Depends onmath.rational.signed.list-summath.rational.signed.multiply-monotonemath.rational.signed.unit-laws

signed/add-respects-equivalence :
  (a ah b bh : ℚ)
  (same-a : a = ah)
  (same-b : b = bh)
  → a + b = ah + bh

signed/add-four-reorder :
  (a b c d : ℚ)
  → a + b + (c + d) = a + c + (b + d)

signed/equivalent-transitive :
  (a b c : ℚ)
  (ab : a = b)
  (bc : b = c)
  → a = c

signed/map-sum-respects-equivalence.{u} :
  (A : Type u) (f g : A → ℚ)
  (hfg : ∀ (x : A), f x = g x)
  (xs : List A)
  → Σ j∈xs, f j = Σ j∈xs, g j

signed/map-sum-zero.{u} :
  (A : Type u) (f : A → ℚ)
  (hf : ∀ (x : A), f x = 0)
  (xs : List A)
  → Σ j∈xs, f j = 0

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

signed/weighted-sum-monotone.{u} :
  (A : Type u) (w x y : A → ℚ)
  (hw : ∀ (i : A), 0 ≤ w i)
  (hxy : ∀ (i : A), x i ≤ y i)
  (idx : List A)
  → Σ i∈idx, w i · x i ≤ Σ i∈idx, w i · y i