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 : 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