betaIntegral_eq_Gamma_mul_div — Mathlib

English

For u,v ∈ ℂ with Re(u)>0 and Re(v)>0, the beta integral satisfies β(u,v) = Γ(u) Γ(v) / Γ(u+v).

Русский

Для u,v ∈ ℂ с Re(u)>0, Re(v)>0, выполняется β(u,v) = Γ(u) Γ(v) / Γ(u+v).

LaTeX

$$$$ \betaIntegral(u,v) = \frac{\Gamma(u) \Gamma(v)}{\Gamma(u+v)}. $$$$

Lean4

theorem betaIntegral_eq_Gamma_mul_div (u v : ℂ) (hu : 0 < u.re) (hv : 0 < v.re) :
    betaIntegral u v = Gamma u * Gamma v / Gamma (u + v) := by
  rw [Gamma_mul_Gamma_eq_betaIntegral hu hv, mul_div_cancel_left₀ _ (Gamma_ne_zero_of_re_pos (add_pos hu hv))]

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