English
For a fixed real p>0, and f,g: α→ℝ with finite-eLp distance, there exists a function g with compact support approximating f in the eLp-pseudonorm with error ε, under same finite-measure restrictions.
Русский
Для заданного p>0 существует приближение функции f непрерывной компактной опорой g в eLp-норме с допуском ε, при условиях равенства интегралов на множества конечной меры.
LaTeX
$$$\\exists g : α \\to E, HasCompactSupport g ∧ (∫ x ‑ ‖f x - g x‖^p ∂μ) ≤ ε ∧ Continuous g ∧ MemLp g (ENNReal.ofReal p) μ$$$
Lean4
/-- Any function in `ℒp` can be approximated by bounded continuous functions when `0 < p < ∞`,
version in terms of `∫`. -/
theorem exists_boundedContinuous_integral_rpow_sub_le [μ.WeaklyRegular] {p : ℝ} (hp : 0 < p) {f : α → E}
(hf : MemLp f (ENNReal.ofReal p) μ) {ε : ℝ} (hε : 0 < ε) :
∃ g : α →ᵇ E, (∫ x, ‖f x - g x‖ ^ p ∂μ) ≤ ε ∧ MemLp g (ENNReal.ofReal p) μ :=
by
have I : 0 < ε ^ (1 / p) := Real.rpow_pos_of_pos hε _
have A : ENNReal.ofReal (ε ^ (1 / p)) ≠ 0 := by simp only [Ne, ENNReal.ofReal_eq_zero, not_le, I]
have B : ENNReal.ofReal p ≠ 0 := by simpa only [Ne, ENNReal.ofReal_eq_zero, not_le] using hp
rcases hf.exists_boundedContinuous_eLpNorm_sub_le ENNReal.coe_ne_top A with ⟨g, hg, g_mem⟩
change eLpNorm _ (ENNReal.ofReal p) _ ≤ _ at hg
refine ⟨g, ?_, g_mem⟩
rwa [(hf.sub g_mem).eLpNorm_eq_integral_rpow_norm B ENNReal.coe_ne_top, ENNReal.ofReal_le_ofReal_iff I.le, one_div,
ENNReal.toReal_ofReal hp.le, Real.rpow_le_rpow_iff _ hε.le (inv_pos.2 hp)] at hg
positivity
