GammaSeq_eq_betaIntegral_of_re_pos

English

For s ∈ ℂ with Re(s) > 0 and n ∈ ℕ, the GammaSeq term factors as a product: ΓSeq(s, n) = n^s · betaIntegral(s, n+1).

Русский

Для s ∈ ℂ с Re(s) > 0 и n ∈ ℕ член ΓSeq(s, n) распадается на произведение: ΓSeq(s, n) = n^s · betaIntegral(s, n+1).

LaTeX

$$$\\\\GammaSeq(s, n) = (n)^{s} \\\\cdot \\betaIntegral(s, n+1)$$$

Lean4

theorem GammaSeq_eq_betaIntegral_of_re_pos {s : ℂ} (hs : 0 < re s) (n : ℕ) :
    GammaSeq s n = (n : ℂ) ^ s * betaIntegral s (n + 1) := by
  rw [GammaSeq, betaIntegral_eval_nat_add_one_right hs n, ← mul_div_assoc]

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