PrimeDegreeSummability.lean

1 import Mathlib.NumberTheory.NumberField.Basic
2 import Mathlib.NumberTheory.NumberField.DirichletDensity
3 import Mathlib.RingTheory.RamificationInertia.Basic
4 import Mathlib.RingTheory.Ideal.Int
5 import Mathlib.Analysis.PSeries
6 
7 /-!
8 # Summability of primes of higher absolute residue degree
9 
10 The prime ideals below are actual height-one prime ideals of the ring of integers.
11 The finite fibre bound is deduced from the ramification-inertia identity.
12 -/
13 
14 noncomputable section
15 set_option autoImplicit false
16 set_option maxHeartbeats 1000000
17 
18 namespace PaperX.PrimeDegreeSummability
19 
20 open NumberField IsDedekindDomain
21 
22 variable (K : Type*) [Field K] [NumberField K]
23 
24 abbrev RationalPrime := {p : ℕ // p.Prime}
25 
26 def primeIdeal (p : RationalPrime) : Ideal ℤ := Ideal.span {(p.1 : ℤ)}
27 
28 instance primeIdeal_isPrime (p : RationalPrime) : (primeIdeal p).IsPrime :=
29   (Ideal.span_singleton_prime (by exact_mod_cast p.2.ne_zero)).mpr
30     (Nat.prime_iff_prime_int.mp p.2)
31 
32 abbrev Above (p : RationalPrime) := (primeIdeal p).primesOver (𝓞 K)
33 
34 instance aboveFintype (p : RationalPrime) : Fintype (Above K p) :=
35   (Algebra.QuasiFinite.finite_primesOver (S := 𝓞 K) (primeIdeal p)).fintype
36 
37 theorem card_above_le (p : RationalPrime) :
38     Fintype.card (Above K p) ≤ Module.finrank ℚ K := by
39   rw [← RingOfIntegers.rank, ← Ideal.sum_ramification_inertia_eq_finrank (primeIdeal p) (𝓞 K),
40     Fintype.card_eq_sum_ones]
41   apply Finset.sum_le_sum
42   intro q _
43   have : q.1.IsPrime := q.2.1
44   exact Right.one_le_mul (q.1.ramificationIdx_pos ℤ) (q.1.inertiaDeg_pos ℤ)
45 
46 def rationalPrimeBelow (q : HeightOneSpectrum (𝓞 K)) : RationalPrime :=
47   ⟨(q.asIdeal.under ℤ).absNorm, Nat.absNorm_under_prime q.asIdeal⟩
48 
49 def primeOverBelow (q : HeightOneSpectrum (𝓞 K)) : Above K (rationalPrimeBelow K q) :=
50   ⟨q.asIdeal, q.isPrime, Int.liesOver_span_absNorm q.asIdeal⟩
51 
52 theorem below_pow_degree (q : HeightOneSpectrum (𝓞 K)) :
53     (rationalPrimeBelow K q).1 ^ q.asIdeal.inertiaDeg ℤ = q.asIdeal.absNorm := by
54   have : q.asIdeal.LiesOver (Ideal.span {((rationalPrimeBelow K q).1 : ℤ)}) :=
55     Int.liesOver_span_absNorm q.asIdeal
56   exact Ideal.pow_inertiaDeg _ _
57 
58 
59 /-- The uniform majorant is summable on all prime ideals, indexed by the prime below. -/
60 theorem summable_prime_majorant :
61     Summable (fun z : (p : RationalPrime) × Above K p => (z.1.1 : ℝ)⁻¹ ^ 2) := by
62   apply (summable_sigma_of_nonneg (fun _ => by positivity)).mpr
63   constructor
64   · intro p
65     exact Summable.of_finite
66   · have hs : Summable (fun p : RationalPrime => (p.1 : ℝ)⁻¹ ^ 2) := by
67       simpa only [inv_pow, Function.comp_def] using
68         (Real.summable_nat_pow_inv.mpr (by norm_num : 1 < 2)).subtype Nat.Prime
69     apply Summable.of_nonneg_of_le (fun _ => by positivity) _
70       (hs.mul_left (Module.finrank ℚ K : ℝ))
71     intro p
72     rw [tsum_fintype]
73     simp only [Finset.sum_const, Finset.card_univ, nsmul_eq_mul]
74     exact mul_le_mul_of_nonneg_right (by exact_mod_cast card_above_le K p) (by positivity)
75 
76 /-- The canonical prime-under map together with the prime itself loses no information. -/
77 theorem prime_encoding_injective : Function.Injective
78     (fun q : HeightOneSpectrum (𝓞 K) =>
79       (⟨rationalPrimeBelow K q, primeOverBelow K q⟩ : (p : RationalPrime) × Above K p)) := by
80   intro q r h
81   have h' := congrArg (fun z : (p : RationalPrime) × Above K p => z.2.1) h
82   exact HeightOneSpectrum.ext h'
83 
84 /-- Reciprocal squared rational primes form a summable majorant on actual prime ideals. -/
85 theorem summable_below_sq :
86     Summable (fun q : HeightOneSpectrum (𝓞 K) => ((rationalPrimeBelow K q).1 : ℝ)⁻¹ ^ 2) := by
87   have h := (summable_prime_majorant K).comp_injective (prime_encoding_injective K)
88   exact h
89 
90 /-- The norm formula gives the reciprocal-square estimate at each higher-degree prime. -/
91 theorem reciprocal_le_below_sq (q : HeightOneSpectrum (𝓞 K))
92     (hq : 2 ≤ q.asIdeal.inertiaDeg ℤ) :
93     (q.asIdeal.absNorm : ℝ)⁻¹ ≤ ((rationalPrimeBelow K q).1 : ℝ)⁻¹ ^ 2 := by
94   rw [← below_pow_degree K q, Nat.cast_pow, inv_pow]
95   have hp : 0 < ((rationalPrimeBelow K q).1 : ℝ) :=
96     by exact_mod_cast (rationalPrimeBelow K q).2.pos
97   apply inv_anti₀ (pow_pos hp 2)
98   exact pow_le_pow_right₀ (by exact_mod_cast (rationalPrimeBelow K q).2.one_lt.le) hq
99 
100 /-- Prime ideals of absolute residue degree at least two have summable reciprocal norms. -/
101 theorem summable_high_degree :
102     Summable (fun q : {q : HeightOneSpectrum (𝓞 K) // 2 ≤ q.asIdeal.inertiaDeg ℤ} =>
103       (q.1.asIdeal.absNorm : ℝ)⁻¹) := by
104   apply Summable.of_nonneg_of_le (fun _ => by positivity) _
105     ((summable_below_sq K).subtype (fun q => 2 ≤ q.asIdeal.inertiaDeg ℤ))
106   exact fun q => reciprocal_le_below_sq K q.1 q.2
107 
108 /-- Explicit global bound for the rational-prime majorant. -/
109 theorem tsum_prime_majorant_le :
110     (∑' z : (p : RationalPrime) × Above K p, (z.1.1 : ℝ)⁻¹ ^ 2) ≤
111       (Module.finrank ℚ K : ℝ) * ∑' p : RationalPrime, (p.1 : ℝ)⁻¹ ^ 2 := by
112   have hs : Summable (fun p : RationalPrime => (p.1 : ℝ)⁻¹ ^ 2) := by
113     simpa only [inv_pow, Function.comp_def] using
114       (Real.summable_nat_pow_inv.mpr (by norm_num : 1 < 2)).subtype Nat.Prime
115   rw [(summable_prime_majorant K).tsum_sigma, ← tsum_mul_left]
116   apply Summable.tsum_le_tsum _ (summable_prime_majorant K).sigma
117     (hs.mul_left (Module.finrank ℚ K : ℝ))
118   intro p
119   rw [tsum_fintype]
120   simp only [Finset.sum_const, Finset.card_univ, nsmul_eq_mul]
121   exact mul_le_mul_of_nonneg_right (by exact_mod_cast card_above_le K p) (by positivity)
122 
123 /-- The higher-degree reciprocal sum is bounded by degree times the prime square series. -/
124 theorem tsum_high_degree_le :
125     (∑' q : {q : HeightOneSpectrum (𝓞 K) // 2 ≤ q.asIdeal.inertiaDeg ℤ},
126       (q.1.asIdeal.absNorm : ℝ)⁻¹) ≤
127       (Module.finrank ℚ K : ℝ) * ∑' p : RationalPrime, (p.1 : ℝ)⁻¹ ^ 2 := by
128   let e (q : {q : HeightOneSpectrum (𝓞 K) // 2 ≤ q.asIdeal.inertiaDeg ℤ}) :
129       (p : RationalPrime) × Above K p := ⟨rationalPrimeBelow K q.1, primeOverBelow K q.1⟩
130   have he : Function.Injective e := (prime_encoding_injective K).comp Subtype.val_injective
131   have hsum := (summable_prime_majorant K).comp_injective he
132   have hbound := tsum_comp_le_tsum_of_inj (summable_prime_majorant K) (fun _ => by positivity) he
133   apply le_trans _ (hbound.trans (tsum_prime_majorant_le K))
134   exact Summable.tsum_le_tsum (fun q => reciprocal_le_below_sq K q.1 q.2)
135     (summable_high_degree K) hsum
136 
137 /-- Divergence forces an absolute degree-one prime outside each finite exclusion. -/
138 theorem exists_degree_one_outside_finite
139     (S : Set (HeightOneSpectrum (𝓞 K)))
140     (hS : ¬ Summable (fun q : S => (q.1.asIdeal.absNorm : ℝ)⁻¹))
141     (bad : Set (HeightOneSpectrum (𝓞 K))) (hbad : bad.Finite) :
142     ∃ q : HeightOneSpectrum (𝓞 K), q ∈ S ∧ q ∉ bad ∧ q.asIdeal.inertiaDeg ℤ = 1 := by
143   classical
144   by_contra h
145   have hdegree (q : S) (hq : q.1 ∉ bad) : 2 ≤ q.1.asIdeal.inertiaDeg ℤ := by
146     have hpos := q.1.asIdeal.inertiaDeg_pos ℤ
147     have hne : q.1.asIdeal.inertiaDeg ℤ ≠ 1 := fun he => h ⟨q.1, q.2, hq, he⟩
148     omega
149   let B : Set S := Subtype.val ⁻¹' bad
150   have hB : B.Finite := hbad.preimage Subtype.val_injective.injOn
151   have hs : Summable (fun q : ↥(Bᶜ) => (q.1.1.asIdeal.absNorm : ℝ)⁻¹) := by
152     let e : ↥(Bᶜ) → {q : HeightOneSpectrum (𝓞 K) // 2 ≤ q.asIdeal.inertiaDeg ℤ} :=
153       fun q => ⟨q.1.1, hdegree q.1 q.2⟩
154     have he : Function.Injective e := by
155       intro x y hxy
156       have hh := congrArg
157         (fun z : {q : HeightOneSpectrum (𝓞 K) // 2 ≤ q.asIdeal.inertiaDeg ℤ} => z.1) hxy
158       exact Subtype.ext (Subtype.ext hh)
159     have hs := (summable_high_degree K).comp_injective he
160     exact hs
161   exact hS (hB.summable_compl_iff.mp hs)
162 
163 /-- Infinitely many degree-one primes remain after every finite exclusion. -/
164 theorem infinite_degree_one_outside_finite
165     (S : Set (HeightOneSpectrum (𝓞 K)))
166     (hS : ¬ Summable (fun q : S => (q.1.asIdeal.absNorm : ℝ)⁻¹))
167     (bad : Set (HeightOneSpectrum (𝓞 K))) (hbad : bad.Finite) :
168     {q | q ∈ S ∧ q ∉ bad ∧ q.asIdeal.inertiaDeg ℤ = 1}.Infinite := by
169   intro hf
170   obtain ⟨q, hq, hn, hd⟩ := exists_degree_one_outside_finite K S hS
171     (bad ∪ {q | q ∈ S ∧ q ∉ bad ∧ q.asIdeal.inertiaDeg ℤ = 1}) (hbad.union hf)
172   have hb : q ∉ bad := fun hb => hn (Or.inl hb)
173   exact hn (Or.inr ⟨hq, hb, hd⟩)
174 
175 end PaperX.PrimeDegreeSummability

Back to source controls