English
For a nonempty finite index set, the norm of the product is bounded by the sup of norms of factors.
Русский
Для конечного непустого множества индексов норма произведения ограничена сверху супом норм множителей.
LaTeX
$$$s \\neq \\varnothing \\Rightarrow \\|\\prod_{i \\in s} f(i)\\| ≤ s.sup (\\|f·\\|)$$$
Lean4
/-- Nonarchimedean norm of a product is less than or equal the norm of any term in the product.
This version is phrased using `Finset.sup'` and `Finset.Nonempty` due to `Finset.sup`
operating over an `OrderBot`, which `ℝ` is not. -/
@[to_additive /-- Nonarchimedean norm of a sum is less than or equal the norm of any term in the
sum. This version is phrased using `Finset.sup'` and `Finset.Nonempty` due to `Finset.sup`
operating over an `OrderBot`, which `ℝ` is not. -/
]
theorem _root_.Finset.Nonempty.norm_prod_le_sup'_norm {s : Finset ι} (hs : s.Nonempty) (f : ι → M) :
‖∏ i ∈ s, f i‖ ≤ s.sup' hs (‖f ·‖) := by
simp only [Finset.le_sup'_iff]
induction hs using Finset.Nonempty.cons_induction with
| singleton j => simp only [Finset.mem_singleton, Finset.prod_singleton, exists_eq_left, le_refl]
| cons j t hj _ IH =>
simp only [Finset.prod_cons, Finset.mem_cons, exists_eq_or_imp]
refine (le_total ‖∏ i ∈ t, f i‖ ‖f j‖).imp ?_ ?_ <;> intro h
· exact (norm_mul_le_max _ _).trans (max_eq_left h).le
· exact ⟨_, IH.choose_spec.left, (norm_mul_le_max _ _).trans <| ((max_eq_right h).le.trans IH.choose_spec.right)⟩
