eLpNorm'_add_le — Mathlib

English

Similarly, if f ∈ MemLp(p,ν) on β, then the second-coordinate projection f∘Prod.snd ∈ MemLp(p,μ×ν) for finite μ.

Русский

Аналогично, если f ∈ MemLp(p,ν) на β, тогда f∘Prod.snd ∈ MemLp(p,μ×ν) при конечной μ.

LaTeX

$$$\\operatorname{MemLp}\\left(f\\circ \\mathrm{Prod.snd}\\right)\\,p\\,(\\mu\\times\\nu)$$$

Lean4

theorem eLpNorm'_add_le (hf : AEStronglyMeasurable f μ) (hg : AEStronglyMeasurable g μ) (hq1 : 1 ≤ q) :
    eLpNorm' (f + g) q μ ≤ 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]
    _ ≤ eLpNorm' f q μ + eLpNorm' g q μ := ENNReal.lintegral_Lp_add_le hf.enorm hg.enorm hq1

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