Theorems · Definition · functional analysis

MeasureTheory.MemLp

{α : Type u_1} →
  {ε : Type u_2} →
    {m0 : MeasurableSpace α} →
      [ENorm ε] →
        [TopologicalSpace ε] →
          (α → ε) → ENNReal → autoParam (MeasureTheory.Measure α) MeasureTheory.MemLp._auto_1 → Prop

The property that f : α → E is a.e. strongly measurable and (∫ ‖f a‖ ^ p ∂μ) ^ (1/p) is finite if p < ∞, or essSup ‖f‖ < ∞ if p = ∞.

Defined in

Mathlib.MeasureTheory.Function.LpSeminorm.Defs

Cited by

457 results in Mathlib

Foundations

Depth 202 from the axioms, rests on 5,268 definitions · uses propext, Classical.choice, Quot.sound

Assumes

ENormTopologicalSpace