NormSignGeometry.lean

1 import PaperX.CountingBoundaryTransport
2 import PaperX.LatticeCountingFull
3 import PaperX.IdealClassQuantitativeGeometry
4 
5 /-! Sign restrictions on the actual number-field cone retain its boundary atlas.
6 This module uses the product of the real embedding coordinates; no field-norm
7 congruence is inferred by ignoring its sign. -/
8 set_option autoImplicit false
9 noncomputable section
10 
11 namespace PaperX.NormSignGeometry
12 open Set MeasureTheory Module
13 open NumberField NumberField.InfinitePlace NumberField.mixedEmbedding
14 open NumberField.mixedEmbedding.fundamentalCone
15 open scoped Classical Pointwise
16 
17 /-- Cutting along the sign of a continuous nonvanishing function creates no new
18 frontier away from the old frontier. -/
19 theorem frontier_positive_restriction {E : Type*} [TopologicalSpace E]
20     {D : Set E} {f : E → ℝ} (hf : Continuous f)
21     (hne : ∀ x ∈ D, f x ≠ 0) :
22     frontier (D ∩ {x | 0 < f x}) ⊆ frontier D := by
23   intro x hx
24   rcases frontier_inter_subset D {x | 0 < f x} hx with h | h
25   · exact h.1
26   · by_cases hxD : x ∈ D
27     · have he : (0 : ℝ) = f x := frontier_lt_subset_eq continuous_const hf h.2
28       exact False.elim (hne x hxD he.symm)
29     · exact ⟨h.1, fun hi => hxD (interior_subset hi)⟩
30 
31 variable (K : Type*) [Field K] [NumberField K]
32 
33 /-- The real-coordinate product whose sign records the real embedding signs. -/
34 def realProduct (x : mixedSpace K) : ℝ := ∏ w : {w : InfinitePlace K // IsReal w}, x.1 w
35 
36 theorem realProduct_continuous : Continuous (realProduct K) := by
37   unfold realProduct
38   fun_prop
39 
40 theorem realProduct_ne_zero {x : mixedSpace K} (hx : x ∈ normLeOne K) :
41     realProduct K x ≠ 0 := by
42   apply Finset.prod_ne_zero_iff.mpr
43   intro w _
44   have h := fundamentalCone.normAtPlace_pos_of_mem hx.1 w.1
45   rw [normAtPlace_apply_of_isReal w.2] at h
46   exact norm_pos_iff.mp h
47 
48 /-- The two real-sign portions of the actual unit cone. -/
49 def signCone (positive : Bool) : Set (mixedSpace K) :=
50   normLeOne K ∩ {x | 0 < if positive then realProduct K x else -realProduct K x}
51 
52 theorem signCone_frontier_subset (positive : Bool) :
53     frontier (signCone K positive) ⊆ frontier (normLeOne K) := by
54   apply frontier_positive_restriction
55   · cases positive <;> simp only [Bool.false_eq_true, ↓reduceIte] <;>
56       first | exact (realProduct_continuous K).neg | exact realProduct_continuous K
57   · intro x hx
58     cases positive <;> simp only [Bool.false_eq_true, ↓reduceIte, neg_ne_zero] <;>
59       exact realProduct_ne_zero K hx
60 
61 theorem signCone_measurable (positive : Bool) : MeasurableSet (signCone K positive) := by
62   apply (measurableSet_normLeOne K).inter
63   apply measurableSet_lt measurable_const
64   cases positive <;> simp only [Bool.false_eq_true, ↓reduceIte] <;>
65     first | exact (realProduct_continuous K).neg.measurable | exact (realProduct_continuous K).measurable
66 
67 theorem signCone_bounded (positive : Bool) : Bornology.IsBounded (signCone K positive) :=
68   (isBounded_normLeOne K).subset inter_subset_left
69 
70 theorem signCone_disjoint : Disjoint (signCone K true) (signCone K false) := by
71   rw [Set.disjoint_left]
72   intro x hx hy
73   have hp : 0 < realProduct K x := hx.2
74   have hn : 0 < -realProduct K x := hy.2
75   linarith
76 
77 theorem signCone_union : signCone K true ∪ signCone K false = normLeOne K := by
78   apply Set.Subset.antisymm
79   · exact union_subset inter_subset_left inter_subset_left
80   · intro x hx
81     rcases lt_or_gt_of_ne (realProduct_ne_zero K hx) with hn | hp
82     · exact Or.inr ⟨hx, neg_pos.mpr hn⟩
83     · exact Or.inl ⟨hx, hp⟩
84 
85 /-- The already constructed actual boundary charts also cover either sign portion. -/
86 def signConeAtlas {ι : Type*} [Fintype ι]
87     (e : mixedSpace K ≃L[ℝ] (ι → ℝ))
88     (hcard : Fintype.card ι = Module.finrank ℚ K) (positive : Bool) :
89     LatticeCounting.LipschitzBoundaryAtlas ι (e '' signCone K positive) :=
90   { CountingBoundaryPolar.boundaryAtlas_image K e hcard with
91     covers := by
92       intro y hy
93       apply (CountingBoundaryPolar.boundaryAtlas_image K e hcard).covers
94       have hs := Set.image_mono (f := e.toHomeomorph) (signCone_frontier_subset K positive)
95       rw [e.toHomeomorph.image_frontier, e.toHomeomorph.image_frontier] at hs
96       exact hs hy }
97 
98 end PaperX.NormSignGeometry

Back to source controls