summable_mul_of_Lp_Lq — Mathlib

English

Let p,q be Hölder conjugates and f,g: ι → ℝ≥0 with f^p, g^q summable. Then f_i g_i is summable.

Русский

Пусть p,q сопряжены; если f^p и g^q суммируемы, то произведение 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 {f g : ι → ℝ≥0} {p q : ℝ} (hpq : p.HolderConjugate q) (hf : Summable fun i => f i ^ p)
    (hg : Summable fun i => g i ^ q) : Summable fun i => f i * g i :=
  (inner_le_Lp_mul_Lq_tsum hpq hf hg).1

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