English
Let a, b be real numbers and t a real exponent with t ≠ −1. Then the real-valued integral from a to b of x(1 + x^2)^t equals (1 + b^2)^{t+1}/(2(t+1)) − (1 + a^2)^{t+1}/(2(t+1)).
Русский
Пусть a, b ∈ ℝ и t ∈ ℝ с t ≠ −1. Тогда интеграл по x от a до b от x(1 + x^2)^t равен (1 + b^2)^{t+1}/(2(t+1)) − (1 + a^2)^{t+1}/(2(t+1)).
LaTeX
$$$$\\displaystyle \\int_{a}^{b} x\\left(1+x^{2}\\right)^{t}\\,dx = \\frac{(1+b^{2})^{t+1}}{2(t+1)} - \\frac{(1+a^{2})^{t+1}}{2(t+1)}.$$$$
Lean4
theorem integral_mul_rpow_one_add_sq {t : ℝ} (ht : t ≠ -1) :
(∫ x : ℝ in a..b, x * (↑1 + x ^ 2) ^ t) =
(↑1 + b ^ 2) ^ (t + 1) / (↑2 * (t + ↑1)) - (↑1 + a ^ 2) ^ (t + 1) / (↑2 * (t + ↑1)) :=
by
have : ∀ x s : ℝ, (((↑1 + x ^ 2) ^ s : ℝ) : ℂ) = (1 + (x : ℂ) ^ 2) ^ (s : ℂ) :=
by
intro x s
norm_cast
rw [ofReal_cpow, ofReal_add, ofReal_pow, ofReal_one]
exact add_nonneg zero_le_one (sq_nonneg x)
rw [← ofReal_inj]
convert integral_mul_cpow_one_add_sq (_ : (t : ℂ) ≠ -1)
· rw [← intervalIntegral.integral_ofReal]
congr with x : 1
rw [ofReal_mul, this x t]
· simp_rw [ofReal_sub, ofReal_div, this a (t + 1), this b (t + 1)]
push_cast; rfl
· rw [← ofReal_one, ← ofReal_neg, Ne, ofReal_inj]
exact ht
