English
Let f: K → F have Fréchet derivative f' at x, and let L: F →SL[σ] F' be a σ-semi-linear map. Then the map x ↦ L(f(σ'(x))) has Fréchet derivative at σ x equal to L(f').
Русский
Пусть f: 𝕜 → F имеет Фрéш derivative f' в точке x, и пусть L: F →SL[σ] F' есть σ-симилинейное отображение. Тогда отображение x ↦ L(f(σ'(x))) имеет Фрéш-образ derivative в σx равный L(f').
LaTeX
$$$\text{If } f: \mathbb{K} \to F \text{ has Frechet derivative } f' \text{ at } x, \text{ and } L: F \toSL[\sigma] F' \text{ is a } \sigma\text{-semilinear map, then } \text{HasDerivAt} (L \circ f \circ \sigma') (L f') (\sigma x).$$$
Lean4
/-- If `L` is a `σ`-semilinear map, and `f` has Fréchet derivative `f'` at `x`, then `L ∘ f ∘ σ⁻¹`
has Fréchet derivative `L ∘ f'` at `σ x`. -/
theorem comp_semilinear (hf : HasDerivAt f f' x) : HasDerivAt (L ∘ f ∘ σ') (L f') (σ x) :=
by
have : RingHomIsometric σ' := .inv σ
let R : 𝕜 →SL[σ'] 𝕜 := ⟨σ'.toSemilinearMap, σ'.isometry.continuous⟩
have hR (k : 𝕜) : R k = σ' k := rfl
rw [hasDerivAt_iff_hasFDerivAt]
convert HasFDerivAt.comp_semilinear L R (f' := (1 : 𝕜 →L[𝕜] 𝕜).smulRight f') ?_
· ext
simp [R]
· rwa [← hasDerivAt_iff_hasFDerivAt, hR, RingHomInvPair.comp_apply_eq]
