Manifold derivatives of continuous-linear-map applications

This file records a local-calculus fact for vector-valued maps on manifolds: at a zero of a vector-valued map u, the derivative of a varying continuous linear map c applied to u has no contribution from the varying operator. Since that contribution is multiplied by u = 0, the operator c need only be continuous, not differentiable.

On a normed space, the imported theorem HasFDerivWithinAt.clm_apply_of_eq_zero is a variant of HasFDerivWithinAt.clm_apply needing only continuity of c. The manifold formula mvfderiv_eq_comp_of_eventuallyEq_clm_apply is its counterpart in charts, specialized to the case used when differentiating changes of fiber coordinates at the zero of a bundle section. It is stated for any map agreeing with y ↦ c y (u y) near the point, which is how fiber coordinates in two trivializations are related.

For maps on a normed space, it also records how mvfderiv acts on vectors given in the model space through NormedSpace.fromTangentSpace: there it is the Fréchet derivative. The precomposing continuous linear map may have any module equipped with a topology as its source.

theorem TauCeti.mvfderiv_eq_comp_of_eventuallyEq_clm_apply {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} {M : Type u_4} {F : Type u_5} {F' : Type u_6} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [TopologicalSpace M] [ChartedSpace H M] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] {x : M} {f : M → F'} {c : M → F →L[𝕜] F'} {u : M → F} (hf : (fun (y : M) => (c y) (u y)) =ᶠ[nhds x] f) (hc : ContinuousAt c x) (hu : MDiffAt u x) (hu0 : u x = 0) : d% f x = c x ∘SL d% u x

At a zero of u, a map agreeing near x with y ↦ c y (u y) has derivative c x composed with the derivative of u: the variation of c is multiplied by u x = 0, so c need only be continuous at x.

theorem TauCeti.mvfderiv_clm_apply_const {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} {M : Type u_4} {F : Type u_5} {F' : Type u_6} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [TopologicalSpace M] [ChartedSpace H M] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] {x : M} {c : M → F →L[𝕜] F'} (hc : MDiffAt c x) (w : F) (v : TangentSpace I x) : ((d% fun (z : M) => (c z) w) x) v = ((d% c x) v) w

Applying a differentiable family of continuous linear maps to a fixed vector commutes with the vector-valued manifold derivative: d (fun z ↦ c z w) x v = (d c x v) w.

theorem ContinuousLinearMap.mvfderiv_comp_fromTangentSpace_symm_comp {𝕜 : Type u_1} {E : Type u_2} {F : Type u_5} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_7} [TopologicalSpace G] [AddCommMonoid G] [Module 𝕜 G] {f : E → F} {z : E} (L : G →L[𝕜] E) : d% f z ∘SL ↑(NormedSpace.fromTangentSpace z).symm ∘SL L = fderiv 𝕜 f z ∘SL L

On a normed space, the vector-valued manifold derivative applied to model-space vectors L v, viewed as tangent vectors via NormedSpace.fromTangentSpace, is the Fréchet derivative applied to L v. No norm is required on the source of L.