CountingBoundaryPolar.lean

1 import PaperX.RayCountingGeometry
2 import Mathlib.Analysis.SpecialFunctions.Complex.Arg
3 
4 set_option autoImplicit false
5 noncomputable section
6 
7 namespace PaperX.CountingBoundaryPolar
8 
9 open NumberField NumberField.InfinitePlace NumberField.mixedEmbedding
10 open NumberField.mixedEmbedding.fundamentalCone
11 open NumberField.Units.dirichletUnitTheorem
12 open PaperX.RayCountingGeometry
13 open scoped Classical
14 
15 variable (K : Type*) [Field K] [NumberField K]
16 
17 abbrev RealPlace := {w : InfinitePlace K // IsReal w}
18 abbrev ComplexPlace := {w : InfinitePlace K // IsComplex w}
19 abbrev Coordinate := InfinitePlace K ⊕ ComplexPlace K
20 abbrev Parameters := Coordinate K → ℝ
21 abbrev Signs := RealPlace K → Bool
22 
23 theorem coordinate_card : Fintype.card (Coordinate K) = Module.finrank ℚ K := by
24   rw [Fintype.card_sum, card_eq_nrRealPlaces_add_nrComplexPlaces]
25   change nrRealPlaces K + nrComplexPlaces K + nrComplexPlaces K = _
26   have h := card_add_two_mul_card_eq_rank K
27   omega
28 
29 open scoped Classical in
30 def shape (u : Parameters K) : realSpace K :=
31   fun w => if w = w₀ then 0 else u (Sum.inl w)
32 
33 def radius (u : Parameters K) : ℝ := u (Sum.inl w₀)
34 def angle (u : Parameters K) (w : ComplexPlace K) : ℝ :=
35   -Real.pi + (2 * Real.pi) * u (Sum.inr w)
36 
37 def moduli (u : Parameters K) : realSpace K :=
38   radius K u • expMapBasis (shape K u)
39 
40 def polarChart (s : Signs K) (u : Parameters K) : mixedSpace K :=
41   (fun w => (if s w then -1 else 1) * moduli K u w.1,
42    fun w => (moduli K u w.1 : ℂ) * Complex.exp ((angle K u w : ℂ) * Complex.I))
43 
44 theorem shape_contDiff : ContDiff ℝ 1 (shape K) := by
45   classical
46   apply contDiff_pi.mpr
47   intro w
48   dsimp [shape]
49   split_ifs
50   · exact contDiff_const
51   · exact contDiff_apply ℝ ℝ _
52 
53 theorem moduli_contDiff : ContDiff ℝ 1 (moduli K) := by
54   exact (contDiff_apply ℝ ℝ (Sum.inl w₀)).smul
55     ((expMapBasis_contDiff K).comp (shape_contDiff K))
56 
57 theorem polarChart_contDiff (s : Signs K) : ContDiff ℝ 1 (polarChart K s) := by
58   apply ContDiff.prodMk
59   · apply contDiff_pi.mpr
60     intro w
61     exact contDiff_const.mul ((contDiff_apply ℝ ℝ w.1).comp (moduli_contDiff K))
62   · apply contDiff_pi.mpr
63     intro w
64     apply ContDiff.mul
65     · exact Complex.ofRealCLM.contDiff.comp
66         ((contDiff_apply ℝ ℝ w.1).comp (moduli_contDiff K))
67     · apply ContDiff.cexp
68       exact (Complex.ofRealCLM.contDiff.comp
69         (contDiff_const.add (contDiff_const.mul (contDiff_apply ℝ ℝ (Sum.inr w))))).mul contDiff_const
70 
71 theorem polarChart_lipschitz (s : Signs K) : ∃ C : NNReal,
72     LipschitzOnWith C (polarChart K s) (Set.Icc (0 : Parameters K) 1) := by
73   apply (polarChart_contDiff K s).contDiffOn.exists_lipschitzOnWith (by decide)
74   · exact convex_Icc _ _
75   · exact isCompact_Icc
76 
77 /-- The physical radial coordinate includes the origin smoothly. -/
78 theorem polarChart_radius_zero (s : Signs K) {u : Parameters K}
79     (hu : radius K u = 0) : polarChart K s u = 0 := by
80   ext w <;> simp [polarChart, moduli, hu]
81 
82 end PaperX.CountingBoundaryPolar

Back to source controls