hasDerivAt_Gamma_one — Mathlib

English

Let Γ denote the gamma function. Then the derivative of Γ at 1 equals the negative Euler–Mascheroni constant, i.e., Γ′(1) = -γ.

Русский

Пусть Γ обозначает гамма-функцию. Тогда производная Γ в точке 1 равна минус постоянной Эйлера-Маскерони γ: Γ′(1) = -γ.

LaTeX

$$$\\\\Gamma'(1) = -\\\\gamma$$$

Lean4

theorem hasDerivAt_Gamma_one : HasDerivAt Gamma (-γ) 1 := by
  simpa only [factorial_zero, cast_one, harmonic_zero, Rat.cast_zero, add_zero, mul_neg, one_mul, cast_zero,
    zero_add] using hasDerivAt_Gamma_nat 0

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