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 #

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

source

theorem not_interval_integrable_of_tendsto_norm_at_top_of_deriv_is_O_filter {E : Type u_1} {F : Type u_2} [normed_add_comm_group E] [normed_space ℝ E] [topological_space.second_countable_topology E] [complete_space E] [normed_add_comm_group F] {f : ℝ → E} {g : ℝ → F} {a b : ℝ} (l : filter ℝ) [l.ne_bot] [filter.tendsto_Ixx_class set.Icc l l] (hl : set.uIcc a b ∈ l) (hd : ∀ᶠ (x : ℝ) in l, differentiable_at ℝ f x) (hf : filter.tendsto (λ (x : ℝ), ‖f x‖) l filter.at_top) (hfg : deriv f =O[l] g) :

¬interval_integrable g measure_theory.measure_space.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.

source

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_add_comm_group E] [normed_space ℝ E] [topological_space.second_countable_topology E] [complete_space E] [normed_add_comm_group F] {f : ℝ → E} {g : ℝ → F} {a b c : ℝ} (hne : a ≠ b) (hc : c ∈ set.uIcc a b) (h_deriv : ∀ᶠ (x : ℝ) in nhds_within c (set.uIcc a b \ {c}), differentiable_at ℝ f x) (h_infty : filter.tendsto (λ (x : ℝ), ‖f x‖) (nhds_within c (set.uIcc a b \ {c})) filter.at_top) (hg : deriv f =O[nhds_within c (set.uIcc a b \ {c})] g) :

¬interval_integrable g measure_theory.measure_space.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.

source

theorem not_interval_integrable_of_tendsto_norm_at_top_of_deriv_is_O_punctured {E : Type u_1} {F : Type u_2} [normed_add_comm_group E] [normed_space ℝ E] [topological_space.second_countable_topology E] [complete_space E] [normed_add_comm_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 : deriv f =O[nhds_within c {c}ᶜ] g) (hne : a ≠ b) (hc : c ∈ set.uIcc a b) :

¬interval_integrable g measure_theory.measure_space.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].

source

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) :

¬interval_integrable f measure_theory.measure_space.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].

source

@[simp]

theorem interval_integrable_sub_inv_iff {a b c : ℝ} :

interval_integrable (λ (x : ℝ), (x - c)⁻¹) measure_theory.measure_space.volume a b ↔ a = b ∨ c ∉ set.uIcc a b

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

source

@[simp]

theorem interval_integrable_inv_iff {a b : ℝ} :

interval_integrable (λ (x : ℝ), x⁻¹) measure_theory.measure_space.volume a b ↔ a = b ∨ 0 ∉ set.uIcc a b

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