Reference · Non-negative rationals

rainbow.math.rational.nnrat.metric-separation

Non-negative rationalssrc/rainbow/math/rational/nnrat/metric_separation.clj0 definitions, 14 theorems

Exact separation for the computational NNRAT distance and finite radius. The raw NNRAT representation is a quotient presentation, so metric separation concludes `nnrat/equivalent`, not structural equality. Scalar distance is zero exactly when its endpoints are equivalent. The finite supremum radius is zero exactly when the functions are pointwise equivalent on every enumerated member; no claim is made outside that finite support. The distance is also a congruence for the quotient: replacing either endpoint by an equivalent value keeps the distance equivalent. Native, kernel-checked, and axiom-free on D63.

nnrat/at-most-antisymmetric :
  (left right : ℚ≥0)
  (left-right : left ≤ right)
  (right-left : right ≤ left)
  → left = right

nnrat/distance-at-most-zero-of-equivalent :
  (left right : ℚ≥0)
  (same : left = right)
  → nnrat/distance left right ≤ 0

nnrat/distance-zero-of-equivalent :
  (left right : ℚ≥0)
  (same : left = right)
  → nnrat/distance left right = 0

nnrat/equivalent-of-distance-at-most-zero :
  (left right : ℚ≥0)
  (distance-at-most-zero : nnrat/distance left right ≤ 0)
  → left = right

nnrat/equivalent-of-distance-zero :
  (left right : ℚ≥0)
  (distance-zero : nnrat/distance left right = 0)
  → left = right

nnrat/distance-zero-iff-equivalent :
  (left right : ℚ≥0)
  → proposition/conjunction (nnrat/distance left right = 0 → left = right) (left = right → nnrat/distance left right = 0)

nnrat/distance-respects-equivalence :
  (left equivalent-left right equivalent-right : ℚ≥0)
  (same-left : left = equivalent-left)
  (same-right : right = equivalent-right)
  → nnrat/distance left right = nnrat/distance equivalent-left equivalent-right

nnrat/distance-add-subadditive :
  (a b c d : ℚ≥0)
  → nnrat/distance (a + b) (c + d) ≤ nnrat/distance a c + nnrat/distance b d

nnrat/distance-multiply-left-bound :
  (factor left right : ℚ≥0)
  → nnrat/distance (factor · left) (factor · right) ≤ factor · nnrat/distance left right

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

nnrat/map-sum-monotone-on.{u} :
  (A : Type u) (f g : A → ℚ≥0) (items : List A)
  (bounded : ∀ (value : A), ∀ (member : list/membership A items value), f value ≤ g value)
  → nnrat/map-sum A f items ≤ nnrat/map-sum A g items

metric/finite-nnrat-sup-radius-zero-of-pointwise-equivalent.{u} :
  (A : Type u) (source : Finset A) (left right : A → ℚ≥0)
  (pointwise : ∀ (state : A), ∀ (member : state ∈ source), left state = right state)
  → max s∈source |left s - right s| = 0

metric/pointwise-equivalent-of-finite-nnrat-sup-radius-zero.{u} :
  (A : Type u) (source : Finset A) (left right : A → ℚ≥0)
  (radius-zero : max s∈source |left s - right s| = 0)
  (state : A)
  (member : state ∈ source)
  → left state = right state

metric/finite-nnrat-sup-radius-zero-iff-pointwise-equivalent.{u} :
  (A : Type u) (source : Finset A) (left right : A → ℚ≥0)
  → proposition/conjunction (max s∈source |left s - right s| = 0 → (∀ (state : A), ∀ (member : state ∈ source), left state = right state)) ((∀ (state : A), ∀ (member : state ∈ source), left state = right state) → max s∈source |left s - right s| = 0)