English
Let Γℂ be the complex gamma function. At 1, its derivative satisfies Γℂ′(1) = - (γ + log(2π)) / π.
Русский
Пусть Γℂ – комплексная гамма-функция. В точке 1 производная удовлетворяет Γℂ′(1) = - (γ + ln(2π)) / π.
LaTeX
$$$\\\\Gamma_{\\mathbb{C}}'(1) = -\\\\frac{\\\\gamma + \\\\log(2\\\\pi)}{\\\\pi}$$$
Lean4
theorem hasDerivAt_Gammaℂ_one : HasDerivAt Gammaℂ (-(γ + log (2 * π)) / π) 1 :=
by
let f (s : ℂ) : ℂ := 2 * (2 * π) ^ (-s)
have : HasDerivAt (fun s : ℂ ↦ 2 * (2 * π : ℂ) ^ (-s)) (-log (2 * π) / π) 1 :=
by
have := (hasDerivAt_neg' (1 : ℂ)).const_cpow (c := 2 * π) (Or.inl (by exact_mod_cast Real.two_pi_pos.ne'))
refine (this.const_mul 2).congr_deriv ?_
rw [mul_neg_one, mul_neg, cpow_neg_one, ← div_eq_inv_mul, ← mul_div_assoc, mul_div_mul_left _ _ two_ne_zero,
neg_div]
have := this.mul hasDerivAt_Gamma_one
simp only at this
rwa [Gamma_one, mul_one, cpow_neg_one, ← div_eq_mul_inv, ← div_div, div_self two_ne_zero, mul_comm (1 / _),
mul_one_div, ← _root_.add_div, ← neg_add, add_comm] at this
