eLpNorm_add_le — Mathlib

English

LpAddConst(p) = 1 whenever 1 ≤ p.

Русский

LpAddConst(p) = 1 при 1 ≤ p.

LaTeX

$$$\\operatorname{LpAddConst}(p) = 1 \\quad \\text{ if } 1 \\le p$$$

Lean4

theorem eLpNorm_add_le (hf : AEStronglyMeasurable f μ) (hg : AEStronglyMeasurable g μ) (hp1 : 1 ≤ p) :
    eLpNorm (f + g) p μ ≤ eLpNorm f p μ + eLpNorm g p μ :=
  by
  by_cases hp0 : p = 0
  · simp [hp0]
  by_cases hp_top : p = ∞
  · simp [hp_top, eLpNormEssSup_add_le]
  have hp1_real : 1 ≤ p.toReal := by rwa [← ENNReal.toReal_one, ENNReal.toReal_le_toReal ENNReal.one_ne_top hp_top]
  repeat rw [eLpNorm_eq_eLpNorm' hp0 hp_top]
  exact eLpNorm'_add_le hf hg hp1_real

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