tendsto_approxOn_range_L1_enorm — Mathlib

English

If the function is integrable, the L1-enorm of the difference between the range-based approxOn and f tends to zero.

Русский

Если функция интегрируема, то линегральная норма различия между аппроксимацией по диапазону и f сходится к нулю.

LaTeX

$$$Tendsto( n \\mapsto \\int \\! \\|approxOn f fmeas (range f \\cup \\{0\\}) 0 (by simp) n x - f x\\| dx )_{n\\to\\infty} = 0.$$$

Lean4

theorem tendsto_approxOn_range_L1_enorm [OpensMeasurableSpace E] {f : β → E} {μ : Measure β}
    [SeparableSpace (range f ∪ {0} : Set E)] (fmeas : Measurable f) (hf : Integrable f μ) :
    Tendsto (fun n => ∫⁻ x, ‖approxOn f fmeas (range f ∪ {0}) 0 (by simp) n x - f x‖ₑ ∂μ) atTop (𝓝 0) :=
  by
  apply tendsto_approxOn_L1_enorm fmeas
  · filter_upwards with x using subset_closure (by simp)
  · simpa using hf.2

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