norm_compLp_sub_le — Mathlib

English

If g ∈ Lp and L is a continuous linear map E→F, then applying L to f within MemLp yields MemLp in the target space.

Русский

Если g ∈ Lp и L — непрерывно линейное отображение E→F, то применение L к f сохраняет принадлежность к MemLp в целевом пространстве.

LaTeX

$$continuousLinearMap_comp$$

Lean4

theorem norm_compLp_sub_le (hg : LipschitzWith c g) (g0 : g 0 = 0) (f f' : Lp E p μ) :
    ‖hg.compLp g0 f - hg.compLp g0 f'‖ ≤ c * ‖f - f'‖ :=
  by
  apply Lp.norm_le_mul_norm_of_ae_le_mul
  filter_upwards [hg.coeFn_compLp g0 f, hg.coeFn_compLp g0 f', Lp.coeFn_sub (hg.compLp g0 f) (hg.compLp g0 f'),
    Lp.coeFn_sub f f'] with a ha1 ha2 ha3 ha4
  simp only [ha1, ha2, ha3, ha4, ← dist_eq_norm, Pi.sub_apply, Function.comp_apply]
  exact hg.dist_le_mul (f a) (f' a)

Похожие утверждения