hasDerivAt_Gamma_one_half — Mathlib

English

Let Γ denote the gamma function. Then the derivative at 1/2 is Γ′(1/2) = -√π(γ + 2 log 2).

Русский

Обозначим гамма-функцию Γ. Тогда производная в точке 1/2: Γ′(1/2) = -√π(γ + 2 ln 2).

LaTeX

$$$\\\\Gamma'(\\\\tfrac{1}{2}) = -\\\\sqrt{\\\\pi}\\\\, (\\\\gamma + 2\\\\log 2)$$$

Lean4

theorem hasDerivAt_Gamma_one_half : HasDerivAt Gamma (-√π * (γ + 2 * log 2)) (1 / 2) :=
  by
  have := HasDerivAt.complex_of_real (differentiableAt_Gamma _ ?_) Real.hasDerivAt_Gamma_one_half Gamma_ofReal
  · simpa only [neg_mul, one_div, ofReal_neg, ofReal_mul, ofReal_add, ofReal_ofNat, ofNat_log, ofReal_inv] using this
  · intro m
    rw [← ofReal_natCast, ← ofReal_neg, ne_eq, ofReal_inj]
    exact ((neg_nonpos.mpr m.cast_nonneg).trans_lt one_half_pos).ne'

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