Skip to content

Commit a0da6e7

Browse files
Ruben-VandeVeldeParcly-Taxel
Ruben-VandeVelde
and
Parcly-Taxel
committed
feat: port SetTheory.Surreal.Dyadic (#5552)
Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>
1 parent b62dfca commit a0da6e7

File tree

3 files changed

+307
-0
lines changed

3 files changed

+307
-0
lines changed

‎Mathlib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2796,6 +2796,7 @@ import Mathlib.SetTheory.Ordinal.Notation
27962796
import Mathlib.SetTheory.Ordinal.Principal
27972797
import Mathlib.SetTheory.Ordinal.Topology
27982798
import Mathlib.SetTheory.Surreal.Basic
2799+
import Mathlib.SetTheory.Surreal.Dyadic
27992800
import Mathlib.SetTheory.ZFC.Basic
28002801
import Mathlib.SetTheory.ZFC.Ordinal
28012802
import Mathlib.Tactic

‎Mathlib/SetTheory/Game/PGame.lean‎

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -790,11 +790,23 @@ theorem le_of_le_of_equiv {x y z : PGame} (h₁ : x ≤ y) (h₂ : y ≈ z) : x
790790
h₁.trans h₂.1
791791
#align pgame.le_of_le_of_equiv PGame.le_of_le_of_equiv
792792

793+
instance : Trans
794+
((· ≤ ·) : PGame → PGame → Prop)
795+
((· ≈ ·) : PGame → PGame → Prop)
796+
((· ≤ ·) : PGame → PGame → Prop) where
797+
trans := le_of_le_of_equiv
798+
793799
@[trans]
794800
theorem le_of_equiv_of_le {x y z : PGame} (h₁ : x ≈ y) : y ≤ z → x ≤ z :=
795801
h₁.1.trans
796802
#align pgame.le_of_equiv_of_le PGame.le_of_equiv_of_le
797803

804+
instance : Trans
805+
((· ≈ ·) : PGame → PGame → Prop)
806+
((· ≤ ·) : PGame → PGame → Prop)
807+
((· ≤ ·) : PGame → PGame → Prop) where
808+
trans := le_of_equiv_of_le
809+
798810
theorem Lf.not_equiv {x y : PGame} (h : x ⧏ y) : ¬(x ≈ y) := fun h' => h.not_ge h'.2
799811
#align pgame.lf.not_equiv PGame.Lf.not_equiv
800812

@@ -856,6 +868,12 @@ theorem lt_of_equiv_of_lt {x y z : PGame} (h₁ : x ≈ y) : y < z → x < z :=
856868
h₁.1.trans_lt
857869
#align pgame.lt_of_equiv_of_lt PGame.lt_of_equiv_of_lt
858870

871+
instance : Trans
872+
((· ≈ ·) : PGame → PGame → Prop)
873+
((· < ·) : PGame → PGame → Prop)
874+
((· < ·) : PGame → PGame → Prop) where
875+
trans := lt_of_equiv_of_lt
876+
859877
theorem lt_congr_imp {x₁ y₁ x₂ y₂ : PGame} (hx : x₁ ≈ x₂) (hy : y₁ ≈ y₂) (h : x₁ < y₁) : x₂ < y₂ :=
860878
hx.2.trans_lt (h.trans_le hy.1)
861879
#align pgame.lt_congr_imp PGame.lt_congr_imp

‎Mathlib/SetTheory/Surreal/Dyadic.lean‎

Lines changed: 288 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,288 @@
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+
! This file was ported from Lean 3 source module set_theory.surreal.dyadic
7+
! leanprover-community/mathlib commit 92ca63f0fb391a9ca5f22d2409a6080e786d99f7
8+
! Please do not edit these lines, except to modify the commit id
9+
! if you have ported upstream changes.
10+
-/
11+
import Mathlib.Algebra.Algebra.Basic
12+
import Mathlib.SetTheory.Game.Birthday
13+
import Mathlib.SetTheory.Surreal.Basic
14+
import Mathlib.RingTheory.Localization.Basic
15+
16+
/-!
17+
# Dyadic numbers
18+
Dyadic numbers are obtained by localizing ℤ away from 2. They are the initial object in the category
19+
of rings with no 2-torsion.
20+
21+
## Dyadic surreal numbers
22+
We construct dyadic surreal numbers using the canonical map from ℤ[2 ^ {-1}] to surreals.
23+
As we currently do not have a ring structure on `Surreal` we construct this map explicitly. Once we
24+
have the ring structure, this map can be constructed directly by sending `2 ^ {-1}` to `half`.
25+
26+
## Embeddings
27+
The above construction gives us an abelian group embedding of ℤ into `Surreal`. The goal is to
28+
extend this to an embedding of dyadic rationals into `Surreal` and use Cauchy sequences of dyadic
29+
rational numbers to construct an ordered field embedding of ℝ into `Surreal`.
30+
-/
31+
32+
33+
universe u
34+
35+
namespace PGame
36+
37+
/-- For a natural number `n`, the pre-game `powHalf (n + 1)` is recursively defined as
38+
`{0 | powHalf n}`. These are the explicit expressions of powers of `1 / 2`. By definition, we have
39+
`powHalf 0 = 1` and `powHalf 1 ≈ 1 / 2` and we prove later on that
40+
`powHalf (n + 1) + powHalf (n + 1) ≈ powHalf n`. -/
41+
def powHalf : ℕ → PGame
42+
| 0 => 1
43+
| n + 1 => ⟨PUnit, PUnit, 0, fun _ => powHalf n⟩
44+
#align pgame.pow_half PGame.powHalf
45+
46+
@[simp]
47+
theorem powHalf_zero : powHalf 0 = 1 :=
48+
rfl
49+
#align pgame.pow_half_zero PGame.powHalf_zero
50+
51+
theorem powHalf_leftMoves (n) : (powHalf n).LeftMoves = PUnit := by cases n <;> rfl
52+
#align pgame.pow_half_left_moves PGame.powHalf_leftMoves
53+
54+
theorem powHalf_zero_rightMoves : (powHalf 0).RightMoves = PEmpty :=
55+
rfl
56+
#align pgame.pow_half_zero_right_moves PGame.powHalf_zero_rightMoves
57+
58+
theorem powHalf_succ_rightMoves (n) : (powHalf (n + 1)).RightMoves = PUnit :=
59+
rfl
60+
#align pgame.pow_half_succ_right_moves PGame.powHalf_succ_rightMoves
61+
62+
@[simp]
63+
theorem powHalf_moveLeft (n i) : (powHalf n).moveLeft i = 0 := by cases n <;> cases i <;> rfl
64+
#align pgame.pow_half_move_left PGame.powHalf_moveLeft
65+
66+
@[simp]
67+
theorem powHalf_succ_moveRight (n i) : (powHalf (n + 1)).moveRight i = powHalf n :=
68+
rfl
69+
#align pgame.pow_half_succ_move_right PGame.powHalf_succ_moveRight
70+
71+
instance uniquePowHalfLeftMoves (n) : Unique (powHalf n).LeftMoves := by
72+
cases n <;> exact PUnit.unique
73+
#align pgame.unique_pow_half_left_moves PGame.uniquePowHalfLeftMoves
74+
75+
instance isEmpty_powHalf_zero_rightMoves : IsEmpty (powHalf 0).RightMoves :=
76+
inferInstanceAs (IsEmpty PEmpty)
77+
#align pgame.is_empty_pow_half_zero_right_moves PGame.isEmpty_powHalf_zero_rightMoves
78+
79+
instance uniquePowHalfSuccRightMoves (n) : Unique (powHalf (n + 1)).RightMoves :=
80+
PUnit.unique
81+
#align pgame.unique_pow_half_succ_right_moves PGame.uniquePowHalfSuccRightMoves
82+
83+
@[simp]
84+
theorem birthday_half : birthday (powHalf 1) = 2 := by
85+
rw [birthday_def]; dsimp; simpa using Order.le_succ (1 : Ordinal)
86+
#align pgame.birthday_half PGame.birthday_half
87+
88+
/-- For all natural numbers `n`, the pre-games `powHalf n` are numeric. -/
89+
theorem numeric_powHalf (n) : (powHalf n).Numeric := by
90+
induction' n with n hn
91+
· exact numeric_one
92+
· constructor
93+
· simpa using hn.moveLeft_lt default
94+
· exact ⟨fun _ => numeric_zero, fun _ => hn⟩
95+
#align pgame.numeric_pow_half PGame.numeric_powHalf
96+
97+
theorem powHalf_succ_lt_powHalf (n : ℕ) : powHalf (n + 1) < powHalf n :=
98+
(numeric_powHalf (n + 1)).lt_moveRight default
99+
#align pgame.pow_half_succ_lt_pow_half PGame.powHalf_succ_lt_powHalf
100+
101+
theorem powHalf_succ_le_powHalf (n : ℕ) : powHalf (n + 1) ≤ powHalf n :=
102+
(powHalf_succ_lt_powHalf n).le
103+
#align pgame.pow_half_succ_le_pow_half PGame.powHalf_succ_le_powHalf
104+
105+
theorem powHalf_le_one (n : ℕ) : powHalf n ≤ 1 := by
106+
induction' n with n hn
107+
· exact le_rfl
108+
· exact (powHalf_succ_le_powHalf n).trans hn
109+
#align pgame.pow_half_le_one PGame.powHalf_le_one
110+
111+
theorem powHalf_succ_lt_one (n : ℕ) : powHalf (n + 1) < 1 :=
112+
(powHalf_succ_lt_powHalf n).trans_le <| powHalf_le_one n
113+
#align pgame.pow_half_succ_lt_one PGame.powHalf_succ_lt_one
114+
115+
theorem powHalf_pos (n : ℕ) : 0 < powHalf n := by
116+
rw [← lf_iff_lt numeric_zero (numeric_powHalf n), zero_lf_le]; simp
117+
#align pgame.pow_half_pos PGame.powHalf_pos
118+
119+
theorem zero_le_powHalf (n : ℕ) : 0 ≤ powHalf n :=
120+
(powHalf_pos n).le
121+
#align pgame.zero_le_pow_half PGame.zero_le_powHalf
122+
123+
theorem add_powHalf_succ_self_eq_powHalf (n) : powHalf (n + 1) + powHalf (n + 1) ≈ powHalf n := by
124+
induction' n using Nat.strong_induction_on with n hn
125+
· constructor <;> rw [le_iff_forall_lf] <;> constructor
126+
· rintro (⟨⟨⟩⟩ | ⟨⟨⟩⟩) <;> apply lf_of_lt
127+
· calc
128+
0 + powHalf n.succ ≈ powHalf n.succ := zero_add_equiv _
129+
_ < powHalf n := powHalf_succ_lt_powHalf n
130+
· calc
131+
powHalf n.succ + 0 ≈ powHalf n.succ := add_zero_equiv _
132+
_ < powHalf n := powHalf_succ_lt_powHalf n
133+
· cases' n with n
134+
· rintro ⟨⟩
135+
rintro ⟨⟩
136+
apply lf_of_moveRight_le
137+
swap; exact Sum.inl default
138+
calc
139+
powHalf n.succ + powHalf (n.succ + 1) ≤ powHalf n.succ + powHalf n.succ :=
140+
add_le_add_left (powHalf_succ_le_powHalf _) _
141+
_ ≈ powHalf n := hn _ (Nat.lt_succ_self n)
142+
· simp only [powHalf_moveLeft, forall_const]
143+
apply lf_of_lt
144+
calc
145+
0 ≈ 0 + 0 := (Equiv.symm (add_zero_equiv 0))
146+
_ ≤ powHalf n.succ + 0 := (add_le_add_right (zero_le_powHalf _) _)
147+
_ < powHalf n.succ + powHalf n.succ := add_lt_add_left (powHalf_pos _) _
148+
· rintro (⟨⟨⟩⟩ | ⟨⟨⟩⟩) <;> apply lf_of_lt
149+
· calc
150+
powHalf n ≈ powHalf n + 0 := (Equiv.symm (add_zero_equiv _))
151+
_ < powHalf n + powHalf n.succ := add_lt_add_left (powHalf_pos _) _
152+
· calc
153+
powHalf n ≈ 0 + powHalf n := (Equiv.symm (zero_add_equiv _))
154+
_ < powHalf n.succ + powHalf n := add_lt_add_right (powHalf_pos _) _
155+
#align pgame.add_pow_half_succ_self_eq_pow_half PGame.add_powHalf_succ_self_eq_powHalf
156+
157+
theorem half_add_half_equiv_one : powHalf 1 + powHalf 1 ≈ 1 :=
158+
add_powHalf_succ_self_eq_powHalf 0
159+
#align pgame.half_add_half_equiv_one PGame.half_add_half_equiv_one
160+
161+
end PGame
162+
163+
namespace Surreal
164+
165+
open PGame
166+
167+
/-- Powers of the surreal number `half`. -/
168+
def powHalf (n : ℕ) : Surreal :=
169+
⟦⟨PGame.powHalf n, PGame.numeric_powHalf n⟩⟧
170+
#align surreal.pow_half Surreal.powHalf
171+
172+
@[simp]
173+
theorem powHalf_zero : powHalf 0 = 1 :=
174+
rfl
175+
#align surreal.pow_half_zero Surreal.powHalf_zero
176+
177+
@[simp]
178+
theorem double_powHalf_succ_eq_powHalf (n : ℕ) : 2 • powHalf n.succ = powHalf n := by
179+
rw [two_nsmul]; exact Quotient.sound (PGame.add_powHalf_succ_self_eq_powHalf n)
180+
#align surreal.double_pow_half_succ_eq_pow_half Surreal.double_powHalf_succ_eq_powHalf
181+
182+
@[simp]
183+
theorem nsmul_pow_two_powHalf (n : ℕ) : 2 ^ n • powHalf n = 1 := by
184+
induction' n with n hn
185+
· simp only [Nat.zero_eq, pow_zero, powHalf_zero, one_smul]
186+
· rw [← hn, ← double_powHalf_succ_eq_powHalf n, smul_smul (2 ^ n) 2 (powHalf n.succ), mul_comm,
187+
pow_succ]
188+
#align surreal.nsmul_pow_two_pow_half Surreal.nsmul_pow_two_powHalf
189+
190+
@[simp]
191+
theorem nsmul_pow_two_powHalf' (n k : ℕ) : 2 ^ n • powHalf (n + k) = powHalf k := by
192+
induction' k with k hk
193+
· simp only [add_zero, Surreal.nsmul_pow_two_powHalf, Nat.zero_eq, eq_self_iff_true,
194+
Surreal.powHalf_zero]
195+
· rw [← double_powHalf_succ_eq_powHalf (n + k), ← double_powHalf_succ_eq_powHalf k,
196+
smul_algebra_smul_comm] at hk
197+
rwa [← zsmul_eq_zsmul_iff' two_ne_zero]
198+
#align surreal.nsmul_pow_two_pow_half' Surreal.nsmul_pow_two_powHalf'
199+
200+
theorem zsmul_pow_two_powHalf (m : ℤ) (n k : ℕ) :
201+
(m * 2 ^ n) • powHalf (n + k) = m • powHalf k := by
202+
rw [mul_zsmul]
203+
congr
204+
norm_cast
205+
exact nsmul_pow_two_powHalf' n k
206+
#align surreal.zsmul_pow_two_pow_half Surreal.zsmul_pow_two_powHalf
207+
208+
theorem dyadic_aux {m₁ m₂ : ℤ} {y₁ y₂ : ℕ} (h₂ : m₁ * 2 ^ y₁ = m₂ * 2 ^ y₂) :
209+
m₁ • powHalf y₂ = m₂ • powHalf y₁ := by
210+
revert m₁ m₂
211+
wlog h : y₁ ≤ y₂
212+
· intro m₁ m₂ aux; exact (this (le_of_not_le h) aux.symm).symm
213+
intro m₁ m₂ h₂
214+
obtain ⟨c, rfl⟩ := le_iff_exists_add.mp h
215+
rw [add_comm, pow_add, ← mul_assoc, mul_eq_mul_right_iff] at h₂
216+
cases' h₂ with h₂ h₂
217+
· rw [h₂, add_comm, zsmul_pow_two_powHalf m₂ c y₁]
218+
· have := Nat.one_le_pow y₁ 2 Nat.succ_pos'
219+
norm_cast at h₂ ; linarith
220+
#align surreal.dyadic_aux Surreal.dyadic_aux
221+
222+
/-- The additive monoid morphism `dyadicMap` sends ⟦⟨m, 2^n⟩⟧ to m • half ^ n. -/
223+
def dyadicMap : Localization.Away (2 : ℤ) →+ Surreal where
224+
toFun x :=
225+
(Localization.liftOn x fun x y => x • powHalf (Submonoid.log y)) <| by
226+
intro m₁ m₂ n₁ n₂ h₁
227+
obtain ⟨⟨n₃, y₃, hn₃⟩, h₂⟩ := Localization.r_iff_exists.mp h₁
228+
simp only [Subtype.coe_mk, mul_eq_mul_left_iff] at h₂
229+
cases h₂
230+
· obtain ⟨a₁, ha₁⟩ := n₁.prop
231+
obtain ⟨a₂, ha₂⟩ := n₂.prop
232+
simp only at ha₁ ha₂ ⊢
233+
have hn₁ : n₁ = Submonoid.pow 2 a₁ := Subtype.ext ha₁.symm
234+
have hn₂ : n₂ = Submonoid.pow 2 a₂ := Subtype.ext ha₂.symm
235+
have h₂ : 1 < (2 : ℤ).natAbs := one_lt_two
236+
rw [hn₁, hn₂, Submonoid.log_pow_int_eq_self h₂, Submonoid.log_pow_int_eq_self h₂]
237+
apply dyadic_aux
238+
rwa [ha₁, ha₂, mul_comm, mul_comm m₂]
239+
· have : (1 : ℤ) ≤ 2 ^ y₃ := by exact_mod_cast Nat.one_le_pow y₃ 2 Nat.succ_pos'
240+
linarith
241+
map_zero' := Localization.liftOn_zero _ _
242+
map_add' x y :=
243+
Localization.induction_on₂ x y <| by
244+
rintro ⟨a, ⟨b, ⟨b', rfl⟩⟩⟩ ⟨c, ⟨d, ⟨d', rfl⟩⟩⟩
245+
have h₂ : 1 < (2 : ℤ).natAbs := one_lt_two
246+
have hpow₂ := Submonoid.log_pow_int_eq_self h₂
247+
simp_rw [Submonoid.pow_apply] at hpow₂
248+
simp_rw [Localization.add_mk, Localization.liftOn_mk, Subtype.coe_mk,
249+
Submonoid.log_mul (Int.pow_right_injective h₂), hpow₂]
250+
calc
251+
(2 ^ b' * c + 2 ^ d' * a) • powHalf (b' + d') =
252+
(c * 2 ^ b') • powHalf (b' + d') + (a * 2 ^ d') • powHalf (d' + b') := by
253+
simp only [add_smul, mul_comm, add_comm]
254+
_ = c • powHalf d' + a • powHalf b' := by simp only [zsmul_pow_two_powHalf]
255+
_ = a • powHalf b' + c • powHalf d' := add_comm _ _
256+
#align surreal.dyadic_map Surreal.dyadicMap
257+
258+
@[simp]
259+
theorem dyadicMap_apply (m : ℤ) (p : Submonoid.powers (2 : ℤ)) :
260+
dyadicMap (IsLocalization.mk' (Localization (Submonoid.powers 2)) m p) =
261+
m • powHalf (Submonoid.log p) := by
262+
rw [← Localization.mk_eq_mk']; rfl
263+
#align surreal.dyadic_map_apply Surreal.dyadicMap_apply
264+
265+
-- @[simp] -- Porting note: simp normal form is `dyadicMap_apply_pow'`
266+
theorem dyadicMap_apply_pow (m : ℤ) (n : ℕ) :
267+
dyadicMap (IsLocalization.mk' (Localization (Submonoid.powers 2)) m (Submonoid.pow 2 n)) =
268+
m • powHalf n := by
269+
rw [dyadicMap_apply, @Submonoid.log_pow_int_eq_self 2 one_lt_two]
270+
#align surreal.dyadic_map_apply_pow Surreal.dyadicMap_apply_pow
271+
272+
@[simp]
273+
theorem dyadicMap_apply_pow' (m : ℤ) (n : ℕ) :
274+
m • Surreal.powHalf (Submonoid.log (Submonoid.pow (2 : ℤ) n)) = m • powHalf n := by
275+
rw [@Submonoid.log_pow_int_eq_self 2 one_lt_two]
276+
277+
/-- We define dyadic surreals as the range of the map `dyadicMap`. -/
278+
def dyadic : Set Surreal :=
279+
Set.range dyadicMap
280+
#align surreal.dyadic Surreal.dyadic
281+
282+
-- We conclude with some ideas for further work on surreals; these would make fun projects.
283+
-- TODO show that the map from dyadic rationals to surreals is injective
284+
-- TODO map the reals into the surreals, using dyadic Dedekind cuts
285+
-- TODO show this is a group homomorphism, and injective
286+
-- TODO show the maps from the dyadic rationals and from the reals
287+
-- into the surreals are multiplicative
288+
end Surreal

0 commit comments

Comments
 (0)