English
For every complex exponent s, the function x ↦ x^s is not Lebesgue integrable on (0, ∞).
Русский
Пусть s ∈ ℂ. Функция x ↦ x^s не интегрируема по Лебегу на (0, ∞).
LaTeX
$$$\forall s \in \mathbb{C}, \int_{0}^{\infty} |x^{s}| \, dx = \infty$$$
Lean4
/-- The complex power function with any exponent is not integrable on `(0, +∞)`. -/
theorem not_integrableOn_Ioi_cpow (s : ℂ) : ¬IntegrableOn (fun x : ℝ ↦ (x : ℂ) ^ s) (Ioi (0 : ℝ)) :=
by
intro h
rcases le_or_gt s.re (-1) with hs | hs
· have : IntegrableOn (fun x : ℝ ↦ (x : ℂ) ^ s) (Ioo (0 : ℝ) 1) := h.mono Ioo_subset_Ioi_self le_rfl
rw [integrableOn_Ioo_cpow_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_cpow_iff zero_lt_one] at this
exact hs.not_gt this
