English
Same as above, but with Lintegral instead of integral, i.e., ∫⁻ ‖f−g‖^p ≤ ε and g in MemLp.
Русский
Аналогично, но с линтегралом: ∫⁻ ‖f−g‖^p ≤ ε и g ∈ MemLp.
LaTeX
$$$\\exists g : α \\to E, HasCompactSupport g ∧ (∫⁻ x, ‖f x - g x‖^p ∂μ) ≤ ε ∧ Continuous g ∧ MemLp g p μ$$$
Lean4
/-- A function in `Lp` can be approximated in `Lp` by continuous functions. -/
theorem boundedContinuousFunction_dense [SecondCountableTopologyEither α E] [Fact (1 ≤ p)] (hp : p ≠ ∞)
[μ.WeaklyRegular] : Dense (boundedContinuousFunction E p μ : Set (Lp E p μ)) :=
by
intro f
refine (mem_closure_iff_nhds_basis EMetric.nhds_basis_closed_eball).2 fun ε hε ↦ ?_
obtain ⟨g, hg, g_mem⟩ : ∃ g : α →ᵇ E, eLpNorm ((f : α → E) - (g : α → E)) p μ ≤ ε ∧ MemLp g p μ :=
(Lp.memLp f).exists_boundedContinuous_eLpNorm_sub_le hp hε.ne'
refine ⟨g_mem.toLp _, ⟨g, rfl⟩, ?_⟩
rwa [EMetric.mem_closedBall', ← Lp.toLp_coeFn f (Lp.memLp f), Lp.edist_toLp_toLp]
