norm_map_tail_le — Mathlib

English

The norm of f evaluated at the init block and last coordinate is bounded by the operator norm of f times the product of norms of all coordinates.

Русский

Норма f( init m ) в сочетании с последней координатой ограничена произведением норм и операторной нормы f.

LaTeX

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

Lean4

theorem norm_map_tail_le (f : Ei 0 →L[𝕜] ContinuousMultilinearMap 𝕜 (fun i : Fin n => Ei i.succ) G) (m : ∀ i, Ei i) :
    ‖f (m 0) (tail m)‖ ≤ ‖f‖ * ∏ i, ‖m i‖ :=
  ContinuousLinearMap.norm_map_removeNth_le (i := 0) f m

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