exists_boundedContinuous_integral_sub_le

English

If f is integrable and p>0, then for any ε>0 there exists a compactly supported g with ∫ ‖f-g‖^p ≤ ε and g is integrable and boundedly continuous.

Русский

Если f интегрируема и p>0, то существует компактно поддерживаемая g с ∫ ‖f-g‖^p ≤ ε и g интегрируема и непрерывно ограничена.

LaTeX

$$$\\exists g : α \\to E, HasCompactSupport g ∧ (∫ x ‖f x - g x‖^p ∂μ) ≤ ε ∧ Continuous g ∧ MemLp g (ENNReal.ofReal p) μ$$$

Lean4

/-- Any integrable function can be approximated by bounded continuous functions,
version in terms of `∫`. -/
theorem exists_boundedContinuous_integral_sub_le [μ.WeaklyRegular] {f : α → E} (hf : Integrable f μ) {ε : ℝ}
    (hε : 0 < ε) : ∃ g : α →ᵇ E, (∫ x, ‖f x - g x‖ ∂μ) ≤ ε ∧ Integrable g μ :=
  by
  simp only [← memLp_one_iff_integrable, ← ENNReal.ofReal_one] at hf ⊢
  simpa using hf.exists_boundedContinuous_integral_rpow_sub_le zero_lt_one hε

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