English
A broader auxiliary bound for high-order derivative estimates in compositions.
Русский
Более общее вспомогательное неравенство для оценок производных композиции.
LaTeX
$$$\displaystyle \|\operatorname{iteratedFDerivWithin}_{\mathbb{k}} n (g \circ f) s x\| \le n! \cdot C \cdot D^n$$$
Lean4
theorem norm_iteratedFDerivWithin_clm_apply {f : E → F →L[𝕜] G} {g : E → F} {s : Set E} {x : E} {N : WithTop ℕ∞} {n : ℕ}
(hf : ContDiffOn 𝕜 N f s) (hg : ContDiffOn 𝕜 N g s) (hs : UniqueDiffOn 𝕜 s) (hx : x ∈ s) (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‖ :=
by
let B : (F →L[𝕜] G) →L[𝕜] F →L[𝕜] G := ContinuousLinearMap.flip (ContinuousLinearMap.apply 𝕜 G)
have hB : ‖B‖ ≤ 1 := by
simp only [B, ContinuousLinearMap.opNorm_flip, ContinuousLinearMap.apply]
refine ContinuousLinearMap.opNorm_le_bound _ zero_le_one fun f => ?_
simp only [ContinuousLinearMap.coe_id', id, one_mul]
rfl
exact B.norm_iteratedFDerivWithin_le_of_bilinear_of_le_one hf hg hs hx hn hB
