ResidueLatticeNormCounts.lean

1 import PaperX.ResidueLatticeIdealWeights
2 import PaperX.ResidueLatticeIdealPoints
3 
4 /-! Actual ideal-residue counts in the norm threshold, with power-saving error. -/
5 set_option autoImplicit false
6 noncomputable section
7 open Ideal Module
8 open scoped nonZeroDivisors Real Classical Pointwise BigOperators
9 open NumberField
10 namespace PaperX.ResidueLattice
11 open PaperX.IdealClassQuantitative
12 variable (K : Type*) [Field K] [NumberField K]
13   (M J : (Ideal (𝓞 K))⁰)
14 
15 /-- Actual points of the ideal lattice in one residue with the prescribed norm threshold. -/
16 def idealNormFiberCount (c : IdealResidues K M J) (y : ℝ) : ℕ :=
17   Nat.card {x : idealEuclideanLattice K J //
18     (Submodule.Quotient.mk x : IdealResidues K M J) = c ∧ x.1 ∈ coneRegion K y}
19 
20 /-- Dilation changes the actual cone norm threshold by the number-field degree. -/
21 theorem idealFiberCount_eq_normFiberCount (c : IdealResidues K M J) {t : ℝ} (ht : 0 < t) :
22     idealFiberCount K M J c t = idealNormFiberCount K M J c (t ^ Module.finrank ℚ K) := by
23   unfold idealFiberCount fiberCount idealNormFiberCount
24   rw [smul_coneRegion_one K ht]
25 
26 /-- The norm-threshold count is an actual congruence count of algebraic integers of J. -/
27 theorem idealNormFiberCount_eq_integer_count (a : (J : Ideal (𝓞 K))) (y : ℝ) :
28     idealNormFiberCount K M J (Submodule.Quotient.mk (idealPointEquiv K J a)) y =
29       Nat.card {x : (J : Ideal (𝓞 K)) // x.1 - a.1 ∈ (M : Ideal (𝓞 K)) ∧
30         integerPoint K x.1 ∈ coneRegion K y} := by
31   unfold idealNormFiberCount
32   exact Nat.card_congr ((idealPointEquiv K J).subtypeEquiv (fun x => by
33     simp only [idealPoint_residue_eq_iff]
34     rfl)).symm
35 
36 /-- All actual additive residues have the same main coefficient and a power-saving norm error. -/
37 theorem exists_idealNormFiber_bound (h : (M : Ideal (𝓞 K)) ≤ J) :
38     ∃ B : ℝ, 0 ≤ B ∧ ∀ (c : IdealResidues K M J) (y : ℝ), 1 ≤ y →
39       |(idealNormFiberCount K M J c y : ℝ) -
40         y * (latticeDensity K J / Nat.card (IdealResidues K M J))| ≤
41         B * (y ^ countExponent K + 1) := by
42   obtain ⟨B, hB, hb⟩ := exists_idealFiber_bound K h
43   refine ⟨B, hB, fun c y hy => ?_⟩
44   have hy0 : 0 < y := lt_of_lt_of_le zero_lt_one hy
45   have hd : Module.finrank ℚ K ≠ 0 := (Module.finrank_pos (R := ℚ) (M := K)).ne'
46   have ht : 1 ≤ y ^ (Module.finrank ℚ K : ℝ)⁻¹ :=
47     Real.one_le_rpow hy (by positivity)
48   have H := hb c (y ^ (Module.finrank ℚ K : ℝ)⁻¹) ht
49   rw [idealFiberCount_eq_normFiberCount K M J c (Real.rpow_pos_of_pos hy0 _),
50     Real.rpow_inv_natCast_pow hy0.le hd, root_boundary_power K y hy0.le] at H
51   exact H
52 
53 variable [Fintype (IdealResidues K M J)]
54 
55 /-- Arbitrary complex residue weights have the actual finite average as leading coefficient. -/
56 theorem exists_idealNormWeighted_bound (h : (M : Ideal (𝓞 K)) ≤ J) :
57     WeightedEstimate (idealNormFiberCount K M J)
58       (fun y => y * (latticeDensity K J / Nat.card (IdealResidues K M J)))
59       (fun y => y ^ countExponent K + 1) :=
60   weightedEstimate_of_uniform_bound _ _ _ (exists_idealNormFiber_bound K M J h)
61 
62 /-- Zero mean gives genuine power-saving cancellation for actual norm-truncated residue counts. -/
63 theorem exists_zeroMean_idealNormWeighted_bound (h : (M : Ideal (𝓞 K)) ≤ J) :
64     ZeroMeanEstimate (idealNormFiberCount K M J) (fun y => y ^ countExponent K + 1) :=
65   (exists_idealNormWeighted_bound K M J h).zeroMean
66 
67 end PaperX.ResidueLattice

Back to source controls