English
The essential supremum norm is subadditive: eLpNormEssSup(f+g) ≤ eLpNormEssSup f + eLpNormEssSup g.
Русский
EssSup-норма подадитивна: eLpNormEssSup(f+g) ≤ eLpNormEssSup f + eLpNormEssSup g.
LaTeX
$$$\\mathrm{eLpNormEssSup}(f+g,\\mu) \\le \\mathrm{eLpNormEssSup}(f,\\mu) + \\mathrm{eLpNormEssSup}(g,\\mu)$$$
Lean4
theorem eLpNorm_add_le' (hf : AEStronglyMeasurable f μ) (hg : AEStronglyMeasurable g μ) (p : ℝ≥0∞) :
eLpNorm (f + g) p μ ≤ LpAddConst p * (eLpNorm f p μ + eLpNorm g p μ) :=
by
rcases eq_or_ne p 0 with (rfl | hp)
· simp only [eLpNorm_exponent_zero, add_zero, mul_zero, le_zero_iff]
rcases lt_or_ge p 1 with (h'p | h'p)
· simp only [eLpNorm_eq_eLpNorm' hp (h'p.trans ENNReal.one_lt_top).ne]
convert eLpNorm'_add_le_of_le_one hf ENNReal.toReal_nonneg _
· have : p ∈ Set.Ioo (0 : ℝ≥0∞) 1 := ⟨hp.bot_lt, h'p⟩
simp only [LpAddConst, if_pos this]
· simpa using ENNReal.toReal_mono ENNReal.one_ne_top h'p.le
· simpa [LpAddConst_of_one_le h'p] using eLpNorm_add_le hf hg h'p
