NormResidueGeneratorAttachment.lean

1 import PaperX.NormResidueLatticeMap
2 import PaperX.IdealNormWeightedAttachment
3 import PaperX.ResidueLatticePointSums
4 
5 /-! Exact attachment of cone lattice sums to bounded algebraic generators. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperX.NormResidueLattice
9 open Ideal NumberField
10 open NumberField.mixedEmbedding NumberField.mixedEmbedding.fundamentalCone
11 open NumberField.mixedEmbedding.euclidean
12 open PaperX.IdealClassQuantitative PaperX.ResidueLattice PaperX.IdealNormWeighted
13 open scoped nonZeroDivisors Classical Pointwise
14 
15 variable (K : Type*) [Field K] [NumberField K]
16 
17 /-- The absolute principal norm at an actual ideal-lattice point is its mixed norm. -/
18 theorem integerRepresentative_absNorm_cast (J : (Ideal (𝓞 K))⁰)
19     (x : idealEuclideanLattice K J) :
20     (absNorm (span {integerRepresentative K J x}) : ℝ) =
21       mixedEmbedding.norm (toMixed K x.1) := by
22   rw [absNorm_span_singleton, Nat.cast_natAbs, ← Rat.cast_intCast, Int.cast_abs,
23     Algebra.coe_norm_int, ← norm_eq_norm]
24   congr 1
25   have h := congrArg (toMixed K) (integerRepresentative_point K J x)
26   simpa only [integerPoint, ContinuousLinearEquiv.apply_symm_apply] using h
27 
28 /-- The bounded cone-point equivalence preserves the represented mixed coordinate. -/
29 theorem coneLatticeEquiv_coe (J : (Ideal (𝓞 K))⁰) (Y : ℝ)
30     (x : (coneRegion K Y ∩ idealEuclideanLattice K J : Set (euclidean.mixedSpace K))) :
31     ((coneLatticeEquiv K J Y x).val : mixedSpace K) = toMixed K x.val := rfl
32 
33 /-- Actual dilated lattice points correspond to generators bounded by the degree power. -/
34 def latticePointsGeneratorEquiv (J : (Ideal (𝓞 K))⁰) {t : ℝ} (ht : 0 < t) :
35     LatticePoints (idealEuclideanLattice K J) (coneRegion K 1) t ≃
36       {a : idealSet K J // mixedEmbedding.norm (a : mixedSpace K) ≤
37         t ^ Module.finrank ℚ K} := by
38   let e : LatticePoints (idealEuclideanLattice K J) (coneRegion K 1) t ≃
39       (coneRegion K (t ^ Module.finrank ℚ K) ∩ idealEuclideanLattice K J :
40         Set (euclidean.mixedSpace K)) :=
41     { toFun := fun x => ⟨x.1.1, ⟨by
42         rw [← smul_coneRegion_one K ht]
43         exact x.2, x.1.2⟩⟩
44       invFun := fun x => ⟨⟨x.1, x.2.2⟩, by
45         rw [smul_coneRegion_one K ht]
46         exact x.2.1⟩
47       left_inv := fun _ => rfl
48       right_inv := fun _ => rfl }
49   exact e.trans (coneLatticeEquiv K J _)
50 
51 /-- This equivalence preserves the actual natural-number norm used by every weight. -/
52 theorem latticePointsGeneratorEquiv_absNorm (J : (Ideal (𝓞 K))⁰) {t : ℝ}
53     (ht : 0 < t) (x : LatticePoints (idealEuclideanLattice K J) (coneRegion K 1) t) :
54     generatorAbsNorm K J (latticePointsGeneratorEquiv K J ht x).val =
55       absNorm (span {integerRepresentative K J x.val}) := by
56   apply Nat.cast_injective (R := ℝ)
57   rw [generatorAbsNorm_cast, integerRepresentative_absNorm_cast]
58   rfl
59 
60 /-- Arbitrary norm weights agree exactly on the lattice and algebraic-generator domains. -/
61 theorem latticeGeneratorSum_eq_boundedGeneratorSum (J : (Ideal (𝓞 K))⁰)
62     (f : ℕ → ℂ) {t : ℝ} (ht : 0 < t) :
63     (∑ᶠ x : LatticePoints (idealEuclideanLattice K J) (coneRegion K 1) t,
64       f (absNorm (span {integerRepresentative K J x.val}))) =
65       boundedGeneratorSum K J f (t ^ Module.finrank ℚ K) := by
66   unfold boundedGeneratorSum
67   exact finsum_eq_of_bijective (latticePointsGeneratorEquiv K J ht)
68     (latticePointsGeneratorEquiv K J ht).bijective
69     (fun x => congrArg f (latticePointsGeneratorEquiv_absNorm K J ht x).symm)
70 
71 end PaperX.NormResidueLattice

Back to source controls