English
For r ∈ ℝ with -1 < r, the function x ↦ x^r is interval-integrable with respect to the volume measure on any interval [a, b].
Русский
Для r ∈ ℝ при -1 < r функция x^r интегрируема по интервалу на любом [a, b] относительно объёма.
LaTeX
$$$\\\\forall a,b \\\\in \\\\mathbb{R}, \\\\text{IntervalIntegrable}(x \\\\mapsto x^{r})\\\\ volume\\\\ a \\\\ b \text{ for } -1 < r.$$$
Lean4
/-- See `intervalIntegrable_rpow` for a version applying to any locally finite measure, but with a
stronger hypothesis on `r`. -/
theorem intervalIntegrable_rpow' {r : ℝ} (h : -1 < r) : IntervalIntegrable (fun x => x ^ r) volume a b :=
by
suffices ∀ c : ℝ, IntervalIntegrable (fun x => x ^ r) volume 0 c by
exact IntervalIntegrable.trans (this a).symm (this b)
have : ∀ c : ℝ, 0 ≤ c → IntervalIntegrable (fun x => x ^ r) volume 0 c :=
by
intro c hc
rw [intervalIntegrable_iff, uIoc_of_le hc]
have hderiv : ∀ x ∈ Ioo 0 c, HasDerivAt (fun x : ℝ => x ^ (r + 1) / (r + 1)) (x ^ r) x :=
by
intro x hx
convert (Real.hasDerivAt_rpow_const (p := r + 1) (Or.inl hx.1.ne')).div_const (r + 1) using 1
simp [(by linarith : r + 1 ≠ 0)]
apply integrableOn_deriv_of_nonneg _ hderiv
· intro x hx; apply rpow_nonneg hx.1.le
· refine (continuousOn_id.rpow_const ?_).div_const _; intro x _; right; linarith
intro c; rcases le_total 0 c with (hc | hc)
· exact this c hc
· rw [IntervalIntegrable.iff_comp_neg, neg_zero]
have m := (this (-c) (by linarith)).smul (cos (r * π))
rw [intervalIntegrable_iff] at m ⊢
refine m.congr_fun ?_ measurableSet_Ioc; intro x hx
rw [uIoc_of_le (by linarith : 0 ≤ -c)] at hx
simp only [Pi.smul_apply, Algebra.id.smul_eq_mul, log_neg_eq_log, mul_comm, rpow_def_of_pos hx.1,
rpow_def_of_neg (by linarith [hx.1] : -x < 0)]
