inner_le_Lp_mul_Lq_tsum' — Mathlib

English

For NNReal-valued f,g with p,q conjugate, the inner product sum over i is bounded by the same Hölder bound, written with tsum' notation.

Русский

Для NNReal-valued f,g с сопряжёнными p,q сумма внутреннего произведения ограничена тем же неравенством Хольдера, выраженным через tsum'.

LaTeX

$$$\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' {f g : ι → ℝ≥0} {p q : ℝ} (hpq : p.HolderConjugate q) (hf : Summable fun i => f i ^ p)
    (hg : 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 hpq hf hg).2

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