Star operations on derivatives #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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 𝕜 = ℂ.
Derivative of x ↦ star x #
@[protected]
theorem
has_deriv_at_filter.star
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{F : Type v}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{f : 𝕜 → F}
{f' : F}
{x : 𝕜}
{L : filter 𝕜}
[star_ring 𝕜]
[has_trivial_star 𝕜]
[star_add_monoid F]
[has_continuous_star F]
[star_module 𝕜 F]
(h : has_deriv_at_filter f f' x L) :
has_deriv_at_filter (λ (x : 𝕜), has_star.star (f x)) (has_star.star f') x L
@[protected]
theorem
has_deriv_within_at.star
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{F : Type v}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{f : 𝕜 → F}
{f' : F}
{x : 𝕜}
{s : set 𝕜}
[star_ring 𝕜]
[has_trivial_star 𝕜]
[star_add_monoid F]
[has_continuous_star F]
[star_module 𝕜 F]
(h : has_deriv_within_at f f' s x) :
has_deriv_within_at (λ (x : 𝕜), has_star.star (f x)) (has_star.star f') s x
@[protected]
theorem
has_deriv_at.star
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{F : Type v}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{f : 𝕜 → F}
{f' : F}
{x : 𝕜}
[star_ring 𝕜]
[has_trivial_star 𝕜]
[star_add_monoid F]
[has_continuous_star F]
[star_module 𝕜 F]
(h : has_deriv_at f f' x) :
has_deriv_at (λ (x : 𝕜), has_star.star (f x)) (has_star.star f') x
@[protected]
theorem
has_strict_deriv_at.star
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{F : Type v}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{f : 𝕜 → F}
{f' : F}
{x : 𝕜}
[star_ring 𝕜]
[has_trivial_star 𝕜]
[star_add_monoid F]
[has_continuous_star F]
[star_module 𝕜 F]
(h : has_strict_deriv_at f f' x) :
has_strict_deriv_at (λ (x : 𝕜), has_star.star (f x)) (has_star.star f') x
@[protected]
theorem
deriv_within.star
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{F : Type v}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{f : 𝕜 → F}
{x : 𝕜}
{s : set 𝕜}
[star_ring 𝕜]
[has_trivial_star 𝕜]
[star_add_monoid F]
[has_continuous_star F]
[star_module 𝕜 F]
(hxs : unique_diff_within_at 𝕜 s x) :
deriv_within (λ (y : 𝕜), has_star.star (f y)) s x = has_star.star (deriv_within f s x)
@[protected]
theorem
deriv.star
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{F : Type v}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{f : 𝕜 → F}
{x : 𝕜}
[star_ring 𝕜]
[has_trivial_star 𝕜]
[star_add_monoid F]
[has_continuous_star F]
[star_module 𝕜 F] :
deriv (λ (y : 𝕜), has_star.star (f y)) x = has_star.star (deriv f x)
@[protected, simp]
theorem
deriv.star'
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{F : Type v}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{f : 𝕜 → F}
[star_ring 𝕜]
[has_trivial_star 𝕜]
[star_add_monoid F]
[has_continuous_star F]
[star_module 𝕜 F] :
deriv (λ (y : 𝕜), has_star.star (f y)) = λ (x : 𝕜), has_star.star (deriv f x)