English
The nn-norm of q.compAlongComposition p c is bounded by the nn-norm of q c.length times the product of the nn-norms of p blocks.
Русский
nnnorm коэффициента q.compAlongComposition p c ограничен nnnorm(q c.length) умноженным на произведение nnnorm(p блоков).
LaTeX
$$$\\mathrm{nnnorm}(q.compAlongComposition p c) \\le \\mathrm{nnnorm}(q(c.length)) \\cdot \\prod_{i} \\mathrm{nnnorm}(p(c.blocksFun i)).$$$
Lean4
/-- The norm of `q.compAlongComposition p c` is controlled by the product of
the norms of the relevant bits of `q` and `p`. -/
theorem compAlongComposition_norm {n : ℕ} (q : FormalMultilinearSeries 𝕜 F G) (p : FormalMultilinearSeries 𝕜 E F)
(c : Composition n) : ‖q.compAlongComposition p c‖ ≤ ‖q c.length‖ * ∏ i, ‖p (c.blocksFun i)‖ :=
ContinuousMultilinearMap.opNorm_le_bound (by positivity) (compAlongComposition_bound _ _ _)
