|
| 1 | +/- |
| 2 | +Copyright (c) 2021 Apurva Nakade. All rights reserved. |
| 3 | +Released under Apache 2.0 license as described in the file LICENSE. |
| 4 | +Authors: Apurva Nakade |
| 5 | +-/ |
| 6 | +import set_theory.surreal.basic |
| 7 | +import ring_theory.localization |
| 8 | + |
| 9 | +/-! |
| 10 | +# Dyadic numbers |
| 11 | +Dyadic numbers are obtained by localizing ℤ away from 2. They are the initial object in the category |
| 12 | +of rings with no 2-torsion. |
| 13 | +
|
| 14 | +## Dyadic surreal numbers |
| 15 | +We construct dyadic surreal numbers using the canonical map from ℤ[2 ^ {-1}] to surreals. |
| 16 | +As we currently do not have a ring structure on `surreal` we construct this map explicitly. Once we |
| 17 | +have the ring structure, this map can be constructed directly by sending `2 ^ {-1}` to `half`. |
| 18 | +
|
| 19 | +## Embeddings |
| 20 | +The above construction gives us an abelian group embedding of ℤ into `surreal`. The goal is to |
| 21 | +extend this to an embedding of dyadic rationals into `surreal` and use Cauchy sequences of dyadic |
| 22 | +rational numbers to construct an ordered field embedding of ℝ into `surreal`. |
| 23 | +-/ |
| 24 | + |
| 25 | +universes u |
| 26 | + |
| 27 | +local infix ` ≈ ` := pgame.equiv |
| 28 | + |
| 29 | +namespace pgame |
| 30 | + |
| 31 | +/-- For a natural number `n`, the pre-game `pow_half (n + 1)` is recursively defined as |
| 32 | +`{ 0 | pow_half n }`. These are the explicit expressions of powers of `half`. By definition, we have |
| 33 | + `pow_half 0 = 0` and `pow_half 1 = half` and we prove later on that |
| 34 | +`pow_half (n + 1) + pow_half (n + 1) ≈ pow_half n`.-/ |
| 35 | +def pow_half : ℕ → pgame |
| 36 | +| 0 := mk punit pempty 0 pempty.elim |
| 37 | +| (n + 1) := mk punit punit 0 (λ _, pow_half n) |
| 38 | + |
| 39 | +@[simp] lemma pow_half_left_moves {n} : (pow_half n).left_moves = punit := |
| 40 | +by cases n; refl |
| 41 | + |
| 42 | +@[simp] lemma pow_half_right_moves {n} : (pow_half (n + 1)).right_moves = punit := |
| 43 | +by cases n; refl |
| 44 | + |
| 45 | +@[simp] lemma pow_half_move_left {n i} : (pow_half n).move_left i = 0 := |
| 46 | +by cases n; cases i; refl |
| 47 | + |
| 48 | +@[simp] lemma pow_half_move_right {n i} : (pow_half (n + 1)).move_right i = pow_half n := |
| 49 | +by cases n; cases i; refl |
| 50 | + |
| 51 | +lemma pow_half_move_left' (n) : |
| 52 | + (pow_half n).move_left (equiv.cast (pow_half_left_moves.symm) punit.star) = 0 := |
| 53 | +by simp only [eq_self_iff_true, pow_half_move_left] |
| 54 | + |
| 55 | +lemma pow_half_move_right' (n) : |
| 56 | + (pow_half (n + 1)).move_right (equiv.cast (pow_half_right_moves.symm) punit.star) = pow_half n := |
| 57 | +by simp only [pow_half_move_right, eq_self_iff_true] |
| 58 | + |
| 59 | +/-- For all natural numbers `n`, the pre-games `pow_half n` are numeric. -/ |
| 60 | +theorem numeric_pow_half {n} : (pow_half n).numeric := |
| 61 | +begin |
| 62 | + induction n with n hn, |
| 63 | + { exact numeric_one }, |
| 64 | + { split, |
| 65 | + { rintro ⟨ ⟩ ⟨ ⟩, |
| 66 | + dsimp only [pi.zero_apply], |
| 67 | + rw ← pow_half_move_left' n, |
| 68 | + apply hn.move_left_lt }, |
| 69 | + { exact ⟨λ _, numeric_zero, λ _, hn⟩ } } |
| 70 | +end |
| 71 | + |
| 72 | +theorem pow_half_succ_lt_pow_half {n : ℕ} : pow_half (n + 1) < pow_half n := |
| 73 | +(@numeric_pow_half (n + 1)).lt_move_right punit.star |
| 74 | + |
| 75 | +theorem pow_half_succ_le_pow_half {n : ℕ} : pow_half (n + 1) ≤ pow_half n := |
| 76 | +le_of_lt numeric_pow_half numeric_pow_half pow_half_succ_lt_pow_half |
| 77 | + |
| 78 | +theorem zero_lt_pow_half {n : ℕ} : 0 < pow_half n := |
| 79 | +by cases n; rw lt_def_le; use ⟨punit.star, pgame.le_refl 0⟩ |
| 80 | + |
| 81 | +theorem zero_le_pow_half {n : ℕ} : 0 ≤ pow_half n := |
| 82 | +le_of_lt numeric_zero numeric_pow_half zero_lt_pow_half |
| 83 | + |
| 84 | +theorem add_pow_half_succ_self_eq_pow_half {n} : pow_half (n + 1) + pow_half (n + 1) ≈ pow_half n := |
| 85 | +begin |
| 86 | + induction n with n hn, |
| 87 | + { exact half_add_half_equiv_one }, |
| 88 | + { split; rw le_def_lt; split, |
| 89 | + { rintro (⟨⟨ ⟩⟩ | ⟨⟨ ⟩⟩), |
| 90 | + { calc 0 + pow_half (n.succ + 1) ≈ pow_half (n.succ + 1) : zero_add_equiv _ |
| 91 | + ... < pow_half n.succ : pow_half_succ_lt_pow_half }, |
| 92 | + { calc pow_half (n.succ + 1) + 0 ≈ pow_half (n.succ + 1) : add_zero_equiv _ |
| 93 | + ... < pow_half n.succ : pow_half_succ_lt_pow_half } }, |
| 94 | + { rintro ⟨ ⟩, |
| 95 | + rw lt_def_le, |
| 96 | + right, |
| 97 | + use sum.inl punit.star, |
| 98 | + calc pow_half (n.succ) + pow_half (n.succ + 1) |
| 99 | + ≤ pow_half (n.succ) + pow_half (n.succ) : add_le_add_left pow_half_succ_le_pow_half |
| 100 | + ... ≈ pow_half n : hn }, |
| 101 | + { rintro ⟨ ⟩, |
| 102 | + calc 0 ≈ 0 + 0 : (add_zero_equiv _).symm |
| 103 | + ... ≤ pow_half (n.succ + 1) + 0 : add_le_add_right zero_le_pow_half |
| 104 | + ... < pow_half (n.succ + 1) + pow_half (n.succ + 1) : add_lt_add_left zero_lt_pow_half }, |
| 105 | + { rintro (⟨⟨ ⟩⟩ | ⟨⟨ ⟩⟩), |
| 106 | + { calc pow_half n.succ |
| 107 | + ≈ pow_half n.succ + 0 : (add_zero_equiv _).symm |
| 108 | + ... < pow_half (n.succ) + pow_half (n.succ + 1) : add_lt_add_left zero_lt_pow_half }, |
| 109 | + { calc pow_half n.succ |
| 110 | + ≈ 0 + pow_half n.succ : (zero_add_equiv _).symm |
| 111 | + ... < pow_half (n.succ + 1) + pow_half (n.succ) : add_lt_add_right zero_lt_pow_half }}} |
| 112 | +end |
| 113 | + |
| 114 | +end pgame |
| 115 | + |
| 116 | +namespace surreal |
| 117 | +open pgame |
| 118 | + |
| 119 | +/-- The surreal number `half`. -/ |
| 120 | +def half : surreal := ⟦⟨pgame.half, pgame.numeric_half⟩⟧ |
| 121 | + |
| 122 | +/-- Powers of the surreal number `half`. -/ |
| 123 | +def pow_half (n : ℕ) : surreal := ⟦⟨pgame.pow_half n, pgame.numeric_pow_half⟩⟧ |
| 124 | + |
| 125 | +@[simp] lemma pow_half_zero : pow_half 0 = 1 := rfl |
| 126 | + |
| 127 | +@[simp] lemma pow_half_one : pow_half 1 = half := rfl |
| 128 | + |
| 129 | +@[simp] theorem add_half_self_eq_one : half + half = 1 := |
| 130 | +quotient.sound pgame.half_add_half_equiv_one |
| 131 | + |
| 132 | +lemma double_pow_half_succ_eq_pow_half (n : ℕ) : 2 • pow_half n.succ = pow_half n := |
| 133 | +begin |
| 134 | + rw two_nsmul, |
| 135 | + apply quotient.sound, |
| 136 | + exact pgame.add_pow_half_succ_self_eq_pow_half, |
| 137 | +end |
| 138 | + |
| 139 | +lemma nsmul_pow_two_pow_half (n : ℕ) : 2 ^ n • pow_half n = 1 := |
| 140 | +begin |
| 141 | + induction n with n hn, |
| 142 | + { simp only [nsmul_one, pow_half_zero, nat.cast_one, pow_zero] }, |
| 143 | + { rw [← hn, ← double_pow_half_succ_eq_pow_half n, smul_smul (2^n) 2 (pow_half n.succ), |
| 144 | + mul_comm, pow_succ] } |
| 145 | +end |
| 146 | + |
| 147 | +lemma nsmul_pow_two_pow_half' (n k : ℕ) : 2 ^ n • pow_half (n + k) = pow_half k := |
| 148 | +begin |
| 149 | + induction k with k hk, |
| 150 | + { simp only [add_zero, surreal.nsmul_pow_two_pow_half, nat.nat_zero_eq_zero, eq_self_iff_true, |
| 151 | + surreal.pow_half_zero] }, |
| 152 | + { rw [← double_pow_half_succ_eq_pow_half (n + k), ← double_pow_half_succ_eq_pow_half k, |
| 153 | + smul_algebra_smul_comm] at hk, |
| 154 | + rwa ← (gsmul_eq_gsmul_iff' two_ne_zero) } |
| 155 | +end |
| 156 | + |
| 157 | +lemma nsmul_int_pow_two_pow_half (m : ℤ) (n k : ℕ) : |
| 158 | + (m * 2 ^ n) • pow_half (n + k) = m • pow_half k := |
| 159 | +begin |
| 160 | + rw mul_gsmul, |
| 161 | + congr, |
| 162 | + norm_cast, |
| 163 | + exact nsmul_pow_two_pow_half' n k, |
| 164 | +end |
| 165 | + |
| 166 | +lemma dyadic_aux {m₁ m₂ : ℤ} {y₁ y₂ : ℕ} (h₂ : m₁ * (2 ^ y₁) = m₂ * (2 ^ y₂)) : |
| 167 | + m₁ • pow_half y₂ = m₂ • pow_half y₁ := |
| 168 | +begin |
| 169 | + revert m₁ m₂, |
| 170 | + wlog h : y₁ ≤ y₂, |
| 171 | + intros m₁ m₂ h₂, |
| 172 | + obtain ⟨c, rfl⟩ := le_iff_exists_add.mp h, |
| 173 | + rw [add_comm, pow_add, ← mul_assoc, mul_eq_mul_right_iff] at h₂, |
| 174 | + cases h₂, |
| 175 | + { rw [h₂, add_comm, nsmul_int_pow_two_pow_half m₂ c y₁] }, |
| 176 | + { have := nat.one_le_pow y₁ 2 nat.succ_pos', |
| 177 | + linarith }, |
| 178 | +end |
| 179 | + |
| 180 | +/-- The map `dyadic_map` sends ⟦⟨m, 2^n⟩⟧ to m • half ^ n. -/ |
| 181 | +def dyadic_map (x : localization (submonoid.powers (2 : ℤ))) : surreal := |
| 182 | +quotient.lift_on' x (λ x : _ × _, x.1 • pow_half (submonoid.log x.2)) $ |
| 183 | +begin |
| 184 | + rintros ⟨m₁, n₁⟩ ⟨m₂, n₂⟩ h₁, |
| 185 | + obtain ⟨⟨n₃, y₃, hn₃⟩, h₂⟩ := localization.r_iff_exists.mp h₁, |
| 186 | + simp only [subtype.coe_mk, mul_eq_mul_right_iff] at h₂, |
| 187 | + cases h₂, |
| 188 | + { simp only, |
| 189 | + obtain ⟨a₁, ha₁⟩ := n₁.prop, |
| 190 | + obtain ⟨a₂, ha₂⟩ := n₂.prop, |
| 191 | + have hn₁ : n₁ = submonoid.pow 2 a₁ := subtype.ext ha₁.symm, |
| 192 | + have hn₂ : n₂ = submonoid.pow 2 a₂ := subtype.ext ha₂.symm, |
| 193 | + have h₂ : 1 < (2 : ℤ).nat_abs, from dec_trivial, |
| 194 | + rw [hn₁, hn₂, submonoid.log_pow_int_eq_self h₂, submonoid.log_pow_int_eq_self h₂], |
| 195 | + apply dyadic_aux, |
| 196 | + rwa [ha₁, ha₂] }, |
| 197 | + { have := nat.one_le_pow y₃ 2 nat.succ_pos', |
| 198 | + linarith } |
| 199 | +end |
| 200 | + |
| 201 | +/-- We define dyadic surreals as the range of the map `dyadic_map`. -/ |
| 202 | +def dyadic : set surreal := set.range dyadic_map |
| 203 | + |
| 204 | +-- We conclude with some ideas for further work on surreals; these would make fun projects. |
| 205 | + |
| 206 | +-- TODO show that the map from dyadic rationals to surreals is a group homomorphism, and injective |
| 207 | + |
| 208 | +-- TODO map the reals into the surreals, using dyadic Dedekind cuts |
| 209 | +-- TODO show this is a group homomorphism, and injective |
| 210 | + |
| 211 | +-- TODO show the maps from the dyadic rationals and from the reals |
| 212 | +-- into the surreals are multiplicative |
| 213 | + |
| 214 | +end surreal |
0 commit comments