Zeta.lean

1 import PaperX.Counting
2 import Mathlib.RingTheory.PowerSeries.Inverse
3 import Mathlib.RingTheory.PowerSeries.Trunc
4 
5 /-!
6 Formal (not analytic) generating series in Q[[X]]. The finite prefix is an
7 actual polynomial truncation. Denominators have constant term one. No
8 floating approximation, numerical fitting, or convergence assumption is used.
9 -/
10 set_option autoImplicit false
11 namespace PaperX.Zeta
12 open PowerSeries
13 
14 noncomputable def geometric (a : ℚ) : ℚ⟦X⟧ := mk fun n => a ^ n
15 
16 theorem geometric_mul_denominator (a : ℚ) :
17     geometric a * (1 - C a * X) = 1 := by
18   rw [mul_sub, mul_one, ← mul_assoc]
19   ext n
20   cases n with
21   | zero => simp [geometric, coeff_zero_eq_constantCoeff_apply]
22   | succ n => simp [geometric, pow_succ]
23 
24 theorem geometric_eq_inverse (a : ℚ) :
25     geometric a = (1 - C a * X)⁻¹ := by
26   apply (eq_inv_iff_mul_eq_one (by simp)).mpr
27   exact geometric_mul_denominator a
28 
29 /-- A geometric tail is represented exactly by a rational formal power series. -/
30 theorem eventually_geometric_formula (a : ℕ → ℚ) (rate : ℚ) (N : ℕ)
31     (htail : ∀ n, N ≤ n → a n = a N * rate ^ (n - N)) :
32     mk a = (trunc N (mk a) : ℚ⟦X⟧) +
33       C (a N) * X ^ N * (1 - C rate * X)⁻¹ := by
34   rw [← geometric_eq_inverse]
35   have rearrange : C (a N) * X ^ N * geometric rate =
36       C (a N) * (geometric rate * X ^ N) := by ring
37   rw [rearrange]
38   ext n
39   simp only [coeff_mk, map_add, Polynomial.coeff_coe, coeff_trunc, coeff_C_mul,
40     coeff_mul_X_pow', geometric]
41   by_cases hn : n < N
42   · simp [hn, show ¬ N ≤ n by omega]
43   · simp [hn, show N ≤ n by omega, htail n (by omega)]
44 
45 noncomputable def weightedCoeff {d : ℕ} (q : ℕ) (w : Fin d → ℕ) (m : ℕ) : ℚ :=
46   if m = 0 then 0 else (q : ℚ) ^ (∑ i, (m - w i))
47 
48 noncomputable def modelZeta {d : ℕ} (q : ℕ) (w : Fin d → ℕ) : ℚ⟦X⟧ :=
49   mk (weightedCoeff q w)
50 
51 /-- Once all coordinates are active, each new digit multiplies the count by q^d. -/
52 theorem weighted_tail {d : ℕ} (q : ℕ) (w : Fin d → ℕ) (N : ℕ)
53     (hN : 0 < N) (bound : ∀ i, w i ≤ N) (n : ℕ) (hn : N ≤ n) :
54     weightedCoeff q w n = weightedCoeff q w N * ((q : ℚ) ^ d) ^ (n-N) := by
55   have hs : (∑ i, (n - w i)) = (∑ i, (N - w i)) + d * (n-N) := by
56     calc
57       (∑ i, (n - w i)) = ∑ i, ((N - w i) + (n-N)) := by
58         apply Finset.sum_congr rfl
59         intro i _
60         have := bound i
61         omega
62       _ = _ := by simp [Finset.sum_add_distrib]
63   simp only [weightedCoeff, ite_eq_right (show n ≠ 0 by omega), ite_eq_right (by omega : N ≠ 0)]
64   rw [hs, pow_add, pow_mul]
65 
66 /-- Weighted seed zeta, with any upper bound M on the weights. This includes d=0. -/
67 theorem weighted_zeta_formula {d : ℕ} (q : ℕ) (w : Fin d → ℕ) (M : ℕ)
68     (bound : ∀ i, w i ≤ M) :
69     modelZeta q w = (trunc (M+1) (modelZeta q w) : ℚ⟦X⟧) +
70       C (weightedCoeff q w (M+1)) * X ^ (M+1) * (1 - C ((q : ℚ)^d) * X)⁻¹ := by
71   exact eventually_geometric_formula (weightedCoeff q w) ((q : ℚ)^d) (M+1)
72     (weighted_tail q w (M+1) (by omega) (fun i => (bound i).trans (by omega)))
73 
74 /-- The smooth formula T/(1-q^d T), as an identity of infinite formal series. -/
75 theorem smooth_zeta_formula (q d : ℕ) :
76     modelZeta q (fun _ : Fin d => 1) = X * (1 - C ((q : ℚ)^d) * X)⁻¹ := by
77   have h := eventually_geometric_formula
78     (weightedCoeff q (fun _ : Fin d => 1)) ((q : ℚ)^d) 1
79     (weighted_tail q (fun _ : Fin d => 1) 1 (by omega) (fun _ => le_rfl))
80   have ht : trunc 1 (modelZeta q (fun _ : Fin d => 1)) = 0 := by
81     ext n
82     by_cases hn : n = 0
83     · subst n
84       simp [modelZeta, weightedCoeff]
85     · simp [modelZeta, weightedCoeff]
86   change modelZeta q (fun _ : Fin d => 1) = _ at h
87   change trunc 1 (mk (weightedCoeff q (fun _ : Fin d => 1))) = 0 at ht
88   rw [ht] at h
89   simpa [weightedCoeff] using h
90 
91 /-- Simplify the first tail coefficient to q^(d(M+1)-sum w_i). -/
92 theorem weighted_first_tail {d : ℕ} (q : ℕ) (w : Fin d → ℕ) (M : ℕ)
93     (bound : ∀ i, w i ≤ M) :
94     weightedCoeff q w (M+1) = (q : ℚ) ^ (d*(M+1) - ∑ i, w i) := by
95   simp only [weightedCoeff, Nat.add_eq_zero_iff, one_ne_zero, and_false, ↓reduceIte]
96   congr 1
97   rw [Finset.sum_tsub_distrib Finset.univ (fun i _ => (bound i).trans (by omega))]
98   simp
99 
100 variable {O : Type*} [CommRing O] [IsDedekindDomain O]
101 variable (P : Ideal O) [P.IsPrime] (hP : P ≠ ⊥) [Finite (O ⧸ P)]
102 
103 /-- Defined using cardinalities of actual ideal-quotient tuples. -/
104 noncomputable def chartZeta {d : ℕ} (w : Fin d → ℕ) : ℚ⟦X⟧ :=
105   mk fun m => if m = 0 then 0 else (Nat.card (PaperX.Counting.WeightedChart P w m) : ℚ)
106 
107 include hP in
108 theorem chartZeta_eq_model {d : ℕ} (w : Fin d → ℕ) :
109     chartZeta P w = modelZeta (PaperX.Counting.residueCard P) w := by
110   ext n
111   simp [chartZeta, modelZeta, weightedCoeff, PaperX.Counting.weighted_chart_count P hP]
112 
113 include hP in
114 theorem actual_weighted_zeta {d : ℕ} (w : Fin d → ℕ) (M : ℕ)
115     (bound : ∀ i, w i ≤ M) :
116     chartZeta P w = (trunc (M+1) (chartZeta P w) : ℚ⟦X⟧) +
117       C ((PaperX.Counting.residueCard P : ℚ) ^ (d*(M+1) - ∑ i, w i)) *
118       X ^ (M+1) * (1 - C ((PaperX.Counting.residueCard P : ℚ)^d) * X)⁻¹ := by
119   rw [chartZeta_eq_model P hP]
120   rw [← weighted_first_tail _ w M bound]
121   exact weighted_zeta_formula _ w M bound
122 
123 include hP in
124 theorem actual_smooth_zeta (d : ℕ) :
125     chartZeta P (fun _ : Fin d => 1) =
126       X * (1 - C ((PaperX.Counting.residueCard P : ℚ)^d) * X)⁻¹ := by
127   rw [chartZeta_eq_model P hP]
128   exact smooth_zeta_formula _ d
129 
130 end PaperX.Zeta

Back to source controls