exists_hasCompactSupport_integral_sub_le

English

Continuous bounded functions are dense in Lp: any Lp function can be approximated in Lp by bounded continuous functions when 1 ≤ p < ∞.

Русский

Плотно ограниченные непрерывные функции плотны в Lp: любую функцию в Lp можно приблизить в Lp-плоскости непрерывными ограниченными функциями.

LaTeX

$$$\\text{Dense}(\\text{boundedContinuousFunction } E p μ : Set (Lp E p μ))$$$

Lean4

/-- In a locally compact space, any integrable function can be approximated by compactly supported
continuous functions, version in terms of `∫`. -/
theorem exists_hasCompactSupport_integral_sub_le [R1Space α] [WeaklyLocallyCompactSpace α] [μ.Regular] {f : α → E}
    (hf : Integrable f μ) {ε : ℝ} (hε : 0 < ε) :
    ∃ g : α → E, HasCompactSupport g ∧ (∫ x, ‖f x - g x‖ ∂μ) ≤ ε ∧ Continuous g ∧ Integrable g μ :=
  by
  simp only [← memLp_one_iff_integrable, ← ENNReal.ofReal_one] at hf ⊢
  simpa using hf.exists_hasCompactSupport_integral_rpow_sub_le zero_lt_one hε

Похожие утверждения