tsum_mul_le_mul_norm' — Mathlib

English

A variant of Hölder bound: under Holder conjugacy, ∑' i, ‖f_i‖·‖g_i‖ ≤ ‖f‖·‖g‖.

Русский

Вариант неравенства Холдера: при сопряженности Холдера ∑' i ‖f_i‖·‖g_i‖ ≤ ‖f‖·‖g‖.

LaTeX

$$$$ \sum_i \|f_i\| \cdot \|g_i\| \le \|f\| \cdot \|g\|. $$$$

Lean4

protected theorem tsum_mul_le_mul_norm' {p q : ℝ≥0∞} (hpq : p.toReal.HolderConjugate q.toReal) (f : lp E p)
    (g : lp E q) : ∑' i, ‖f i‖ * ‖g i‖ ≤ ‖f‖ * ‖g‖ :=
  (lp.tsum_mul_le_mul_norm hpq f g).2

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