English
Let iso be a linear isometry between E and F. For any map f : G → E and any x, the existence of the Fréchet derivative of iso ∘ f at x with derivative f' is equivalent to the Fréchet differentiability of f at x with derivative given by (iso.symm) ∘ f'. In particular, D(iso ∘ f)(x) = iso ∘ Df(x).
Русский
Пусть iso является линейной изометрией между пространствами E и F. Для любого отображения f: G → E и точки x равенство существования производной Фреше для композиции iso ∘ f в точке x с производной f' эквивалентно существованию производной Фреше для f в точке x с производной, равной (iso.symm) ∘ f'. В частности, D(iso ∘ f)(x) = iso ∘ Df(x).
LaTeX
$$$$ \\HasFDerivAt(\\mathrm{iso} \\circ f)\\ f'\\ x \\;\\Longleftrightarrow\\; \\HasFDerivAt f\\ ((\\mathrm{iso.symm}) \\circ f')\\ x $$$$
Lean4
theorem comp_hasFDerivAt_iff' {f : G → E} {x : G} {f' : G →L[𝕜] F} :
HasFDerivAt (iso ∘ f) f' x ↔ HasFDerivAt f ((iso.symm : F →L[𝕜] E).comp f') x :=
(iso : E ≃L[𝕜] F).comp_hasFDerivAt_iff'
