enorm_prod_le — Mathlib

English

In ENNorm setting, the ENNReal norm of a sum is at most the sum of ENNorms.

Русский

В рамках ENNORM: ‖∑ f(i)‖ₑ ≤ ∑ ‖f(i)‖ₑ.

LaTeX

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

Lean4

@[to_additive existing]
theorem enorm_prod_le (s : Finset ι) (f : ι → ε) : ‖∏ i ∈ s, f i‖ₑ ≤ ∑ i ∈ s, ‖f i‖ₑ :=
  by
  rw [← Multiplicative.ofAdd_le, ofAdd_sum]
  refine Finset.le_prod_of_submultiplicative (Multiplicative.ofAdd ∘ enorm) ?_ (fun x y => ?_) _ _
  · simp
  · exact enorm_mul_le' x y

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