English
If f ∈ MemLp and g is Lipschitz, then g∘f ∈ MemLp; moreover, one has a bound for the Lp-norm of the composition in terms of the Lp-norm of f and the Lipschitz constant.
Русский
Если f ∈ MemLp и g Lipschitz, тогда g∘f ∈ MemLp; более того, нормa Lp композиции контролируется константой липшиц.
LaTeX
$$comp_memLp$$
Lean4
/-- 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`. -/
def compLp (hg : LipschitzWith c g) (g0 : g 0 = 0) (f : Lp E p μ) : Lp F p μ :=
⟨AEEqFun.comp g hg.continuous (f : α →ₘ[μ] E),
by
suffices ∀ᵐ x ∂μ, ‖AEEqFun.comp g hg.continuous (f : α →ₘ[μ] E) x‖ ≤ c * ‖f x‖ from Lp.mem_Lp_of_ae_le_mul this
filter_upwards [AEEqFun.coeFn_comp g hg.continuous (f : α →ₘ[μ] E)] with a ha
simp only [ha]
rw [← dist_zero_right, ← dist_zero_right, ← g0]
exact hg.dist_le_mul (f a) 0⟩
