AlgebraicCompletion.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 
6 import KomorebiPaperIV.Appell
7 import Mathlib.Data.Nat.Choose.Cast
8 import Mathlib.Algebra.Polynomial.BigOperators
9 import Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
10 import Mathlib.Algebra.Polynomial.HasseDeriv
11 import Mathlib.RingTheory.PowerSeries.Expand
12 import Mathlib.Algebra.Polynomial.Div
13 
14 /-!
15 # Algebraic completion for Paper IV
16 
17 This file records branch-free algebraic statements from Paper IV that were not
18 part of the initial checkpoint.  In particular, it proves the exact
19 factorial-rescaled triangular inverse system used for the normalized residue
20 sections.
21 -/
22 
23 namespace Komorebi.PaperIV
24 
25 open scoped PowerSeries
26 
27 noncomputable section
28 
29 section ResidueInverse
30 
31 variable {K : Type*} [Field K] [CharZero K]
32 
33 /-- The reduced normalized residue section
34 `j! * sum_n X^n / (N n + j)!`. -/
35 def normalizedResidueSection (N j : ℕ) : K⟦X⟧ :=
36   PowerSeries.mk fun n =>
37     (j.factorial : K) / ((N * n + j).factorial : K)
38 
39 omit [CharZero K] in
40 @[simp]
41 theorem coeff_normalizedResidueSection (N j n : ℕ) :
42     PowerSeries.coeff n (normalizedResidueSection (K := K) N j) =
43       (j.factorial : K) / ((N * n + j).factorial : K) := by
44   simp [normalizedResidueSection]
45 
46 @[simp]
47 theorem constantCoeff_normalizedResidueSection (N j : ℕ) :
48     (normalizedResidueSection (K := K) N j).constantCoeff = 1 := by
49   rw [← PowerSeries.coeff_zero_eq_constantCoeff]
50   rw [coeff_normalizedResidueSection]
51   have hj : (j.factorial : K) ≠ 0 := by
52     exact_mod_cast j.factorial_pos.ne'
53   simpa using div_self hj
54 
55 /-- Paper IV's coefficient `C_{N,j}(n)`, including its `(N n)!` scaling. -/
56 def residueInverseCoeff (N j n : ℕ) : K :=
57   ((N * n).factorial : K) *
58     PowerSeries.coeff n (normalizedResidueSection (K := K) N j)⁻¹
59 
60 /-- The exact factorial-rescaled triangular inverse identity of Theorem 9.2. -/
61 theorem residueInverseCoeff_triangular (N j n : ℕ) :
62     (∑ q ∈ Finset.range (n + 1),
63         ((N * n + j).choose (N * q) : K) *
64           residueInverseCoeff (K := K) N j q) =
65       if n = 0 then 1 else 0 := by
66   let D : K⟦X⟧ := normalizedResidueSection (K := K) N j
67   have hD : D.constantCoeff = 1 := by
68     simp [D]
69   have hunit : D.constantCoeff ≠ 0 := by simp [hD]
70   have hinv : D⁻¹ * D = 1 := by
71     rw [mul_comm]
72     exact PowerSeries.mul_inv_cancel D hunit
73   have hcoeff := congrArg (PowerSeries.coeff (R := K) n) hinv
74   rw [PowerSeries.coeff_mul,
75     Finset.Nat.sum_antidiagonal_eq_sum_range_succ_mk] at hcoeff
76   simp only [PowerSeries.coeff_one] at hcoeff
77   let scale : K := ((N * n + j).factorial : K) / (j.factorial : K)
78   have hterm (q : ℕ) (hq : q ∈ Finset.range (n + 1)) :
79       scale *
80           (PowerSeries.coeff q D⁻¹ * PowerSeries.coeff (n - q) D) =
81         ((N * n + j).choose (N * q) : K) *
82           residueInverseCoeff (K := K) N j q := by
83     have hqn : q ≤ n := Nat.le_of_lt_succ (Finset.mem_range.mp hq)
84     have hmul : N * q ≤ N * n := Nat.mul_le_mul_left N hqn
85     have hle : N * q ≤ N * n + j := hmul.trans (Nat.le_add_right _ _)
86     have hsplit : N * q + N * (n - q) = N * n := by
87       rw [← Nat.mul_add, Nat.add_sub_of_le hqn]
88     have hsub : N * n + j - N * q = N * (n - q) + j := by omega
89     have hfacj : (j.factorial : K) ≠ 0 := by
90       exact_mod_cast j.factorial_pos.ne'
91     have hfacq : ((N * q).factorial : K) ≠ 0 := by
92       exact_mod_cast (N * q).factorial_pos.ne'
93     have hfacrest : ((N * (n - q) + j).factorial : K) ≠ 0 := by
94       exact_mod_cast (N * (n - q) + j).factorial_pos.ne'
95     rw [show PowerSeries.coeff (n - q) D =
96         (j.factorial : K) / ((N * (n - q) + j).factorial : K) by
97       simp [D]]
98     rw [residueInverseCoeff]
99     rw [Nat.cast_choose K hle, hsub]
100     dsimp [scale]
101     field_simp
102     ring
103   calc
104     (∑ q ∈ Finset.range (n + 1),
105         ((N * n + j).choose (N * q) : K) *
106           residueInverseCoeff (K := K) N j q) =
107         ∑ q ∈ Finset.range (n + 1),
108           scale * (PowerSeries.coeff q D⁻¹ * PowerSeries.coeff (n - q) D) := by
109             apply Finset.sum_congr rfl
110             intro q hq
111             exact (hterm q hq).symm
112     _ = scale *
113         ∑ q ∈ Finset.range (n + 1),
114           PowerSeries.coeff q D⁻¹ * PowerSeries.coeff (n - q) D := by
115             rw [Finset.mul_sum]
116     _ = scale * (if n = 0 then 1 else 0) := by rw [hcoeff]
117     _ = if n = 0 then 1 else 0 := by
118       by_cases hn : n = 0
119       · subst n
120         have hj : (j.factorial : K) ≠ 0 := by
121           exact_mod_cast j.factorial_pos.ne'
122         simp [scale, hj]
123       · simp [hn]
124 
125 @[simp]
126 theorem residueInverseCoeff_zero (N j : ℕ) :
127     residueInverseCoeff (K := K) N j 0 = 1 := by
128   simpa using residueInverseCoeff_triangular (K := K) N j 0
129 
130 /-- The solved triangular recurrence displayed in Theorem 9.2. -/
131 theorem residueInverseCoeff_recurrence (N j n : ℕ) (hn : 0 < n) :
132     residueInverseCoeff (K := K) N j n =
133       -(∑ q ∈ Finset.range n,
134           ((N * n + j).choose (N * q) : K) *
135             residueInverseCoeff (K := K) N j q) /
136         ((N * n + j).choose (N * n) : K) := by
137   have hsum := residueInverseCoeff_triangular (K := K) N j n
138   have hn0 : n ≠ 0 := Nat.ne_of_gt hn
139   simp only [hn0, ↓reduceIte] at hsum
140   rw [Finset.sum_range_succ] at hsum
141   have hle : N * n ≤ N * n + j := by omega
142   have hden : ((N * n + j).choose (N * n) : K) ≠ 0 := by
143     exact_mod_cast (Nat.choose_pos hle).ne'
144   apply (eq_div_iff hden).2
145   linear_combination hsum
146 
147 end ResidueInverse
148 
149 section SparseAppell
150 
151 variable {R : Type*} [CommRing R]
152 
153 /-- Inflate block coefficients to the full EGF index set, putting zero away
154 from indices divisible by `N`. -/
155 def blockCoefficientSequence (N : ℕ) (c : ℕ → R) (q : ℕ) : R :=
156   if N ∣ q then c (q / N) else 0
157 
158 @[simp]
159 theorem blockCoefficientSequence_mul (N : ℕ) (hN : 0 < N)
160     (c : ℕ → R) (n : ℕ) :
161     blockCoefficientSequence N c (N * n) = c n := by
162   simp [blockCoefficientSequence, Nat.mul_div_cancel_left n hN]
163 
164 /-- A sparse Appell polynomial contains only the coefficient indices in the
165 specified congruence block. -/
166 theorem appellPolynomial_eq_sparse_sum (N m : ℕ) (c : ℕ → R) :
167     appellPolynomial (blockCoefficientSequence N c) m =
168       ∑ q ∈ (Finset.range (m + 1)).filter (fun q => N ∣ q),
169         Polynomial.C
170             ((m.choose q : R) * blockCoefficientSequence N c q) *
171           Polynomial.X ^ (m - q) := by
172   rw [appellPolynomial]
173   symm
174   refine Finset.sum_subset (Finset.filter_subset _ _) ?_
175   intro q hq hqfilter
176   have hnot : ¬N ∣ q := by
177     intro hdiv
178     apply hqfilter
179     exact Finset.mem_filter.mpr ⟨hq, hdiv⟩
180   rw [blockCoefficientSequence]
181   simp [hnot]
182 
183 /-- Proposition 9.7 in exact block form: only the indices `N n ≤ m`
184 contribute to the Appell polynomial. -/
185 theorem appellPolynomial_eq_block_sum (N m : ℕ) (hN : 0 < N)
186     (c : ℕ → R) :
187     appellPolynomial (blockCoefficientSequence N c) m =
188       ∑ n ∈ Finset.range (m / N + 1),
189         Polynomial.C ((m.choose (N * n) : R) * c n) *
190           Polynomial.X ^ (m - N * n) := by
191   rw [appellPolynomial_eq_sparse_sum]
192   symm
193   refine Finset.sum_bij (fun n _ => N * n) ?_ ?_ ?_ ?_
194   · intro n hn
195     apply Finset.mem_filter.mpr
196     constructor
197     · apply Finset.mem_range.mpr
198       have hnle : n ≤ m / N := Nat.le_of_lt_succ (Finset.mem_range.mp hn)
199       have hmul : n * N ≤ m := (Nat.le_div_iff_mul_le hN).mp hnle
200       simpa [Nat.mul_comm] using Nat.lt_succ_of_le hmul
201     · exact dvd_mul_right N n
202   · intro n₁ _ n₂ _ heq
203     exact Nat.mul_left_cancel hN heq
204   · intro q hq
205     rcases Finset.mem_filter.mp hq with ⟨hqrange, hdiv⟩
206     rcases hdiv with ⟨n, rfl⟩
207     refine ⟨n, ?_, rfl⟩
208     apply Finset.mem_range.mpr
209     rw [Nat.lt_add_one_iff]
210     apply (Nat.le_div_iff_mul_le hN).mpr
211     have hNm : N * n ≤ m := Nat.le_of_lt_succ (Finset.mem_range.mp hqrange)
212     simpa [Nat.mul_comm] using hNm
213   · intro n hn
214     simp [blockCoefficientSequence_mul N hN]
215 
216 /-- Every Appell polynomial with unit zeroth base coefficient is monic of its
217 displayed degree. -/
218 theorem appellPolynomial_isMonicOfDegree [Nontrivial R] (a : ℕ → R) (m : ℕ)
219     (ha : a 0 = 1) :
220     Polynomial.IsMonicOfDegree (appellPolynomial a m) m := by
221   rw [Polynomial.isMonicOfDegree_iff]
222   constructor
223   · rw [appellPolynomial]
224     apply Polynomial.natDegree_sum_le_of_forall_le
225     intro q hq
226     exact (Polynomial.natDegree_C_mul_X_pow_le _ _).trans (Nat.sub_le m q)
227   · rw [appellPolynomial, Polynomial.finsetSum_coeff]
228     rw [Finset.sum_eq_single 0]
229     · simp [ha]
230     · intro q hq hq0
231       rw [Polynomial.coeff_C_mul, Polynomial.coeff_X_pow]
232       have hqm : q ≤ m := Nat.le_of_lt_succ (Finset.mem_range.mp hq)
233       have hne : m ≠ m - q := by omega
234       simp [hne]
235     · simp
236 
237 /-- The block form of Proposition 9.7 is monic when its zeroth reciprocal
238 coefficient is one. -/
239 theorem blockAppellPolynomial_isMonicOfDegree [Nontrivial R]
240     (N m : ℕ) (c : ℕ → R) (hc : c 0 = 1) :
241     Polynomial.IsMonicOfDegree
242       (appellPolynomial (blockCoefficientSequence N c) m) m := by
243   apply appellPolynomial_isMonicOfDegree
244   simp [blockCoefficientSequence, hc]
245 
246 /-- Corollary 9.10: block-supported Appell polynomials transform by the
247 character `omega^m` whenever `omega^N = 1`. -/
248 theorem eval_appellPolynomial_block_covariance (N m : ℕ) (hN : 0 < N)
249     (c : ℕ → R) (omega x : R) (homega : omega ^ N = 1) :
250     (appellPolynomial (blockCoefficientSequence N c) m).eval (omega * x) =
251       omega ^ m *
252         (appellPolynomial (blockCoefficientSequence N c) m).eval x := by
253   rw [appellPolynomial_eq_block_sum N m hN c,
254     Polynomial.eval_finsetSum, Polynomial.eval_finsetSum]
255   rw [Finset.mul_sum]
256   apply Finset.sum_congr rfl
257   intro n hn
258   have hnle : n ≤ m / N := Nat.le_of_lt_succ (Finset.mem_range.mp hn)
259   have hmul : N * n ≤ m := by
260     have : n * N ≤ m := (Nat.le_div_iff_mul_le hN).mp hnle
261     simpa [Nat.mul_comm] using this
262   simp only [Polynomial.eval_mul, Polynomial.eval_C, Polynomial.eval_pow,
263     Polynomial.eval_X]
264   rw [mul_pow]
265   have hpow : omega ^ (m - N * n) = omega ^ m := by
266     calc
267       omega ^ (m - N * n) = omega ^ (m - N * n) * 1 := by rw [mul_one]
268       _ = omega ^ (m - N * n) * (omega ^ N) ^ n := by rw [homega, one_pow]
269       _ = omega ^ (m - N * n) * omega ^ (N * n) := by rw [pow_mul]
270       _ = omega ^ (m - N * n + N * n) := by rw [pow_add]
271       _ = omega ^ m := by rw [Nat.sub_add_cancel hmul]
272   rw [hpow]
273   ring
274 
275 section ResidueAppell
276 
277 variable {K : Type*} [Field K] [CharZero K]
278 
279 omit [CharZero K] in
280 /-- Proposition 9.7 specialized to the reciprocal of the normalized residue
281 section from Theorem 9.2. -/
282 theorem residueAppellPolynomial_explicit (N j m : ℕ) (hN : 0 < N) :
283     appellPolynomial
284         (blockCoefficientSequence N
285           (residueInverseCoeff (K := K) N j)) m =
286       ∑ n ∈ Finset.range (m / N + 1),
287         Polynomial.C
288             ((m.choose (N * n) : K) * residueInverseCoeff (K := K) N j n) *
289           Polynomial.X ^ (m - N * n) := by
290   exact appellPolynomial_eq_block_sum N m hN _
291 
292 /-- The residue-section Appell polynomial is monic of degree `m`. -/
293 theorem residueAppellPolynomial_isMonicOfDegree (N j m : ℕ) (_hN : 0 < N) :
294     Polynomial.IsMonicOfDegree
295       (appellPolynomial
296         (blockCoefficientSequence N
297           (residueInverseCoeff (K := K) N j)) m) m := by
298   exact blockAppellPolynomial_isMonicOfDegree N m _
299     (residueInverseCoeff_zero (K := K) N j)
300 
301 omit [CharZero K] in
302 /-- Corollary 9.10 specialized to the normalized residue-section reciprocal. -/
303 theorem eval_residueAppellPolynomial_covariance (N j m : ℕ) (hN : 0 < N)
304     (omega x : K) (homega : omega ^ N = 1) :
305     (appellPolynomial
306         (blockCoefficientSequence N
307           (residueInverseCoeff (K := K) N j)) m).eval (omega * x) =
308       omega ^ m *
309         (appellPolynomial
310           (blockCoefficientSequence N
311             (residueInverseCoeff (K := K) N j)) m).eval x := by
312   exact eval_appellPolynomial_block_covariance N m hN _ omega x homega
313 
314 end ResidueAppell
315 
316 end SparseAppell
317 
318 section DifferentialOperator
319 
320 variable {R : Type*} [CommRing R]
321 
322 /-- The finite action of a constant-coefficient formal symbol whose exponential
323 generating coefficients are `a`.  Hasse derivatives encode the factors
324 `derivative^q / q!` without any characteristic-zero assumption. -/
325 def egfConstantCoeffAction (a : ℕ → R) (f : Polynomial R) : Polynomial R :=
326   ∑ q ∈ Finset.range (f.natDegree + 1),
327     Polynomial.C (a q) * Polynomial.hasseDeriv q f
328 
329 /-- The first operator identity of Proposition 9.9: applying the formal symbol
330 with EGF coefficients `a` to `X^m` gives its Appell polynomial exactly. -/
331 theorem egfConstantCoeffAction_X_pow [Nontrivial R] (a : ℕ → R) (m : ℕ) :
332     egfConstantCoeffAction a (Polynomial.X ^ m) = appellPolynomial a m := by
333   rw [egfConstantCoeffAction, Polynomial.natDegree_X_pow, appellPolynomial]
334   apply Finset.sum_congr rfl
335   intro q _hq
336   rw [Polynomial.X_pow_eq_monomial, Polynomial.hasseDeriv_monomial]
337   simp only [mul_one, ← Polynomial.C_mul_X_pow_eq_monomial]
338   rw [← mul_assoc, ← map_mul]
339   congr 1
340   exact congrArg Polynomial.C (mul_comm (a q) (m.choose q : R))
341 
342 /-- Proposition 9.9 specialized to the normalized residue-section reciprocal:
343 the corresponding finite constant-coefficient action produces the Appell
344 polynomial from `X^m`. -/
345 theorem egfConstantCoeffAction_residue_X_pow
346     {K : Type*} [Field K] [CharZero K] (N j m : ℕ) :
347     egfConstantCoeffAction
348         (blockCoefficientSequence N
349           (residueInverseCoeff (K := K) N j))
350         (Polynomial.X ^ m) =
351       appellPolynomial
352         (blockCoefficientSequence N
353           (residueInverseCoeff (K := K) N j)) m := by
354   exact egfConstantCoeffAction_X_pow _ m
355 
356 end DifferentialOperator
357 
358 section TruncatedOperatorInversion
359 
360 variable {S : Type*} [CommRing S]
361 
362 /-- Polynomial differential symbols evaluated at the formal derivative. -/
363 def polynomialDifferentialEval :
364     Polynomial S →+* Module.End S (Polynomial S) :=
365   Polynomial.eval₂RingHom' (algebraMap S (Module.End S (Polynomial S)))
366     Polynomial.derivative
367     fun a => Algebra.commute_algebraMap_left a Polynomial.derivative
368 
369 @[simp]
370 theorem polynomialDifferentialEval_X :
371     polynomialDifferentialEval (S := S) Polynomial.X = Polynomial.derivative := by
372   simp [polynomialDifferentialEval]
373 
374 /-- The degree-`d` truncation of a formal differential symbol. -/
375 def truncatedDifferentialOperator (d : ℕ) (A : S⟦X⟧) :
376     Module.End S (Polynomial S) :=
377   polynomialDifferentialEval (PowerSeries.trunc (d + 1) A)
378 
379 theorem coeff_trunc_mul_trunc_of_lt (A B : S⟦X⟧) {d q : ℕ} (hq : q < d + 1) :
380     (PowerSeries.trunc (d + 1) A * PowerSeries.trunc (d + 1) B).coeff q =
381       PowerSeries.coeff q (A * B) := by
382   rw [Polynomial.coeff_mul, PowerSeries.coeff_mul]
383   apply Finset.sum_congr rfl
384   intro p hp
385   have hpadd : p.1 + p.2 = q := Finset.mem_antidiagonal.mp hp
386   have hp1 : p.1 < d + 1 := by omega
387   have hp2 : p.2 < d + 1 := by omega
388   simp only [PowerSeries.coeff_trunc, hp1, hp2, ↓reduceIte]
389 
390 /-- If two formal symbols multiply to one, their degree-`d` truncations multiply
391 to one modulo `X^(d+1)`. -/
392 theorem X_pow_dvd_trunc_mul_trunc_sub_one {A B : S⟦X⟧} (d : ℕ)
393     (hAB : A * B = 1) :
394     Polynomial.X ^ (d + 1) ∣
395       PowerSeries.trunc (d + 1) A * PowerSeries.trunc (d + 1) B - 1 := by
396   rw [Polynomial.X_pow_dvd_iff]
397   intro q hq
398   rw [Polynomial.coeff_sub, coeff_trunc_mul_trunc_of_lt A B hq]
399   rw [hAB]
400   simp [PowerSeries.coeff_one, Polynomial.coeff_one]
401 
402 /-- Constant-coefficient operator inversion on polynomials: if `A * B = 1`,
403 then the degree-`d` truncations of `A(∂)` and `B(∂)` compose to the
404 identity on every polynomial of degree at most `d`. -/
405 theorem truncatedDifferentialOperator_mul_apply_of_natDegree_le
406     {A B : S⟦X⟧} {d : ℕ} {p : Polynomial S} (hp : p.natDegree ≤ d)
407     (hAB : A * B = 1) :
408     (truncatedDifferentialOperator d A * truncatedDifferentialOperator d B) p = p := by
409   obtain ⟨Q, hQ⟩ := X_pow_dvd_trunc_mul_trunc_sub_one (S := S) d hAB
410   have hQ' :
411       PowerSeries.trunc (d + 1) A * PowerSeries.trunc (d + 1) B - 1 =
412         Q * Polynomial.X ^ (d + 1) := by
413     rw [hQ, mul_comm]
414   have heval := congrArg polynomialDifferentialEval hQ'
415   simp only [map_sub, map_mul, map_pow, map_one] at heval
416   have hderiv :
417       ((Polynomial.derivative : Module.End S (Polynomial S)) ^ (d + 1)) p = 0 := by
418     rw [Module.End.pow_apply]
419     exact Polynomial.iterate_derivative_eq_zero
420       (lt_of_le_of_lt hp (Nat.lt_succ_self d))
421   have happ := congrArg (fun T : Module.End S (Polynomial S) => T p) heval
422   rw [LinearMap.sub_apply, Module.End.mul_apply, Module.End.mul_apply,
423     Module.End.one_apply] at happ
424   rw [polynomialDifferentialEval_X] at happ
425   change
426     polynomialDifferentialEval (PowerSeries.trunc (d + 1) A)
427           (polynomialDifferentialEval (PowerSeries.trunc (d + 1) B) p) - p =
428       polynomialDifferentialEval Q
429         (((Polynomial.derivative : Module.End S (Polynomial S)) ^ (d + 1)) p) at happ
430   rw [hderiv, LinearMap.map_zero] at happ
431   change
432     (polynomialDifferentialEval (PowerSeries.trunc (d + 1) A) *
433       polynomialDifferentialEval (PowerSeries.trunc (d + 1) B)) p = p
434   exact sub_eq_zero.mp happ
435 
436 /-- The `r = 1` inverse-operator relation of Proposition 9.9 for a normalized
437 residue section.  `expand N` performs the substitution `w = z^N`; hence the
438 two displayed symbols are `Φₙ,ⱼ(z^N)` and its reciprocal. -/
439 theorem truncatedDifferentialOperator_normalizedResidueSection_inverse
440     {K : Type*} [Field K] [CharZero K] (N j d : ℕ) (hN : 0 < N)
441     {p : Polynomial K} (hp : p.natDegree ≤ d) :
442     (truncatedDifferentialOperator d
443         (PowerSeries.expand N hN.ne'
444           (normalizedResidueSection (K := K) N j)) *
445       truncatedDifferentialOperator d
446         (PowerSeries.expand N hN.ne'
447           (normalizedResidueSection (K := K) N j)⁻¹)) p = p := by
448   apply truncatedDifferentialOperator_mul_apply_of_natDegree_le hp
449   rw [← map_mul]
450   rw [PowerSeries.mul_inv_cancel]
451   · exact map_one _
452   · simp
453 
454 end TruncatedOperatorInversion
455 
456 end
457 
458 end Komorebi.PaperIV

Back to source controls