The distance between rational numbers
Content created by Louis Wasserman.
Created on 2025-04-23.
Last modified on 2025-04-23.
{-# 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 open import metric-spaces.metric-space-of-rational-numbers open import metric-spaces.metric-space-of-rational-numbers-with-open-neighborhoods
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-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)
Relationship to the metric space of rational numbers
abstract leq-dist-neighborhood-leq-ℚ : (ε : ℚ⁺) (p q : ℚ) → neighborhood-leq-ℚ ε p q → leq-ℚ (rational-dist-ℚ p q) (rational-ℚ⁺ ε) leq-dist-neighborhood-leq-ℚ ε⁺@(ε , _) p q (H , K) = leq-dist-leq-diff-ℚ ( p) ( q) ( ε) ( swap-right-diff-leq-ℚ p ε q (leq-transpose-right-add-ℚ p q ε K)) ( swap-right-diff-leq-ℚ q ε p (leq-transpose-right-add-ℚ q p ε H)) neighborhood-leq-leq-dist-ℚ : (ε : ℚ⁺) (p q : ℚ) → leq-ℚ (rational-dist-ℚ p q) (rational-ℚ⁺ ε) → neighborhood-leq-ℚ ε p q neighborhood-leq-leq-dist-ℚ ε⁺@(ε , _) p q |p-q|≤ε = ( leq-transpose-left-diff-ℚ ( q) ( ε) ( p) ( swap-right-diff-leq-ℚ ( q) ( p) ( ε) ( transitive-leq-ℚ ( q -ℚ p) ( rational-dist-ℚ p q) ( ε) ( |p-q|≤ε) ( leq-reversed-diff-dist-ℚ p q)))) , ( leq-transpose-left-diff-ℚ ( p) ( ε) ( q) ( swap-right-diff-leq-ℚ ( p) ( q) ( ε) ( transitive-leq-ℚ ( p -ℚ q) ( rational-dist-ℚ p q) ( ε) ( |p-q|≤ε) ( leq-diff-dist-ℚ p q)))) leq-dist-iff-neighborhood-leq-ℚ : (ε : ℚ⁺) (p q : ℚ) → leq-ℚ (rational-dist-ℚ p q) (rational-ℚ⁺ ε) ↔ neighborhood-leq-ℚ ε p q pr1 (leq-dist-iff-neighborhood-leq-ℚ ε p q) = neighborhood-leq-leq-dist-ℚ ε p q pr2 (leq-dist-iff-neighborhood-leq-ℚ ε p q) = leq-dist-neighborhood-leq-ℚ ε p q
Relationship to the metric space of rational numbers with open neighborhoods
abstract le-dist-neighborhood-le-ℚ : (ε : ℚ⁺) (p q : ℚ) → neighborhood-le-ℚ ε p q → le-ℚ (rational-dist-ℚ p q) (rational-ℚ⁺ ε) le-dist-neighborhood-le-ℚ ε⁺@(ε , _) p q (H , K) = le-dist-le-diff-ℚ ( p) ( q) ( ε) ( swap-right-diff-le-ℚ p ε q (le-transpose-right-add-ℚ p q ε K)) ( swap-right-diff-le-ℚ q ε p (le-transpose-right-add-ℚ q p ε H)) neighborhood-le-le-dist-ℚ : (ε : ℚ⁺) (p q : ℚ) → le-ℚ (rational-dist-ℚ p q) (rational-ℚ⁺ ε) → neighborhood-le-ℚ ε p q neighborhood-le-le-dist-ℚ ε⁺@(ε , _) p q |p-q|<ε = ( le-transpose-left-diff-ℚ ( q) ( ε) ( p) ( swap-right-diff-le-ℚ ( q) ( p) ( ε) ( concatenate-leq-le-ℚ ( q -ℚ p) ( rational-dist-ℚ p q) ( ε) ( leq-reversed-diff-dist-ℚ p q) ( |p-q|<ε)))) , ( le-transpose-left-diff-ℚ ( p) ( ε) ( q) ( swap-right-diff-le-ℚ ( p) ( q) ( ε) ( concatenate-leq-le-ℚ ( p -ℚ q) ( rational-dist-ℚ p q) ( ε) ( leq-diff-dist-ℚ p q) ( |p-q|<ε)))) le-dist-iff-neighborhood-le-ℚ : (ε : ℚ⁺) (p q : ℚ) → le-ℚ (rational-dist-ℚ p q) (rational-ℚ⁺ ε) ↔ neighborhood-le-ℚ ε p q pr1 (le-dist-iff-neighborhood-le-ℚ ε p q) = neighborhood-le-le-dist-ℚ ε p q pr2 (le-dist-iff-neighborhood-le-ℚ ε p q) = le-dist-neighborhood-le-ℚ ε p q
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-04-23. Louis Wasserman. Distance between rational numbers (#1400).