# Documentation

Mathlib.Geometry.Manifold.ContMDiffMFDeriv

### Interactions between differentiability, smoothness and manifold derivatives #

We give the relation between MDifferentiable, ContMDiff, mfderiv, tangentMap and related notions.

## Main statements #

• ContMDiffOn.contMDiffOn_tangentMapWithin states that the bundled derivative of a Cⁿ function in a domain is Cᵐ when m + 1 ≤ n.
• ContMDiff.contMDiff_tangentMap states that the bundled derivative of a Cⁿ function is Cᵐ when m + 1 ≤ n.

### The derivative of a smooth function is smooth #

theorem ContMDiffAt.mfderiv {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] [Is : ] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] [I's : ] {F : Type u_8} [] {G : Type u_9} [] {J : } {N : Type u_10} [] [] [Js : ] {m : ℕ∞} {n : ℕ∞} {x₀ : N} (f : NMM') (g : NM) (hf : ContMDiffAt () I' n () (x₀, g x₀)) (hg : ContMDiffAt J I m g x₀) (hmn : m + 1 n) :
ContMDiffAt J (modelWithCornersSelf 𝕜 (E →L[𝕜] E')) m (inTangentCoordinates I I' g (fun x => f x (g x)) (fun x => mfderiv I I' (f x) (g x)) x₀) x₀

The function that sends x to the y-derivative of f(x,y) at g(x) is C^m at x₀, where the derivative is taken as a continuous linear map. We have to assume that f is C^n at (x₀, g(x₀)) for n ≥ m + 1 and g is C^m at x₀. We have to insert a coordinate change from x₀ to x to make the derivative sensible. This result is used to show that maps into the 1-jet bundle and cotangent bundle are smooth. ContMDiffAt.mfderiv_const is a special case of this.

This result should be generalized to a ContMDiffWithinAt for mfderivWithin. If we do that, we can deduce ContMDiffOn.contMDiffOn_tangentMapWithin from this.

theorem ContMDiffAt.mfderiv_const {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] [Is : ] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] [I's : ] {m : ℕ∞} {n : ℕ∞} {x₀ : M} {f : MM'} (hf : ContMDiffAt I I' n f x₀) (hmn : m + 1 n) :
ContMDiffAt I (modelWithCornersSelf 𝕜 (E →L[𝕜] E')) m (inTangentCoordinates I I' id f (mfderiv I I' f) x₀) x₀

The derivative D_yf(y) is C^m at x₀, where the derivative is taken as a continuous linear map. We have to assume that f is C^n at x₀ for some n ≥ m + 1. We have to insert a coordinate change from x₀ to x to make the derivative sensible. This is a special case of ContMDiffAt.mfderiv where f does not contain any parameters and g = id.

theorem ContMDiffAt.mfderiv_apply {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] [Is : ] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] [I's : ] {F : Type u_8} [] {G : Type u_9} [] {J : } {N : Type u_10} [] [] [Js : ] {F' : Type u_11} [] [NormedSpace 𝕜 F'] {G' : Type u_12} [] {J' : ModelWithCorners 𝕜 F' G'} {N' : Type u_13} [] [ChartedSpace G' N'] {m : ℕ∞} {n : ℕ∞} {x₀ : N'} (f : NMM') (g : NM) (g₁ : N'N) (g₂ : N'E) (hf : ContMDiffAt () I' n () (g₁ x₀, g (g₁ x₀))) (hg : ContMDiffAt J I m g (g₁ x₀)) (hg₁ : ContMDiffAt J' J m g₁ x₀) (hg₂ : ContMDiffAt J' () m g₂ x₀) (hmn : m + 1 n) :
ContMDiffAt J' () m (fun x => ↑(inTangentCoordinates I I' g (fun x => f x (g x)) (fun x => mfderiv I I' (f x) (g x)) (g₁ x₀) (g₁ x)) (g₂ x)) x₀

The function that sends x to the y-derivative of f(x,y) at g(x) applied to g₂(x) is C^n at x₀, where the derivative is taken as a continuous linear map. We have to assume that f is C^(n+1) at (x₀, g(x₀)) and g is C^n at x₀. We have to insert a coordinate change from x₀ to g₁(x) to make the derivative sensible.

This is similar to ContMDiffAt.mfderiv, but where the continuous linear map is applied to a (variable) vector.

### The tangent map of a smooth function is smooth #

theorem ContMDiffOn.continuousOn_tangentMapWithin_aux {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {n : ℕ∞} {f : HH'} {s : Set H} (hf : ContMDiffOn I I' n f s) (hn : 1 n) (hs : ) :
ContinuousOn (tangentMapWithin I I' f s) (Bundle.TotalSpace.proj ⁻¹' s)

If a function is C^n with 1 ≤ n on a domain with unique derivatives, then its bundled derivative is continuous. In this auxiliary lemma, we prove this fact when the source and target space are model spaces in models with corners. The general fact is proved in ContMDiffOn.continuousOn_tangentMapWithin

theorem ContMDiffOn.contMDiffOn_tangentMapWithin_aux {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {m : ℕ∞} {n : ℕ∞} {f : HH'} {s : Set H} (hf : ContMDiffOn I I' n f s) (hmn : m + 1 n) (hs : ) :
ContMDiffOn () () m (tangentMapWithin I I' f s) (Bundle.TotalSpace.proj ⁻¹' s)

If a function is C^n on a domain with unique derivatives, then its bundled derivative is C^m when m+1 ≤ n. In this auxiliary lemma, we prove this fact when the source and target space are model spaces in models with corners. The general fact is proved in ContMDiffOn.contMDiffOn_tangentMapWithin

theorem ContMDiffOn.contMDiffOn_tangentMapWithin {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] [Is : ] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] [I's : ] {f : MM'} {s : Set M} {m : ℕ∞} {n : ℕ∞} (hf : ContMDiffOn I I' n f s) (hmn : m + 1 n) (hs : ) :
ContMDiffOn () () m (tangentMapWithin I I' f s) (Bundle.TotalSpace.proj ⁻¹' s)

If a function is C^n on a domain with unique derivatives, then its bundled derivative is C^m when m+1 ≤ n.

theorem ContMDiffOn.continuousOn_tangentMapWithin {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] [Is : ] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] [I's : ] {f : MM'} {s : Set M} {n : ℕ∞} (hf : ContMDiffOn I I' n f s) (hmn : 1 n) (hs : ) :
ContinuousOn (tangentMapWithin I I' f s) (Bundle.TotalSpace.proj ⁻¹' s)

If a function is C^n on a domain with unique derivatives, with 1 ≤ n, then its bundled derivative is continuous there.

theorem ContMDiff.contMDiff_tangentMap {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] [Is : ] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] [I's : ] {f : MM'} {m : ℕ∞} {n : ℕ∞} (hf : ContMDiff I I' n f) (hmn : m + 1 n) :
ContMDiff () () m (tangentMap I I' f)

If a function is C^n, then its bundled derivative is C^m when m+1 ≤ n.

theorem ContMDiff.continuous_tangentMap {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] [Is : ] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] [I's : ] {f : MM'} {n : ℕ∞} (hf : ContMDiff I I' n f) (hmn : 1 n) :

If a function is C^n, with 1 ≤ n, then its bundled derivative is continuous.

theorem TangentBundle.tangentMap_tangentBundle_pure {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] (I : ) (M : Type u_4) [] [] [Is : ] (p : ) :
tangentMap I () () p = { proj := { proj := p.proj, snd := 0 }, snd := (p.snd, 0) }

The derivative of the zero section of the tangent bundle maps ⟨x, v⟩ to ⟨⟨x, 0⟩, ⟨v, 0⟩⟩.

Note that, as currently framed, this is a statement in coordinates, thus reliant on the choice of the coordinate system we use on the tangent bundle.

However, the result itself is coordinate-dependent only to the extent that the coordinates determine a splitting of the tangent bundle. Moreover, there is a canonical splitting at each point of the zero section (since there is a canonical horizontal space there, the tangent space to the zero section, in addition to the canonical vertical space which is the kernel of the derivative of the projection), and this canonical splitting is also the one that comes from the coordinates on the tangent bundle in our definitions. So this statement is not as crazy as it may seem.

TODO define splittings of vector bundles; state this result invariantly.

theorem ContMDiffMap.mdifferentiable' {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {n : ℕ∞} (f : ContMDiffMap I I' M M' n) (hn : 1 n) :
MDifferentiable I I' f
theorem ContMDiffMap.mdifferentiable {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] (f : ContMDiffMap I I' M M' ) :
MDifferentiable I I' f
theorem ContMDiffMap.mdifferentiableAt {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] (f : ContMDiffMap I I' M M' ) {x : M} :
MDifferentiableAt I I' (f) x