|
| 1 | +# The distance between rational numbers |
| 2 | + |
| 3 | +```agda |
| 4 | +{-# OPTIONS --lossy-unification #-} |
| 5 | +
|
| 6 | +module elementary-number-theory.distance-rational-numbers where |
| 7 | +``` |
| 8 | + |
| 9 | +<details><summary>Imports</summary> |
| 10 | + |
| 11 | +```agda |
| 12 | +open import elementary-number-theory.absolute-value-rational-numbers |
| 13 | +open import elementary-number-theory.addition-rational-numbers |
| 14 | +open import elementary-number-theory.additive-group-of-rational-numbers |
| 15 | +open import elementary-number-theory.difference-rational-numbers |
| 16 | +open import elementary-number-theory.inequality-rational-numbers |
| 17 | +open import elementary-number-theory.maximum-rational-numbers |
| 18 | +open import elementary-number-theory.minimum-rational-numbers |
| 19 | +open import elementary-number-theory.multiplication-rational-numbers |
| 20 | +open import elementary-number-theory.nonnegative-rational-numbers |
| 21 | +open import elementary-number-theory.positive-rational-numbers |
| 22 | +open import elementary-number-theory.rational-numbers |
| 23 | +open import elementary-number-theory.strict-inequality-rational-numbers |
| 24 | +
|
| 25 | +open import foundation.action-on-identifications-binary-functions |
| 26 | +open import foundation.action-on-identifications-functions |
| 27 | +open import foundation.coproduct-types |
| 28 | +open import foundation.dependent-pair-types |
| 29 | +open import foundation.identity-types |
| 30 | +open import foundation.logical-equivalences |
| 31 | +open import foundation.transport-along-identifications |
| 32 | +
|
| 33 | +open import metric-spaces.metric-space-of-rational-numbers |
| 34 | +open import metric-spaces.metric-space-of-rational-numbers-with-open-neighborhoods |
| 35 | +``` |
| 36 | + |
| 37 | +</details> |
| 38 | + |
| 39 | +## Idea |
| 40 | + |
| 41 | +The |
| 42 | +{{#concept "distance function" Disambiguation="between rational numbers" Agda=dist-ℚ}} |
| 43 | +between [rational numbers](elementary-number-theory.rational-numbers.md) |
| 44 | +measures how far two rational numbers are apart. |
| 45 | + |
| 46 | +```agda |
| 47 | +dist-ℚ : ℚ → ℚ → ℚ⁰⁺ |
| 48 | +dist-ℚ p q = abs-ℚ (p -ℚ q) |
| 49 | +
|
| 50 | +rational-dist-ℚ : ℚ → ℚ → ℚ |
| 51 | +rational-dist-ℚ p q = rational-ℚ⁰⁺ (dist-ℚ p q) |
| 52 | +``` |
| 53 | + |
| 54 | +## Properties |
| 55 | + |
| 56 | +### Commutativity |
| 57 | + |
| 58 | +```agda |
| 59 | +abstract |
| 60 | + commutative-dist-ℚ : (p q : ℚ) → dist-ℚ p q = dist-ℚ q p |
| 61 | + commutative-dist-ℚ p q = |
| 62 | + inv (abs-neg-ℚ _) ∙ ap abs-ℚ (distributive-neg-diff-ℚ _ _) |
| 63 | +``` |
| 64 | + |
| 65 | +### The differences of the arguments are less than or equal to their distance |
| 66 | + |
| 67 | +```agda |
| 68 | +abstract |
| 69 | + leq-diff-dist-ℚ : (p q : ℚ) → leq-ℚ (p -ℚ q) (rational-dist-ℚ p q) |
| 70 | + leq-diff-dist-ℚ p q = leq-abs-ℚ (p -ℚ q) |
| 71 | +
|
| 72 | + leq-reversed-diff-dist-ℚ : |
| 73 | + (p q : ℚ) → leq-ℚ (q -ℚ p) (rational-dist-ℚ p q) |
| 74 | + leq-reversed-diff-dist-ℚ p q = |
| 75 | + tr |
| 76 | + ( leq-ℚ (q -ℚ p)) |
| 77 | + ( ap rational-ℚ⁰⁺ (commutative-dist-ℚ q p)) |
| 78 | + ( leq-diff-dist-ℚ q p) |
| 79 | +``` |
| 80 | + |
| 81 | +### Zero laws |
| 82 | + |
| 83 | +```agda |
| 84 | +abstract |
| 85 | + right-zero-law-dist-ℚ : (q : ℚ) → dist-ℚ q zero-ℚ = abs-ℚ q |
| 86 | + right-zero-law-dist-ℚ q = ap abs-ℚ (right-unit-law-add-ℚ _) |
| 87 | +
|
| 88 | + left-zero-law-dist-ℚ : (q : ℚ) → dist-ℚ zero-ℚ q = abs-ℚ q |
| 89 | + left-zero-law-dist-ℚ q = commutative-dist-ℚ _ _ ∙ right-zero-law-dist-ℚ q |
| 90 | +``` |
| 91 | + |
| 92 | +### Distributivity laws |
| 93 | + |
| 94 | +```agda |
| 95 | +abstract |
| 96 | + left-distributive-mul-dist-ℚ : |
| 97 | + (p : ℚ⁰⁺) (q r : ℚ) → |
| 98 | + p *ℚ⁰⁺ dist-ℚ q r = dist-ℚ (rational-ℚ⁰⁺ p *ℚ q) (rational-ℚ⁰⁺ p *ℚ r) |
| 99 | + left-distributive-mul-dist-ℚ p⁰⁺@(p , _) q r = |
| 100 | + eq-ℚ⁰⁺ |
| 101 | + ( equational-reasoning |
| 102 | + p *ℚ rational-dist-ℚ q r |
| 103 | + = rational-abs-ℚ (p *ℚ (q -ℚ r)) |
| 104 | + by ap rational-ℚ⁰⁺ (inv (abs-left-mul-nonnegative-ℚ _ p⁰⁺)) |
| 105 | + = rational-abs-ℚ (p *ℚ q +ℚ p *ℚ (neg-ℚ r)) |
| 106 | + by ap rational-abs-ℚ (left-distributive-mul-add-ℚ p q (neg-ℚ r)) |
| 107 | + = rational-abs-ℚ (p *ℚ q -ℚ p *ℚ r) |
| 108 | + by ap rational-abs-ℚ (ap (p *ℚ q +ℚ_) (right-negative-law-mul-ℚ _ _))) |
| 109 | +
|
| 110 | + right-distributive-mul-dist-ℚ : |
| 111 | + (p : ℚ⁰⁺) (q r : ℚ) → |
| 112 | + dist-ℚ q r *ℚ⁰⁺ p = dist-ℚ (q *ℚ rational-ℚ⁰⁺ p) (r *ℚ rational-ℚ⁰⁺ p) |
| 113 | + right-distributive-mul-dist-ℚ p⁰⁺@(p , _) q r = |
| 114 | + eq-ℚ⁰⁺ |
| 115 | + ( equational-reasoning |
| 116 | + rational-dist-ℚ q r *ℚ p |
| 117 | + = p *ℚ rational-dist-ℚ q r by commutative-mul-ℚ _ _ |
| 118 | + = rational-dist-ℚ (p *ℚ q) (p *ℚ r) |
| 119 | + by ap rational-ℚ⁰⁺ (left-distributive-mul-dist-ℚ p⁰⁺ q r) |
| 120 | + = rational-dist-ℚ (q *ℚ p) (r *ℚ p) |
| 121 | + by |
| 122 | + ap-binary |
| 123 | + ( rational-dist-ℚ) |
| 124 | + ( commutative-mul-ℚ _ _) |
| 125 | + ( commutative-mul-ℚ _ _)) |
| 126 | +``` |
| 127 | + |
| 128 | +### Triangle inequality |
| 129 | + |
| 130 | +```agda |
| 131 | +abstract |
| 132 | + triangle-inequality-dist-ℚ : |
| 133 | + (p q r : ℚ) → leq-ℚ⁰⁺ (dist-ℚ p r) (dist-ℚ p q +ℚ⁰⁺ dist-ℚ q r) |
| 134 | + triangle-inequality-dist-ℚ p q r = |
| 135 | + tr |
| 136 | + ( λ s → leq-ℚ⁰⁺ s (dist-ℚ p q +ℚ⁰⁺ dist-ℚ q r)) |
| 137 | + ( ap abs-ℚ |
| 138 | + ( inv (associative-add-ℚ _ _ (neg-ℚ r)) ∙ |
| 139 | + ap (_-ℚ r) (is-section-diff-ℚ _ _))) |
| 140 | + ( triangle-inequality-abs-ℚ (p -ℚ q) (q -ℚ r)) |
| 141 | +``` |
| 142 | + |
| 143 | +### Bounding the distance between rational numbers |
| 144 | + |
| 145 | +```agda |
| 146 | +abstract |
| 147 | + leq-dist-leq-diff-ℚ : |
| 148 | + (p q r : ℚ) → leq-ℚ (p -ℚ q) r → leq-ℚ (q -ℚ p) r → |
| 149 | + leq-ℚ (rational-dist-ℚ p q) r |
| 150 | + leq-dist-leq-diff-ℚ p q r p-q≤r q-p≤r = |
| 151 | + leq-abs-leq-leq-neg-ℚ |
| 152 | + ( p -ℚ q) |
| 153 | + ( r) |
| 154 | + ( p-q≤r) |
| 155 | + ( inv-tr (λ s → leq-ℚ s r) (distributive-neg-diff-ℚ p q) q-p≤r) |
| 156 | +
|
| 157 | + le-dist-le-diff-ℚ : |
| 158 | + (p q r : ℚ) → le-ℚ (p -ℚ q) r → le-ℚ (q -ℚ p) r → |
| 159 | + le-ℚ (rational-dist-ℚ p q) r |
| 160 | + le-dist-le-diff-ℚ p q r p-q<r q-p<r = |
| 161 | + le-abs-le-le-neg-ℚ |
| 162 | + ( p -ℚ q) |
| 163 | + ( r) |
| 164 | + ( p-q<r) |
| 165 | + ( inv-tr (λ s → le-ℚ s r) (distributive-neg-diff-ℚ p q) q-p<r) |
| 166 | +``` |
| 167 | + |
| 168 | +### Relationship to the metric space of rational numbers |
| 169 | + |
| 170 | +```agda |
| 171 | +abstract |
| 172 | + leq-dist-neighborhood-leq-ℚ : |
| 173 | + (ε : ℚ⁺) (p q : ℚ) → |
| 174 | + neighborhood-leq-ℚ ε p q → |
| 175 | + leq-ℚ (rational-dist-ℚ p q) (rational-ℚ⁺ ε) |
| 176 | + leq-dist-neighborhood-leq-ℚ ε⁺@(ε , _) p q (H , K) = |
| 177 | + leq-dist-leq-diff-ℚ |
| 178 | + ( p) |
| 179 | + ( q) |
| 180 | + ( ε) |
| 181 | + ( swap-right-diff-leq-ℚ p ε q (leq-transpose-right-add-ℚ p q ε K)) |
| 182 | + ( swap-right-diff-leq-ℚ q ε p (leq-transpose-right-add-ℚ q p ε H)) |
| 183 | +
|
| 184 | + neighborhood-leq-leq-dist-ℚ : |
| 185 | + (ε : ℚ⁺) (p q : ℚ) → |
| 186 | + leq-ℚ (rational-dist-ℚ p q) (rational-ℚ⁺ ε) → |
| 187 | + neighborhood-leq-ℚ ε p q |
| 188 | + neighborhood-leq-leq-dist-ℚ ε⁺@(ε , _) p q |p-q|≤ε = |
| 189 | + ( leq-transpose-left-diff-ℚ |
| 190 | + ( q) |
| 191 | + ( ε) |
| 192 | + ( p) |
| 193 | + ( swap-right-diff-leq-ℚ |
| 194 | + ( q) |
| 195 | + ( p) |
| 196 | + ( ε) |
| 197 | + ( transitive-leq-ℚ |
| 198 | + ( q -ℚ p) |
| 199 | + ( rational-dist-ℚ p q) |
| 200 | + ( ε) |
| 201 | + ( |p-q|≤ε) |
| 202 | + ( leq-reversed-diff-dist-ℚ p q)))) , |
| 203 | + ( leq-transpose-left-diff-ℚ |
| 204 | + ( p) |
| 205 | + ( ε) |
| 206 | + ( q) |
| 207 | + ( swap-right-diff-leq-ℚ |
| 208 | + ( p) |
| 209 | + ( q) |
| 210 | + ( ε) |
| 211 | + ( transitive-leq-ℚ |
| 212 | + ( p -ℚ q) |
| 213 | + ( rational-dist-ℚ p q) |
| 214 | + ( ε) |
| 215 | + ( |p-q|≤ε) |
| 216 | + ( leq-diff-dist-ℚ p q)))) |
| 217 | +
|
| 218 | +leq-dist-iff-neighborhood-leq-ℚ : |
| 219 | + (ε : ℚ⁺) (p q : ℚ) → |
| 220 | + leq-ℚ (rational-dist-ℚ p q) (rational-ℚ⁺ ε) ↔ |
| 221 | + neighborhood-leq-ℚ ε p q |
| 222 | +pr1 (leq-dist-iff-neighborhood-leq-ℚ ε p q) = neighborhood-leq-leq-dist-ℚ ε p q |
| 223 | +pr2 (leq-dist-iff-neighborhood-leq-ℚ ε p q) = leq-dist-neighborhood-leq-ℚ ε p q |
| 224 | +``` |
| 225 | + |
| 226 | +### Relationship to the metric space of rational numbers with open neighborhoods |
| 227 | + |
| 228 | +```agda |
| 229 | +abstract |
| 230 | + le-dist-neighborhood-le-ℚ : |
| 231 | + (ε : ℚ⁺) (p q : ℚ) → |
| 232 | + neighborhood-le-ℚ ε p q → |
| 233 | + le-ℚ (rational-dist-ℚ p q) (rational-ℚ⁺ ε) |
| 234 | + le-dist-neighborhood-le-ℚ ε⁺@(ε , _) p q (H , K) = |
| 235 | + le-dist-le-diff-ℚ |
| 236 | + ( p) |
| 237 | + ( q) |
| 238 | + ( ε) |
| 239 | + ( swap-right-diff-le-ℚ p ε q (le-transpose-right-add-ℚ p q ε K)) |
| 240 | + ( swap-right-diff-le-ℚ q ε p (le-transpose-right-add-ℚ q p ε H)) |
| 241 | +
|
| 242 | + neighborhood-le-le-dist-ℚ : |
| 243 | + (ε : ℚ⁺) (p q : ℚ) → |
| 244 | + le-ℚ (rational-dist-ℚ p q) (rational-ℚ⁺ ε) → |
| 245 | + neighborhood-le-ℚ ε p q |
| 246 | + neighborhood-le-le-dist-ℚ ε⁺@(ε , _) p q |p-q|<ε = |
| 247 | + ( le-transpose-left-diff-ℚ |
| 248 | + ( q) |
| 249 | + ( ε) |
| 250 | + ( p) |
| 251 | + ( swap-right-diff-le-ℚ |
| 252 | + ( q) |
| 253 | + ( p) |
| 254 | + ( ε) |
| 255 | + ( concatenate-leq-le-ℚ |
| 256 | + ( q -ℚ p) |
| 257 | + ( rational-dist-ℚ p q) |
| 258 | + ( ε) |
| 259 | + ( leq-reversed-diff-dist-ℚ p q) |
| 260 | + ( |p-q|<ε)))) , |
| 261 | + ( le-transpose-left-diff-ℚ |
| 262 | + ( p) |
| 263 | + ( ε) |
| 264 | + ( q) |
| 265 | + ( swap-right-diff-le-ℚ |
| 266 | + ( p) |
| 267 | + ( q) |
| 268 | + ( ε) |
| 269 | + ( concatenate-leq-le-ℚ |
| 270 | + ( p -ℚ q) |
| 271 | + ( rational-dist-ℚ p q) |
| 272 | + ( ε) |
| 273 | + ( leq-diff-dist-ℚ p q) |
| 274 | + ( |p-q|<ε)))) |
| 275 | +
|
| 276 | +le-dist-iff-neighborhood-le-ℚ : |
| 277 | + (ε : ℚ⁺) (p q : ℚ) → |
| 278 | + le-ℚ (rational-dist-ℚ p q) (rational-ℚ⁺ ε) ↔ |
| 279 | + neighborhood-le-ℚ ε p q |
| 280 | +pr1 (le-dist-iff-neighborhood-le-ℚ ε p q) = neighborhood-le-le-dist-ℚ ε p q |
| 281 | +pr2 (le-dist-iff-neighborhood-le-ℚ ε p q) = le-dist-neighborhood-le-ℚ ε p q |
| 282 | +``` |
| 283 | + |
| 284 | +### The distance between two rational numbers is the difference of their maximum and minimum |
| 285 | + |
| 286 | +```agda |
| 287 | +abstract |
| 288 | + eq-dist-diff-leq-ℚ : (p q : ℚ) → leq-ℚ p q → rational-dist-ℚ p q = q -ℚ p |
| 289 | + eq-dist-diff-leq-ℚ p q p≤q = |
| 290 | + equational-reasoning |
| 291 | + rational-dist-ℚ p q |
| 292 | + = rational-dist-ℚ q p by ap rational-ℚ⁰⁺ (commutative-dist-ℚ p q) |
| 293 | + = q -ℚ p |
| 294 | + by |
| 295 | + rational-abs-zero-leq-ℚ |
| 296 | + ( q -ℚ p) |
| 297 | + ( backward-implication (iff-translate-diff-leq-zero-ℚ p q) p≤q) |
| 298 | +
|
| 299 | + eq-dist-diff-max-min-ℚ : |
| 300 | + (p q : ℚ) → rational-dist-ℚ p q = max-ℚ p q -ℚ min-ℚ p q |
| 301 | + eq-dist-diff-max-min-ℚ p q = |
| 302 | + rec-coproduct |
| 303 | + ( λ p≤q → |
| 304 | + equational-reasoning |
| 305 | + rational-dist-ℚ p q |
| 306 | + = q -ℚ p by eq-dist-diff-leq-ℚ p q p≤q |
| 307 | + = max-ℚ p q -ℚ min-ℚ p q |
| 308 | + by |
| 309 | + inv |
| 310 | + ( ap-diff-ℚ |
| 311 | + ( left-leq-right-max-ℚ p q p≤q) |
| 312 | + ( left-leq-right-min-ℚ p q p≤q))) |
| 313 | + ( λ q≤p → |
| 314 | + equational-reasoning |
| 315 | + rational-dist-ℚ p q |
| 316 | + = rational-dist-ℚ q p by ap rational-ℚ⁰⁺ (commutative-dist-ℚ p q) |
| 317 | + = p -ℚ q by eq-dist-diff-leq-ℚ q p q≤p |
| 318 | + = max-ℚ p q -ℚ min-ℚ p q |
| 319 | + by |
| 320 | + inv |
| 321 | + ( ap-diff-ℚ |
| 322 | + ( right-leq-left-max-ℚ p q q≤p) |
| 323 | + ( right-leq-left-min-ℚ p q q≤p))) |
| 324 | + ( linear-leq-ℚ p q) |
| 325 | +``` |
0 commit comments