English
Let f : E → F and g : F →L[𝕜] G. Then the i-th iterated derivative within a set s satisfies that it equals applying the left linear map to the i-th iterated derivative of f, provided i ≤ n and appropriate smoothness around the point.
Русский
Пусть f : E → F и линейное отображение g слева; тогда i-я итерационная производная внутри множества s от g ∘ f равна g применённой к i-й итерационной производной f внутри s, при выполнении условий
LaTeX
$$$\text{If } f:E\to F,\ g:F\to_L[\mathbb{K}] G,\ s\subset E,\ x\in s,\ i\in\mathbb{N},\ i\le n, \;\nabla_i(g\circ f) = g\circ\nabla_i f$$$
Lean4
/-- The iterated derivative within a set of the composition with a linear map on the left is
obtained by applying the linear map to the iterated derivative. -/
theorem iteratedFDerivWithin_comp_left {f : E → F} (g : F →L[𝕜] G) (hf : ContDiffWithinAt 𝕜 n f s x)
(hs : UniqueDiffOn 𝕜 s) (hx : x ∈ s) {i : ℕ} (hi : i ≤ n) :
iteratedFDerivWithin 𝕜 i (g ∘ f) s x = g.compContinuousMultilinearMap (iteratedFDerivWithin 𝕜 i f s x) :=
by
rcases hf.contDiffOn' hi (by simp) with ⟨U, hU, hxU, hfU⟩
rw [← iteratedFDerivWithin_inter_open hU hxU, ← iteratedFDerivWithin_inter_open (f := f) hU hxU]
rw [insert_eq_of_mem hx] at hfU
exact
.symm <|
(hfU.ftaylorSeriesWithin (hs.inter hU)).continuousLinearMap_comp g |>.eq_iteratedFDerivWithin_of_uniqueDiffOn
le_rfl (hs.inter hU) ⟨hx, hxU⟩
