integrable_of_isBigO_cocompact — Mathlib

English

If f is locally integrable, then certain Big‑O bounds imply integrability of f.

Русский

Если f локально интегрируема, то некоторые границы типа Big‑O приводят к интегрируемости f.

LaTeX

$$$\\mathrm{LocallyIntegrable}\\, f \\,\\Rightarrow \\, \\cdots$$$

Lean4

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

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