English
If g is antilipschitz and uniformly continuous, the inverse implication holds: MemLp(f,p,μ) if MemLp(g∘f,p,μ) with antilipschitz conditions.
Русский
Если g анлипшиц и единообразно непрерывно, то эквивалентно: MemLp(f,p,μ) если MemLp(g∘f,p,μ) под условиями антипод Lip.
LaTeX
$$memLp_comp_antilipschitzWith$$
Lean4
theorem of_comp_antilipschitzWith {α E F} {K'} [MeasurableSpace α] {μ : Measure α} [NormedAddCommGroup E]
[NormedAddCommGroup F] {f : α → E} {g : E → F} (hL : MemLp (g ∘ f) p μ) (hg : UniformContinuous g)
(hg' : AntilipschitzWith K' g) (g0 : g 0 = 0) : MemLp f p μ :=
by
have A : ∀ x, ‖f x‖ ≤ K' * ‖g (f x)‖ := by
intro x
rw [← dist_zero_right, ← dist_zero_right, ← g0]
apply hg'.le_mul_dist
have B : AEStronglyMeasurable f μ := (hg'.isUniformEmbedding hg).isEmbedding.aestronglyMeasurable_comp_iff.1 hL.1
exact hL.of_le_mul B (Filter.Eventually.of_forall A)
