English
The global bound for the product holds without the within qualifier.
Русский
Глобальная граница для произведения без within.
LaTeX
$$$\displaystyle \left\| \operatorname{iteratedFDeriv}_{\mathbb{k}} n (\lambda y. f(y) \cdot g(y)) x \right\| \\le \\sum_{i=0}^{n} {n \choose i} \\| \operatorname{iteratedFDeriv}_{\mathbb{k}} i f x \| \\cdot \\| \operatorname{iteratedFDeriv}_{\mathbb{k}} (n-i) g x \|.$$
Lean4
theorem norm_iteratedFDeriv_smul_le {f : E → 𝕜'} {g : E → F} {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‖ :=
(ContinuousLinearMap.lsmul 𝕜 𝕜' : 𝕜' →L[𝕜] F →L[𝕜] F).norm_iteratedFDeriv_le_of_bilinear_of_le_one hf hg x hn
ContinuousLinearMap.opNorm_lsmul_le
