English
Specialized tendsto for the range-based approximation in the Lp setting.
Русский
Специализированная сходимость для аппроксимации по диапазону в нулевой норме Lp.
LaTeX
$$$Tendsto( n \\mapsto (approxOn f fmeas (range f \\cup \\{0\\}) 0 (by simp) n) \\to f)$ в Lp-пространстве.$$
Lean4
/-- Any function in `ℒp` can be approximated by a simple function if `p < ∞`. -/
theorem _root_.MeasureTheory.MemLp.exists_simpleFunc_eLpNorm_sub_lt {E : Type*} [NormedAddCommGroup E] {f : β → E}
{μ : Measure β} (hf : MemLp f p μ) (hp_ne_top : p ≠ ∞) {ε : ℝ≥0∞} (hε : ε ≠ 0) :
∃ g : β →ₛ E, eLpNorm (f - ⇑g) p μ < ε ∧ MemLp g p μ :=
by
borelize E
let f' := hf.1.mk f
rsuffices ⟨g, hg, g_mem⟩ : ∃ g : β →ₛ E, eLpNorm (f' - ⇑g) p μ < ε ∧ MemLp g p μ
· refine ⟨g, ?_, g_mem⟩
suffices eLpNorm (f - ⇑g) p μ = eLpNorm (f' - ⇑g) p μ by rwa [this]
apply eLpNorm_congr_ae
filter_upwards [hf.1.ae_eq_mk] with x hx
simpa only [Pi.sub_apply, sub_left_inj] using hx
have hf' : MemLp f' p μ := hf.ae_eq hf.1.ae_eq_mk
have f'meas : Measurable f' := hf.1.measurable_mk
have : SeparableSpace (range f' ∪ {0} : Set E) :=
StronglyMeasurable.separableSpace_range_union_singleton hf.1.stronglyMeasurable_mk
rcases ((tendsto_approxOn_range_Lp_eLpNorm hp_ne_top f'meas hf'.2).eventually <| gt_mem_nhds hε.bot_lt).exists with
⟨n, hn⟩
rw [← eLpNorm_neg, neg_sub] at hn
exact ⟨_, hn, memLp_approxOn_range f'meas hf' _⟩
