CountingBoundaryAtlas.lean

1 import PaperX.CountingBoundaryCover
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 scoped Classical
11 
12 variable (K : Type*) [Field K] [NumberField K]
13 
14 abbrev FaceCoordinates (w : InfinitePlace K) :=
15   {i : Coordinate K // i ≠ Sum.inl w}
16 abbrev FaceIndex := Signs K × InfinitePlace K × Bool
17 abbrev BoundaryParameters := Fin (Module.finrank ℚ K - 1) → ℝ
18 
19 theorem faceCoordinates_card (w : InfinitePlace K) :
20     Fintype.card (FaceCoordinates K w) = Module.finrank ℚ K - 1 := by
21   simp only [FaceCoordinates, ne_eq, Fintype.card_subtype_compl, Fintype.card_subtype_eq,
22     coordinate_card]
23 
24 def faceEquiv (w : InfinitePlace K) :
25     FaceCoordinates K w ≃ Fin (Module.finrank ℚ K - 1) :=
26   Fintype.equivFinOfCardEq (faceCoordinates_card K w)
27 
28 def insertFace (w : InfinitePlace K) (b : Bool) (v : BoundaryParameters K) : Parameters K :=
29   fun i => if h : i = Sum.inl w then (if b then 1 else 0) else v (faceEquiv K w ⟨i, h⟩)
30 
31 def faceChart (j : FaceIndex K) (v : BoundaryParameters K) : mixedSpace K :=
32   polarChart K j.1 (insertFace K j.2.1 j.2.2 v)
33 
34 theorem insertFace_contDiff (w : InfinitePlace K) (b : Bool) :
35     ContDiff ℝ 1 (insertFace K w b) := by
36   apply contDiff_pi.mpr
37   intro i
38   dsimp [insertFace]
39   by_cases h : i = Sum.inl w
40   · simp only [dite_eq_left h]
41     exact contDiff_const
42   · simp only [dite_eq_right h]
43     exact contDiff_apply ℝ ℝ (faceEquiv K w ⟨i, h⟩)
44 
45 theorem faceChart_contDiff (j : FaceIndex K) : ContDiff ℝ 1 (faceChart K j) :=
46   (polarChart_contDiff K j.1).comp (insertFace_contDiff K j.2.1 j.2.2)
47 
48 theorem faceChart_lipschitz (j : FaceIndex K) : ∃ C : NNReal,
49     LipschitzOnWith C (faceChart K j) (Set.Icc (0 : BoundaryParameters K) 1) := by
50   apply (faceChart_contDiff K j).contDiffOn.exists_lipschitzOnWith (by decide)
51   · exact convex_Icc _ _
52   · exact isCompact_Icc
53 
54 theorem faceChart_common_lipschitz : ∃ C : NNReal, ∀ j : FaceIndex K,
55     LipschitzOnWith C (faceChart K j) (Set.Icc (0 : BoundaryParameters K) 1) := by
56   let c : FaceIndex K → NNReal := fun j => (faceChart_lipschitz K j).choose
57   refine ⟨Finset.univ.sup c, fun j => ?_⟩
58   exact (faceChart_lipschitz K j).choose_spec.weaken
59     (Finset.le_sup (f := c) (Finset.mem_univ j))
60 
61 def restrictFace (w : InfinitePlace K) (u : Parameters K) : BoundaryParameters K :=
62   fun i => u ((faceEquiv K w).symm i).1
63 
64 theorem insertFace_restrictFace (w : InfinitePlace K) (b : Bool) (u : Parameters K)
65     (hu : u (Sum.inl w) = if b then 1 else 0) :
66     insertFace K w b (restrictFace K w u) = u := by
67   ext i
68   by_cases hi : i = Sum.inl w
69   · subst i
70     simp [insertFace, hu]
71   · simp [insertFace, restrictFace, hi]
72 
73 theorem restrictFace_mem_cube (w : InfinitePlace K) {u : Parameters K}
74     (hu : u ∈ Set.Icc (0 : Parameters K) 1) :
75     restrictFace K w u ∈ Set.Icc (0 : BoundaryParameters K) 1 :=
76   ⟨fun _ => hu.1 _, fun _ => hu.2 _⟩
77 
78 /-- Actual mixed-space frontier covered by finitely many smooth charts of dimension `d-1`. -/
79 theorem frontier_faceChart_cover :
80     frontier (normLeOne K) ⊆
81       ⋃ j : FaceIndex K, faceChart K j '' Set.Icc (0 : BoundaryParameters K) 1 := by
82   intro x hx
83   obtain ⟨s, u, hu, ⟨w, hw⟩, heq⟩ := frontier_cube_faces K hx
84   rcases hw with hw | hw
85   · refine Set.mem_iUnion.mpr ⟨(s, w, false), restrictFace K w u,
86       restrictFace_mem_cube K w hu, ?_⟩
87     dsimp [faceChart]
88     rw [insertFace_restrictFace K w false u (by simpa using hw)]
89     exact heq
90   · refine Set.mem_iUnion.mpr ⟨(s, w, true), restrictFace K w u,
91       restrictFace_mem_cube K w hu, ?_⟩
92     dsimp [faceChart]
93     rw [insertFace_restrictFace K w true u (by simpa using hw)]
94     exact heq
95 
96 /-- A uniform Lipschitz boundary atlas with the exact parameter dimension, including degree one. -/
97 theorem exists_boundary_atlas :
98     ∃ m : ℕ, ∃ C : NNReal,
99     ∃ f : Fin m → BoundaryParameters K → mixedSpace K,
100       (∀ j, LipschitzOnWith C (f j) (Set.Icc (0 : BoundaryParameters K) 1)) ∧
101       frontier (normLeOne K) ⊆
102         ⋃ j : Fin m, f j '' Set.Icc (0 : BoundaryParameters K) 1 := by
103   obtain ⟨C, hC⟩ := faceChart_common_lipschitz K
104   let e := Fintype.equivFin (FaceIndex K)
105   refine ⟨Fintype.card (FaceIndex K), C, fun j => faceChart K (e.symm j),
106     fun j => hC _, ?_⟩
107   intro x hx
108   obtain ⟨j, hj⟩ := Set.mem_iUnion.mp (frontier_faceChart_cover K hx)
109   refine Set.mem_iUnion.mpr ⟨e j, ?_⟩
110   simpa using hj
111 
112 end PaperX.CountingBoundaryPolar

Back to source controls