Reference · Non-negative rationals

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

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

Distance of finite NNRAT sums is bounded by the sum of distances. Sum the two additive-closeness inequalities termwise, distribute map-sum over addition up to rational equivalence, and recover the distance bound. This needs neither a triangle axiom nor a signed-distance bridge. The list may be empty or contain duplicates; no normalization is required.

nnrat/map-sum-distance-bound-by.{u} :
  (A : Type u) (left right radius : A → ℚ≥0)
  (pointwise : ∀ (x : A), nnrat/distance (left x) (right x) ≤ radius x)
  (source : List A)
  → nnrat/distance (nnrat/map-sum A left source) (nnrat/map-sum A right source) ≤ nnrat/map-sum A radius source

nnrat/map-sum-distance-bound.{u} :
  (A : Type u) (left right : A → ℚ≥0) (source : List A)
  → nnrat/distance (nnrat/map-sum A left source) (nnrat/map-sum A right source) ≤ nnrat/map-sum A (fun x => nnrat/distance (left x) (right x)) source