inner_le_Lp_mul_Lq_tsum_of_nonneg'

English

Variant for Real-valued nonnegative functions with HasSum and tsum versions.

Русский

Вариант для вещественных неотрицательных функций с HasSum и tsum-версиями.

LaTeX

$$$\text{Summable}(f_i g_i) \quad\text{and}\quad \sum_i f_i g_i \le (\sum_i f_i^p)^{1/p} (\sum_i g_i^q)^{1/q}$$$

Lean4

theorem inner_le_Lp_mul_Lq_tsum_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) :
    ∑' i, f i * g i ≤ (∑' i, f i ^ p) ^ (1 / p) * (∑' i, g i ^ q) ^ (1 / q) :=
  (inner_le_Lp_mul_Lq_tsum_of_nonneg hpq hf hg hf_sum hg_sum).2

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