ThetaZeroBell.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIV.ZeroMomentCoefficients
6 
7 namespace Komorebi.PaperIV
8 noncomputable section
9 
10 theorem powerSeries_linear_ode_unique {f g H : PowerSeries ℂ}
11     (h0 : f.constantCoeff = g.constantCoeff)
12     (hf : PowerSeries.derivative ℂ f = f * H)
13     (hg : PowerSeries.derivative ℂ g = g * H) : f = g := by
14   ext n
15   induction n using Nat.strong_induction_on with
16   | h n ih =>
17       cases n with
18       | zero => simpa only [PowerSeries.coeff_zero_eq_constantCoeff] using h0
19       | succ n =>
20           have he : PowerSeries.coeff n (PowerSeries.derivative ℂ f) =
21               PowerSeries.coeff n (PowerSeries.derivative ℂ g) := by
22             rw [hf, hg, PowerSeries.coeff_mul, PowerSeries.coeff_mul]
23             apply Finset.sum_congr rfl
24             intro p hp
25             rw [ih p.1 (by have := Finset.mem_antidiagonal.mp hp; omega)]
26           simp only [PowerSeries.coeff_derivative] at he
27           exact mul_right_cancel₀ (by exact_mod_cast Nat.succ_ne_zero n : (n + 1 : ℂ) ≠ 0) he
28 
29 def thetaZeroBellInput (N : ℕ) (u : ℂ) : PowerSeries ℂ :=
30   bellInput (fun m => ((m - 1).factorial : ℂ) * (-1 : ℂ) ^ m *
31     zeroPowerSum (entireReducedDenominator N) m * (u ^ (N * m) + u))
32 
33 theorem thetaZeroBellInput_derivative {N : ℕ} (hN : 2 ≤ N) (u : ℂ) :
34     PowerSeries.derivative ℂ (thetaZeroBellInput N u) = thetaLogDerivativeSeries N u := by
35   ext n
36   rw [PowerSeries.coeff_derivative, coeff_thetaLogDerivativeSeries,
37     kappaCoeff_eq_zeroPowerSum hN (by omega)]
38   simp only [thetaZeroBellInput, bellInput, PowerSeries.coeff_mk, Nat.succ_ne_zero, ↓reduceIte, Nat.add_sub_cancel, Nat.factorial_succ,
39     Nat.cast_mul, Nat.cast_add, Nat.cast_one]
40   have hn : (n.factorial : ℂ) ≠ 0 := by exact_mod_cast n.factorial_ne_zero
41   have hn1 : (n + 1 : ℂ) ≠ 0 := by exact_mod_cast Nat.succ_ne_zero n
42   field_simp
43 
44 theorem thetaSeries_eq_zero_bell_exp {N : ℕ} (hN : 2 ≤ N) (u : ℂ) :
45     thetaSeries N u = (PowerSeries.exp ℂ).subst (thetaZeroBellInput N u) := by
46   have hB0 : (thetaZeroBellInput N u).constantCoeff = 0 := constantCoeff_bellInput _
47   have hB : PowerSeries.HasSubst (thetaZeroBellInput N u) := PowerSeries.HasSubst.of_constantCoeff_zero' hB0
48   apply powerSeries_linear_ode_unique (H := thetaLogDerivativeSeries N u)
49   · have h0 := thetaOrdCoeff_zero (R := ℂ) N u
50     rw [thetaOrdCoeff, PowerSeries.coeff_zero_eq_constantCoeff] at h0
51     rw [h0]
52     change 1 = MvPowerSeries.constantCoeff ((PowerSeries.exp ℂ).subst (thetaZeroBellInput N u))
53     rw [PowerSeries.constantCoeff_subst_of_constantCoeff_zero hB0]
54     simp
55   · exact derivative_thetaSeries N u
56   · rw [PowerSeries.derivative_subst hB,
57       PowerSeries.derivative_exp, thetaZeroBellInput_derivative hN]
58 
59 /-- Proposition 12.8, with the signed zero sums in the displayed Bell input. -/
60 theorem thetaCoeff_zero_sum_bell {N : ℕ} (hN : 2 ≤ N) (n : ℕ) (u : ℂ) :
61     thetaCoeff N n u = ((N * n).factorial : ℂ) / (n.factorial : ℂ) *
62       completeExponentialBell n (fun m => ((m - 1).factorial : ℂ) * (-1 : ℂ) ^ m *
63         zeroPowerSum (entireReducedDenominator N) m * (u ^ (N * m) + u)) := by
64   rw [thetaCoeff, blockCoeff, thetaSeries_eq_zero_bell_exp hN, completeExponentialBell]
65   have hn : (n.factorial : ℂ) ≠ 0 := by exact_mod_cast n.factorial_ne_zero
66   dsimp [thetaZeroBellInput]
67   field_simp
68 
69 end
70 end Komorebi.PaperIV

Back to source controls