eLpNorm_sub_le' — Mathlib

English

The difference bound: eLpNorm(f−g) ≤ LpAddConst(p) (eLpNorm f + eLpNorm g).

Русский

Построение границы разности: eLpNorm(f−g) ≤ LpAddConst(p) (eLpNorm f + eLpNorm g).

LaTeX

$$$\\mathrm{eLpNorm}(f-g,p,\\mu) \\le \\mathrm{LpAddConst}(p)\\, (\\mathrm{eLpNorm}(f,p,\\mu) + \\mathrm{eLpNorm}(g,p,\\mu))$$$

Lean4

theorem eLpNorm_sub_le' {f g : α → E} (hf : AEStronglyMeasurable f μ) (hg : AEStronglyMeasurable g μ) (p : ℝ≥0∞) :
    eLpNorm (f - g) p μ ≤ LpAddConst p * (eLpNorm f p μ + eLpNorm g p μ) := by
  simpa only [sub_eq_add_neg, eLpNorm_neg] using eLpNorm_add_le' hf hg.neg p

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