English
The function x^−1 is not interval integrable on [a, ∞).
Русский
Функция x^−1 не интегрируема по интервалу [a, ∞).
LaTeX
$$$\\neg \\operatorname{IntegrableOn}(x^{-1}, [a, \\infty))$$$
Lean4
/-- The function `fun x ↦ x⁻¹` is not integrable on any interval `[a, +∞)`. -/
theorem not_IntegrableOn_Ici_inv {a : ℝ} : ¬IntegrableOn (fun x => x⁻¹) (Ici a) :=
by
have A : ∀ᶠ x in atTop, HasDerivAt (fun x => Real.log x) x⁻¹ x := by
filter_upwards [Ioi_mem_atTop 0] with x hx using Real.hasDerivAt_log (ne_of_gt hx)
have B : Tendsto (fun x => ‖Real.log x‖) atTop atTop := tendsto_norm_atTop_atTop.comp Real.tendsto_log_atTop
exact
not_integrableOn_of_tendsto_norm_atTop_of_deriv_isBigO_filter atTop (Ici_mem_atTop a)
(A.mono (fun x hx ↦ hx.differentiableAt)) B (Filter.EventuallyEq.isBigO (A.mono (fun x hx ↦ hx.deriv)))
