integrable_of_isBigO_atBot — Mathlib

English

If f is locally integrable on [a, ∞) and f = O[atTop] g with g integrable atTop, then f is integrable on [a, ∞).

Русский

Если f локально интегрируема на [a, ∞) и f = O[atTop] g, где g интегрируема на atTop, то f интегрируема на [a, ∞).

LaTeX

$$$\\mathrm{LocallyIntegrableOn}\\ f\\ (Ici\\ a) \\Rightarrow \\mathrm{IntegrableOn}\\ f\\ (Ici\\ a)$$$

Lean4

/-- If `f` is locally integrable, `f` has a top element, and `f =O[atBot] g`, for some
`g` integrable at `atBot`, then `f` is integrable. -/
theorem integrable_of_isBigO_atBot [IsMeasurablyGenerated (atBot (α := α))] [OrderTop α] (hf : LocallyIntegrable f μ)
    (ho : f =O[atBot] g) (hg : IntegrableAtFilter g atBot μ) : Integrable f μ :=
  by
  refine integrable_iff_integrableAtFilter_atBot.mpr ⟨ho.integrableAtFilter ?_ hg, hf⟩
  exact hf.aestronglyMeasurable.stronglyMeasurableAtFilter

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