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_integrableOn_of_tendsto_norm_atTop_of_deriv_isBigO_filter_aux {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [CompleteSpace E] {f : ℝ → E} {g : ℝ → F} {k : Set ℝ} (l : Filter ℝ) [Filter.NeBot l] [Filter.TendstoIxxClass Set.Icc l l] (hl : k ∈ l) (hd : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x) (hf : Filter.Tendsto (fun (x : ℝ) => ‖f x‖) l Filter.atTop) (hfg : deriv f =O[l] g) : ¬MeasureTheory.IntegrableOn g k MeasureTheory.volume

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 set k belonging to l. Auxiliary version assuming that E is complete.

theorem not_integrableOn_of_tendsto_norm_atTop_of_deriv_isBigO_filter {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] {f : ℝ → E} {g : ℝ → F} {k : Set ℝ} (l : Filter ℝ) [Filter.NeBot l] [Filter.TendstoIxxClass Set.Icc l l] (hl : k ∈ l) (hd : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x) (hf : Filter.Tendsto (fun (x : ℝ) => ‖f x‖) l Filter.atTop) (hfg : deriv f =O[l] g) : ¬MeasureTheory.IntegrableOn g k MeasureTheory.volume

theorem not_intervalIntegrable_of_tendsto_norm_atTop_of_deriv_isBigO_filter {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] {f : ℝ → E} {g : ℝ → F} {a : ℝ} {b : ℝ} (l : Filter ℝ) [Filter.NeBot l] [Filter.TendstoIxxClass Set.Icc l l] (hl : Set.uIcc a b ∈ l) (hd : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x) (hf : Filter.Tendsto (fun (x : ℝ) => ‖f x‖) l Filter.atTop) (hfg : deriv f =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} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] {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}), DifferentiableAt ℝ f x) (h_infty : Filter.Tendsto (fun (x : ℝ) => ‖f x‖) (nhdsWithin c (Set.uIcc a b \ {c})) Filter.atTop) (hg : deriv f =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} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] {f : ℝ → E} {g : ℝ → F} {a : ℝ} {b : ℝ} {c : ℝ} (h_deriv : ∀ᶠ (x : ℝ) in nhdsWithin c {c}ᶜ, DifferentiableAt ℝ f x) (h_infty : Filter.Tendsto (fun (x : ℝ) => ‖f x‖) (nhdsWithin c {c}ᶜ) Filter.atTop) (hg : deriv f =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} [NormedAddCommGroup F] {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].

theorem not_IntegrableOn_Ici_inv {a : ℝ} : ¬MeasureTheory.IntegrableOn (fun (x : ℝ) => x⁻¹) (Set.Ici a) MeasureTheory.volume

The function fun x ↦ x⁻¹ is not integrable on any interval [a, +∞).

theorem not_IntegrableOn_Ioi_inv {a : ℝ} : ¬MeasureTheory.IntegrableOn (fun (x : ℝ) => x⁻¹) (Set.Ioi a) MeasureTheory.volume

The function fun x ↦ x⁻¹ is not integrable on any interval (a, +∞).