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).
theorem
HasDerivAtFilter.star
{𝕜 : Type u}
[NontriviallyNormedField 𝕜]
[StarRing 𝕜]
{F : Type v}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[StarAddMonoid F]
[StarModule 𝕜 F]
[ContinuousStar F]
{f : 𝕜 → F}
{f' : F}
{x : 𝕜}
[TrivialStar 𝕜]
{L : Filter 𝕜}
(h : HasDerivAtFilter f f' x L)
:
HasDerivAtFilter (fun (x : 𝕜) => star (f x)) (star f') x 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 𝕜}
:
theorem
deriv.star
{𝕜 : Type u}
[NontriviallyNormedField 𝕜]
[StarRing 𝕜]
{F : Type v}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[StarAddMonoid F]
[StarModule 𝕜 F]
[ContinuousStar F]
{f : 𝕜 → F}
{x : 𝕜}
[TrivialStar 𝕜]
:
@[simp]
theorem
deriv.star'
{𝕜 : Type u}
[NontriviallyNormedField 𝕜]
[StarRing 𝕜]
{F : Type v}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[StarAddMonoid F]
[StarModule 𝕜 F]
[ContinuousStar F]
{f : 𝕜 → F}
[TrivialStar 𝕜]
:
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 conj 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.
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.