integrableAtFilter_of_tendsto — Mathlib

English

If f is strongly measurable at filter l and μ finite at l, and f tends to b along l ∩ ae μ, then f is IntegrableAtFilter at l.

Русский

Если f сурово измерима по l, μ конечно на l, и f стремится к границе через l ∩ ae μ, тогда f интегрируемо по l.

LaTeX

$$$\\text{StronglyMeasurableAtFilter}(f, l, \\mu) \\land \\mu.FiniteAtFilter(l) \\land \\text{Tendsto}(f, l \\cap \\mathrm{ae}\\,\\mu, \\mathcal{N}(b)) \\Rightarrow \\operatorname{IntegrableAtFilter}(f, l, \\mu).$$$

Lean4

theorem integrableAtFilter_of_tendsto {f : α → E} {l : Filter α} [IsMeasurablyGenerated l]
    (hfm : StronglyMeasurableAtFilter f l μ) (hμ : μ.FiniteAtFilter l) {b} (hf : Tendsto f l (𝓝 b)) :
    IntegrableAtFilter f l μ :=
  hμ.integrableAtFilter hfm hf.norm.isBoundedUnder_le

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