eLpNorm_sub_le — Mathlib

English

Let f, g be AEStronglyMeasurable functions on α with respect to μ, and p ≥ 1. Then the eLp-norm of their difference is bounded by the sum of their eLp-norms: eLpNorm(f − g) p μ ≤ eLpNorm(f) p μ + eLpNorm(g) p μ.

Русский

Пусть f, g — AEStronglyMeasurable функции относительно μ, и p ≥ 1. Тогда eLp-норма разности не превосходит суммы eLp-норм двух функций: eLpNorm(f − g) p μ ≤ eLpNorm(f) p μ + eLpNorm(g) p μ.

LaTeX

$$$eLpNorm\,(f - g)\,p\,μ \leq eLpNorm\,f\,p\,μ + eLpNorm\,g\,p\,μ$$$

Lean4

theorem eLpNorm_sub_le {f g : α → E} (hf : AEStronglyMeasurable f μ) (hg : AEStronglyMeasurable g μ) (hp : 1 ≤ p) :
    eLpNorm (f - g) p μ ≤ eLpNorm f p μ + eLpNorm g p μ := by
  simpa [LpAddConst_of_one_le hp] using eLpNorm_sub_le' hf hg p

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