Star operations on derivatives

For detailed documentation of the Fréchet derivative, see the module docstring of Analysis/Calculus/FDeriv/Basic.lean.

This file contains the usual formulas (and existence assertions) for the derivative of the star operation. Note that these only apply when the field that the derivative is respect to has a trivial star operation; which as should be expected rules out 𝕜 = ℂ.

theorem HasStrictFDerivAt.star {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [StarRing 𝕜] [TrivialStar 𝕜] {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} (h : HasStrictFDerivAt f f' x) : HasStrictFDerivAt (fun (x : E) => star (f x)) (ContinuousLinearMap.comp (↑(starL' 𝕜)) f') x

theorem HasFDerivAtFilter.star {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [StarRing 𝕜] [TrivialStar 𝕜] {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} (h : HasFDerivAtFilter f f' x L) : HasFDerivAtFilter (fun (x : E) => star (f x)) (ContinuousLinearMap.comp (↑(starL' 𝕜)) f') x L

theorem HasFDerivWithinAt.star {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [StarRing 𝕜] [TrivialStar 𝕜] {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} (h : HasFDerivWithinAt f f' s x) : HasFDerivWithinAt (fun (x : E) => star (f x)) (ContinuousLinearMap.comp (↑(starL' 𝕜)) f') s x

theorem HasFDerivAt.star {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [StarRing 𝕜] [TrivialStar 𝕜] {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} (h : HasFDerivAt f f' x) : HasFDerivAt (fun (x : E) => star (f x)) (ContinuousLinearMap.comp (↑(starL' 𝕜)) f') x

theorem DifferentiableWithinAt.star {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [StarRing 𝕜] [TrivialStar 𝕜] {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} (h : DifferentiableWithinAt 𝕜 f s x) : DifferentiableWithinAt 𝕜 (fun (y : E) => star (f y)) s x

@[simp]

theorem differentiableWithinAt_star_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [StarRing 𝕜] [TrivialStar 𝕜] {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} : DifferentiableWithinAt 𝕜 (fun (y : E) => star (f y)) s x ↔ DifferentiableWithinAt 𝕜 f s x

theorem DifferentiableAt.star {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [StarRing 𝕜] [TrivialStar 𝕜] {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} (h : DifferentiableAt 𝕜 f x) : DifferentiableAt 𝕜 (fun (y : E) => star (f y)) x

@[simp]

theorem differentiableAt_star_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [StarRing 𝕜] [TrivialStar 𝕜] {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} : DifferentiableAt 𝕜 (fun (y : E) => star (f y)) x ↔ DifferentiableAt 𝕜 f x

theorem DifferentiableOn.star {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [StarRing 𝕜] [TrivialStar 𝕜] {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} (h : DifferentiableOn 𝕜 f s) : DifferentiableOn 𝕜 (fun (y : E) => star (f y)) s

@[simp]

theorem differentiableOn_star_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [StarRing 𝕜] [TrivialStar 𝕜] {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} : DifferentiableOn 𝕜 (fun (y : E) => star (f y)) s ↔ DifferentiableOn 𝕜 f s

theorem Differentiable.star {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [StarRing 𝕜] [TrivialStar 𝕜] {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} (h : Differentiable 𝕜 f) : Differentiable 𝕜 fun (y : E) => star (f y)

@[simp]

theorem differentiable_star_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [StarRing 𝕜] [TrivialStar 𝕜] {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} : (Differentiable 𝕜 fun (y : E) => star (f y)) ↔ Differentiable 𝕜 f

theorem fderivWithin_star {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [StarRing 𝕜] [TrivialStar 𝕜] {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} (hxs : UniqueDiffWithinAt 𝕜 s x) : fderivWithin 𝕜 (fun (y : E) => star (f y)) s x = ContinuousLinearMap.comp (↑(starL' 𝕜)) (fderivWithin 𝕜 f s x)

@[simp]

theorem fderiv_star {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [StarRing 𝕜] [TrivialStar 𝕜] {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} : fderiv 𝕜 (fun (y : E) => star (f y)) x = ContinuousLinearMap.comp (↑(starL' 𝕜)) (fderiv 𝕜 f x)