eLpNorm'_add_le_of_le_one — Mathlib

English

If 0 ≤ q ≤ 1, then eLpNorm'(f+g) ≤ 2^{1/q - 1}(eLpNorm'(f) + eLpNorm'(g)).

Русский

Пусть 0 ≤ q ≤ 1. Тогда eLpNorm'(f+g) ≤ 2^{1/q - 1}(eLpNorm'(f) + eLpNorm'(g)).

LaTeX

$$$\\mathrm{eLpNorm}'(f+g, q, \\mu) \\le 2^{\\,1/q - 1}\\bigl( \\mathrm{eLpNorm}'(f, q, \\mu) + \\mathrm{eLpNorm}'(g, q, \\mu) \\bigr)$$$

Lean4

theorem eLpNorm'_add_le_of_le_one (hf : AEStronglyMeasurable f μ) (hq0 : 0 ≤ q) (hq1 : q ≤ 1) :
    eLpNorm' (f + g) q μ ≤ 2 ^ (1 / q - 1) * (eLpNorm' f q μ + eLpNorm' g q μ) :=
  calc
    (∫⁻ a, ‖(f + g) a‖ₑ ^ q ∂μ) ^ (1 / q) ≤ (∫⁻ a, (((‖f ·‖ₑ)) + (‖g ·‖ₑ)) a ^ q ∂μ) ^ (1 / q) :=
      by
      gcongr with a
      simp only [Pi.add_apply, enorm_add_le]
    _ ≤ (2 : ℝ≥0∞) ^ (1 / q - 1) * (eLpNorm' f q μ + eLpNorm' g q μ) :=
      ENNReal.lintegral_Lp_add_le_of_le_one hf.enorm hq0 hq1

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