Termwise differentiation of series

hasDerivAt_tsum_fun differentiates a series of functions termwise on an open set, given locally-uniform summable bounds on the derivatives on compact subsets. Mathlib's derivWithin_tsum (in Mathlib.Topology.Algebra.InfiniteSum.TsumUniformlyOn) is the derivWithin version of this; the HasDerivAt form proved here is not yet in Mathlib.

iter_deriv_comp_bound3 provides the summable geometric bounds on compact subsets of the upper half-plane for (2π n)^k · ‖exp (2π i n z)‖, used for the q-expansion derivative bounds in FG.lean.

noncomputable def cts_exp_two_pi_n (K : Set ℂ) : C(↑K, ℂ)

Equations

• cts_exp_two_pi_n K = { toFun := fun (r : ↑K) => Complex.exp (2 * ↑Real.pi * Complex.I * ↑r), continuous_toFun := ⋯ }

theorem hasDerivAt_tsum_fun {α : Type u_1} (f : α → ℂ → ℂ) {s : Set ℂ} (hs : IsOpen s) (x : ℂ) (hx : x ∈ s) (hf : ∀ y ∈ s, Summable fun (n : α) => f n y) (hu : ∀ K ⊆ s, IsCompact K → ∃ (u : α → ℝ), Summable u ∧ ∀ (n : α) (k : ↑K), ‖derivWithin (f n) s ↑k‖ ≤ u n) (hf2 : ∀ (n : α) (r : ↑s), DifferentiableAt ℂ (f n) ↑r) : HasDerivAt (fun (z : ℂ) => ∑' (n : α), f n z) (∑' (n : α), derivWithin (fun (z : ℂ) => f n z) s x) x

theorem iter_deriv_comp_bound3 (K : Set ℂ) (hK1 : K ⊆ {z : ℂ | 0 < z.im}) (hK2 : IsCompact K) (k : ℕ) : ∃ (u : ℕ → ℝ), Summable u ∧ ∀ (n : ℕ) (r : ↑K), (2 * |Real.pi| * ↑n) ^ k * ‖Complex.exp (2 * ↑Real.pi * Complex.I * ↑n * ↑r)‖ ≤ u n