English
The range of the map sending a bounded continuous function to its Lp-equivalence class is dense in Lp.
Русский
Область отображения, сопоставляющего непрерывной ограниченной функции её класс в Lp, плотно заполнена в Lp.
LaTeX
$$$DenseRange( toLp p μ 𝕜 : (α \\toᵇ E) →L[𝕜] Lp E p μ)$$$
Lean4
/-- Any function in `ℒp` can be approximated by bounded continuous functions when `p < ∞`,
version in terms of `eLpNorm`. -/
theorem exists_boundedContinuous_eLpNorm_sub_le [μ.WeaklyRegular] (hp : p ≠ ∞) {f : α → E} (hf : MemLp f p μ) {ε : ℝ≥0∞}
(hε : ε ≠ 0) : ∃ g : α →ᵇ E, eLpNorm (f - (g : α → E)) p μ ≤ ε ∧ MemLp g p μ :=
by
suffices H : ∃ g : α → E, eLpNorm (f - g) p μ ≤ ε ∧ Continuous g ∧ MemLp g p μ ∧ IsBounded (range g)
by
rcases H with ⟨g, hg, g_cont, g_mem, g_bd⟩
exact
⟨⟨⟨g, g_cont⟩, Metric.isBounded_range_iff.1 g_bd⟩, hg, g_mem⟩
-- It suffices to check that the set of functions we consider approximates characteristic
-- functions, is stable under addition and made 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, f_bd⟩ ⟨g_cont, g_mem, g_bd⟩
refine ⟨f_cont.add g_cont, f_mem.add g_mem, ?_⟩
let f' : α →ᵇ E := ⟨⟨f, f_cont⟩, Metric.isBounded_range_iff.1 f_bd⟩
let g' : α →ᵇ E := ⟨⟨g, g_cont⟩, Metric.isBounded_range_iff.1 g_bd⟩
exact (f' + g').isBounded_range
· exact fun f ⟨_, h, _⟩ => h.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_closed, μs⟩ : ∃ s, s ⊆ t ∧ IsClosed s ∧ μ (t \ s) < η :=
ht.exists_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
rcases exists_continuous_eLpNorm_sub_le_of_closed hp s_closed isOpen_univ (subset_univ _) hsμ.ne c δpos.ne' with
⟨f, f_cont, I2, f_bound, -, 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, ?_⟩
exact (BoundedContinuousFunction.ofNormedAddCommGroup f f_cont _ f_bound).isBounded_range
