Theorems · Theorem · functional analysis

LipschitzWith.comp_memLp

∀ {p : ENNReal} {α : Type u_6} {E : Type u_7} {F : Type u_8} {K : NNReal} [inst : MeasurableSpace α]
  {μ : MeasureTheory.Measure α} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedAddCommGroup F] {f : α → E} {g : E → F},
  LipschitzWith K g → g 0 = 0 → MeasureTheory.MemLp f p μ → MeasureTheory.MemLp (g ∘ f) p μ

Defined in

Mathlib.MeasureTheory.Function.LpSpace.Basic

Cited by

6 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceNormedAddCommGroupNormedAddCommGroup