English
If g is a continuous linear equivalence, then the i-th iterated derivative within s of g ∘ f equals the left-linear map applied to the i-th iterated derivative within s of f, for all i.
Русский
Пусть g — непрерывное линейное эквивалентное отображение; тогда i-я итерационная производная внутри s от g ∘ f равна g-у применении к i-й производной внутри s от f, для всех i.
LaTeX
$$$\forall i:\; iteratedFDerivWithin_{\mathbb{K}}^i(g\circ f)\,s\,x = g.toContinuousLinearMap\,\circ\; iteratedFDerivWithin_{\mathbb{K}}^i f\,s\,x$$$
Lean4
/-- The iterated derivative within a set of the composition with a linear equiv on the left is
obtained by applying the linear equiv to the iterated derivative. This is true without
differentiability assumptions. -/
theorem iteratedFDerivWithin_comp_left (g : F ≃L[𝕜] G) (f : E → F) (hs : UniqueDiffOn 𝕜 s) (hx : x ∈ s) (i : ℕ) :
iteratedFDerivWithin 𝕜 i (g ∘ f) s x =
(g : F →L[𝕜] G).compContinuousMultilinearMap (iteratedFDerivWithin 𝕜 i f s x) :=
by
induction i generalizing x with ext1 m
| zero =>
simp only [iteratedFDerivWithin_zero_apply, comp_apply, ContinuousLinearMap.compContinuousMultilinearMap_coe,
coe_coe]
| succ i IH =>
rw [iteratedFDerivWithin_succ_apply_left]
have Z :
fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i (g ∘ f) s) s x =
fderivWithin 𝕜 (g.continuousMultilinearMapCongrRight (fun _ : Fin i => E) ∘ iteratedFDerivWithin 𝕜 i f s) s x :=
fderivWithin_congr' (@IH) hx
simp_rw [Z]
rw [(g.continuousMultilinearMapCongrRight fun _ : Fin i => E).comp_fderivWithin (hs x hx)]
simp only [ContinuousLinearMap.coe_comp', ContinuousLinearEquiv.coe_coe, comp_apply,
ContinuousLinearEquiv.continuousMultilinearMapCongrRight_apply,
ContinuousLinearMap.compContinuousMultilinearMap_coe, EmbeddingLike.apply_eq_iff_eq]
rw [iteratedFDerivWithin_succ_apply_left]
