Theorems · Theorem · measure theory

MeasureTheory.MemLp.eLpNorm_eq_integral_rpow_norm

∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {H : Type u_6} [inst : NormedAddCommGroup H]
  {f : α → H} {p : ENNReal},
  p ≠ 0 →
    p ≠ ⊤ →
      MeasureTheory.MemLp f p μ →
        MeasureTheory.eLpNorm f p μ = ENNReal.ofReal ((∫ (a : α), ‖f a‖ ^ p.toReal ∂μ) ^ p.toReal⁻¹)

Defined in

Mathlib.MeasureTheory.Integral.Bochner.Basic

Cited by

4 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroup