compAlongComposition_nnnorm — Mathlib

English

The norm of q.compAlongComposition p c is bounded by the product of the norm of q at c.length and the norms of p’s blocks.

Русский

Нормa q.compAlongComposition p c ограничена произведением нормы q на c.length и норм блоков p.

LaTeX

$$$\\|q.compAlongComposition p c\\| \\le \\|q(c.length)\\| \\cdot \\prod_{i} \\|p(c.blocksFun i)\\|.$$$

Lean4

theorem compAlongComposition_nnnorm {n : ℕ} (q : FormalMultilinearSeries 𝕜 F G) (p : FormalMultilinearSeries 𝕜 E F)
    (c : Composition n) : ‖q.compAlongComposition p c‖₊ ≤ ‖q c.length‖₊ * ∏ i, ‖p (c.blocksFun i)‖₊ := by
  rw [← NNReal.coe_le_coe]; push_cast; exact q.compAlongComposition_norm p c

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