RotationDensity.lean

1 import Mathlib.NumberTheory.Niven
2 import Mathlib.Topology.Instances.AddCircle.DenseSubgroup
3 import Mathlib.Analysis.SpecialFunctions.Complex.Circle
4 import Mathlib.Topology.Algebra.Group.SubmonoidClosure
5 
6 set_option autoImplicit false
7 namespace Komorebi.LSM.RotationDensity
8 
9 /-- The exact rational unit complex number used by the rotation model. -/
10 noncomputable def rotation : Circle :=
11   ⟨⟨3/5,4/5⟩, by
12     apply mem_sphere_zero_iff_norm.mpr
13     apply (sq_eq_sq₀ (norm_nonneg _) (by norm_num : (0:ℝ)≤1)).mp
14     norm_num [← Complex.normSq_eq_norm_sq, Complex.normSq_apply]⟩
15 
16 @[simp] theorem rotation_coe_re : (rotation : ℂ).re = 3/5 := rfl
17 @[simp] theorem rotation_coe_im : (rotation : ℂ).im = 4/5 := rfl
18 
19 theorem rotation_arg_cos : Real.cos (Complex.arg (rotation : ℂ)) = 3/5 := by
20   rw [Complex.cos_arg rotation.coe_ne_zero, Circle.norm_coe, div_one, rotation_coe_re]
21 
22 /-- Its angle is not a rational fraction of a turn. -/
23 theorem rotation_arg_irrational :
24     Irrational (Complex.arg (rotation : ℂ)/(2*Real.pi)) := by
25   intro h
26   obtain ⟨q,hq⟩ := h
27   have harg : Complex.arg (rotation : ℂ) = (2*q : ℚ)*Real.pi := by
28     have hp : 2*Real.pi ≠ 0 := by positivity
29     have he := (div_eq_iff hp).mp hq.symm
30     push_cast
31     nlinarith
32   have hc := niven ⟨2*q,harg⟩ (⟨(3/5:ℚ), by rw [rotation_arg_cos]; norm_num⟩)
33   rw [rotation_arg_cos] at hc
34   norm_num at hc
35 
36 /-- No positive power of the actual rational rotation is the identity. -/
37 theorem rotation_pow_ne_one (n : ℕ) (hn : 0<n) : rotation^n ≠ 1 := by
38   intro h
39   have he : Circle.exp ((n:ℝ)*Complex.arg (rotation : ℂ)) = 1 := by
40     rw [Circle.exp_natCast_mul, Circle.exp_arg, h]
41   obtain ⟨k,hk⟩ := Circle.exp_eq_one.mp he
42   apply rotation_arg_irrational
43   refine ⟨(k:ℚ)/n, ?_⟩
44   have hnR : (n:ℝ) ≠ 0 := by exact_mod_cast Nat.ne_of_gt hn
45   have hpi : Real.pi ≠ 0 := Real.pi_ne_zero
46   push_cast
47   field_simp
48   nlinarith
49 
50 /-- Integer powers are dense via the additive circle and Niven's theorem. -/
51 theorem rotation_integer_dense : DenseRange (fun n : ℤ => rotation^n) := by
52   have hd := AddCircle.denseRange_zsmul_coe_iff.mpr rotation_arg_irrational
53   let e := AddCircle.homeomorphCircle (T := 2*Real.pi) (by positivity : 2*Real.pi ≠ 0)
54   have hm := e.surjective.denseRange.comp hd e.continuous
55   convert hm using 1
56   funext n
57   change rotation^n = e (n • (Complex.arg (rotation : ℂ) : AddCircle (2*Real.pi)))
58   rw [show e = AddCircle.homeomorphCircle (T := 2*Real.pi) (by positivity) from rfl,
59     AddCircle.homeomorphCircle_apply, AddCircle.toCircle_zsmul, AddCircle.toCircle_apply_mk]
60   simp only [div_self (by positivity : 2*Real.pi ≠ 0), one_mul, Circle.exp_arg]
61 
62 /-- Forward, nonnegative powers are dense; negative time is not an input. -/
63 theorem rotation_forward_dense : DenseRange (fun n : ℕ => rotation^n) :=
64   denseRange_zpow_iff_pow.mp rotation_integer_dense
65 
66 /-- The topological closure is the entire actual unit circle. -/
67 theorem rotation_forward_closure :
68     closure (Set.range (fun n : ℕ => rotation^n)) = Set.univ :=
69   rotation_forward_dense.closure_range
70 
71 /-- Any closed property holding on the forward orbit holds on the whole circle. -/
72 theorem forward_closed_property (P : Circle → Prop) (hclosed : IsClosed {u | P u})
73     (horbit : ∀ n : ℕ, P (rotation^n)) (u : Circle) : P u :=
74   rotation_forward_dense.induction_on u hclosed horbit
75 
76 /-- Starting at any unit spatial direction gives a dense forward orbit. -/
77 theorem rotation_orbit_dense (u : Circle) : DenseRange (fun n : ℕ => rotation^n*u) :=
78   (Homeomorph.mulRight u).surjective.denseRange.comp rotation_forward_dense
79     (Homeomorph.mulRight u).continuous
80 
81 end Komorebi.LSM.RotationDensity

Back to source controls