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 Frechet 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} : UniqueMDiffWithinAt (modelWithCornersSelf 𝕜 E) s x ↔ UniqueDiffWithinAt 𝕜 s x

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 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 uniqueMDiffOn_iff_uniqueDiffOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {s : Set E} : UniqueMDiffOn (modelWithCornersSelf 𝕜 E) s ↔ UniqueDiffOn 𝕜 s

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 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.

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

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

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)} : HasMFDerivAt (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') f x f' ↔ HasFDerivAt f 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} : MDifferentiableWithinAt (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') f s x ↔ DifferentiableWithinAt 𝕜 f s x

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

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} : MDifferentiableOn (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') f s ↔ DifferentiableOn 𝕜 f s

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'} : MDifferentiable (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') f ↔ Differentiable 𝕜 f

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

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

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