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.
Main definitions #
In addition to the above, this file provides two important definitions.
mvfderiv I f xis the manifold Fréchet derivative atx : Mof a vector-valued functionf : M → V, but taking values in the target normed spaceVinstead ofTangentSpace% (f x) V. Mathematically, this uses the global trivializationT V ≅ V × V, yielding an identificationT_v V ≅ Vfor eachv : V. In Lean, we post-compose the differentialmfderiv% f xwithNormedSpace.fromTangentSpace. IfVis a field, this coincides with the exterior derivative offas a section of the cotangent bundle. There is notationd% fformvfderiv I fvia a custom elaborator scoped to theManifoldnamespace, with a corresponding delaborator,mvfderivWithinwith notationd[s] fformvfderivWithin I f sin theManifoldnamespace: the analogous concept within a set, with analogous API lemmas
Main results #
This file contains
- results about the differentiability of scalar multiplication (
mfderiv_smuland friends), - basic lemmas about
mvfderiv(such as addition, subtraction, multiplication and constants), - analogous lemmas about
mvfderivWithin, - composition lemmas about
mvfderivWithinandmvfderiv.
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
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 (f • g) x
theorem
MDifferentiableAt.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]
{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 (i : M) => f i • g i) x
Eta-expanded form of MDifferentiableAt.smul
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] (f • g)
theorem
MDifferentiableOn.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]
{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 (i : M) => f i • g i
Eta-expanded form of MDifferentiableOn.smul
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 (f • g)
theorem
MDifferentiable.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]
{V : Type u_18}
[NormedAddCommGroup V]
[NormedSpace 𝕜 V]
{f : M → 𝕜}
{g : M → V}
(hf : MDiff f)
(hg : MDiff g)
:
MDiff fun (i : M) => f i • g i
Eta-expanded form of MDifferentiable.smul
Exterior derivative of a vector-valued function #
noncomputable def
mvfderivWithin
{𝕜 : 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)
(s : Set M)
(x : M)
:
mvfderivWithin I J f s x is the mfderiv of a vector-valued function f on M at x
within the set s, but taking values in the target normed space directly.
The difference to mfderivWithin is explained in the module-docstring for
Mathlib/Geometry/Manifold/MFDeriv/NormedSpace.lean.
Future: this could be generalised to functions into additive torsors over abelian Lie groups.
Equations
- d[s] g x = ↑(NormedSpace.fromTangentSpace (g x)) ∘SL mfderiv[s] g x
Instances For
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)
:
mvfderiv I J f x is the mfderiv of a vector-valued function f on M at x,
but taking values in the target normed space directly.
The difference to mfderiv is explained in the module-docstring for
Mathlib/Geometry/Manifold/MFDeriv/NormedSpace.lean.
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.
mvfderiv I J f x is the mfderiv of a vector-valued function f on M at x,
but taking values in the target normed space directly.
The difference to mfderiv is explained in the module-docstring for
Mathlib/Geometry/Manifold/MFDeriv/NormedSpace.lean.
Future: this could be generalised to functions into additive torsors over abelian Lie groups.
Equations
Instances For
d[s] f x (scoped to the Manifold namespace) elaborates to mvfderivWithin I f s x,
trying to determine I and J from the local context.
Equations
- One or more equations did not get rendered due to their size.
Instances For
d% f x (scoped to the Manifold namespace) elaborates to mvfderiv I f x,
trying to determine I and J from the local context.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Delaborator for mvfderivWithin.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Delaborator for mvfderiv.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
mvfderivWithin_univ
{𝕜 : 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 : M → F}
:
theorem
mvfderivWithin_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]
{s : Set M}
(c : F)
{x : M}
:
@[simp]
theorem
mvfderivWithin_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]
{s : Set M}
{g g' : M → F}
{x : M}
(hg : MDiffAt[s] g x)
(hg' : MDiffAt[s] g' x)
(hs : UniqueMDiffAt[s] x)
:
theorem
mvfderivWithin_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]
{s : Set M}
{g g' : M → F}
{x : M}
(hg : MDiffAt[s] g x)
(hg' : MDiffAt[s] g' x)
(hs : UniqueMDiffAt[s] x)
:
Eta-expanded form of mvfderivWithin_add
@[simp]
theorem
mvfderivWithin_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]
{s : Set M}
{g g' : M → F}
{x : M}
(hg : MDiffAt[s] g x)
(hg' : MDiffAt[s] g' x)
(hs : UniqueMDiffAt[s] x)
:
theorem
mvfderivWithin_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]
{s : Set M}
{g g' : M → F}
{x : M}
(hg : MDiffAt[s] g x)
(hg' : MDiffAt[s] g' x)
(hs : UniqueMDiffAt[s] x)
:
Eta-expanded form of mvfderivWithin_sub
@[simp]
theorem
mvfderivWithin_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]
{s : Set M}
{g : M → F}
{x : M}
(hs : UniqueMDiffAt[s] x)
:
theorem
mvfderivWithin_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]
{s : Set M}
{g : M → F}
{x : M}
(hs : UniqueMDiffAt[s] x)
:
Eta-expanded form of mvfderivWithin_neg
@[simp]
theorem
mvfderivWithin_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]
{s : Set M}
{x : M}
{a : M → 𝕜}
(ha : MDiffAt[s] a x)
{g : M → F}
(hg : MDiffAt[s] g x)
(hs : UniqueMDiffAt[s] x)
:
theorem
mvfderivWithin_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]
{s : Set M}
{x : M}
{a : M → 𝕜}
(ha : MDiffAt[s] a x)
{g : M → F}
(hg : MDiffAt[s] g x)
(hs : UniqueMDiffAt[s] x)
:
Eta-expanded form of mvfderivWithin_smul
@[simp]
theorem
mvfderivWithin_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]
{s : Set M}
{f g : M → 𝕜}
{x : M}
(hf : MDiffAt[s] f x)
(hg : MDiffAt[s] g x)
(hs : UniqueMDiffAt[s] x)
:
theorem
mvfderivWithin_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]
{s : Set M}
{f g : M → 𝕜}
{x : M}
(hf : MDiffAt[s] f x)
(hg : MDiffAt[s] g x)
(hs : UniqueMDiffAt[s] x)
:
Eta-expanded form of mvfderivWithin_mul
@[simp]
theorem
mvfderivWithin_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}
{s : Set M}
(hs : UniqueMDiffAt[s] x)
:
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.
theorem
MDifferentiableWithinAt.mvfderivWithin
{𝕜 : 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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{s : Set M}
{x : M}
{f : M → E'}
(h : MDiffAt[s] f x)
:
d[s] f x = fderivWithin 𝕜 (writtenInExtChartAt I (modelWithCornersSelf 𝕜 E') x f) (↑(extChartAt I x).symm ⁻¹' s ∩ Set.range ↑I)
(↑(extChartAt I x) x)
theorem
MDifferentiableAt.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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{x : M}
{f : M → E'}
(h : MDiffAt f x)
:
d% f x = fderivWithin 𝕜 (writtenInExtChartAt I (modelWithCornersSelf 𝕜 E') x f) (Set.range ↑I) (↑(extChartAt I x) x)
@[simp]
theorem
mvfderivWithin_eq_fderivWithin
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{f : E → E'}
{s : Set E}
{x : E}
:
For maps between vector spaces, mvfderivWithin and fderivWithin coincide.
@[simp]
theorem
mvfderiv_eq_fderiv
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{f : E → E'}
{x : E}
:
For maps between vector spaces, mvfderiv and fderiv coincide.
theorem
mfderivWithin_eq_fderivWithin
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{f : E → E'}
{s : Set E}
{x : E}
:
mfderiv[s] f x = ↑(NormedSpace.fromTangentSpace (f x)).symm ∘SL fderivWithin 𝕜 f s x ∘SL ↑(NormedSpace.fromTangentSpace x)
For maps between vector spaces, mfderivWithin and fderivWithin coincide.
theorem
mfderiv_eq_fderiv
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{f : E → E'}
{x : E}
:
mfderiv% f x = ↑(NormedSpace.fromTangentSpace (f x)).symm ∘SL fderiv 𝕜 f x ∘SL ↑(NormedSpace.fromTangentSpace x)
For maps between vector spaces, mfderiv and fderiv coincide.
Composition lemmas for mvfderiv(Within) #
theorem
mvfderivWithin_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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{F : Type u_8}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : M' → M}
{g : M → F}
{u : Set M}
{s : Set M'}
(x : M')
(hg : MDiffAt[u] g (f x))
(hf : MDiffAt[s] f x)
(h : s ⊆ f ⁻¹' u)
(hxs : UniqueMDiffAt[s] x)
:
theorem
mvfderivWithin_comp_of_eq
{𝕜 : 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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{F : Type u_8}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : M' → M}
{g : M → F}
{x : M'}
{y : M}
{u : Set M}
{s : Set M'}
(hg : MDiffAt[u] g y)
(hf : MDiffAt[s] f x)
(h : s ⊆ f ⁻¹' u)
(hxs : UniqueMDiffAt[s] x)
(hy : f x = y)
:
theorem
mvfderivWithin_comp_of_preimage_mem_nhdsWithin
{𝕜 : 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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{F : Type u_8}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : M' → M}
{g : M → F}
{u : Set M}
{s : Set M'}
(x : M')
(hg : MDiffAt[u] g (f x))
(hf : MDiffAt[s] f x)
(h : f ⁻¹' u ∈ nhdsWithin x s)
(hxs : UniqueMDiffAt[s] x)
:
theorem
mvfderivWithin_comp_of_preimage_mem_nhdsWithin_of_eq
{𝕜 : 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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{F : Type u_8}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : M' → M}
{g : M → F}
{y : M}
{u : Set M}
{s : Set M'}
(x : M')
(hg : MDiffAt[u] g y)
(hf : MDiffAt[s] f x)
(h : f ⁻¹' u ∈ nhdsWithin x s)
(hxs : UniqueMDiffAt[s] x)
(hy : f x = y)
:
theorem
mvfderiv_comp_mfderivWithin
{𝕜 : 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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{F : Type u_8}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : M' → M}
{g : M → F}
{s : Set M'}
(x : M')
(hg : MDiffAt g (f x))
(hf : MDiffAt[s] f x)
(hxs : UniqueMDiffAt[s] x)
:
theorem
mvfderiv_comp_mfderivWithin_of_eq
{𝕜 : 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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{F : Type u_8}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : M' → M}
{g : M → F}
{x : M'}
{y : M}
{s : Set M'}
(hg : MDiffAt g y)
(hf : MDiffAt[s] f x)
(hxs : UniqueMDiffAt[s] x)
(hy : f x = y)
:
theorem
mvfderiv_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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{F : Type u_8}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : M' → M}
{g : M → F}
(x : M')
(hg : MDiffAt g (f x))
(hf : MDiffAt f x)
:
theorem
mvfderiv_comp_of_eq
{𝕜 : 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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{F : Type u_8}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : M' → M}
{g : M → F}
{x : M'}
{y : M}
(hg : MDiffAt g y)
(hf : MDiffAt f x)
(hy : f x = y)
:
theorem
mvfderiv_comp_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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{F : Type u_8}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : M' → M}
{g : M → F}
(x : M')
(hg : MDiffAt g (f x))
(hf : MDiffAt f x)
(v : TangentSpace I' x)
:
theorem
mvfderiv_comp_apply_of_eq
{𝕜 : 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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{F : Type u_8}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : M' → M}
{g : M → F}
{y : M}
(x : M')
(hg : MDiffAt g y)
(hf : MDiffAt f x)
(hy : f x = y)
(v : TangentSpace I' x)
: