English
The derivative of Gamma at 1/2 is −√π(γ + 2 log 2).
Русский
Производная гаммы в точке 1/2 равна −√π(γ + 2 log 2).
LaTeX
$$\operatorname{deriv} \Gamma \left( \tfrac{1}{2} \right) = -\sqrt{\pi}\, (\gamma + 2 \log 2)$$
Lean4
theorem hasDerivAt_Gamma_one_half : HasDerivAt Gamma (-√π * (γ + 2 * log 2)) (1 / 2) :=
by
have h_diff {s : ℝ} (hs : 0 < s) : DifferentiableAt ℝ Gamma s :=
differentiableAt_Gamma fun m ↦ ((neg_nonpos.mpr m.cast_nonneg).trans_lt hs).ne'
have h_diff' {s : ℝ} (hs : 0 < s) : DifferentiableAt ℝ (fun s ↦ Gamma (2 * s)) s :=
.comp (g := Gamma) _ (h_diff <| mul_pos two_pos hs) (differentiableAt_id.const_mul _)
refine
(h_diff one_half_pos).hasDerivAt.congr_deriv
?_
-- We calculate the deriv of Gamma at 1/2 using the doubling formula, since we already know
-- the derivative of Gamma at 1.
calc
deriv Gamma (1 / 2)
_ = (deriv (fun s ↦ Gamma s * Gamma (s + 1 / 2)) (1 / 2)) + √π * γ :=
by
rw [deriv_fun_mul, Gamma_one_half_eq, add_assoc, ← mul_add, deriv_comp_add_const,
(by norm_num : 1 / 2 + 1 / 2 = (1 : ℝ)), Gamma_one, mul_one, eulerMascheroniConstant_eq_neg_deriv,
add_neg_cancel, mul_zero, add_zero]
· apply h_diff;
simp -- s = 1
· exact ((h_diff (by simp)).hasDerivAt.comp_add_const).differentiableAt
_ = (deriv (fun s ↦ Gamma (2 * s) * 2 ^ (1 - 2 * s) * √π) (1 / 2)) + √π * γ := by
rw [funext Gamma_mul_Gamma_add_half]
_ = √π * (deriv (fun s ↦ Gamma (2 * s) * 2 ^ (1 - 2 * s)) (1 / 2) + γ) :=
by
rw [mul_comm √π, mul_comm √π, deriv_mul_const, add_mul]
apply DifferentiableAt.mul
·
exact
.comp (g := Gamma) _
(by apply h_diff; simp) -- s = 1
(differentiableAt_id.const_mul _)
· exact (differentiableAt_const _).rpow (by fun_prop) two_ne_zero
_ = √π * (deriv (fun s ↦ Gamma (2 * s)) (1 / 2) + deriv (fun s : ℝ ↦ 2 ^ (1 - 2 * s)) (1 / 2) + γ) :=
by
congr 2
rw [deriv_fun_mul]
· congr 1 <;> norm_num
· exact h_diff' one_half_pos
· exact DifferentiableAt.rpow (by fun_prop) (by fun_prop) two_ne_zero
_ = √π * (-2 * γ + deriv (fun s : ℝ ↦ 2 ^ (1 - 2 * s)) (1 / 2) + γ) :=
by
congr 3
change deriv (Gamma ∘ fun s ↦ 2 * s) _ = _
rw [deriv_comp, deriv_const_mul, mul_one_div, div_self two_ne_zero, deriv_id''] <;> dsimp only
· rw [mul_one, mul_comm, hasDerivAt_Gamma_one.deriv, mul_neg, neg_mul]
· fun_prop
· apply h_diff;
simp -- s = 1
· fun_prop
_ = √π * (-2 * γ + -(2 * log 2) + γ) := by
congr 3
apply HasDerivAt.deriv
have :=
HasDerivAt.rpow (hasDerivAt_const (1 / 2 : ℝ) (2 : ℝ)) (?_ : HasDerivAt (fun s : ℝ ↦ 1 - 2 * s) (-2) (1 / 2))
two_pos
· norm_num at this; exact this
simp_rw [mul_comm (2 : ℝ) _]
apply HasDerivAt.const_sub
exact hasDerivAt_mul_const (2 : ℝ)
_ = -√π * (γ + 2 * log 2) := by ring
