eLpNormEssSup_add_le — Mathlib

English

There exists a positive η such that, for measurable f,g with Lp-norms ≤ η, the Lp-norm of f+g is < δ.

Русский

Существует положительная η такая, что для измеримых f,g с ∥f∥_Lp ≤ η и ∥g∥_Lp ≤ η норма ∥f+g∥_Lp меньше заданного δ.

LaTeX

$$$\\exists \\eta>0,\\; \\forall f,g,\\; \\|f\\|_{L^p} \\le \\eta,\\; \\|g\\|_{L^p} \\le \\eta \\Rightarrow \\|f+g\\|_{L^p} < \\delta$$$

Lean4

theorem eLpNormEssSup_add_le : eLpNormEssSup (f + g) μ ≤ eLpNormEssSup f μ + eLpNormEssSup g μ :=
  by
  refine le_trans (essSup_mono_ae (Eventually.of_forall fun x => ?_)) (ENNReal.essSup_add_le _ _)
  simp_rw [Pi.add_apply]
  exact enorm_add_le _ _

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