NormResidueWeightedCounting.lean

1 import PaperX.NormResidueLatticeMap
2 import PaperX.NormSignDilation
3 
4 /-! Computed finite norm weights on the two actual sign regions.
5 The zero-mean premise concerns the actual ideal-lattice quotient; it is not
6 inferred from nontriviality of a character on a larger residue ring. -/
7 set_option autoImplicit false
8 noncomputable section
9 namespace PaperX.NormResidueLattice
10 open Ideal NumberField Module MeasureTheory
11 open PaperX.IdealClassQuantitative PaperX.ResidueLattice PaperX.NormResidue
12 open PaperX.NormSignGeometry PaperX.NormSignArithmetic
13 open scoped nonZeroDivisors Pointwise Classical
14 
15 variable (K : Type*) [Field K] [NumberField K]
16 
17 /-- A finite arithmetic norm weight, corrected for the sign of the field norm. -/
18 def normWeight (M J : (Ideal (𝓞 K))⁰) (m : ℕ)
19     (hM : (M : Ideal (𝓞 K)) ≤ modulusIdeal (𝓞 K) m)
20     (χ : ZMod m → ℂ) (positive : Bool) (c : IdealResidues K M J) : ℂ :=
21   χ (if positive then residueNorm K M J m hM c else -residueNorm K M J m hM c)
22 
23 /-- At every counted integer, the computed residue weight is its actual absolute principal norm. -/
24 theorem normWeight_mk (M J : (Ideal (𝓞 K))⁰) (m : ℕ)
25     (hM : (M : Ideal (𝓞 K)) ≤ modulusIdeal (𝓞 K) m)
26     (χ : ZMod m → ℂ) (positive : Bool) (x : (J : Ideal (𝓞 K)))
27     {t : ℝ} (ht : 0 < t) (hx : integerPoint K x.1 ∈ t • signRegion K positive) :
28     normWeight K M J m hM χ positive (Submodule.Quotient.mk (idealPointEquiv K J x)) =
29       χ (Ideal.absNorm (Ideal.span {x.1}) : ZMod m) := by
30   cases positive with
31   | true =>
32     have hs := (integer_norm_pos_of_mem_smul_signRegion K ht hx).le
33     have hn := principal_absNorm_residue_nonneg K m hs
34     rw [integerQuotientNorm_mk] at hn
35     simp only [normWeight, ↓reduceIte, residueNorm_mk]
36     exact congrArg χ hn.symm
37   | false =>
38     have hs := (integer_norm_neg_of_mem_smul_signRegion K ht hx).le
39     have hn := principal_absNorm_residue_nonpos K m hs
40     rw [integerQuotientNorm_mk] at hn
41     simp only [normWeight, Bool.false_eq_true, ↓reduceIte, residueNorm_mk]
42     exact congrArg χ hn.symm
43 
44 /-- The two sign portions recombined before any roots-of-unity division. -/
45 def normWeightedCount (M J : (Ideal (𝓞 K))⁰) (m : ℕ)
46     (hM : (M : Ideal (𝓞 K)) ≤ modulusIdeal (𝓞 K) m)
47     [Fintype (IdealResidues K M J)] (χ : ZMod m → ℂ) (t : ℝ) : ℂ :=
48   ∑ positive : Bool,
49     weightedFiberCount (idealEuclideanLattice K M) (idealEuclideanLattice K J)
50       (signRegion K positive) (normWeight K M J m hM χ positive) t
51 
52 /-- Vanishing of the two actual finite norm averages yields a surface-order bound
53 for the recombined arithmetic norm count. -/
54 theorem exists_normWeightedCount_bound {M J : (Ideal (𝓞 K))⁰}
55     (hMJ : (M : Ideal (𝓞 K)) ≤ J) (m : ℕ)
56     (hM : (M : Ideal (𝓞 K)) ≤ modulusIdeal (𝓞 K) m)
57     [Fintype (IdealResidues K M J)] (χ : ZMod m → ℂ)
58     (hmean : ∀ positive : Bool, ∑ c : IdealResidues K M J, normWeight K M J m hM χ positive c = 0) :
59     ∃ B : ℝ, 0 ≤ B ∧ ∀ t : ℝ, 1 ≤ t →
60       ‖normWeightedCount K M J m hM χ t‖ ≤
61         B * (t ^ (Module.finrank ℚ K - 1) + 1) := by
62   choose B hB0 hB using exists_sign_zeroMean_bound K hMJ
63   refine ⟨∑ positive : Bool,
64     (∑ c : IdealResidues K M J, ‖normWeight K M J m hM χ positive c‖) * B positive, ?_, ?_⟩
65   · exact Finset.sum_nonneg (fun positive _ =>
66       mul_nonneg (Finset.sum_nonneg (fun _ _ => norm_nonneg _)) (hB0 positive))
67   · intro t ht
68     unfold normWeightedCount
69     calc
70       _ ≤ ∑ positive : Bool,
71           ‖weightedFiberCount (idealEuclideanLattice K M) (idealEuclideanLattice K J)
72             (signRegion K positive) (normWeight K M J m hM χ positive) t‖ := norm_sum_le _ _
73       _ ≤ ∑ positive : Bool,
74           ((∑ c : IdealResidues K M J, ‖normWeight K M J m hM χ positive c‖) * B positive) *
75             (t ^ (Module.finrank ℚ K - 1) + 1) := by
76           exact Finset.sum_le_sum (fun positive _ => hB positive _ (hmean positive) t ht)
77       _ = _ := (Finset.sum_mul _ _ _).symm
78 
79 end PaperX.NormResidueLattice

Back to source controls