Reference · Non-negative rationals

rainbow.math.rational.nnrat.shared-residual-mass

Non-negative rationalssrc/rainbow/math/rational/nnrat/shared_residual_mass.clj2 definitions, 5 theorems

Canonical common/residual decomposition, computed without choice. c=min(a,b), p=distance(c,a), q=distance(c,b). Then c+p~a, c+q~b, at least one residual is zero, and distance(a,b)~p+q.

Depends onmath.rational.nnrat.distance-translationmath.rational.nnrat.ordered-distancemath.rational.nnrat.minmax

nnrat/left-residual-mass :
  (a b : ℚ≥0)
  → ℚ≥0

nnrat/right-residual-mass :
  (a b : ℚ≥0)
  → ℚ≥0

nnrat/shared-plus-left-residual :
  (a b : ℚ≥0)
  → minmax/min a b + nnrat/left-residual-mass a b = a

nnrat/shared-plus-right-residual :
  (a b : ℚ≥0)
  → minmax/min a b + nnrat/right-residual-mass a b = b

nnrat/residual-masses-disjoint :
  (a b : ℚ≥0)
  → proposition/disjunction (nnrat/distance (minmax/min a b) a = 0) (nnrat/distance (minmax/min a b) b = 0)

nnrat/residual-masses-preserve-distance :
  (a b : ℚ≥0)
  → nnrat/distance (nnrat/left-residual-mass a b) (nnrat/right-residual-mass a b) = nnrat/distance a b

nnrat/distance-is-residual-mass-sum :
  (a b : ℚ≥0)
  → nnrat/distance a b = nnrat/distance (minmax/min a b) a + nnrat/distance (minmax/min a b) b