integrableOn_of_isBigO_atBot — Mathlib

English

If f is locally integrable on (−∞, a] and f = O[atBot] g with g integrable at atBot, then f is integrable on (−∞, a].

Русский

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

LaTeX

$$$\\mathrm{LocallyIntegrableOn} \\, f\\; (Iic\\; a) \\, \\Rightarrow \\, \\mathrm{integrableOn}\\, f\\, (Iic\\, a)$$$

Lean4

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

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