Star operations on derivatives #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
For detailed documentation of the Fréchet derivative,
see the module docstring of analysis/calculus/fderiv/basic.lean.
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
has_strict_fderiv_at.star
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
[star_ring 𝕜]
[has_trivial_star 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[star_add_monoid F]
[normed_space 𝕜 F]
[star_module 𝕜 F]
[has_continuous_star F]
{f : E → F}
{f' : E →L[𝕜] F}
{x : E}
(h : has_strict_fderiv_at f f' x) :
has_strict_fderiv_at (λ (x : E), has_star.star (f x)) (↑(starL' 𝕜).comp f') x
theorem
has_fderiv_at_filter.star
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
[star_ring 𝕜]
[has_trivial_star 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[star_add_monoid F]
[normed_space 𝕜 F]
[star_module 𝕜 F]
[has_continuous_star F]
{f : E → F}
{f' : E →L[𝕜] F}
{x : E}
{L : filter E}
(h : has_fderiv_at_filter f f' x L) :
has_fderiv_at_filter (λ (x : E), has_star.star (f x)) (↑(starL' 𝕜).comp f') x L
theorem
has_fderiv_within_at.star
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
[star_ring 𝕜]
[has_trivial_star 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[star_add_monoid F]
[normed_space 𝕜 F]
[star_module 𝕜 F]
[has_continuous_star F]
{f : E → F}
{f' : E →L[𝕜] F}
{x : E}
{s : set E}
(h : has_fderiv_within_at f f' s x) :
has_fderiv_within_at (λ (x : E), has_star.star (f x)) (↑(starL' 𝕜).comp f') s x
theorem
has_fderiv_at.star
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
[star_ring 𝕜]
[has_trivial_star 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[star_add_monoid F]
[normed_space 𝕜 F]
[star_module 𝕜 F]
[has_continuous_star F]
{f : E → F}
{f' : E →L[𝕜] F}
{x : E}
(h : has_fderiv_at f f' x) :
has_fderiv_at (λ (x : E), has_star.star (f x)) (↑(starL' 𝕜).comp f') x
theorem
differentiable_within_at.star
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
[star_ring 𝕜]
[has_trivial_star 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[star_add_monoid F]
[normed_space 𝕜 F]
[star_module 𝕜 F]
[has_continuous_star F]
{f : E → F}
{x : E}
{s : set E}
(h : differentiable_within_at 𝕜 f s x) :
differentiable_within_at 𝕜 (λ (y : E), has_star.star (f y)) s x
@[simp]
theorem
differentiable_within_at_star_iff
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
[star_ring 𝕜]
[has_trivial_star 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[star_add_monoid F]
[normed_space 𝕜 F]
[star_module 𝕜 F]
[has_continuous_star F]
{f : E → F}
{x : E}
{s : set E} :
differentiable_within_at 𝕜 (λ (y : E), has_star.star (f y)) s x ↔ differentiable_within_at 𝕜 f s x
theorem
differentiable_at.star
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
[star_ring 𝕜]
[has_trivial_star 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[star_add_monoid F]
[normed_space 𝕜 F]
[star_module 𝕜 F]
[has_continuous_star F]
{f : E → F}
{x : E}
(h : differentiable_at 𝕜 f x) :
differentiable_at 𝕜 (λ (y : E), has_star.star (f y)) x
@[simp]
theorem
differentiable_at_star_iff
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
[star_ring 𝕜]
[has_trivial_star 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[star_add_monoid F]
[normed_space 𝕜 F]
[star_module 𝕜 F]
[has_continuous_star F]
{f : E → F}
{x : E} :
differentiable_at 𝕜 (λ (y : E), has_star.star (f y)) x ↔ differentiable_at 𝕜 f x
theorem
differentiable_on.star
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
[star_ring 𝕜]
[has_trivial_star 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[star_add_monoid F]
[normed_space 𝕜 F]
[star_module 𝕜 F]
[has_continuous_star F]
{f : E → F}
{s : set E}
(h : differentiable_on 𝕜 f s) :
differentiable_on 𝕜 (λ (y : E), has_star.star (f y)) s
@[simp]
theorem
differentiable_on_star_iff
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
[star_ring 𝕜]
[has_trivial_star 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[star_add_monoid F]
[normed_space 𝕜 F]
[star_module 𝕜 F]
[has_continuous_star F]
{f : E → F}
{s : set E} :
differentiable_on 𝕜 (λ (y : E), has_star.star (f y)) s ↔ differentiable_on 𝕜 f s
theorem
differentiable.star
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
[star_ring 𝕜]
[has_trivial_star 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[star_add_monoid F]
[normed_space 𝕜 F]
[star_module 𝕜 F]
[has_continuous_star F]
{f : E → F}
(h : differentiable 𝕜 f) :
differentiable 𝕜 (λ (y : E), has_star.star (f y))
@[simp]
theorem
differentiable_star_iff
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
[star_ring 𝕜]
[has_trivial_star 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[star_add_monoid F]
[normed_space 𝕜 F]
[star_module 𝕜 F]
[has_continuous_star F]
{f : E → F} :
differentiable 𝕜 (λ (y : E), has_star.star (f y)) ↔ differentiable 𝕜 f
theorem
fderiv_within_star
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
[star_ring 𝕜]
[has_trivial_star 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[star_add_monoid F]
[normed_space 𝕜 F]
[star_module 𝕜 F]
[has_continuous_star F]
{f : E → F}
{x : E}
{s : set E}
(hxs : unique_diff_within_at 𝕜 s x) :
fderiv_within 𝕜 (λ (y : E), has_star.star (f y)) s x = ↑(starL' 𝕜).comp (fderiv_within 𝕜 f s x)
@[simp]
theorem
fderiv_star
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
[star_ring 𝕜]
[has_trivial_star 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[star_add_monoid F]
[normed_space 𝕜 F]
[star_module 𝕜 F]
[has_continuous_star F]
{f : E → F}
{x : E} :