Theorems · Theorem · functional analysis

MeasureTheory.MemLp.enorm_rpow_div

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

Defined in

Mathlib.MeasureTheory.Function.LpSpace.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceContinuousENorm