English
For finite p and suitable μ, the sequence of eLpNorms of the difference between approxOn and f tends to 0 as n → ∞.
Русский
При конечном p и допустимом μ последовательность eLpNorm разности между approxOn и f стремится к нулю при n → ∞.
LaTeX
$$$\\text{Let } p\\neq \\infty. \\; Tendsto\\bigl( n \\mapsto \\|approxOn f hf s y_0 h_0 n - f\\|_{eLp}(p,\\mu) \\bigr)_{n\\to\\infty} = 0.$$$
Lean4
theorem tendsto_approxOn_Lp_eLpNorm [OpensMeasurableSpace E] {f : β → E} (hf : Measurable f) {s : Set E} {y₀ : E}
(h₀ : y₀ ∈ s) [SeparableSpace s] (hp_ne_top : p ≠ ∞) {μ : Measure β} (hμ : ∀ᵐ x ∂μ, f x ∈ closure s)
(hi : eLpNorm (fun x => f x - y₀) p μ < ∞) :
Tendsto (fun n => eLpNorm (⇑(approxOn f hf s y₀ h₀ n) - f) p μ) atTop (𝓝 0) :=
by
by_cases hp_zero : p = 0
· simpa only [hp_zero, eLpNorm_exponent_zero] using tendsto_const_nhds
have hp : 0 < p.toReal := toReal_pos hp_zero hp_ne_top
suffices Tendsto (fun n => ∫⁻ x, ‖approxOn f hf s y₀ h₀ n x - f x‖ₑ ^ p.toReal ∂μ) atTop (𝓝 0)
by
simp only [eLpNorm_eq_lintegral_rpow_enorm hp_zero hp_ne_top]
convert continuous_rpow_const.continuousAt.tendsto.comp this
simp [zero_rpow_of_pos (_root_.inv_pos.mpr hp)]
-- We simply check the conditions of the Dominated Convergence Theorem:
-- (1) The function "`p`-th power of distance between `f` and the approximation" is measurable
have hF_meas n : Measurable fun x => ‖approxOn f hf s y₀ h₀ n x - f x‖ₑ ^ p.toReal := by
simpa only [← edist_eq_enorm_sub] using
(approxOn f hf s y₀ h₀ n).measurable_bind (fun y x => edist y (f x) ^ p.toReal) fun y =>
(measurable_edist_right.comp hf).pow_const p.toReal
have h_bound n : (fun x ↦ ‖approxOn f hf s y₀ h₀ n x - f x‖ₑ ^ p.toReal) ≤ᵐ[μ] (‖f · - y₀‖ₑ ^ p.toReal) :=
.of_forall fun x => rpow_le_rpow (coe_mono (nnnorm_approxOn_le hf h₀ x n)) toReal_nonneg
have h_fin : (∫⁻ a : β, ‖f a - y₀‖ₑ ^ p.toReal ∂μ) ≠ ⊤ :=
(lintegral_rpow_enorm_lt_top_of_eLpNorm_lt_top hp_zero hp_ne_top hi).ne
have h_lim : ∀ᵐ a : β ∂μ, Tendsto (‖approxOn f hf s y₀ h₀ · a - f a‖ₑ ^ p.toReal) atTop (𝓝 0) :=
by
filter_upwards [hμ] with a ha
have : Tendsto (fun n => (approxOn f hf s y₀ h₀ n) a - f a) atTop (𝓝 (f a - f a)) :=
(tendsto_approxOn hf h₀ ha).sub tendsto_const_nhds
convert continuous_rpow_const.continuousAt.tendsto.comp (tendsto_coe.mpr this.nnnorm)
simp [zero_rpow_of_pos hp]
-- Then we apply the Dominated Convergence Theorem
simpa using tendsto_lintegral_of_dominated_convergence _ hF_meas h_bound h_fin h_lim
