Reference · Non-negative rationals

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

Non-negative rationalssrc/rainbow/math/rational/nnrat/map_sum_append.clj0 definitions, 1 theorems

Finite nnrat sums split over list concatenation, up to nnrat equivalence (~): nnrat/map-sum-append : map-sum f (append xs ys) ~ map-sum f xs + map-sum f ys The block/partition-decomposition law: the sum over a concatenated index list is the sum of the block sums. Reusable for LP column generation (append new columns), expectation over a partitioned sample space, and any divide-and-sum. Proof: List.rec induction on xs (list/append reduces definitionally on its left argument); nil case is add-zero-left, cons case is add-associative plus add-respects-equivalence and the IH. Polymorphic in the element type. Native and axiom-free; chains nnrat-list-sum, nnrat-additive-reassociation, nnrat-identities on d63.

Depends onmath.rational.nnrat.list-summath.rational.nnrat.additive-reassociationmath.rational.nnrat.identities

nnrat/map-sum-append.{u} :
  (A : Type u) (f : A → ℚ≥0) (xs ys : List A)
  → nnrat/map-sum A f (list/append A xs ys) = nnrat/map-sum A f xs + nnrat/map-sum A f ys