Theorems · Definition · measure theory

MeasureTheory.lpMeas

{α : Type u_1} →
  (F : Type u_2) →
    (𝕜 : Type u_3) →
      [inst : RCLike 𝕜] →
        [inst_1 : NormedAddCommGroup F] →
          [inst_2 : NormedSpace 𝕜 F] →
            MeasurableSpace α →
              [inst_3 : MeasurableSpace α] →
                (p : ENNReal) → (μ : MeasureTheory.Measure α) → Submodule 𝕜 ↥(MeasureTheory.Lp F p μ)

lpMeas F 𝕜 m p μ is the subspace of Lp F p μ containing functions f verifying AEStronglyMeasurable[m] f μ, i.e. functions which are μ-a.e. equal to an m-strongly measurable function.

Defined in

Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable

Cited by

46 results in Mathlib

Foundations

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

Assumes

RCLikeNormedAddCommGroupNormedSpaceMeasurableSpace