le_opNorm — Mathlib

English

For any m, the value ∥f(m)∥ is bounded by the operator norm times the product of ∥m_i∥.

Русский

Для любого m значение ∥f(m)∥ не превышает нормы оператора, умноженной на произведение ∥m_i∥.

LaTeX

$$$$ \\|f m\\| \\le \\|f\\| \\cdot \\prod_i \\|m_i\\|.$$$$

Lean4

/-- The fundamental property of the operator norm of a continuous multilinear map:
`‖f m‖` is bounded by `‖f‖` times the product of the `‖m i‖`. -/
theorem le_opNorm (f : ContinuousMultilinearMap 𝕜 E G) (m : ∀ i, E i) : ‖f m‖ ≤ ‖f‖ * ∏ i, ‖m i‖ :=
  f.isLeast_opNorm.1.2 m

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