enorm_prod_le_of_le — Mathlib

English

The ENNorm of a finite product is at most the sum of ENNorms.

Русский

ENNorm конечного произведения не больше суммы ENNorm.

LaTeX

$$$$\Big\|\prod_{i\in s} f(i)\Big\|_{e} \le \sum_{i\in s} \|f(i)\|_{e}.$$$$

Lean4

@[to_additive]
theorem enorm_prod_le_of_le (s : Finset ι) {f : ι → ε} {n : ι → ℝ≥0∞} (h : ∀ b ∈ s, ‖f b‖ₑ ≤ n b) :
    ‖∏ b ∈ s, f b‖ₑ ≤ ∑ b ∈ s, n b :=
  (enorm_prod_le s f).trans <| Finset.sum_le_sum h

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