sum_nnnorm_apply_le_nnnorm' — Mathlib

English

Let f: ι → G_i with finite ι. Then ∑_i ∥f(i)∥₊ ≤ card(ι) · ∥f∥₊.

Русский

Пусть f: ι → G_i, ι конечное. Тогда ∑_i ∥f(i)∥₊ ≤ card(ι) · ∥f∥₊.

LaTeX

$$$\sum_i ∥f(i)∥_+ \le |\iota| \cdot ∥f∥_+$$$

Lean4

/-- The $L^1$ norm is less than the $L^\infty$ norm scaled by the cardinality. -/
@[to_additive Pi.sum_nnnorm_apply_le_nnnorm /-- The $L^1$ norm is less than the $L^\infty$ norm
    scaled by the cardinality. -/
    ]
theorem sum_nnnorm_apply_le_nnnorm' : ∑ i, ‖f i‖₊ ≤ Fintype.card ι • ‖f‖₊ :=
  (NNReal.coe_sum ..).trans_le <| Pi.sum_norm_apply_le_norm' _

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