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.

source

theorem uniqueMDiffWithinAt_iff_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

source

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.

source

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.

source

theorem uniqueMDiffOn_iff_uniqueDiffOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {s : Set E} :

UniqueMDiffOn (modelWithCornersSelf 𝕜 E) s ↔ UniqueDiffOn 𝕜 s

source

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.

source

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.

source

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

UniqueMDiffOn (modelWithCornersSelf 𝕜 E) (Set.range ↑I)

source

@[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} :

writtenInExtChartAt (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') x f = f

source

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

HasMFDerivWithinAt (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') f s x f' ↔ HasFDerivWithinAt f f' s x

source

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.

source

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.

source

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

HasMFDerivAt (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') f x f' ↔ HasFDerivAt f f' x

source

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.

source

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.

source

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

MDifferentiableWithinAt (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') f s x ↔ DifferentiableWithinAt 𝕜 f s x

For maps between vector spaces, MDifferentiableWithinAt and DifferentiableWithinAt coincide

source

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

source

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

source

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

MDifferentiableAt (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') f x ↔ DifferentiableAt 𝕜 f x

For maps between vector spaces, MDifferentiableAt and DifferentiableAt coincide

source

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

source

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

source

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

MDifferentiableOn (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') f s ↔ DifferentiableOn 𝕜 f s

For maps between vector spaces, MDifferentiableOn and DifferentiableOn coincide

source

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

source

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

source

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

MDifferentiable (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') f ↔ Differentiable 𝕜 f

For maps between vector spaces, MDifferentiable and Differentiable coincide

source

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

source

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

source

@[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

source

@[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