English
For a function f: F → G and a linear isomorphism iso: E ≃L[𝕜] F, the HasFDerivWithinAt of the composition f ∘ iso with a derivative f' ∘ iso is equivalent to HasFDerivWithinAt of f with derivative f' at the image point, i.e., HasFDerivWithinAt (f ∘ iso) (f' ∘ iso) (iso^{-1} s) x ⇔ HasFDerivWithinAt f f' s (iso x).
Русский
Для функции f : F → G и линейного изоморфизма iso: E ≃L[𝕜] F равенство HasFDerivWithinAt композиции f ∘ iso с производной f' ∘ iso эквивалентно HasFDerivWithinAt f f' на образе, т.е. HasFDerivWithinAt (f ∘ iso) (f' ∘ iso) (iso^{-1}(s)) x ⇔ HasFDerivWithinAt f f' s (iso x).
LaTeX
$$$ HasFDerivWithinAt (f \\circ iso) (f' \\circ iso) (iso^{-1} s) x \\iff HasFDerivWithinAt f f' s (iso x)$$$
Lean4
theorem comp_right_hasFDerivWithinAt_iff {f : F → G} {s : Set F} {x : E} {f' : F →L[𝕜] G} :
HasFDerivWithinAt (f ∘ iso) (f'.comp (iso : E →L[𝕜] F)) (iso ⁻¹' s) x ↔ HasFDerivWithinAt f f' s (iso x) :=
by
refine ⟨fun H => ?_, fun H => H.comp x iso.hasFDerivWithinAt (mapsTo_preimage _ s)⟩
rw [← iso.symm_apply_apply x] at H
have A : f = (f ∘ iso) ∘ iso.symm :=
by
rw [Function.comp_assoc, iso.self_comp_symm]
rfl
have B : f' = (f'.comp (iso : E →L[𝕜] F)).comp (iso.symm : F →L[𝕜] E) := by
rw [ContinuousLinearMap.comp_assoc, iso.coe_comp_coe_symm, ContinuousLinearMap.comp_id]
rw [A, B]
apply H.comp (iso x) iso.symm.hasFDerivWithinAt
intro y hy
simpa only [mem_preimage, apply_symm_apply] using hy
