Derivatives of continuous-linear-map applications #
This file records a zero-value rule for differentiating the pointwise application of a varying continuous linear map. At a zero of the vector-valued argument, the variation of the operator contributes nothing to the derivative, so the operator-valued map need only be continuous. It also records the derivative of the application of a varying continuous linear map to a fixed vector.
Main declarations #
HasFDerivWithinAt.clm_apply_of_eq_zero: the derivative ofy ↦ c y (u y)at a zero ofu, assuming only continuity ofc.TauCeti.fderiv_clm_apply_const_apply: the derivative ofy ↦ c y vin the directionwisDc(w) v.
theorem
HasFDerivWithinAt.clm_apply_of_eq_zero
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{F' : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup F']
[NormedSpace 𝕜 F']
{c : E → F →L[𝕜] F'}
{u : E → F}
{u' : E →L[𝕜] F}
{s : Set E}
{z : E}
(hc : ContinuousWithinAt c s z)
(hu : HasFDerivWithinAt u u' s z)
(hu0 : u z = 0)
:
HasFDerivWithinAt (fun (y : E) => (c y) (u y)) (c z ∘SL u') s z
At a zero of u, the variation of c is multiplied by u y = O(y - z), so it contributes
nothing to the derivative.
theorem
TauCeti.fderiv_clm_apply_const_apply
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{F' : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup F']
[NormedSpace 𝕜 F']
{c : E → F →L[𝕜] F'}
{x : E}
(hc : DifferentiableAt 𝕜 c x)
(v : F)
(w : E)
:
Differentiating y ↦ c y v for a fixed vector v in the direction w gives the derivative
of c in the direction w, applied to v.