English
Iterated derivatives commute with left composition by continuous linear equivalences.
Русский
Итеративные производные коммутируют с левой композицией непрерывных линейных эквивалентностей.
LaTeX
$$$\forall g:\, F \simeq_L G,\; iteratedFDerivWithin 𝕜 i (g \circ f) s x = g \circ (iteratedFDerivWithin 𝕜 i f s x)$$$
Lean4
/-- If `f` admits a Taylor series `p` in a set `s`, and `g` is linear, then `f ∘ g` admits a Taylor
series in `g ⁻¹' s`, whose `k`-th term is given by `p k (g v₁, ..., g vₖ)` . -/
theorem compContinuousLinearMap (hf : HasFTaylorSeriesUpToOn n f p s) (g : G →L[𝕜] E) :
HasFTaylorSeriesUpToOn n (f ∘ g) (fun x k => (p (g x) k).compContinuousLinearMap fun _ => g) (g ⁻¹' s) :=
by
let A : ∀ m : ℕ, (E [×m]→L[𝕜] F) → G [×m]→L[𝕜] F := fun m h => h.compContinuousLinearMap fun _ => g
have hA : ∀ m, IsBoundedLinearMap 𝕜 (A m) := fun m => isBoundedLinearMap_continuousMultilinearMap_comp_linear g
constructor
· intro x hx
simp only [(hf.zero_eq (g x) hx).symm, Function.comp_apply]
change (p (g x) 0 fun _ : Fin 0 => g 0) = p (g x) 0 0
rw [ContinuousLinearMap.map_zero]
rfl
· intro m hm x hx
convert
(hA m).hasFDerivAt.comp_hasFDerivWithinAt x
((hf.fderivWithin m hm (g x) hx).comp x g.hasFDerivWithinAt (Subset.refl _))
ext y v
change p (g x) (Nat.succ m) (g ∘ cons y v) = p (g x) m.succ (cons (g y) (g ∘ v))
rw [comp_cons]
· intro m hm
exact (hA m).continuous.comp_continuousOn <| (hf.cont m hm).comp g.continuous.continuousOn <| Subset.refl _
