NormResidueGeneratorSum.lean

1 import PaperX.NormResidueWeightedCounting
2 import PaperX.NormSignPartition
3 
4 /-! The finite residue calculation is the actual principal-norm sum on cone
5 points, before applying roots-of-unity multiplicity or dividing by a norm. -/
6 set_option autoImplicit false
7 noncomputable section
8 
9 namespace PaperX.NormResidueLattice
10 open Ideal NumberField
11 open PaperX.IdealClassQuantitative PaperX.ResidueLattice PaperX.NormResidue
12 open PaperX.NormSignGeometry
13 open scoped nonZeroDivisors Classical Pointwise BigOperators
14 variable (K : Type*) [Field K] [NumberField K]
15 
16 /-- The actual absolute principal norm weight of the unique algebraic integer
17 underlying an integral ideal-lattice point. -/
18 def generatorPointWeight (J : (Ideal (𝓞 K))⁰) (m : ℕ) (χ : ZMod m → ℂ)
19     (x : idealEuclideanLattice K J) : ℂ :=
20   χ (Ideal.absNorm (Ideal.span {integerRepresentative K J x}) : ZMod m)
21 
22 theorem normWeight_actualPoint (M J : (Ideal (𝓞 K))⁰) (m : ℕ)
23     (hM : (M : Ideal (𝓞 K)) ≤ modulusIdeal (𝓞 K) m)
24     (χ : ZMod m → ℂ) (positive : Bool) {t : ℝ} (ht : 0 < t)
25     (x : LatticePoints (idealEuclideanLattice K J) (signRegion K positive) t) :
26     normWeight K M J m hM χ positive (Submodule.Quotient.mk x.1) =
27       generatorPointWeight K J m χ x.1 := by
28   have hx : integerPoint K (integerRepresentative K J x.1) ∈ t • signRegion K positive := by
29     rw [integerRepresentative_point]
30     exact x.2
31   have he := normWeight_mk K M J m hM χ positive ((idealPointEquiv K J).symm x.1) ht hx
32   rw [Equiv.apply_symm_apply] at he
33   exact he
34 
35 /-- The residue-weighted count on either sign portion is its actual point sum. -/
36 theorem weightedFiberCount_eq_generatorPointSum (M J : (Ideal (𝓞 K))⁰) (m : ℕ)
37     (hM : (M : Ideal (𝓞 K)) ≤ modulusIdeal (𝓞 K) m)
38     [Fintype (IdealResidues K M J)] (χ : ZMod m → ℂ) (positive : Bool)
39     {t : ℝ} (ht : 0 < t) :
40     weightedFiberCount (idealEuclideanLattice K M) (idealEuclideanLattice K J)
41         (signRegion K positive) (normWeight K M J m hM χ positive) t =
42       ∑ᶠ x : LatticePoints (idealEuclideanLattice K J) (signRegion K positive) t,
43         generatorPointWeight K J m χ x.1 := by
44   rw [weightedFiberCount_eq_pointSum _ _ (signRegion_bounded K positive)]
45   unfold latticePointSum
46   exact finsum_congr (normWeight_actualPoint K M J m hM χ positive ht)
47 
48 /-- Recombination gives one sum over the actual cone points, weighted by the
49 absolute norms of their actual principal ideals. No multiplicity is suppressed. -/
50 theorem normWeightedCount_eq_generatorPointSum (M J : (Ideal (𝓞 K))⁰) (m : ℕ)
51     (hM : (M : Ideal (𝓞 K)) ≤ modulusIdeal (𝓞 K) m)
52     [Fintype (IdealResidues K M J)] (χ : ZMod m → ℂ) {t : ℝ} (ht : 0 < t) :
53     normWeightedCount K M J m hM χ t =
54       ∑ᶠ x : LatticePoints (idealEuclideanLattice K J) (coneRegion K 1) t,
55         χ (Ideal.absNorm (Ideal.span {integerRepresentative K J x.1}) : ZMod m) := by
56   unfold normWeightedCount
57   simp_rw [weightedFiberCount_eq_generatorPointSum K M J m hM χ _ ht]
58   rw [Fintype.sum_bool]
59   exact (finsum_latticePoints_sign_split K (idealEuclideanLattice K J)
60     (generatorPointWeight K J m χ) ht).symm
61 
62 end PaperX.NormResidueLattice

Back to source controls