SingularZeta.lean

1 import PaperX.Singular
2 import PaperX.Zeta
3 
4 /-! Rational singular seed zeta in Q[[X]], proved at all coefficient indices. -/
5 set_option autoImplicit false
6 namespace PaperX.SingularZeta
7 open PowerSeries
8 
9 noncomputable def rootCoeff (q e m : ℕ) : ℚ :=
10   if m = 0 then 0 else (q : ℚ) ^ (m - (m ⌈/⌉ e))
11 
12 noncomputable def rootZeta (q e : ℕ) : ℚ⟦X⟧ := mk (rootCoeff q e)
13 
14 theorem ceil_add_period (n e : ℕ) (he : 0 < e) :
15     (n+e) ⌈/⌉ e = (n ⌈/⌉ e)+1 := by
16   simp only [Nat.ceilDiv_eq_add_pred_div]
17   have h : n + e + e - 1 = (n+e-1) + e := by omega
18   rw [h, Nat.add_div_right _ he]
19 
20 /-- After the initial e coefficients, the coefficients recur with ratio q^(e-1). -/
21 theorem rootCoeff_period (q e n : ℕ) (he : 0 < e) (hn : 0 < n) :
22     rootCoeff q e (n+e) = rootCoeff q e n * (q : ℚ)^(e-1) := by
23   have hc := PaperX.Singular.ceil_threshold_le n e he
24   have ht : (n+e) - ((n ⌈/⌉ e)+1) = (n - (n ⌈/⌉ e)) + (e-1) := by omega
25   simp only [rootCoeff, ite_eq_right (by omega : n+e ≠ 0), ite_eq_right (by omega : n ≠ 0)]
26   rw [ceil_add_period n e he, ht, pow_add]
27 
28 theorem initial_coefficient (q e n : ℕ) (he : 0 < e) (hn : 0 < n) (hne : n ≤ e) :
29     rootCoeff q e n = (q : ℚ)^(n-1) := by
30   have hupper : n ⌈/⌉ e ≤ 1 := (ceilDiv_le_iff_le_mul he).mpr (by simpa using hne)
31   have hlower : 1 ≤ n ⌈/⌉ e := by
32     have h := le_smul_ceilDiv (b := n) he
33     simp only [smul_eq_mul] at h
34     by_contra H
35     have hz : n ⌈/⌉ e = 0 := by omega
36     simp [hz] at h
37     omega
38   have hc : n ⌈/⌉ e = 1 := by omega
39   simp [rootCoeff, hc, show n ≠ 0 by omega]
40 
41 /-- The denominator removes the infinite tail, leaving an actual polynomial. -/
42 theorem singular_denominator_identity (q e : ℕ) (he : 0 < e) :
43     rootZeta q e * (1 - C ((q : ℚ)^(e-1)) * X^e) =
44       (trunc (e+1) (rootZeta q e) : ℚ⟦X⟧) := by
45   rw [mul_sub, mul_one, ← mul_assoc]
46   ext n
47   simp only [map_sub, Polynomial.coeff_coe, coeff_trunc, coeff_mul_X_pow', coeff_mul_C,
48     rootZeta, coeff_mk]
49   by_cases hn : n < e
50   · simp [show ¬ e ≤ n by omega, show n < e+1 by omega]
51   · by_cases hne : n = e
52     · subst n
53       simp [rootCoeff]
54     · have hp : 0 < n-e := by omega
55       have h := rootCoeff_period q e (n-e) he hp
56       rw [Nat.sub_add_cancel (by omega : e ≤ n)] at h
57       simp [show e ≤ n by omega, show ¬n < e+1 by omega, h]
58 
59 /-- The rational zeta function. Its numerator is supported in degrees 1,...,e. -/
60 theorem singular_zeta_formula (q e : ℕ) (he : 0 < e) :
61     rootZeta q e = (trunc (e+1) (rootZeta q e) : ℚ⟦X⟧) *
62       (1 - C ((q : ℚ)^(e-1)) * X^e)⁻¹ := by
63   apply (eq_mul_inv_iff_mul_eq (by simp [Nat.ne_of_gt he])).mpr
64   exact singular_denominator_identity q e he
65 
66 /-- This identifies every numerator coefficient with the manuscript's finite sum. -/
67 theorem numerator_coefficients (q e n : ℕ) (he : 0 < e) :
68     (trunc (e+1) (rootZeta q e)).coeff n =
69       if 0 < n ∧ n ≤ e then (q : ℚ)^(n-1) else 0 := by
70   rw [coeff_trunc]
71   simp only [rootZeta, coeff_mk]
72   by_cases hn : 0 < n ∧ n ≤ e
73   · simp [hn, show n < e+1 by omega, initial_coefficient q e n he hn.1 hn.2]
74   · by_cases hz : n = 0
75     · subst n
76       simp [rootCoeff]
77     · simp [hn, show ¬ n < e+1 by omega]
78 
79 variable {O : Type*} [CommRing O] [IsDomain O] [IsDiscreteValuationRing O]
80 variable [Finite (O ⧸ IsLocalRing.maximalIdeal O)]
81 
82 /-- Generating series defined from cardinalities of actual polynomial roots. -/
83 noncomputable def actualRootZeta (e : ℕ) : ℚ⟦X⟧ :=
84   mk fun m => if m = 0 then 0 else (Nat.card (PaperX.Singular.Roots (O := O) m e) : ℚ)
85 
86 theorem actualRootZeta_eq_model (e : ℕ) (he : 0 < e) :
87     actualRootZeta (O := O) e = rootZeta (Nat.card (O ⧸ IsLocalRing.maximalIdeal O)) e := by
88   ext n
89   simp [actualRootZeta, rootZeta, rootCoeff, PaperX.Singular.singular_root_count n e he]
90 
91 theorem actual_singular_zeta (e : ℕ) (he : 0 < e) :
92     actualRootZeta (O := O) e = (trunc (e+1) (actualRootZeta (O := O) e) : ℚ⟦X⟧) *
93       (1 - C ((Nat.card (O ⧸ IsLocalRing.maximalIdeal O) : ℚ)^(e-1)) * X^e)⁻¹ := by
94   rw [actualRootZeta_eq_model e he]
95   exact singular_zeta_formula _ e he
96 
97 end PaperX.SingularZeta

Back to source controls