ResidueLatticeIdealWeights.lean

1 import PaperX.ResidueLatticeWeights
2 
3 /-! Weighted residue counts for actual nonzero integral ideals, with no geometric hypotheses. -/
4 set_option autoImplicit false
5 noncomputable section
6 open Ideal Module
7 open scoped nonZeroDivisors Real Classical Pointwise BigOperators
8 open NumberField
9 namespace PaperX.ResidueLattice
10 open PaperX.IdealClassQuantitative
11 variable (K : Type*) [Field K] [NumberField K]
12   (M J : (Ideal (𝓞 K))⁰) [Fintype (IdealResidues K M J)]
13 
14 /-- Weight each actual ideal-lattice point by its additive residue class. -/
15 def idealWeightedCount (w : IdealResidues K M J → ℂ) (t : ℝ) : ℂ :=
16   ∑ c : IdealResidues K M J, w c * (idealFiberCount K M J c t : ℂ)
17 
18 /-- The residue-weighted count is exactly the finite sum over actual cone lattice points. -/
19 theorem idealWeightedCount_eq_pointSum (w : IdealResidues K M J → ℂ) (t : ℝ) :
20     idealWeightedCount K M J w t = latticePointSum (idealEuclideanLattice K M)
21       (idealEuclideanLattice K J) (coneRegion K 1) w t :=
22   weightedFiberCount_eq_pointSum _ _ (coneRegion_one_bounded K) w t
23 
24 /-- Uniform arithmetic residue weights have their exact finite average as main coefficient. -/
25 theorem exists_idealWeighted_bound (h : (M : Ideal (𝓞 K)) ≤ J) :
26     WeightedEstimate (idealFiberCount K M J)
27       (fun t => t ^ Module.finrank ℚ K * (latticeDensity K J / Nat.card (IdealResidues K M J)))
28       (fun t => t ^ (Module.finrank ℚ K - 1) + 1) :=
29   weightedEstimate_of_uniform_bound _ _ _ (exists_idealFiber_bound K h)
30 
31 /-- A zero finite average gives surface-order cancellation in an actual ideal lattice. -/
32 theorem exists_zeroMean_idealWeighted_bound (h : (M : Ideal (𝓞 K)) ≤ J) :
33     ZeroMeanEstimate (idealFiberCount K M J) (fun t => t ^ (Module.finrank ℚ K - 1) + 1) :=
34   (exists_idealWeighted_bound K M J h).zeroMean
35 
36 end PaperX.ResidueLattice

Back to source controls