English
For every real s, the function x ↦ x^s is not integrable on (0, ∞).
Русский
Для любого действительного s функция x^s не интегрируема на (0, ∞).
LaTeX
$$$\\forall s \\in \\mathbb{R}, \\; \\neg\\mathrm{IntegrableOn}(x \\mapsto x^{s}, Ioi(0))$$$
Lean4
/-- The real power function with any exponent is not integrable on `(0, +∞)`. -/
theorem not_integrableOn_Ioi_rpow (s : ℝ) : ¬IntegrableOn (fun x ↦ x ^ s) (Ioi (0 : ℝ)) :=
by
intro h
rcases le_or_gt s (-1) with hs | hs
· have : IntegrableOn (fun x ↦ x ^ s) (Ioo (0 : ℝ) 1) := h.mono Ioo_subset_Ioi_self le_rfl
rw [integrableOn_Ioo_rpow_iff zero_lt_one] at this
exact hs.not_gt this
· have : IntegrableOn (fun x ↦ x ^ s) (Ioi (1 : ℝ)) := h.mono (Ioi_subset_Ioi zero_le_one) le_rfl
rw [integrableOn_Ioi_rpow_iff zero_lt_one] at this
exact hs.not_gt this
