English
Let Γℝ denote the real gamma function. Then Γℝ′(1) = - (γ + log(4π)) / 2.
Русский
Пусть Γℝ обозначает вещественную гамма-функцию. Тогда Γℝ′(1) = - (γ + ln(4π)) / 2.
LaTeX
$$$\\\\Gamma_{\\\\mathbb{R}}'(1) = -\\\\frac{\\\\gamma + \\\\log(4\\\\pi)}{2}$$$
Lean4
theorem hasDerivAt_Gammaℝ_one : HasDerivAt Gammaℝ (-(γ + log (4 * π)) / 2) 1 :=
by
let f (s : ℂ) : ℂ := π ^ (-s / 2)
let g (s : ℂ) : ℂ := Gamma (s / 2)
have aux : (π : ℂ) ^ (1 / 2 : ℂ) = ↑√π := by
rw [Real.sqrt_eq_rpow, ofReal_cpow Real.pi_pos.le, ofReal_div, ofReal_one, ofReal_ofNat]
have aux2 : (√π : ℂ) ≠ 0 := by rw [ofReal_ne_zero]; positivity
have hf : HasDerivAt f (-log π / 2 / √π) 1 :=
by
have := ((hasDerivAt_neg (1 : ℂ)).div_const 2).const_cpow (c := π) (Or.inr (by simp))
refine this.congr_deriv ?_
rw [mul_assoc, ← mul_div_assoc, mul_neg_one, neg_div, cpow_neg, ← div_eq_inv_mul, aux]
have hg : HasDerivAt g (-√π * (γ + 2 * log 2) / 2) 1 :=
by
have := hasDerivAt_Gamma_one_half.comp 1 (?_ : HasDerivAt (fun s : ℂ ↦ s / 2) (1 / 2) 1)
· rwa [mul_one_div] at this
· exact (hasDerivAt_id _).div_const _
refine HasDerivAt.congr_deriv (hf.mul hg) ?_
simp only [f]
rw [Gamma_one_half_eq, aux, div_mul_cancel₀ _ aux2, neg_div _ (1 : ℂ), cpow_neg, aux, mul_div_assoc, ← mul_assoc,
mul_neg, inv_mul_cancel₀ aux2, neg_one_mul, ← neg_div, ← _root_.add_div, ← neg_add, add_comm, add_assoc, ←
ofReal_log Real.pi_pos.le, ← ofReal_ofNat, ← ofReal_log zero_le_two, ← ofReal_mul, ← Nat.cast_ofNat (R := ℝ), ←
Real.log_pow, ← ofReal_add, ← Real.log_mul (by positivity) (by positivity), Nat.cast_ofNat, ofReal_ofNat,
ofReal_log (by positivity)]
norm_num
