ParameterThetaCompletion.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 
6 import KomorebiPaperIV.AlgebraicCompletion
7 import KomorebiPaperIV.ThetaCore
8 import Mathlib.Algebra.Polynomial.Eval.Defs
9 import Mathlib.Algebra.Polynomial.Degree.Operations
10 
11 /-!
12 # Parameter and theta completion for Paper IV
13 
14 This file supplies manuscript-facing arbitrary-parameter versions of the
15 normalized-residue reciprocal and Appell constructions.  It also packages the
16 theta coefficients as honest polynomials in the parameter and proves the
17 formal Newton recurrence.
18 -/
19 
20 namespace Komorebi.PaperIV
21 
22 open scoped PowerSeries
23 
24 noncomputable section
25 
26 section Naturality
27 
28 variable {R S : Type*} [CommRing R] [Algebra ℚ R]
29   [CommRing S] [Algebra ℚ S]
30 
31 /-- A normalized residue section over an arbitrary rational algebra.  This is
32 the rational-coefficient form of `normalizedResidueSection`. -/
33 def normalizedResidueSectionAlg (N j : ℕ) : R⟦X⟧ :=
34   PowerSeries.mk fun n =>
35     algebraMap ℚ R ((j.factorial : ℚ) / ((N * n + j).factorial : ℚ))
36 
37 @[simp]
38 theorem coeff_normalizedResidueSectionAlg (N j n : ℕ) :
39     PowerSeries.coeff n (normalizedResidueSectionAlg (R := R) N j) =
40       algebraMap ℚ R
41         ((j.factorial : ℚ) / ((N * n + j).factorial : ℚ)) := by
42   simp [normalizedResidueSectionAlg]
43 
44 @[simp]
45 theorem constantCoeff_normalizedResidueSectionAlg (N j : ℕ) :
46     (normalizedResidueSectionAlg (R := R) N j).constantCoeff = 1 := by
47   rw [← PowerSeries.coeff_zero_eq_constantCoeff]
48   rw [coeff_normalizedResidueSectionAlg]
49   simp only [Nat.mul_zero, zero_add]
50   have hj : (j.factorial : ℚ) ≠ 0 := by positivity
51   rw [div_self hj, map_one]
52 
53 theorem normalizedResidueSectionAlg_eq_normalizedResidueSection
54     {K : Type*} [Field K] [CharZero K] (N j : ℕ) :
55     normalizedResidueSectionAlg (R := K) N j =
56       normalizedResidueSection (K := K) N j := by
57   ext n
58   rw [coeff_normalizedResidueSectionAlg, coeff_normalizedResidueSection]
59   simp
60 
61 theorem map_normalizedResidueSectionAlg (φ : R →ₐ[ℚ] S) (N j : ℕ) :
62     PowerSeries.map (φ : R →+* S) (normalizedResidueSectionAlg (R := R) N j) =
63       normalizedResidueSectionAlg (R := S) N j := by
64   ext n
65   simp
66 
67 /-- Formal negative logarithm of the normalized residue section. -/
68 def normalizedResidueNegativeLog (N j : ℕ) : R⟦X⟧ :=
69   -PowerSeries.logOf (normalizedResidueSectionAlg (R := R) N j)
70 
71 @[simp]
72 theorem constantCoeff_normalizedResidueNegativeLog (N j : ℕ) :
73     (normalizedResidueNegativeLog (R := R) N j).constantCoeff = 0 := by
74   simp [normalizedResidueNegativeLog,
75     PowerSeries.constantCoeff_logOf,
76     constantCoeff_normalizedResidueSectionAlg]
77 
78 /-- `logOf` commutes with morphisms of rational algebras on unit-constant
79 series. -/
80 theorem map_logOf_of_constantCoeff_one (φ : R →ₐ[ℚ] S) {f : R⟦X⟧}
81     (hf : f.constantCoeff = 1) :
82     PowerSeries.map (φ : R →+* S) (PowerSeries.logOf f) =
83       PowerSeries.logOf (PowerSeries.map (φ : R →+* S) f) := by
84   rw [PowerSeries.logOf_eq, PowerSeries.logOf_eq]
85   have hzero : (f - 1).constantCoeff = 0 := by simp [hf]
86   let hsub : PowerSeries.HasSubst (f - 1) :=
87     PowerSeries.HasSubst.of_constantCoeff_zero' hzero
88   change ((PowerSeries.log R).subst (f - 1)).map (φ : R →+* S) = _
89   rw [PowerSeries.map_subst hsub]
90   rw [PowerSeries.map_log]
91   have hmap : MvPowerSeries.map (φ : R →+* S) (f - 1) =
92       PowerSeries.map (φ : R →+* S) f - 1 := by
93     rw [map_sub, map_one]
94     rfl
95   rw [hmap]
96 
97 theorem map_normalizedResidueNegativeLog (φ : R →ₐ[ℚ] S) (N j : ℕ) :
98     PowerSeries.map (φ : R →+* S)
99         (normalizedResidueNegativeLog (R := R) N j) =
100       normalizedResidueNegativeLog (R := S) N j := by
101   rw [normalizedResidueNegativeLog, normalizedResidueNegativeLog, map_neg,
102     map_logOf_of_constantCoeff_one φ
103       (constantCoeff_normalizedResidueSectionAlg (R := R) N j),
104     map_normalizedResidueSectionAlg]
105 
106 /-- Naturality of a zero-constant formal exponential parameter family. -/
107 theorem map_formalExpFamily (φ : R →ₐ[ℚ] S) {L : R⟦X⟧}
108     (hL : L.constantCoeff = 0) (r : R) :
109     PowerSeries.map (φ : R →+* S) (formalExpFamily L r) =
110       formalExpFamily (PowerSeries.map (φ : R →+* S) L) (φ r) := by
111   let hsub : PowerSeries.HasSubst L :=
112     PowerSeries.HasSubst.of_constantCoeff_zero' hL
113   rw [formalExpFamily, formalExpFamily]
114   change ((PowerSeries.rescale r (PowerSeries.exp R)).subst L).map
115       (φ : R →+* S) = _
116   rw [PowerSeries.map_subst hsub]
117   rw [← PowerSeries.rescale_map (φ : R →+* S), PowerSeries.map_exp]
118   have hmap : MvPowerSeries.map (φ : R →+* S) L =
119       PowerSeries.map (φ : R →+* S) L := rfl
120   rw [hmap]
121   rfl
122 
123 @[simp]
124 theorem constantCoeff_formalExpFamily_of_zero {L : R⟦X⟧}
125     (hL : L.constantCoeff = 0) (r : R) :
126     (formalExpFamily L r).constantCoeff = 1 := by
127   rw [formalExpFamily]
128   change MvPowerSeries.constantCoeff
129       ((PowerSeries.rescale r (PowerSeries.exp R)).subst L) = 1
130   rw [PowerSeries.constantCoeff_subst_of_constantCoeff_zero hL]
131   rw [← PowerSeries.coeff_zero_eq_constantCoeff, PowerSeries.coeff_rescale]
132   simp
133 
134 end Naturality
135 
136 section ResidueParameter
137 
138 variable {R : Type*} [CommRing R] [Algebra ℚ R]
139 
140 /-- The exact formal family `Phi_(N,j)(w)^(-r)`. -/
141 def residuePowerSeries (N j : ℕ) (r : R) : R⟦X⟧ :=
142   formalExpFamily (normalizedResidueNegativeLog (R := R) N j) r
143 
144 @[simp]
145 theorem constantCoeff_residuePowerSeries (N j : ℕ) (r : R) :
146     (residuePowerSeries N j r).constantCoeff = 1 := by
147   rw [residuePowerSeries, formalExpFamily]
148   change MvPowerSeries.constantCoeff
149       ((PowerSeries.rescale r (PowerSeries.exp R)).subst
150         (normalizedResidueNegativeLog N j)) = 1
151   rw [PowerSeries.constantCoeff_subst_of_constantCoeff_zero
152     (constantCoeff_normalizedResidueNegativeLog N j)]
153   rw [← PowerSeries.coeff_zero_eq_constantCoeff, PowerSeries.coeff_rescale]
154   simp
155 
156 @[simp]
157 theorem residuePowerSeries_zero (N j : ℕ) :
158     residuePowerSeries (R := R) N j 0 = 1 := by
159   exact formalExpFamily_zero (constantCoeff_normalizedResidueNegativeLog N j)
160 
161 theorem residuePowerSeries_neg_one (N j : ℕ) :
162     residuePowerSeries (R := R) N j (-1) =
163       normalizedResidueSectionAlg N j := by
164   rw [residuePowerSeries,
165     formalExpFamily_eq_exp_subst
166       (constantCoeff_normalizedResidueNegativeLog (R := R) N j)]
167   rw [normalizedResidueNegativeLog]
168   have h := exp_subst_logOf
169     (constantCoeff_normalizedResidueSectionAlg (R := R) N j)
170   simpa using h
171 
172 theorem residuePowerSeries_add (N j : ℕ) (r s : R) :
173     residuePowerSeries N j r * residuePowerSeries N j s =
174       residuePowerSeries N j (r + s) := by
175   exact formalExpFamily_semigroup
176     (constantCoeff_normalizedResidueNegativeLog N j) r s
177 
178 theorem map_residuePowerSeries {S : Type*} [CommRing S] [Algebra ℚ S]
179     (φ : R →ₐ[ℚ] S) (N j : ℕ) (r : R) :
180     PowerSeries.map (φ : R →+* S) (residuePowerSeries N j r) =
181       residuePowerSeries N j (φ r) := by
182   rw [residuePowerSeries, map_formalExpFamily φ
183     (constantCoeff_normalizedResidueNegativeLog N j),
184     map_normalizedResidueNegativeLog]
185   rfl
186 
187 section Field
188 
189 variable {K : Type*} [Field K] [CharZero K]
190 
191 theorem residuePowerSeries_one_eq_inverse (N j : ℕ) :
192     residuePowerSeries (R := K) N j 1 =
193       (normalizedResidueSectionAlg N j)⁻¹ := by
194   apply (PowerSeries.eq_inv_iff_mul_eq_one
195     (by simp : (normalizedResidueSectionAlg (R := K) N j).constantCoeff ≠ 0)).2
196   rw [← residuePowerSeries_neg_one (R := K) N j]
197   rw [residuePowerSeries_add, add_neg_cancel, residuePowerSeries_zero]
198 
199 end Field
200 
201 /-- Paper IV's arbitrary-order coefficient `C_(N,j,n)(r)`. -/
202 def residuePowerCoeff (N j n : ℕ) (r : R) : R :=
203   blockCoeff N n (residuePowerSeries N j r)
204 
205 @[simp]
206 theorem residuePowerCoeff_zero (N j : ℕ) (r : R) :
207     residuePowerCoeff N j 0 r = 1 := by
208   simp [residuePowerCoeff, blockCoeff]
209 
210 theorem residuePowerCoeff_addition (N j n : ℕ) (r s : R) :
211     residuePowerCoeff N j n (r + s) =
212       ∑ q ∈ Finset.range (n + 1),
213         ((N * n).choose (N * q) : R) *
214           residuePowerCoeff N j q r * residuePowerCoeff N j (n - q) s := by
215   exact reciprocal_block_convolution
216     (constantCoeff_normalizedResidueNegativeLog N j) N n r s
217 
218 theorem residuePowerCoeff_one_eq_residueInverseCoeff
219     {K : Type*} [Field K] [CharZero K] (N j n : ℕ) :
220     residuePowerCoeff (R := K) N j n 1 =
221       residueInverseCoeff (K := K) N j n := by
222   rw [residuePowerCoeff, residueInverseCoeff,
223     residuePowerSeries_one_eq_inverse,
224     normalizedResidueSectionAlg_eq_normalizedResidueSection]
225   rfl
226 
227 section PolynomialParameter
228 
229 variable {K : Type*} [Field K] [CharZero K]
230 
231 /-- The coefficient `C_(N,j,n)(r)` lifted to an honest polynomial in `r`. -/
232 def residuePowerCoeffPolynomial (N j n : ℕ) : Polynomial K :=
233   residuePowerCoeff (R := Polynomial K) N j n Polynomial.X
234 
235 /-- Evaluation of the polynomial lift recovers the arbitrary scalar
236 parameter coefficient. -/
237 theorem eval_residuePowerCoeffPolynomial (N j n : ℕ) (r : K) :
238     (residuePowerCoeffPolynomial (K := K) N j n).eval r =
239       residuePowerCoeff (R := K) N j n r := by
240   let φ : Polynomial K →ₐ[ℚ] K :=
241     (Polynomial.aeval r).restrictScalars ℚ
242   change φ (residuePowerCoeff
243       (R := Polynomial K) N j n Polynomial.X) = _
244   rw [residuePowerCoeff, residuePowerCoeff, blockCoeff, blockCoeff]
245   simp only [map_mul, map_natCast]
246   congr 1
247   change PowerSeries.coeff n
248       (PowerSeries.map (φ : Polynomial K →+* K)
249         (residuePowerSeries N j Polynomial.X)) = _
250   rw [map_residuePowerSeries φ]
251   simp [φ]
252 
253 /-- Coefficients of `exp (X L)` have parameter degree at most their series
254 index when the coefficients of `L` are scalar constants. -/
255 theorem natDegree_coeff_formalExpFamily_map_C_le
256     (L : K⟦X⟧) (hL : L.constantCoeff = 0) (n : ℕ) :
257     (PowerSeries.coeff n
258       (formalExpFamily (PowerSeries.map Polynomial.C L) Polynomial.X)).natDegree ≤ n := by
259   induction n using Nat.strong_induction_on with
260   | h n ih =>
261       cases n with
262       | zero =>
263           rw [PowerSeries.coeff_zero_eq_constantCoeff]
264           rw [constantCoeff_formalExpFamily_of_zero]
265           · simp
266           · change Polynomial.C (PowerSeries.constantCoeff L) = 0
267             rw [hL, map_zero]
268       | succ k =>
269           let LC : (Polynomial K)⟦X⟧ := PowerSeries.map Polynomial.C L
270           have hLC : LC.constantCoeff = 0 := by
271             change Polynomial.C (PowerSeries.constantCoeff L) = 0
272             rw [hL, map_zero]
273           have hrec := formalExpFamily_coefficient_recurrence
274             hLC Polynomial.X k
275           have hsum :
276               (∑ p ∈ Finset.antidiagonal k,
277                 PowerSeries.coeff p.1 (formalExpFamily LC Polynomial.X) *
278                   ((p.2 + 1 : Polynomial K) *
279                     PowerSeries.coeff (p.2 + 1) LC)).natDegree ≤ k := by
280             apply Polynomial.natDegree_sum_le_of_forall_le
281             intro p hp
282             have hpadd : p.1 + p.2 = k := Finset.mem_antidiagonal.mp hp
283             have hp_lt : p.1 < k + 1 := by omega
284             have hpdeg :
285                 (PowerSeries.coeff p.1
286                   (formalExpFamily LC Polynomial.X)).natDegree ≤ p.1 := by
287               simpa [LC] using ih p.1 hp_lt
288             have hconst :
289                 (((p.2 + 1 : Polynomial K) *
290                   PowerSeries.coeff (p.2 + 1) LC)).natDegree ≤ 0 := by
291               have ha : (p.2 + 1 : Polynomial K).natDegree ≤ 0 := by
292                 change (Polynomial.C (p.2 : K) + Polynomial.C 1).natDegree ≤ 0
293                 rw [← map_add]
294                 simp
295               have hb : (PowerSeries.coeff (p.2 + 1) LC).natDegree ≤ 0 := by
296                 rw [show PowerSeries.coeff (p.2 + 1) LC =
297                     Polynomial.C (PowerSeries.coeff (p.2 + 1) L) by
298                       simp [LC]]
299                 simp
300               exact Polynomial.natDegree_mul_le_of_le ha hb
301             exact (Polynomial.natDegree_mul_le_of_le hpdeg hconst).trans (by omega)
302           have hrhs :
303               (Polynomial.X *
304                 ∑ p ∈ Finset.antidiagonal k,
305                   PowerSeries.coeff p.1 (formalExpFamily LC Polynomial.X) *
306                     ((p.2 + 1 : Polynomial K) *
307                       PowerSeries.coeff (p.2 + 1) LC)).natDegree ≤ k + 1 := by
308             exact (Polynomial.natDegree_mul_le_of_le Polynomial.natDegree_X_le hsum).trans
309               (by omega)
310           have hscalar : (k + 1 : Polynomial K) =
311               Polynomial.C (k + 1 : K) := by simp
312           have hscalar_ne : (k + 1 : K) ≠ 0 := by
313             exact_mod_cast Nat.succ_ne_zero k
314           rw [hscalar] at hrec
315           have hdeg_left :
316               (Polynomial.C (k + 1 : K) *
317                 PowerSeries.coeff (k + 1)
318                   (formalExpFamily LC Polynomial.X)).natDegree =
319                 (PowerSeries.coeff (k + 1)
320                   (formalExpFamily LC Polynomial.X)).natDegree := by
321             rw [Polynomial.natDegree_C_mul hscalar_ne]
322           rw [← hdeg_left]
323           rw [hrec]
324           simpa only [LC] using hrhs
325 
326 /-- The top parameter coefficient of `exp (X L)` comes only from the nth
327 power of the linear term of `L`. -/
328 theorem coeff_parameterDegree_formalExpFamily_map_C
329     (L : K⟦X⟧) (hL : L.constantCoeff = 0) (n : ℕ) :
330     (PowerSeries.coeff n
331       (formalExpFamily (PowerSeries.map Polynomial.C L) Polynomial.X)).coeff n =
332       (PowerSeries.coeff 1 L) ^ n / (n.factorial : K) := by
333   induction n with
334   | zero =>
335       rw [PowerSeries.coeff_zero_eq_constantCoeff,
336         constantCoeff_formalExpFamily_of_zero]
337       · simp
338       · change Polynomial.C (PowerSeries.constantCoeff L) = 0
339         rw [hL, map_zero]
340   | succ k ih =>
341       let LC : (Polynomial K)⟦X⟧ := PowerSeries.map Polynomial.C L
342       have hLC : LC.constantCoeff = 0 := by
343         change Polynomial.C (PowerSeries.constantCoeff L) = 0
344         rw [hL, map_zero]
345       have hrec := formalExpFamily_coefficient_recurrence
346         hLC Polynomial.X k
347       rw [Finset.Nat.sum_antidiagonal_eq_sum_range_succ_mk] at hrec
348       have hsumCoeff :
349           (fun p : Polynomial K => p.coeff k)
350               (∑ q ∈ Finset.range (k + 1),
351                 PowerSeries.coeff q (formalExpFamily LC Polynomial.X) *
352                   ((((k - q : ℕ) : Polynomial K) + 1) *
353                     PowerSeries.coeff (k - q + 1) LC)) =
354             (PowerSeries.coeff k
355               (formalExpFamily LC Polynomial.X)).coeff k *
356                 PowerSeries.coeff 1 L := by
357         change
358           (∑ q ∈ Finset.range (k + 1),
359             PowerSeries.coeff q (formalExpFamily LC Polynomial.X) *
360               ((((k - q : ℕ) : Polynomial K) + 1) *
361                 PowerSeries.coeff (k - q + 1) LC)).coeff k = _
362         rw [Polynomial.finsetSum_coeff, Finset.sum_range_succ]
363         have hvanish :
364             ∑ q ∈ Finset.range k,
365                 (fun p : Polynomial K => p.coeff k)
366                   (PowerSeries.coeff q (formalExpFamily LC Polynomial.X) *
367                     ((((k - q : ℕ) : Polynomial K) + 1) *
368                       PowerSeries.coeff (k - q + 1) LC)) = 0 := by
369           apply Finset.sum_eq_zero
370           intro q hq
371           have hqk : q < k := Finset.mem_range.mp hq
372           have hqdeg :
373               (PowerSeries.coeff q
374                 (formalExpFamily LC Polynomial.X)).natDegree ≤ q := by
375             simpa [LC] using natDegree_coeff_formalExpFamily_map_C_le L hL q
376           have hconst :
377               (((((k - q : ℕ) : Polynomial K) + 1) *
378                 PowerSeries.coeff (k - q + 1) LC)).natDegree ≤ 0 := by
379             have ha : (((k - q : ℕ) : Polynomial K) + 1).natDegree ≤ 0 := by
380               simp
381             have hb :
382                 (PowerSeries.coeff (k - q + 1) LC).natDegree ≤ 0 := by
383               rw [show PowerSeries.coeff (k - q + 1) LC =
384                   Polynomial.C (PowerSeries.coeff (k - q + 1) L) by
385                     simp [LC]]
386               simp
387             exact Polynomial.natDegree_mul_le_of_le ha hb
388           exact Polynomial.coeff_eq_zero_of_natDegree_lt
389             ((Polynomial.natDegree_mul_le_of_le hqdeg hconst).trans_lt (by omega))
390         rw [hvanish, zero_add]
391         simp only [Nat.sub_self, zero_add]
392         rw [show PowerSeries.coeff 1 LC =
393             Polynomial.C (PowerSeries.coeff 1 L) by simp [LC]]
394         simp [Polynomial.coeff_mul_C]
395       have hpoly := congrArg (fun p : Polynomial K => p.coeff (k + 1)) hrec
396       rw [show (k + 1 : Polynomial K) =
397           Polynomial.C (k + 1 : K) by simp,
398         Polynomial.coeff_C_mul, Polynomial.coeff_X_mul] at hpoly
399       simp only [Nat.succ_eq_add_one] at hpoly
400       have hsumCoeffEq :
401           (∑ q ∈ Finset.range (k + 1),
402             PowerSeries.coeff q (formalExpFamily LC Polynomial.X) *
403               ((((k - q : ℕ) : Polynomial K) + 1) *
404                 PowerSeries.coeff (k - q + 1) LC)).coeff k =
405             (PowerSeries.coeff k
406               (formalExpFamily LC Polynomial.X)).coeff k *
407                 PowerSeries.coeff 1 L := hsumCoeff
408       rw [hsumCoeffEq] at hpoly
409       change (k + 1 : K) *
410           (PowerSeries.coeff (k + 1)
411             (formalExpFamily LC Polynomial.X)).coeff (k + 1) = _ at hpoly
412       rw [show PowerSeries.coeff k (formalExpFamily LC Polynomial.X) =
413           PowerSeries.coeff k
414             (formalExpFamily (PowerSeries.map Polynomial.C L) Polynomial.X) by rfl,
415         ih] at hpoly
416       rw [show PowerSeries.coeff (k + 1)
417           (formalExpFamily (PowerSeries.map Polynomial.C L) Polynomial.X) =
418           PowerSeries.coeff (k + 1)
419             (formalExpFamily LC Polynomial.X) by rfl]
420       have hfac : (k.factorial : K) ≠ 0 := by
421         exact_mod_cast k.factorial_pos.ne'
422       have hsuccfac : ((k + 1).factorial : K) ≠ 0 := by
423         exact_mod_cast (k + 1).factorial_pos.ne'
424       apply (eq_div_iff hsuccfac).2
425       rw [Nat.factorial_succ, Nat.cast_mul]
426       rw [Nat.cast_add, Nat.cast_one]
427       calc
428         (PowerSeries.coeff (k + 1)
429               (formalExpFamily LC Polynomial.X)).coeff (k + 1) *
430             ((k + 1 : K) * (k.factorial : K)) =
431           ((k + 1 : K) *
432             (PowerSeries.coeff (k + 1)
433               (formalExpFamily LC Polynomial.X)).coeff (k + 1)) *
434                 (k.factorial : K) := by ring
435         _ = (((PowerSeries.coeff 1 L) ^ k / (k.factorial : K)) *
436               PowerSeries.coeff 1 L) * (k.factorial : K) := by rw [hpoly]
437         _ = (PowerSeries.coeff 1 L) ^ (k + 1) := by
438           rw [pow_succ]
439           field_simp
440 
441 theorem coeff_one_logOf_of_constantCoeff_one {f : K⟦X⟧}
442     (hf : f.constantCoeff = 1) :
443     PowerSeries.coeff 1 (PowerSeries.logOf f) = PowerSeries.coeff 1 f := by
444   have h := congrArg (PowerSeries.coeff (R := K) 0)
445     (mul_derivative_logOf hf)
446   rw [PowerSeries.coeff_mul, Finset.Nat.antidiagonal_zero] at h
447   simp [PowerSeries.coeff_derivative, hf] at h
448   exact h
449 
450 theorem coeff_one_normalizedResidueNegativeLog (N j : ℕ) :
451     PowerSeries.coeff 1 (normalizedResidueNegativeLog (R := K) N j) =
452       -(j.factorial : K) / ((N + j).factorial : K) := by
453   rw [normalizedResidueNegativeLog, map_neg,
454     coeff_one_logOf_of_constantCoeff_one
455       (constantCoeff_normalizedResidueSectionAlg (R := K) N j),
456     coeff_normalizedResidueSectionAlg]
457   simp only [Nat.mul_one]
458   rw [show N + j = N * 1 + j by simp]
459   simp
460   ring
461 
462 /-- Exact leading coefficient asserted in Theorem 9.4. -/
463 theorem coeff_residuePowerCoeffPolynomial_parameterDegree (N j n : ℕ) :
464     (residuePowerCoeffPolynomial (K := K) N j n).coeff n =
465       ((N * n).factorial : K) / (n.factorial : K) *
466         (-(j.factorial : K) / ((N + j).factorial : K)) ^ n := by
467   let L : K⟦X⟧ := normalizedResidueNegativeLog (R := K) N j
468   let Cφ : K →ₐ[ℚ] Polynomial K :=
469     (Polynomial.CAlgHom : K →ₐ[K] Polynomial K).restrictScalars ℚ
470   have hmapL : PowerSeries.map (Cφ : K →+* Polynomial K) L =
471       normalizedResidueNegativeLog (R := Polynomial K) N j := by
472     simpa [L, Cφ] using map_normalizedResidueNegativeLog Cφ N j
473   have hmapC : PowerSeries.map (Cφ : K →+* Polynomial K) L =
474       PowerSeries.map Polynomial.C L := by
475     ext q
476     simp [Cφ]
477   rw [residuePowerCoeffPolynomial, residuePowerCoeff, blockCoeff,
478     residuePowerSeries, ← hmapL]
479   rw [show ((N * n).factorial : Polynomial K) =
480       Polynomial.C ((N * n).factorial : K) by simp]
481   rw [hmapC]
482   rw [Polynomial.coeff_C_mul,
483     coeff_parameterDegree_formalExpFamily_map_C L
484       (constantCoeff_normalizedResidueNegativeLog N j),
485     coeff_one_normalizedResidueNegativeLog]
486   field_simp
487 
488 theorem natDegree_residuePowerCoeffPolynomial_le (N j n : ℕ) :
489     (residuePowerCoeffPolynomial (K := K) N j n).natDegree ≤ n := by
490   let L : K⟦X⟧ := normalizedResidueNegativeLog (R := K) N j
491   let Cφ : K →ₐ[ℚ] Polynomial K :=
492     (Polynomial.CAlgHom : K →ₐ[K] Polynomial K).restrictScalars ℚ
493   have hmapL : PowerSeries.map (Cφ : K →+* Polynomial K) L =
494       normalizedResidueNegativeLog (R := Polynomial K) N j := by
495     simpa [L, Cφ] using map_normalizedResidueNegativeLog Cφ N j
496   have hdeg := natDegree_coeff_formalExpFamily_map_C_le L
497     (constantCoeff_normalizedResidueNegativeLog N j) n
498   rw [residuePowerCoeffPolynomial, residuePowerCoeff, blockCoeff,
499     residuePowerSeries, ← hmapL]
500   exact (Polynomial.natDegree_C_mul_le _ _).trans hdeg
501 
502 /-- The parameter degree in Theorem 9.4 is exact. -/
503 theorem natDegree_residuePowerCoeffPolynomial (N j n : ℕ) :
504     (residuePowerCoeffPolynomial (K := K) N j n).natDegree = n := by
505   apply Polynomial.natDegree_eq_of_le_of_coeff_ne_zero
506     (natDegree_residuePowerCoeffPolynomial_le N j n)
507   rw [coeff_residuePowerCoeffPolynomial_parameterDegree]
508   have hNn : ((N * n).factorial : K) ≠ 0 := by
509     exact_mod_cast (N * n).factorial_pos.ne'
510   have hn : (n.factorial : K) ≠ 0 := by
511     exact_mod_cast n.factorial_pos.ne'
512   have hj : (j.factorial : K) ≠ 0 := by
513     exact_mod_cast j.factorial_pos.ne'
514   have hNj : ((N + j).factorial : K) ≠ 0 := by
515     exact_mod_cast (N + j).factorial_pos.ne'
516   exact mul_ne_zero (div_ne_zero hNn hn)
517     (pow_ne_zero n (div_ne_zero (neg_ne_zero.mpr hj) hNj))
518 
519 end PolynomialParameter
520 
521 end ResidueParameter
522 
523 section ResidueAppellParameter
524 
525 variable {R : Type*} [CommRing R] [Algebra ℚ R]
526 
527 /-- The normalized-residue logarithm after the substitution `w = z^N`. -/
528 def expandedResidueNegativeLog (N j : ℕ) (hN : 0 < N) : R⟦X⟧ :=
529   PowerSeries.expand N hN.ne'
530     (normalizedResidueNegativeLog (R := R) N j)
531 
532 @[simp]
533 theorem constantCoeff_expandedResidueNegativeLog (N j : ℕ) (hN : 0 < N) :
534     (expandedResidueNegativeLog (R := R) N j hN).constantCoeff = 0 := by
535   simp [expandedResidueNegativeLog]
536 
537 /-- Expanding the reduced arbitrary-order reciprocal commutes with its formal
538 exponential construction. -/
539 theorem expand_residuePowerSeries (N j : ℕ) (hN : 0 < N) (r : R) :
540     PowerSeries.expand N hN.ne' (residuePowerSeries N j r) =
541       formalExpFamily (expandedResidueNegativeLog N j hN) r := by
542   rw [residuePowerSeries, formalExpFamily, expandedResidueNegativeLog]
543   let hsub : PowerSeries.HasSubst
544       (normalizedResidueNegativeLog (R := R) N j) :=
545     PowerSeries.HasSubst.of_constantCoeff_zero'
546       (constantCoeff_normalizedResidueNegativeLog N j)
547   exact PowerSeries.expand_subst N hN.ne' hsub
548     (PowerSeries.rescale r (PowerSeries.exp R))
549 
550 /-- The EGF coefficients of the expanded reciprocal are precisely the sparse
551 block sequence attached to `C_(N,j,n)(r)`. -/
552 theorem egfCoeff_expand_residuePowerSeries (N j q : ℕ) (hN : 0 < N)
553     (r : R) :
554     egfCoeff q (PowerSeries.expand N hN.ne' (residuePowerSeries N j r)) =
555       blockCoefficientSequence N (fun n => residuePowerCoeff N j n r) q := by
556   by_cases hdvd : N ∣ q
557   · have hmul : N * (q / N) = q := Nat.mul_div_cancel' hdvd
558     simp [egfCoeff, blockCoefficientSequence, residuePowerCoeff, blockCoeff,
559       PowerSeries.coeff_expand, hdvd, hmul]
560   · simp [egfCoeff, blockCoefficientSequence, PowerSeries.coeff_expand, hdvd]
561 
562 /-- The exact arbitrary-order residue Appell polynomial
563 `E_m^(N,j,r)(x)`. -/
564 def residueAppellPolynomialParam (N j : ℕ) (hN : 0 < N)
565     (r : R) (m : ℕ) : Polynomial R :=
566   formalAppellPolynomial (expandedResidueNegativeLog N j hN) r m
567 
568 theorem residueAppellPolynomialParam_eq_block (N j : ℕ) (hN : 0 < N)
569     (r : R) (m : ℕ) :
570     residueAppellPolynomialParam N j hN r m =
571       appellPolynomial
572         (blockCoefficientSequence N (fun n => residuePowerCoeff N j n r)) m := by
573   rw [residueAppellPolynomialParam, formalAppellPolynomial]
574   congr 1
575   funext q
576   rw [← expand_residuePowerSeries N j hN r]
577   exact egfCoeff_expand_residuePowerSeries N j q hN r
578 
579 /-- The manuscript's finite explicit sum, now specialized at arbitrary
580 reciprocal order `r`. -/
581 theorem residueAppellPolynomialParam_explicit (N j : ℕ) (hN : 0 < N)
582     (r : R) (m : ℕ) :
583     residueAppellPolynomialParam N j hN r m =
584       ∑ n ∈ Finset.range (m / N + 1),
585         Polynomial.C
586             ((m.choose (N * n) : R) * residuePowerCoeff N j n r) *
587           Polynomial.X ^ (m - N * n) := by
588   rw [residueAppellPolynomialParam_eq_block]
589   exact appellPolynomial_eq_block_sum N m hN _
590 
591 /-- Exact Appell lowering law for every residue order. -/
592 theorem derivative_residueAppellPolynomialParam (N j : ℕ) (hN : 0 < N)
593     (r : R) (m : ℕ) :
594     Polynomial.derivative (residueAppellPolynomialParam N j hN r (m + 1)) =
595       Polynomial.C (m + 1 : R) * residueAppellPolynomialParam N j hN r m := by
596   exact derivative_formalAppellPolynomial
597     (expandedResidueNegativeLog N j hN) r m
598 
599 /-- Exact Appell translation law in the manuscript's arbitrary-order
600 normalized-residue specialization. -/
601 theorem eval_residueAppellPolynomialParam_add (N j : ℕ) (hN : 0 < N)
602     (r x y : R) (m : ℕ) :
603     (residueAppellPolynomialParam N j hN r m).eval (x + y) =
604       ∑ p ∈ Finset.antidiagonal m,
605         (m.choose p.1 : R) *
606           (residueAppellPolynomialParam N j hN r p.1).eval x * y ^ p.2 := by
607   let L : R⟦X⟧ := expandedResidueNegativeLog N j hN
608   have hL : L.constantCoeff = 0 := by simp [L]
609   have h := appell_addition hL r x y m
610   simpa [residueAppellPolynomialParam, L, eval_formalAppellPolynomial] using h
611 
612 /-- Exact joint convolution in space and residue order. -/
613 theorem eval_residueAppellPolynomialParam_two_parameter
614     (N j : ℕ) (hN : 0 < N) (r s x y : R) (m : ℕ) :
615     (residueAppellPolynomialParam N j hN (r + s) m).eval (x + y) =
616       ∑ p ∈ Finset.antidiagonal m,
617         (m.choose p.1 : R) *
618           (residueAppellPolynomialParam N j hN r p.1).eval x *
619           (residueAppellPolynomialParam N j hN s p.2).eval y := by
620   let L : R⟦X⟧ := expandedResidueNegativeLog N j hN
621   have hL : L.constantCoeff = 0 := by simp [L]
622   have h := appell_two_parameter_convolution hL r s x y m
623   simpa [residueAppellPolynomialParam, L, eval_formalAppellPolynomial] using h
624 
625 /-- The arbitrary-order residue Appell polynomial is monic of exact degree
626 `m`. -/
627 theorem residueAppellPolynomialParam_isMonicOfDegree [Nontrivial R]
628     (N j : ℕ) (hN : 0 < N) (r : R) (m : ℕ) :
629     Polynomial.IsMonicOfDegree
630       (residueAppellPolynomialParam N j hN r m) m := by
631   rw [residueAppellPolynomialParam_eq_block]
632   apply blockAppellPolynomial_isMonicOfDegree
633   simp [residuePowerCoeff_zero]
634 
635 /-- The exact root-of-unity covariance at arbitrary residue order. -/
636 theorem eval_residueAppellPolynomialParam_covariance
637     (N j : ℕ) (hN : 0 < N) (r ω x : R) (hω : ω ^ N = 1) (m : ℕ) :
638     (residueAppellPolynomialParam N j hN r m).eval (ω * x) =
639       ω ^ m * (residueAppellPolynomialParam N j hN r m).eval x := by
640   rw [residueAppellPolynomialParam_eq_block]
641   exact eval_appellPolynomial_block_covariance N m hN _ ω x hω
642 
643 /-- First half of the differential-operator representation: the arbitrary
644 residue symbol acting on `X^m` is the named Appell polynomial. -/
645 theorem egfConstantCoeffAction_residuePowerSeries_X_pow
646     (N j : ℕ) (hN : 0 < N) (r : R) (m : ℕ) [Nontrivial R] :
647     egfConstantCoeffAction
648         (fun q => egfCoeff q
649           (PowerSeries.expand N hN.ne' (residuePowerSeries N j r)))
650         (Polynomial.X ^ m) =
651       residueAppellPolynomialParam N j hN r m := by
652   rw [egfConstantCoeffAction_X_pow]
653   rw [residueAppellPolynomialParam_eq_block]
654   congr 1
655   funext q
656   exact egfCoeff_expand_residuePowerSeries N j q hN r
657 
658 /-- Arbitrary formal powers with opposite orders give inverse finite
659 differential operators on every polynomial of degree at most `d`. -/
660 theorem truncatedDifferentialOperator_residuePowerSeries_inverse
661     (N j : ℕ) (hN : 0 < N) (r : R) (d : ℕ)
662     {p : Polynomial R} (hp : p.natDegree ≤ d) :
663     (truncatedDifferentialOperator d
664         (PowerSeries.expand N hN.ne' (residuePowerSeries N j (-r))) *
665       truncatedDifferentialOperator d
666         (PowerSeries.expand N hN.ne' (residuePowerSeries N j r))) p = p := by
667   apply truncatedDifferentialOperator_mul_apply_of_natDegree_le hp
668   rw [← map_mul, residuePowerSeries_add, neg_add_cancel,
669     residuePowerSeries_zero, map_one]
670 
671 end ResidueAppellParameter
672 
673 section ThetaPolynomial
674 
675 variable {R S : Type*} [CommRing R] [Algebra ℚ R]
676   [CommRing S] [Algebra ℚ S]
677 
678 theorem map_reducedDenominator (φ : R →ₐ[ℚ] S) (N : ℕ) :
679     PowerSeries.map (φ : R →+* S) (reducedDenominator (R := R) N) =
680       reducedDenominator (R := S) N := by
681   ext n
682   simp [reducedDenominator]
683 
684 theorem map_negativeLogDenominator (φ : R →ₐ[ℚ] S) (N : ℕ) :
685     PowerSeries.map (φ : R →+* S)
686         (negativeLogDenominator (R := R) N) =
687       negativeLogDenominator (R := S) N := by
688   rw [negativeLogDenominator, negativeLogDenominator, map_neg,
689     map_logOf_of_constantCoeff_one φ
690       (constantCoeff_reducedDenominator (R := R) N),
691     map_reducedDenominator]
692 
693 theorem map_reciprocalSeries (φ : R →ₐ[ℚ] S) (N : ℕ) (r : R) :
694     PowerSeries.map (φ : R →+* S) (reciprocalSeries N r) =
695       reciprocalSeries N (φ r) := by
696   rw [reciprocalSeries, map_formalExpFamily φ
697     (constantCoeff_negativeLogDenominator N), map_negativeLogDenominator]
698   rfl
699 
700 theorem map_thetaSeries (φ : R →ₐ[ℚ] S) (N : ℕ) (u : R) :
701     PowerSeries.map (φ : R →+* S) (thetaSeries N u) =
702       thetaSeries N (φ u) := by
703   rw [thetaSeries, thetaSeries, map_mul]
704   rw [← PowerSeries.rescale_map (φ : R →+* S),
705     ← PowerSeries.rescale_map (φ : R →+* S)]
706   rw [map_reciprocalSeries, map_reciprocalSeries]
707   simp
708 
709 section Field
710 
711 variable {K : Type*} [Field K] [CharZero K]
712 
713 /-- Paper IV's theta coefficient as a polynomial in its parameter. -/
714 def thetaPolynomial (N n : ℕ) : Polynomial K :=
715   thetaCoeff (R := Polynomial K) N n Polynomial.X
716 
717 /-- The reciprocal coefficient `P_(N,n)(u)` as a polynomial in `u`. -/
718 def reciprocalCoeffPolynomialOver (N n : ℕ) : Polynomial K :=
719   reciprocalCoeff (R := Polynomial K) N n Polynomial.X
720 
721 theorem eval_reciprocalCoeffPolynomialOver (N n : ℕ) (u : K) :
722     (reciprocalCoeffPolynomialOver (K := K) N n).eval u =
723       reciprocalCoeff (R := K) N n u := by
724   let φ : Polynomial K →ₐ[ℚ] K :=
725     (Polynomial.aeval u).restrictScalars ℚ
726   change φ (reciprocalCoeff
727       (R := Polynomial K) N n Polynomial.X) = _
728   rw [reciprocalCoeff, reciprocalCoeff, blockCoeff, blockCoeff]
729   simp only [map_mul, map_natCast]
730   congr 1
731   change PowerSeries.coeff n
732       (PowerSeries.map (φ : Polynomial K →+* K)
733         (reciprocalSeries N Polynomial.X)) = _
734   rw [map_reciprocalSeries φ]
735   simp [φ]
736 
737 theorem natDegree_reciprocalCoeffPolynomialOver_le (N n : ℕ) :
738     (reciprocalCoeffPolynomialOver (K := K) N n).natDegree ≤ n := by
739   let L : K⟦X⟧ := negativeLogDenominator (R := K) N
740   let Cφ : K →ₐ[ℚ] Polynomial K :=
741     (Polynomial.CAlgHom : K →ₐ[K] Polynomial K).restrictScalars ℚ
742   have hmapL : PowerSeries.map (Cφ : K →+* Polynomial K) L =
743       negativeLogDenominator (R := Polynomial K) N := by
744     simpa [L, Cφ] using map_negativeLogDenominator Cφ N
745   have hdeg := natDegree_coeff_formalExpFamily_map_C_le L
746     (constantCoeff_negativeLogDenominator N) n
747   rw [reciprocalCoeffPolynomialOver, reciprocalCoeff, blockCoeff,
748     reciprocalSeries, ← hmapL]
749   exact (Polynomial.natDegree_C_mul_le _ _).trans hdeg
750 
751 theorem reciprocalCoeff_polynomial_one_eq_C (N n : ℕ) :
752     reciprocalCoeff (R := Polynomial K) N n 1 =
753       Polynomial.C (reciprocalCoeff (R := K) N n 1) := by
754   let Cφ : K →ₐ[ℚ] Polynomial K :=
755     (Polynomial.CAlgHom : K →ₐ[K] Polynomial K).restrictScalars ℚ
756   have hs := congrArg (PowerSeries.coeff (R := Polynomial K) n)
757     (map_reciprocalSeries Cφ N (1 : K))
758   rw [PowerSeries.coeff_map] at hs
759   simp [Cφ] at hs
760   rw [reciprocalCoeff, reciprocalCoeff, blockCoeff, blockCoeff, ← hs]
761   simp
762 
763 theorem eval_thetaPolynomial (N n : ℕ) (u : K) :
764     (thetaPolynomial (K := K) N n).eval u = thetaCoeff N n u := by
765   let φ : Polynomial K →ₐ[ℚ] K :=
766     (Polynomial.aeval u).restrictScalars ℚ
767   change φ (thetaCoeff (R := Polynomial K) N n Polynomial.X) = _
768   rw [thetaCoeff, thetaCoeff, blockCoeff, blockCoeff]
769   simp only [map_mul, map_natCast]
770   congr 1
771   change PowerSeries.coeff n
772       (PowerSeries.map (φ : Polynomial K →+* K)
773         (thetaSeries N Polynomial.X)) = _
774   rw [map_thetaSeries φ]
775   simp [φ]
776 
777 /-- The reconstruction theorem gives the manuscript degree bound on the
778 theta polynomial. -/
779 theorem natDegree_thetaPolynomial_le (N n : ℕ) (hN : 0 < N) :
780     (thetaPolynomial (K := K) N n).natDegree ≤ N * n := by
781   rw [thetaPolynomial, thetaCoeff_reconstruction]
782   have hsum :
783       (∑ q ∈ Finset.range (n + 1),
784         ((N * n).choose (N * q) : Polynomial K) *
785           reciprocalCoeff N q 1 * Polynomial.X ^ (N * q) *
786             reciprocalCoeff N (n - q) Polynomial.X).natDegree ≤ N * n := by
787     apply Polynomial.natDegree_sum_le_of_forall_le
788     intro q hq
789     have hqn : q ≤ n := Nat.le_of_lt_succ (Finset.mem_range.mp hq)
790     have hconstChoose :
791         ((N * n).choose (N * q) : Polynomial K).natDegree ≤ 0 := by simp
792     have hconstOne :
793         (reciprocalCoeff (R := Polynomial K) N q 1).natDegree ≤ 0 := by
794       rw [reciprocalCoeff_polynomial_one_eq_C]
795       simp
796     have hX : (Polynomial.X ^ (N * q) : Polynomial K).natDegree ≤ N * q :=
797       Polynomial.natDegree_X_pow_le (N * q)
798     have hparam :
799         (reciprocalCoeff (R := Polynomial K) N (n - q) Polynomial.X).natDegree ≤
800           n - q := by
801       exact natDegree_reciprocalCoeffPolynomialOver_le N (n - q)
802     have hterm :
803         (((N * n).choose (N * q) : Polynomial K) *
804           reciprocalCoeff N q 1 * Polynomial.X ^ (N * q) *
805             reciprocalCoeff N (n - q) Polynomial.X).natDegree ≤
806           N * q + (n - q) := by
807       have hbase :
808           (((N * n).choose (N * q) : Polynomial K) *
809             reciprocalCoeff N q 1).natDegree ≤ 0 := by
810         simpa using Polynomial.natDegree_mul_le_of_le hconstChoose hconstOne
811       have hwithX :
812           (((N * n).choose (N * q) : Polynomial K) *
813             reciprocalCoeff N q 1 * Polynomial.X ^ (N * q)).natDegree ≤
814               N * q := by
815         simpa using Polynomial.natDegree_mul_le_of_le hbase hX
816       exact Polynomial.natDegree_mul_le_of_le hwithX hparam
817     have hone : 1 ≤ N := hN
818     have hrest : n - q ≤ N * (n - q) := by
819       calc
820         n - q = 1 * (n - q) := by simp
821         _ ≤ N * (n - q) := Nat.mul_le_mul_right (n - q) hone
822     have hsplit : N * q + N * (n - q) = N * n := by
823       rw [← Nat.mul_add, Nat.add_sub_of_le hqn]
824     exact hterm.trans (by omega)
825   have hsign : ((-1 : Polynomial K) ^ n).natDegree ≤ 0 := by
826     have hneg : (-1 : Polynomial K).natDegree ≤ 0 := by simp
827     simpa only [Nat.mul_zero] using Polynomial.natDegree_pow_le_of_le n hneg
828   simpa using Polynomial.natDegree_mul_le_of_le hsign hsum
829 
830 /-- The first trivial theta factor, now as literal polynomial divisibility. -/
831 theorem X_dvd_thetaPolynomial (N n : ℕ) (hN : 0 < N) (hn : 0 < n) :
832     Polynomial.X ∣ thetaPolynomial (K := K) N n := by
833   rw [Polynomial.X_dvd_iff, Polynomial.coeff_zero_eq_eval_zero,
834     eval_thetaPolynomial]
835   exact thetaCoeff_zero_parameter_of_pos N hN hn
836 
837 /-- For even block size, the second trivial theta factor is literal
838 divisibility by `X + 1`. -/
839 theorem X_add_one_dvd_thetaPolynomial_of_even
840     (N n : ℕ) (_hN : 0 < N) (heven : Even N) (hn : 0 < n) :
841     Polynomial.X + 1 ∣ thetaPolynomial (K := K) N n := by
842   have hroot : (thetaPolynomial (K := K) N n).IsRoot (-1) := by
843     rw [Polynomial.IsRoot, eval_thetaPolynomial]
844     exact thetaCoeff_neg_one_of_even_of_pos N heven hn
845   have hdvd := Polynomial.dvd_iff_isRoot.mpr hroot
846   simpa [sub_neg_eq_add] using hdvd
847 
848 end Field
849 
850 end ThetaPolynomial
851 
852 section ThetaNewton
853 
854 variable {R : Type*} [CommRing R] [Algebra ℚ R]
855 
856 omit [Algebra ℚ R] in
857 /-- Formal differentiation commutes with rescaling up to the chain-rule
858 factor. -/
859 theorem derivative_rescale_series (a : R) (f : R⟦X⟧) :
860     PowerSeries.derivative R (PowerSeries.rescale a f) =
861       PowerSeries.C a *
862         PowerSeries.rescale a (PowerSeries.derivative R f) := by
863   ext n
864   rw [PowerSeries.coeff_derivative, PowerSeries.coeff_C_mul,
865     PowerSeries.coeff_rescale, PowerSeries.coeff_rescale,
866     PowerSeries.coeff_derivative, pow_succ]
867   ring
868 
869 omit [Algebra ℚ R] in
870 theorem rescale_C_series (a r : R) :
871     PowerSeries.rescale a (PowerSeries.C r) = PowerSeries.C r := by
872   ext (_ | n)
873   · simp
874   · simp
875 
876 /-- Logarithmic-derivative factor for a rescaled reciprocal family. -/
877 def scaledReciprocalLogDerivative (N : ℕ) (a r : R) : R⟦X⟧ :=
878   PowerSeries.C (a * r) *
879     PowerSeries.rescale a
880       (PowerSeries.derivative R (negativeLogDenominator N))
881 
882 theorem derivative_rescale_reciprocalSeries (N : ℕ) (a r : R) :
883     PowerSeries.derivative R
884         (PowerSeries.rescale a (reciprocalSeries N r)) =
885       PowerSeries.rescale a (reciprocalSeries N r) *
886         scaledReciprocalLogDerivative N a r := by
887   rw [derivative_rescale_series, derivative_reciprocalSeries]
888   rw [map_mul, map_mul]
889   rw [rescale_C_series]
890   rw [scaledReciprocalLogDerivative]
891   rw [map_mul]
892   ring
893 
894 /-- The logarithmic derivative multiplying the theta series. -/
895 def thetaLogDerivativeSeries (N : ℕ) (u : R) : R⟦X⟧ :=
896   scaledReciprocalLogDerivative N (-u ^ N) 1 +
897     scaledReciprocalLogDerivative N (-1) u
898 
899 theorem derivative_thetaSeries (N : ℕ) (u : R) :
900     PowerSeries.derivative R (thetaSeries N u) =
901       thetaSeries N u * thetaLogDerivativeSeries N u := by
902   rw [thetaSeries, thetaLogDerivativeSeries,
903     (PowerSeries.derivative R).leibniz]
904   simp only [smul_eq_mul]
905   rw [
906     derivative_rescale_reciprocalSeries,
907     derivative_rescale_reciprocalSeries]
908   ring
909 
910 @[simp]
911 theorem coeff_thetaLogDerivativeSeries (N k : ℕ) (u : R) :
912     PowerSeries.coeff k (thetaLogDerivativeSeries N u) =
913       (-1 : R) ^ (k + 1) * kappaCoeff N (k + 1) *
914         (u ^ (N * (k + 1)) + u) := by
915   rw [thetaLogDerivativeSeries, map_add, scaledReciprocalLogDerivative,
916     scaledReciprocalLogDerivative, PowerSeries.coeff_C_mul,
917     PowerSeries.coeff_C_mul, PowerSeries.coeff_rescale,
918     PowerSeries.coeff_rescale, PowerSeries.coeff_derivative, kappaCoeff]
919   rw [neg_pow, neg_pow, ← pow_mul]
920   rw [Nat.cast_add, Nat.cast_one]
921   ring
922 
923 /-- Ordinary reduced-variable theta coefficient.  This is the manuscript's
924 `theta_(N,n)(u) = Theta_(N,n)(u)/(Nn)!`. -/
925 def thetaOrdCoeff (N n : ℕ) (u : R) : R :=
926   PowerSeries.coeff n (thetaSeries N u)
927 
928 @[simp]
929 theorem thetaOrdCoeff_zero (N : ℕ) (u : R) :
930     thetaOrdCoeff N 0 u = 1 := by
931   rw [thetaOrdCoeff, thetaSeries, PowerSeries.coeff_mul,
932     Finset.Nat.antidiagonal_zero]
933   simp
934 
935 /-- Theta Newton recurrence in exact antidiagonal indexing.  Replacing
936 `k + 1` by `n` and `p.2 + 1` by `m` gives the displayed manuscript sum
937 from `m = 1` through `m = n`. -/
938 theorem thetaOrdCoeff_newton (N k : ℕ) (u : R) :
939     (k + 1 : R) * thetaOrdCoeff N (k + 1) u =
940       ∑ p ∈ Finset.antidiagonal k,
941         thetaOrdCoeff N p.1 u *
942           ((-1 : R) ^ (p.2 + 1) * kappaCoeff N (p.2 + 1) *
943             (u ^ (N * (p.2 + 1)) + u)) := by
944   have h := congrArg (PowerSeries.coeff (R := R) k)
945     (derivative_thetaSeries (R := R) N u)
946   rw [PowerSeries.coeff_derivative, PowerSeries.coeff_mul] at h
947   simp only [coeff_thetaLogDerivativeSeries] at h
948   simpa [thetaOrdCoeff, mul_comm] using h
949 
950 /-- The normalization of the first logarithmic coefficient used in the
951 closed form for the first theta polynomial. -/
952 theorem factorial_mul_kappaCoeff_one (N : ℕ) :
953     (N.factorial : R) * kappaCoeff N 1 = 1 := by
954   have hlog := mul_derivative_logOf
955     (constantCoeff_reducedDenominator (R := R) N)
956   have hcoeff := congrArg (PowerSeries.coeff (R := R) 0) hlog
957   rw [PowerSeries.coeff_mul, PowerSeries.coeff_derivative] at hcoeff
958   rw [Finset.Nat.antidiagonal_zero] at hcoeff
959   simp at hcoeff
960   have hcoeff' :
961       PowerSeries.coeff 1 (PowerSeries.logOf
962         (reducedDenominator (R := R) N)) =
963         algebraMap ℚ R ((-1 : ℚ) / (N.factorial : ℚ)) := by
964     rw [← hcoeff]
965     rw [← PowerSeries.coeff_zero_eq_constantCoeff,
966       PowerSeries.coeff_derivative]
967     simp
968   rw [kappaCoeff, negativeLogDenominator]
969   simp only [Nat.cast_one, one_mul, map_neg]
970   rw [hcoeff']
971   rw [show (N.factorial : R) =
972     algebraMap ℚ R (N.factorial : ℚ) by simp]
973   rw [← map_neg, ← map_mul]
974   have hfac : (N.factorial : ℚ) ≠ 0 := by positivity
975   field_simp
976   simp
977 
978 /-- The first theta coefficient from Proposition 10.4. -/
979 theorem thetaCoeff_one (N : ℕ) (u : R) :
980     thetaCoeff N 1 u = -(u ^ N + u) := by
981   have hrec := thetaOrdCoeff_newton (R := R) N 0 u
982   simp only [Nat.cast_zero, zero_add, one_mul,
983     Finset.Nat.antidiagonal_zero, Finset.sum_singleton,
984     thetaOrdCoeff_zero, pow_one, Nat.mul_one] at hrec
985   rw [thetaCoeff, blockCoeff]
986   simp only [Nat.mul_one]
987   change (N.factorial : R) * thetaOrdCoeff N 1 u = _
988   rw [hrec]
989   have hk := factorial_mul_kappaCoeff_one (R := R) N
990   calc
991     (N.factorial : R) *
992         ((-1 : R) * kappaCoeff N 1 * (u ^ N + u)) =
993       -((N.factorial : R) * kappaCoeff N 1) * (u ^ N + u) := by ring
994     _ = -(u ^ N + u) := by rw [hk]; ring
995 
996 end ThetaNewton
997 
998 end
999 
1000 end Komorebi.PaperIV

Back to source controls