Theorems · Theorem · measure theory

MeasureTheory.Integrable.induction

∀ {α : Type u_1} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E] {μ : MeasureTheory.Measure α}
  (P : (α → E) → Prop),
  (∀ (c : E) ⦃s : Set α⦄, MeasurableSet s → μ s < ⊤ → P (s.indicator fun x => c)) →
    (∀ ⦃f g : α → E⦄,
        Disjoint (Function.support f) (Function.support g) →
          MeasureTheory.Integrable f μ → MeasureTheory.Integrable g μ → P f → P g → P (f + g)) →
      IsClosed {f | P ↑↑f} →
        (∀ ⦃f g : α → E⦄, f =ᵐ[μ] g → MeasureTheory.Integrable f μ → P f → P g) →
          ∀ ⦃f : α → E⦄, MeasureTheory.Integrable f μ → P f

To prove something for an arbitrary integrable function in a normed group, it suffices to show that * the property holds for (multiples of) characteristic functions; * is closed under addition; * the set of functions in the L¹ space for which the property holds is closed. * the property is closed under the almost-everywhere equal relation. It is possible to make the hypotheses in the induction steps a bit stronger, and such conditions can be added once we need them (for example in h_add it is only necessary to consider the sum of a simple function with a multiple of a characteristic function and that the intersection of their images is a subset of {0}).

Defined in

Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

Cited by

8 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceNormedAddCommGroup