norm_Lp_toLp_restrict_le — Mathlib

English

The Lp-norms do not increase under restriction: the norm of the restricted element is at most the norm of the original element.

Русский

Нормы Lp не растут при ограничении: норма ограниченного элемента не превышает норму исходного элемента.

LaTeX

$$$$\\|((Lp.memLp f).restrict s).toLp f\\| ≤ \\|f\\|$$$$

Lean4

/-- For `f : Lp E p μ`, we can define an element of `Lp E p (μ.restrict s)` by
`(Lp.memLp f).restrict s).toLp f`. This map is non-expansive. -/
theorem norm_Lp_toLp_restrict_le (s : Set X) (f : Lp E p μ) : ‖((Lp.memLp f).restrict s).toLp f‖ ≤ ‖f‖ :=
  by
  rw [Lp.norm_def, Lp.norm_def, eLpNorm_congr_ae (MemLp.coeFn_toLp _)]
  refine ENNReal.toReal_mono (Lp.eLpNorm_ne_top _) ?_
  exact eLpNorm_mono_measure _ Measure.restrict_le_self

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