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.

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] [normed_space E] [topological_space.second_countable_topology E] [complete_space E] [normed_group F] {f : → E} {g : → F} {a b c : } (h_deriv : ∀ᶠ (x : ) in nhds_within c {c}, differentiable_at f x) (h_infty : filter.tendsto (λ (x : ), f x) (nhds_within c {c}) filter.at_top) (hg : asymptotics.is_O (deriv f) g (nhds_within c {c})) (hne : a b) (hc : c set.interval 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_group F] {f : → F} {a b c : } (hf : asymptotics.is_O (λ (x : ), (x - c)⁻¹) f (nhds_within c {c})) (hne : a b) (hc : c set.interval 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].