Star operations on derivatives

This file contains the usual formulas (and existence assertions) for the derivative of the star operation.

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 HasDerivAt.conj_conj and DifferentiableAt.conj_conj, showing that conj ∘ f ∘ conj is differentiable when f is (and giving a formula for its derivative).

Derivative of x ↦ star x

theorem HasDerivAtFilter.star {𝕜 : Type u} [NontriviallyNormedField 𝕜] [StarRing 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [StarAddMonoid F] [StarModule 𝕜 F] [ContinuousStar F] {f : 𝕜 → F} {f' : F} [TrivialStar 𝕜] {L : Filter (𝕜 × 𝕜)} (h : HasDerivAtFilter f f' L) : HasDerivAtFilter (fun (x : 𝕜) => star (f x)) (star f') L

theorem HasDerivWithinAt.star {𝕜 : Type u} [NontriviallyNormedField 𝕜] [StarRing 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [StarAddMonoid F] [StarModule 𝕜 F] [ContinuousStar F] {f : 𝕜 → F} {f' : F} {x : 𝕜} [TrivialStar 𝕜] {s : Set 𝕜} (h : HasDerivWithinAt f f' s x) : HasDerivWithinAt (fun (x : 𝕜) => star (f x)) (star f') s x

theorem HasDerivAt.star {𝕜 : Type u} [NontriviallyNormedField 𝕜] [StarRing 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [StarAddMonoid F] [StarModule 𝕜 F] [ContinuousStar F] {f : 𝕜 → F} {f' : F} {x : 𝕜} [TrivialStar 𝕜] (h : HasDerivAt f f' x) : HasDerivAt (fun (x : 𝕜) => star (f x)) (star f') x

theorem HasStrictDerivAt.star {𝕜 : Type u} [NontriviallyNormedField 𝕜] [StarRing 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [StarAddMonoid F] [StarModule 𝕜 F] [ContinuousStar F] {f : 𝕜 → F} {f' : F} {x : 𝕜} [TrivialStar 𝕜] (h : HasStrictDerivAt f f' x) : HasStrictDerivAt (fun (x : 𝕜) => star (f x)) (star f') x

theorem derivWithin.star {𝕜 : Type u} [NontriviallyNormedField 𝕜] [StarRing 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [StarAddMonoid F] [StarModule 𝕜 F] [ContinuousStar F] {f : 𝕜 → F} {x : 𝕜} [TrivialStar 𝕜] {s : Set 𝕜} : derivWithin (fun (y : 𝕜) => star (f y)) s x = star (derivWithin f s x)

theorem deriv.star {𝕜 : Type u} [NontriviallyNormedField 𝕜] [StarRing 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [StarAddMonoid F] [StarModule 𝕜 F] [ContinuousStar F] {f : 𝕜 → F} {x : 𝕜} [TrivialStar 𝕜] : deriv (fun (y : 𝕜) => star (f y)) x = star (deriv f x)

@[simp]

theorem deriv.star' {𝕜 : Type u} [NontriviallyNormedField 𝕜] [StarRing 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [StarAddMonoid F] [StarModule 𝕜 F] [ContinuousStar F] {f : 𝕜 → F} [TrivialStar 𝕜] : (deriv fun (y : 𝕜) => star (f y)) = fun (x : 𝕜) => star (deriv f x)

theorem HasDerivAt.star_conj {𝕜 : Type u} [NontriviallyNormedField 𝕜] [StarRing 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [StarAddMonoid F] [StarModule 𝕜 F] [ContinuousStar F] {x : 𝕜} [NormedStarGroup 𝕜] {f : 𝕜 → F} {f' : F} (hf : HasDerivAt f f' x) : HasDerivAt (star ∘ f ∘ ⇑(starRingEnd 𝕜)) (star f') ((starRingEnd 𝕜) x)

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

@[simp]

theorem hasDerivAt_star_conj_iff {𝕜 : Type u} [NontriviallyNormedField 𝕜] [StarRing 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [StarAddMonoid F] [StarModule 𝕜 F] [ContinuousStar F] [NormedStarGroup 𝕜] {f : 𝕜 → F} {x : 𝕜} {f' : F} : HasDerivAt (star ∘ f ∘ ⇑(starRingEnd 𝕜)) f' x ↔ HasDerivAt f (star f') ((starRingEnd 𝕜) x)

A function f has derivative f' at z iff star ∘ f ∘ conj has derivative star f' at conj z.

theorem HasDerivAt.conj_conj {𝕜 : Type u} [NontriviallyNormedField 𝕜] [StarRing 𝕜] {x : 𝕜} [NormedStarGroup 𝕜] {f : 𝕜 → 𝕜} {f' : 𝕜} (hf : HasDerivAt f f' x) : HasDerivAt (⇑(starRingEnd 𝕜) ∘ f ∘ ⇑(starRingEnd 𝕜)) ((starRingEnd 𝕜) f') ((starRingEnd 𝕜) x)

If f has derivative f' at z, then conj ∘ f ∘ conj has derivative conj f' at conj z.

@[simp]

theorem hasDerivAt_conj_conj_iff {𝕜 : Type u} [NontriviallyNormedField 𝕜] [StarRing 𝕜] [NormedStarGroup 𝕜] {f : 𝕜 → 𝕜} {x f' : 𝕜} : HasDerivAt (⇑(starRingEnd 𝕜) ∘ f ∘ ⇑(starRingEnd 𝕜)) f' x ↔ HasDerivAt f ((starRingEnd 𝕜) f') ((starRingEnd 𝕜) x)

A function f has derivative f' at z iff conj ∘ f ∘ conj has derivative conj f' at conj z.

theorem DifferentiableAt.star_conj {𝕜 : Type u} [NontriviallyNormedField 𝕜] [StarRing 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [StarAddMonoid F] [StarModule 𝕜 F] [ContinuousStar F] {x : 𝕜} [NormedStarGroup 𝕜] {f : 𝕜 → F} (hf : DifferentiableAt 𝕜 f x) : DifferentiableAt 𝕜 (star ∘ f ∘ ⇑(starRingEnd 𝕜)) ((starRingEnd 𝕜) x)

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

@[simp]

theorem differentiableAt_star_conj_iff {𝕜 : Type u} [NontriviallyNormedField 𝕜] [StarRing 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [StarAddMonoid F] [StarModule 𝕜 F] [ContinuousStar F] {x : 𝕜} [NormedStarGroup 𝕜] {f : 𝕜 → F} : DifferentiableAt 𝕜 (star ∘ f ∘ ⇑(starRingEnd 𝕜)) x ↔ DifferentiableAt 𝕜 f ((starRingEnd 𝕜) x)

A function f is differentiable at conj z iff star ∘ f ∘ conj is differentiable at z.

theorem DifferentiableAt.conj_conj {𝕜 : Type u} [NontriviallyNormedField 𝕜] [StarRing 𝕜] {x : 𝕜} [NormedStarGroup 𝕜] {f : 𝕜 → 𝕜} (hf : DifferentiableAt 𝕜 f x) : DifferentiableAt 𝕜 (⇑(starRingEnd 𝕜) ∘ f ∘ ⇑(starRingEnd 𝕜)) ((starRingEnd 𝕜) x)

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

@[simp]

theorem differentiableAt_conj_conj_iff {𝕜 : Type u} [NontriviallyNormedField 𝕜] [StarRing 𝕜] {x : 𝕜} [NormedStarGroup 𝕜] {f : 𝕜 → 𝕜} : DifferentiableAt 𝕜 (⇑(starRingEnd 𝕜) ∘ f ∘ ⇑(starRingEnd 𝕜)) x ↔ DifferentiableAt 𝕜 f ((starRingEnd 𝕜) x)

A function f is differentiable at conj z iff conj ∘ f ∘ conj is differentiable at z.

@[simp]

theorem deriv_star_conj {𝕜 : Type u} [NontriviallyNormedField 𝕜] [StarRing 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [StarAddMonoid F] [StarModule 𝕜 F] [ContinuousStar F] [NormedStarGroup 𝕜] {f : 𝕜 → F} : deriv (star ∘ f ∘ ⇑(starRingEnd 𝕜)) = star ∘ deriv f ∘ ⇑(starRingEnd 𝕜)

The derivative of star ∘ f ∘ conj is star ∘ deriv f ∘ conj.

@[simp]

theorem deriv_conj_conj {𝕜 : Type u} [NontriviallyNormedField 𝕜] [StarRing 𝕜] [NormedStarGroup 𝕜] {f : 𝕜 → 𝕜} : deriv (⇑(starRingEnd 𝕜) ∘ f ∘ ⇑(starRingEnd 𝕜)) = ⇑(starRingEnd 𝕜) ∘ deriv f ∘ ⇑(starRingEnd 𝕜)

The derivative of conj ∘ f ∘ conj is conj ∘ deriv f ∘ conj.