Reference · Signed rationals

rainbow.math.rational.signed.list-sum

Signed rationalssrc/rainbow/math/rational/signed/list_sum.clj1 definitions, 5 theorems

Finite sums of signed rationals over a list, and their order laws. signed/map-sum A f xs = f x0 + f x1 + ... + f xn (empty sum = 0) signed/map-sum-monotone : (forall x, f x <= g x) -> sum f xs <= sum g xs signed/map-sum-nonpositive : (forall x, f x <= 0) -> sum f xs <= 0 signed/map-sum-nonnegative : (forall x, 0 <= f x) -> 0 <= sum f xs The nnrat side already had `nnrat/map-sum`; the signed side had nothing, so every aggregate over signed quantities -- a Lagrangian penalty, a dot product, a total reward with sign -- had to stay abstract. These are the same List.rec folds: nil is order-reflexivity at `signed/zero`, cons is `signed/add-monotone` against the induction hypothesis, and the two sign versions additionally collapse the `0 + 0` produced in the cons step with `signed/add-zero-right`. Polymorphic in the index type. Native and axiom-free; chains signed order monotonicity and signed limit uniqueness (for signed/add-zero-right) on D63.

Depends onmath.rational.signed.limit-uniquenessmath.rational.signed.order-monotone

signed/map-sum.{u} :
  (A : Type u) (f : A → ℚ) (x₁ : List A)
  → ℚ

signed/map-sum-empty.{u} :
  (A : Type u) (f : A → ℚ)
  → Σ j∈[], f j = 0

signed/map-sum-cons.{u} :
  (A : Type u) (f : A → ℚ) (head : A) (tail : List A)
  → Σ j∈data/cons A head tail, f j = f head + Σ j∈tail, f j

signed/map-sum-monotone.{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-nonpositive.{u} :
  (A : Type u) (f : A → ℚ)
  (hf : ∀ (x : A), f x ≤ 0)
  (xs : List A)
  → Σ j∈xs, f j ≤ 0

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