# 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} {E : Type u_2} [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] (f : E →L[𝕜] E') {s : Set E} {x : E} :
HasMFDerivWithinAt () () (f) s x f
theorem ContinuousLinearMap.hasMFDerivAt {𝕜 : Type u_1} {E : Type u_2} [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] (f : E →L[𝕜] E') {x : E} :
HasMFDerivAt () () (f) x f
theorem ContinuousLinearMap.mdifferentiableWithinAt {𝕜 : Type u_1} {E : Type u_2} [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] (f : E →L[𝕜] E') {s : Set E} {x : E} :
MDifferentiableWithinAt () () (f) s x
theorem ContinuousLinearMap.mdifferentiableOn {𝕜 : Type u_1} {E : Type u_2} [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] (f : E →L[𝕜] E') {s : Set E} :
MDifferentiableOn () () (f) s
theorem ContinuousLinearMap.mdifferentiableAt {𝕜 : Type u_1} {E : Type u_2} [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] (f : E →L[𝕜] E') {x : E} :
MDifferentiableAt () () (f) x
theorem ContinuousLinearMap.mdifferentiable {𝕜 : Type u_1} {E : Type u_2} [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] (f : E →L[𝕜] E') :
MDifferentiable () () f
theorem ContinuousLinearMap.mfderiv_eq {𝕜 : Type u_1} {E : Type u_2} [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] (f : E →L[𝕜] E') {x : E} :
mfderiv () () (f) x = f
theorem ContinuousLinearMap.mfderivWithin_eq {𝕜 : Type u_1} {E : Type u_2} [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] (f : E →L[𝕜] E') {s : Set E} {x : E} (hs : ) :
mfderivWithin () () (f) s x = f
theorem ContinuousLinearEquiv.hasMFDerivWithinAt {𝕜 : Type u_1} {E : Type u_2} [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] (f : E ≃L[𝕜] E') {s : Set E} {x : E} :
HasMFDerivWithinAt () () (f) s x f
theorem ContinuousLinearEquiv.hasMFDerivAt {𝕜 : Type u_1} {E : Type u_2} [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] (f : E ≃L[𝕜] E') {x : E} :
HasMFDerivAt () () (f) x f
theorem ContinuousLinearEquiv.mdifferentiableWithinAt {𝕜 : Type u_1} {E : Type u_2} [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] (f : E ≃L[𝕜] E') {s : Set E} {x : E} :
MDifferentiableWithinAt () () (f) s x
theorem ContinuousLinearEquiv.mdifferentiableOn {𝕜 : Type u_1} {E : Type u_2} [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] (f : E ≃L[𝕜] E') {s : Set E} :
MDifferentiableOn () () (f) s
theorem ContinuousLinearEquiv.mdifferentiableAt {𝕜 : Type u_1} {E : Type u_2} [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] (f : E ≃L[𝕜] E') {x : E} :
MDifferentiableAt () () (f) x
theorem ContinuousLinearEquiv.mdifferentiable {𝕜 : Type u_1} {E : Type u_2} [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] (f : E ≃L[𝕜] E') :
MDifferentiable () () f
theorem ContinuousLinearEquiv.mfderiv_eq {𝕜 : Type u_1} {E : Type u_2} [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] (f : E ≃L[𝕜] E') {x : E} :
mfderiv () () (f) x = f
theorem ContinuousLinearEquiv.mfderivWithin_eq {𝕜 : Type u_1} {E : Type u_2} [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] (f : E ≃L[𝕜] E') {s : Set E} {x : E} (hs : ) :
mfderivWithin () () (f) s x = f

#### Identity #

theorem hasMFDerivAt_id {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] (I : ) {M : Type u_4} [] [] (x : M) :
HasMFDerivAt I I id x ()
theorem hasMFDerivWithinAt_id {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] (I : ) {M : Type u_4} [] [] (s : Set M) (x : M) :
HasMFDerivWithinAt I I id s x ()
theorem mdifferentiableAt_id {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] (I : ) {M : Type u_4} [] [] {x : M} :
theorem mdifferentiableWithinAt_id {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] (I : ) {M : Type u_4} [] [] {s : Set M} {x : M} :
theorem mdifferentiable_id {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] (I : ) {M : Type u_4} [] [] :
theorem mdifferentiableOn_id {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] (I : ) {M : Type u_4} [] [] {s : Set M} :
@[simp]
theorem mfderiv_id {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] (I : ) {M : Type u_4} [] [] {x : M} :
mfderiv I I id x =
theorem mfderivWithin_id {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] (I : ) {M : Type u_4} [] [] {s : Set M} {x : M} (hxs : ) :
mfderivWithin I I id s x =
@[simp]
theorem tangentMap_id {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] (I : ) {M : Type u_4} [] [] :
tangentMap I I id = id
theorem tangentMapWithin_id {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] (I : ) {M : Type u_4} [] [] {s : Set M} {p : } (hs : UniqueMDiffWithinAt I s p.proj) :
tangentMapWithin I I id s p = p

#### Constants #

theorem hasMFDerivAt_const {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] (I : ) {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] (I' : ModelWithCorners 𝕜 E' H') {M' : Type u_7} [] [ChartedSpace H' M'] [] (c : M') (x : M) :
HasMFDerivAt I I' (fun (x : M) => c) x 0
theorem hasMFDerivWithinAt_const {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] (I : ) {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] (I' : ModelWithCorners 𝕜 E' H') {M' : Type u_7} [] [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} {E : Type u_2} [] {H : Type u_3} [] (I : ) {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] (I' : ModelWithCorners 𝕜 E' H') {M' : Type u_7} [] [ChartedSpace H' M'] [] {x : M} {c : M'} :
MDifferentiableAt I I' (fun (x : M) => c) x
theorem mdifferentiableWithinAt_const {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] (I : ) {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] (I' : ModelWithCorners 𝕜 E' H') {M' : Type u_7} [] [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} {E : Type u_2} [] {H : Type u_3} [] (I : ) {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] (I' : ModelWithCorners 𝕜 E' H') {M' : Type u_7} [] [ChartedSpace H' M'] [] {c : M'} :
MDifferentiable I I' fun (x : M) => c
theorem mdifferentiableOn_const {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] (I : ) {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] (I' : ModelWithCorners 𝕜 E' H') {M' : Type u_7} [] [ChartedSpace H' M'] [] {s : Set M} {c : M'} :
MDifferentiableOn I I' (fun (x : M) => c) s
@[simp]
theorem mfderiv_const {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] (I : ) {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] (I' : ModelWithCorners 𝕜 E' H') {M' : Type u_7} [] [ChartedSpace H' M'] [] {x : M} {c : M'} :
mfderiv I I' (fun (x : M) => c) x = 0
theorem mfderivWithin_const {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] (I : ) {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] (I' : ModelWithCorners 𝕜 E' H') {M' : Type u_7} [] [ChartedSpace H' M'] [] {s : Set M} {x : M} {c : M'} (hxs : ) :
mfderivWithin I I' (fun (x : M) => c) s x = 0

### Operations on the product of two manifolds #

theorem hasMFDerivAt_fst {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] (I : ) {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] (I' : ModelWithCorners 𝕜 E' H') {M' : Type u_7} [] [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} {E : Type u_2} [] {H : Type u_3} [] (I : ) {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] (I' : ModelWithCorners 𝕜 E' H') {M' : Type u_7} [] [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} {E : Type u_2} [] {H : Type u_3} [] (I : ) {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] (I' : ModelWithCorners 𝕜 E' H') {M' : Type u_7} [] [ChartedSpace H' M'] [] {x : M × M'} :
MDifferentiableAt (I.prod I') I Prod.fst x
theorem mdifferentiableWithinAt_fst {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] (I : ) {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] (I' : ModelWithCorners 𝕜 E' H') {M' : Type u_7} [] [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} {E : Type u_2} [] {H : Type u_3} [] (I : ) {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] (I' : ModelWithCorners 𝕜 E' H') {M' : Type u_7} [] [ChartedSpace H' M'] [] :
MDifferentiable (I.prod I') I Prod.fst
theorem mdifferentiableOn_fst {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] (I : ) {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] (I' : ModelWithCorners 𝕜 E' H') {M' : Type u_7} [] [ChartedSpace H' M'] [] {s : Set (M × M')} :
MDifferentiableOn (I.prod I') I Prod.fst s
@[simp]
theorem mfderiv_fst {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] (I : ) {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] (I' : ModelWithCorners 𝕜 E' H') {M' : Type u_7} [] [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} {E : Type u_2} [] {H : Type u_3} [] (I : ) {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] (I' : ModelWithCorners 𝕜 E' H') {M' : Type u_7} [] [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} {E : Type u_2} [] {H : Type u_3} [] (I : ) {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] (I' : ModelWithCorners 𝕜 E' H') {M' : Type u_7} [] [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} {E : Type u_2} [] {H : Type u_3} [] (I : ) {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] (I' : ModelWithCorners 𝕜 E' H') {M' : Type u_7} [] [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} {E : Type u_2} [] {H : Type u_3} [] (I : ) {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] (I' : ModelWithCorners 𝕜 E' H') {M' : Type u_7} [] [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} {E : Type u_2} [] {H : Type u_3} [] (I : ) {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] (I' : ModelWithCorners 𝕜 E' H') {M' : Type u_7} [] [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} {E : Type u_2} [] {H : Type u_3} [] (I : ) {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] (I' : ModelWithCorners 𝕜 E' H') {M' : Type u_7} [] [ChartedSpace H' M'] [] {x : M × M'} :
MDifferentiableAt (I.prod I') I' Prod.snd x
theorem mdifferentiableWithinAt_snd {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] (I : ) {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] (I' : ModelWithCorners 𝕜 E' H') {M' : Type u_7} [] [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} {E : Type u_2} [] {H : Type u_3} [] (I : ) {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] (I' : ModelWithCorners 𝕜 E' H') {M' : Type u_7} [] [ChartedSpace H' M'] [] :
MDifferentiable (I.prod I') I' Prod.snd
theorem mdifferentiableOn_snd {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] (I : ) {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] (I' : ModelWithCorners 𝕜 E' H') {M' : Type u_7} [] [ChartedSpace H' M'] [] {s : Set (M × M')} :
MDifferentiableOn (I.prod I') I' Prod.snd s
@[simp]
theorem mfderiv_snd {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] (I : ) {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] (I' : ModelWithCorners 𝕜 E' H') {M' : Type u_7} [] [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} {E : Type u_2} [] {H : Type u_3} [] (I : ) {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] (I' : ModelWithCorners 𝕜 E' H') {M' : Type u_7} [] [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} {E : Type u_2} [] {H : Type u_3} [] (I : ) {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] (I' : ModelWithCorners 𝕜 E' H') {M' : Type u_7} [] [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} {E : Type u_2} [] {H : Type u_3} [] (I : ) {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] (I' : ModelWithCorners 𝕜 E' H') {M' : Type u_7} [] [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} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] [] {E'' : Type u_8} [] [NormedSpace 𝕜 E''] {H'' : Type u_9} [] {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10} [] [ChartedSpace H'' M''] [] {f : MM'} {g : MM''} {x : M} (hf : MDifferentiableAt I I' f x) (hg : MDifferentiableAt I I'' g x) :
mfderiv I (I'.prod I'') (fun (x : M) => (f x, g x)) x = (mfderiv I I' f x).prod (mfderiv I I'' g x)
theorem mfderiv_prod_left {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] (I : ) {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] (I' : ModelWithCorners 𝕜 E' H') {M' : Type u_7} [] [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} {E : Type u_2} [] {H : Type u_3} [] (I : ) {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] (I' : ModelWithCorners 𝕜 E' H') {M' : Type u_7} [] [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} {E : Type u_2} [] {H : Type u_3} [] (I : ) {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] (I' : ModelWithCorners 𝕜 E' H') {M' : Type u_7} [] [ChartedSpace H' M'] [] {E'' : Type u_8} [] [NormedSpace 𝕜 E''] {H'' : Type u_9} [] (I'' : ModelWithCorners 𝕜 E'' H'') {M'' : Type u_10} [] [ChartedSpace H'' M''] [] {f : M × M'M''} {p : M × M'} (hf : MDifferentiableAt (I.prod I') I'' f p) :
mfderiv (I.prod I') I'' f p = let_fun this := mfderiv (I.prod I') I'' (fun (z : M × M') => f (z.1, p.2)) p + mfderiv (I.prod I') I'' (fun (z : M × M') => f (p.1, z.2)) p; this

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} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {z : M} {f : ME'} {g : ME'} {f' : →L[𝕜] E'} {g' : →L[𝕜] E'} (hf : HasMFDerivAt I () f z f') (hg : HasMFDerivAt I () g z g') :
HasMFDerivAt I () (f + g) z (f' + g')
theorem MDifferentiableAt.add {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {z : M} {f : ME'} {g : ME'} (hf : MDifferentiableAt I () f z) (hg : MDifferentiableAt I () g z) :
MDifferentiableAt I () (f + g) z
theorem MDifferentiable.add {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {f : ME'} {g : ME'} (hf : MDifferentiable I () f) (hg : MDifferentiable I () g) :
MDifferentiable I () (f + g)
theorem mfderiv_add {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {z : M} {f : ME'} {g : ME'} (hf : MDifferentiableAt I () f z) (hg : MDifferentiableAt I () g z) :
mfderiv I () (f + g) z = mfderiv I () f z + mfderiv I () g z
theorem HasMFDerivAt.const_smul {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {z : M} {f : ME'} {f' : →L[𝕜] E'} (hf : HasMFDerivAt I () f z f') (s : 𝕜) :
HasMFDerivAt I () (s f) z (s f')
theorem MDifferentiableAt.const_smul {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {z : M} {f : ME'} (hf : MDifferentiableAt I () f z) (s : 𝕜) :
MDifferentiableAt I () (s f) z
theorem MDifferentiable.const_smul {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {f : ME'} (s : 𝕜) (hf : MDifferentiable I () f) :
MDifferentiable I () (s f)
theorem const_smul_mfderiv {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {z : M} {f : ME'} (hf : MDifferentiableAt I () f z) (s : 𝕜) :
mfderiv I () (s f) z = s mfderiv I () f z
theorem HasMFDerivAt.neg {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {z : M} {f : ME'} {f' : →L[𝕜] E'} (hf : HasMFDerivAt I () f z f') :
HasMFDerivAt I () (-f) z (-f')
theorem hasMFDerivAt_neg {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {z : M} {f : ME'} {f' : →L[𝕜] E'} :
HasMFDerivAt I () (-f) z (-f') HasMFDerivAt I () f z f'
theorem MDifferentiableAt.neg {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {z : M} {f : ME'} (hf : MDifferentiableAt I () f z) :
theorem mdifferentiableAt_neg {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {z : M} {f : ME'} :
theorem MDifferentiable.neg {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {f : ME'} (hf : MDifferentiable I () f) :
theorem mfderiv_neg {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] (f : ME') (x : M) :
mfderiv I () (-f) x = -mfderiv I () f x
theorem HasMFDerivAt.sub {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {z : M} {f : ME'} {g : ME'} {f' : →L[𝕜] E'} {g' : →L[𝕜] E'} (hf : HasMFDerivAt I () f z f') (hg : HasMFDerivAt I () g z g') :
HasMFDerivAt I () (f - g) z (f' - g')
theorem MDifferentiableAt.sub {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {z : M} {f : ME'} {g : ME'} (hf : MDifferentiableAt I () f z) (hg : MDifferentiableAt I () g z) :
MDifferentiableAt I () (f - g) z
theorem MDifferentiable.sub {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {f : ME'} {g : ME'} (hf : MDifferentiable I () f) (hg : MDifferentiable I () g) :
MDifferentiable I () (f - g)
theorem mfderiv_sub {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {z : M} {f : ME'} {g : ME'} (hf : MDifferentiableAt I () f z) (hg : MDifferentiableAt I () g z) :
mfderiv I () (f - g) z = mfderiv I () f z - mfderiv I () g z
theorem HasMFDerivWithinAt.mul' {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {s : Set M} {z : M} {F' : Type u_11} [] [] {p : MF'} {q : MF'} {p' : →L[𝕜] F'} {q' : →L[𝕜] F'} (hp : HasMFDerivWithinAt I () p s z p') (hq : HasMFDerivWithinAt I () q s z q') :
HasMFDerivWithinAt I () (p * q) s z (p z q' + p'.smulRight (q z))
theorem HasMFDerivAt.mul' {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {z : M} {F' : Type u_11} [] [] {p : MF'} {q : MF'} {p' : →L[𝕜] F'} {q' : →L[𝕜] F'} (hp : HasMFDerivAt I () p z p') (hq : HasMFDerivAt I () q z q') :
HasMFDerivAt I () (p * q) z (p z q' + p'.smulRight (q z))
theorem MDifferentiableWithinAt.mul {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {s : Set M} {z : M} {F' : Type u_11} [] [] {p : MF'} {q : MF'} (hp : MDifferentiableWithinAt I () p s z) (hq : MDifferentiableWithinAt I () q s z) :
MDifferentiableWithinAt I () (p * q) s z
theorem MDifferentiableAt.mul {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {z : M} {F' : Type u_11} [] [] {p : MF'} {q : MF'} (hp : MDifferentiableAt I () p z) (hq : MDifferentiableAt I () q z) :
MDifferentiableAt I () (p * q) z
theorem MDifferentiableOn.mul {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {s : Set M} {F' : Type u_11} [] [] {p : MF'} {q : MF'} (hp : MDifferentiableOn I () p s) (hq : MDifferentiableOn I () q s) :
MDifferentiableOn I () (p * q) s
theorem MDifferentiable.mul {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {F' : Type u_11} [] [] {p : MF'} {q : MF'} (hp : MDifferentiable I () p) (hq : MDifferentiable I () q) :
MDifferentiable I () (p * q)
theorem HasMFDerivWithinAt.mul {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {s : Set M} {z : M} {F' : Type u_11} [] [] {p : MF'} {q : MF'} {p' : →L[𝕜] F'} {q' : →L[𝕜] F'} (hp : HasMFDerivWithinAt I () p s z p') (hq : HasMFDerivWithinAt I () q s z q') :
HasMFDerivWithinAt I () (p * q) s z (p z q' + q z p')
theorem HasMFDerivAt.mul {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {z : M} {F' : Type u_11} [] [] {p : MF'} {q : MF'} {p' : →L[𝕜] F'} {q' : →L[𝕜] F'} (hp : HasMFDerivAt I () p z p') (hq : HasMFDerivAt I () q z q') :
HasMFDerivAt I () (p * q) z (p z q' + q z p')