English
If f is locally integrable and f = O[atTop] g with g integrable at atTop, then f is integrable.
Русский
Если f локально интегрируема и f = O[atTop] g, где g интегрируема на atTop, то f интегрируема.
LaTeX
$$$\\mathrm{LocallyIntegrable}\\, f \\,\\Rightarrow \\, \\mathrm{integrable\\_atTop}\\, g \\Rightarrow \\mathrm{Integrable}\\, f$$$
Lean4
/-- If `f` is locally integrable, and `f =O[atBot] g`, `f =O[atTop] g'` for some
`g`, `g'` integrable at `atBot` and `atTop` respectively, then `f` is integrable. -/
theorem integrable_of_isBigO_atBot_atTop [IsMeasurablyGenerated (atBot (α := α))]
[IsMeasurablyGenerated (atTop (α := α))] (hf : LocallyIntegrable f μ) (ho : f =O[atBot] g)
(hg : IntegrableAtFilter g atBot μ) (ho' : f =O[atTop] g') (hg' : IntegrableAtFilter g' atTop μ) : Integrable f μ :=
by
refine
integrable_iff_integrableAtFilter_atBot_atTop.mpr ⟨⟨ho.integrableAtFilter ?_ hg, ho'.integrableAtFilter ?_ hg'⟩, hf⟩
all_goals exact hf.aestronglyMeasurable.stronglyMeasurableAtFilter
