le_mul_prod_of_opNorm_le_of_le — Mathlib

English

The operator norm is the least C such that the pointwise bound holds for all m.

Русский

Операторная норма является наименьшей константой C, для которой выполняется пунктирное неравенство для всех m.

LaTeX

$$$$ \\|f\\| \\le C \\quad\\text{iff}\\quad \\forall m, \\|f m\\| \\le C \\prod_i \\|m_i\\|.$$$

Lean4

theorem le_mul_prod_of_opNorm_le_of_le {f : ContinuousMultilinearMap 𝕜 E G} {m : ∀ i, E i} {C : ℝ} {b : ι → ℝ}
    (hC : ‖f‖ ≤ C) (hm : ∀ i, ‖m i‖ ≤ b i) : ‖f m‖ ≤ C * ∏ i, b i :=
  (f.le_opNorm m).trans <| by gcongr; exacts [f.opNorm_nonneg.trans hC, hm _]

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