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