integrable — Mathlib

English

If f = O[⊤] g and g is integrable at the top, then f is integrable at the top; similarly at the bottom with atBot.

Русский

Если f = O[⊤] g и g интегрируема на вершине, тогда f интегрируемо вверху; аналогично внизу с atBot.

LaTeX

$$$\\mathrm{IntegrableAtFilter}\\, f\\, \\text{atTop}$ when $f=O[\\text{atTop}] g$ and $IntegrableAtFilter g atTop$; similarly for atBot$$

Lean4

/-- Variant of `MeasureTheory.Integrable.mono` taking `f =O[⊤] (g)` instead of `‖f(x)‖ ≤ ‖g(x)‖` -/
theorem integrable (hfm : AEStronglyMeasurable f μ) (hf : f =O[⊤] g) (hg : Integrable g μ) : Integrable f μ :=
  by
  rewrite [← integrableAtFilter_top] at *
  exact hf.integrableAtFilter ⟨univ, univ_mem, hfm.restrict⟩ hg

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