NormResidueUnitCounting.lean

1 import PaperX.NormResidueWeightedCounting
2 import PaperX.IdealResidueUnitActionMean
3 
4 /-! Actual norm-weighted residue counts with finite mean derived from a unit witness.
5 Both signed averages are proved, rather than included as counting hypotheses. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperX.NormResidueLattice
9 open Ideal NumberField
10 open PaperX.ResidueLattice PaperX.NormResidue PaperX.IdealResidueUnitAction
11 open scoped nonZeroDivisors BigOperators
12 
13 variable (K : Type*) [Field K] [NumberField K]
14 
15 /-- The unit permutation proves the zero mean for each of the two actual sign weights. -/
16 theorem normWeight_sum_eq_zero (M J : (Ideal (𝓞 K))⁰) (m : ℕ)
17     (hprod : modulusIdeal (𝓞 K) m * (J : Ideal (𝓞 K)) ≤ M)
18     (hM : (M : Ideal (𝓞 K)) ≤ modulusIdeal (𝓞 K) m)
19     [Fintype (IdealResidues K M J)] (χ : ZMod m →* ℂ)
20     (u : (𝓞 K ⧸ modulusIdeal (𝓞 K) m)ˣ)
21     (hu : χ (integerQuotientNorm K m (u : 𝓞 K ⧸ modulusIdeal (𝓞 K) m)) ≠ 1)
22     (positive : Bool) :
23     ∑ c : IdealResidues K M J, normWeight K M J m hM χ positive c = 0 := by
24   cases positive with
25   | false =>
26     simpa [normWeight] using
27       sum_mul_residueNorm_eq_zero K M J m hprod hM χ u hu (-1)
28   | true =>
29     simpa [normWeight] using
30       sum_mul_residueNorm_eq_zero K M J m hprod hM χ u hu 1
31 
32 /-- The arithmetic unit witness supplies the cancellation needed by actual signed-region counting. -/
33 theorem exists_normWeightedCount_bound_of_unit {M J : (Ideal (𝓞 K))⁰}
34     (hMJ : (M : Ideal (𝓞 K)) ≤ J) (m : ℕ)
35     (hM : (M : Ideal (𝓞 K)) ≤ modulusIdeal (𝓞 K) m)
36     (hprod : modulusIdeal (𝓞 K) m * (J : Ideal (𝓞 K)) ≤ M)
37     [Fintype (IdealResidues K M J)] (χ : ZMod m →* ℂ)
38     (u : (𝓞 K ⧸ modulusIdeal (𝓞 K) m)ˣ)
39     (hu : χ (integerQuotientNorm K m (u : 𝓞 K ⧸ modulusIdeal (𝓞 K) m)) ≠ 1) :
40     ∃ B : ℝ, 0 ≤ B ∧ ∀ t : ℝ, 1 ≤ t →
41       ‖normWeightedCount K M J m hM χ t‖ ≤
42         B * (t ^ (Module.finrank ℚ K - 1) + 1) :=
43   exists_normWeightedCount_bound K hMJ m hM χ
44     (normWeight_sum_eq_zero K M J m hprod hM χ u hu)
45 
46 /-- The actual count for the canonical ideal modulus mJ, with its finite enumeration derived. -/
47 def modulusNormWeightedCount (J : (Ideal (𝓞 K))⁰) (m : ℕ) (hm : m ≠ 0)
48     (χ : ZMod m → ℂ) (t : ℝ) : ℂ :=
49   letI := Fintype.ofFinite (IdealResidues K (modulusTimesIdeal K J m hm) J)
50   normWeightedCount K (modulusTimesIdeal K J m hm) J m
51     (modulusTimesIdeal_le_modulus K J m hm) χ t
52 
53 /-- Surface-order cancellation for actual J/mJ weights, with no supplied finite mean
54 or coprimality condition on J. The residue-unit witness remains explicit. -/
55 theorem exists_modulusNormWeightedCount_bound (J : (Ideal (𝓞 K))⁰)
56     (m : ℕ) (hm : m ≠ 0) (χ : ZMod m →* ℂ)
57     (u : (𝓞 K ⧸ modulusIdeal (𝓞 K) m)ˣ)
58     (hu : χ (integerQuotientNorm K m (u : 𝓞 K ⧸ modulusIdeal (𝓞 K) m)) ≠ 1) :
59     ∃ B : ℝ, 0 ≤ B ∧ ∀ t : ℝ, 1 ≤ t →
60       ‖modulusNormWeightedCount K J m hm χ t‖ ≤
61         B * (t ^ (Module.finrank ℚ K - 1) + 1) := by
62   let := Fintype.ofFinite (IdealResidues K (modulusTimesIdeal K J m hm) J)
63   exact exists_normWeightedCount_bound_of_unit K (modulusTimesIdeal_le K J m hm) m
64     (modulusTimesIdeal_le_modulus K J m hm) le_rfl χ u hu
65 
66 end PaperX.NormResidueLattice

Back to source controls