HasFDerivAtFilter.star

theorem HasFDerivAtFilter.star : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : StarRing 𝕜] [inst_2 : TrivialStar 𝕜] {E : Type u_2} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E] {F : Type u_3} [inst_5 : NormedAddCommGroup F] [inst_6 : StarAddMonoid F] [inst_7 : NormedSpace 𝕜 F] [inst_8 : StarModule 𝕜 F] [inst_9 : ContinuousStar F] {f : E → F} {f' : E →L[𝕜] F} {x : E} {L : Filter E}, HasFDerivAtFilter f f' x L → HasFDerivAtFilter (fun x => star (f x)) ((↑(starL' 𝕜)).comp f') x L

This theorem states that if a function `f` from a normed additive commutative group `E` to a star add monoid `F`, both of which are normed spaces over a nontrivially normed field `𝕜` with star structure, has a derivative `f'` at a point `x` with respect to a filter `L`, then the function that maps `x` to the star of `f(x)` also has a derivative at `x` with respect to `L`. The derivative of the latter function is the composition of `f'` and the continuous linear map induced by the star operation on `𝕜`.

More concisely: If `f: E → F` is a differentiable function from a normed additive commutative group `E` to a star add monoid `F` over a nontrivially normed field `𝕜` with star structure, then the function `x mapsto 𝓝(f(x))` (where `𝓝` denotes the star operation on `F`) is differentiable at `x` and its derivative is `𝓝(f'(x)) ∘ 🌍(x)`, where `🌍: 𝕜 → 𝓝(𝕜)` is the continuous linear map induced by the star operation on `𝕜`.