English
The nth derivative of a finite product is bounded by a multinomial sum of derivatives of the factors up to order n.
Русский
Производная порядка n от конечного произведения ограничена мультиномиальной суммой производных факторов.
LaTeX
$$$\displaystyle \left\| \operatorname{iteratedFDerivWithin}_{\mathbb{k}} n (\prod_{j\in u} f_j \cdot) \\ s \\ x \right\| \\le \\sum_{p \in u.sym n} (p : Multiset \! ι).multinomial * \\prod_{j \in u} \left\| \operatorname{iteratedFDerivWithin}_{\mathbb{k}} (Multiset.count j p) (f_j) s x \right\| .$$
Lean4
theorem norm_iteratedFDerivWithin_mul_le {f : E → A} {g : E → A} {N : WithTop ℕ∞} (hf : ContDiffOn 𝕜 N f s)
(hg : ContDiffOn 𝕜 N g s) (hs : UniqueDiffOn 𝕜 s) {x : E} (hx : x ∈ s) {n : ℕ} (hn : n ≤ N) :
‖iteratedFDerivWithin 𝕜 n (fun y => f y * g y) s x‖ ≤
∑ i ∈ Finset.range (n + 1),
(n.choose i : ℝ) * ‖iteratedFDerivWithin 𝕜 i f s x‖ * ‖iteratedFDerivWithin 𝕜 (n - i) g s x‖ :=
(ContinuousLinearMap.mul 𝕜 A : A →L[𝕜] A →L[𝕜] A).norm_iteratedFDerivWithin_le_of_bilinear_of_le_one hf hg hs hx hn
(ContinuousLinearMap.opNorm_mul_le _ _)
