sum_norm_apply_le_norm' — Mathlib

English

Let f be a function f: ι → G_i with finite ι. Then the sum of the norms satisfies ∑_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_norm_apply_le_norm /-- The $L^1$ norm is less than the $L^\infty$ norm scaled
    by the cardinality. -/
    ]
theorem sum_norm_apply_le_norm' : ∑ i, ‖f i‖ ≤ Fintype.card ι • ‖f‖ :=
  Finset.sum_le_card_nsmul _ _ _ fun i _hi => norm_le_pi_norm' _ i

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