English
Let s and t be complex numbers and a a positive real number. Then the integral from 0 to a of x^(s−1) (a−x)^(t−1) dx equals a^(s+t−1) times the beta integral Beta(s,t). In other words, the beta integral scales by the factor a^(s+t−1).
Русский
Пусть s и t — комплексные числа, a > 0 — действительное. Тогда ∫_0^a x^{s−1} (a−x)^{t−1} dx = a^{s+t−1} βIntegral(s,t).
LaTeX
$$$$ \\int_{0}^{a} x^{s-1} (a-x)^{t-1} \\, dx \;=\; a^{s+t-1} \\betaIntegral s t.$$$$
Lean4
theorem betaIntegral_scaled (s t : ℂ) {a : ℝ} (ha : 0 < a) :
∫ x in 0..a, (x : ℂ) ^ (s - 1) * ((a : ℂ) - x) ^ (t - 1) = (a : ℂ) ^ (s + t - 1) * betaIntegral s t :=
by
have ha' : (a : ℂ) ≠ 0 := ofReal_ne_zero.mpr ha.ne'
rw [betaIntegral]
have A : (a : ℂ) ^ (s + t - 1) = a * ((a : ℂ) ^ (s - 1) * (a : ℂ) ^ (t - 1)) := by
rw [(by abel : s + t - 1 = 1 + (s - 1) + (t - 1)), cpow_add _ _ ha', cpow_add 1 _ ha', cpow_one, mul_assoc]
rw [A, mul_assoc, ← intervalIntegral.integral_const_mul, ← real_smul, ← zero_div a, ← div_self ha.ne', ←
intervalIntegral.integral_comp_div _ ha.ne', zero_div]
simp_rw [intervalIntegral.integral_of_le ha.le]
refine setIntegral_congr_fun measurableSet_Ioc fun x hx => ?_
rw [mul_mul_mul_comm]
congr 1
· rw [← mul_cpow_ofReal_nonneg ha.le (div_pos hx.1 ha).le, ofReal_div, mul_div_cancel₀ _ ha']
· rw [(by norm_cast : (1 : ℂ) - ↑(x / a) = ↑(1 - x / a)), ←
mul_cpow_ofReal_nonneg ha.le (sub_nonneg.mpr <| (div_le_one ha).mpr hx.2)]
push_cast
rw [mul_sub, mul_one, mul_div_cancel₀ _ ha']
