ratio_le_opNorm — Mathlib

English

The NN-norm of f is bounded by C iff for all inputs m, ‖f m‖₊ ≤ C ∏ ‖m_i‖₊.

Русский

NN-норма f ограничена C тогда и только тогда, когда для всех входов m выполняется ‖f m‖₊ ≤ C ∏ ‖m_i‖₊.

LaTeX

$$$$ \\|f\\|_{nn} \\le C \\;\\text{iff} \\; \\forall m, \\|f m\\|_{nn} \\le C \\prod_i \\|m_i\\|_{nn}.$$$$

Lean4

theorem ratio_le_opNorm (f : ContinuousMultilinearMap 𝕜 E G) (m : ∀ i, E i) : (‖f m‖ / ∏ i, ‖m i‖) ≤ ‖f‖ :=
  div_le_of_le_mul₀ (by positivity) (opNorm_nonneg _) (f.le_opNorm m)

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