English
The bound applies to a finite product of functions, with a multinomial coefficient weighting the derivatives.
Русский
Предел применяется к произведению конечного числа функций.
LaTeX
$$$\displaystyle \left\| \operatorname{iteratedFDeriv}_{\mathbb{k}} n (\prod_{j\in u} f_j \cdot) x \right\| \\le \\sum_{p \in u.sym n} (p : Multiset ι).multinomial * \\prod_{j \in u} \left\| \operatorname{iteratedFDeriv}_{\mathbb{k}} (Multiset.count j p) (f_j) x \right\| .$$
Lean4
theorem norm_iteratedFDeriv_mul_le {f : E → A} {g : E → A} {N : WithTop ℕ∞} (hf : ContDiff 𝕜 N f) (hg : ContDiff 𝕜 N g)
(x : E) {n : ℕ} (hn : n ≤ N) :
‖iteratedFDeriv 𝕜 n (fun y => f y * g y) x‖ ≤
∑ i ∈ Finset.range (n + 1), (n.choose i : ℝ) * ‖iteratedFDeriv 𝕜 i f x‖ * ‖iteratedFDeriv 𝕜 (n - i) g x‖ :=
by
simp_rw [← iteratedFDerivWithin_univ]
exact norm_iteratedFDerivWithin_mul_le hf.contDiffOn hg.contDiffOn uniqueDiffOn_univ (mem_univ x) hn
