norm_map_insertNth_le — Mathlib

English

For a multilinear map f and a snoc operation, the norm of f(snoc m x) is bounded by the product of the operator norm, the norm of x, and the product of norms of m.

Русский

Для отображения f и операции snoc: норма f( snoc m x ) ограничена произведением операторной нормы, ‖x‖ и произведения ‖m_i‖.

LaTeX

$$$\|f( snoc\; m\; x)\| \leq (\|f\| \cdot \prod_i \|m_i\|) \cdot \|x\|$$$

Lean4

theorem norm_map_insertNth_le (f : ContinuousMultilinearMap 𝕜 Ei G) {i : Fin (n + 1)} (x : Ei i)
    (m : ∀ j, Ei (i.succAbove j)) : ‖f (i.insertNth x m)‖ ≤ ‖f‖ * ‖x‖ * ∏ i, ‖m i‖ := by
  simpa [i.prod_univ_succAbove, mul_assoc] using f.le_opNorm (i.insertNth x m)

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