Theorems · Theorem · measure theory

MeasureTheory.MemLp.induction_stronglyMeasurable

∀ {α : Type u_1} {F : Type u_2} {p : ENNReal} [inst : NormedAddCommGroup F] {m m0 : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} [inst_1 : Fact (1 ≤ p)] [inst_2 : NormedSpace ℝ F],
  m ≤ m0 →
    p ≠ ⊤ →
      ∀ (P : (α → F) → Prop),
        (∀ (c : F) ⦃s : Set α⦄, MeasurableSet s → μ s < ⊤ → P (s.indicator fun x => c)) →
          (∀ ⦃f g : α → F⦄,
              Disjoint (Function.support f) (Function.support g) →
                MeasureTheory.MemLp f p μ →
                  MeasureTheory.MemLp g p μ →
                    MeasureTheory.StronglyMeasurable f → MeasureTheory.StronglyMeasurable g → P f → P g → P (f + g)) →
            IsClosed {f | P ↑↑↑f} →
              (∀ ⦃f g : α → F⦄, f =ᵐ[μ] g → MeasureTheory.MemLp f p μ → P f → P g) →
                ∀ ⦃f : α → F⦄, MeasureTheory.MemLp f p μ → MeasureTheory.AEStronglyMeasurable f μ → P f

To prove something for an arbitrary MemLp function a.e. strongly measurable with respect to a sub-σ-algebra m in a normed space, it suffices to show that * the property holds for (multiples of) characteristic functions which are measurable w.r.t. m; * is closed under addition; * the set of functions in the Lᵖ space strongly measurable w.r.t. m for which the property holds is closed. * the property is closed under the almost-everywhere equal relation.

Defined in

Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupFactNormedSpace