English
The k-th iterated derivative commutes with infinite sums over integers: iteratedDerivWithin_k of the sum over n in Z equals the sum over n of iteratedDerivWithin_k applied to each summand.
Русский
Порядок взятия кратной производной и бесконечной суммы над n ∈ ℤ можно поменять: производная по k на сумму эквивалентна сумме по n от производных по k каждого слагаемого.
LaTeX
$$$\operatorname{iteratedDerivWithin}_k\left(\sum_{n∈\mathbb{Z}} f(n)\right) = \sum_{n∈\mathbb{Z}} \operatorname{iteratedDerivWithin}_k f(n).$$$
Lean4
/-- The infinte sum of `k`-th iterated derivative of the complex exponential multiplied by a
function that grows polynomially is absolutely and uniformly convergent. -/
theorem summableLocallyUniformlyOn_iteratedDerivWithin_smul_cexp (k l : ℕ) {f : ℕ → ℂ} {p : ℝ} (hp : 0 < p)
(hf : f =O[atTop] (fun n ↦ ((n ^ l) : ℝ))) :
SummableLocallyUniformlyOn (fun n ↦ (f n) • iteratedDerivWithin k (fun z ↦ cexp (2 * π * I * z / p) ^ n) ℍₒ) ℍₒ :=
by
apply SummableLocallyUniformlyOn_of_locally_bounded isOpen_upperHalfPlaneSet
intro K hK hKc
have : CompactSpace K := isCompact_univ_iff.mp (isCompact_iff_isCompact_univ.mp hKc)
let c : ContinuousMap K ℂ := ⟨fun r : K ↦ Complex.exp (2 * π * I * r / p), by fun_prop⟩
let r : ℝ := ‖mkOfCompact c‖
have hr : ‖r‖ < 1 :=
by
simp only [norm_norm, r, norm_lt_iff_of_compact Real.zero_lt_one, mkOfCompact_apply, ContinuousMap.coe_mk, c]
intro x
have h1 : cexp (2 * π * I * (x / p)) = cexp (2 * π * I * x / p) := by ring_nf
simpa using h1 ▸ norm_exp_two_pi_I_lt_one ⟨((x : ℂ) / p), by aesop⟩
refine
⟨_, by
simpa using
(summable_norm_mul_geometric_of_norm_lt_one' hr (Asymptotics.isBigO_norm_left.mpr (aux_IsBigO_mul k l p hf))),
fun n z hz ↦ ?_⟩
have h0 := pow_le_pow_left₀ (norm_nonneg _) (norm_coe_le_norm (mkOfCompact c) ⟨z, hz⟩) n
simp only [norm_mkOfCompact, mkOfCompact_apply, ContinuousMap.coe_mk, ← exp_nsmul', Pi.smul_apply,
iteratedDerivWithin_cexp_aux k n p isOpen_upperHalfPlaneSet (hK hz), smul_eq_mul, norm_mul, norm_pow,
Complex.norm_div, norm_ofNat, norm_real, Real.norm_eq_abs, norm_I, mul_one, norm_natCast, abs_norm, ge_iff_le, r,
c] at *
rw [← mul_assoc]
gcongr
convert h0
rw [← norm_pow, ← exp_nsmul']
