English
Under integrability assumptions, the sequence of simple-function approximants built from the range of f converges to f in Lp norm.
Русский
При условии интегрируемости последовательность простых аппроксимаций, построенных по диапазону f, сходится к f в норме Lp.
LaTeX
$$$Tendsto\\bigl( n \\mapsto (memLp_approxOn_range fmeas hf n).toLp (approxOn f fmeas (range f \\cup \\{0\\}) 0 (by simp) n)\\bigr)_{n\\to\\infty} (\\mathcal{N}(hf.toLp f)).$$$
Lean4
theorem tendsto_approxOn_range_Lp [BorelSpace E] {f : β → E} [hp : Fact (1 ≤ p)] (hp_ne_top : p ≠ ∞) {μ : Measure β}
(fmeas : Measurable f) [SeparableSpace (range f ∪ {0} : Set E)] (hf : MemLp f p μ) :
Tendsto (fun n => (memLp_approxOn_range fmeas hf n).toLp (approxOn f fmeas (range f ∪ {0}) 0 (by simp) n)) atTop
(𝓝 (hf.toLp f)) :=
by simpa only [Lp.tendsto_Lp_iff_tendsto_eLpNorm''] using tendsto_approxOn_range_Lp_eLpNorm hp_ne_top fmeas hf.2
