hasDerivAt_Gamma_nat — Mathlib

English

For every n, has derivative at n+1 equals n!(-γ + H_n) in Complex.

Русский

Для каждого n в комплексном контексте производная Γ в n+1 равна n!(-γ + H_n).

LaTeX

$$HasDerivAt Gamma (n ! * (-γ + H_n)) (n + 1)$$

Lean4

theorem hasDerivAt_Gamma_nat (n : ℕ) : HasDerivAt Gamma (n ! * (-γ + harmonic n)) (n + 1) := by
  exact_mod_cast
    HasDerivAt.complex_of_real (by exact_mod_cast differentiableAt_Gamma_nat_add_one n) (Real.hasDerivAt_Gamma_nat n)
      Gamma_ofReal

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