le_of_opNorm_le — Mathlib

English

The least nonnegative bound for the NN-norm version of ‖f m‖ is ‖f‖₊.

Русский

Наименьшее неотрицательное ограничение для версии NN-нормы ‖f m‖ равняется ‖f‖₊.

LaTeX

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

Lean4

theorem le_of_opNorm_le {f : ContinuousMultilinearMap 𝕜 E G} {C : ℝ} (h : ‖f‖ ≤ C) (m : ∀ i, E i) :
    ‖f m‖ ≤ C * ∏ i, ‖m i‖ :=
  le_mul_prod_of_opNorm_le_of_le h fun _ ↦ le_rfl

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