# Documentation

Mathlib.Analysis.SpecialFunctions.NonIntegrable

# Non integrable functions #

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

## Main results #

• not_intervalIntegrable_of_tendsto_norm_atTop_of_deriv_isBigO_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_intervalIntegrable_of_tendsto_norm_atTop_of_deriv_isBigO_filter: a version of not_intervalIntegrable_of_tendsto_norm_atTop_of_deriv_isBigO_punctured that works for one-sided neighborhoods;

• not_intervalIntegrable_of_sub_inv_isBigO_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];

• intervalIntegrable_sub_inv_iff, intervalIntegrable_inv_iff: integrability conditions for (x - c)⁻¹ and x⁻¹.

## Tags #

integrable function

theorem not_intervalIntegrable_of_tendsto_norm_atTop_of_deriv_isBigO_filter {E : Type u_1} {F : Type u_2} [] [] {f : E} {g : F} {a : } {b : } (l : ) [] [Filter.TendstoIxxClass Set.Icc l l] (hl : Set.uIcc a b l) (hd : ∀ᶠ (x : ) in l, ) (hf : Filter.Tendsto (fun x => f x) l Filter.atTop) (hfg : =O[l] g) :
¬IntervalIntegrable g MeasureTheory.volume a b

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_intervalIntegrable_of_tendsto_norm_atTop_of_deriv_isBigO_within_diff_singleton {E : Type u_1} {F : Type u_2} [] [] {f : E} {g : F} {a : } {b : } {c : } (hne : a b) (hc : c Set.uIcc a b) (h_deriv : ∀ᶠ (x : ) in nhdsWithin c (Set.uIcc a b \ {c}), ) (h_infty : Filter.Tendsto (fun x => f x) (nhdsWithin c (Set.uIcc a b \ {c})) Filter.atTop) (hg : =O[nhdsWithin c (Set.uIcc a b \ {c})] g) :
¬IntervalIntegrable g MeasureTheory.volume a b

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_intervalIntegrable_of_tendsto_norm_atTop_of_deriv_isBigO_punctured {E : Type u_1} {F : Type u_2} [] [] {f : E} {g : F} {a : } {b : } {c : } (h_deriv : ∀ᶠ (x : ) in nhdsWithin c {c}, ) (h_infty : Filter.Tendsto (fun x => f x) (nhdsWithin c {c}) Filter.atTop) (hg : =O[nhdsWithin c {c}] g) (hne : a b) (hc : c Set.uIcc a b) :
¬IntervalIntegrable g MeasureTheory.volume 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_intervalIntegrable_of_sub_inv_isBigO_punctured {F : Type u_2} {f : F} {a : } {b : } {c : } (hf : (fun x => (x - c)⁻¹) =O[nhdsWithin c {c}] f) (hne : a b) (hc : c Set.uIcc a b) :
¬IntervalIntegrable f MeasureTheory.volume 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]
theorem intervalIntegrable_sub_inv_iff {a : } {b : } {c : } :
IntervalIntegrable (fun x => (x - c)⁻¹) MeasureTheory.volume a b a = b ¬c Set.uIcc a b

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

@[simp]
theorem intervalIntegrable_inv_iff {a : } {b : } :
IntervalIntegrable (fun x => x⁻¹) MeasureTheory.volume a b a = b ¬0 Set.uIcc a b

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