Reference · Non-negative rationals

rainbow.math.rational.nnrat.list-sum

Non-negative rationalssrc/rainbow/math/rational/nnrat/list_sum.clj1 definitions, 3 theorems

Finite sum of an nnrat-valued map over a list, and its monotonicity -- the n-ary generalization of nnrat/wsum2-monotone and the fold-level induction the scout flagged as the missing piece for dot-product / LP bounds: nnrat/map-sum A f xs = f x0 + f x1 + ... + f xn (empty sum = 0) nnrat/map-sum-monotone : (forall x, f x <= g x) -> map-sum f xs <= map-sum g xs Termwise domination lifts through a finite sum. This is the reusable engine behind: expected-value monotonicity (sum of weighted rewards), norm/penalty bounds (sum of nonneg terms), and dot-product monotonicity c.x <= c.x' when x is dominated coordinatewise -- hence LP weak-duality-style objective bounds. Proof: native List.rec fold of nnrat/add from nnrat/zero; monotonicity is a List.rec induction whose nil case is at-most-reflexive 0 and whose cons case is nnrat/add-monotone (f head <= g head, tail-sum <= tail-sum by the IH). Polymorphic in the element type A. Native and axiom-free; chains nnrat-add-monotone on d63.

Depends onmath.rational.nnrat.add-monotone

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

nnrat/map-sum-empty.{u} :
  (A : Type u) (f : A → ℚ≥0)
  → nnrat/map-sum A f [] = 0

nnrat/map-sum-cons.{u} :
  (A : Type u) (f : A → ℚ≥0) (head : A) (tail : List A)
  → nnrat/map-sum A f (data/cons A head tail) = f head + nnrat/map-sum A f tail

nnrat/map-sum-monotone.{u} :
  (A : Type u) (f g : A → ℚ≥0)
  (hfg : ∀ (x : A), f x ≤ g x)
  (xs : List A)
  → nnrat/map-sum A f xs ≤ nnrat/map-sum A g xs