TsumderivWithin

@[reducible, inline]

abbrev ℍ' : Set ℂ

The open upper half-plane as a subset of ℂ.

Equations

• ℍ' = {z : ℂ | 0 < z.im}

theorem upper_half_plane_isOpen : IsOpen ℍ'

theorem derivWithin_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) : derivWithin (fun (z : ℂ) => ∑' (n : α), f n z) s x = ∑' (n : α), derivWithin (fun (z : ℂ) => f n z) s x

theorem der_iter_eq_der_aux2 (k n : ℕ) (r : ↑ℍ') : DifferentiableAt ℂ (fun (z : ℂ) => iteratedDerivWithin k (fun (s : ℂ) => Complex.exp (2 * ↑Real.pi * Complex.I * ↑n * s)) ℍ' z) ↑r

theorem der_iter_eq_der2 (k n : ℕ) (r : ↑ℍ') : deriv (iteratedDerivWithin k (fun (s : ℂ) => Complex.exp (2 * ↑Real.pi * Complex.I * ↑n * s)) ℍ') ↑r = derivWithin (iteratedDerivWithin k (fun (s : ℂ) => Complex.exp (2 * ↑Real.pi * Complex.I * ↑n * s)) ℍ') ℍ' ↑r

theorem der_iter_eq_der2' (k n : ℕ) (r : ↑ℍ') : derivWithin (iteratedDerivWithin k (fun (s : ℂ) => Complex.exp (2 * ↑Real.pi * Complex.I * ↑n * s)) ℍ') ℍ' ↑r = iteratedDerivWithin (k + 1) (fun (s : ℂ) => Complex.exp (2 * ↑Real.pi * Complex.I * ↑n * s)) ℍ' ↑r

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

The continuous map z ↦ exp (2π i z) restricted to a subset K of ℂ.

Equations

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

theorem iter_deriv_comp_bound2 (K : Set ℂ) (hK1 : K ⊆ ℍ') (hK2 : IsCompact K) (k : ℕ) : ∃ (u : ℕ → ℝ), Summable u ∧ ∀ (n : ℕ) (r : ↑K), ‖derivWithin (iteratedDerivWithin k (fun (s : ℂ) => Complex.exp (2 * ↑Real.pi * Complex.I * ↑n * s)) ℍ') ℍ' ↑r‖ ≤ u n

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 hasDerivWithinAt_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) : HasDerivWithinAt (fun (z : ℂ) => ∑' (n : α), f n z) (∑' (n : α), derivWithin (fun (z : ℂ) => f n z) s x) s x

theorem iter_deriv_comp_bound3 (K : Set ℂ) (hK1 : K ⊆ ℍ') (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