Theorems · Definition · functional analysis

MeasureTheory.lpNorm

{α : Type u_1} →
  {E : Type u_4} → {m0 : MeasurableSpace α} → [NormedAddCommGroup E] → (α → E) → ENNReal → MeasureTheory.Measure α → ℝ

Real-valued ℒp seminorm, equal to 0 for p = 0, to (∫ ‖f a‖^p ∂μ) ^ p⁻¹ for 0 < p < ∞ and to essSup ‖f‖ μ for p = ∞. This is well-defined only if MemLp f p μ. Otherwise, it equals 0.

Defined in

Mathlib.MeasureTheory.Function.LpSeminorm.Defs

Cited by

50 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroup