Reference · Non-negative rationals

rainbow.math.rational.nnrat.map-sum-additive

Non-negative rationalssrc/rainbow/math/rational/nnrat/map_sum_additive.clj0 definitions, 2 theorems

Additive congruences for nnrat/map-sum, up to nnrat equivalence (~) -- the Fubini prerequisites. nnrat addition only associates/commutes up to ~ (the groupings give equal-by-nat-identity but syntactically distinct denominators), so these are equivalences, bridged to <= later by at-most-respects-equivalence: nnrat/map-sum-zero : map-sum (\_.0) is ~ 0 nnrat/map-sum-add : map-sum (\i. f i + g i) is ~ map-sum f is + map-sum g is Both by List.rec induction: nil is reflexive (empty sum reduces to 0); the cons case pushes the head term out with nnrat/add-respects-equivalence + the IH and, for map-sum-add, the four-term reorder (a+b)+(c+d) ~ (a+c)+(b+d). Polymorphic in the element type. Native and axiom-free; chains nnrat-list-sum and nnrat-additive-reassociation on d63.

Depends onmath.rational.nnrat.list-summath.rational.nnrat.additive-reassociation

nnrat/map-sum-zero.{u} :
  (A : Type u) (is : List A)
  → nnrat/map-sum A (fun x₃ => 0) is = 0

nnrat/map-sum-add.{u} :
  (A : Type u) (f g : A → ℚ≥0) (is : List A)
  → nnrat/map-sum A (fun i => f i + g i) is = nnrat/map-sum A f is + nnrat/map-sum A g is