English
Let B be a bounded bilinear map and f,g be C^N on the domain. For every x and n ≤ N, the nth derivative of (y ↦ B(f(y), g(y))) at x is bounded by the product of ‖B‖ and the binomial sum of derivatives of f and g at x.
Русский
Пусть B — ограниченная билинеарная, f и g — действия C^N на всей области. Для любого x и для любого n ≤ N норму n-ой производной по составному выражению B(f(y), g(y)) в точке x ограничиваем суммой по биномиалу, умноженной на ‖B‖ и сопряжённые нормы производных f и g в x.
LaTeX
$$$\displaystyle \left\| \operatorname{iteratedFDeriv} \\ 𝕜 \\ n (\lambda y. B(f(y), g(y)))\ x \\right\| \\le \\|B\| \\cdot \sum_{i=0}^{n} {n \choose i} \\| \operatorname{iteratedFDeriv}_{\mathbb{k}} i f x \| \\cdot \\| \operatorname{iteratedFDeriv}_{\mathbb{k}} (n-i) g 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:
`‖D^n (x ↦ B (f x) (g x))‖ ≤ ‖B‖ ∑_{k ≤ n} n.choose k ‖D^k f‖ ‖D^{n-k} g‖` -/
theorem norm_iteratedFDeriv_le_of_bilinear (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) :
‖iteratedFDeriv 𝕜 n (fun y => B (f y) (g y)) x‖ ≤
‖B‖ * ∑ 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 hf.contDiffOn hg.contDiffOn uniqueDiffOn_univ (mem_univ x) hn
