English
The Beta integral converges for all u,v with positive real parts.
Русский
Пределитель Beta-конгруентности сходится для любых u,v с положительной вещественной частью.
LaTeX
$$$\forall u,v\in\mathbb{C},\ \Re(u)>0\ \&\ \Re(v)>0 \ \Rightarrow \text{IntervalIntegrable}(x^{u-1}(1-x)^{v-1},0,1)$$$
Lean4
/-- The Beta integral is convergent for all `u, v` of positive real part. -/
theorem betaIntegral_convergent {u v : ℂ} (hu : 0 < re u) (hv : 0 < re v) :
IntervalIntegrable (fun x => (x : ℂ) ^ (u - 1) * (1 - (x : ℂ)) ^ (v - 1) : ℝ → ℂ) volume 0 1 :=
by
refine (betaIntegral_convergent_left hu v).trans ?_
rw [IntervalIntegrable.iff_comp_neg]
convert ((betaIntegral_convergent_left hv u).comp_add_right 1).symm using 1
· ext1 x
conv_lhs => rw [mul_comm]
congr 2 <;> · push_cast; ring
· norm_num
· simp
