norm_map_init_le — Mathlib

English

For a multilinear map f and a tail m, the tail-bound inequality holds: the norm of f applied to tail(m) is bounded by the product with the x-vector tail.

Русский

Для многолинейного отображения f и хвоста m выполняется неравенство: нормa f( tail m ) ограничена произведением и нормой хвоста.

LaTeX

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

Lean4

theorem norm_map_init_le (f : ContinuousMultilinearMap 𝕜 (fun i : Fin n => Ei <| castSucc i) (Ei (last n) →L[𝕜] G))
    (m : ∀ i, Ei i) : ‖f (init m) (m (last n))‖ ≤ ‖f‖ * ∏ i, ‖m i‖ :=
  by
  rw [prod_univ_castSucc, ← mul_assoc]
  exact (f (init m)).le_of_opNorm_le (f.le_opNorm _) _

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