norm_compAlongOrderedFinpartition_le

English

The operator norm of the composed map c.compAlongOrderedFinpartition is bounded by the product of the operator norms of f and p across blocks: ‖c.compAlongOrderedFinpartition f p‖ ≤ ‖f‖ ∏i ‖p i‖.

Русский

Норма оператора композиции c.compAlongOrderedFinpartition ограничена произведением норм операторов f и p по блокам: ‖c.compAlongOrderedFinpartition f p‖ ≤ ‖f‖ ∏i ‖p i‖.

LaTeX

$$‖c.compAlongOrderedFinpartition f p‖ ≤ ‖f‖ * ∏ i, ‖p i‖$$

Lean4

theorem norm_compAlongOrderedFinpartition_le (f : F [×c.length]→L[𝕜] G) (p : ∀ i, E [×c.partSize i]→L[𝕜] F) :
    ‖c.compAlongOrderedFinpartition f p‖ ≤ ‖f‖ * ∏ i, ‖p i‖ :=
  by
  refine ContinuousMultilinearMap.opNorm_le_bound (by positivity) fun v ↦ ?_
  rw [compAlongOrderFinpartition_apply, mul_assoc, ← c.prod_sigma_eq_prod, ← Finset.prod_mul_distrib]
  exact f.le_opNorm_mul_prod_of_le <| c.norm_applyOrderedFinpartition_le _ _

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