Equivalence of manifold differentiability with the basic definition for functions between

vector spaces

The API in this file is mostly copied from Mathlib.Geometry.Manifold.ContMDiff.NormedSpace, providing the same statements for higher smoothness. In this file, we do the same for differentiability.

theorem DifferentiableWithinAt.comp_mdifferentiableWithinAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_8} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {F' : Type u_11} [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] {g : F → F'} {f : M → F} {s : Set M} {t : Set F} {x : M} (hg : DifferentiableWithinAt 𝕜 g t (f x)) (hf : MDifferentiableWithinAt I (modelWithCornersSelf 𝕜 F) f s x) (h : Set.MapsTo f s t) : MDifferentiableWithinAt I (modelWithCornersSelf 𝕜 F') (g ∘ f) s x

theorem DifferentiableAt.comp_mdifferentiableWithinAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_8} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {F' : Type u_11} [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] {g : F → F'} {f : M → F} {s : Set M} {x : M} (hg : DifferentiableAt 𝕜 g (f x)) (hf : MDifferentiableWithinAt I (modelWithCornersSelf 𝕜 F) f s x) : MDifferentiableWithinAt I (modelWithCornersSelf 𝕜 F') (g ∘ f) s x

theorem DifferentiableAt.comp_mdifferentiableAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_8} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {F' : Type u_11} [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] {g : F → F'} {f : M → F} {x : M} (hg : DifferentiableAt 𝕜 g (f x)) (hf : MDifferentiableAt I (modelWithCornersSelf 𝕜 F) f x) : MDifferentiableAt I (modelWithCornersSelf 𝕜 F') (g ∘ f) x

theorem Differentiable.comp_mdifferentiableWithinAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_8} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {F' : Type u_11} [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] {g : F → F'} {f : M → F} {s : Set M} {x : M} (hg : Differentiable 𝕜 g) (hf : MDifferentiableWithinAt I (modelWithCornersSelf 𝕜 F) f s x) : MDifferentiableWithinAt I (modelWithCornersSelf 𝕜 F') (g ∘ f) s x

theorem Differentiable.comp_mdifferentiableAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_8} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {F' : Type u_11} [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] {g : F → F'} {f : M → F} {x : M} (hg : Differentiable 𝕜 g) (hf : MDifferentiableAt I (modelWithCornersSelf 𝕜 F) f x) : MDifferentiableAt I (modelWithCornersSelf 𝕜 F') (g ∘ f) x

theorem Differentiable.comp_mdifferentiable {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_8} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {F' : Type u_11} [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] {g : F → F'} {f : M → F} (hg : Differentiable 𝕜 g) (hf : MDifferentiable I (modelWithCornersSelf 𝕜 F) f) : MDifferentiable I (modelWithCornersSelf 𝕜 F') (g ∘ f)

Linear maps between normed spaces are differentiable

theorem MDifferentiableWithinAt.clm_precomp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F₁ : Type u_14} [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] {F₂ : Type u_15} [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] {F₃ : Type u_16} [NormedAddCommGroup F₃] [NormedSpace 𝕜 F₃] {f : M → F₁ →L[𝕜] F₂} {s : Set M} {x : M} (hf : MDifferentiableWithinAt I (modelWithCornersSelf 𝕜 (F₁ →L[𝕜] F₂)) f s x) : MDifferentiableWithinAt I (modelWithCornersSelf 𝕜 ((F₂ →L[𝕜] F₃) →L[𝕜] F₁ →L[𝕜] F₃)) (fun (y : M) => ContinuousLinearMap.precomp F₃ (f y)) s x

theorem MDifferentiableAt.clm_precomp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F₁ : Type u_14} [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] {F₂ : Type u_15} [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] {F₃ : Type u_16} [NormedAddCommGroup F₃] [NormedSpace 𝕜 F₃] {f : M → F₁ →L[𝕜] F₂} {x : M} (hf : MDifferentiableAt I (modelWithCornersSelf 𝕜 (F₁ →L[𝕜] F₂)) f x) : MDifferentiableAt I (modelWithCornersSelf 𝕜 ((F₂ →L[𝕜] F₃) →L[𝕜] F₁ →L[𝕜] F₃)) (fun (y : M) => ContinuousLinearMap.precomp F₃ (f y)) x

theorem MDifferentiableOn.clm_precomp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F₁ : Type u_14} [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] {F₂ : Type u_15} [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] {F₃ : Type u_16} [NormedAddCommGroup F₃] [NormedSpace 𝕜 F₃] {f : M → F₁ →L[𝕜] F₂} {s : Set M} (hf : MDifferentiableOn I (modelWithCornersSelf 𝕜 (F₁ →L[𝕜] F₂)) f s) : MDifferentiableOn I (modelWithCornersSelf 𝕜 ((F₂ →L[𝕜] F₃) →L[𝕜] F₁ →L[𝕜] F₃)) (fun (y : M) => ContinuousLinearMap.precomp F₃ (f y)) s

theorem MDifferentiable.clm_precomp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F₁ : Type u_14} [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] {F₂ : Type u_15} [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] {F₃ : Type u_16} [NormedAddCommGroup F₃] [NormedSpace 𝕜 F₃] {f : M → F₁ →L[𝕜] F₂} (hf : MDifferentiable I (modelWithCornersSelf 𝕜 (F₁ →L[𝕜] F₂)) f) : MDifferentiable I (modelWithCornersSelf 𝕜 ((F₂ →L[𝕜] F₃) →L[𝕜] F₁ →L[𝕜] F₃)) fun (y : M) => ContinuousLinearMap.precomp F₃ (f y)

theorem MDifferentiableWithinAt.clm_postcomp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F₁ : Type u_14} [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] {F₂ : Type u_15} [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] {F₃ : Type u_16} [NormedAddCommGroup F₃] [NormedSpace 𝕜 F₃] {f : M → F₂ →L[𝕜] F₃} {s : Set M} {x : M} (hf : MDifferentiableWithinAt I (modelWithCornersSelf 𝕜 (F₂ →L[𝕜] F₃)) f s x) : MDifferentiableWithinAt I (modelWithCornersSelf 𝕜 ((F₁ →L[𝕜] F₂) →L[𝕜] F₁ →L[𝕜] F₃)) (fun (y : M) => ContinuousLinearMap.postcomp F₁ (f y)) s x

theorem MDifferentiableAt.clm_postcomp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F₁ : Type u_14} [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] {F₂ : Type u_15} [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] {F₃ : Type u_16} [NormedAddCommGroup F₃] [NormedSpace 𝕜 F₃] {f : M → F₂ →L[𝕜] F₃} {x : M} (hf : MDifferentiableAt I (modelWithCornersSelf 𝕜 (F₂ →L[𝕜] F₃)) f x) : MDifferentiableAt I (modelWithCornersSelf 𝕜 ((F₁ →L[𝕜] F₂) →L[𝕜] F₁ →L[𝕜] F₃)) (fun (y : M) => ContinuousLinearMap.postcomp F₁ (f y)) x

theorem MDifferentiableOn.clm_postcomp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F₁ : Type u_14} [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] {F₂ : Type u_15} [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] {F₃ : Type u_16} [NormedAddCommGroup F₃] [NormedSpace 𝕜 F₃] {f : M → F₂ →L[𝕜] F₃} {s : Set M} (hf : MDifferentiableOn I (modelWithCornersSelf 𝕜 (F₂ →L[𝕜] F₃)) f s) : MDifferentiableOn I (modelWithCornersSelf 𝕜 ((F₁ →L[𝕜] F₂) →L[𝕜] F₁ →L[𝕜] F₃)) (fun (y : M) => ContinuousLinearMap.postcomp F₁ (f y)) s

theorem MDifferentiable.clm_postcomp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F₁ : Type u_14} [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] {F₂ : Type u_15} [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] {F₃ : Type u_16} [NormedAddCommGroup F₃] [NormedSpace 𝕜 F₃] {f : M → F₂ →L[𝕜] F₃} (hf : MDifferentiable I (modelWithCornersSelf 𝕜 (F₂ →L[𝕜] F₃)) f) : MDifferentiable I (modelWithCornersSelf 𝕜 ((F₁ →L[𝕜] F₂) →L[𝕜] F₁ →L[𝕜] F₃)) fun (y : M) => ContinuousLinearMap.postcomp F₁ (f y)

theorem MDifferentiableWithinAt.clm_comp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F₁ : Type u_14} [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] {F₂ : Type u_15} [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] {F₃ : Type u_16} [NormedAddCommGroup F₃] [NormedSpace 𝕜 F₃] {g : M → F₁ →L[𝕜] F₃} {f : M → F₂ →L[𝕜] F₁} {s : Set M} {x : M} (hg : MDifferentiableWithinAt I (modelWithCornersSelf 𝕜 (F₁ →L[𝕜] F₃)) g s x) (hf : MDifferentiableWithinAt I (modelWithCornersSelf 𝕜 (F₂ →L[𝕜] F₁)) f s x) : MDifferentiableWithinAt I (modelWithCornersSelf 𝕜 (F₂ →L[𝕜] F₃)) (fun (x : M) => (g x).comp (f x)) s x

theorem MDifferentiableAt.clm_comp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F₁ : Type u_14} [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] {F₂ : Type u_15} [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] {F₃ : Type u_16} [NormedAddCommGroup F₃] [NormedSpace 𝕜 F₃] {g : M → F₁ →L[𝕜] F₃} {f : M → F₂ →L[𝕜] F₁} {x : M} (hg : MDifferentiableAt I (modelWithCornersSelf 𝕜 (F₁ →L[𝕜] F₃)) g x) (hf : MDifferentiableAt I (modelWithCornersSelf 𝕜 (F₂ →L[𝕜] F₁)) f x) : MDifferentiableAt I (modelWithCornersSelf 𝕜 (F₂ →L[𝕜] F₃)) (fun (x : M) => (g x).comp (f x)) x

theorem MDifferentiableOn.clm_comp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F₁ : Type u_14} [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] {F₂ : Type u_15} [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] {F₃ : Type u_16} [NormedAddCommGroup F₃] [NormedSpace 𝕜 F₃] {g : M → F₁ →L[𝕜] F₃} {f : M → F₂ →L[𝕜] F₁} {s : Set M} (hg : MDifferentiableOn I (modelWithCornersSelf 𝕜 (F₁ →L[𝕜] F₃)) g s) (hf : MDifferentiableOn I (modelWithCornersSelf 𝕜 (F₂ →L[𝕜] F₁)) f s) : MDifferentiableOn I (modelWithCornersSelf 𝕜 (F₂ →L[𝕜] F₃)) (fun (x : M) => (g x).comp (f x)) s

theorem MDifferentiable.clm_comp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F₁ : Type u_14} [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] {F₂ : Type u_15} [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] {F₃ : Type u_16} [NormedAddCommGroup F₃] [NormedSpace 𝕜 F₃] {g : M → F₁ →L[𝕜] F₃} {f : M → F₂ →L[𝕜] F₁} (hg : MDifferentiable I (modelWithCornersSelf 𝕜 (F₁ →L[𝕜] F₃)) g) (hf : MDifferentiable I (modelWithCornersSelf 𝕜 (F₂ →L[𝕜] F₁)) f) : MDifferentiable I (modelWithCornersSelf 𝕜 (F₂ →L[𝕜] F₃)) fun (x : M) => (g x).comp (f x)

theorem MDifferentiableWithinAt.clm_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F₁ : Type u_14} [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] {F₂ : Type u_15} [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] {g : M → F₁ →L[𝕜] F₂} {f : M → F₁} {s : Set M} {x : M} (hg : MDifferentiableWithinAt I (modelWithCornersSelf 𝕜 (F₁ →L[𝕜] F₂)) g s x) (hf : MDifferentiableWithinAt I (modelWithCornersSelf 𝕜 F₁) f s x) : MDifferentiableWithinAt I (modelWithCornersSelf 𝕜 F₂) (fun (x : M) => (g x) (f x)) s x

Applying a linear map to a vector is differentiable within a set. Version in vector spaces. For a version in nontrivial vector bundles, see MDifferentiableWithinAt.clm_apply_of_inCoordinates.

theorem MDifferentiableAt.clm_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F₁ : Type u_14} [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] {F₂ : Type u_15} [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] {g : M → F₁ →L[𝕜] F₂} {f : M → F₁} {x : M} (hg : MDifferentiableAt I (modelWithCornersSelf 𝕜 (F₁ →L[𝕜] F₂)) g x) (hf : MDifferentiableAt I (modelWithCornersSelf 𝕜 F₁) f x) : MDifferentiableAt I (modelWithCornersSelf 𝕜 F₂) (fun (x : M) => (g x) (f x)) x

Applying a linear map to a vector is differentiable. Version in vector spaces. For a version in nontrivial vector bundles, see MDifferentiableAt.clm_apply_of_inCoordinates.

theorem MDifferentiableOn.clm_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F₁ : Type u_14} [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] {F₂ : Type u_15} [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] {g : M → F₁ →L[𝕜] F₂} {f : M → F₁} {s : Set M} (hg : MDifferentiableOn I (modelWithCornersSelf 𝕜 (F₁ →L[𝕜] F₂)) g s) (hf : MDifferentiableOn I (modelWithCornersSelf 𝕜 F₁) f s) : MDifferentiableOn I (modelWithCornersSelf 𝕜 F₂) (fun (x : M) => (g x) (f x)) s

theorem MDifferentiable.clm_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F₁ : Type u_14} [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] {F₂ : Type u_15} [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] {g : M → F₁ →L[𝕜] F₂} {f : M → F₁} (hg : MDifferentiable I (modelWithCornersSelf 𝕜 (F₁ →L[𝕜] F₂)) g) (hf : MDifferentiable I (modelWithCornersSelf 𝕜 F₁) f) : MDifferentiable I (modelWithCornersSelf 𝕜 F₂) fun (x : M) => (g x) (f x)

theorem MDifferentiableWithinAt.cle_arrowCongr {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F₁ : Type u_14} [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] {F₂ : Type u_15} [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] {F₃ : Type u_16} [NormedAddCommGroup F₃] [NormedSpace 𝕜 F₃] {F₄ : Type u_17} [NormedAddCommGroup F₄] [NormedSpace 𝕜 F₄] {f : M → F₁ ≃L[𝕜] F₂} {g : M → F₃ ≃L[𝕜] F₄} {s : Set M} {x : M} (hf : MDifferentiableWithinAt I (modelWithCornersSelf 𝕜 (F₂ →L[𝕜] F₁)) (fun (x : M) => ↑(f x).symm) s x) (hg : MDifferentiableWithinAt I (modelWithCornersSelf 𝕜 (F₃ →L[𝕜] F₄)) (fun (x : M) => ↑(g x)) s x) : MDifferentiableWithinAt I (modelWithCornersSelf 𝕜 ((F₁ →L[𝕜] F₃) →L[𝕜] F₂ →L[𝕜] F₄)) (fun (y : M) => ↑((f y).arrowCongr (g y))) s x

theorem MDifferentiableAt.cle_arrowCongr {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F₁ : Type u_14} [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] {F₂ : Type u_15} [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] {F₃ : Type u_16} [NormedAddCommGroup F₃] [NormedSpace 𝕜 F₃] {F₄ : Type u_17} [NormedAddCommGroup F₄] [NormedSpace 𝕜 F₄] {f : M → F₁ ≃L[𝕜] F₂} {g : M → F₃ ≃L[𝕜] F₄} {x : M} (hf : MDifferentiableAt I (modelWithCornersSelf 𝕜 (F₂ →L[𝕜] F₁)) (fun (x : M) => ↑(f x).symm) x) (hg : MDifferentiableAt I (modelWithCornersSelf 𝕜 (F₃ →L[𝕜] F₄)) (fun (x : M) => ↑(g x)) x) : MDifferentiableAt I (modelWithCornersSelf 𝕜 ((F₁ →L[𝕜] F₃) →L[𝕜] F₂ →L[𝕜] F₄)) (fun (y : M) => ↑((f y).arrowCongr (g y))) x

theorem MDifferentiableOn.cle_arrowCongr {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F₁ : Type u_14} [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] {F₂ : Type u_15} [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] {F₃ : Type u_16} [NormedAddCommGroup F₃] [NormedSpace 𝕜 F₃] {F₄ : Type u_17} [NormedAddCommGroup F₄] [NormedSpace 𝕜 F₄] {f : M → F₁ ≃L[𝕜] F₂} {g : M → F₃ ≃L[𝕜] F₄} {s : Set M} (hf : MDifferentiableOn I (modelWithCornersSelf 𝕜 (F₂ →L[𝕜] F₁)) (fun (x : M) => ↑(f x).symm) s) (hg : MDifferentiableOn I (modelWithCornersSelf 𝕜 (F₃ →L[𝕜] F₄)) (fun (x : M) => ↑(g x)) s) : MDifferentiableOn I (modelWithCornersSelf 𝕜 ((F₁ →L[𝕜] F₃) →L[𝕜] F₂ →L[𝕜] F₄)) (fun (y : M) => ↑((f y).arrowCongr (g y))) s

theorem MDifferentiable.cle_arrowCongr {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F₁ : Type u_14} [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] {F₂ : Type u_15} [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] {F₃ : Type u_16} [NormedAddCommGroup F₃] [NormedSpace 𝕜 F₃] {F₄ : Type u_17} [NormedAddCommGroup F₄] [NormedSpace 𝕜 F₄] {f : M → F₁ ≃L[𝕜] F₂} {g : M → F₃ ≃L[𝕜] F₄} (hf : MDifferentiable I (modelWithCornersSelf 𝕜 (F₂ →L[𝕜] F₁)) fun (x : M) => ↑(f x).symm) (hg : MDifferentiable I (modelWithCornersSelf 𝕜 (F₃ →L[𝕜] F₄)) fun (x : M) => ↑(g x)) : MDifferentiable I (modelWithCornersSelf 𝕜 ((F₁ →L[𝕜] F₃) →L[𝕜] F₂ →L[𝕜] F₄)) fun (y : M) => ↑((f y).arrowCongr (g y))

theorem MDifferentiableWithinAt.clm_prodMap {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F₁ : Type u_14} [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] {F₂ : Type u_15} [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] {F₃ : Type u_16} [NormedAddCommGroup F₃] [NormedSpace 𝕜 F₃] {F₄ : Type u_17} [NormedAddCommGroup F₄] [NormedSpace 𝕜 F₄] {g : M → F₁ →L[𝕜] F₃} {f : M → F₂ →L[𝕜] F₄} {s : Set M} {x : M} (hg : MDifferentiableWithinAt I (modelWithCornersSelf 𝕜 (F₁ →L[𝕜] F₃)) g s x) (hf : MDifferentiableWithinAt I (modelWithCornersSelf 𝕜 (F₂ →L[𝕜] F₄)) f s x) : MDifferentiableWithinAt I (modelWithCornersSelf 𝕜 (F₁ × F₂ →L[𝕜] F₃ × F₄)) (fun (x : M) => (g x).prodMap (f x)) s x

theorem MDifferentiableAt.clm_prodMap {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F₁ : Type u_14} [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] {F₂ : Type u_15} [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] {F₃ : Type u_16} [NormedAddCommGroup F₃] [NormedSpace 𝕜 F₃] {F₄ : Type u_17} [NormedAddCommGroup F₄] [NormedSpace 𝕜 F₄] {g : M → F₁ →L[𝕜] F₃} {f : M → F₂ →L[𝕜] F₄} {x : M} (hg : MDifferentiableAt I (modelWithCornersSelf 𝕜 (F₁ →L[𝕜] F₃)) g x) (hf : MDifferentiableAt I (modelWithCornersSelf 𝕜 (F₂ →L[𝕜] F₄)) f x) : MDifferentiableAt I (modelWithCornersSelf 𝕜 (F₁ × F₂ →L[𝕜] F₃ × F₄)) (fun (x : M) => (g x).prodMap (f x)) x

theorem MDifferentiableOn.clm_prodMap {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F₁ : Type u_14} [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] {F₂ : Type u_15} [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] {F₃ : Type u_16} [NormedAddCommGroup F₃] [NormedSpace 𝕜 F₃] {F₄ : Type u_17} [NormedAddCommGroup F₄] [NormedSpace 𝕜 F₄] {g : M → F₁ →L[𝕜] F₃} {f : M → F₂ →L[𝕜] F₄} {s : Set M} (hg : MDifferentiableOn I (modelWithCornersSelf 𝕜 (F₁ →L[𝕜] F₃)) g s) (hf : MDifferentiableOn I (modelWithCornersSelf 𝕜 (F₂ →L[𝕜] F₄)) f s) : MDifferentiableOn I (modelWithCornersSelf 𝕜 (F₁ × F₂ →L[𝕜] F₃ × F₄)) (fun (x : M) => (g x).prodMap (f x)) s

theorem MDifferentiable.clm_prodMap {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F₁ : Type u_14} [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] {F₂ : Type u_15} [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] {F₃ : Type u_16} [NormedAddCommGroup F₃] [NormedSpace 𝕜 F₃] {F₄ : Type u_17} [NormedAddCommGroup F₄] [NormedSpace 𝕜 F₄] {g : M → F₁ →L[𝕜] F₃} {f : M → F₂ →L[𝕜] F₄} (hg : MDifferentiable I (modelWithCornersSelf 𝕜 (F₁ →L[𝕜] F₃)) g) (hf : MDifferentiable I (modelWithCornersSelf 𝕜 (F₂ →L[𝕜] F₄)) f) : MDifferentiable I (modelWithCornersSelf 𝕜 (F₁ × F₂ →L[𝕜] F₃ × F₄)) fun (x : M) => (g x).prodMap (f x)

Differentiability of scalar multiplication

theorem MDifferentiableWithinAt.smul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {s : Set M} {x : M} {V : Type u_18} [NormedAddCommGroup V] [NormedSpace 𝕜 V] {f : M → 𝕜} {g : M → V} (hf : MDifferentiableWithinAt I (modelWithCornersSelf 𝕜 𝕜) f s x) (hg : MDifferentiableWithinAt I (modelWithCornersSelf 𝕜 V) g s x) : MDifferentiableWithinAt I (modelWithCornersSelf 𝕜 V) (fun (p : M) => f p • g p) s x

theorem MDifferentiableAt.smul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {x : M} {V : Type u_18} [NormedAddCommGroup V] [NormedSpace 𝕜 V] {f : M → 𝕜} {g : M → V} (hf : MDifferentiableAt I (modelWithCornersSelf 𝕜 𝕜) f x) (hg : MDifferentiableAt I (modelWithCornersSelf 𝕜 V) g x) : MDifferentiableAt I (modelWithCornersSelf 𝕜 V) (fun (p : M) => f p • g p) x

theorem MDifferentiableOn.smul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {s : Set M} {V : Type u_18} [NormedAddCommGroup V] [NormedSpace 𝕜 V] {f : M → 𝕜} {g : M → V} (hf : MDifferentiableOn I (modelWithCornersSelf 𝕜 𝕜) f s) (hg : MDifferentiableOn I (modelWithCornersSelf 𝕜 V) g s) : MDifferentiableOn I (modelWithCornersSelf 𝕜 V) (fun (p : M) => f p • g p) s

theorem MDifferentiable.smul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {V : Type u_18} [NormedAddCommGroup V] [NormedSpace 𝕜 V] {f : M → 𝕜} {g : M → V} (hf : MDifferentiable I (modelWithCornersSelf 𝕜 𝕜) f) (hg : MDifferentiable I (modelWithCornersSelf 𝕜 V) g) : MDifferentiable I (modelWithCornersSelf 𝕜 V) fun (p : M) => f p • g p