ReciprocalCompletion.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 
6 import KomorebiPaperIV.ReciprocalCore
7 import Mathlib.Data.Nat.Choose.Cast
8 import Mathlib.Algebra.Polynomial.Eval.Defs
9 
10 /-!
11 # Reciprocal and tangent completion certificates
12 
13 This file strengthens the branch-free algebraic coverage of Sections 7 and 8
14 of Paper IV.  All identities are formal-power-series identities.  In
15 particular, the higher Riccati theorem below uses a recursively defined
16 complete differential Bell polynomial and does not appeal to pointwise
17 division or to an analytic logarithm branch.
18 -/
19 
20 namespace Komorebi.PaperIV
21 
22 open scoped PowerSeries
23 
24 noncomputable section
25 
26 section ParameterRecurrence
27 
28 variable {R : Type*} [CommRing R] [Algebra ℚ R]
29 
30 /-- The denominator times the derivative of its reciprocal parameter family
31 satisfies the exact logarithmic-differentiation equation. -/
32 theorem reducedDenominator_reciprocalSeries_differentialEquation
33     (N : ℕ) (r : R) :
34     reducedDenominator N * PowerSeries.derivative R (reciprocalSeries N r) +
35         PowerSeries.C r *
36           (PowerSeries.derivative R (reducedDenominator N) *
37             reciprocalSeries N r) = 0 := by
38   rw [derivative_reciprocalSeries]
39   have hlog := reducedDenominator_mul_reducedTangentSeries (R := R) N
40   rw [reducedTangentSeries] at hlog
41   calc
42     reducedDenominator N *
43           (PowerSeries.C r * reciprocalSeries N r *
44             PowerSeries.derivative R (negativeLogDenominator N)) +
45         PowerSeries.C r *
46           (PowerSeries.derivative R (reducedDenominator N) *
47             reciprocalSeries N r) =
48         PowerSeries.C r * reciprocalSeries N r *
49           (reducedDenominator N *
50             PowerSeries.derivative R (negativeLogDenominator N)) +
51         PowerSeries.C r * reciprocalSeries N r *
52           PowerSeries.derivative R (reducedDenominator N) := by ring
53     _ = 0 := by rw [hlog]; ring
54 
55 /-- Coefficient form of the parameter recurrence before factorial
56 rescaling.  Multiplying this identity by `N (N(n+1)-1)!` gives the two
57 binomial sums displayed in Theorem 7.3. -/
58 theorem reciprocalOrdCoeff_parameter_equation (N n : ℕ) (r : R) :
59     (∑ p ∈ Finset.antidiagonal n,
60         PowerSeries.coeff p.1 (reducedDenominator (R := R) N) *
61           ((p.2 + 1 : R) * reciprocalOrdCoeff N (p.2 + 1) r)) +
62       r * ∑ p ∈ Finset.antidiagonal n,
63         ((p.1 + 1 : R) *
64           PowerSeries.coeff (p.1 + 1) (reducedDenominator (R := R) N)) *
65             reciprocalOrdCoeff N p.2 r = 0 := by
66   have h := congrArg (PowerSeries.coeff (R := R) n)
67     (reducedDenominator_reciprocalSeries_differentialEquation (R := R) N r)
68   rw [map_add, PowerSeries.coeff_mul, PowerSeries.coeff_C_mul,
69     PowerSeries.coeff_mul] at h
70   simp only [map_zero] at h
71   simp_rw [PowerSeries.coeff_derivative] at h
72   simpa [reciprocalOrdCoeff, mul_assoc, mul_left_comm, mul_comm] using h
73 
74 end ParameterRecurrence
75 
76 section ExactParameterRecurrence
77 
78 variable {K : Type*} [Field K] [CharZero K]
79 
80 private theorem scaled_reducedDenominator_term
81     {N n k : ℕ} (hN : 0 < N) (hk : k < n) :
82     (((N * n - 1).factorial : K) * (N : K)) *
83         (PowerSeries.coeff k (reducedDenominator (R := K) N) *
84           (n - k : K)) =
85       (-1 : K) ^ k * ((N * n - 1).choose (N * k) : K) *
86         ((N * (n - k)).factorial : K) := by
87   have hkn : k ≤ n := Nat.le_of_lt hk
88   have hNkn : 0 < N * (n - k) := Nat.mul_pos hN (Nat.sub_pos_of_lt hk)
89   have hmul_lt : N * k < N * n := (Nat.mul_lt_mul_left hN).2 hk
90   have hmul_le : N * k ≤ N * n := Nat.le_of_lt hmul_lt
91   have hchoose : N * k ≤ N * n - 1 := by omega
92   have hsub : N * n - 1 - N * k = N * (n - k) - 1 := by
93     rw [Nat.mul_sub_left_distrib]
94     omega
95   have hfac :
96       ((N * (n - k)).factorial : K) =
97         (N * (n - k) : K) * ((N * (n - k) - 1).factorial : K) := by
98     exact_mod_cast (Nat.mul_factorial_pred hNkn.ne').symm
99   have hfacNk : ((N * k).factorial : K) ≠ 0 := by
100     exact_mod_cast (N * k).factorial_pos.ne'
101   have hfacRest : ((N * (n - k) - 1).factorial : K) ≠ 0 := by
102     exact_mod_cast (N * (n - k) - 1).factorial_pos.ne'
103   rw [coeff_reducedDenominator]
104   rw [eq_ratCast]
105   push_cast
106   have hsign : ((↑((-1 : ℚ) ^ k) : K)) = (-1 : K) ^ k := by norm_cast
107   rw [hsign]
108   rw [Nat.cast_choose K hchoose, hsub, hfac]
109   field_simp [hfacNk, hfacRest]
110 
111 private theorem scaled_derivative_reducedDenominator_term
112     {N n k : ℕ} (hN : 0 < N) (hk : 0 < k) (hkn : k ≤ n) :
113     (((N * n - 1).factorial : K) * (N : K)) *
114         ((k : K) *
115           PowerSeries.coeff k (reducedDenominator (R := K) N)) =
116       (-1 : K) ^ k * ((N * n - 1).choose (N * k - 1) : K) *
117         ((N * (n - k)).factorial : K) := by
118   have hNk : 0 < N * k := Nat.mul_pos hN hk
119   have hmul_le : N * k ≤ N * n := Nat.mul_le_mul_left N hkn
120   have hchoose : N * k - 1 ≤ N * n - 1 := by omega
121   have hsub : N * n - 1 - (N * k - 1) = N * (n - k) := by
122     rw [Nat.mul_sub_left_distrib]
123     omega
124   have hfac :
125       ((N * k).factorial : K) =
126         (N * k : K) * ((N * k - 1).factorial : K) := by
127     exact_mod_cast (Nat.mul_factorial_pred hNk.ne').symm
128   have hfacNk : ((N * k).factorial : K) ≠ 0 := by
129     exact_mod_cast (N * k).factorial_pos.ne'
130   have hfacPred : ((N * k - 1).factorial : K) ≠ 0 := by
131     exact_mod_cast (N * k - 1).factorial_pos.ne'
132   have hfacRest : ((N * (n - k)).factorial : K) ≠ 0 := by
133     exact_mod_cast (N * (n - k)).factorial_pos.ne'
134   have hN0 : (N : K) ≠ 0 := by exact_mod_cast hN.ne'
135   have hk0 : (k : K) ≠ 0 := by exact_mod_cast hk.ne'
136   rw [coeff_reducedDenominator]
137   rw [eq_ratCast]
138   push_cast
139   have hsign : ((↑((-1 : ℚ) ^ k) : K)) = (-1 : K) ^ k := by norm_cast
140   rw [hsign]
141   rw [Nat.cast_choose K hchoose, hsub, hfac]
142   field_simp [hfacNk, hfacPred, hfacRest, hN0, hk0]
143 
144 private theorem scaled_reciprocalOrdCoeff_term
145     {N n k : ℕ} (hN : 0 < N) (hk : k < n) (r : K) :
146     (((N * n - 1).factorial : K) * (N : K)) *
147         (PowerSeries.coeff k (reducedDenominator (R := K) N) *
148           ((n - k : K) * reciprocalOrdCoeff N (n - k) r)) =
149       (-1 : K) ^ k * ((N * n - 1).choose (N * k) : K) *
150         reciprocalCoeff N (n - k) r := by
151   rw [reciprocalCoeff, blockCoeff, reciprocalOrdCoeff]
152   have hs := scaled_reducedDenominator_term (K := K) hN hk
153   calc
154     (((N * n - 1).factorial : K) * (N : K)) *
155         (PowerSeries.coeff k (reducedDenominator (R := K) N) *
156           ((n - k : K) *
157             PowerSeries.coeff (n - k) (reciprocalSeries N r))) =
158       ((((N * n - 1).factorial : K) * (N : K)) *
159         (PowerSeries.coeff k (reducedDenominator (R := K) N) *
160           (n - k : K))) *
161             PowerSeries.coeff (n - k) (reciprocalSeries N r) := by ring
162     _ = ((-1 : K) ^ k * ((N * n - 1).choose (N * k) : K) *
163         ((N * (n - k)).factorial : K)) *
164           PowerSeries.coeff (n - k) (reciprocalSeries N r) := by rw [hs]
165     _ = (-1 : K) ^ k * ((N * n - 1).choose (N * k) : K) *
166         (((N * (n - k)).factorial : K) *
167           PowerSeries.coeff (n - k) (reciprocalSeries N r)) := by ring
168 
169 private theorem scaled_derivative_reciprocalOrdCoeff_term
170     {N n k : ℕ} (hN : 0 < N) (hk : 0 < k) (hkn : k ≤ n) (r : K) :
171     (((N * n - 1).factorial : K) * (N : K)) *
172         (((k : K) *
173           PowerSeries.coeff k (reducedDenominator (R := K) N)) *
174             reciprocalOrdCoeff N (n - k) r) =
175       (-1 : K) ^ k * ((N * n - 1).choose (N * k - 1) : K) *
176         reciprocalCoeff N (n - k) r := by
177   rw [reciprocalCoeff, blockCoeff, reciprocalOrdCoeff]
178   have hs := scaled_derivative_reducedDenominator_term (K := K) hN hk hkn
179   calc
180     (((N * n - 1).factorial : K) * (N : K)) *
181         (((k : K) *
182           PowerSeries.coeff k (reducedDenominator (R := K) N)) *
183             PowerSeries.coeff (n - k) (reciprocalSeries N r)) =
184       ((((N * n - 1).factorial : K) * (N : K)) *
185         ((k : K) *
186           PowerSeries.coeff k (reducedDenominator (R := K) N))) *
187             PowerSeries.coeff (n - k) (reciprocalSeries N r) := by ring
188     _ = ((-1 : K) ^ k * ((N * n - 1).choose (N * k - 1) : K) *
189         ((N * (n - k)).factorial : K)) *
190           PowerSeries.coeff (n - k) (reciprocalSeries N r) := by rw [hs]
191     _ = (-1 : K) ^ k * ((N * n - 1).choose (N * k - 1) : K) *
192         (((N * (n - k)).factorial : K) *
193           PowerSeries.coeff (n - k) (reciprocalSeries N r)) := by ring
194 
195 /-- Exact factorially normalized coefficient equation behind Theorem 7.3.
196 The second sum uses the reindexing `k = q + 1`, so all displayed indices are
197 total natural-number expressions. -/
198 theorem reciprocalCoeff_parameter_equation
199     {N n : ℕ} (hN : 0 < N) (hn : 0 < n) (r : K) :
200     (∑ k ∈ Finset.range n,
201         (-1 : K) ^ k * ((N * n - 1).choose (N * k) : K) *
202           reciprocalCoeff N (n - k) r) +
203       r * ∑ q ∈ Finset.range n,
204         (-1 : K) ^ (q + 1) *
205           ((N * n - 1).choose (N * (q + 1) - 1) : K) *
206             reciprocalCoeff N (n - (q + 1)) r = 0 := by
207   have hraw := reciprocalOrdCoeff_parameter_equation (R := K) N (n - 1) r
208   rw [Finset.Nat.sum_antidiagonal_eq_sum_range_succ_mk,
209     Finset.Nat.sum_antidiagonal_eq_sum_range_succ_mk] at hraw
210   simp only [Nat.succ_eq_add_one] at hraw
211   have hpred : n - 1 + 1 = n := Nat.sub_add_cancel (Nat.one_le_iff_ne_zero.mpr hn.ne')
212   have hfirst :
213       (∑ k ∈ Finset.range n,
214           PowerSeries.coeff k (reducedDenominator (R := K) N) *
215             ((n - k : K) * reciprocalOrdCoeff N (n - k) r)) =
216         ∑ k ∈ Finset.range (n - 1 + 1),
217           PowerSeries.coeff k (reducedDenominator (R := K) N) *
218             ((((n - 1 - k : ℕ) : K) + 1) *
219               reciprocalOrdCoeff N (n - 1 - k + 1) r) := by
220     rw [hpred]
221     apply Finset.sum_congr rfl
222     intro k hk
223     have hklt : k < n := Finset.mem_range.mp hk
224     have hidx : n - 1 - k + 1 = n - k := by omega
225     have hcast : (((n - 1 - k : ℕ) : K) + 1) = (n - k : K) := by
226       have hc := congrArg (fun m : ℕ => (m : K)) hidx
227       simpa only [Nat.cast_add, Nat.cast_one,
228         Nat.cast_sub (Nat.le_of_lt hklt)] using hc
229     rw [hcast, hidx]
230   have hsecond :
231       (∑ q ∈ Finset.range n,
232           ((q + 1 : K) *
233             PowerSeries.coeff (q + 1) (reducedDenominator (R := K) N)) *
234               reciprocalOrdCoeff N (n - (q + 1)) r) =
235         ∑ q ∈ Finset.range (n - 1 + 1),
236           ((q + 1 : K) *
237             PowerSeries.coeff (q + 1) (reducedDenominator (R := K) N)) *
238               reciprocalOrdCoeff N (n - 1 - q) r := by
239     rw [hpred]
240     apply Finset.sum_congr rfl
241     intro q hq
242     have hqlt : q < n := Finset.mem_range.mp hq
243     have hidx : n - 1 - q = n - (q + 1) := by omega
244     rw [hidx]
245   rw [← hfirst, ← hsecond] at hraw
246   let scale : K := ((N * n - 1).factorial : K) * (N : K)
247   have hscaled :
248       scale *
249         ((∑ k ∈ Finset.range n,
250             PowerSeries.coeff k (reducedDenominator (R := K) N) *
251               ((n - k : K) * reciprocalOrdCoeff N (n - k) r)) +
252           r * ∑ q ∈ Finset.range n,
253             ((q + 1 : K) *
254               PowerSeries.coeff (q + 1) (reducedDenominator (R := K) N)) *
255                 reciprocalOrdCoeff N (n - (q + 1)) r) = 0 := by
256     rw [hraw, mul_zero]
257   have hfirstScaled :
258       scale *
259           (∑ k ∈ Finset.range n,
260             PowerSeries.coeff k (reducedDenominator (R := K) N) *
261               ((n - k : K) * reciprocalOrdCoeff N (n - k) r)) =
262         ∑ k ∈ Finset.range n,
263           (-1 : K) ^ k * ((N * n - 1).choose (N * k) : K) *
264             reciprocalCoeff N (n - k) r := by
265     rw [Finset.mul_sum]
266     apply Finset.sum_congr rfl
267     intro k hk
268     exact scaled_reciprocalOrdCoeff_term (K := K) hN (Finset.mem_range.mp hk) r
269   have hsecondScaled :
270       scale *
271           (∑ q ∈ Finset.range n,
272             ((q + 1 : K) *
273               PowerSeries.coeff (q + 1) (reducedDenominator (R := K) N)) *
274                 reciprocalOrdCoeff N (n - (q + 1)) r) =
275         ∑ q ∈ Finset.range n,
276           (-1 : K) ^ (q + 1) *
277             ((N * n - 1).choose (N * (q + 1) - 1) : K) *
278               reciprocalCoeff N (n - (q + 1)) r := by
279     rw [Finset.mul_sum]
280     apply Finset.sum_congr rfl
281     intro q hq
282     have hqlt : q < n := Finset.mem_range.mp hq
283     simpa [scale, Nat.succ_eq_add_one] using
284       (scaled_derivative_reciprocalOrdCoeff_term
285         (K := K) hN (Nat.zero_lt_succ q) (Nat.succ_le_iff.mpr hqlt) r)
286   calc
287     (∑ k ∈ Finset.range n,
288         (-1 : K) ^ k * ((N * n - 1).choose (N * k) : K) *
289           reciprocalCoeff N (n - k) r) +
290       r * ∑ q ∈ Finset.range n,
291         (-1 : K) ^ (q + 1) *
292           ((N * n - 1).choose (N * (q + 1) - 1) : K) *
293             reciprocalCoeff N (n - (q + 1)) r =
294       scale *
295         ((∑ k ∈ Finset.range n,
296             PowerSeries.coeff k (reducedDenominator (R := K) N) *
297               ((n - k : K) * reciprocalOrdCoeff N (n - k) r)) +
298           r * ∑ q ∈ Finset.range n,
299             ((q + 1 : K) *
300               PowerSeries.coeff (q + 1) (reducedDenominator (R := K) N)) *
301                 reciprocalOrdCoeff N (n - (q + 1)) r) := by
302         rw [mul_add, hfirstScaled]
303         rw [show scale *
304             (r * ∑ q ∈ Finset.range n,
305               ((q + 1 : K) *
306                 PowerSeries.coeff (q + 1) (reducedDenominator (R := K) N)) *
307                   reciprocalOrdCoeff N (n - (q + 1)) r) =
308             r * (scale * ∑ q ∈ Finset.range n,
309               ((q + 1 : K) *
310                 PowerSeries.coeff (q + 1) (reducedDenominator (R := K) N)) *
311                   reciprocalOrdCoeff N (n - (q + 1)) r) by ring,
312           hsecondScaled]
313     _ = 0 := hscaled
314 
315 /-- The solved parameter recurrence, exactly matching Theorem 7.3 after the
316 harmless reindexing `k = q + 1` in the second finite sum. -/
317 theorem reciprocalCoeff_parameter_recurrence
318     {N n : ℕ} (hN : 0 < N) (hn : 0 < n) (r : K) :
319     reciprocalCoeff N n r =
320       -(∑ k ∈ Finset.Ico 1 n,
321           (-1 : K) ^ k * ((N * n - 1).choose (N * k) : K) *
322             reciprocalCoeff N (n - k) r) -
323       r * ∑ q ∈ Finset.range n,
324         (-1 : K) ^ (q + 1) *
325           ((N * n - 1).choose (N * (q + 1) - 1) : K) *
326             reciprocalCoeff N (n - (q + 1)) r := by
327   let f : ℕ → K := fun k =>
328     (-1 : K) ^ k * ((N * n - 1).choose (N * k) : K) *
329       reciprocalCoeff N (n - k) r
330   have hsplit :
331       (∑ k ∈ Finset.range n, f k) =
332         reciprocalCoeff N n r + ∑ k ∈ Finset.Ico 1 n, f k := by
333     have hi := Finset.sum_Ico_eq_sub f (show 1 ≤ n by omega)
334     simp only [Finset.sum_range_one] at hi
335     have hf0 : f 0 = reciprocalCoeff N n r := by simp [f]
336     rw [hi, hf0]
337     ring
338   have h := reciprocalCoeff_parameter_equation (K := K) hN hn r
339   change (∑ k ∈ Finset.range n, f k) + _ = 0 at h
340   rw [hsplit] at h
341   change reciprocalCoeff N n r =
342       -(∑ k ∈ Finset.Ico 1 n, f k) - _
343   linear_combination h
344 
345 @[simp]
346 theorem reciprocalCoeff_block_zero (N : ℕ) (r : K) :
347     reciprocalCoeff N 0 r = 1 := by
348   simp [reciprocalCoeff, blockCoeff]
349 
350 /-- The first reciprocal polynomial: `P_(N,1)(r) = r`. -/
351 theorem reciprocalCoeff_one {N : ℕ} (hN : 0 < N) (r : K) :
352     reciprocalCoeff N 1 r = r := by
353   have h := reciprocalCoeff_parameter_recurrence
354     (K := K) hN (n := 1) (by omega) r
355   simpa using h
356 
357 /-- A recurrence-normal-form certificate for the second reciprocal
358 polynomial.  The two adjacent binomial coefficients combine to the compact
359 formula printed in Corollary 7.7. -/
360 theorem reciprocalCoeff_two_recurrence_form
361     {N : ℕ} (hN : 0 < N) (r : K) :
362     reciprocalCoeff N 2 r =
363       ((2 * N - 1).choose N : K) * r +
364         r * (((2 * N - 1).choose (N - 1) : K) * r - 1) := by
365   have h := reciprocalCoeff_parameter_recurrence
366     (K := K) hN (n := 2) (by omega) r
367   norm_num [Finset.sum_range_succ, Finset.sum_Ico_eq_sub,
368     reciprocalCoeff_one hN] at h
369   rw [Nat.mul_comm N 2] at h
370   linear_combination h
371 
372 /-- A recurrence-normal-form certificate for the third reciprocal
373 polynomial.  Substitution of the preceding second-degree formula and the
374 standard adjacent-binomial identities yields the compact form in
375 Corollary 7.7. -/
376 theorem reciprocalCoeff_three_recurrence_form
377     {N : ℕ} (hN : 0 < N) (r : K) :
378     reciprocalCoeff N 3 r =
379       ((3 * N - 1).choose N : K) * reciprocalCoeff N 2 r -
380         ((3 * N - 1).choose (2 * N) : K) * r +
381       r * (((3 * N - 1).choose (N - 1) : K) * reciprocalCoeff N 2 r -
382         ((3 * N - 1).choose (2 * N - 1) : K) * r + 1) := by
383   have h := reciprocalCoeff_parameter_recurrence
384     (K := K) hN (n := 3) (by omega) r
385   norm_num [Finset.sum_range_succ, Finset.sum_Ico_eq_sub,
386     reciprocalCoeff_one hN] at h
387   rw [Nat.mul_comm N 3, Nat.mul_comm N 2] at h
388   linear_combination h
389 
390 end ExactParameterRecurrence
391 
392 section PolynomialFactor
393 
394 /-- The universal reciprocal coefficient obtained by taking the parameter to
395 be the indeterminate `X` over `ℚ`.  This is a literal polynomial lift of
396 `P_(N,n)(r)`, not merely a function-valued surrogate. -/
397 def reciprocalCoeffPolynomial (N n : ℕ) : Polynomial ℚ :=
398   reciprocalCoeff (R := Polynomial ℚ) N n Polynomial.X
399 
400 /-- Corollary 7.8 in the universal polynomial ring: every positive-index
401 reciprocal coefficient has the factor `X`. -/
402 theorem X_dvd_reciprocalCoeffPolynomial
403     (N : ℕ) {n : ℕ} (hn : 0 < n) :
404     Polynomial.X ∣ reciprocalCoeffPolynomial N n := by
405   have hpred : n - 1 + 1 = n := Nat.sub_add_cancel (Nat.one_le_iff_ne_zero.mpr hn.ne')
406   have hnewton := reciprocalOrdCoeff_newton
407     (R := Polynomial ℚ) N Polynomial.X (n - 1)
408   have hcast : (((n - 1 : ℕ) : Polynomial ℚ) + 1) =
409       (n : Polynomial ℚ) := by
410     have hc := congrArg (fun m : ℕ => (m : Polynomial ℚ)) hpred
411     simpa only [Nat.cast_add, Nat.cast_one] using hc
412   rw [hpred, hcast] at hnewton
413   have hdivScaled :
414       Polynomial.X ∣ (n : Polynomial ℚ) *
415         reciprocalOrdCoeff N n Polynomial.X := by
416     rw [hnewton]
417     exact dvd_mul_right Polynomial.X _
418   have hnq : (n : ℚ) ≠ 0 := by exact_mod_cast hn.ne'
419   have huq : IsUnit (n : ℚ) := isUnit_iff_ne_zero.mpr hnq
420   have hu : IsUnit (n : Polynomial ℚ) := by
421     change IsUnit (Polynomial.C (n : ℚ))
422     exact huq.map Polynomial.C
423   have hcoeff :
424       Polynomial.X ∣ reciprocalOrdCoeff N n Polynomial.X :=
425     hu.dvd_mul_left.mp hdivScaled
426   rw [reciprocalCoeffPolynomial, reciprocalCoeff, blockCoeff]
427   exact dvd_mul_of_dvd_right hcoeff _
428 
429 /-- Equivalent root-at-zero certificate for the universal polynomial. -/
430 theorem coeff_zero_reciprocalCoeffPolynomial
431     (N : ℕ) {n : ℕ} (hn : 0 < n) :
432     (reciprocalCoeffPolynomial N n).coeff 0 = 0 := by
433   exact Polynomial.X_dvd_iff.mp
434     (X_dvd_reciprocalCoeffPolynomial N hn)
435 
436 end PolynomialFactor
437 
438 section TransferTangent
439 
440 variable {R : Type*} [CommRing R] [Algebra ℚ R]
441 
442 /-- The manuscript's factorially normalized `z`-variable tangent
443 coefficient `T_N(n)`. -/
444 def transferTangentCoeff (N n : ℕ) : R :=
445   (N : R) * ((N * n + N - 1).factorial : R) * kappaCoeff N (n + 1)
446 
447 /-- Exact named form of Proposition 8.2. -/
448 theorem transferTangentCoeff_eq_kappa (N n : ℕ) :
449     transferTangentCoeff (R := R) N n =
450       (N : R) * ((N * n + N - 1).factorial : R) * kappaCoeff N (n + 1) := by
451   rfl
452 
453 section Field
454 
455 variable {K : Type*} [Field K] [CharZero K]
456 
457 private theorem scaled_tangent_convolution_term
458     {N n k : ℕ} (hN : 0 < N) (hk : k ≤ n) :
459     ((N : K) * ((N * n + N - 1).factorial : K)) *
460         (PowerSeries.coeff k (reducedDenominator (R := K) N) *
461           kappaCoeff N (n - k + 1)) =
462       (-1 : K) ^ k *
463         ((N * n + N - 1).choose (N * k) : K) *
464           transferTangentCoeff N (n - k) := by
465   have hmul : N * k ≤ N * n := Nat.mul_le_mul_left N hk
466   have hchoose : N * k ≤ N * n + N - 1 := by omega
467   have hsub :
468       N * n + N - 1 - N * k = N * (n - k) + N - 1 := by
469     rw [Nat.mul_sub_left_distrib]
470     omega
471   have hfacK : ((N * k).factorial : K) ≠ 0 := by
472     exact_mod_cast (N * k).factorial_pos.ne'
473   have hfacRest : ((N * (n - k) + N - 1).factorial : K) ≠ 0 := by
474     exact_mod_cast (N * (n - k) + N - 1).factorial_pos.ne'
475   rw [coeff_reducedDenominator, eq_ratCast]
476   push_cast
477   have hsign : ((↑((-1 : ℚ) ^ k) : K)) = (-1 : K) ^ k := by norm_cast
478   rw [hsign, Nat.cast_choose K hchoose, hsub]
479   rw [transferTangentCoeff]
480   field_simp [hfacK, hfacRest]
481 
482 private theorem scaled_tangent_convolution_rhs
483     (N n : ℕ) (hN : 0 < N) :
484     ((N : K) * ((N * n + N - 1).factorial : K)) *
485         (-(PowerSeries.coeff (n + 1) (reducedDenominator (R := K) N) *
486           (n + 1 : K))) = (-1 : K) ^ n := by
487   have hpos : 0 < N * (n + 1) := Nat.mul_pos hN (Nat.succ_pos n)
488   have htop : N * n + N - 1 = N * (n + 1) - 1 := by
489     rw [Nat.mul_add, Nat.mul_one]
490   have hfac :
491       ((N * (n + 1)).factorial : K) =
492         (N * (n + 1) : K) * ((N * (n + 1) - 1).factorial : K) := by
493     exact_mod_cast (Nat.mul_factorial_pred hpos.ne').symm
494   have hfacTop : ((N * (n + 1) - 1).factorial : K) ≠ 0 := by
495     exact_mod_cast (N * (n + 1) - 1).factorial_pos.ne'
496   have hN0 : (N : K) ≠ 0 := by exact_mod_cast hN.ne'
497   have hn0 : (n + 1 : K) ≠ 0 := by
498     exact_mod_cast (Nat.succ_ne_zero n)
499   rw [coeff_reducedDenominator, eq_ratCast]
500   push_cast
501   have hsign : ((↑((-1 : ℚ) ^ (n + 1)) : K)) =
502       (-1 : K) ^ (n + 1) := by norm_cast
503   rw [hsign, htop, hfac]
504   field_simp [hfacTop, hN0, hn0]
505   rw [pow_succ]
506   ring
507 
508 /-- Fully normalized convolution equation for the named `z`-variable tangent
509 coefficients. -/
510 theorem transferTangentCoeff_convolution
511     (N n : ℕ) (hN : 0 < N) :
512     (∑ k ∈ Finset.range (n + 1),
513         (-1 : K) ^ k *
514           ((N * n + N - 1).choose (N * k) : K) *
515             transferTangentCoeff N (n - k)) = (-1 : K) ^ n := by
516   have hraw := reducedTangent_coefficient_convolution (R := K) N n
517   rw [Finset.Nat.sum_antidiagonal_eq_sum_range_succ_mk] at hraw
518   let scale : K := (N : K) * ((N * n + N - 1).factorial : K)
519   have hscaled := congrArg (fun x : K => scale * x) hraw
520   have hleft :
521       scale *
522           (∑ k ∈ Finset.range (n + 1),
523             PowerSeries.coeff k (reducedDenominator (R := K) N) *
524               kappaCoeff N (n - k + 1)) =
525         ∑ k ∈ Finset.range (n + 1),
526           (-1 : K) ^ k *
527             ((N * n + N - 1).choose (N * k) : K) *
528               transferTangentCoeff N (n - k) := by
529     rw [Finset.mul_sum]
530     apply Finset.sum_congr rfl
531     intro k hk
532     exact scaled_tangent_convolution_term
533       (K := K) hN (Nat.le_of_lt_succ (Finset.mem_range.mp hk))
534   rw [hleft, scaled_tangent_convolution_rhs (K := K) N n hN] at hscaled
535   exact hscaled
536 
537 /-- The exact tangent recurrence of Theorem 8.3. -/
538 theorem transferTangentCoeff_recurrence
539     (N n : ℕ) (hN : 0 < N) :
540     transferTangentCoeff (R := K) N n =
541       (-1 : K) ^ n -
542         ∑ k ∈ Finset.Ico 1 (n + 1),
543           (-1 : K) ^ k *
544             ((N * n + N - 1).choose (N * k) : K) *
545               transferTangentCoeff N (n - k) := by
546   let f : ℕ → K := fun k =>
547     (-1 : K) ^ k *
548       ((N * n + N - 1).choose (N * k) : K) *
549         transferTangentCoeff N (n - k)
550   have hsplit :
551       (∑ k ∈ Finset.range (n + 1), f k) =
552         transferTangentCoeff N n + ∑ k ∈ Finset.Ico 1 (n + 1), f k := by
553     have hi := Finset.sum_Ico_eq_sub f (show 1 ≤ n + 1 by omega)
554     simp only [Finset.sum_range_one] at hi
555     have hf0 : f 0 = transferTangentCoeff N n := by simp [f]
556     rw [hi, hf0]
557     ring
558   have h := transferTangentCoeff_convolution (K := K) N n hN
559   change (∑ k ∈ Finset.range (n + 1), f k) = (-1 : K) ^ n at h
560   rw [hsplit] at h
561   change transferTangentCoeff N n =
562       (-1 : K) ^ n - ∑ k ∈ Finset.Ico 1 (n + 1), f k
563   linear_combination h
564 
565 @[simp]
566 theorem transferTangentCoeff_zero (N : ℕ) (hN : 0 < N) :
567     transferTangentCoeff (R := K) N 0 = 1 := by
568   simpa using transferTangentCoeff_recurrence (K := K) N 0 hN
569 
570 end Field
571 
572 end TransferTangent
573 
574 section FormalRiccati
575 
576 variable {K : Type*} [Field K] [CharZero K]
577 
578 /-- Formal transfer tangent `-D_N'/D_N` in the full `z` variable. -/
579 def formalTransferTangent (N : ℕ) : K⟦X⟧ :=
580   -PowerSeries.derivative K (signedSection (R := K) N 0) *
581     (signedSection (R := K) N 0)⁻¹
582 
583 /-- The complete differential Bell polynomial evaluated at the successive
584 derivatives of a single logarithmic derivative.  Recursively,
585 `Y_0 = 1` and `Y_(n+1) = Y_n' + g Y_n`. -/
586 def differentialBellSeries (g : K⟦X⟧) : ℕ → K⟦X⟧
587   | 0 => 1
588   | n + 1 =>
589       PowerSeries.derivative K (differentialBellSeries g n) +
590         g * differentialBellSeries g n
591 
592 omit [CharZero K] in
593 @[simp]
594 theorem differentialBellSeries_zero (g : K⟦X⟧) :
595     differentialBellSeries g 0 = 1 := rfl
596 
597 omit [CharZero K] in
598 @[simp]
599 theorem differentialBellSeries_succ (g : K⟦X⟧) (n : ℕ) :
600     differentialBellSeries g (n + 1) =
601       PowerSeries.derivative K (differentialBellSeries g n) +
602         g * differentialBellSeries g n := rfl
603 
604 omit [CharZero K] in
605 /-- Recursive differential Bell polynomials encode every iterated derivative
606 of a formal series satisfying `f' = g f`. -/
607 theorem iterate_derivative_eq_differentialBellSeries_mul
608     (f g : K⟦X⟧)
609     (hfg : PowerSeries.derivative K f = g * f) (n : ℕ) :
610     (PowerSeries.derivative K)^[n] f = differentialBellSeries g n * f := by
611   induction n with
612   | zero => simp
613   | succ n ih =>
614       rw [Function.iterate_succ_apply', ih, Derivation.leibniz, hfg]
615       simp only [smul_eq_mul]
616       rw [differentialBellSeries_succ]
617       ring
618 
619 /-- The formal tangent is exactly the negative logarithmic derivative: this
620 version avoids any analytic choice of logarithm. -/
621 theorem derivative_signedSection_zero_eq_neg_formalTransferTangent_mul
622     {N : ℕ} (hN : 0 < N) :
623     PowerSeries.derivative K (signedSection (R := K) N 0) =
624       -formalTransferTangent N * signedSection (R := K) N 0 := by
625   have hconst :
626       PowerSeries.constantCoeff (signedSection (R := K) N 0) = 1 := by
627     simpa using
628       (constantCoeff_iterate_derivative_signedSection
629         (R := K) (j := 0) (k := 0) hN hN)
630   have hunit :
631       PowerSeries.constantCoeff (signedSection (R := K) N 0) ≠ 0 := by
632     simp [hconst]
633   rw [formalTransferTangent]
634   simp only [neg_mul, neg_neg]
635   rw [mul_assoc, PowerSeries.inv_mul_cancel _ hunit, mul_one]
636 
637 /-- Formal scalar higher Riccati identity (Theorem 8.5).  It is the exact
638 power-series analogue of
639 `Y_N(-T,-T',..., -T^(N-1)) = -1`. -/
640 theorem differentialBellSeries_neg_formalTransferTangent_eq_neg_one
641     {N : ℕ} (hN : 0 < N) :
642     differentialBellSeries (-formalTransferTangent (K := K) N) N = -1 := by
643   let D : K⟦X⟧ := signedSection (R := K) N 0
644   have hconst : D.constantCoeff = 1 := by
645     simpa [D] using
646       (constantCoeff_iterate_derivative_signedSection
647         (R := K) (j := 0) (k := 0) hN hN)
648   have hD : D ≠ 0 := by
649     intro hzero
650     rw [hzero, map_zero] at hconst
651     exact zero_ne_one hconst
652   have hbell := iterate_derivative_eq_differentialBellSeries_mul
653     D (-formalTransferTangent (K := K) N)
654       (by
655         simpa [D] using
656           (derivative_signedSection_zero_eq_neg_formalTransferTangent_mul
657             (K := K) hN)) N
658   have hcycle := iterate_derivative_signedSection (R := K) (j := 0) hN
659   rw [show D = signedSection (R := K) N 0 by rfl, hcycle] at hbell
660   apply mul_right_cancel₀ hD
661   simpa [D, mul_assoc] using hbell.symm
662 
663 end FormalRiccati
664 
665 end
666 
667 end Komorebi.PaperIV

Back to source controls