norm_applyOrderedFinpartition_le — Mathlib

English

The operator norm bound: the norm of c.applyOrderedFinpartition p v at m is bounded by the product of the operator norm of p m and the norms of v along the block m.

Русский

Нормальная граница оператора: нормa c.applyOrderedFinpartition p v на m не превосходит произведение нормы p m и норм v внутри блока m.

LaTeX

$$‖c.applyOrderedFinpartition p v m‖ ≤ ‖p m‖ * ∏ i : Fin (c.partSize m), ‖v (c.emb m i)‖$$

Lean4

theorem norm_applyOrderedFinpartition_le (p : ∀ (i : Fin c.length), E [×c.partSize i]→L[𝕜] F) (v : Fin n → E)
    (m : Fin c.length) : ‖c.applyOrderedFinpartition p v m‖ ≤ ‖p m‖ * ∏ i : Fin (c.partSize m), ‖v (c.emb m i)‖ :=
  (p m).le_opNorm _

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