tendsto_integral_approxOn_of_measurable_of_range_subset

English

If the range of f together with 0 lies in a separable set s, then the approximating integrals via approxOn converge to the integral of f.

Русский

Если диапазон значений f вместе с нулём лежит в сепарабельном множестве s, то аппроксимационные интегралы сходятся к интегралу f.

LaTeX

$$$\\text{If }\\mathrm{range}(f)\\cup\\{0\\}\\subseteq s\\text{ and }f\\text{ is integrable and measurable, then }\\lim_{n\\to\\infty} (\\text{approxOn}(f,fmeas,s,0,n))_\\text{integral} = \\int f.$$$

Lean4

theorem tendsto_integral_approxOn_of_measurable_of_range_subset [MeasurableSpace E] [BorelSpace E] {f : α → E}
    (fmeas : Measurable f) (hf : Integrable f μ) (s : Set E) [SeparableSpace s] (hs : range f ∪ {0} ⊆ s) :
    Tendsto (fun n => (SimpleFunc.approxOn f fmeas s 0 (hs <| by simp) n).integral μ) atTop (𝓝 <| ∫ x, f x ∂μ) :=
  by
  apply tendsto_integral_approxOn_of_measurable hf fmeas _ _ (integrable_zero _ _ _)
  exact
    Eventually.of_forall fun x =>
      subset_closure
        (hs (Set.mem_union_left _ (mem_range_self _)))
          -- We redeclare `E` here to temporarily avoid
          -- the `[CompleteSpace E]` and `[NormedSpace ℝ E]` instances.

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