integrableOn_of_isBigO_atTop — Mathlib

English

Analogous results hold at the top endpoint for LocallyIntegrable and LocallyIntegrableOn in the atTop region.

Русский

Аналогичные результаты справедливы для верха и для LocallyIntegrable и LocallyIntegrableOn в области atTop.

LaTeX

$$$\\mathrm{LocallyIntegrableOn}\\, f\\; (\\text{Ici a}) \\, \\Rightarrow \\, \\cdots$$$

Lean4

/-- If `f` is locally integrable on `[a, ∞)`, and `f =O[atTop] g`, for some
`g` integrable at `atTop`, then `f` is integrable on `[a, ∞)`. -/
theorem integrableOn_of_isBigO_atTop [IsMeasurablyGenerated (atTop (α := α))] (hf : LocallyIntegrableOn f (Ici a) μ)
    (ho : f =O[atTop] g) (hg : IntegrableAtFilter g atTop μ) : IntegrableOn f (Ici a) μ :=
  by
  refine integrableOn_Ici_iff_integrableAtFilter_atTop.mpr ⟨ho.integrableAtFilter ?_ hg, hf⟩
  exact ⟨Ici a, Ici_mem_atTop a, hf.aestronglyMeasurable⟩

Похожие утверждения