English
If f has derivative f' at z, then star ∘ f ∘ star has derivative starL ∘ f' ∘ starL at star z.
Русский
Если у f есть производная f' в z, то star ∘ f ∘ star имеет производную starL ∘ f' ∘ starL в star z.
LaTeX
$$$\\text{HasFDerivAt}(f,f',z) \\Rightarrow \\text{HasFDerivAt}(\\mathrm{star} \\circ f \\circ \\mathrm{star}, \\ (\\mathrm{starL}_{\\mathbb{K}})^{\\-1} \\circ f' \\circ \\mathrm{starL}_{\\mathbb{K}}, \\mathrm{star}(z))$$$
Lean4
/-- If `f` has derivative `f'` at `z`, then `star ∘ f ∘ star` has derivative `starL ∘ f' ∘ starL`
at `star z`. -/
@[fun_prop]
theorem star_star {f : E → F} {z : E} {f' : E →L[𝕜] F} (hf : HasFDerivAt f f' z) :
HasFDerivAt (star ∘ f ∘ star) ((starL 𝕜).toContinuousLinearMap.comp <| f'.comp (starL 𝕜).toContinuousLinearMap)
(star z) :=
.comp_semilinear (starL 𝕜).toContinuousLinearMap (starL 𝕜).toContinuousLinearMap (by simpa using hf)
