Theorems · Theorem · functional analysis

LipschitzWith.memLp_comp_iff_of_antilipschitz

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

Defined in

Mathlib.MeasureTheory.Function.LpSpace.Basic

Cited by

3 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceNormedAddCommGroupNormedAddCommGroup