Theorems · Theorem · measure theory

MeasureTheory.MemLp.exists_simpleFunc_eLpNorm_sub_lt

∀ {β : Type u_2} [inst : MeasurableSpace β] {p : ENNReal} {E : Type u_7} [inst_1 : NormedAddCommGroup E] {f : β → E}
  {μ : MeasureTheory.Measure β},
  MeasureTheory.MemLp f p μ →
    p ≠ ⊤ → ∀ {ε : ENNReal}, ε ≠ 0 → ∃ g, MeasureTheory.eLpNorm (f - ⇑g) p μ < ε ∧ MeasureTheory.MemLp (⇑g) p μ

Any function in ℒp can be approximated by a simple function if p < ∞.

Defined in

Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

Cited by

2 results in Mathlib

Foundations

Depth 221 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

MeasurableSpaceNormedAddCommGroup