exists_boundedContinuous_lintegral_sub_le

English

Any Lp function can be approximated by a bounded continuous function in eLpNorm; the approximant g is bounded and continuous and lies in MemLp.

Русский

Любую функцию из Lp можно аппроксимировать ограниченной непрерывной функцией в eLpNorm; аппроксимирующая функция g ограничена, непрерывна и принадлежит MemLp.

LaTeX

$$$\\exists g : α \\to E, HasCompactSupport g \\land eLpNorm (f - g) p μ ≤ ε \\land Continuous g \\land MemLp g p μ$$$

Lean4

/-- Any integrable function can be approximated by bounded continuous functions,
version in terms of `∫⁻`. -/
theorem exists_boundedContinuous_lintegral_sub_le [μ.WeaklyRegular] {f : α → E} (hf : Integrable f μ) {ε : ℝ≥0∞}
    (hε : ε ≠ 0) : ∃ g : α →ᵇ E, ∫⁻ x, ‖f x - g x‖ₑ ∂μ ≤ ε ∧ Integrable g μ :=
  by
  simp only [← memLp_one_iff_integrable, ← eLpNorm_one_eq_lintegral_enorm] at hf ⊢
  exact hf.exists_boundedContinuous_eLpNorm_sub_le ENNReal.one_ne_top hε

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