tendsto_approxOn_range_Lp_eLpNorm

English

A direct bound relating edist to y0 and edist to f is provided by edist_approxOn_y0_le.

Русский

Прямое неравенство, связывающее edist до y0 и edist до f, задается через edist_approxOn_y0_le.

LaTeX

$$$edist(y_0, approxOn f hf s y_0 h_0 n x) \\le edist(y_0, f x) + edist(y_0, f x).$$$

Lean4

theorem tendsto_approxOn_range_Lp_eLpNorm [BorelSpace E] {f : β → E} (hp_ne_top : p ≠ ∞) {μ : Measure β}
    (fmeas : Measurable f) [SeparableSpace (range f ∪ {0} : Set E)] (hf : eLpNorm f p μ < ∞) :
    Tendsto (fun n => eLpNorm (⇑(approxOn f fmeas (range f ∪ {0}) 0 (by simp) n) - f) p μ) atTop (𝓝 0) :=
  by
  refine tendsto_approxOn_Lp_eLpNorm fmeas _ hp_ne_top ?_ ?_
  · filter_upwards with x using subset_closure (by simp)
  · simpa using hf

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