CountingBoundaryTransport.lean

1 import PaperX.CountingBoundaryAtlas
2 import PaperX.LatticeCountingInterface
3 
4 set_option autoImplicit false
5 noncomputable section
6 
7 namespace PaperX.CountingBoundaryPolar
8 
9 open NumberField NumberField.mixedEmbedding
10 open NumberField.mixedEmbedding.fundamentalCone
11 open PaperX.LatticeCounting
12 open scoped Classical
13 
14 variable (K : Type*) [Field K] [NumberField K]
15 
16 /-- The actual cone supplies the grid-counting atlas after any continuous linear coordinates. -/
17 theorem nonempty_boundaryAtlas_image {ι : Type*} [Fintype ι]
18     (e : mixedSpace K ≃L[ℝ] (ι → ℝ))
19     (hcard : Fintype.card ι = Module.finrank ℚ K) :
20     Nonempty (LipschitzBoundaryAtlas ι (e '' normLeOne K)) := by
21   let P (n : ℕ) : Prop := ∃ m : ℕ, ∃ C : NNReal,
22       ∃ f : Fin m → (Fin (n - 1) → ℝ) → mixedSpace K,
23         (∀ j, LipschitzOnWith C (f j) (Set.Icc (0 : Fin (n - 1) → ℝ) 1)) ∧
24         frontier (normLeOne K) ⊆ ⋃ j : Fin m,
25           f j '' Set.Icc (0 : Fin (n - 1) → ℝ) 1
26   have hd : P (Module.finrank ℚ K) := exists_boundary_atlas K
27   have h : P (Fintype.card ι) := Eq.mpr (congrArg P hcard) hd
28   obtain ⟨m, C, f, hf, hcover⟩ := h
29   refine ⟨{ charts := m
30             lip := ‖e.toContinuousLinearMap‖₊ * C
31             map := fun j v => e (f j v)
32             lipschitz := fun j => e.toContinuousLinearMap.lipschitzWith.comp_lipschitzOnWith (hf j)
33             covers := ?_ }⟩
34   intro y hy
35   have hy' : y ∈ e '' frontier (normLeOne K) := by
36     change y ∈ e.toHomeomorph '' frontier (normLeOne K)
37     rw [e.toHomeomorph.image_frontier]
38     exact hy
39   obtain ⟨x, hx, rfl⟩ := hy'
40   obtain ⟨j, v, hv, heq⟩ := Set.mem_iUnion.mp (hcover hx)
41   refine Set.mem_iUnion.mpr ⟨j, v, hv, ?_⟩
42   exact congrArg e heq
43 
44 def boundaryAtlas_image {ι : Type*} [Fintype ι]
45     (e : mixedSpace K ≃L[ℝ] (ι → ℝ))
46     (hcard : Fintype.card ι = Module.finrank ℚ K) :
47     LipschitzBoundaryAtlas ι (e '' normLeOne K) :=
48   Classical.choice (nonempty_boundaryAtlas_image K e hcard)
49 
50 end PaperX.CountingBoundaryPolar

Back to source controls