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 #

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 โ„) [l.NeBot] [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 โ„) [l.NeBot] [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 โ„) [l.NeBot] [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, +โˆž).