English
If μ is finite on s, f is AEStronglyMeasurable μ, and f is almost everywhere bounded by M on s, then f is integrable on s with respect to μ.
Русский
Если μ ограничена на s, f AEStronglyMeasurable μ и ограничена на s почти везде сверху M, тогда f интегрируемо на s по μ.
LaTeX
$$$\\mu(s) \\neq \\infty \\land \\text{AEStronglyMeasurable}(f, \\mu) \\land (\\forall^\\mathrm{a.e.} a \\partial(\\mu\\restriction s), \\lVert f(a) \\rVert \\le M) \\Rightarrow \\operatorname{IntegrableOn}(f, s, \\mu).$$$
Lean4
/-- If `μ` is a measure finite at filter `l` and `f` is a function such that its norm is bounded
above at `l`, then `f` is integrable at `l`. -/
theorem integrableAtFilter {f : α → E} {l : Filter α} [IsMeasurablyGenerated l] (hfm : StronglyMeasurableAtFilter f l μ)
(hμ : μ.FiniteAtFilter l) (hf : l.IsBoundedUnder (· ≤ ·) (norm ∘ f)) : IntegrableAtFilter f l μ :=
by
obtain ⟨C, hC⟩ : ∃ C, ∀ᶠ s in l.smallSets, ∀ x ∈ s, ‖f x‖ ≤ C :=
hf.imp fun C hC => eventually_smallSets.2 ⟨_, hC, fun t => id⟩
rcases (hfm.eventually.and (hμ.eventually.and hC)).exists_measurable_mem_of_smallSets with ⟨s, hsl, hsm, hfm, hμ, hC⟩
refine ⟨s, hsl, ⟨hfm, .restrict_of_bounded hμ (C := C) ?_⟩⟩
rw [ae_restrict_eq hsm, eventually_inf_principal]
exact Eventually.of_forall hC
