IdealClassQuantitativeTheorem.lean

1 import PaperX.IdealClassQuantitativeGeometry
2 import PaperX.LatticeCountingFull
3 
4 /-!
5 # Quantitative counting in every ordinary ideal class of a number field
6 
7 The boundary atlas, lattice estimate, and arithmetic attachment are all
8 constructed for the actual objects. No quantitative counting assumption remains.
9 -/
10 set_option autoImplicit false
11 noncomputable section
12 
13 open Ideal MeasureTheory Module Filter Asymptotics
14 open scoped nonZeroDivisors Real Classical Pointwise
15 open NumberField NumberField.InfinitePlace NumberField.mixedEmbedding
16 open NumberField.mixedEmbedding.euclidean NumberField.mixedEmbedding.fundamentalCone
17 open NumberField.Units
18 
19 namespace PaperX.IdealClassQuantitative
20 
21 variable (K : Type*) [Field K] [NumberField K]
22 
23 /-- A surface-order estimate for the actual ideal lattice and unit fundamental cone. -/
24 theorem exists_ideal_lattice_bound (J : (Ideal (𝓞 K))⁰) :
25     ∃ B : ℝ, 0 ≤ B ∧ ∀ t : ℝ, 1 ≤ t →
26       |(Nat.card (t • coneRegion K 1 ∩ idealEuclideanLattice K J :
27         Set (euclidean.mixedSpace K)) : ℝ) -
28         latticeDensity K J * t ^ Module.finrank ℚ K| ≤
29           B * (t ^ (Module.finrank ℚ K - 1) + 1) := by
30   let b := Module.Free.chooseBasis ℤ (idealEuclideanLattice K J)
31   obtain ⟨A⟩ := ideal_cone_boundaryAtlas K J b
32   obtain ⟨B, hB0, hB⟩ := PaperX.LatticeCountingTransport.exists_lattice_discrepancy_bound
33     (idealEuclideanLattice K J) b (coneRegion_one_measurable K) (coneRegion_one_bounded K) A
34   refine ⟨B, hB0, fun t ht => ?_⟩
35   have h := hB 0 t ht
36   simpa only [zero_add, Set.image_smul, ideal_basis_card K b, latticeDensity, mul_comm] using h
37 
38 /-- Every ordinary ideal class has the quantitative asymptotic with its explicit common residue. -/
39 theorem classCount_isBigO (C : ClassGroup (𝓞 K)) :
40     (fun s : ℝ => (classCount K C s : ℝ) - classResidue K * s) =O[atTop]
41       (fun s : ℝ => s ^ countExponent K) := by
42   obtain ⟨J, hJ⟩ := ClassGroup.mk0_surjective C⁻¹
43   obtain ⟨B, hB0, hB⟩ := exists_ideal_lattice_bound K J
44   exact class_isBigO_of_dilation_bound K hJ hB0 hB
45 
46 /-- The same result as a bound valid at every threshold at least one. -/
47 theorem exists_classCount_bound (C : ClassGroup (𝓞 K)) :
48     ∃ M : ℝ, 0 ≤ M ∧ ∀ s : ℝ, 1 ≤ s →
49       |(classCount K C s : ℝ) - classResidue K * s| ≤ M * s ^ countExponent K := by
50   obtain ⟨J, hJ⟩ := ClassGroup.mk0_surjective C⁻¹
51   obtain ⟨B, hB0, hB⟩ := exists_ideal_lattice_bound K J
52   refine ⟨B / torsionOrder K *
53     ((absNorm (J : Ideal (𝓞 K)) : ℝ) ^ countExponent K + 1), ?_, ?_⟩
54   · exact mul_nonneg (div_nonneg hB0 (torsionOrder_cast_pos K).le)
55       (add_nonneg (Real.rpow_nonneg (Nat.cast_nonneg _) _) zero_le_one)
56   · exact class_bound_of_norm_bound K hJ hB0 (norm_bound_of_dilation_bound K J B hB)
57 
58 end PaperX.IdealClassQuantitative

Back to source controls