dominated integrability

Stream: Is there code for X?

[Alex Kontorovich]

I can't seem to find this in the library: If g is integrable on $(0,\infty)$, say, and $f=O(g)$ atTop, then f is integrable:

import Mathlib.MeasureTheory.Integral.IntegrableOn
import Mathlib.Order.Filter.AtTopBot
import Mathlib.MeasureTheory.Measure.Haar.OfBasis

open MeasureTheory Set Filter

example (f g : ℝ → ℝ) (g_integrableOn : IntegrableOn g (Ioi (0 : ℝ)))
    (f_le_g_atTop : f =O[atTop] g) : IntegrableOn f (Ioi (0 : ℝ)) := by
  sorry

Any hints would be much appreciated; thanks!

[Mitchell Lee]

I don't think this is true because you need a hypothesis about the behavior of f on atBot as well.

[Mitchell Lee]

Also, that f is locally integrable.

[Alex Kontorovich]

Sure, not atBot I think (since I'm only integrating down to 0), but local integrability might be needed. Is there some theorem like this one, with sufficient hypotheses?... Thanks!

[Mitchell Lee]

What about this?

[Mitchell Lee]

https://leanprover-community.github.io/mathlib4_docs////Mathlib/MeasureTheory/Integral/Asymptotics.html#Asymptotics.IsBigO.integrable

[Mitchell Lee]

Or this one: docs#MeasureTheory.LocallyIntegrable.integrable_of_isBigO_cocompact

[Alex Kontorovich]

Great, thanks! This should do what I needed: docs#MeasureTheory.LocallyIntegrableOn.integrableOn_of_isBigO_atTop