English
Let u be a complex number with Re(u) > 0 and let n be a natural number. Then the beta function evaluated at (u, n+1) has the explicit finite product form: β(u, n+1) = n! / ∏_{j=0}^{n} (u + j).
Русский
Пусть u ∈ ℂ так, что Re(u) > 0, и пусть n ∈ ℕ. Тогда β(u, n+1) имеет явную формулу: β(u, n+1) = n! / ∏_{j=0}^{n} (u + j).
LaTeX
$$$\\\\forall u \in \\mathbb{C}, \\, Re(u) > 0, \\\\forall n \\\\in \\\\mathbb{N},\\\\ β(u, n+1) = \\frac{n!}{\\prod_{j=0}^{n} (u + j)}$$$
Lean4
/-- Explicit formula for the Beta function when second argument is a positive integer. -/
theorem betaIntegral_eval_nat_add_one_right {u : ℂ} (hu : 0 < re u) (n : ℕ) :
betaIntegral u (n + 1) = n ! / ∏ j ∈ Finset.range (n + 1), (u + j) := by
induction n generalizing u with
| zero =>
rw [Nat.cast_zero, zero_add, betaIntegral_eval_one_right hu, Nat.factorial_zero, Nat.cast_one]
simp
| succ n IH =>
have := betaIntegral_recurrence hu (?_ : 0 < re n.succ)
swap; · rw [← ofReal_natCast, ofReal_re]; positivity
rw [mul_comm u _, ← eq_div_iff] at this
swap; · contrapose! hu; rw [hu, zero_re]
rw [this, Finset.prod_range_succ', Nat.cast_succ, IH]
swap; · rw [add_re, one_re]; positivity
rw [Nat.factorial_succ, Nat.cast_mul, Nat.cast_add, Nat.cast_one, Nat.cast_zero, add_zero, ← mul_div_assoc, ←
div_div]
congr 3 with j : 1
push_cast; abel
