Theorems · Theorem · functional analysis

MeasureTheory.memLp_enorm_rpow_iff

∀ {α : Type u_1} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {ε : Type u_6}
  [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε] {q : ENNReal} {f : α → ε},
  MeasureTheory.AEStronglyMeasurable f μ →
    q ≠ 0 → q ≠ ⊤ → (MeasureTheory.MemLp (fun x => ‖f x‖ₑ ^ q.toReal) (p / q) μ ↔ MeasureTheory.MemLp f p μ)

Defined in

Mathlib.MeasureTheory.Function.LpSpace.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceContinuousENorm