mathlib3 documentation

analysis.calculus.deriv.star

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)