summable_mul — Mathlib

English

Under Holder conjugacy, for f ∈ lp E p and g ∈ lp E q, the inequality holds: ∑' i, ‖f i‖·‖g i‖ ≤ ‖f‖·‖g‖.

Русский

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

LaTeX

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

Lean4

protected theorem summable_mul {p q : ℝ≥0∞} (hpq : p.toReal.HolderConjugate q.toReal) (f : lp E p) (g : lp E q) :
    Summable fun i => ‖f i‖ * ‖g i‖ :=
  (lp.tsum_mul_le_mul_norm hpq f g).1

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