memLp_approxOn_range — Mathlib

English

If p ≤ ∞ and the function f has finite eLpNorm, then the approximants based on the range of f converge to f in eLpNorm.

Русский

Если p ограничено сверху и eLpNorm(f) < ∞, то аппроксимации по диапазону сходятся к f в eLpNorm.

LaTeX

$$$Tendsto\\ bigl( n \\mapsto eLpNorm( f - approxOn f hf (range f \\cup \\{0\\}) 0 (by simp) n) \\bigr)_{n\\to\\infty} = 0.$$$

Lean4

theorem memLp_approxOn_range [BorelSpace E] {f : β → E} {μ : Measure β} (fmeas : Measurable f)
    [SeparableSpace (range f ∪ {0} : Set E)] (hf : MemLp f p μ) (n : ℕ) :
    MemLp (approxOn f fmeas (range f ∪ {0}) 0 (by simp) n) p μ :=
  memLp_approxOn fmeas hf (y₀ := 0) (by simp) MemLp.zero n

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