English
A variant of tendsto_approxOn_Lp_eLpNorm where a range-based target is used; the result follows from the previous theorem by a simple specialization.
Русский
Вариант tendsto_approxOn_Lp_eLpNorm, где граница достигается через диапазон; следует из предыдущей теоремы.
LaTeX
$$$\\text{If } f:\\beta\\to E,\\; s=\\mathrm{range}(f)\\cup\\{0\},\\; \\text{then the same tendsto holds for the approximants onto } s.$$$
Lean4
theorem memLp_approxOn [BorelSpace E] {f : β → E} {μ : Measure β} (fmeas : Measurable f) (hf : MemLp f p μ) {s : Set E}
{y₀ : E} (h₀ : y₀ ∈ s) [SeparableSpace s] (hi₀ : MemLp (fun _ => y₀) p μ) (n : ℕ) :
MemLp (approxOn f fmeas s y₀ h₀ n) p μ :=
by
refine ⟨(approxOn f fmeas s y₀ h₀ n).aestronglyMeasurable, ?_⟩
suffices eLpNorm (fun x => approxOn f fmeas s y₀ h₀ n x - y₀) p μ < ⊤
by
have : MemLp (fun x => approxOn f fmeas s y₀ h₀ n x - y₀) p μ :=
⟨(approxOn f fmeas s y₀ h₀ n - const β y₀).aestronglyMeasurable, this⟩
convert eLpNorm_add_lt_top this hi₀
ext x
simp
have hf' : MemLp (fun x => ‖f x - y₀‖) p μ :=
by
have h_meas : Measurable fun x => ‖f x - y₀‖ :=
by
simp only [← dist_eq_norm]
exact (continuous_id.dist continuous_const).measurable.comp fmeas
refine ⟨h_meas.aemeasurable.aestronglyMeasurable, ?_⟩
rw [eLpNorm_norm]
convert eLpNorm_add_lt_top hf hi₀.neg with x
simp [sub_eq_add_neg]
have : ∀ᵐ x ∂μ, ‖approxOn f fmeas s y₀ h₀ n x - y₀‖ ≤ ‖‖f x - y₀‖ + ‖f x - y₀‖‖ :=
by
filter_upwards with x
convert norm_approxOn_y₀_le fmeas h₀ x n using 1
rw [Real.norm_eq_abs, abs_of_nonneg]
positivity
calc
eLpNorm (fun x => approxOn f fmeas s y₀ h₀ n x - y₀) p μ ≤ eLpNorm (fun x => ‖f x - y₀‖ + ‖f x - y₀‖) p μ :=
eLpNorm_mono_ae this
_ < ⊤ := eLpNorm_add_lt_top hf' hf'
