doublingGamma_eq_Gamma — Mathlib

English

For all s with s > 0, doublingGamma(s) equals Gamma(s).

Русский

Для всех s > 0 doublingGamma(s) = Γ(s).

LaTeX

$$$ \mathrm{doublingGamma}(s) = \Gamma(s) \quad (s > 0) $$$

Lean4

theorem doublingGamma_eq_Gamma {s : ℝ} (hs : 0 < s) : doublingGamma s = Gamma s :=
  by
  refine
    eq_Gamma_of_log_convex doublingGamma_log_convex_Ioi (fun {y} hy => doublingGamma_add_one y hy.ne')
      (fun {y} hy => ?_) doublingGamma_one hs
  apply_rules [mul_pos, Gamma_pos_of_pos, add_pos, inv_pos_of_pos, rpow_pos_of_pos, two_pos, one_pos,
    sqrt_pos_of_pos pi_pos]

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