English
If ‖B‖ ≤ 1, the bound becomes independent of ‖B‖ on the right-hand side.
Русский
Если ‖B‖ ≤ 1, правая часть не содержит зависимость от ‖B‖.
LaTeX
$$$\displaystyle \left\| \operatorname{iteratedFDerivWithin}_{\mathbb{k}} \\ n (\lambda y. B(f(y), 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
/-- Bounding the norm of the iterated derivative of `B (f x) (g x)` within a set in terms of the
iterated derivatives of `f` and `g` when `B` is bilinear of norm at most `1`:
`‖D^n (x ↦ B (f x) (g x))‖ ≤ ∑_{k ≤ n} n.choose k ‖D^k f‖ ‖D^{n-k} g‖` -/
theorem norm_iteratedFDerivWithin_le_of_bilinear_of_le_one (B : E →L[𝕜] F →L[𝕜] G) {f : D → E} {g : D → F}
{N : WithTop ℕ∞} {s : Set D} {x : D} (hf : ContDiffOn 𝕜 N f s) (hg : ContDiffOn 𝕜 N g s) (hs : UniqueDiffOn 𝕜 s)
(hx : x ∈ s) {n : ℕ} (hn : n ≤ N) (hB : ‖B‖ ≤ 1) :
‖iteratedFDerivWithin 𝕜 n (fun y => B (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‖ :=
by
apply (B.norm_iteratedFDerivWithin_le_of_bilinear hf hg hs hx hn).trans
exact mul_le_of_le_one_left (by positivity) hB
