English
For real r with the usual convergence condition, the integral ∫_a^b x^r dx equals (b^{r+1} - a^{r+1})/(r+1).
Русский
Для вещественного r при обычном условии сходимости интеграл ∫_a^b x^r dx равен (b^{r+1} - a^{r+1})/(r+1).
LaTeX
$$$\int_{a}^{b} x^{r} \, dx = \frac{b^{r+1} - a^{r+1}}{r+1}$$$
Lean4
theorem integral_rpow {r : ℝ} (h : -1 < r ∨ r ≠ -1 ∧ (0 : ℝ) ∉ [[a, b]]) :
∫ x in a..b, x ^ r = (b ^ (r + 1) - a ^ (r + 1)) / (r + 1) :=
by
have h' : -1 < (r : ℂ).re ∨ (r : ℂ) ≠ -1 ∧ (0 : ℝ) ∉ [[a, b]] :=
by
cases h
· left; rwa [Complex.ofReal_re]
· right; rwa [← Complex.ofReal_one, ← Complex.ofReal_neg, Ne, Complex.ofReal_inj]
have : (∫ x in a..b, (x : ℂ) ^ (r : ℂ)) = ((b : ℂ) ^ (r + 1 : ℂ) - (a : ℂ) ^ (r + 1 : ℂ)) / (r + 1) :=
integral_cpow h'
apply_fun Complex.re at this; convert this
· simp_rw [intervalIntegral_eq_integral_uIoc, Complex.real_smul, Complex.re_ofReal_mul, rpow_def, ←
RCLike.re_eq_complex_re, smul_eq_mul]
rw [integral_re]
refine intervalIntegrable_iff.mp ?_
rcases h' with h' | h'
· exact intervalIntegrable_cpow' h'
· exact intervalIntegrable_cpow (Or.inr h'.2)
· rw [(by push_cast; rfl : (r : ℂ) + 1 = ((r + 1 : ℝ) : ℂ))]
simp_rw [div_eq_inv_mul, ← Complex.ofReal_inv, Complex.re_ofReal_mul, Complex.sub_re, rpow_def]
