NormSignPartition.lean

1 import PaperX.NormSignResidueCounting
2 import PaperX.ResidueLatticePointSums
3 
4 /-! Exact decomposition of actual cone points and their sums by norm sign. -/
5 set_option autoImplicit false
6 noncomputable section
7 
8 namespace PaperX.NormSignGeometry
9 open Set NumberField NumberField.mixedEmbedding
10 open IdealClassQuantitative ResidueLattice
11 open scoped Classical Pointwise BigOperators
12 variable (K : Type*) [Field K] [NumberField K]
13 
14 theorem signRegion_disjoint : Disjoint (signRegion K true) (signRegion K false) := by
15   rw [Set.disjoint_left]
16   intro x hx hy
17   exact Set.disjoint_left.mp (signCone_disjoint K) hx hy
18 
19 theorem signRegion_union : signRegion K true ∪ signRegion K false = coneRegion K 1 := by
20   rw [signRegion, signRegion, ← Set.preimage_union, signCone_union, coneRegion_one]
21 
22 theorem smul_signRegion_disjoint {t : ℝ} (ht : 0 < t) :
23     Disjoint (t • signRegion K true) (t • signRegion K false) := by
24   rw [Set.disjoint_left]
25   intro x hx hy
26   exact Set.disjoint_left.mp (signRegion_disjoint K)
27     ((Set.mem_smul_set_iff_inv_smul_mem₀ ht.ne' _ _).mp hx)
28     ((Set.mem_smul_set_iff_inv_smul_mem₀ ht.ne' _ _).mp hy)
29 
30 theorem smul_signRegion_union (t : ℝ) :
31     t • signRegion K true ∪ t • signRegion K false = t • coneRegion K 1 := by
32   rw [← Set.smul_set_union, signRegion_union]
33 
34 /-- The actual bounded lattice points split into the two disjoint sign portions. -/
35 def latticePointsSignEquiv (L : Submodule ℤ (euclidean.mixedSpace K)) {t : ℝ} (ht : 0 < t) :
36     LatticePoints L (coneRegion K 1) t ≃
37       LatticePoints L (signRegion K true) t ⊕ LatticePoints L (signRegion K false) t := by
38   let P : Set L := {x | (x : euclidean.mixedSpace K) ∈ t • signRegion K true}
39   let N : Set L := {x | (x : euclidean.mixedSpace K) ∈ t • signRegion K false}
40   have hd : Disjoint P N := by
41     rw [Set.disjoint_left]
42     intro x hx hy
43     exact Set.disjoint_left.mp (smul_signRegion_disjoint K ht) hx hy
44   have he : ∀ x : L, (x : euclidean.mixedSpace K) ∈ t • coneRegion K 1 ↔ x ∈ P ∪ N := by
45     intro x
46     change (x : euclidean.mixedSpace K) ∈ t • coneRegion K 1 ↔
47       (x : euclidean.mixedSpace K) ∈ t • signRegion K true ∪ t • signRegion K false
48     rw [smul_signRegion_union]
49   exact (Equiv.subtypeEquivRight he).trans (Equiv.Set.union hd)
50 
51 @[simp]
52 theorem latticePointsSignEquiv_symm_inl_coe
53     (L : Submodule ℤ (euclidean.mixedSpace K)) {t : ℝ} (ht : 0 < t)
54     (x : LatticePoints L (signRegion K true) t) :
55     ((latticePointsSignEquiv K L ht).symm (Sum.inl x)).1 = x.1 := rfl
56 
57 @[simp]
58 theorem latticePointsSignEquiv_symm_inr_coe
59     (L : Submodule ℤ (euclidean.mixedSpace K)) {t : ℝ} (ht : 0 < t)
60     (x : LatticePoints L (signRegion K false) t) :
61     ((latticePointsSignEquiv K L ht).symm (Sum.inr x)).1 = x.1 := rfl
62 
63 /-- Every complex weight on the actual lattice points splits without changing
64 the underlying points. All three domains are finite by boundedness. -/
65 theorem finsum_latticePoints_sign_split
66     (L : Submodule ℤ (euclidean.mixedSpace K)) [DiscreteTopology L]
67     (w : L → ℂ) {t : ℝ} (ht : 0 < t) :
68     (∑ᶠ x : LatticePoints L (coneRegion K 1) t, w x.1) =
69       (∑ᶠ x : LatticePoints L (signRegion K true) t, w x.1) +
70       (∑ᶠ x : LatticePoints L (signRegion K false) t, w x.1) := by
71   let : Finite (LatticePoints L (coneRegion K 1) t) :=
72     finite_latticePoints L (coneRegion_one_bounded K) t
73   let : Finite (LatticePoints L (signRegion K true) t) :=
74     finite_latticePoints L (signRegion_bounded K true) t
75   let : Finite (LatticePoints L (signRegion K false) t) :=
76     finite_latticePoints L (signRegion_bounded K false) t
77   let : Fintype (LatticePoints L (coneRegion K 1) t) := Fintype.ofFinite _
78   let : Fintype (LatticePoints L (signRegion K true) t) := Fintype.ofFinite _
79   let : Fintype (LatticePoints L (signRegion K false) t) := Fintype.ofFinite _
80   rw [finsum_eq_sum_of_fintype, finsum_eq_sum_of_fintype, finsum_eq_sum_of_fintype]
81   rw [← (latticePointsSignEquiv K L ht).symm.sum_comp (fun x => w x.1),
82     Fintype.sum_sum_type]
83   simp only [latticePointsSignEquiv_symm_inl_coe, latticePointsSignEquiv_symm_inr_coe]
84 
85 end PaperX.NormSignGeometry

Back to source controls