English
If a vector‑valued function f is O[l] (g) and g is integrable at l, then f is integrable at l (under suitable measurability assumptions).
Русский
Если функция f есть O[l](g) и g интегрируема на l, то f интегрируема на l (при подходящих предположениях measurability).
LaTeX
$$$\\text{IntegrableAtFilter } f\\; l\\; \\mu$ under $f=O[l]\,g$, $hg$ integrable$$
Lean4
/-- If `f = O[l] g` on measurably generated `l`, `f` is strongly measurable at `l`,
and `g` is integrable at `l`, then `f` is integrable at `l`. -/
theorem integrableAtFilter [IsMeasurablyGenerated l] (hf : f =O[l] g) (hfm : StronglyMeasurableAtFilter f l μ)
(hg : IntegrableAtFilter g l μ) : IntegrableAtFilter f l μ :=
by
obtain ⟨C, hC⟩ := hf.bound
obtain ⟨s, hsl, hsm, hfg, hf, hg⟩ :=
(hC.smallSets.and <| hfm.eventually.and hg.eventually).exists_measurable_mem_of_smallSets
refine ⟨s, hsl, (hg.norm.const_mul C).mono hf ?_⟩
refine (ae_restrict_mem hsm).mono fun x hx ↦ ?_
exact (hfg x hx).trans (le_abs_self _)
