tendsto_approxOn_L1_enorm — Mathlib

English

The L1-enorm (integral of the absolute difference) between approxOn and f tends to 0 when the measure μ is used and the function is integrable.

Русский

Норма L1 (линтеграл абсолютной разности) между approxOn и f сходится к нулю при интегрируемости и выбранной мере μ.

LaTeX

$$$\\text{Tendsto}\\bigl( n \\mapsto \\int^{\\-}\\|approxOn f hf s y_0 h_0 n x - f x\\|\\ d\\mu(x)\\bigr)_{n\\to\\infty} = 0.$$$

Lean4

theorem tendsto_approxOn_L1_enorm [OpensMeasurableSpace E] {f : β → E} (hf : Measurable f) {s : Set E} {y₀ : E}
    (h₀ : y₀ ∈ s) [SeparableSpace s] {μ : Measure β} (hμ : ∀ᵐ x ∂μ, f x ∈ closure s)
    (hi : HasFiniteIntegral (fun x => f x - y₀) μ) :
    Tendsto (fun n => ∫⁻ x, ‖approxOn f hf s y₀ h₀ n x - f x‖ₑ ∂μ) atTop (𝓝 0) := by
  simpa [eLpNorm_one_eq_lintegral_enorm] using
    tendsto_approxOn_Lp_eLpNorm hf h₀ one_ne_top hμ (by simpa [eLpNorm_one_eq_lintegral_enorm] using hi)

Похожие утверждения