# mathlibdocumentation

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 #

• not_interval_integrable_of_tendsto_norm_at_top_of_deriv_is_O_punctured: if f tends to infinity along 𝓝[≠] c and f' = O(g) along the same filter, then g is not interval integrable on any nontrivial integral a..b, c ∈ [a, b].

• not_interval_integrable_of_tendsto_norm_at_top_of_deriv_is_O_filter: a version of not_interval_integrable_of_tendsto_norm_at_top_of_deriv_is_O_punctured that works for one-sided neighborhoods;

• not_interval_integrable_of_sub_inv_is_O_punctured: if 1 / (x - c) = O(f) as x → c, x ≠ c, then f is not interval integrable on any nontrivial interval a..b, c ∈ [a, b];

• interval_integrable_sub_inv_iff, interval_integrable_inv_iff: integrability conditions for (x - c)⁻¹ and x⁻¹.

## Tags #

integrable function

theorem not_interval_integrable_of_tendsto_norm_at_top_of_deriv_is_O_filter {E : Type u_1} {F : Type u_2} [normed_group E] [ E] [normed_group F] {f : → E} {g : → F} {a b : } (l : filter ) [l.ne_bot] (hl : b l) (hd : ∀ᶠ (x : ) in l, ) (hf : filter.tendsto (λ (x : ), f x) l filter.at_top) (hfg : g l) :

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.

theorem not_interval_integrable_of_tendsto_norm_at_top_of_deriv_is_O_within_diff_singleton {E : Type u_1} {F : Type u_2} [normed_group E] [ E] [normed_group F] {f : → E} {g : → F} {a b c : } (hne : a b) (hc : c b) (h_deriv : ∀ᶠ (x : ) in b \ {c}), ) (h_infty : filter.tendsto (λ (x : ), f x) b \ {c})) filter.at_top) (hg : g b \ {c}))) :

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.

theorem not_interval_integrable_of_tendsto_norm_at_top_of_deriv_is_O_punctured {E : Type u_1} {F : Type u_2} [normed_group E] [ E] [normed_group F] {f : → E} {g : → F} {a b c : } (h_deriv : ∀ᶠ (x : ) in {c}, ) (h_infty : filter.tendsto (λ (x : ), f x) {c}) filter.at_top) (hg : g {c})) (hne : a b) (hc : c 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_group F] {f : → F} {a b c : } (hf : asymptotics.is_O (λ (x : ), (x - c)⁻¹) f {c})) (hne : a b) (hc : c 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]
theorem interval_integrable_inv_iff {a b : } :
a b a = b 0 b

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