English
For all natural n and l, the function z ↦ iteratedDerivWithin l (cotTerm z n) is differentiable on the upper half-plane.
Русский
Для всех натуральных n и l функция z ↦ iteratedDerivWithin l (cotTerm z n) дифференцируема на верхней полуплоскости.
LaTeX
$$$$\forall n,l \in \mathbb{N},\; \; \text{DifferentiableOn } \mathbb{C}\; (\lambda z. \operatorname{iteratedDerivWithin} l (\lambda w. \cotTerm w\; n)\; \mathbb{H}_{0})\; \mathbb{H}_{0}. $$$$
Lean4
theorem differentiableOn_iteratedDerivWithin_cotTerm (n l : ℕ) :
DifferentiableOn ℂ (iteratedDerivWithin l (fun z ↦ cotTerm z n) ℍₒ) ℍₒ :=
by
suffices
DifferentiableOn ℂ (fun z : ℂ ↦ (-1) ^ l * l ! * ((z + (n + 1)) ^ (-1 - l : ℤ) + (z - (n + 1)) ^ (-1 - l : ℤ))) ℍₒ
by exact this.congr fun z hz ↦ eqOn_iteratedDerivWithin_cotTerm_upperHalfPlaneSet l n hz
apply DifferentiableOn.const_mul
apply DifferentiableOn.add <;> refine DifferentiableOn.zpow (by fun_prop) <| .inl fun x hx ↦ ?_
· simpa [add_eq_zero_iff_neg_eq'] using (UpperHalfPlane.ne_int ⟨x, hx⟩ (-(n + 1))).symm
· simpa [sub_eq_zero] using (UpperHalfPlane.ne_int ⟨x, hx⟩ (n + 1))
