Documentation

Mathlib.Analysis.Calculus.FDeriv.Star

Star operations on derivatives #

This file contains the usual formulas (and existence assertions) for the FrΓ©chet derivative of the star operation. For detailed documentation of the FrΓ©chet derivative, see the module docstring of Analysis/Calculus/FDeriv/Basic.lean.

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 HasFDerivAt.star_star and DifferentiableAt.star_star, showing that star ∘ f ∘ star is differentiable when f is (and giving a formula for its derivative).

theorem HasStrictFDerivAt.star {π•œ : Type u_1} [NontriviallyNormedField π•œ] [StarRing π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [StarAddMonoid F] [NormedSpace π•œ F] [StarModule π•œ F] [ContinuousStar F] {f : E β†’ F} {f' : E β†’L[π•œ] F} {x : E} [TrivialStar π•œ] (h : HasStrictFDerivAt f f' x) :
HasStrictFDerivAt (fun (x : E) => star (f x)) ((↑(starL' π•œ)).comp f') x
theorem HasFDerivAtFilter.star {π•œ : Type u_1} [NontriviallyNormedField π•œ] [StarRing π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [StarAddMonoid F] [NormedSpace π•œ F] [StarModule π•œ F] [ContinuousStar F] {f : E β†’ F} {f' : E β†’L[π•œ] F} {x : E} {L : Filter E} [TrivialStar π•œ] (h : HasFDerivAtFilter f f' x L) :
HasFDerivAtFilter (fun (x : E) => star (f x)) ((↑(starL' π•œ)).comp f') x L
theorem HasFDerivWithinAt.star {π•œ : Type u_1} [NontriviallyNormedField π•œ] [StarRing π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [StarAddMonoid F] [NormedSpace π•œ F] [StarModule π•œ F] [ContinuousStar F] {f : E β†’ F} {f' : E β†’L[π•œ] F} {x : E} {s : Set E} [TrivialStar π•œ] (h : HasFDerivWithinAt f f' s x) :
HasFDerivWithinAt (fun (x : E) => star (f x)) ((↑(starL' π•œ)).comp f') s x
theorem HasFDerivAt.star {π•œ : Type u_1} [NontriviallyNormedField π•œ] [StarRing π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [StarAddMonoid F] [NormedSpace π•œ F] [StarModule π•œ F] [ContinuousStar F] {f : E β†’ F} {f' : E β†’L[π•œ] F} {x : E} [TrivialStar π•œ] (h : HasFDerivAt f f' x) :
HasFDerivAt (fun (x : E) => star (f x)) ((↑(starL' π•œ)).comp f') x
theorem DifferentiableWithinAt.star {π•œ : Type u_1} [NontriviallyNormedField π•œ] [StarRing π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [StarAddMonoid F] [NormedSpace π•œ F] [StarModule π•œ F] [ContinuousStar F] {f : E β†’ F} {x : E} {s : Set E} [TrivialStar π•œ] (h : DifferentiableWithinAt π•œ f s x) :
DifferentiableWithinAt π•œ (fun (y : E) => star (f y)) s x
@[simp]
theorem differentiableWithinAt_star_iff {π•œ : Type u_1} [NontriviallyNormedField π•œ] [StarRing π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [StarAddMonoid F] [NormedSpace π•œ F] [StarModule π•œ F] [ContinuousStar F] {f : E β†’ F} {x : E} {s : Set E} [TrivialStar π•œ] :
DifferentiableWithinAt π•œ (fun (y : E) => star (f y)) s x ↔ DifferentiableWithinAt π•œ f s x
theorem DifferentiableAt.star {π•œ : Type u_1} [NontriviallyNormedField π•œ] [StarRing π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [StarAddMonoid F] [NormedSpace π•œ F] [StarModule π•œ F] [ContinuousStar F] {f : E β†’ F} {x : E} [TrivialStar π•œ] (h : DifferentiableAt π•œ f x) :
DifferentiableAt π•œ (fun (y : E) => star (f y)) x
@[simp]
theorem differentiableAt_star_iff {π•œ : Type u_1} [NontriviallyNormedField π•œ] [StarRing π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [StarAddMonoid F] [NormedSpace π•œ F] [StarModule π•œ F] [ContinuousStar F] {f : E β†’ F} {x : E} [TrivialStar π•œ] :
DifferentiableAt π•œ (fun (y : E) => star (f y)) x ↔ DifferentiableAt π•œ f x
theorem DifferentiableOn.star {π•œ : Type u_1} [NontriviallyNormedField π•œ] [StarRing π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [StarAddMonoid F] [NormedSpace π•œ F] [StarModule π•œ F] [ContinuousStar F] {f : E β†’ F} {s : Set E} [TrivialStar π•œ] (h : DifferentiableOn π•œ f s) :
DifferentiableOn π•œ (fun (y : E) => star (f y)) s
@[simp]
theorem differentiableOn_star_iff {π•œ : Type u_1} [NontriviallyNormedField π•œ] [StarRing π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [StarAddMonoid F] [NormedSpace π•œ F] [StarModule π•œ F] [ContinuousStar F] {f : E β†’ F} {s : Set E} [TrivialStar π•œ] :
DifferentiableOn π•œ (fun (y : E) => star (f y)) s ↔ DifferentiableOn π•œ f s
theorem Differentiable.star {π•œ : Type u_1} [NontriviallyNormedField π•œ] [StarRing π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [StarAddMonoid F] [NormedSpace π•œ F] [StarModule π•œ F] [ContinuousStar F] {f : E β†’ F} [TrivialStar π•œ] (h : Differentiable π•œ f) :
Differentiable π•œ fun (y : E) => star (f y)
@[simp]
theorem differentiable_star_iff {π•œ : Type u_1} [NontriviallyNormedField π•œ] [StarRing π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [StarAddMonoid F] [NormedSpace π•œ F] [StarModule π•œ F] [ContinuousStar F] {f : E β†’ F} [TrivialStar π•œ] :
(Differentiable π•œ fun (y : E) => star (f y)) ↔ Differentiable π•œ f
theorem fderivWithin_star {π•œ : Type u_1} [NontriviallyNormedField π•œ] [StarRing π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [StarAddMonoid F] [NormedSpace π•œ F] [StarModule π•œ F] [ContinuousStar F] {f : E β†’ F} {x : E} {s : Set E} [TrivialStar π•œ] (hxs : UniqueDiffWithinAt π•œ s x) :
fderivWithin π•œ (fun (y : E) => star (f y)) s x = (↑(starL' π•œ)).comp (fderivWithin π•œ f s x)
@[simp]
theorem fderiv_star {π•œ : Type u_1} [NontriviallyNormedField π•œ] [StarRing π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [StarAddMonoid F] [NormedSpace π•œ F] [StarModule π•œ F] [ContinuousStar F] {f : E β†’ F} {x : E} [TrivialStar π•œ] :
fderiv π•œ (fun (y : E) => star (f y)) x = (↑(starL' π•œ)).comp (fderiv π•œ f x)

Composing on the left and right with star #

theorem HasFDerivAt.star_star {π•œ : Type u_1} [NontriviallyNormedField π•œ] [StarRing π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [StarAddMonoid F] [NormedSpace π•œ F] [StarModule π•œ F] [ContinuousStar F] [StarAddMonoid E] [StarModule π•œ E] [ContinuousStar E] [NormedStarGroup π•œ] {f : E β†’ F} {z : E} {f' : E β†’L[π•œ] F} (hf : HasFDerivAt f f' z) :
HasFDerivAt (star ∘ f ∘ star) ((↑(starL π•œ)).comp (f'.comp ↑(starL π•œ))) (star z)

If f has derivative f' at z, then star ∘ f ∘ star has derivative starL ∘ f' ∘ starL at star z.

theorem DifferentiableAt.star_star {π•œ : Type u_1} [NontriviallyNormedField π•œ] [StarRing π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [StarAddMonoid F] [NormedSpace π•œ F] [StarModule π•œ F] [ContinuousStar F] [StarAddMonoid E] [StarModule π•œ E] [ContinuousStar E] [NormedStarGroup π•œ] {f : E β†’ F} {z : E} (hf : DifferentiableAt π•œ f z) :

If f is differentiable at z, then star ∘ f ∘ star is differentiable at star z.