English
A product rule bound for iterated derivatives within a subset.
Русский
Граница для итеративного произведения внутри множества.
LaTeX
$$$\displaystyle \|\operatorname{iteratedFDerivWithin}_{\mathbb{k}} n (f(y) g(y)) s x\| \\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_clm_apply_const {f : E → F →L[𝕜] G} {c : F} {s : Set E} {x : E} {N : WithTop ℕ∞}
{n : ℕ} (hf : ContDiffWithinAt 𝕜 N f s x) (hs : UniqueDiffOn 𝕜 s) (hx : x ∈ s) (hn : n ≤ N) :
‖iteratedFDerivWithin 𝕜 n (fun y : E => (f y) c) s x‖ ≤ ‖c‖ * ‖iteratedFDerivWithin 𝕜 n f s x‖ :=
by
let g : (F →L[𝕜] G) →L[𝕜] G := ContinuousLinearMap.apply 𝕜 G c
have h := g.norm_compContinuousMultilinearMap_le (iteratedFDerivWithin 𝕜 n f s x)
rw [← g.iteratedFDerivWithin_comp_left hf hs hx hn] at h
refine h.trans ?_
gcongr
refine g.opNorm_le_bound (norm_nonneg _) fun f => ?_
rw [ContinuousLinearMap.apply_apply, mul_comm]
exact f.le_opNorm c
