Documentation

Mathlib.Geometry.Manifold.MFDeriv.FDeriv

Relations between vector space derivative and manifold derivative #

The manifold derivative mfderiv, when considered on the model vector space with its trivial manifold structure, coincides with the usual FrΓ©chet derivative fderiv. In this section, we prove this and related statements.

theorem uniqueMDiffWithinAt_iff_uniqueDiffWithinAt {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {s : Set E} {x : E} :
theorem UniqueDiffWithinAt.uniqueMDiffWithinAt {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {s : Set E} {x : E} :
UniqueDiffWithinAt π•œ s x β†’ UniqueMDiffWithinAt (modelWithCornersSelf π•œ E) s x

Alias of the reverse direction of uniqueMDiffWithinAt_iff_uniqueDiffWithinAt.

theorem UniqueMDiffWithinAt.uniqueDiffWithinAt {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {s : Set E} {x : E} :
UniqueMDiffWithinAt (modelWithCornersSelf π•œ E) s x β†’ UniqueDiffWithinAt π•œ s x

Alias of the forward direction of uniqueMDiffWithinAt_iff_uniqueDiffWithinAt.

theorem uniqueMDiffOn_iff_uniqueDiffOn {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {s : Set E} :
theorem UniqueDiffOn.uniqueMDiffOn {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {s : Set E} :
UniqueDiffOn π•œ s β†’ UniqueMDiffOn (modelWithCornersSelf π•œ E) s

Alias of the reverse direction of uniqueMDiffOn_iff_uniqueDiffOn.

theorem UniqueMDiffOn.uniqueDiffOn {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {s : Set E} :
UniqueMDiffOn (modelWithCornersSelf π•œ E) s β†’ UniqueDiffOn π•œ s

Alias of the forward direction of uniqueMDiffOn_iff_uniqueDiffOn.

theorem ModelWithCorners.uniqueMDiffOn {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners π•œ E H) :
@[simp]
theorem writtenInExtChartAt_model_space {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace π•œ E'] {f : E β†’ E'} {x : E} :
theorem hasMFDerivWithinAt_iff_hasFDerivWithinAt {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace π•œ E'] {f : E β†’ E'} {s : Set E} {x : E} {f' : TangentSpace (modelWithCornersSelf π•œ E) x β†’L[π•œ] TangentSpace (modelWithCornersSelf π•œ E') (f x)} :
theorem HasFDerivWithinAt.hasMFDerivWithinAt {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace π•œ E'] {f : E β†’ E'} {s : Set E} {x : E} {f' : TangentSpace (modelWithCornersSelf π•œ E) x β†’L[π•œ] TangentSpace (modelWithCornersSelf π•œ E') (f x)} :
HasFDerivWithinAt f f' s x β†’ HasMFDerivWithinAt (modelWithCornersSelf π•œ E) (modelWithCornersSelf π•œ E') f s x f'

Alias of the reverse direction of hasMFDerivWithinAt_iff_hasFDerivWithinAt.

theorem HasMFDerivWithinAt.hasFDerivWithinAt {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace π•œ E'] {f : E β†’ E'} {s : Set E} {x : E} {f' : TangentSpace (modelWithCornersSelf π•œ E) x β†’L[π•œ] TangentSpace (modelWithCornersSelf π•œ E') (f x)} :
HasMFDerivWithinAt (modelWithCornersSelf π•œ E) (modelWithCornersSelf π•œ E') f s x f' β†’ HasFDerivWithinAt f f' s x

Alias of the forward direction of hasMFDerivWithinAt_iff_hasFDerivWithinAt.

theorem hasMFDerivAt_iff_hasFDerivAt {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace π•œ E'] {f : E β†’ E'} {x : E} {f' : TangentSpace (modelWithCornersSelf π•œ E) x β†’L[π•œ] TangentSpace (modelWithCornersSelf π•œ E') (f x)} :
theorem HasFDerivAt.hasMFDerivAt {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace π•œ E'] {f : E β†’ E'} {x : E} {f' : TangentSpace (modelWithCornersSelf π•œ E) x β†’L[π•œ] TangentSpace (modelWithCornersSelf π•œ E') (f x)} :
HasFDerivAt f f' x β†’ HasMFDerivAt (modelWithCornersSelf π•œ E) (modelWithCornersSelf π•œ E') f x f'

Alias of the reverse direction of hasMFDerivAt_iff_hasFDerivAt.

theorem HasMFDerivAt.hasFDerivAt {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace π•œ E'] {f : E β†’ E'} {x : E} {f' : TangentSpace (modelWithCornersSelf π•œ E) x β†’L[π•œ] TangentSpace (modelWithCornersSelf π•œ E') (f x)} :
HasMFDerivAt (modelWithCornersSelf π•œ E) (modelWithCornersSelf π•œ E') f x f' β†’ HasFDerivAt f f' x

Alias of the forward direction of hasMFDerivAt_iff_hasFDerivAt.

theorem mdifferentiableWithinAt_iff_differentiableWithinAt {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace π•œ E'] {f : E β†’ E'} {s : Set E} {x : E} :

For maps between vector spaces, MDifferentiableWithinAt and DifferentiableWithinAt coincide

theorem MDifferentiableWithinAt.differentiableWithinAt {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace π•œ E'] {f : E β†’ E'} {s : Set E} {x : E} :
MDifferentiableWithinAt (modelWithCornersSelf π•œ E) (modelWithCornersSelf π•œ E') f s x β†’ DifferentiableWithinAt π•œ f s x

Alias of the forward direction of mdifferentiableWithinAt_iff_differentiableWithinAt.


For maps between vector spaces, MDifferentiableWithinAt and DifferentiableWithinAt coincide

theorem DifferentiableWithinAt.mdifferentiableWithinAt {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace π•œ E'] {f : E β†’ E'} {s : Set E} {x : E} :
DifferentiableWithinAt π•œ f s x β†’ MDifferentiableWithinAt (modelWithCornersSelf π•œ E) (modelWithCornersSelf π•œ E') f s x

Alias of the reverse direction of mdifferentiableWithinAt_iff_differentiableWithinAt.


For maps between vector spaces, MDifferentiableWithinAt and DifferentiableWithinAt coincide

theorem mdifferentiableAt_iff_differentiableAt {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace π•œ E'] {f : E β†’ E'} {x : E} :

For maps between vector spaces, MDifferentiableAt and DifferentiableAt coincide

theorem DifferentiableAt.mdifferentiableAt {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace π•œ E'] {f : E β†’ E'} {x : E} :
DifferentiableAt π•œ f x β†’ MDifferentiableAt (modelWithCornersSelf π•œ E) (modelWithCornersSelf π•œ E') f x

Alias of the reverse direction of mdifferentiableAt_iff_differentiableAt.


For maps between vector spaces, MDifferentiableAt and DifferentiableAt coincide

theorem MDifferentiableAt.differentiableAt {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace π•œ E'] {f : E β†’ E'} {x : E} :
MDifferentiableAt (modelWithCornersSelf π•œ E) (modelWithCornersSelf π•œ E') f x β†’ DifferentiableAt π•œ f x

Alias of the forward direction of mdifferentiableAt_iff_differentiableAt.


For maps between vector spaces, MDifferentiableAt and DifferentiableAt coincide

theorem mdifferentiableOn_iff_differentiableOn {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace π•œ E'] {f : E β†’ E'} {s : Set E} :

For maps between vector spaces, MDifferentiableOn and DifferentiableOn coincide

theorem MDifferentiableOn.differentiableOn {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace π•œ E'] {f : E β†’ E'} {s : Set E} :
MDifferentiableOn (modelWithCornersSelf π•œ E) (modelWithCornersSelf π•œ E') f s β†’ DifferentiableOn π•œ f s

Alias of the forward direction of mdifferentiableOn_iff_differentiableOn.


For maps between vector spaces, MDifferentiableOn and DifferentiableOn coincide

theorem DifferentiableOn.mdifferentiableOn {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace π•œ E'] {f : E β†’ E'} {s : Set E} :
DifferentiableOn π•œ f s β†’ MDifferentiableOn (modelWithCornersSelf π•œ E) (modelWithCornersSelf π•œ E') f s

Alias of the reverse direction of mdifferentiableOn_iff_differentiableOn.


For maps between vector spaces, MDifferentiableOn and DifferentiableOn coincide

theorem mdifferentiable_iff_differentiable {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace π•œ E'] {f : E β†’ E'} :

For maps between vector spaces, MDifferentiable and Differentiable coincide

theorem Differentiable.mdifferentiable {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace π•œ E'] {f : E β†’ E'} :
Differentiable π•œ f β†’ MDifferentiable (modelWithCornersSelf π•œ E) (modelWithCornersSelf π•œ E') f

Alias of the reverse direction of mdifferentiable_iff_differentiable.


For maps between vector spaces, MDifferentiable and Differentiable coincide

theorem MDifferentiable.differentiable {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace π•œ E'] {f : E β†’ E'} :
MDifferentiable (modelWithCornersSelf π•œ E) (modelWithCornersSelf π•œ E') f β†’ Differentiable π•œ f

Alias of the forward direction of mdifferentiable_iff_differentiable.


For maps between vector spaces, MDifferentiable and Differentiable coincide

@[simp]
theorem mfderivWithin_eq_fderivWithin {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace π•œ E'] {f : E β†’ E'} {s : Set E} {x : E} :
mfderivWithin (modelWithCornersSelf π•œ E) (modelWithCornersSelf π•œ E') f s x = fderivWithin π•œ f s x

For maps between vector spaces, mfderivWithin and fderivWithin coincide

@[simp]
theorem mfderiv_eq_fderiv {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace π•œ E'] {f : E β†’ E'} {x : E} :
mfderiv (modelWithCornersSelf π•œ E) (modelWithCornersSelf π•œ E') f x = fderiv π•œ f x

For maps between vector spaces, mfderiv and fderiv coincide