English
For u with positive real part, the left endpoint convergence holds for Beta integrand with parameter v.
Русский
Пусть Re(u) > 0; тогда интеграл слева по [0,1/2] сходится для функции x^{u-1}(1-x)^{v-1}.
LaTeX
$$$\text{betaIntegral_convergent_left}(u,v)\!:\! \text{IntervalIntegrable} (x \mapsto x^{u-1}(1-x)^{v-1}) [0,1/2]$$$
Lean4
/-- Auxiliary lemma for `betaIntegral_convergent`, showing convergence at the left endpoint. -/
theorem betaIntegral_convergent_left {u : ℂ} (hu : 0 < re u) (v : ℂ) :
IntervalIntegrable (fun x => (x : ℂ) ^ (u - 1) * (1 - (x : ℂ)) ^ (v - 1) : ℝ → ℂ) volume 0 (1 / 2) :=
by
apply IntervalIntegrable.mul_continuousOn
· refine intervalIntegral.intervalIntegrable_cpow' ?_
rwa [sub_re, one_re, ← zero_sub, sub_lt_sub_iff_right]
· apply continuousOn_of_forall_continuousAt
intro x hx
rw [uIcc_of_le (by positivity : (0 : ℝ) ≤ 1 / 2)] at hx
apply ContinuousAt.cpow
· exact (continuous_const.sub continuous_ofReal).continuousAt
· exact continuousAt_const
· norm_cast
exact ofReal_mem_slitPlane.2 <| by linarith only [hx.2]
