English
The operator norm of f.compAlongComposition p c is bounded by the product of the operator norm of f and the operator norms of p’s blocks, times the product of the norms of the inputs.
Русский
Нормa оператора f.compAlongComposition p c ограничена произведением норм f и норм блоков p, умноженным на произведение норм входов.
LaTeX
$$$\\|f.compAlongComposition p c\\| \\le \\|f\\| \\cdot \\prod_{i} \\|p(c.blocksFun i)\\| \\cdot \\prod_{i} \\|v(i)\\|$$$
Lean4
/-- The norm of `f.compAlongComposition p c` is controlled by the product of
the norms of the relevant bits of `f` and `p`. -/
theorem compAlongComposition_bound {n : ℕ} (p : FormalMultilinearSeries 𝕜 E F) (c : Composition n)
(f : F [×c.length]→L[𝕜] G) (v : Fin n → E) :
‖f.compAlongComposition p c v‖ ≤ (‖f‖ * ∏ i, ‖p (c.blocksFun i)‖) * ∏ i : Fin n, ‖v i‖ :=
calc
‖f.compAlongComposition p c v‖ = ‖f (p.applyComposition c v)‖ := rfl
_ ≤ ‖f‖ * ∏ i, ‖p.applyComposition c v i‖ := (ContinuousMultilinearMap.le_opNorm _ _)
_ ≤ ‖f‖ * ∏ i, ‖p (c.blocksFun i)‖ * ∏ j : Fin (c.blocksFun i), ‖(v ∘ c.embedding i) j‖ :=
by
gcongr with i
apply ContinuousMultilinearMap.le_opNorm
_ = (‖f‖ * ∏ i, ‖p (c.blocksFun i)‖) * ∏ i, ∏ j : Fin (c.blocksFun i), ‖(v ∘ c.embedding i) j‖ := by
rw [Finset.prod_mul_distrib, mul_assoc]
_ = (‖f‖ * ∏ i, ‖p (c.blocksFun i)‖) * ∏ i : Fin n, ‖v i‖ :=
by
rw [← c.blocksFinEquiv.prod_comp, ← Finset.univ_sigma_univ, Finset.prod_sigma]
congr
