English
For every k and d, the iterated derivative within the upper half-plane set equals the same pole expression as in the integer complement case.
Русский
Для любых k и d итеративная производная внутри множества верхней полуплоскости совпадает с тем же выражением полюсов, что и в случае комплексных целых.
LaTeX
$$$$\forall k,d \in \mathbb{N},\; \;\; \operatorname{EqOn}\left(\operatorname{iteratedDerivWithin}\{k\}\; (\lambda z\; \cotTerm\, z\; d)\; \mathbb{H}_{0}\right) \\ (z \mapsto (-1)^k k! \left((z+(d+1))^{-1-k} + (z-(d+1))^{-1-k}\right)) \\ {\mathbb{H}_{0}^{\mathbb{Z}}}. $$$$
Lean4
theorem eqOn_iteratedDerivWithin_cotTerm_upperHalfPlaneSet (d : ℕ) :
EqOn (iteratedDerivWithin k (fun z ↦ cotTerm z d) ℍₒ)
(fun z ↦ (-1) ^ k * k ! * ((z + (d + 1)) ^ (-1 - k : ℤ) + (z - (d + 1)) ^ (-1 - k : ℤ))) ℍₒ :=
by
apply
Set.EqOn.trans
(upperHalfPlane_inter_integerComplement ▸
iteratedDerivWithin_congr_right_of_isOpen (fun z ↦ cotTerm z d) k isOpen_upperHalfPlaneSet
(isOpen_compl_range_intCast))
intro z hz
simpa using eqOn_iteratedDerivWithin_cotTerm_integerComplement k d (coe_mem_integerComplement ⟨z, hz⟩)
