norm_def — Mathlib

English

Let f be a continuous multilinear map with domain E = (E_i) and codomain G. The operator norm of f is the smallest nonnegative real number C such that for every choice m = (m_i) with m_i ∈ E_i, we have ∥f(m)∥ ≤ C ∏_i ∥m_i∥.

Русский

Пусть f — непрерывное мультилинейное отображение с доменом E = (E_i) и кодом G. Операторная норма f есть наименьенная неотрицательная константа C такая, что для любого выбора m = (m_i) с m_i ∈ E_i выполняется ∥f(m)∥ ≤ C ∏_i ∥m_i∥.

LaTeX

$$$$ \\|f\\| = \\inf\\{\,c \\ge 0 \\;|\\; \\forall m:\\, \\|f m\\| \\le c \\cdot \\prod_i \\|m_i\\|\\}.$$$$

Lean4

theorem norm_def (f : ContinuousMultilinearMap 𝕜 E G) : ‖f‖ = sInf {c | 0 ≤ (c : ℝ) ∧ ∀ m, ‖f m‖ ≤ c * ∏ i, ‖m i‖} :=
  rfl

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