English
For every s > 0, log(doublingGamma(s)) equals log Γ(s/2) + log Γ(s/2+1/2) + s log 2 − log(2√π).
Русский
Для любого s > 0 логарифм doublingGamma(s) равен log Γ(s/2) + log Γ(s/2+1/2) + s log 2 − log(2√π).
LaTeX
$$$ \log\bigl( \mathrm{doublingGamma}(s) \bigr) = \log\Gamma\left(\tfrac{s}{2}\right) + \log\Gamma\left(\tfrac{s}{2}+\tfrac{1}{2}\right) + s \log 2 - \log\bigl(2\sqrt{\pi}\bigr) $$$
Lean4
theorem log_doublingGamma_eq :
EqOn (log ∘ doublingGamma) (fun s => log (Gamma (s / 2)) + log (Gamma (s / 2 + 1 / 2)) + s * log 2 - log (2 * √π))
(Ioi 0) :=
by
intro s hs
have h1 : √π ≠ 0 := sqrt_ne_zero'.mpr pi_pos
have h2 : Gamma (s / 2) ≠ 0 := (Gamma_pos_of_pos <| div_pos hs two_pos).ne'
have h3 : Gamma (s / 2 + 1 / 2) ≠ 0 := (Gamma_pos_of_pos <| add_pos (div_pos hs two_pos) one_half_pos).ne'
have h4 : (2 : ℝ) ^ (s - 1) ≠ 0 := (rpow_pos_of_pos two_pos _).ne'
rw [Function.comp_apply, doublingGamma, log_div (mul_ne_zero (mul_ne_zero h2 h3) h4) h1,
log_mul (mul_ne_zero h2 h3) h4, log_mul h2 h3, log_rpow two_pos, log_mul two_ne_zero h1]
ring_nf
