Semilinear composition of derivatives within sets

Composing on both sides by continuous semilinear maps with inverse scalar homomorphisms transports a Fréchet derivative, even at boundary points of a set. This includes conjugating both the argument and value of a complex differentiable function.

HasFDerivWithinAt.comp_semilinear extends Mathlib's HasFDerivAt.comp_semilinear to arbitrary source and target sets. The local comp_semilinear_of_tendsto form only requires that R approaches the target set near the point under consideration. The corresponding DifferentiableWithinAt lemmas transport differentiability without specifying a derivative.

theorem HasFDerivWithinAt.comp_semilinear_of_tendsto {𝕜 : Type u_1} {𝕜' : Type u_2} {V : Type u_3} {V' : Type u_4} {W : Type u_5} {W' : Type u_6} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] {σ : 𝕜 →+* 𝕜'} {σ' : 𝕜' →+* 𝕜} [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [SeminormedAddCommGroup V'] [NormedSpace 𝕜' V'] [SeminormedAddCommGroup W] [NormedSpace 𝕜 W] [SeminormedAddCommGroup W'] [NormedSpace 𝕜' W'] [RingHomIsometric σ] [RingHomInvPair σ σ'] (L : W →SL[σ] W') (R : V' →SL[σ'] V) {f : V → W} {f' : V →L[𝕜] W} {s : Set V'} {t : Set V} {x : V'} (hf : HasFDerivWithinAt f f' t (R x)) (hR : Filter.Tendsto (⇑R) (nhdsWithin x s) (nhdsWithin (R x) t)) : HasFDerivWithinAt (⇑L ∘ f ∘ ⇑R) (L ∘SL f' ∘SL R) s x

If L and R are continuous semilinear maps with inverse scalar homomorphisms, and R tends to R x within t as its argument tends to x within s, then a derivative of f within t at R x transports to a derivative of L ∘ f ∘ R within s at x. The two semilinear twists cancel in the resulting derivative.

theorem HasFDerivWithinAt.comp_semilinear {𝕜 : Type u_1} {𝕜' : Type u_2} {V : Type u_3} {V' : Type u_4} {W : Type u_5} {W' : Type u_6} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] {σ : 𝕜 →+* 𝕜'} {σ' : 𝕜' →+* 𝕜} [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [SeminormedAddCommGroup V'] [NormedSpace 𝕜' V'] [SeminormedAddCommGroup W] [NormedSpace 𝕜 W] [SeminormedAddCommGroup W'] [NormedSpace 𝕜' W'] [RingHomIsometric σ] [RingHomInvPair σ σ'] (L : W →SL[σ] W') (R : V' →SL[σ'] V) {f : V → W} {f' : V →L[𝕜] W} {s : Set V'} {t : Set V} {x : V'} (hf : HasFDerivWithinAt f f' t (R x)) (hR : Set.MapsTo (⇑R) s t) : HasFDerivWithinAt (⇑L ∘ f ∘ ⇑R) (L ∘SL f' ∘SL R) s x

If L and R are continuous semilinear maps with inverse scalar homomorphisms, and R maps s into t, then a derivative of f within t at R x transports to a derivative of L ∘ f ∘ R within s at x.

theorem DifferentiableWithinAt.comp_semilinear₂_of_tendsto {𝕜 : Type u_1} {𝕜' : Type u_2} {V : Type u_3} {V' : Type u_4} {W : Type u_5} {W' : Type u_6} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] {σ : 𝕜 →+* 𝕜'} {σ' : 𝕜' →+* 𝕜} [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [SeminormedAddCommGroup V'] [NormedSpace 𝕜' V'] [SeminormedAddCommGroup W] [NormedSpace 𝕜 W] [SeminormedAddCommGroup W'] [NormedSpace 𝕜' W'] [RingHomIsometric σ] [RingHomInvPair σ σ'] (L : W →SL[σ] W') (R : V' →SL[σ'] V) {f : V → W} {s : Set V'} {t : Set V} {x : V'} (hf : DifferentiableWithinAt 𝕜 f t (R x)) (hR : Filter.Tendsto (⇑R) (nhdsWithin x s) (nhdsWithin (R x) t)) : DifferentiableWithinAt 𝕜' (⇑L ∘ f ∘ ⇑R) s x

Composing on both sides by continuous semilinear maps with inverse scalar homomorphisms preserves differentiability within sets, provided the inner map tends to the target point within the target set.

theorem DifferentiableWithinAt.comp_semilinear₂ {𝕜 : Type u_1} {𝕜' : Type u_2} {V : Type u_3} {V' : Type u_4} {W : Type u_5} {W' : Type u_6} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] {σ : 𝕜 →+* 𝕜'} {σ' : 𝕜' →+* 𝕜} [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [SeminormedAddCommGroup V'] [NormedSpace 𝕜' V'] [SeminormedAddCommGroup W] [NormedSpace 𝕜 W] [SeminormedAddCommGroup W'] [NormedSpace 𝕜' W'] [RingHomIsometric σ] [RingHomInvPair σ σ'] (L : W →SL[σ] W') (R : V' →SL[σ'] V) {f : V → W} {s : Set V'} {t : Set V} {x : V'} (hf : DifferentiableWithinAt 𝕜 f t (R x)) (hR : Set.MapsTo (⇑R) s t) : DifferentiableWithinAt 𝕜' (⇑L ∘ f ∘ ⇑R) s x

Composing on both sides by continuous semilinear maps with inverse scalar homomorphisms preserves differentiability within sets when the inner map carries the source set into the target set.