English
If the bilinear map has norm at most 1, the bound is unchanged by within-set derivatives.
Русский
Если норма билинеарного отображения не превышает 1, неравенство сохраняется для within-derivatives.
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)` 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_iteratedFDeriv_le_of_bilinear_of_le_one (B : E →L[𝕜] F →L[𝕜] G) {f : D → E} {g : D → F} {N : WithTop ℕ∞}
(hf : ContDiff 𝕜 N f) (hg : ContDiff 𝕜 N g) (x : D) {n : ℕ} (hn : n ≤ N) (hB : ‖B‖ ≤ 1) :
‖iteratedFDeriv 𝕜 n (fun y => B (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
B.norm_iteratedFDerivWithin_le_of_bilinear_of_le_one hf.contDiffOn hg.contDiffOn uniqueDiffOn_univ (mem_univ x) hn
hB
