isLeast_opNNNorm

Mathlib.Analysis.NormedSpace.Alternating.Basic

URI: https://scilib.ai/kg/mathlib#ContinuousAlternatingMap.isLeast_opNNNorm

English

The least nonnegative bound for nnNorm coincides with the nnNorm of f.

Русский

Наименьшая граница nnNorm совпадает с nnNorm f.

LaTeX

$$$$\|f\|_{nn} = \min\{C \ge 0 : ∀ m, \|f m\|_{nn} ≤ C \prod_i \|m_i\|_{nn}\}.$$$$

Lean4

theorem isLeast_opNNNorm (f : E [⋀^ι]→L[𝕜] F) : IsLeast {C : ℝ≥0 | ∀ m, ‖f m‖₊ ≤ C * ∏ i, ‖m i‖₊} ‖f‖₊ :=
  f.1.isLeast_opNNNorm

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru