FormalExponential.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 
6 import Mathlib.Data.Nat.Choose.Cast
7 import Mathlib.RingTheory.PowerSeries.Exp
8 import Mathlib.RingTheory.PowerSeries.Expand
9 
10 /-!
11 # Formal exponential parameter families
12 
13 For a zero-constant formal logarithm `L`, `formalExpFamily L r` is the
14 formal series `exp (r L)`.  This is the branch-free algebraic core of the
15 reciprocal families in Paper IV (where `L = -log Δ_N`).
16 -/
17 
18 namespace Komorebi.PaperIV
19 
20 open scoped PowerSeries
21 
22 noncomputable section
23 
24 variable {R : Type*} [CommRing R] [Algebra ℚ R]
25 
26 /-- Formal `exp (r L)`, implemented by substituting `L` into `exp (rX)`. -/
27 def formalExpFamily (L : R⟦X⟧) (r : R) : R⟦X⟧ :=
28   (PowerSeries.rescale r (PowerSeries.exp R)).subst L
29 
30 theorem formalExpFamily_semigroup {L : R⟦X⟧} (hL : L.constantCoeff = 0) (r s : R) :
31     formalExpFamily L r * formalExpFamily L s = formalExpFamily L (r + s) := by
32   let hsub : PowerSeries.HasSubst L := PowerSeries.HasSubst.of_constantCoeff_zero' hL
33   rw [formalExpFamily, formalExpFamily, formalExpFamily]
34   rw [← PowerSeries.subst_mul hsub]
35   rw [PowerSeries.exp_mul_exp_eq_exp_add]
36 
37 theorem formalExpFamily_zero {L : R⟦X⟧} (hL : L.constantCoeff = 0) :
38     formalExpFamily L 0 = 1 := by
39   rw [formalExpFamily, PowerSeries.rescale_zero_apply]
40   let hsub : PowerSeries.HasSubst L := PowerSeries.HasSubst.of_constantCoeff_zero' hL
41   rw [PowerSeries.constantCoeff_exp]
42   change PowerSeries.subst L (1 : R⟦X⟧) = 1
43   rw [← PowerSeries.coe_substAlgHom hsub, map_one]
44 
45 theorem formalExpFamily_one (L : R⟦X⟧) :
46     formalExpFamily L 1 = (PowerSeries.exp R).subst L := by
47   rw [formalExpFamily, show PowerSeries.rescale 1 (PowerSeries.exp R) = PowerSeries.exp R by simp]
48 
49 /-- Formal derivative of `exp (rX)`. -/
50 theorem derivative_rescale_exp (r : R) :
51     PowerSeries.derivative R (PowerSeries.rescale r (PowerSeries.exp R)) =
52       PowerSeries.C r * PowerSeries.rescale r (PowerSeries.exp R) := by
53   ext n
54   rw [PowerSeries.coeff_derivative, PowerSeries.coeff_C_mul]
55   simp only [PowerSeries.coeff_rescale, PowerSeries.coeff_exp]
56   have hrat :
57       algebraMap ℚ R (1 / ((n + 1).factorial : ℚ)) * (n + 1 : R) =
58         algebraMap ℚ R (1 / (n.factorial : ℚ)) := by
59     have key : (n + 1 : R) = algebraMap ℚ R (n + 1) := by
60       rw [map_add, map_natCast, map_one]
61     rw [key, ← map_mul]
62     congr 1
63     rw [Nat.factorial_succ, Nat.cast_mul, Nat.cast_add_one]
64     field_simp
65   rw [pow_succ]
66   calc
67     r ^ n * r * algebraMap ℚ R (1 / ((n + 1).factorial : ℚ)) * (n + 1 : R) =
68         r * r ^ n *
69           (algebraMap ℚ R (1 / ((n + 1).factorial : ℚ)) * (n + 1 : R)) := by ring
70     _ = r * (r ^ n * algebraMap ℚ R (1 / (n.factorial : ℚ))) := by
71       rw [hrat]
72       ring
73 
74 /-- Chain rule for the formal reciprocal family. -/
75 theorem derivative_formalExpFamily {L : R⟦X⟧} (hL : L.constantCoeff = 0) (r : R) :
76     PowerSeries.derivative R (formalExpFamily L r) =
77       PowerSeries.C r * formalExpFamily L r * PowerSeries.derivative R L := by
78   let hsub : PowerSeries.HasSubst L := PowerSeries.HasSubst.of_constantCoeff_zero' hL
79   rw [formalExpFamily, PowerSeries.derivative_subst hsub, derivative_rescale_exp]
80   rw [PowerSeries.subst_mul hsub, PowerSeries.subst_C]
81   simp only [PowerSeries.C_apply]
82 
83 /-- Newton-type finite coefficient recurrence for `exp (rL)`. -/
84 theorem formalExpFamily_coefficient_recurrence {L : R⟦X⟧}
85     (hL : L.constantCoeff = 0) (r : R) (n : ℕ) :
86     (n + 1 : R) * PowerSeries.coeff (n + 1) (formalExpFamily L r) =
87       r * ∑ p ∈ Finset.antidiagonal n,
88         PowerSeries.coeff p.1 (formalExpFamily L r) *
89           ((p.2 + 1 : R) * PowerSeries.coeff (p.2 + 1) L) := by
90   have hd : PowerSeries.derivative R (formalExpFamily L r) =
91       PowerSeries.C r *
92         (formalExpFamily L r * PowerSeries.derivative R L) := by
93     simpa only [mul_assoc] using derivative_formalExpFamily hL r
94   have h := congrArg (PowerSeries.coeff (R := R) n) hd
95   rw [PowerSeries.coeff_derivative, PowerSeries.coeff_C_mul,
96     PowerSeries.coeff_mul] at h
97   simp_rw [PowerSeries.coeff_derivative] at h
98   simpa [mul_assoc, mul_left_comm, mul_comm] using h
99 
100 /-- Exponential-generating coefficient: `n! [X^n] f`. -/
101 def egfCoeff (n : ℕ) (f : R⟦X⟧) : R :=
102   (n.factorial : R) * PowerSeries.coeff n f
103 
104 omit [Algebra ℚ R] in
105 /-- Coefficient multiplication in exponential-generating normalization. -/
106 theorem egfCoeff_mul (n : ℕ) (f g : R⟦X⟧) :
107     egfCoeff n (f * g) =
108       ∑ p ∈ Finset.antidiagonal n,
109         (n.choose p.1 : R) * egfCoeff p.1 f * egfCoeff p.2 g := by
110   rw [egfCoeff, PowerSeries.coeff_mul, Finset.mul_sum]
111   apply Finset.sum_congr rfl
112   intro p hp
113   have hpadd : p.1 + p.2 = n := Finset.mem_antidiagonal.mp hp
114   have hnat :
115       (p.1 + p.2).choose p.1 * p.1.factorial * p.2.factorial =
116         (p.1 + p.2).factorial := by
117     simpa [Nat.add_comm, Nat.mul_comm, Nat.mul_left_comm, Nat.mul_assoc] using
118       Nat.add_choose_mul_factorial_mul_factorial p.2 p.1
119   have hcast :
120       (((p.1 + p.2).choose p.1 : ℕ) : R) * (p.1.factorial : R) * (p.2.factorial : R) =
121         ((p.1 + p.2).factorial : R) := by
122     simpa only [Nat.cast_mul] using congrArg (fun z : ℕ => (z : R)) hnat
123   rw [← hpadd]
124   rw [egfCoeff, egfCoeff]
125   rw [← hcast]
126   ring
127 
128 /-- Paper IV's block normalization `(N n)! [w^n] f`. -/
129 def blockCoeff (N n : ℕ) (f : R⟦X⟧) : R :=
130   ((N * n).factorial : R) * PowerSeries.coeff n f
131 
132 omit [Algebra ℚ R] in
133 /-- Cauchy multiplication in the block normalization used by `P_{N,n}`. -/
134 theorem blockCoeff_mul (N n : ℕ) (f g : R⟦X⟧) :
135     blockCoeff N n (f * g) =
136       ∑ q ∈ Finset.range (n + 1),
137         ((N * n).choose (N * q) : R) * blockCoeff N q f * blockCoeff N (n - q) g := by
138   rw [blockCoeff, PowerSeries.coeff_mul]
139   rw [Finset.Nat.sum_antidiagonal_eq_sum_range_succ_mk]
140   rw [Finset.mul_sum]
141   apply Finset.sum_congr rfl
142   intro q hq
143   have hqn : q ≤ n := Nat.le_of_lt_succ (Finset.mem_range.mp hq)
144   have hsum : N * q + N * (n - q) = N * n := by
145     rw [← Nat.mul_add, Nat.add_sub_of_le hqn]
146   have hnat :
147       (N * q + N * (n - q)).choose (N * q) * (N * q).factorial *
148           (N * (n - q)).factorial =
149         (N * q + N * (n - q)).factorial := by
150     simpa [Nat.add_comm, Nat.mul_comm, Nat.mul_left_comm, Nat.mul_assoc] using
151       Nat.add_choose_mul_factorial_mul_factorial (N * (n - q)) (N * q)
152   have hcast :
153       (((N * q + N * (n - q)).choose (N * q) : ℕ) : R) *
154           ((N * q).factorial : R) * ((N * (n - q)).factorial : R) =
155         ((N * q + N * (n - q)).factorial : R) := by
156     simpa only [Nat.cast_mul] using congrArg (fun z : ℕ => (z : R)) hnat
157   rw [← hsum]
158   rw [blockCoeff, blockCoeff]
159   rw [← hcast]
160   ring
161 
162 /-- Exact block coefficient convolution for the reciprocal parameter semigroup. -/
163 theorem reciprocal_block_convolution {L : R⟦X⟧} (hL : L.constantCoeff = 0)
164     (N n : ℕ) (r s : R) :
165     blockCoeff N n (formalExpFamily L (r + s)) =
166       ∑ q ∈ Finset.range (n + 1),
167         ((N * n).choose (N * q) : R) *
168           blockCoeff N q (formalExpFamily L r) *
169           blockCoeff N (n - q) (formalExpFamily L s) := by
170   rw [← formalExpFamily_semigroup hL]
171   exact blockCoeff_mul N n _ _
172 
173 /-- Binomial-type normalization of the same parameter semigroup. -/
174 theorem reciprocal_binomial_type {L : R⟦X⟧} (hL : L.constantCoeff = 0)
175     (n : ℕ) (r s : R) :
176     egfCoeff n (formalExpFamily L (r + s)) =
177       ∑ p ∈ Finset.antidiagonal n,
178         (n.choose p.1 : R) * egfCoeff p.1 (formalExpFamily L r) *
179           egfCoeff p.2 (formalExpFamily L s) := by
180   rw [← formalExpFamily_semigroup hL]
181   exact egfCoeff_mul n _ _
182 
183 section Field
184 
185 variable {K : Type*} [Field K]
186 
187 /-- Triangular inverse identity for any unit-constant formal series. -/
188 theorem inverse_coefficient_convolution {D : K⟦X⟧} (hD : D.constantCoeff = 1) (n : ℕ) :
189     (∑ p ∈ Finset.antidiagonal n,
190         PowerSeries.coeff p.1 D * PowerSeries.coeff p.2 D⁻¹) =
191       if n = 0 then 1 else 0 := by
192   have hunit : D.constantCoeff ≠ 0 := by simp [hD]
193   have h := congrArg (PowerSeries.coeff (R := K) n) (PowerSeries.mul_inv_cancel D hunit)
194   rw [PowerSeries.coeff_mul] at h
195   simpa [PowerSeries.coeff_one] using h
196 
197 /-- The inverse's constant coefficient remains one. -/
198 theorem constantCoeff_inverse_of_one {D : K⟦X⟧} (hD : D.constantCoeff = 1) :
199     D⁻¹.constantCoeff = 1 := by
200   rw [PowerSeries.constantCoeff_inv, hD, inv_one]
201 
202 end Field
203 
204 end
205 
206 end Komorebi.PaperIV

Back to source controls