English
In a locally compact space, any function in Lp can be approximated by a compactly supported continuous function in the eLp-norm, given p<∞, with the approximant g having compact support, and f−g small in eLp-norm; moreover g is continuous and belongs to MemLp.
Русский
В локально компактном пространстве любую функцию в Lp можно приблизить компактно поддерживаемой непрерывной функцией в eLp-норме, при p<∞; аппроксимирующая функция g имеет компактную опору, непрерывна и принадлежит MemLp.
LaTeX
$$$\\exists g:\\alpha \\to E\\; HasCompactSupport g \\land eLpNorm (f - g) p μ ≤ ε \\land Continuous g \\land MemLp g p μ$$$
Lean4
/-- In a locally compact space, any function in `ℒp` can be approximated by compactly supported
continuous functions when `p < ∞`, version in terms of `eLpNorm`. -/
theorem exists_hasCompactSupport_eLpNorm_sub_le [R1Space α] [WeaklyLocallyCompactSpace α] [μ.Regular] (hp : p ≠ ∞)
{f : α → E} (hf : MemLp f p μ) {ε : ℝ≥0∞} (hε : ε ≠ 0) :
∃ g : α → E, HasCompactSupport g ∧ eLpNorm (f - g) p μ ≤ ε ∧ Continuous g ∧ MemLp g p μ :=
by
suffices H : ∃ g : α → E, eLpNorm (f - g) p μ ≤ ε ∧ Continuous g ∧ MemLp g p μ ∧ HasCompactSupport g
by
rcases H with ⟨g, hg, g_cont, g_mem, g_support⟩
exact
⟨g, g_support, hg, g_cont, g_mem⟩
-- It suffices to check that the set of functions we consider approximates characteristic
-- functions, is stable under addition and consists of ae strongly measurable functions.
-- First check the latter easy facts.
apply hf.induction_dense hp _ _ _ _ hε
rotate_left
-- stability under addition
· rintro f g ⟨f_cont, f_mem, hf⟩ ⟨g_cont, g_mem, hg⟩
exact
⟨f_cont.add g_cont, f_mem.add g_mem, hf.add hg⟩
-- ae strong measurability
· rintro f ⟨_f_cont, f_mem, _hf⟩
exact f_mem.aestronglyMeasurable
intro c t ht htμ ε hε
rcases exists_Lp_half E μ p hε with ⟨δ, δpos, hδ⟩
obtain ⟨η, ηpos, hη⟩ : ∃ η : ℝ≥0, 0 < η ∧ ∀ s : Set α, μ s ≤ η → eLpNorm (s.indicator fun _x => c) p μ ≤ δ :=
exists_eLpNorm_indicator_le hp c δpos.ne'
have hη_pos' : (0 : ℝ≥0∞) < η := ENNReal.coe_pos.2 ηpos
obtain ⟨s, st, s_compact, s_closed, μs⟩ : ∃ s, s ⊆ t ∧ IsCompact s ∧ IsClosed s ∧ μ (t \ s) < η :=
ht.exists_isCompact_isClosed_diff_lt htμ.ne hη_pos'.ne'
have hsμ : μ s < ∞ := (measure_mono st).trans_lt htμ
have I1 : eLpNorm ((s.indicator fun _y => c) - t.indicator fun _y => c) p μ ≤ δ :=
by
rw [← eLpNorm_neg, neg_sub, ← indicator_diff st]
exact hη _ μs.le
obtain ⟨k, k_compact, sk⟩ : ∃ k : Set α, IsCompact k ∧ s ⊆ interior k := exists_compact_superset s_compact
rcases exists_continuous_eLpNorm_sub_le_of_closed hp s_closed isOpen_interior sk hsμ.ne c δpos.ne' with
⟨f, f_cont, I2, _f_bound, f_support, f_mem⟩
have I3 : eLpNorm (f - t.indicator fun _y => c) p μ ≤ ε :=
by
convert
(hδ _ _ (f_mem.aestronglyMeasurable.sub (aestronglyMeasurable_const.indicator s_closed.measurableSet))
((aestronglyMeasurable_const.indicator s_closed.measurableSet).sub (aestronglyMeasurable_const.indicator ht))
I2 I1).le using
2
simp only [sub_add_sub_cancel]
refine ⟨f, I3, f_cont, f_mem, HasCompactSupport.intro k_compact fun x hx => ?_⟩
rw [← Function.notMem_support]
contrapose! hx
exact interior_subset (f_support hx)
