English
For every natural k and z in the upper half-plane, the k-th iterated derivative of the exponential power series agrees with the sum over n of the k-th iterated derivative of exp(2π i s)^n evaluated at s = z.
Русский
Для каждого натурального k и z в верхней полуплоскости равенство для k-й итерационной производной степенного ряда экспоненты: сумма по n от k-й производной эксп(2π i s)^n при s = z.
LaTeX
$$$\operatorname{iteratedDerivWithin}_k \left( z \mapsto \sum_n (e^{2\pi i z})^n \right) = \sum_n \operatorname{iteratedDerivWithin}_k \left( s \mapsto (e^{2\pi i s})^n \right),$$$
Lean4
/-- This is a version of `summableLocallyUniformlyOn_iteratedDerivWithin_smul_cexp` for level one
and q-expansion coefficients all `1`. -/
theorem summableLocallyUniformlyOn_iteratedDerivWithin_cexp (k : ℕ) :
SummableLocallyUniformlyOn (fun n ↦ iteratedDerivWithin k (fun z ↦ cexp (2 * π * I * z) ^ n) ℍₒ) ℍₒ :=
by
have h0 : (fun n : ℕ ↦ (1 : ℂ)) =O[atTop] fun n ↦ ((n ^ 1) : ℝ) :=
by
simp only [Asymptotics.isBigO_iff, norm_one, norm_pow, Real.norm_natCast, eventually_atTop, ge_iff_le]
exact ⟨1, 1, fun b hb ↦ by norm_cast; simp [hb]⟩
simpa using summableLocallyUniformlyOn_iteratedDerivWithin_smul_cexp k 1 (p := 1) (by norm_num) h0
