RayCountingGeometry.lean

1 import Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
2 import Mathlib.Analysis.Calculus.ContDiff.RCLike
3 
4 /-!
5 Concrete geometry of the existing ordinary unit cone. This module locates its frontier in
6 parameter faces and gives a Lipschitz physical radial parametrization on the normalized box.
7 It does not yet construct the sign/angle boundary atlas in mixed space or count lattice points.
8 -/
9 
10 set_option autoImplicit false
11 noncomputable section
12 
13 namespace PaperX.RayCountingGeometry
14 
15 open NumberField NumberField.InfinitePlace NumberField.mixedEmbedding
16 open NumberField.mixedEmbedding.fundamentalCone
17 open NumberField.Units.dirichletUnitTheorem
18 open scoped Pointwise
19 
20 variable (K : Type*) [Field K] [NumberField K]
21 
22 /-- Every nonzero boundary point comes from a boundary point of the logarithmic parameter set. -/
23 theorem frontier_moduli {x : mixedSpace K} (hx : x ∈ frontier (normLeOne K)) :
24     x = 0 ∨ ∃ y : realSpace K,
25       y ∈ frontier (paramSet K) ∧ expMapBasis y = normAtAllPlaces x := by
26   have hc := closure_normLeOne_subset K hx.1
27   change normAtAllPlaces x ∈ compactSet K at hc
28   rw [compactSet_eq_union] at hc
29   rcases hc with ⟨y, hy, heq⟩ | hz
30   · right
31     refine ⟨y, ⟨hy, ?_⟩, heq⟩
32     intro hi
33     exact hx.2 (subset_interior_normLeOne K ⟨y, hi, heq⟩)
34   · left
35     apply forall_normAtPlace_eq_zero_iff.mp
36     intro w
37     exact congrFun (Set.mem_singleton_iff.mp hz) w
38 
39 /-- The parameter frontier consists only of the radial top or faces of the unit box. -/
40 theorem frontier_parameter_faces {y : realSpace K} (hy : y ∈ frontier (paramSet K)) :
41     y w₀ = 0 ∨ ∃ w : InfinitePlace K, w ≠ w₀ ∧ (y w = 0 ∨ y w = 1) := by
42   classical
43   have hb : ∀ w, y w ∈ (if w = w₀ then Set.Iic 0 else Set.Icc 0 1) := by
44     simpa only [closure_paramSet, Set.mem_univ_pi] using hy.1
45   by_contra hn
46   push Not at hn
47   apply hy.2
48   rw [interior_paramSet, Set.mem_univ_pi]
49   intro w
50   by_cases hw : w = w₀
51   · subst w
52     simp only [ite_true, Set.mem_Iio]
53     exact lt_of_le_of_ne (by simpa using hb w₀) hn.1
54   · simp only [hw, ite_false, Set.mem_Ioo]
55     have hbw : 0 ≤ y w ∧ y w ≤ 1 := by simpa [hw] using hb w
56     exact ⟨lt_of_le_of_ne hbw.1 (Ne.symm (hn.2 w hw).1),
57       lt_of_le_of_ne hbw.2 (hn.2 w hw).2⟩
58 
59 open scoped Classical in
60 /-- The normalized shape box from the actual fundamental-cone coordinates. -/
61 def shapeBox : Set (realSpace K) :=
62   Set.univ.pi fun w => if w = w₀ then {0} else Set.Icc 0 1
63 
64 theorem shapeBox_compact : IsCompact (shapeBox K) := by
65   classical
66   apply isCompact_univ_pi
67   intro w
68   split_ifs
69   · exact isCompact_singleton
70   · exact isCompact_Icc
71 
72 theorem shapeBox_convex : Convex ℝ (shapeBox K) := by
73   classical
74   apply convex_pi
75   intro w _
76   split_ifs
77   · exact convex_singleton 0
78   · exact convex_Icc 0 1
79 
80 /-- Radial compactification uses a physical scalar, with no logarithm at the origin. -/
81 def radialChart (p : ℝ × realSpace K) : realSpace K := p.1 • expMapBasis p.2
82 
83 theorem expMapBasis_contDiff : ContDiff ℝ 1 (expMapBasis : realSpace K → realSpace K) := by
84   apply contDiff_pi.mpr
85   intro w
86   simp only [expMapBasis_apply, expMap_apply]
87   exact (contDiff_const.mul
88     ((contDiff_apply ℝ ℝ w).comp (completeBasis K).equivFunL.symm.contDiff)).exp
89 
90 theorem radialChart_contDiff : ContDiff ℝ 1 (radialChart K) :=
91   contDiff_fst.smul ((expMapBasis_contDiff K).comp contDiff_snd)
92 
93 theorem radialChart_lipschitz : ∃ C : NNReal,
94     LipschitzOnWith C (radialChart K) (Set.Icc (0 : ℝ) 1 ×ˢ shapeBox K) := by
95   apply (radialChart_contDiff K).contDiffOn.exists_lipschitzOnWith (by decide)
96   · exact (convex_Icc 0 1).prod (shapeBox_convex K)
97   · exact isCompact_Icc.prod (shapeBox_compact K)
98 
99 theorem radialChart_image :
100     radialChart K '' (Set.Icc 0 1 ×ˢ shapeBox K) = compactSet K := by
101   ext y
102   simp only [Set.mem_image, Set.mem_prod, radialChart, compactSet, shapeBox,
103     Set.mem_smul, exists_exists_and_eq_and]
104   constructor
105   · rintro ⟨⟨t, z⟩, ⟨ht, hz⟩, rfl⟩
106     exact ⟨t, ht, z, hz, rfl⟩
107   · rintro ⟨t, ht, z, hz, rfl⟩
108     exact ⟨(t, z), ⟨ht, hz⟩, rfl⟩
109 
110 /-- Nonzero boundary moduli lie on the radial top or a face of the compact unit box. -/
111 theorem frontier_radial_faces {x : mixedSpace K} (hx : x ∈ frontier (normLeOne K)) :
112     x = 0 ∨ ∃ t : ℝ, ∃ z : realSpace K,
113       t ∈ Set.Ioc 0 1 ∧ z ∈ shapeBox K ∧
114       (t = 1 ∨ ∃ w : InfinitePlace K, w ≠ w₀ ∧ (z w = 0 ∨ z w = 1)) ∧
115       radialChart K (t, z) = normAtAllPlaces x := by
116   classical
117   rcases frontier_moduli K hx with hzero | ⟨y, hy, heq⟩
118   · exact Or.inl hzero
119   have hb : ∀ w, y w ∈ (if w = w₀ then Set.Iic 0 else Set.Icc 0 1) := by
120     simpa only [closure_paramSet, Set.mem_univ_pi] using hy.1
121   right
122   refine ⟨Real.exp (y w₀), fun w => if w = w₀ then 0 else y w, ?_, ?_, ?_, ?_⟩
123   · exact ⟨Real.exp_pos _, Real.exp_le_one_iff.mpr (by simpa using hb w₀)⟩
124   · rw [shapeBox, Set.mem_univ_pi]
125     intro w
126     by_cases hw : w = w₀
127     · simp [hw]
128     · simpa [hw] using hb w
129   · rcases frontier_parameter_faces K hy with hr | ⟨w, hw, hwf⟩
130     · exact Or.inl (by simp [hr])
131     · exact Or.inr ⟨w, hw, by simpa [hw] using hwf⟩
132   · exact (expMapBasis_apply'' y).symm.trans heq
133 
134 end PaperX.RayCountingGeometry

Back to source controls