The distance between rational numbers
Content created by Louis Wasserman and malarbol.
Created on 2025-04-23.
Last modified on 2025-05-19.
{-# OPTIONS --lossy-unification #-} module elementary-number-theory.distance-rational-numbers where
Imports
open import elementary-number-theory.absolute-value-rational-numbers open import elementary-number-theory.addition-rational-numbers open import elementary-number-theory.additive-group-of-rational-numbers open import elementary-number-theory.difference-rational-numbers open import elementary-number-theory.inequality-rational-numbers open import elementary-number-theory.maximum-rational-numbers open import elementary-number-theory.minimum-rational-numbers open import elementary-number-theory.multiplication-rational-numbers open import elementary-number-theory.nonnegative-rational-numbers open import elementary-number-theory.positive-rational-numbers open import elementary-number-theory.rational-numbers open import elementary-number-theory.strict-inequality-rational-numbers open import foundation.action-on-identifications-binary-functions open import foundation.action-on-identifications-functions open import foundation.coproduct-types open import foundation.dependent-pair-types open import foundation.identity-types open import foundation.logical-equivalences open import foundation.transport-along-identifications
Idea
The distance function¶ between rational numbers measures how far two rational numbers are apart.
dist-ℚ : ℚ → ℚ → ℚ⁰⁺ dist-ℚ p q = abs-ℚ (p -ℚ q) rational-dist-ℚ : ℚ → ℚ → ℚ rational-dist-ℚ p q = rational-ℚ⁰⁺ (dist-ℚ p q)
Properties
Commutativity
abstract commutative-dist-ℚ : (p q : ℚ) → dist-ℚ p q = dist-ℚ q p commutative-dist-ℚ p q = inv (abs-neg-ℚ _) ∙ ap abs-ℚ (distributive-neg-diff-ℚ _ _)
The differences of the arguments are less than or equal to their distance
abstract leq-diff-dist-ℚ : (p q : ℚ) → leq-ℚ (p -ℚ q) (rational-dist-ℚ p q) leq-diff-dist-ℚ p q = leq-abs-ℚ (p -ℚ q) leq-reversed-diff-dist-ℚ : (p q : ℚ) → leq-ℚ (q -ℚ p) (rational-dist-ℚ p q) leq-reversed-diff-dist-ℚ p q = tr ( leq-ℚ (q -ℚ p)) ( ap rational-ℚ⁰⁺ (commutative-dist-ℚ q p)) ( leq-diff-dist-ℚ q p)
Zero laws
abstract right-zero-law-dist-ℚ : (q : ℚ) → dist-ℚ q zero-ℚ = abs-ℚ q right-zero-law-dist-ℚ q = ap abs-ℚ (right-unit-law-add-ℚ _) left-zero-law-dist-ℚ : (q : ℚ) → dist-ℚ zero-ℚ q = abs-ℚ q left-zero-law-dist-ℚ q = commutative-dist-ℚ _ _ ∙ right-zero-law-dist-ℚ q
Distributivity laws
abstract left-distributive-abs-mul-dist-ℚ : (p q r : ℚ) → abs-ℚ p *ℚ⁰⁺ dist-ℚ q r = dist-ℚ (p *ℚ q) (p *ℚ r) left-distributive-abs-mul-dist-ℚ p q r = equational-reasoning abs-ℚ p *ℚ⁰⁺ dist-ℚ q r = abs-ℚ (p *ℚ (q -ℚ r)) by (inv (abs-mul-ℚ p (q -ℚ r))) = dist-ℚ (p *ℚ q) (p *ℚ r) by ap abs-ℚ (left-distributive-mul-diff-ℚ p q r) right-distributive-abs-mul-dist-ℚ : (p q r : ℚ) → dist-ℚ q r *ℚ⁰⁺ abs-ℚ p = dist-ℚ (q *ℚ p) (r *ℚ p) right-distributive-abs-mul-dist-ℚ p q r = equational-reasoning dist-ℚ q r *ℚ⁰⁺ abs-ℚ p = abs-ℚ p *ℚ⁰⁺ dist-ℚ q r by commutative-mul-ℚ⁰⁺ (dist-ℚ q r) (abs-ℚ p) = dist-ℚ (p *ℚ q) (p *ℚ r) by left-distributive-abs-mul-dist-ℚ p q r = dist-ℚ (q *ℚ p) (r *ℚ p) by ap-binary dist-ℚ (commutative-mul-ℚ p q) (commutative-mul-ℚ p r) left-distributive-mul-dist-ℚ : (p : ℚ⁰⁺) (q r : ℚ) → p *ℚ⁰⁺ dist-ℚ q r = dist-ℚ (rational-ℚ⁰⁺ p *ℚ q) (rational-ℚ⁰⁺ p *ℚ r) left-distributive-mul-dist-ℚ p⁰⁺@(p , _) q r = eq-ℚ⁰⁺ ( equational-reasoning p *ℚ rational-dist-ℚ q r = rational-abs-ℚ (p *ℚ (q -ℚ r)) by ap rational-ℚ⁰⁺ (inv (abs-left-mul-nonnegative-ℚ _ p⁰⁺)) = rational-abs-ℚ (p *ℚ q +ℚ p *ℚ (neg-ℚ r)) by ap rational-abs-ℚ (left-distributive-mul-add-ℚ p q (neg-ℚ r)) = rational-abs-ℚ (p *ℚ q -ℚ p *ℚ r) by ap rational-abs-ℚ (ap (p *ℚ q +ℚ_) (right-negative-law-mul-ℚ _ _))) right-distributive-mul-dist-ℚ : (p : ℚ⁰⁺) (q r : ℚ) → dist-ℚ q r *ℚ⁰⁺ p = dist-ℚ (q *ℚ rational-ℚ⁰⁺ p) (r *ℚ rational-ℚ⁰⁺ p) right-distributive-mul-dist-ℚ p⁰⁺@(p , _) q r = eq-ℚ⁰⁺ ( equational-reasoning rational-dist-ℚ q r *ℚ p = p *ℚ rational-dist-ℚ q r by commutative-mul-ℚ _ _ = rational-dist-ℚ (p *ℚ q) (p *ℚ r) by ap rational-ℚ⁰⁺ (left-distributive-mul-dist-ℚ p⁰⁺ q r) = rational-dist-ℚ (q *ℚ p) (r *ℚ p) by ap-binary ( rational-dist-ℚ) ( commutative-mul-ℚ _ _) ( commutative-mul-ℚ _ _))
Triangle inequality
abstract triangle-inequality-dist-ℚ : (p q r : ℚ) → leq-ℚ⁰⁺ (dist-ℚ p r) (dist-ℚ p q +ℚ⁰⁺ dist-ℚ q r) triangle-inequality-dist-ℚ p q r = tr ( λ s → leq-ℚ⁰⁺ s (dist-ℚ p q +ℚ⁰⁺ dist-ℚ q r)) ( ap abs-ℚ ( inv (associative-add-ℚ _ _ (neg-ℚ r)) ∙ ap (_-ℚ r) (is-section-diff-ℚ _ _))) ( triangle-inequality-abs-ℚ (p -ℚ q) (q -ℚ r))
Bounding the distance between rational numbers
abstract leq-dist-leq-diff-ℚ : (p q r : ℚ) → leq-ℚ (p -ℚ q) r → leq-ℚ (q -ℚ p) r → leq-ℚ (rational-dist-ℚ p q) r leq-dist-leq-diff-ℚ p q r p-q≤r q-p≤r = leq-abs-leq-leq-neg-ℚ ( p -ℚ q) ( r) ( p-q≤r) ( inv-tr (λ s → leq-ℚ s r) (distributive-neg-diff-ℚ p q) q-p≤r) le-dist-le-diff-ℚ : (p q r : ℚ) → le-ℚ (p -ℚ q) r → le-ℚ (q -ℚ p) r → le-ℚ (rational-dist-ℚ p q) r le-dist-le-diff-ℚ p q r p-q<r q-p<r = le-abs-le-le-neg-ℚ ( p -ℚ q) ( r) ( p-q<r) ( inv-tr (λ s → le-ℚ s r) (distributive-neg-diff-ℚ p q) q-p<r)
The distance between two rational numbers is the difference of their maximum and minimum
abstract eq-dist-diff-leq-ℚ : (p q : ℚ) → leq-ℚ p q → rational-dist-ℚ p q = q -ℚ p eq-dist-diff-leq-ℚ p q p≤q = equational-reasoning rational-dist-ℚ p q = rational-dist-ℚ q p by ap rational-ℚ⁰⁺ (commutative-dist-ℚ p q) = q -ℚ p by rational-abs-zero-leq-ℚ ( q -ℚ p) ( backward-implication (iff-translate-diff-leq-zero-ℚ p q) p≤q) eq-dist-diff-max-min-ℚ : (p q : ℚ) → rational-dist-ℚ p q = max-ℚ p q -ℚ min-ℚ p q eq-dist-diff-max-min-ℚ p q = rec-coproduct ( λ p≤q → equational-reasoning rational-dist-ℚ p q = q -ℚ p by eq-dist-diff-leq-ℚ p q p≤q = max-ℚ p q -ℚ min-ℚ p q by inv ( ap-diff-ℚ ( left-leq-right-max-ℚ p q p≤q) ( left-leq-right-min-ℚ p q p≤q))) ( λ q≤p → equational-reasoning rational-dist-ℚ p q = rational-dist-ℚ q p by ap rational-ℚ⁰⁺ (commutative-dist-ℚ p q) = p -ℚ q by eq-dist-diff-leq-ℚ q p q≤p = max-ℚ p q -ℚ min-ℚ p q by inv ( ap-diff-ℚ ( right-leq-left-max-ℚ p q q≤p) ( right-leq-left-min-ℚ p q q≤p))) ( linear-leq-ℚ p q)
Recent changes
- 2025-05-19. malarbol. Lipschitz-continuous functions between metric spaces (#1417).
- 2025-04-23. Louis Wasserman. Distance between rational numbers (#1400).