CountingBoundaryCover.lean

1 import PaperX.CountingBoundaryPolar
2 
3 set_option autoImplicit false
4 noncomputable section
5 
6 namespace PaperX.CountingBoundaryPolar
7 
8 open NumberField NumberField.InfinitePlace NumberField.mixedEmbedding
9 open NumberField.mixedEmbedding.fundamentalCone
10 open NumberField.Units.dirichletUnitTheorem
11 open PaperX.RayCountingGeometry
12 open scoped Classical
13 
14 variable (K : Type*) [Field K] [NumberField K]
15 
16 def signs (x : mixedSpace K) : Signs K := fun w => decide (x.1 w < 0)
17 
18 def parameters (t : ℝ) (z : realSpace K) (x : mixedSpace K) : Parameters K :=
19   Sum.elim (fun w => if w = w₀ then t else z w)
20     (fun w => (Complex.arg (x.2 w) + Real.pi) / (2 * Real.pi))
21 
22 theorem parameters_radius (t : ℝ) (z : realSpace K) (x : mixedSpace K) :
23     radius K (parameters K t z x) = t := by simp [radius, parameters]
24 
25 theorem parameters_shape (t : ℝ) {z : realSpace K} (hz : z ∈ shapeBox K)
26     (x : mixedSpace K) : shape K (parameters K t z x) = z := by
27   ext w
28   have hb := (Set.mem_univ_pi.mp hz) w
29   by_cases hw : w = w₀
30   · subst w
31     simpa [shape, parameters] using (show z w₀ = 0 from by simpa [shapeBox] using hb).symm
32   · simp [shape, parameters, hw]
33 
34 theorem parameters_angle (t : ℝ) (z : realSpace K) (x : mixedSpace K)
35     (w : ComplexPlace K) : angle K (parameters K t z x) w = Complex.arg (x.2 w) := by
36   dsimp [angle, parameters]
37   have hp : 2 * Real.pi ≠ 0 := mul_ne_zero (by norm_num) Real.pi_ne_zero
38   field_simp
39   ring
40 
41 theorem parameters_mem_cube {t : ℝ} (ht : t ∈ Set.Icc (0 : ℝ) 1)
42     {z : realSpace K} (hz : z ∈ shapeBox K) (x : mixedSpace K) :
43     parameters K t z x ∈ Set.Icc (0 : Parameters K) 1 := by
44   constructor
45   · intro i
46     rcases i with w | w
47     · dsimp [parameters]
48       split_ifs with hw
49       · exact ht.1
50       · have hb := (Set.mem_univ_pi.mp hz) w
51         exact (show z w ∈ Set.Icc (0 : ℝ) 1 from by simpa [shapeBox, hw] using hb).1
52     · dsimp [parameters]
53       exact div_nonneg (by linarith [Complex.neg_pi_lt_arg (x.2 w)]) (by positivity)
54   · intro i
55     rcases i with w | w
56     · dsimp [parameters]
57       split_ifs with hw
58       · exact ht.2
59       · have hb := (Set.mem_univ_pi.mp hz) w
60         exact (show z w ∈ Set.Icc (0 : ℝ) 1 from by simpa [shapeBox, hw] using hb).2
61     · dsimp [parameters]
62       apply (div_le_one (by positivity : (0 : ℝ) < 2 * Real.pi)).mpr
63       linarith [Complex.arg_le_pi (x.2 w)]
64 
65 theorem parameters_reconstruct {t : ℝ} {z : realSpace K}
66     (hz : z ∈ shapeBox K) (x : mixedSpace K)
67     (hm : radialChart K (t, z) = normAtAllPlaces x) :
68     polarChart K (signs K x) (parameters K t z x) = x := by
69   have hm' : moduli K (parameters K t z x) = normAtAllPlaces x := by
70     rw [moduli, parameters_radius, parameters_shape K t hz]
71     exact hm
72   apply Prod.ext
73   · funext w
74     simp only [polarChart, hm', normAtAllPlaces_apply,
75       normAtPlace_apply_of_isReal w.prop, signs]
76     by_cases hw : x.1 w < 0
77     · simp [hw, Real.norm_eq_abs, abs_of_neg hw]
78     · simp [hw, Real.norm_eq_abs, abs_of_nonneg (le_of_not_gt hw)]
79   · funext w
80     simp only [polarChart, hm', parameters_angle, normAtAllPlaces_apply,
81       normAtPlace_apply_of_isComplex w.prop]
82     exact Complex.norm_mul_exp_arg_mul_I (x.2 w)
83 
84 /-- Every actual boundary point is a signed polar chart of a cube face. -/
85 theorem frontier_cube_faces {x : mixedSpace K} (hx : x ∈ frontier (normLeOne K)) :
86     ∃ s : Signs K, ∃ u : Parameters K,
87       u ∈ Set.Icc (0 : Parameters K) 1 ∧
88       (∃ w : InfinitePlace K, u (Sum.inl w) = 0 ∨ u (Sum.inl w) = 1) ∧
89       polarChart K s u = x := by
90   rcases frontier_radial_faces K hx with hzero | ⟨t, z, ht, hz, hf, hm⟩
91   · subst x
92     refine ⟨fun _ => false, 0, ⟨le_rfl, ?_⟩, ⟨w₀, Or.inl rfl⟩, ?_⟩
93     · intro i; norm_num
94     · exact polarChart_radius_zero K _ rfl
95   · refine ⟨signs K x, parameters K t z x, parameters_mem_cube K ⟨ht.1.le, ht.2⟩ hz x,
96       ?_, parameters_reconstruct K hz x hm⟩
97     rcases hf with htop | ⟨w, hw, hface⟩
98     · exact ⟨w₀, Or.inr (by simp [parameters, htop])⟩
99     · exact ⟨w, by simpa [parameters, hw] using hface⟩
100 
101 end PaperX.CountingBoundaryPolar

Back to source controls