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
HasMFDerivAt.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}
{f' : TangentSpace I x โL[๐] ๐}
(hs : HasMFDerivAt I (modelWithCornersSelf ๐ ๐) f x ((โ(NormedSpace.fromTangentSpace (f x)).symm).comp f'))
{g' : TangentSpace I x โL[๐] V}
(hg : HasMFDerivAt I (modelWithCornersSelf ๐ V) g x ((โ(NormedSpace.fromTangentSpace (g x)).symm).comp g'))
:
HasMFDerivAt I (modelWithCornersSelf ๐ V) (f โข g) x
(f x โข (โ(NormedSpace.fromTangentSpace ((f โข g) x)).symm).comp g' + (ContinuousLinearMap.toSpanSingleton ๐ ((NormedSpace.fromTangentSpace ((f โข g) x)).symm (g x))).comp f')
Given maps f, g from a manifold into a field ๐ and ๐-vector space V, respectively, if
at some point x, f has differential f' : TangentSpace I x โL[๐] ๐ and g has differential
g' : TangentSpace I x โL[๐] V (both phrased using the predicate HasMFDerivAt), it follows that
their scalar multiplication f โข g has differential f x โข g' + toSpanSingleton ๐ (g x) โL f'.
In fact, the statement above is not literally true, because, for example, the differential of g
really takes values in the tangent space to V at g x, rather than in V itself. Of course, this
tangent space can be canonically identified with V.
This lemma phrases the formula using the equiv NormedSpace.fromTangentSpace, which provides this
canonical identification. (It would also be possible to phrase the formula without this equiv,
instead using casting and definitional abuse.)
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
theorem
mfderiv_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)
:
mfderiv% (f โข g) x = f x โข (โ(NormedSpace.fromTangentSpace ((f โข g) x)).symm).comp
((โ(NormedSpace.fromTangentSpace (g x))).comp (mfderiv% g x)) + (ContinuousLinearMap.toSpanSingleton ๐ ((NormedSpace.fromTangentSpace ((f โข g) x)).symm (g x))).comp
((โ(NormedSpace.fromTangentSpace (f x))).comp (mfderiv% f x))
Given maps f, g from a manifold into a field ๐ and ๐-vector space V, respectively, the
formula for the mfderiv (differential) of their scalar multiplication f โข g.
Mathematically speaking the formula is d(f โข g) = f โข dg + df โ g, i.e.
mfderiv% (f โข g) x = f x โข mfderiv% g x + toSpanSingleton ๐ (g x) โL mfderiv% f x,
but this doesn't typecheck because mfderiv% (f โข g) x and mfderiv% g x take values in different
tangent spaces -- respectively the tangent spaces to V at (f โข g) x and g x. Of course, both
these tangent spaces can be canonically identified with V.
This lemma phrases the formula using the equiv NormedSpace.fromTangentSpace, which provides this
canonical identification. (It would also be possible to phrase the formula without this equiv,
instead using casting and definitional abuse.)
It is good practice to use the equiv NormedSpace.fromTangentSpace throughout a computation. If
this is done, typically mfderiv% (f โข g) x will only turn up paired with this equiv (i.e., in an
expression (fromTangentSpace _) โL mfderiv% (f โข g) x), and the more convenient lemma
fromTangentSpace_mfderiv_smul (see below) can be used instead.
theorem
fromTangentSpace_mfderiv_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)
:
(โ(NormedSpace.fromTangentSpace ((f โข g) x))).comp (mfderiv% (f โข g) x) = f x โข (โ(NormedSpace.fromTangentSpace (g x))).comp (mfderiv% g x) + (ContinuousLinearMap.toSpanSingleton ๐ (g x)).comp ((โ(NormedSpace.fromTangentSpace (f x))).comp (mfderiv% f x))
Given maps f, g from a manifold into a field ๐ and ๐-vector space V, respectively, the
formula for the mfderiv (differential) of their scalar multiplication f โข g.
Mathematically speaking the formula is d(f โข g) = f โข dg + df โ g, i.e.
mfderiv% (f โข g) x = f x โข mfderiv% g x + toSpanSingleton ๐ (g x) โL mfderiv% f x,
but this doesn't typecheck because mfderiv% (f โข g) x and mfderiv% g x take values in different
tangent spaces -- respectively the tangent spaces to V at (f โข g) x and g x. Of course, both
these tangent spaces can be canonically identified with V.
This lemma phrases the formula using the equiv NormedSpace.fromTangentSpace, which provides this
canonical identification. (It would also be possible to phrase the formula without this equiv,
instead using casting and definitional abuse.)
theorem
fromTangentSpace_mfderiv_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)
:
(โ(NormedSpace.fromTangentSpace (f x โข g x))).comp (mfderiv% (f โข g) x) = f x โข (โ(NormedSpace.fromTangentSpace (g x))).comp (mfderiv% g x) + (ContinuousLinearMap.toSpanSingleton ๐ (g x)).comp ((โ(NormedSpace.fromTangentSpace (f x))).comp (mfderiv% f x))
Given maps f, g from a manifold into a field ๐ and ๐-vector space V, respectively, the
formula for the mfderiv (differential) of their scalar multiplication f โข g.
Mathematically speaking the formula is d(f โข g) = f โข dg + df โ g, but to get it to typecheck
we need a phrasing involving the canonical identification NormedSpace.fromTangentSpace between
the vector space V and the tangent space to this vector space at any point. This is because two
different tangent spaces (at (f โข g) x and g x) appear in the equation.
This is a defeq variant of the main lemma fromTangentSpace_mfderiv_smul, in which we work in the
tangent space at f x โข g x (the simp-normal form) rather than at (f โข g) x.
theorem
fromTangentSpace_mfderiv_smul_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]
{x : M}
{V : Type u_18}
[NormedAddCommGroup V]
[NormedSpace ๐ V]
{f : M โ ๐}
{g : M โ V}
(hf : MDiffAt f x)
(hg : MDiffAt g x)
(v : TangentSpace I x)
:
(NormedSpace.fromTangentSpace ((f โข g) x)) ((mfderiv% (f โข g) x) v) = f x โข (NormedSpace.fromTangentSpace (g x)) ((mfderiv% g x) v) + (NormedSpace.fromTangentSpace (f x)) ((mfderiv% f x) v) โข g x
Given maps f, g from a manifold into a field ๐ and ๐-vector space V, respectively, the
formula for the mfderiv (differential) of their scalar multiplication f โข g in the direction of
the tangent vector v.
Mathematically speaking the formula is d(f โข g)(v) = f โข dg(v) + df(v) โข g, but to get it to
typecheck we need a phrasing involving the canonical identification NormedSpace.fromTangentSpace
between the vector space V and the tangent space to this vector space at any point. This is
because two different tangent spaces (at (f โข g) x and g x) appear in the equation.
theorem
fromTangentSpace_mfderiv_smul_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]
{x : M}
{V : Type u_18}
[NormedAddCommGroup V]
[NormedSpace ๐ V]
{f : M โ ๐}
{g : M โ V}
(hf : MDiffAt f x)
(hg : MDiffAt g x)
(v : TangentSpace I x)
:
(NormedSpace.fromTangentSpace (f x โข g x)) ((mfderiv% (f โข g) x) v) = f x โข (NormedSpace.fromTangentSpace (g x)) ((mfderiv% g x) v) + (NormedSpace.fromTangentSpace (f x)) ((mfderiv% f x) v) โข g x
Given maps f, g from a manifold into a field ๐ and ๐-vector space V, respectively, the
formula for the mfderiv (differential) of their scalar multiplication f โข g in the direction of
the tangent vector v.
Mathematically speaking the formula is d(f โข g)(v) = f โข dg(v) + df(v) โข g, but to get it to
typecheck we need a phrasing involving the canonical identification NormedSpace.fromTangentSpace
between the vector space V and the tangent space to this vector space at any point. This is
because two different tangent spaces (at (f โข g) x and g x) appear in the equation.
This is a defeq variant of the main lemma fromTangentSpace_mfderiv_smul_apply, in which we work in
the tangent space at f x โข g x (the simp-normal form) rather than at (f โข g) x.