English
If f is differentiable at R z, then L ∘ f ∘ R is differentiable at z (linearization through semilinear maps).
Русский
Если f дифференцируема в R z, то L ∘ f ∘ R дифференцируема в z.
LaTeX
$$$\mathrm{DifferentiableAt}_{\mathbb{K}} f (R z) \Rightarrow \mathrm{DifferentiableAt}_{\mathbb{K}} (L \circ f \circ R) z$$$
Lean4
/-- If `L` and `R` are semilinear maps whose composite is linear, and `f` has Fréchet derivative
`f'` at `R z`, then `L ∘ f ∘ R` has Fréchet derivative `L ∘ f' ∘ R` at `z`. -/
theorem comp_semilinear {f : V → W} {z : V'} {f' : V →L[𝕜] W} (hf : HasFDerivAt f f' (R z)) :
HasFDerivAt (L ∘ f ∘ R) (L.comp (f'.comp R)) z :=
by
have : RingHomIsometric σ' := .inv σ
rw [hasFDerivAt_iff_isLittleO_nhds_zero] at ⊢ hf
have := hf.comp_tendsto (R.map_zero ▸ R.continuous.continuousAt.tendsto)
simpa using ((L.isBigO_comp _ _).trans_isLittleO this).trans_isBigO (R.isBigO_id _)
