Lp_add_le_tsum' — Mathlib

English

Same as Minkowski inequality for tsum with a trailing prime variant.

Русский

То же самое, что и неравенство Минковского для сумм в бесконечности, вариант с апострофом.

LaTeX

$$$\left(\sum_{i} (f_i+g_i)^p\right)^{1/p} \le \left(\sum_i f_i^p\right)^{1/p} + \left(\sum_i g_i^p\right)^{1/p}$$$

Lean4

theorem Lp_add_le_tsum' {f g : ι → ℝ≥0} {p : ℝ} (hp : 1 ≤ p) (hf : Summable fun i => f i ^ p)
    (hg : Summable fun i => g i ^ p) :
    (∑' i, (f i + g i) ^ p) ^ (1 / p) ≤ (∑' i, f i ^ p) ^ (1 / p) + (∑' i, g i ^ p) ^ (1 / p) :=
  (Lp_add_le_tsum hp hf hg).2

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