Star operations on derivatives

This file contains the usual formulas (and existence assertions) for the Fréchet derivative of the star operation. For detailed documentation of the Fréchet derivative, see the module docstring of Analysis/Calculus/FDeriv/Basic.lean.

Most of the results in this file only apply when the field that the derivative is respect to has a trivial star operation; which as should be expected rules out 𝕜 = ℂ. The exceptions are HasFDerivAt.star_star and DifferentiableAt.star_star, showing that star ∘ f ∘ star is differentiable when f is (and giving a formula for its derivative).

theorem HasStrictFDerivAt.star {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [StarRing 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [StarAddMonoid F] [NormedSpace 𝕜 F] [StarModule 𝕜 F] [ContinuousStar F] {f : E → F} {f' : E →L[𝕜] F} {x : E} [TrivialStar 𝕜] (h : HasStrictFDerivAt f f' x) : HasStrictFDerivAt (fun (x : E) => star (f x)) ((↑(starL' 𝕜)).comp f') x

theorem HasFDerivAtFilter.star {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [StarRing 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [StarAddMonoid F] [NormedSpace 𝕜 F] [StarModule 𝕜 F] [ContinuousStar F] {f : E → F} {f' : E →L[𝕜] F} {x : E} {L : Filter E} [TrivialStar 𝕜] (h : HasFDerivAtFilter f f' x L) : HasFDerivAtFilter (fun (x : E) => star (f x)) ((↑(starL' 𝕜)).comp f') x L

theorem HasFDerivWithinAt.star {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [StarRing 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [StarAddMonoid F] [NormedSpace 𝕜 F] [StarModule 𝕜 F] [ContinuousStar F] {f : E → F} {f' : E →L[𝕜] F} {x : E} {s : Set E} [TrivialStar 𝕜] (h : HasFDerivWithinAt f f' s x) : HasFDerivWithinAt (fun (x : E) => star (f x)) ((↑(starL' 𝕜)).comp f') s x

theorem HasFDerivAt.star {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [StarRing 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [StarAddMonoid F] [NormedSpace 𝕜 F] [StarModule 𝕜 F] [ContinuousStar F] {f : E → F} {f' : E →L[𝕜] F} {x : E} [TrivialStar 𝕜] (h : HasFDerivAt f f' x) : HasFDerivAt (fun (x : E) => star (f x)) ((↑(starL' 𝕜)).comp f') x

theorem DifferentiableWithinAt.star {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [StarRing 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [StarAddMonoid F] [NormedSpace 𝕜 F] [StarModule 𝕜 F] [ContinuousStar F] {f : E → F} {x : E} {s : Set E} [TrivialStar 𝕜] (h : DifferentiableWithinAt 𝕜 f s x) : DifferentiableWithinAt 𝕜 (fun (y : E) => star (f y)) s x

@[simp]

theorem differentiableWithinAt_star_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [StarRing 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [StarAddMonoid F] [NormedSpace 𝕜 F] [StarModule 𝕜 F] [ContinuousStar F] {f : E → F} {x : E} {s : Set E} [TrivialStar 𝕜] : DifferentiableWithinAt 𝕜 (fun (y : E) => star (f y)) s x ↔ DifferentiableWithinAt 𝕜 f s x

theorem DifferentiableAt.star {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [StarRing 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [StarAddMonoid F] [NormedSpace 𝕜 F] [StarModule 𝕜 F] [ContinuousStar F] {f : E → F} {x : E} [TrivialStar 𝕜] (h : DifferentiableAt 𝕜 f x) : DifferentiableAt 𝕜 (fun (y : E) => star (f y)) x

@[simp]

theorem differentiableAt_star_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [StarRing 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [StarAddMonoid F] [NormedSpace 𝕜 F] [StarModule 𝕜 F] [ContinuousStar F] {f : E → F} {x : E} [TrivialStar 𝕜] : DifferentiableAt 𝕜 (fun (y : E) => star (f y)) x ↔ DifferentiableAt 𝕜 f x

theorem DifferentiableOn.star {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [StarRing 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [StarAddMonoid F] [NormedSpace 𝕜 F] [StarModule 𝕜 F] [ContinuousStar F] {f : E → F} {s : Set E} [TrivialStar 𝕜] (h : DifferentiableOn 𝕜 f s) : DifferentiableOn 𝕜 (fun (y : E) => star (f y)) s

@[simp]

theorem differentiableOn_star_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [StarRing 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [StarAddMonoid F] [NormedSpace 𝕜 F] [StarModule 𝕜 F] [ContinuousStar F] {f : E → F} {s : Set E} [TrivialStar 𝕜] : DifferentiableOn 𝕜 (fun (y : E) => star (f y)) s ↔ DifferentiableOn 𝕜 f s

theorem Differentiable.star {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [StarRing 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [StarAddMonoid F] [NormedSpace 𝕜 F] [StarModule 𝕜 F] [ContinuousStar F] {f : E → F} [TrivialStar 𝕜] (h : Differentiable 𝕜 f) : Differentiable 𝕜 fun (y : E) => star (f y)

@[simp]

theorem differentiable_star_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [StarRing 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [StarAddMonoid F] [NormedSpace 𝕜 F] [StarModule 𝕜 F] [ContinuousStar F] {f : E → F} [TrivialStar 𝕜] : (Differentiable 𝕜 fun (y : E) => star (f y)) ↔ Differentiable 𝕜 f

theorem fderivWithin_star {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [StarRing 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [StarAddMonoid F] [NormedSpace 𝕜 F] [StarModule 𝕜 F] [ContinuousStar F] {f : E → F} {x : E} {s : Set E} [TrivialStar 𝕜] (hxs : UniqueDiffWithinAt 𝕜 s x) : fderivWithin 𝕜 (fun (y : E) => star (f y)) s x = (↑(starL' 𝕜)).comp (fderivWithin 𝕜 f s x)

@[simp]

theorem fderiv_star {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [StarRing 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [StarAddMonoid F] [NormedSpace 𝕜 F] [StarModule 𝕜 F] [ContinuousStar F] {f : E → F} {x : E} [TrivialStar 𝕜] : fderiv 𝕜 (fun (y : E) => star (f y)) x = (↑(starL' 𝕜)).comp (fderiv 𝕜 f x)

Composing on the left and right with star

theorem HasFDerivAt.star_star {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [StarRing 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [StarAddMonoid F] [NormedSpace 𝕜 F] [StarModule 𝕜 F] [ContinuousStar F] [StarAddMonoid E] [StarModule 𝕜 E] [ContinuousStar E] [NormedStarGroup 𝕜] {f : E → F} {z : E} {f' : E →L[𝕜] F} (hf : HasFDerivAt f f' z) : HasFDerivAt (star ∘ f ∘ star) ((↑(starL 𝕜)).comp (f'.comp ↑(starL 𝕜))) (star z)

If f has derivative f' at z, then star ∘ f ∘ star has derivative starL ∘ f' ∘ starL at star z.

theorem DifferentiableAt.star_star {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [StarRing 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [StarAddMonoid F] [NormedSpace 𝕜 F] [StarModule 𝕜 F] [ContinuousStar F] [StarAddMonoid E] [StarModule 𝕜 E] [ContinuousStar E] [NormedStarGroup 𝕜] {f : E → F} {z : E} (hf : DifferentiableAt 𝕜 f z) : DifferentiableAt 𝕜 (star ∘ f ∘ star) (star z)

If f is differentiable at z, then star ∘ f ∘ star is differentiable at star z.