English
For MemLp elements, one can approximate by a bounded continuous function g in the eLp-norm with error ε, preserving membership in MemLp.
Русский
Для элемента MemLp можно аппроксимировать ограниченной непрерывной функцией g в eLp-норме с ошибкой ε, сохраняя принадлежность MemLp.
LaTeX
$$$\\exists g : α \\to E, HasCompactSupport g ∧ eLpNorm (f - g) p μ ≤ ε ∧ Continuous g ∧ MemLp g p μ$$$
Lean4
/-- Continuous functions are dense in `MeasureTheory.Lp`, `1 ≤ p < ∞`. This theorem assumes that
the domain is a compact space because otherwise `ContinuousMap.toLp` is undefined. Use
`BoundedContinuousFunction.toLp_denseRange` if the domain is not a compact space. -/
theorem toLp_denseRange [CompactSpace α] [μ.WeaklyRegular] [IsFiniteMeasure μ] (hp : p ≠ ∞) :
DenseRange (toLp p μ 𝕜 : C(α, E) →L[𝕜] Lp E p μ) :=
by
refine (BoundedContinuousFunction.toLp_denseRange _ _ 𝕜 hp).mono ?_
refine range_subset_iff.2 fun f ↦ ?_
exact ⟨f.toContinuousMap, rfl⟩
