English
Under the same finite-measure equality-on-sets hypothesis, the Lintegral of the norm of g on s is no greater than that of f on s.
Русский
При тех же предпосылках равенств интегралов по конечным мерам на множествах, линегральная норма на s не большe, чем у f на s.
LaTeX
$$$\\forall s,\\ MeasurableSet[m] s \\rightarrow μ s ≠ ∞ \\rightarrow \\int⁻ x in s, ‖g x‖ₑ ∂μ ≤ \\int⁻ x in s, ‖f x‖ₑ ∂μ$$$
Lean4
/-- In a locally compact space, any function in `ℒp` can be approximated by compactly supported
continuous functions when `0 < p < ∞`, version in terms of `∫`. -/
theorem exists_hasCompactSupport_integral_rpow_sub_le [R1Space α] [WeaklyLocallyCompactSpace α] [μ.Regular] {p : ℝ}
(hp : 0 < p) {f : α → E} (hf : MemLp f (ENNReal.ofReal p) μ) {ε : ℝ} (hε : 0 < ε) :
∃ g : α → E, HasCompactSupport g ∧ (∫ x, ‖f x - g x‖ ^ p ∂μ) ≤ ε ∧ Continuous g ∧ 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_hasCompactSupport_eLpNorm_sub_le ENNReal.coe_ne_top A with ⟨g, g_support, hg, g_cont, g_mem⟩
change eLpNorm _ (ENNReal.ofReal p) _ ≤ _ at hg
refine ⟨g, g_support, ?_, g_cont, 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
