Differentiability of specific functions #
In this file, we establish differentiability results for
- continuous linear maps and continuous linear equivalences
- the identity
- constant functions
- products
- arithmetic operations (such as addition and scalar multiplication).
Differentiability of specific functions #
theorem
ContinuousLinearMap.hasMFDerivWithinAt
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
(f : E →L[𝕜] E')
{s : Set E}
{x : E}
:
HasMFDerivWithinAt (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') (⇑f) s x f
theorem
ContinuousLinearMap.hasMFDerivAt
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
(f : E →L[𝕜] E')
{x : E}
:
HasMFDerivAt (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') (⇑f) x f
theorem
ContinuousLinearMap.mdifferentiableWithinAt
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
(f : E →L[𝕜] E')
{s : Set E}
{x : E}
:
MDifferentiableWithinAt (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') (⇑f) s x
theorem
ContinuousLinearMap.mdifferentiableOn
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
(f : E →L[𝕜] E')
{s : Set E}
:
MDifferentiableOn (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') (⇑f) s
theorem
ContinuousLinearMap.mdifferentiableAt
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
(f : E →L[𝕜] E')
{x : E}
:
MDifferentiableAt (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') (⇑f) x
theorem
ContinuousLinearMap.mdifferentiable
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
(f : E →L[𝕜] E')
:
MDifferentiable (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') ⇑f
theorem
ContinuousLinearMap.mfderiv_eq
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
(f : E →L[𝕜] E')
{x : E}
:
mfderiv (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') (⇑f) x = f
theorem
ContinuousLinearMap.mfderivWithin_eq
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
(f : E →L[𝕜] E')
{s : Set E}
{x : E}
(hs : UniqueMDiffWithinAt (modelWithCornersSelf 𝕜 E) s x)
:
mfderivWithin (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') (⇑f) s x = f
theorem
ContinuousLinearEquiv.hasMFDerivWithinAt
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
(f : E ≃L[𝕜] E')
{s : Set E}
{x : E}
:
HasMFDerivWithinAt (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') (⇑f) s x ↑f
theorem
ContinuousLinearEquiv.hasMFDerivAt
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
(f : E ≃L[𝕜] E')
{x : E}
:
HasMFDerivAt (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') (⇑f) x ↑f
theorem
ContinuousLinearEquiv.mdifferentiableWithinAt
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
(f : E ≃L[𝕜] E')
{s : Set E}
{x : E}
:
MDifferentiableWithinAt (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') (⇑f) s x
theorem
ContinuousLinearEquiv.mdifferentiableOn
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
(f : E ≃L[𝕜] E')
{s : Set E}
:
MDifferentiableOn (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') (⇑f) s
theorem
ContinuousLinearEquiv.mdifferentiableAt
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
(f : E ≃L[𝕜] E')
{x : E}
:
MDifferentiableAt (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') (⇑f) x
theorem
ContinuousLinearEquiv.mdifferentiable
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
(f : E ≃L[𝕜] E')
:
MDifferentiable (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') ⇑f
theorem
ContinuousLinearEquiv.mfderiv_eq
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
(f : E ≃L[𝕜] E')
{x : E}
:
mfderiv (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') (⇑f) x = ↑f
theorem
ContinuousLinearEquiv.mfderivWithin_eq
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
(f : E ≃L[𝕜] E')
{s : Set E}
{x : E}
(hs : UniqueMDiffWithinAt (modelWithCornersSelf 𝕜 E) s x)
:
mfderivWithin (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') (⇑f) s x = ↑f
Identity #
theorem
hasMFDerivAt_id
{𝕜 : 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)
:
HasMFDerivAt I I id x (ContinuousLinearMap.id 𝕜 (TangentSpace I x))
theorem
hasMFDerivWithinAt_id
{𝕜 : 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)
:
HasMFDerivWithinAt I I id s x (ContinuousLinearMap.id 𝕜 (TangentSpace I x))
theorem
mdifferentiableAt_id
{𝕜 : 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}
:
MDifferentiableAt I I id x
theorem
mdifferentiableWithinAt_id
{𝕜 : 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}
:
MDifferentiableWithinAt I I id s x
theorem
mdifferentiable_id
{𝕜 : 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]
:
MDifferentiable I I id
theorem
mdifferentiableOn_id
{𝕜 : 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}
:
MDifferentiableOn I I id s
@[simp]
theorem
mfderiv_id
{𝕜 : 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}
:
mfderiv I I id x = ContinuousLinearMap.id 𝕜 (TangentSpace I x)
theorem
mfderivWithin_id
{𝕜 : 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}
(hxs : UniqueMDiffWithinAt I s x)
:
mfderivWithin I I id s x = ContinuousLinearMap.id 𝕜 (TangentSpace I x)
@[simp]
theorem
tangentMap_id
{𝕜 : 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]
:
tangentMap I I id = id
theorem
tangentMapWithin_id
{𝕜 : 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}
{p : TangentBundle I M}
(hs : UniqueMDiffWithinAt I s p.proj)
:
tangentMapWithin I I id s p = p
Constants #
theorem
hasMFDerivAt_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]
{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']
(c : M')
(x : M)
:
HasMFDerivAt I I' (fun (x : M) => c) x 0
theorem
hasMFDerivWithinAt_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]
{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']
(c : M')
(s : Set M)
(x : M)
:
HasMFDerivWithinAt I I' (fun (x : M) => c) s x 0
theorem
mdifferentiableAt_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]
{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']
{x : M}
{c : M'}
:
MDifferentiableAt I I' (fun (x : M) => c) x
theorem
mdifferentiableWithinAt_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]
{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']
{s : Set M}
{x : M}
{c : M'}
:
MDifferentiableWithinAt I I' (fun (x : M) => c) s x
theorem
mdifferentiable_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]
{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']
{c : M'}
:
MDifferentiable I I' fun (x : M) => c
theorem
mdifferentiableOn_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]
{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']
{s : Set M}
{c : M'}
:
MDifferentiableOn I I' (fun (x : M) => c) s
@[simp]
theorem
mfderiv_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]
{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']
{x : M}
{c : M'}
:
theorem
mfderivWithin_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]
{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']
{s : Set M}
{x : M}
{c : M'}
(hxs : UniqueMDiffWithinAt I s x)
:
mfderivWithin I I' (fun (x : M) => c) s x = 0
Operations on the product of two manifolds #
theorem
hasMFDerivAt_fst
{𝕜 : 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']
(x : M × M')
:
HasMFDerivAt (I.prod I') I Prod.fst x (ContinuousLinearMap.fst 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2))
theorem
hasMFDerivWithinAt_fst
{𝕜 : 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']
(s : Set (M × M'))
(x : M × M')
:
HasMFDerivWithinAt (I.prod I') I Prod.fst s x (ContinuousLinearMap.fst 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2))
theorem
mdifferentiableAt_fst
{𝕜 : 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']
{x : M × M'}
:
MDifferentiableAt (I.prod I') I Prod.fst x
theorem
mdifferentiableWithinAt_fst
{𝕜 : 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']
{s : Set (M × M')}
{x : M × M'}
:
MDifferentiableWithinAt (I.prod I') I Prod.fst s x
theorem
mdifferentiable_fst
{𝕜 : 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']
:
MDifferentiable (I.prod I') I Prod.fst
theorem
mdifferentiableOn_fst
{𝕜 : 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']
{s : Set (M × M')}
:
MDifferentiableOn (I.prod I') I Prod.fst s
@[simp]
theorem
mfderiv_fst
{𝕜 : 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']
{x : M × M'}
:
mfderiv (I.prod I') I Prod.fst x = ContinuousLinearMap.fst 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2)
theorem
mfderivWithin_fst
{𝕜 : 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']
{s : Set (M × M')}
{x : M × M'}
(hxs : UniqueMDiffWithinAt (I.prod I') s x)
:
mfderivWithin (I.prod I') I Prod.fst s x = ContinuousLinearMap.fst 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2)
@[simp]
theorem
tangentMap_prod_fst
{𝕜 : 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']
{p : TangentBundle (I.prod I') (M × M')}
:
tangentMap (I.prod I') I Prod.fst p = { proj := p.proj.1, snd := p.snd.1 }
theorem
tangentMapWithin_prod_fst
{𝕜 : 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']
{s : Set (M × M')}
{p : TangentBundle (I.prod I') (M × M')}
(hs : UniqueMDiffWithinAt (I.prod I') s p.proj)
:
tangentMapWithin (I.prod I') I Prod.fst s p = { proj := p.proj.1, snd := p.snd.1 }
theorem
hasMFDerivAt_snd
{𝕜 : 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']
(x : M × M')
:
HasMFDerivAt (I.prod I') I' Prod.snd x (ContinuousLinearMap.snd 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2))
theorem
hasMFDerivWithinAt_snd
{𝕜 : 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']
(s : Set (M × M'))
(x : M × M')
:
HasMFDerivWithinAt (I.prod I') I' Prod.snd s x (ContinuousLinearMap.snd 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2))
theorem
mdifferentiableAt_snd
{𝕜 : 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']
{x : M × M'}
:
MDifferentiableAt (I.prod I') I' Prod.snd x
theorem
mdifferentiableWithinAt_snd
{𝕜 : 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']
{s : Set (M × M')}
{x : M × M'}
:
MDifferentiableWithinAt (I.prod I') I' Prod.snd s x
theorem
mdifferentiable_snd
{𝕜 : 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']
:
MDifferentiable (I.prod I') I' Prod.snd
theorem
mdifferentiableOn_snd
{𝕜 : 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']
{s : Set (M × M')}
:
MDifferentiableOn (I.prod I') I' Prod.snd s
@[simp]
theorem
mfderiv_snd
{𝕜 : 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']
{x : M × M'}
:
mfderiv (I.prod I') I' Prod.snd x = ContinuousLinearMap.snd 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2)
theorem
mfderivWithin_snd
{𝕜 : 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']
{s : Set (M × M')}
{x : M × M'}
(hxs : UniqueMDiffWithinAt (I.prod I') s x)
:
mfderivWithin (I.prod I') I' Prod.snd s x = ContinuousLinearMap.snd 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2)
@[simp]
theorem
tangentMap_prod_snd
{𝕜 : 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']
{p : TangentBundle (I.prod I') (M × M')}
:
tangentMap (I.prod I') I' Prod.snd p = { proj := p.proj.2, snd := p.snd.2 }
theorem
tangentMapWithin_prod_snd
{𝕜 : 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']
{s : Set (M × M')}
{p : TangentBundle (I.prod I') (M × M')}
(hs : UniqueMDiffWithinAt (I.prod I') s p.proj)
:
tangentMapWithin (I.prod I') I' Prod.snd s p = { proj := p.proj.2, snd := p.snd.2 }
theorem
MDifferentiableAt.mfderiv_prod
{𝕜 : 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']
{E'' : Type u_8}
[NormedAddCommGroup E'']
[NormedSpace 𝕜 E'']
{H'' : Type u_9}
[TopologicalSpace H'']
{I'' : ModelWithCorners 𝕜 E'' H''}
{M'' : Type u_10}
[TopologicalSpace M'']
[ChartedSpace H'' M'']
{f : M → M'}
{g : M → M''}
{x : M}
(hf : MDifferentiableAt I I' f x)
(hg : MDifferentiableAt I I'' g x)
:
theorem
mfderiv_prod_left
{𝕜 : 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']
{x₀ : M}
{y₀ : M'}
:
mfderiv I (I.prod I') (fun (x : M) => (x, y₀)) x₀ = ContinuousLinearMap.inl 𝕜 (TangentSpace I x₀) (TangentSpace I' y₀)
theorem
mfderiv_prod_right
{𝕜 : 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']
{x₀ : M}
{y₀ : M'}
:
mfderiv I' (I.prod I') (fun (y : M') => (x₀, y)) y₀ = ContinuousLinearMap.inr 𝕜 (TangentSpace I x₀) (TangentSpace I' y₀)
theorem
mfderiv_prod_eq_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]
{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']
{E'' : Type u_8}
[NormedAddCommGroup E'']
[NormedSpace 𝕜 E'']
{H'' : Type u_9}
[TopologicalSpace H'']
{I'' : ModelWithCorners 𝕜 E'' H''}
{M'' : Type u_10}
[TopologicalSpace M'']
[ChartedSpace H'' M'']
{f : M × M' → M''}
{p : M × M'}
(hf : MDifferentiableAt (I.prod I') I'' f p)
:
The total derivative of a function in two variables is the sum of the partial derivatives.
Note that to state this (without casts) we need to be able to see through the definition of
TangentSpace.
Arithmetic #
Note that in the HasMFDerivAt lemmas there is an abuse of the defeq between E' and
TangentSpace 𝓘(𝕜, E') (f z) (similarly for g',F',p',q'). In general this defeq is not
canonical, but in this case (the tangent space of a vector space) it is canonical.
theorem
HasMFDerivAt.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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{z : M}
{f g : M → E'}
{f' g' : TangentSpace I z →L[𝕜] E'}
(hf : HasMFDerivAt I (modelWithCornersSelf 𝕜 E') f z f')
(hg : HasMFDerivAt I (modelWithCornersSelf 𝕜 E') g z g')
:
HasMFDerivAt I (modelWithCornersSelf 𝕜 E') (f + g) z (f' + g')
theorem
MDifferentiableAt.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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{z : M}
{f g : M → E'}
(hf : MDifferentiableAt I (modelWithCornersSelf 𝕜 E') f z)
(hg : MDifferentiableAt I (modelWithCornersSelf 𝕜 E') g z)
:
MDifferentiableAt I (modelWithCornersSelf 𝕜 E') (f + g) z
theorem
MDifferentiable.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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{f g : M → E'}
(hf : MDifferentiable I (modelWithCornersSelf 𝕜 E') f)
(hg : MDifferentiable I (modelWithCornersSelf 𝕜 E') g)
:
MDifferentiable I (modelWithCornersSelf 𝕜 E') (f + g)
theorem
mfderiv_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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{z : M}
{f g : M → E'}
(hf : MDifferentiableAt I (modelWithCornersSelf 𝕜 E') f z)
(hg : MDifferentiableAt I (modelWithCornersSelf 𝕜 E') g z)
:
mfderiv I (modelWithCornersSelf 𝕜 E') (f + g) z = mfderiv I (modelWithCornersSelf 𝕜 E') f z + mfderiv I (modelWithCornersSelf 𝕜 E') g z
theorem
HasMFDerivAt.const_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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{z : M}
{f : M → E'}
{f' : TangentSpace I z →L[𝕜] E'}
(hf : HasMFDerivAt I (modelWithCornersSelf 𝕜 E') f z f')
(s : 𝕜)
:
HasMFDerivAt I (modelWithCornersSelf 𝕜 E') (s • f) z (s • f')
theorem
MDifferentiableAt.const_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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{z : M}
{f : M → E'}
(hf : MDifferentiableAt I (modelWithCornersSelf 𝕜 E') f z)
(s : 𝕜)
:
MDifferentiableAt I (modelWithCornersSelf 𝕜 E') (s • f) z
theorem
MDifferentiable.const_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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{f : M → E'}
(s : 𝕜)
(hf : MDifferentiable I (modelWithCornersSelf 𝕜 E') f)
:
MDifferentiable I (modelWithCornersSelf 𝕜 E') (s • f)
theorem
const_smul_mfderiv
{𝕜 : 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']
{z : M}
{f : M → E'}
(hf : MDifferentiableAt I (modelWithCornersSelf 𝕜 E') f z)
(s : 𝕜)
:
mfderiv I (modelWithCornersSelf 𝕜 E') (s • f) z = s • mfderiv I (modelWithCornersSelf 𝕜 E') f z
theorem
HasMFDerivAt.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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{z : M}
{f : M → E'}
{f' : TangentSpace I z →L[𝕜] E'}
(hf : HasMFDerivAt I (modelWithCornersSelf 𝕜 E') f z f')
:
HasMFDerivAt I (modelWithCornersSelf 𝕜 E') (-f) z (-f')
theorem
hasMFDerivAt_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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{z : M}
{f : M → E'}
{f' : TangentSpace I z →L[𝕜] E'}
:
HasMFDerivAt I (modelWithCornersSelf 𝕜 E') (-f) z (-f') ↔ HasMFDerivAt I (modelWithCornersSelf 𝕜 E') f z f'
theorem
MDifferentiableAt.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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{z : M}
{f : M → E'}
(hf : MDifferentiableAt I (modelWithCornersSelf 𝕜 E') f z)
:
MDifferentiableAt I (modelWithCornersSelf 𝕜 E') (-f) z
theorem
mdifferentiableAt_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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{z : M}
{f : M → E'}
:
MDifferentiableAt I (modelWithCornersSelf 𝕜 E') (-f) z ↔ MDifferentiableAt I (modelWithCornersSelf 𝕜 E') f z
theorem
MDifferentiable.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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{f : M → E'}
(hf : MDifferentiable I (modelWithCornersSelf 𝕜 E') f)
:
MDifferentiable I (modelWithCornersSelf 𝕜 E') (-f)
theorem
mfderiv_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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
(f : M → E')
(x : M)
:
mfderiv I (modelWithCornersSelf 𝕜 E') (-f) x = -mfderiv I (modelWithCornersSelf 𝕜 E') f x
theorem
HasMFDerivAt.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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{z : M}
{f g : M → E'}
{f' g' : TangentSpace I z →L[𝕜] E'}
(hf : HasMFDerivAt I (modelWithCornersSelf 𝕜 E') f z f')
(hg : HasMFDerivAt I (modelWithCornersSelf 𝕜 E') g z g')
:
HasMFDerivAt I (modelWithCornersSelf 𝕜 E') (f - g) z (f' - g')
theorem
MDifferentiableAt.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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{z : M}
{f g : M → E'}
(hf : MDifferentiableAt I (modelWithCornersSelf 𝕜 E') f z)
(hg : MDifferentiableAt I (modelWithCornersSelf 𝕜 E') g z)
:
MDifferentiableAt I (modelWithCornersSelf 𝕜 E') (f - g) z
theorem
MDifferentiable.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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{f g : M → E'}
(hf : MDifferentiable I (modelWithCornersSelf 𝕜 E') f)
(hg : MDifferentiable I (modelWithCornersSelf 𝕜 E') g)
:
MDifferentiable I (modelWithCornersSelf 𝕜 E') (f - g)
theorem
mfderiv_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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{z : M}
{f g : M → E'}
(hf : MDifferentiableAt I (modelWithCornersSelf 𝕜 E') f z)
(hg : MDifferentiableAt I (modelWithCornersSelf 𝕜 E') g z)
:
mfderiv I (modelWithCornersSelf 𝕜 E') (f - g) z = mfderiv I (modelWithCornersSelf 𝕜 E') f z - mfderiv I (modelWithCornersSelf 𝕜 E') g z
theorem
HasMFDerivWithinAt.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}
{z : M}
{F' : Type u_11}
[NormedRing F']
[NormedAlgebra 𝕜 F']
{p q : M → F'}
{p' q' : TangentSpace I z →L[𝕜] F'}
(hp : HasMFDerivWithinAt I (modelWithCornersSelf 𝕜 F') p s z p')
(hq : HasMFDerivWithinAt I (modelWithCornersSelf 𝕜 F') q s z q')
:
HasMFDerivWithinAt I (modelWithCornersSelf 𝕜 F') (p * q) s z (p z • q' + p'.smulRight (q z))
theorem
HasMFDerivAt.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]
{z : M}
{F' : Type u_11}
[NormedRing F']
[NormedAlgebra 𝕜 F']
{p q : M → F'}
{p' q' : TangentSpace I z →L[𝕜] F'}
(hp : HasMFDerivAt I (modelWithCornersSelf 𝕜 F') p z p')
(hq : HasMFDerivAt I (modelWithCornersSelf 𝕜 F') q z q')
:
HasMFDerivAt I (modelWithCornersSelf 𝕜 F') (p * q) z (p z • q' + p'.smulRight (q z))
theorem
MDifferentiableWithinAt.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}
{z : M}
{F' : Type u_11}
[NormedRing F']
[NormedAlgebra 𝕜 F']
{p q : M → F'}
(hp : MDifferentiableWithinAt I (modelWithCornersSelf 𝕜 F') p s z)
(hq : MDifferentiableWithinAt I (modelWithCornersSelf 𝕜 F') q s z)
:
MDifferentiableWithinAt I (modelWithCornersSelf 𝕜 F') (p * q) s z
theorem
MDifferentiableAt.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]
{z : M}
{F' : Type u_11}
[NormedRing F']
[NormedAlgebra 𝕜 F']
{p q : M → F'}
(hp : MDifferentiableAt I (modelWithCornersSelf 𝕜 F') p z)
(hq : MDifferentiableAt I (modelWithCornersSelf 𝕜 F') q z)
:
MDifferentiableAt I (modelWithCornersSelf 𝕜 F') (p * q) z
theorem
MDifferentiableOn.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' : Type u_11}
[NormedRing F']
[NormedAlgebra 𝕜 F']
{p q : M → F'}
(hp : MDifferentiableOn I (modelWithCornersSelf 𝕜 F') p s)
(hq : MDifferentiableOn I (modelWithCornersSelf 𝕜 F') q s)
:
MDifferentiableOn I (modelWithCornersSelf 𝕜 F') (p * q) s
theorem
MDifferentiable.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' : Type u_11}
[NormedRing F']
[NormedAlgebra 𝕜 F']
{p q : M → F'}
(hp : MDifferentiable I (modelWithCornersSelf 𝕜 F') p)
(hq : MDifferentiable I (modelWithCornersSelf 𝕜 F') q)
:
MDifferentiable I (modelWithCornersSelf 𝕜 F') (p * q)
theorem
HasMFDerivWithinAt.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}
{z : M}
{F' : Type u_11}
[NormedCommRing F']
[NormedAlgebra 𝕜 F']
{p q : M → F'}
{p' q' : TangentSpace I z →L[𝕜] F'}
(hp : HasMFDerivWithinAt I (modelWithCornersSelf 𝕜 F') p s z p')
(hq : HasMFDerivWithinAt I (modelWithCornersSelf 𝕜 F') q s z q')
:
HasMFDerivWithinAt I (modelWithCornersSelf 𝕜 F') (p * q) s z (p z • q' + q z • p')
theorem
HasMFDerivAt.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]
{z : M}
{F' : Type u_11}
[NormedCommRing F']
[NormedAlgebra 𝕜 F']
{p q : M → F'}
{p' q' : TangentSpace I z →L[𝕜] F'}
(hp : HasMFDerivAt I (modelWithCornersSelf 𝕜 F') p z p')
(hq : HasMFDerivAt I (modelWithCornersSelf 𝕜 F') q z q')
:
HasMFDerivAt I (modelWithCornersSelf 𝕜 F') (p * q) z (p z • q' + q z • p')