integrableAtFilter_of_tendsto_ae — Mathlib

English

Same as above: boundedness implies integrability on a set with finite measure.

Русский

То же: ограниченность по М требует интегрируемость на множестве с конечной мерой.

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

theorem integrableAtFilter_of_tendsto_ae {f : α → E} {l : Filter α} [IsMeasurablyGenerated l]
    (hfm : StronglyMeasurableAtFilter f l μ) (hμ : μ.FiniteAtFilter l) {b} (hf : Tendsto f (l ⊓ ae μ) (𝓝 b)) :
    IntegrableAtFilter f l μ :=
  (hμ.inf_of_left.integrableAtFilter (hfm.filter_mono inf_le_left) hf.norm.isBoundedUnder_le).of_inf_ae

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