mathlib3 documentation

analysis.special_functions.non_integrable

Non integrable functions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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].

theorem not_interval_integrable_of_sub_inv_is_O_punctured {F : Type u_2} [normed_add_comm_group F] {f : F} {a b c : } (hf : (λ (x : ), (x - c)⁻¹) =O[nhds_within c {c}] f) (hne : a b) (hc : c set.uIcc 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].