eqOn_iteratedDerivWithin_cotTerm_integerComplement

English

For all k and d, the iterated derivative within the complex-integer-complement set matches the explicit pole expression.

Русский

Для всех k и d итеративная производная внутри множества комплексных чисел, не целых, совпадает с явным выражением полюсов.

LaTeX

$$$$\forall k,d \in \mathbb{N},\; \;\; \operatorname{EqOn}\left(\operatorname{iteratedDerivWithin}\\{k}\, (\lambda z\; \cotTerm\, z\; d)\right) \\ (z \mapsto (-1)^k k! \left((z+(d+1))^{-1-k} + (z-(d+1))^{-1-k}\right)) \\ {\mathbb{C}_{\mathbb{Z}}}. $$$$

Lean4

theorem eqOn_iteratedDerivWithin_cotTerm_integerComplement (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 (iteratedDerivWithin_of_isOpen isOpen_compl_range_intCast)
  exact eqOn_iteratedDeriv_cotTerm ..

Похожие утверждения