Appell.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 
6 import KomorebiPaperIV.FormalExponential
7 import Mathlib.Algebra.Polynomial.Derivative
8 
9 /-!
10 # Formal Appell systems
11 
12 This file packages the product `exp (rL) exp (xX)` and proves the exact
13 one- and two-parameter coefficient convolution laws.  These are the
14 formal generating-series statements behind Paper IV's block Appell family.
15 -/
16 
17 namespace Komorebi.PaperIV
18 
19 open scoped PowerSeries
20 
21 noncomputable section
22 
23 variable {R : Type*} [CommRing R] [Algebra ℚ R]
24 
25 /-- The Appell generating series `exp (rL) exp (xX)`. -/
26 def appellSeries (L : R⟦X⟧) (r x : R) : R⟦X⟧ :=
27   formalExpFamily L r * PowerSeries.rescale x (PowerSeries.exp R)
28 
29 /-- The Appell polynomial value encoded by the exponential generating series. -/
30 def appellCoeff (L : R⟦X⟧) (r x : R) (m : ℕ) : R :=
31   egfCoeff m (appellSeries L r x)
32 
33 /-- Product law in both the order parameter and the space variable. -/
34 theorem appellSeries_two_parameter {L : R⟦X⟧} (hL : L.constantCoeff = 0)
35     (r s x y : R) :
36     appellSeries L r x * appellSeries L s y = appellSeries L (r + s) (x + y) := by
37   rw [appellSeries, appellSeries, appellSeries]
38   calc
39     (formalExpFamily L r * PowerSeries.rescale x (PowerSeries.exp R)) *
40         (formalExpFamily L s * PowerSeries.rescale y (PowerSeries.exp R)) =
41       (formalExpFamily L r * formalExpFamily L s) *
42         (PowerSeries.rescale x (PowerSeries.exp R) *
43           PowerSeries.rescale y (PowerSeries.exp R)) := by ring
44     _ = formalExpFamily L (r + s) * PowerSeries.rescale (x + y) (PowerSeries.exp R) := by
45       rw [formalExpFamily_semigroup hL, PowerSeries.exp_mul_exp_eq_exp_add]
46 
47 /-- Paper IV's exact two-parameter Appell convolution. -/
48 theorem appell_two_parameter_convolution {L : R⟦X⟧} (hL : L.constantCoeff = 0)
49     (r s x y : R) (m : ℕ) :
50     appellCoeff L (r + s) (x + y) m =
51       ∑ p ∈ Finset.antidiagonal m,
52         (m.choose p.1 : R) * appellCoeff L r x p.1 * appellCoeff L s y p.2 := by
53   unfold appellCoeff
54   rw [← appellSeries_two_parameter hL]
55   exact egfCoeff_mul m _ _
56 
57 /-- The EGF coefficient of `exp (xX)` is `x^m`. -/
58 theorem egfCoeff_rescale_exp (x : R) (m : ℕ) :
59     egfCoeff m (PowerSeries.rescale x (PowerSeries.exp R)) = x ^ m := by
60   rw [egfCoeff, PowerSeries.coeff_rescale, PowerSeries.coeff_exp]
61   have hfac :
62       (m.factorial : R) * algebraMap ℚ R (1 / (m.factorial : ℚ)) = 1 := by
63     have key : (m.factorial : R) = algebraMap ℚ R (m.factorial : ℚ) := by
64       rw [map_natCast]
65     rw [key, ← map_mul]
66     field_simp
67     simp
68   calc
69     (m.factorial : R) * (x ^ m * algebraMap ℚ R (1 / (m.factorial : ℚ))) =
70         x ^ m * ((m.factorial : R) * algebraMap ℚ R (1 / (m.factorial : ℚ))) := by ring
71     _ = x ^ m := by rw [hfac, mul_one]
72 
73 theorem appellCoeff_zero_parameter {L : R⟦X⟧} (hL : L.constantCoeff = 0)
74     (y : R) (m : ℕ) :
75     appellCoeff L 0 y m = y ^ m := by
76   rw [appellCoeff, appellSeries, formalExpFamily_zero hL, one_mul,
77     egfCoeff_rescale_exp]
78 
79 /-- Appell translation/addition law. -/
80 theorem appell_addition {L : R⟦X⟧} (hL : L.constantCoeff = 0)
81     (r x y : R) (m : ℕ) :
82     appellCoeff L r (x + y) m =
83       ∑ p ∈ Finset.antidiagonal m,
84         (m.choose p.1 : R) * appellCoeff L r x p.1 * y ^ p.2 := by
85   have h := appell_two_parameter_convolution hL r 0 x y m
86   simpa [appellCoeff_zero_parameter hL] using h
87 
88 /-- The reciprocal-family coefficients are the Appell values at `x = 0`. -/
89 theorem appellCoeff_at_zero (L : R⟦X⟧) (r : R) (m : ℕ) :
90     appellCoeff L r 0 m = egfCoeff m (formalExpFamily L r) := by
91   rw [appellCoeff, appellSeries]
92   have hexp : PowerSeries.rescale 0 (PowerSeries.exp R) = 1 := by
93     rw [PowerSeries.rescale_zero_apply, PowerSeries.constantCoeff_exp, map_one]
94   rw [hexp, mul_one]
95 
96 /-- Polynomial reconstructed from its Appell base coefficients. -/
97 def appellPolynomial (a : ℕ → R) (m : ℕ) : Polynomial R :=
98   ∑ q ∈ Finset.range (m + 1),
99     Polynomial.C ((m.choose q : R) * a q) * Polynomial.X ^ (m - q)
100 
101 omit [Algebra ℚ R] in
102 /-- The exact Appell lowering law, proved for arbitrary base coefficients. -/
103 theorem derivative_appellPolynomial (a : ℕ → R) (m : ℕ) :
104     Polynomial.derivative (appellPolynomial a (m + 1)) =
105       Polynomial.C (m + 1 : R) * appellPolynomial a m := by
106   rw [appellPolynomial, appellPolynomial]
107   rw [map_sum]
108   rw [Finset.sum_range_succ]
109   simp only [Polynomial.derivative_mul, Polynomial.derivative_C, zero_mul, zero_add,
110     Polynomial.derivative_X_pow]
111   simp only [Nat.sub_self, Nat.cast_zero, map_zero, zero_mul, mul_zero, add_zero]
112   rw [Finset.mul_sum]
113   apply Finset.sum_congr rfl
114   intro q hq
115   have hqm : q ≤ m := Nat.le_of_lt_succ (Finset.mem_range.mp hq)
116   have hsub : m + 1 - q - 1 = m - q := by omega
117   have hnat := Nat.choose_mul_succ_eq m q
118   have hcast :
119       (m.choose q : R) * (m + 1 : R) =
120         ((m + 1).choose q : R) * ((m + 1 - q : ℕ) : R) := by
121     simpa only [Nat.cast_mul, Nat.cast_add, Nat.cast_one, Nat.cast_sub hqm] using
122       congrArg (fun z : ℕ => (z : R)) hnat
123   rw [hsub]
124   simp only [← mul_assoc, ← map_mul]
125   apply congrArg (fun c : R => Polynomial.C c * Polynomial.X ^ (m - q))
126   calc
127     ((m + 1).choose q : R) * a q * ((m + 1 - q : ℕ) : R) =
128         (((m + 1).choose q : R) * ((m + 1 - q : ℕ) : R)) * a q := by ring
129     _ = ((m.choose q : R) * (m + 1 : R)) * a q := by rw [← hcast]
130     _ = (m + 1 : R) * (m.choose q : R) * a q := by ring
131 
132 /-- Paper IV's Appell polynomial attached to `exp (rL)`. -/
133 def formalAppellPolynomial (L : R⟦X⟧) (r : R) (m : ℕ) : Polynomial R :=
134   appellPolynomial (fun q => egfCoeff q (formalExpFamily L r)) m
135 
136 /-- Paper IV's Appell derivative law. -/
137 theorem derivative_formalAppellPolynomial (L : R⟦X⟧) (r : R) (m : ℕ) :
138     Polynomial.derivative (formalAppellPolynomial L r (m + 1)) =
139       Polynomial.C (m + 1 : R) * formalAppellPolynomial L r m := by
140   exact derivative_appellPolynomial _ m
141 
142 theorem eval_formalAppellPolynomial (L : R⟦X⟧) (r x : R) (m : ℕ) :
143     (formalAppellPolynomial L r m).eval x = appellCoeff L r x m := by
144   rw [formalAppellPolynomial, appellPolynomial, Polynomial.eval_finsetSum]
145   unfold appellCoeff appellSeries
146   rw [egfCoeff_mul]
147   rw [Finset.Nat.sum_antidiagonal_eq_sum_range_succ_mk]
148   apply Finset.sum_congr rfl
149   intro q hq
150   simp only [Polynomial.eval_mul, Polynomial.eval_C, Polynomial.eval_pow, Polynomial.eval_X]
151   rw [egfCoeff_rescale_exp]
152 
153 end
154 
155 end Komorebi.PaperIV

Back to source controls