Lp_add_le_tsum_of_nonneg' — Mathlib

English

If f,g ≥ 0 with HasSum of f^p and g^p equal to A^p and B^p, then there exists C ≥ 0 with C ≤ A+B and HasSum of (f+g)^p equal to C^p.

Русский

Пусть f,g ≥ 0 и HasSum(f^p)=A^p, HasSum(g^p)=B^p. Тогда существует C≥0 с C ≤ A+B и HasSum((f+g)^p)=C^p.

LaTeX

$$$\exists C\ge 0\; (C\le A+B) \land HasSum(\lambda i. (f_i+g_i)^p)\, C^p$$$

Lean4

theorem Lp_add_le_tsum_of_nonneg' (hp : 1 ≤ p) (hf : ∀ i, 0 ≤ f i) (hg : ∀ i, 0 ≤ g i)
    (hf_sum : Summable fun i => f i ^ p) (hg_sum : 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_of_nonneg hp hf hg hf_sum hg_sum).2

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