summable_mul_of_Lp_Lq_of_nonneg — Mathlib

English

If hpq are Hölder conjugates and f,g are nonnegative with appropriate summability, then f_i g_i is summable.

Русский

Если hpq сопряжены и существуют соответствующие суммирования, то f_i g_i суммируемо.

LaTeX

$$$\text{Summable}(f_i g_i)$ при условии $\text{Summable}(f_i^p)$ и $\text{Summable}(g_i^q)$ и $p,q$ сопряжены.$$

Lean4

theorem summable_mul_of_Lp_Lq_of_nonneg (hpq : p.HolderConjugate q) (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 ^ q) : Summable fun i => f i * g i :=
  (inner_le_Lp_mul_Lq_tsum_of_nonneg hpq hf hg hf_sum hg_sum).1

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