Theorems · Definition · functional analysis

LipschitzWith.compLp

{α : Type u_1} →
  {E : Type u_4} →
    {F : Type u_5} →
      {m : MeasurableSpace α} →
        {p : ENNReal} →
          {μ : MeasureTheory.Measure α} →
            [inst : NormedAddCommGroup E] →
              [inst_1 : NormedAddCommGroup F] →
                {g : E → F} →
                  {c : NNReal} → LipschitzWith c g → g 0 = 0 → ↥(MeasureTheory.Lp E p μ) → ↥(MeasureTheory.Lp F p μ)

When g is a Lipschitz function sending 0 to 0 and f is in Lp, then g ∘ f is well defined as an element of Lp.

Defined in

Mathlib.MeasureTheory.Function.LpSpace.Basic

Cited by

7 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedAddCommGroup