English
The same bilinear bound applies to the scalar product f(y) g(y) within a set.
Русский
Та же граница действует для скалярного умножения внутри множества.
LaTeX
$$$\displaystyle \left\| \operatorname{iteratedFDerivWithin}_{\mathbb{k}} n (\lambda y. f(y) \cdot g(y)) \\ s \\ x \right\| \\le \\sum_{i=0}^{n} {n \choose i} \\| \operatorname{iteratedFDerivWithin}_{\mathbb{k}} i f \\ s \\ x \| \\cdot \\| \operatorname{iteratedFDerivWithin}_{\mathbb{k}} (n-i) g \\ s \\ x \|.$$
Lean4
theorem norm_iteratedFDerivWithin_smul_le {f : E → 𝕜'} {g : E → F} {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.lsmul 𝕜 𝕜' : 𝕜' →L[𝕜] F →L[𝕜] F).norm_iteratedFDerivWithin_le_of_bilinear_of_le_one hf hg hs hx
hn ContinuousLinearMap.opNorm_lsmul_le
