English
If k ≥ 1, then the family n ↦ iteratedDerivWithin k (cotTerm z n) is summably locally uniformly on the upper half-plane.
Русский
Если k ≥ 1, то семейство n ↦ iteratedDerivWithin k (cotTerm z n) образует суммируемость локально равномерная на верхней полуплоскости.
LaTeX
$$$$\forall k \in \mathbb{N},\; k \ge 1:\; \text{SummableLocallyUniformlyOn}\left( z \mapsto \operatorname{iteratedDerivWithin} k (\lambda n. \cotTerm\, z\, n)\; \mathbb{H}_{0}\right)\; \mathbb{H}_{0}. $$$$
Lean4
theorem summableLocallyUniformlyOn_iteratedDerivWithin_cotTerm {k : ℕ} (hk : 1 ≤ k) :
SummableLocallyUniformlyOn (fun n ↦ iteratedDerivWithin k (fun z ↦ cotTerm z n) ℍₒ) ℍₒ :=
by
apply SummableLocallyUniformlyOn_of_locally_bounded isOpen_upperHalfPlaneSet
intro K hK hKc
obtain ⟨A, B, hB, HABK⟩ :=
subset_verticalStrip_of_isCompact
((isCompact_iff_isCompact_univ.mp hKc).image_of_continuousOn (continuous_inclusion hK |>.continuousOn))
exact
⟨cotTermUpperBound k A B hB, summable_cotTermUpperBound A B hB hk,
iteratedDerivWithin_cotTerm_bounded_uniformly hK A B hB HABK⟩
