English
Let u and v be complex numbers with Re(u) > 0 and Re(v) > 0. Then u times BetaIntegral(u, v+1) equals v times BetaIntegral(u+1, v).
Русский
Пусть u, v — комплексные числа такие, что Re(u) > 0 и Re(v) > 0. Тогда u·βIntegral(u, v+1) = v·βIntegral(u+1, v).
LaTeX
$$$$ u\\,\\betaIntegral(u, v+1) = v\\,\\betaIntegral(u+1, v), \\qquad \\Re(u) > 0, \\Re(v) > 0. $$$$
Lean4
/-- Recurrence formula for the Beta function. -/
theorem betaIntegral_recurrence {u v : ℂ} (hu : 0 < re u) (hv : 0 < re v) :
u * betaIntegral u (v + 1) = v * betaIntegral (u + 1) v := by
-- NB: If we knew `Gamma (u + v + 1) ≠ 0` this would be an easy consequence of
-- `Gamma_mul_Gamma_eq_betaIntegral`; but we don't know that yet. We will prove it later, but
-- this lemma is needed in the proof. So we give a (somewhat laborious) direct argument.
let F : ℝ → ℂ := fun x => (x : ℂ) ^ u * (1 - (x : ℂ)) ^ v
have hu' : 0 < re (u + 1) := by rw [add_re, one_re]; positivity
have hv' : 0 < re (v + 1) := by rw [add_re, one_re]; positivity
have hc : ContinuousOn F (Icc 0 1) :=
by
refine (continuousOn_of_forall_continuousAt fun x hx => ?_).mul (continuousOn_of_forall_continuousAt fun x hx => ?_)
· refine (continuousAt_cpow_const_of_re_pos (Or.inl ?_) hu).comp continuous_ofReal.continuousAt
rw [ofReal_re]; exact hx.1
· refine
(continuousAt_cpow_const_of_re_pos (Or.inl ?_) hv).comp (continuous_const.sub continuous_ofReal).continuousAt
rw [sub_re, one_re, ofReal_re, sub_nonneg]
exact hx.2
have hder :
∀ x : ℝ,
x ∈ Ioo (0 : ℝ) 1 →
HasDerivAt F (u * ((x : ℂ) ^ (u - 1) * (1 - (x : ℂ)) ^ v) - v * ((x : ℂ) ^ u * (1 - (x : ℂ)) ^ (v - 1))) x :=
by
intro x hx
have U : HasDerivAt (fun y : ℂ => y ^ u) (u * (x : ℂ) ^ (u - 1)) ↑x :=
by
have := @HasDerivAt.cpow_const _ _ _ u (hasDerivAt_id (x : ℂ)) (Or.inl ?_)
· simp only [id_eq, mul_one] at this
exact this
· rw [id_eq, ofReal_re]; exact hx.1
have V : HasDerivAt (fun y : ℂ => (1 - y) ^ v) (-v * (1 - (x : ℂ)) ^ (v - 1)) ↑x :=
by
have A := @HasDerivAt.cpow_const _ _ _ v (hasDerivAt_id (1 - (x : ℂ))) (Or.inl ?_)
swap; · rw [id, sub_re, one_re, ofReal_re, sub_pos]; exact hx.2
simp_rw [id] at A
have B : HasDerivAt (fun y : ℂ => 1 - y) (-1) ↑x := by apply HasDerivAt.const_sub; apply hasDerivAt_id
convert HasDerivAt.comp (↑x) A B using 1
ring
convert (U.mul V).comp_ofReal using 1
ring
have h_int := ((betaIntegral_convergent hu hv').const_mul u).sub ((betaIntegral_convergent hu' hv).const_mul v)
rw [add_sub_cancel_right, add_sub_cancel_right] at h_int
have int_ev := intervalIntegral.integral_eq_sub_of_hasDerivAt_of_le zero_le_one hc hder h_int
have hF0 : F 0 = 0 :=
by
simp only [F, mul_eq_zero, ofReal_zero, cpow_eq_zero_iff, Ne, true_and, sub_zero, one_cpow, one_ne_zero, or_false]
contrapose! hu; rw [hu, zero_re]
have hF1 : F 1 = 0 :=
by
simp only [F, mul_eq_zero, ofReal_one, one_cpow, one_ne_zero, sub_self, cpow_eq_zero_iff, Ne, true_and, false_or]
contrapose! hv; rw [hv, zero_re]
rw [hF0, hF1, sub_zero, intervalIntegral.integral_sub, intervalIntegral.integral_const_mul,
intervalIntegral.integral_const_mul] at int_ev
· rw [betaIntegral, betaIntegral, ← sub_eq_zero]
convert int_ev <;> ring
· apply IntervalIntegrable.const_mul
convert betaIntegral_convergent hu hv'; ring
· apply IntervalIntegrable.const_mul
convert betaIntegral_convergent hu' hv; ring
