Theorems · Theorem · measure theory

MeasureTheory.Lp.induction

∀ {α : Type u_1} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E] {p : ENNReal}
  {μ : MeasureTheory.Measure α} [_i : Fact (1 ≤ p)],
  p ≠ ⊤ →
    ∀ (motive : ↥(MeasureTheory.Lp E p μ) → Prop),
      (∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ⊤),
          motive ↑(MeasureTheory.Lp.simpleFunc.indicatorConst p hs ⋯ c)) →
        (∀ ⦃f g : α → E⦄ (hf : MeasureTheory.MemLp f p μ) (hg : MeasureTheory.MemLp g p μ),
            Disjoint (Function.support f) (Function.support g) →
              motive (MeasureTheory.MemLp.toLp f hf) →
                motive (MeasureTheory.MemLp.toLp g hg) →
                  motive (MeasureTheory.MemLp.toLp f hf + MeasureTheory.MemLp.toLp g hg)) →
          IsClosed {f | motive f} → ∀ (f : ↥(MeasureTheory.Lp E p μ)), motive f

To prove something for an arbitrary Lp function in a second countable Borel normed group, it suffices to show that * the property holds for (multiples of) characteristic functions; * is closed under addition; * the set of functions in Lp for which the property holds is closed.

Defined in

Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

Cited by

5 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceNormedAddCommGroupFact