isLeast_opNorm — Mathlib

English

The operator norm is the least bound among all admissible bounds in the defining set.

Русский

Операторная норма является наименьшей границей среди допустимых границ в определении нормы.

LaTeX

$$$$ \\|f\\| = \\min\\{\,C \\ge 0 : \\forall m, \\|f m\\| \\le C \\prod_i \\|m_i\\|\\}.$$$$

Lean4

theorem isLeast_opNorm (f : ContinuousMultilinearMap 𝕜 E G) :
    IsLeast {c : ℝ | 0 ≤ c ∧ ∀ m, ‖f m‖ ≤ c * ∏ i, ‖m i‖} ‖f‖ :=
  by
  refine IsClosed.isLeast_csInf ?_ bounds_nonempty bounds_bddBelow
  simp only [Set.setOf_and, Set.setOf_forall]
  exact isClosed_Ici.inter (isClosed_iInter fun m ↦ isClosed_le continuous_const (continuous_id.mul continuous_const))

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