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.lean, 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 : MDiffAt[s] f x) (h : Set.MapsTo f s t) : MDiffAt[s] (g ∘ f) 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 : MDiffAt[s] f x) : MDiffAt[s] (g ∘ f) 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 : MDiffAt f x) : MDiffAt (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 : MDiffAt[s] f x) : MDiffAt[s] (g ∘ f) 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 : MDiffAt f x) : MDiffAt (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)

theorem MDifferentiableWithinAt.differentiableWithinAt_comp_extChartAt_symm {𝕜 : 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} {F : Type u_18} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : M → F} (hf : MDiffAt[s] f x) : DifferentiableWithinAt 𝕜 (f ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x).symm ⁻¹' s ∩ Set.range ↑I) (↑(extChartAt I x) x)

theorem DifferentiableWithinAt.mdifferentiableWithinAt_of_comp_extChartAt_symm {𝕜 : 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} {F : Type u_18} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : M → F} [IsManifold I 1 M] (hf : DifferentiableWithinAt 𝕜 (f ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x).symm ⁻¹' s ∩ Set.range ↑I) (↑(extChartAt I x) x)) : MDiffAt[s] f x

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 : MDiffAt[s] f x) : (MDiffAt[s] fun (y : M) => ContinuousLinearMap.precomp F₃ (f y)) 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 : MDiffAt f x) : (MDiffAt 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 : MDiffAt[s] f x) : (MDiffAt[s] fun (y : M) => ContinuousLinearMap.postcomp F₁ (f y)) 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 : MDiffAt f x) : (MDiffAt 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 : MDiffAt[s] g x) (hf : MDiffAt[s] f x) : (MDiffAt[s] fun (x : M) => (g x).comp (f x)) 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 : MDiffAt g x) (hf : MDiffAt f x) : (MDiffAt 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 : MDiffAt[s] g x) (hf : MDiffAt[s] f x) : (MDiffAt[s] fun (x : M) => (g x) (f x)) 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 : MDiffAt g x) (hf : MDiffAt f x) : (MDiffAt 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 : (MDiffAt[s] fun (x : M) => ↑(f x).symm) x) (hg : (MDiffAt[s] fun (x : M) => ↑(g x)) x) : (MDiffAt[s] fun (y : M) => ↑((f y).arrowCongr (g y))) 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 : (MDiffAt fun (x : M) => ↑(f x).symm) x) (hg : (MDiffAt fun (x : M) => ↑(g x)) x) : (MDiffAt 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 : MDiffAt[s] g x) (hf : MDiffAt[s] f x) : (MDiffAt[s] fun (x : M) => (g x).prodMap (f x)) 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 : MDiffAt g x) (hf : MDiffAt f x) : (MDiffAt 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 : MDiffAt[s] f x) (hg : MDiffAt[s] g x) : (MDiffAt[s] fun (p : M) => f p • g p) 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 : MDiffAt f x) (hg : MDiffAt g x) : (MDiffAt 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