# 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].

## Tags #

integrable function

theorem not_integrableOn_of_tendsto_norm_atTop_of_deriv_isBigO_filter_aux {E : Type u_1} {F : Type u_2} [] [] {f : โ โ E} {g : โ โ F} {k : } (l : ) [l.NeBot] [Filter.TendstoIxxClass Set.Icc l l] (hl : k โ l) (hd : โแถ  (x : โ) in l, ) (hf : Filter.Tendsto (fun (x : โ) => โf xโ) l Filter.atTop) (hfg : =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} [] {f : โ โ E} {g : โ โ F} {k : } (l : ) [l.NeBot] [Filter.TendstoIxxClass Set.Icc l l] (hl : k โ l) (hd : โแถ  (x : โ) in l, ) (hf : Filter.Tendsto (fun (x : โ) => โf xโ) l Filter.atTop) (hfg : =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} [] {f : โ โ E} {g : โ โ F} {a : โ} {b : โ} (l : ) [l.NeBot] [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 : โ) => ) 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 : โ) => ) (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 : โ) => ) (Set.Ioi a) MeasureTheory.volume

The function fun x โฆ xโปยน is not integrable on any interval (a, +โ).