Basic facts about manifold derivatives

This file collects general facts about mfderiv that need nothing beyond Mathlib's basic manifold-derivative API.

Main results

• TauCeti.mfderiv_comp_of_apply_eq_self: the chain rule at a fixed point f x = x, with both derivatives taken at x, so the composite is an endomorphism of the single tangent space T_x M.
• HasMFDerivAt.iterate: the chain rule for iterates at a fixed point, d(f^[n])_x = (df_x) ^ n.
• TauCeti.mfderiv_injective_of_leftInverse: a map with a left inverse differentiable along its image has injective derivative.
• TauCeti.mfderiv_comp_const_add_smul_apply: the chain rule for the affine reparametrization w ↦ c + ε • w of a map from a normed space, d(u(c + ε •))_w = ε • du_(c + ε • w), with no differentiability hypothesis.

theorem TauCeti.mfderiv_comp_of_apply_eq_self {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} {M : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [TopologicalSpace M] [ChartedSpace H M] {x : M} {f g : M → M} (hg : MDiffAt g x) (hf : MDiffAt f x) (hfx : f x = x) : mfderiv% (g ∘ f) x = mfderiv% g x ∘SL mfderiv% f x

The chain rule at a fixed point: if f x = x, the derivative of g ∘ f at x is the composite of the derivatives of g and f at x, the tangent space at f x being that at x.

theorem HasMFDerivAt.iterate {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} {M : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [TopologicalSpace M] [ChartedSpace H M] {x : M} {f : M → M} {f' : TangentSpace I x →L[𝕜] TangentSpace I x} (hf : HasMFDerivAt% f x f') (hx : f x = x) (n : ℕ) : HasMFDerivAt% f^[n] x (f' ^ n)

The chain rule for iterates at a fixed point. If f x = x and f has differential f' at x, an endomorphism of T_x M, then f^[n] has differential f' ^ n at x. This is the manifold version of HasFDerivAt.iterate.

theorem TauCeti.mfderiv_injective_of_leftInverse {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} {M : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [TopologicalSpace M] [ChartedSpace H M] {x : M} {E' : Type u_5} {H' : Type u_6} {N : Type u_7} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [TopologicalSpace H'] {J : ModelWithCorners 𝕜 E' H'} [TopologicalSpace N] [ChartedSpace H' N] {f : M → N} {g : N → M} (hg : MDiffAt g (f x)) (hf : MDiffAt f x) (hgf : Function.LeftInverse g f) : Function.Injective ⇑(mfderiv% f x)

A map f with a left inverse g has injective derivative at every point x where f is differentiable and g is differentiable at f x: by the chain rule, dg_(f x) is a left inverse of df_x.

theorem TauCeti.mfderiv_comp_const_add_smul_apply {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} {M : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (u : F → M) (c w : F) (ε : 𝕜) (v : F) : ((mfderiv% fun (w : F) => u (c + ε • w)) w) v = ε • (mfderiv% u (c + ε • w)) v

The derivative of an affine reparametrization. For a map u from a normed space, the derivative of w ↦ u (c + ε • w) at w is ε times the derivative of u at c + ε • w. No differentiability is needed: for ε ≠ 0 the reparametrization is invertible, so both maps are differentiable or neither is, and for ε = 0 the reparametrized map is constant. This is the manifold version of fderiv_comp_smul and fderiv_comp_add_left.