mathlib documentation

analysis.special_functions.non_integrable

Non integrable functions #

In this file we prove that the derivative of a function that tends to infinity is not interval integrable, see interval_integral.not_integrable_has_deriv_at_of_tendsto_norm_at_top_filter and interval_integral.not_integrable_has_deriv_at_of_tendsto_norm_at_top_punctured. Then we apply the latter lemma to prove that the function λ x, x⁻¹ is integrable on a..b if and only if a = b or 0 ∉ [a, b].

Main results #

Tags #

integrable function

If f is eventually differentiable along a nontrivial filter l : filter that is generated by convex sets, the norm of f tends to infinity along l, and f' = O(g) along l, where f' is the derivative of f, then g is not integrable on any interval a..b such that [a, b] ∈ l.

If a ≠ b, c ∈ [a, b], f is differentiable in the neighborhood of c within [a, b] \ {c}, ‖f x‖ → ∞ as x → c within [a, b] \ {c}, and f' = O(g) along 𝓝[[a, b] \ {c}] c, where f' is the derivative of f, then g is not interval integrable on a..b.

If f is differentiable in a punctured neighborhood of c, ‖f x‖ → ∞ as x → c (more formally, along the filter 𝓝[≠] c), and f' = O(g) along 𝓝[≠] c, where f' is the derivative of f, then g is not interval integrable on any nontrivial interval a..b such that c ∈ [a, b].

If f grows in the punctured neighborhood of c : ℝ at least as fast as 1 / (x - c), then it is not interval integrable on any nontrivial interval a..b, c ∈ [a, b].

@[simp]

The function λ x, (x - c)⁻¹ is integrable on a..b if and only if a = b or c ∉ [a, b].

@[simp]

The function λ x, x⁻¹ is integrable on a..b if and only if a = b or 0 ∉ [a, b].