Star operations on derivatives #
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
HasDerivAtFilter.star
{𝕜 : Type u}
[NontriviallyNormedField 𝕜]
{F : Type v}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : 𝕜 → F}
[StarRing 𝕜]
[TrivialStar 𝕜]
[StarAddMonoid F]
[ContinuousStar F]
[StarModule 𝕜 F]
{f' : F}
{x : 𝕜}
{L : Filter 𝕜}
(h : HasDerivAtFilter f f' x L)
:
HasDerivAtFilter (fun (x : 𝕜) => star (f x)) (star f') x L
theorem
HasDerivWithinAt.star
{𝕜 : Type u}
[NontriviallyNormedField 𝕜]
{F : Type v}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : 𝕜 → F}
[StarRing 𝕜]
[TrivialStar 𝕜]
[StarAddMonoid F]
[ContinuousStar F]
[StarModule 𝕜 F]
{f' : F}
{s : Set 𝕜}
{x : 𝕜}
(h : HasDerivWithinAt f f' s x)
:
HasDerivWithinAt (fun (x : 𝕜) => star (f x)) (star f') s x
theorem
HasDerivAt.star
{𝕜 : Type u}
[NontriviallyNormedField 𝕜]
{F : Type v}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : 𝕜 → F}
[StarRing 𝕜]
[TrivialStar 𝕜]
[StarAddMonoid F]
[ContinuousStar F]
[StarModule 𝕜 F]
{f' : F}
{x : 𝕜}
(h : HasDerivAt f f' x)
:
HasDerivAt (fun (x : 𝕜) => star (f x)) (star f') x
theorem
HasStrictDerivAt.star
{𝕜 : Type u}
[NontriviallyNormedField 𝕜]
{F : Type v}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : 𝕜 → F}
[StarRing 𝕜]
[TrivialStar 𝕜]
[StarAddMonoid F]
[ContinuousStar F]
[StarModule 𝕜 F]
{f' : F}
{x : 𝕜}
(h : HasStrictDerivAt f f' x)
:
HasStrictDerivAt (fun (x : 𝕜) => star (f x)) (star f') x
theorem
derivWithin.star
{𝕜 : Type u}
[NontriviallyNormedField 𝕜]
{F : Type v}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : 𝕜 → F}
[StarRing 𝕜]
[TrivialStar 𝕜]
[StarAddMonoid F]
[ContinuousStar F]
[StarModule 𝕜 F]
{s : Set 𝕜}
{x : 𝕜}
(hxs : UniqueDiffWithinAt 𝕜 s x)
:
derivWithin (fun (y : 𝕜) => star (f y)) s x = star (derivWithin f s x)
theorem
deriv.star
{𝕜 : Type u}
[NontriviallyNormedField 𝕜]
{F : Type v}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : 𝕜 → F}
[StarRing 𝕜]
[TrivialStar 𝕜]
[StarAddMonoid F]
[ContinuousStar F]
[StarModule 𝕜 F]
{x : 𝕜}
:
@[simp]
theorem
deriv.star'
{𝕜 : Type u}
[NontriviallyNormedField 𝕜]
{F : Type v}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : 𝕜 → F}
[StarRing 𝕜]
[TrivialStar 𝕜]
[StarAddMonoid F]
[ContinuousStar F]
[StarModule 𝕜 F]
: