Theorems · Definition · functional analysis

MeasureTheory.eLpNorm

{α : Type u_1} →
  {ε : Type u_2} →
    [ENorm ε] →
      {x : MeasurableSpace α} →
        (α → ε) → ENNReal → autoParam (MeasureTheory.Measure α) MeasureTheory.eLpNorm._auto_1 → ENNReal

ℒp seminorm, equal to 0 for p=0, to (∫ ‖f a‖^p ∂μ) ^ (1/p) for 0 < p < ∞ and to essSup ‖f‖ μ for p = ∞.

Defined in

Mathlib.MeasureTheory.Function.LpSeminorm.Defs

Cited by

329 results in Mathlib

Foundations

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

Assumes

ENorm