hasDerivAt_Gamma_nat — Mathlib

English

For all n ∈ ℕ, HasDerivAt Gamma (n+1) equals n! times (-γ + H_n) in the complex setting.

Русский

Для всех n ∈ ℕ в комплексном контексте имеет место HasDerivAt Γ (n+1) = n!(-γ + H_n).

LaTeX

$$HasDerivAt Γ (n ! * (-\gamma + H_n)) (n + 1)$$

Lean4

theorem hasDerivAt_Gamma_nat (n : ℕ) : HasDerivAt Gamma (n ! * (-γ + harmonic n)) (n + 1) :=
  (deriv_Gamma_nat n).symm ▸ (differentiableAt_Gamma fun m ↦ (by linarith : (n : ℝ) + 1 ≠ -m)).hasDerivAt

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