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.
In addition to the above, this file provides
- results about the differentiability of scalar multiplication (
mfderiv_smuland friends), and mvfderiv: the exterior derivative of a vector-valued function, as a section of the cotangent bundle; adds notationd% fformvfderiv I fvia a custom elaborator scoped to theManifoldnamespace, with a corresponding delaborator, and adds basic lemmas aboutmvfderiv(such as addition, subtraction, multiplication and constants).
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 : MDiff f)
:
MDiff (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 : MDiff[s] f)
:
MDiff[s] fun (y : M) => ContinuousLinearMap.precomp Fβ (f y)
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 : MDiff f)
:
MDiff 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 : MDiff[s] f)
:
MDiff[s] fun (y : M) => ContinuousLinearMap.postcomp Fβ (f y)
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 : MDiff f)
:
MDiff 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 βSL 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 βSL 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 : MDiff[s] g)
(hf : MDiff[s] f)
:
MDiff[s] fun (x : M) => g x βSL f x
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 : MDiff g)
(hf : MDiff f)
:
MDiff fun (x : M) => g x βSL 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 : MDiff[s] g)
(hf : MDiff[s] f)
:
MDiff[s] fun (x : M) => (g x) (f x)
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 : MDiff g)
(hf : MDiff f)
:
MDiff 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 : MDiff[s] fun (x : M) => β(f x).symm)
(hg : MDiff[s] fun (x : M) => β(g x))
:
MDiff[s] fun (y : M) => β((f y).arrowCongr (g y))
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 : MDiff fun (x : M) => β(f x).symm)
(hg : MDiff fun (x : M) => β(g x))
:
MDiff 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 : MDiff[s] g)
(hf : MDiff[s] f)
:
MDiff[s] fun (x : M) => (g x).prodMap (f x)
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 : MDiff g)
(hf : MDiff f)
:
MDiff 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 βSL f'))
{g' : TangentSpace I x βL[π] V}
(hg : HasMFDerivAt I (modelWithCornersSelf π V) g x (β(NormedSpace.fromTangentSpace (g x)).symm βSL g'))
:
HasMFDerivAt I (modelWithCornersSelf π V) (f β’ g) x
(f x β’ β(NormedSpace.fromTangentSpace ((f β’ g) x)).symm βSL g' + ContinuousLinearMap.toSpanSingleton π ((NormedSpace.fromTangentSpace ((f β’ g) x)).symm (g x)) βSL 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 : MDiff[s] f)
(hg : MDiff[s] g)
:
MDiff[s] fun (p : M) => f p β’ g p
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 : MDiff f)
(hg : MDiff g)
:
MDiff 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 βSL β(NormedSpace.fromTangentSpace (g x)) βSL mfderiv% g x + ContinuousLinearMap.toSpanSingleton π ((NormedSpace.fromTangentSpace ((f β’ g) x)).symm (g x)) βSL β(NormedSpace.fromTangentSpace (f x)) βSL 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)) βSL mfderiv% (f β’ g) x = f x β’ β(NormedSpace.fromTangentSpace (g x)) βSL mfderiv% g x + ContinuousLinearMap.toSpanSingleton π (g x) βSL β(NormedSpace.fromTangentSpace (f x)) βSL 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)) βSL mfderiv% (f β’ g) x = f x β’ β(NormedSpace.fromTangentSpace (g x)) βSL mfderiv% g x + ContinuousLinearMap.toSpanSingleton π (g x) βSL β(NormedSpace.fromTangentSpace (f x)) βSL 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.
Exterior derivative of a vector-valued function #
noncomputable def
mvfderiv
{π : 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]
(g : M β F)
(x : M)
:
The exterior derivative of a vector-valued function on M,
as a section of the cotangent bundle.
Future: this could be generalised to functions into additive torsors over abelian Lie groups.
Equations
- d% g x = β(NormedSpace.fromTangentSpace (g x)) βSL mfderiv% g x
Instances For
@[deprecated mvfderiv (since := "2026-05-17")]
def
extDerivFun
{π : 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]
(g : M β F)
(x : M)
:
Alias of mvfderiv.
The exterior derivative of a vector-valued function on M,
as a section of the cotangent bundle.
Future: this could be generalised to functions into additive torsors over abelian Lie groups.
Equations
Instances For
Delaborator for mvfderiv.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
mvfderiv_const
{π : 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]
(c : F)
{x : M}
:
@[simp]
theorem
mvfderiv_add
{π : 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]
{g g' : M β F}
{x : M}
(hg : MDiffAt g x)
(hg' : MDiffAt g' x)
:
theorem
mvfderiv_fun_add
{π : 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]
{g g' : M β F}
{x : M}
(hg : MDiffAt g x)
(hg' : MDiffAt g' x)
:
Eta-expanded form of mvfderiv_add
@[deprecated mvfderiv_add (since := "2026-05-17")]
theorem
extDerivFun_add
{π : 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]
{g g' : M β F}
{x : M}
(hg : MDiffAt g x)
(hg' : MDiffAt g' x)
:
Alias of mvfderiv_add.
@[simp]
theorem
mvfderiv_sub
{π : 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]
{g g' : M β F}
{x : M}
(hg : MDiffAt g x)
(hg' : MDiffAt g' x)
:
theorem
mvfderiv_fun_sub
{π : 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]
{g g' : M β F}
{x : M}
(hg : MDiffAt g x)
(hg' : MDiffAt g' x)
:
Eta-expanded form of mvfderiv_sub
@[simp]
theorem
mvfderiv_neg
{π : 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]
{g : M β F}
{x : M}
:
theorem
mvfderiv_fun_neg
{π : 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]
{g : M β F}
{x : M}
:
Eta-expanded form of mvfderiv_neg
@[simp]
theorem
mvfderiv_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]
{F : Type u_8}
[NormedAddCommGroup F]
[NormedSpace π F]
{x : M}
{a : M β π}
(ha : MDiffAt a x)
{g : M β F}
(hg : MDiffAt g x)
:
theorem
mvfderiv_fun_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]
{F : Type u_8}
[NormedAddCommGroup F]
[NormedSpace π F]
{x : M}
{a : M β π}
(ha : MDiffAt a x)
{g : M β F}
(hg : MDiffAt g x)
:
Eta-expanded form of mvfderiv_smul
@[simp]
theorem
mvfderiv_mul
{π : 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 g : M β π}
{x : M}
(hf : MDiffAt f x)
(hg : MDiffAt g x)
:
theorem
mvfderiv_fun_mul
{π : 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 g : M β π}
{x : M}
(hf : MDiffAt f x)
(hg : MDiffAt g x)
:
Eta-expanded form of mvfderiv_mul
@[simp]
theorem
mvfderiv_zero
{π : 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]
{x : M}
:
@[deprecated mvfderiv_zero (since := "2026-05-17")]
theorem
extDerivFun_zero
{π : 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]
{x : M}
:
Alias of mvfderiv_zero.