toLp_denseRange — Mathlib

English

The image of bounded functions under the Lp-map is dense in Lp; bounded continuous functions approximate any Lp function.

Русский

Образ отображения Lp от ограниченных функций плотно заполняет Lp; ограниченные непрерывные функции аппроксимируют любую функцию в Lp.

LaTeX

$$$DenseRange( toLp p μ 𝕜 : (α \\toᵇ E) →L[𝕜] Lp E p μ)$$$

Lean4

theorem toLp_denseRange [μ.WeaklyRegular] [IsFiniteMeasure μ] (hp : p ≠ ∞) :
    DenseRange (toLp p μ 𝕜 : (α →ᵇ E) →L[𝕜] Lp E p μ) := by
  simpa only [← range_toLp p μ (𝕜 := 𝕜)] using MeasureTheory.Lp.boundedContinuousFunction_dense E μ hp

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