nnnorm_prod_le_of_le — Mathlib

English

For a finite s and f: s→E with nonnegative bounds n, if ‖f(b)‖₊ ≤ n(b) for all b∈s, then ‖∏ f(b)‖₊ ≤ ∑ n(b).

Русский

Для конечного множества s и функции f: s→E с ограничителями n, если ‖f(b)‖₊ ≤ n(b) для всех b∈s, тогда ‖∏ f(b)‖₊ ≤ ∑ n(b).

LaTeX

$$$\displaystyle \forall s\;\forall f:\,s\to E\;\forall n:\,s\to \mathbb{R}_{\ge 0},\; (\forall b\in s,\; \|f(b)\|_+ \le n(b)) \Rightarrow \|\prod_{b\in s} f(b)\|_+ \le \sum_{b\in s} n(b).$$$

Lean4

@[to_additive]
theorem nnnorm_prod_le_of_le (s : Finset ι) {f : ι → E} {n : ι → ℝ≥0} (h : ∀ b ∈ s, ‖f b‖₊ ≤ n b) :
    ‖∏ b ∈ s, f b‖₊ ≤ ∑ b ∈ s, n b :=
  (norm_prod_le_of_le s h).trans_eq (NNReal.coe_sum ..).symm

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