# Documentation

Mathlib.Geometry.Manifold.MFDeriv

# The derivative of functions between smooth manifolds #

Let M and M' be two smooth manifolds with corners over a field π (with respective models with corners I on (E, H) and I' on (E', H')), and let f : M β M'. We define the derivative of the function at a point, within a set or along the whole space, mimicking the API for (FrΓ©chet) derivatives. It is denoted by mfderiv I I' f x, where "m" stands for "manifold" and "f" for "FrΓ©chet" (as in the usual derivative fderiv π f x).

## Main definitions #

• UniqueMDiffOn I s : predicate saying that, at each point of the set s, a function can have at most one derivative. This technical condition is important when we define mfderivWithin below, as otherwise there is an arbitrary choice in the derivative, and many properties will fail (for instance the chain rule). This is analogous to UniqueDiffOn π s in a vector space.

Let f be a map between smooth manifolds. The following definitions follow the fderiv API.

• mfderiv I I' f x : the derivative of f at x, as a continuous linear map from the tangent space at x to the tangent space at f x. If the map is not differentiable, this is 0.
• mfderivWithin I I' f s x : the derivative of f at x within s, as a continuous linear map from the tangent space at x to the tangent space at f x. If the map is not differentiable within s, this is 0.
• MDifferentiableAt I I' f x : Prop expressing whether f is differentiable at x.
• MDifferentiableWithinAt π f s x : Prop expressing whether f is differentiable within s at x.
• HasMFDerivAt I I' f s x f' : Prop expressing whether f has f' as a derivative at x.
• HasMFDerivWithinAt I I' f s x f' : Prop expressing whether f has f' as a derivative within s at x.
• MDifferentiableOn I I' f s : Prop expressing that f is differentiable on the set s.
• MDifferentiable I I' f : Prop expressing that f is differentiable everywhere.
• tangentMap I I' f : the derivative of f, as a map from the tangent bundle of M to the tangent bundle of M'.

We also establish results on the differential of the identity, constant functions, charts, extended charts. For functions between vector spaces, we show that the usual notions and the manifold notions coincide.

## Implementation notes #

The tangent bundle is constructed using the machinery of topological fiber bundles, for which one can define bundled morphisms and construct canonically maps from the total space of one bundle to the total space of another one. One could use this mechanism to construct directly the derivative of a smooth map. However, we want to define the derivative of any map (and let it be zero if the map is not differentiable) to avoid proof arguments everywhere. This means we have to go back to the details of the definition of the total space of a fiber bundle constructed from core, to cook up a suitable definition of the derivative. It is the following: at each point, we have a preferred chart (used to identify the fiber above the point with the model vector space in fiber bundles). Then one should read the function using these preferred charts at x and f x, and take the derivative of f in these charts.

Due to the fact that we are working in a model with corners, with an additional embedding I of the model space H in the model vector space E, the charts taking values in E are not the original charts of the manifold, but those ones composed with I, called extended charts. We define writtenInExtChartAt I I' x f for the function f written in the preferred extended charts. Then the manifold derivative of f, at x, is just the usual derivative of writtenInExtChartAt I I' x f, at the point (extChartAt I x) x.

There is a subtelty with respect to continuity: if the function is not continuous, then the image of a small open set around x will not be contained in the source of the preferred chart around f x, which means that when reading f in the chart one is losing some information. To avoid this, we include continuity in the definition of differentiablity (which is reasonable since with any definition, differentiability implies continuity).

Warning: the derivative (even within a subset) is a linear map on the whole tangent space. Suppose that one is given a smooth submanifold N, and a function which is smooth on N (i.e., its restriction to the subtype N is smooth). Then, in the whole manifold M, the property MDifferentiableOn I I' f N holds. However, mfderivWithin I I' f N is not uniquely defined (what values would one choose for vectors that are transverse to N?), which can create issues down the road. The problem here is that knowing the value of f along N does not determine the differential of f in all directions. This is in contrast to the case where N would be an open subset, or a submanifold with boundary of maximal dimension, where this issue does not appear. The predicate UniqueMDiffOn I N indicates that the derivative along N is unique if it exists, and is an assumption in most statements requiring a form of uniqueness.

On a vector space, the manifold derivative and the usual derivative are equal. This means in particular that they live on the same space, i.e., the tangent space is defeq to the original vector space. To get this property is a motivation for our definition of the tangent space as a single copy of the vector space, instead of more usual definitions such as the space of derivations, or the space of equivalence classes of smooth curves in the manifold.

## Tags #

Derivative, manifold

### Derivative of maps between manifolds #

The derivative of a smooth map f between smooth manifold M and M' at x is a bounded linear map from the tangent space to M at x, to the tangent space to M' at f x. Since we defined the tangent space using one specific chart, the formula for the derivative is written in terms of this specific chart.

We use the names MDifferentiable and mfderiv, where the prefix letter m means "manifold".

def DifferentiableWithinAtProp {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] (I : ModelWithCorners π E H) {E' : Type u_5} [] [NormedSpace π E'] {H' : Type u_6} [] (I' : ModelWithCorners π E' H') (f : H β H') (s : Set H) (x : H) :

Property in the model space of a model with corners of being differentiable within at set at a point, when read in the model vector space. This property will be lifted to manifolds to define differentiable functions between manifolds.

Instances For
theorem differentiable_within_at_localInvariantProp {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] (I : ModelWithCorners π E H) {E' : Type u_5} [] [NormedSpace π E'] {H' : Type u_6} [] (I' : ModelWithCorners π E' H') :

Being differentiable in the model space is a local property, invariant under smooth maps. Therefore, it will lift nicely to manifolds.

def UniqueMDiffWithinAt {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] (I : ModelWithCorners π E H) {M : Type u_4} [] [] (s : Set M) (x : M) :

Predicate ensuring that, at a point and within a set, a function can have at most one derivative. This is expressed using the preferred chart at the considered point.

Instances For
def UniqueMDiffOn {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] (I : ModelWithCorners π E H) {M : Type u_4} [] [] (s : Set M) :

Predicate ensuring that, at all points of a set, a function can have at most one derivative.

Instances For
def MDifferentiableWithinAt {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] (I : ModelWithCorners π E H) {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'] (f : M β M') (s : Set M) (x : M) :

MDifferentiableWithinAt I I' f s x indicates that the function f between manifolds has a derivative at the point x within the set s. This is a generalization of DifferentiableWithinAt to manifolds.

We require continuity in the definition, as otherwise points close to x in s could be sent by f outside of the chart domain around f x. Then the chart could do anything to the image points, and in particular by coincidence writtenInExtChartAt I I' x f could be differentiable, while this would not mean anything relevant.

Instances For
theorem mdifferentiableWithinAt_iff_liftPropWithinAt {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] (I : ModelWithCorners π E H) {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'] (f : M β M') (s : Set M) (x : M) :
def MDifferentiableAt {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] (I : ModelWithCorners π E H) {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'] (f : M β M') (x : M) :

MDifferentiableAt I I' f x indicates that the function f between manifolds has a derivative at the point x. This is a generalization of DifferentiableAt to manifolds.

We require continuity in the definition, as otherwise points close to x could be sent by f outside of the chart domain around f x. Then the chart could do anything to the image points, and in particular by coincidence writtenInExtChartAt I I' x f could be differentiable, while this would not mean anything relevant.

Instances For
theorem mdifferentiableAt_iff_liftPropAt {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] (I : ModelWithCorners π E H) {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'] (f : M β M') (x : M) :
def MDifferentiableOn {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] (I : ModelWithCorners π E H) {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'] (f : M β M') (s : Set M) :

MDifferentiableOn I I' f s indicates that the function f between manifolds has a derivative within s at all points of s. This is a generalization of DifferentiableOn to manifolds.

Instances For
def MDifferentiable {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] (I : ModelWithCorners π E H) {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'] (f : M β M') :

MDifferentiable I I' f indicates that the function f between manifolds has a derivative everywhere. This is a generalization of Differentiable to manifolds.

Instances For
def LocalHomeomorph.MDifferentiable {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] (I : ModelWithCorners π E H) {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'] (f : ) :

Prop registering if a local homeomorphism is a local diffeomorphism on its source

Instances For
def HasMFDerivWithinAt {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] (I : ModelWithCorners π E H) {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'] [] (f : M β M') (s : Set M) (x : M) (f' : βL[π] TangentSpace I' (f x)) :

HasMFDerivWithinAt I I' f s x f' indicates that the function f between manifolds has, at the point x and within the set s, the derivative f'. Here, f' is a continuous linear map from the tangent space at x to the tangent space at f x.

This is a generalization of HasFDerivWithinAt to manifolds (as indicated by the prefix m). The order of arguments is changed as the type of the derivative f' depends on the choice of x.

We require continuity in the definition, as otherwise points close to x in s could be sent by f outside of the chart domain around f x. Then the chart could do anything to the image points, and in particular by coincidence writtenInExtChartAt I I' x f could be differentiable, while this would not mean anything relevant.

Instances For
def HasMFDerivAt {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] (I : ModelWithCorners π E H) {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'] [] (f : M β M') (x : M) (f' : βL[π] TangentSpace I' (f x)) :

HasMFDerivAt I I' f x f' indicates that the function f between manifolds has, at the point x, the derivative f'. Here, f' is a continuous linear map from the tangent space at x to the tangent space at f x.

We require continuity in the definition, as otherwise points close to x s could be sent by f outside of the chart domain around f x. Then the chart could do anything to the image points, and in particular by coincidence writtenInExtChartAt I I' x f could be differentiable, while this would not mean anything relevant.

Instances For
def mfderivWithin {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] (I : ModelWithCorners π E H) {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'] [] (f : M β M') (s : Set M) (x : M) :
βL[π] TangentSpace I' (f x)

Let f be a function between two smooth manifolds. Then mfderivWithin I I' f s x is the derivative of f at x within s, as a continuous linear map from the tangent space at x to the tangent space at f x.

Instances For
def mfderiv {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] (I : ModelWithCorners π E H) {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'] [] (f : M β M') (x : M) :
βL[π] TangentSpace I' (f x)

Let f be a function between two smooth manifolds. Then mfderiv I I' f x is the derivative of f at x, as a continuous linear map from the tangent space at x to the tangent space at f x.

Instances For
def tangentMapWithin {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] (I : ModelWithCorners π E H) {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'] [] (f : M β M') (s : Set M) :
β TangentBundle I' M'

The derivative within a set, as a map between the tangent bundles

Instances For
def tangentMap {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] (I : ModelWithCorners π E H) {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'] [] (f : M β M') :
β TangentBundle I' M'

The derivative, as a map between the tangent bundles

Instances For

### Unique differentiability sets in manifolds #

theorem uniqueMDiffWithinAt_univ {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] (I : ModelWithCorners π E H) {M : Type u_4} [] [] {x : M} :
UniqueMDiffWithinAt I Set.univ x
theorem uniqueMDiffWithinAt_iff {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {M : Type u_4} [] [] {s : Set M} {x : M} :
β UniqueDiffWithinAt π (β() β»ΒΉ' s β© ().target) (β() x)
theorem UniqueMDiffWithinAt.mono_nhds {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {M : Type u_4} [] [] {s : Set M} {t : Set M} {x : M} (hs : ) (ht : β€ ) :
theorem UniqueMDiffWithinAt.mono_of_mem {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {M : Type u_4} [] [] {s : Set M} {t : Set M} {x : M} (hs : ) (ht : t β ) :
theorem UniqueMDiffWithinAt.mono {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {M : Type u_4} [] [] {x : M} {s : Set M} {t : Set M} (h : ) (st : s β t) :
theorem UniqueMDiffWithinAt.inter' {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {M : Type u_4} [] [] {x : M} {s : Set M} {t : Set M} (hs : ) (ht : t β ) :
theorem UniqueMDiffWithinAt.inter {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {M : Type u_4} [] [] {x : M} {s : Set M} {t : Set M} (hs : ) (ht : t β nhds x) :
theorem IsOpen.uniqueMDiffWithinAt {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {M : Type u_4} [] [] {x : M} {s : Set M} (xs : x β s) (hs : ) :
theorem UniqueMDiffOn.inter {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {M : Type u_4} [] [] {s : Set M} {t : Set M} (hs : ) (ht : ) :
theorem IsOpen.uniqueMDiffOn {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {M : Type u_4} [] [] {s : Set M} (hs : ) :
theorem uniqueMDiffOn_univ {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {M : Type u_4} [] [] :
UniqueMDiffOn I Set.univ
theorem UniqueMDiffWithinAt.eq {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {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'] {f : M β M'} {x : M} {s : Set M} [Is : ] [I's : ] {f' : βL[π] TangentSpace I' (f x)} {fβ' : βL[π] TangentSpace I' (f x)} (U : ) (h : HasMFDerivWithinAt I I' f s x f') (hβ : HasMFDerivWithinAt I I' f s x fβ') :
f' = fβ'

UniqueMDiffWithinAt achieves its goal: it implies the uniqueness of the derivative.

theorem UniqueMDiffOn.eq {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {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'] {f : M β M'} {x : M} {s : Set M} [Is : ] [I's : ] {f' : βL[π] TangentSpace I' (f x)} {fβ' : βL[π] TangentSpace I' (f x)} (U : ) (hx : x β s) (h : HasMFDerivWithinAt I I' f s x f') (hβ : HasMFDerivWithinAt I I' f s x fβ') :
f' = fβ'
theorem UniqueMDiffWithinAt.prod {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {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'} {s : Set M} {t : Set M'} (hs : ) (ht : ) :
theorem UniqueMDiffOn.prod {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {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} {t : Set M'} (hs : ) (ht : ) :

### General lemmas on derivatives of functions between manifolds #

We mimick the API for functions between vector spaces

theorem mdifferentiableWithinAt_iff {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {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'] {f : M β M'} {s : Set M} {x : M} :
MDifferentiableWithinAt I I' f s x β β§ DifferentiableWithinAt π (writtenInExtChartAt I I' x f) (().target β© β() β»ΒΉ' s) (β() x)
theorem mdifferentiableWithinAt_iff_of_mem_source {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {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'] {f : M β M'} {x : M} {s : Set M} [Is : ] [I's : ] {x' : M} {y : M'} (hx : x' β (chartAt H x).toLocalEquiv.source) (hy : f x' β (chartAt H' y).toLocalEquiv.source) :
MDifferentiableWithinAt I I' f s x' β β§ DifferentiableWithinAt π (β(extChartAt I' y) β f β β()) (β() β»ΒΉ' s β© Set.range βI) (β() x')

One can reformulate differentiability within a set at a point as continuity within this set at this point, and differentiability in any chart containing that point.

theorem mfderivWithin_zero_of_not_mdifferentiableWithinAt {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {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'] {f : M β M'} {x : M} {s : Set M} [Is : ] [I's : ] (h : Β¬MDifferentiableWithinAt I I' f s x) :
mfderivWithin I I' f s x = 0
theorem mfderiv_zero_of_not_mdifferentiableAt {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {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'] {f : M β M'} {x : M} [Is : ] [I's : ] (h : Β¬MDifferentiableAt I I' f x) :
mfderiv I I' f x = 0
theorem HasMFDerivWithinAt.mono {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {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'] {f : M β M'} {x : M} {s : Set M} {t : Set M} [Is : ] [I's : ] {f' : βL[π] TangentSpace I' (f x)} (h : HasMFDerivWithinAt I I' f t x f') (hst : s β t) :
HasMFDerivWithinAt I I' f s x f'
theorem HasMFDerivAt.hasMFDerivWithinAt {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {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'] {f : M β M'} {x : M} {s : Set M} [Is : ] [I's : ] {f' : βL[π] TangentSpace I' (f x)} (h : HasMFDerivAt I I' f x f') :
HasMFDerivWithinAt I I' f s x f'
theorem HasMFDerivWithinAt.mdifferentiableWithinAt {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {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'] {f : M β M'} {x : M} {s : Set M} [Is : ] [I's : ] {f' : βL[π] TangentSpace I' (f x)} (h : HasMFDerivWithinAt I I' f s x f') :
theorem HasMFDerivAt.mdifferentiableAt {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {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'] {f : M β M'} {x : M} [Is : ] [I's : ] {f' : βL[π] TangentSpace I' (f x)} (h : HasMFDerivAt I I' f x f') :
@[simp]
theorem hasMFDerivWithinAt_univ {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {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'] {f : M β M'} {x : M} [Is : ] [I's : ] {f' : βL[π] TangentSpace I' (f x)} :
HasMFDerivWithinAt I I' f Set.univ x f' β HasMFDerivAt I I' f x f'
theorem hasMFDerivAt_unique {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {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'] {f : M β M'} {x : M} [Is : ] [I's : ] {fβ' : βL[π] TangentSpace I' (f x)} {fβ' : βL[π] TangentSpace I' (f x)} (hβ : HasMFDerivAt I I' f x fβ') (hβ : HasMFDerivAt I I' f x fβ') :
fβ' = fβ'
theorem hasMFDerivWithinAt_inter' {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {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'] {f : M β M'} {x : M} {s : Set M} {t : Set M} [Is : ] [I's : ] {f' : βL[π] TangentSpace I' (f x)} (h : t β ) :
HasMFDerivWithinAt I I' f (s β© t) x f' β HasMFDerivWithinAt I I' f s x f'
theorem hasMFDerivWithinAt_inter {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {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'] {f : M β M'} {x : M} {s : Set M} {t : Set M} [Is : ] [I's : ] {f' : βL[π] TangentSpace I' (f x)} (h : t β nhds x) :
HasMFDerivWithinAt I I' f (s β© t) x f' β HasMFDerivWithinAt I I' f s x f'
theorem HasMFDerivWithinAt.union {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {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'] {f : M β M'} {x : M} {s : Set M} {t : Set M} [Is : ] [I's : ] {f' : βL[π] TangentSpace I' (f x)} (hs : HasMFDerivWithinAt I I' f s x f') (ht : HasMFDerivWithinAt I I' f t x f') :
HasMFDerivWithinAt I I' f (s βͺ t) x f'
theorem HasMFDerivWithinAt.mono_of_mem {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {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'] {f : M β M'} {x : M} {s : Set M} {t : Set M} [Is : ] [I's : ] {f' : βL[π] TangentSpace I' (f x)} (h : HasMFDerivWithinAt I I' f s x f') (ht : s β ) :
HasMFDerivWithinAt I I' f t x f'
theorem HasMFDerivWithinAt.hasMFDerivAt {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {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'] {f : M β M'} {x : M} {s : Set M} [Is : ] [I's : ] {f' : βL[π] TangentSpace I' (f x)} (h : HasMFDerivWithinAt I I' f s x f') (hs : s β nhds x) :
HasMFDerivAt I I' f x f'
theorem MDifferentiableWithinAt.hasMFDerivWithinAt {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {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'] {f : M β M'} {x : M} {s : Set M} [Is : ] [I's : ] (h : MDifferentiableWithinAt I I' f s x) :
HasMFDerivWithinAt I I' f s x (mfderivWithin I I' f s x)
theorem MDifferentiableWithinAt.mfderivWithin {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {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'] {f : M β M'} {x : M} {s : Set M} [Is : ] [I's : ] (h : MDifferentiableWithinAt I I' f s x) :
mfderivWithin I I' f s x = fderivWithin π (writtenInExtChartAt I I' x f) (β() β»ΒΉ' s β© Set.range βI) (β() x)
theorem MDifferentiableAt.hasMFDerivAt {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {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'] {f : M β M'} {x : M} [Is : ] [I's : ] (h : MDifferentiableAt I I' f x) :
HasMFDerivAt I I' f x (mfderiv I I' f x)
theorem MDifferentiableAt.mfderiv {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {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'] {f : M β M'} {x : M} [Is : ] [I's : ] (h : MDifferentiableAt I I' f x) :
mfderiv I I' f x = fderivWithin π (writtenInExtChartAt I I' x f) (Set.range βI) (β() x)
theorem HasMFDerivAt.mfderiv {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {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'] {f : M β M'} {x : M} [Is : ] [I's : ] {f' : βL[π] TangentSpace I' (f x)} (h : HasMFDerivAt I I' f x f') :
mfderiv I I' f x = f'
theorem HasMFDerivWithinAt.mfderivWithin {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {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'] {f : M β M'} {x : M} {s : Set M} [Is : ] [I's : ] {f' : βL[π] TangentSpace I' (f x)} (h : HasMFDerivWithinAt I I' f s x f') (hxs : ) :
mfderivWithin I I' f s x = f'
theorem MDifferentiable.mfderivWithin {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {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'] {f : M β M'} {x : M} {s : Set M} [Is : ] [I's : ] (h : MDifferentiableAt I I' f x) (hxs : ) :
mfderivWithin I I' f s x = mfderiv I I' f x
theorem mfderivWithin_subset {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {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'] {f : M β M'} {x : M} {s : Set M} {t : Set M} [Is : ] [I's : ] (st : s β t) (hs : ) (h : MDifferentiableWithinAt I I' f t x) :
mfderivWithin I I' f s x = mfderivWithin I I' f t x
theorem MDifferentiableWithinAt.mono {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {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'] {f : M β M'} {x : M} {s : Set M} {t : Set M} (hst : s β t) (h : MDifferentiableWithinAt I I' f t x) :
theorem mdifferentiableWithinAt_univ {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {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'] {f : M β M'} {x : M} :
theorem mdifferentiableWithinAt_inter {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {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'] {f : M β M'} {x : M} {s : Set M} {t : Set M} (ht : t β nhds x) :
theorem mdifferentiableWithinAt_inter' {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {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'] {f : M β M'} {x : M} {s : Set M} {t : Set M} (ht : t β ) :
theorem MDifferentiableAt.mdifferentiableWithinAt {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {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'] {f : M β M'} {x : M} {s : Set M} (h : MDifferentiableAt I I' f x) :
theorem MDifferentiableWithinAt.mdifferentiableAt {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {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'] {f : M β M'} {x : M} {s : Set M} (h : MDifferentiableWithinAt I I' f s x) (hs : s β nhds x) :
theorem MDifferentiableOn.mdifferentiableAt {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {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'] {f : M β M'} {x : M} {s : Set M} (h : MDifferentiableOn I I' f s) (hx : s β nhds x) :
theorem MDifferentiableOn.mono {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {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'] {f : M β M'} {s : Set M} {t : Set M} (h : MDifferentiableOn I I' f t) (st : s β t) :
theorem mdifferentiableOn_univ {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {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'] {f : M β M'} :
theorem MDifferentiable.mdifferentiableOn {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {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'] {f : M β M'} {s : Set M} (h : MDifferentiable I I' f) :
theorem mdifferentiableOn_of_locally_mdifferentiableOn {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {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'] {f : M β M'} {s : Set M} (h : β (x : M), x β s β β u, β§ x β u β§ MDifferentiableOn I I' f (s β© u)) :
@[simp]
theorem mfderivWithin_univ {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {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'] {f : M β M'} [Is : ] [I's : ] :
mfderivWithin I I' f Set.univ = mfderiv I I' f
theorem mfderivWithin_inter {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {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'] {f : M β M'} {x : M} {s : Set M} {t : Set M} [Is : ] [I's : ] (ht : t β nhds x) :
mfderivWithin I I' f (s β© t) x = mfderivWithin I I' f s x
theorem mdifferentiableAt_iff_of_mem_source {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {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'] {f : M β M'} {x : M} [Is : ] [I's : ] {x' : M} {y : M'} (hx : x' β (chartAt H x).toLocalEquiv.source) (hy : f x' β (chartAt H' y).toLocalEquiv.source) :
MDifferentiableAt I I' f x' β ContinuousAt f x' β§ DifferentiableWithinAt π (β(extChartAt I' y) β f β β()) (Set.range βI) (β() x')

### Deducing differentiability from smoothness #

theorem ContMDiffWithinAt.mdifferentiableWithinAt {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {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'] {f : M β M'} {x : M} {s : Set M} {n : ββ} (hf : ContMDiffWithinAt I I' n f s x) (hn : 1 β€ n) :
theorem ContMDiffAt.mdifferentiableAt {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {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'] {f : M β M'} {x : M} {n : ββ} (hf : ContMDiffAt I I' n f x) (hn : 1 β€ n) :
theorem ContMDiffOn.mdifferentiableOn {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {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'] {f : M β M'} {s : Set M} {n : ββ} (hf : ContMDiffOn I I' n f s) (hn : 1 β€ n) :
theorem ContMDiff.mdifferentiable {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {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'] {f : M β M'} {n : ββ} (hf : ContMDiff I I' n f) (hn : 1 β€ n) :
theorem SmoothWithinAt.mdifferentiableWithinAt {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {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'] {f : M β M'} {x : M} {s : Set M} (hf : SmoothWithinAt I I' f s x) :
theorem SmoothAt.mdifferentiableAt {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {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'] {f : M β M'} {x : M} (hf : SmoothAt I I' f x) :
theorem SmoothOn.mdifferentiableOn {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {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'] {f : M β M'} {s : Set M} (hf : SmoothOn I I' f s) :
theorem Smooth.mdifferentiable {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {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'] {f : M β M'} (hf : Smooth I I' f) :
theorem Smooth.mdifferentiableAt {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {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'] {f : M β M'} {x : M} (hf : Smooth I I' f) :
theorem Smooth.mdifferentiableWithinAt {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {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'] {f : M β M'} {x : M} {s : Set M} (hf : Smooth I I' f) :

### Deriving continuity from differentiability on manifolds #

theorem HasMFDerivWithinAt.continuousWithinAt {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {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'] {f : M β M'} {x : M} {s : Set M} [Is : ] [I's : ] {f' : βL[π] TangentSpace I' (f x)} (h : HasMFDerivWithinAt I I' f s x f') :
theorem HasMFDerivAt.continuousAt {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {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'] {f : M β M'} {x : M} [Is : ] [I's : ] {f' : βL[π] TangentSpace I' (f x)} (h : HasMFDerivAt I I' f x f') :
theorem MDifferentiableWithinAt.continuousWithinAt {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {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'] {f : M β M'} {x : M} {s : Set M} (h : MDifferentiableWithinAt I I' f s x) :
theorem MDifferentiableAt.continuousAt {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {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'] {f : M β M'} {x : M} (h : MDifferentiableAt I I' f x) :
theorem MDifferentiableOn.continuousOn {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {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'] {f : M β M'} {s : Set M} (h : MDifferentiableOn I I' f s) :
theorem MDifferentiable.continuous {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {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'] {f : M β M'} (h : MDifferentiable I I' f) :
theorem tangentMapWithin_subset {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {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'] {f : M β M'} {s : Set M} {t : Set M} [Is : ] [I's : ] {p : } (st : s β t) (hs : UniqueMDiffWithinAt I s p.proj) (h : MDifferentiableWithinAt I I' f t p.proj) :
tangentMapWithin I I' f s p = tangentMapWithin I I' f t p
theorem tangentMapWithin_univ {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {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'] {f : M β M'} [Is : ] [I's : ] :
tangentMapWithin I I' f Set.univ = tangentMap I I' f
theorem tangentMapWithin_eq_tangentMap {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {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'] {f : M β M'} {s : Set M} [Is : ] [I's : ] {p : } (hs : UniqueMDiffWithinAt I s p.proj) (h : MDifferentiableAt I I' f p.proj) :
tangentMapWithin I I' f s p = tangentMap I I' f p
@[simp]
theorem tangentMapWithin_proj {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {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'] {f : M β M'} {s : Set M} [Is : ] [I's : ] {p : } :
(tangentMapWithin I I' f s p).proj = f p.proj
@[simp]
theorem tangentMap_proj {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {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'] {f : M β M'} [Is : ] [I's : ] {p : } :
(tangentMap I I' f p).proj = f p.proj
theorem MDifferentiableWithinAt.prod_mk {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {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''] {x : M} {s : Set M} {f : M β M'} {g : M β M''} (hf : MDifferentiableWithinAt I I' f s x) (hg : MDifferentiableWithinAt I I'' g s x) :
MDifferentiableWithinAt I () (fun x => (f x, g x)) s x
theorem MDifferentiableAt.prod_mk {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {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''] {x : M} {f : M β M'} {g : M β M''} (hf : MDifferentiableAt I I' f x) (hg : MDifferentiableAt I I'' g x) :
MDifferentiableAt I () (fun x => (f x, g x)) x
theorem MDifferentiableOn.prod_mk {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {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''] {s : Set M} {f : M β M'} {g : M β M''} (hf : MDifferentiableOn I I' f s) (hg : MDifferentiableOn I I'' g s) :
MDifferentiableOn I () (fun x => (f x, g x)) s
theorem MDifferentiable.prod_mk {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {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'} {g : M β M''} (hf : MDifferentiable I I' f) (hg : MDifferentiable I I'' g) :
MDifferentiable I () fun x => (f x, g x)
theorem MDifferentiableWithinAt.prod_mk_space {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace π E'] {E'' : Type u_8} [] [NormedSpace π E''] {x : M} {s : Set M} {f : M β E'} {g : M β E''} (hf : MDifferentiableWithinAt I (modelWithCornersSelf π E') f s x) (hg : MDifferentiableWithinAt I (modelWithCornersSelf π E'') g s x) :
MDifferentiableWithinAt I (modelWithCornersSelf π (E' Γ E'')) (fun x => (f x, g x)) s x
theorem MDifferentiableAt.prod_mk_space {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace π E'] {E'' : Type u_8} [] [NormedSpace π E''] {x : M} {f : M β E'} {g : M β E''} (hf : MDifferentiableAt I (modelWithCornersSelf π E') f x) (hg : MDifferentiableAt I (modelWithCornersSelf π E'') g x) :
MDifferentiableAt I (modelWithCornersSelf π (E' Γ E'')) (fun x => (f x, g x)) x
theorem MDifferentiableOn.prod_mk_space {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace π E'] {E'' : Type u_8} [] [NormedSpace π E''] {s : Set M} {f : M β E'} {g : M β E''} (hf : MDifferentiableOn I (modelWithCornersSelf π E') f s) (hg : MDifferentiableOn I (modelWithCornersSelf π E'') g s) :
MDifferentiableOn I (modelWithCornersSelf π (E' Γ E'')) (fun x => (f x, g x)) s
theorem MDifferentiable.prod_mk_space {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace π E'] {E'' : Type u_8} [] [NormedSpace π E''] {f : M β E'} {g : M β E''} (hf : MDifferentiable I (modelWithCornersSelf π E') f) (hg : MDifferentiable I (modelWithCornersSelf π E'') g) :
MDifferentiable I (modelWithCornersSelf π (E' Γ E'')) fun x => (f x, g x)

### Congruence lemmas for derivatives on manifolds #

theorem HasMFDerivWithinAt.congr_of_eventuallyEq {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {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'] {f : M β M'} {fβ : M β M'} {x : M} {s : Set M} [Is : ] [I's : ] {f' : βL[π] TangentSpace I' (f x)} (h : HasMFDerivWithinAt I I' f s x f') (hβ : fβ =αΆ [] f) (hx : fβ x = f x) :
HasMFDerivWithinAt I I' fβ s x f'
theorem HasMFDerivWithinAt.congr_mono {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {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'] {f : M β M'} {fβ : M β M'} {x : M} {s : Set M} {t : Set M} [Is : ] [I's : ] {f' : βL[π] TangentSpace I' (f x)} (h : HasMFDerivWithinAt I I' f s x f') (ht : β (x : M), x β t β fβ x = f x) (hx : fβ x = f x) (hβ : t β s) :
HasMFDerivWithinAt I I' fβ t x f'
theorem HasMFDerivAt.congr_of_eventuallyEq {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {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'] {f : M β M'} {fβ : M β M'} {x : M} [Is : ] [I's : ] {f' : βL[π] TangentSpace I' (f x)} (h : HasMFDerivAt I I' f x f') (hβ : fβ =αΆ [nhds x] f) :
HasMFDerivAt I I' fβ x f'
theorem MDifferentiableWithinAt.congr_of_eventuallyEq {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {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'] {f : M β M'} {fβ : M β M'} {x : M} {s : Set M} [Is : ] [I's : ] (h : MDifferentiableWithinAt I I' f s x) (hβ : fβ =αΆ [] f) (hx : fβ x = f x) :
MDifferentiableWithinAt I I' fβ s x
theorem Filter.EventuallyEq.mdifferentiableWithinAt_iff {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] (I : ModelWithCorners π E H) {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'] {f : M β M'} {fβ : M β M'} {x : M} {s : Set M} [Is : ] [I's : ] (hβ : fβ =αΆ [] f) (hx : fβ x = f x) :
theorem MDifferentiableWithinAt.congr_mono {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {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'] {f : M β M'} {fβ : M β M'} {x : M} {s : Set M} {t : Set M} [Is : ] [I's : ] (h : MDifferentiableWithinAt I I' f s x) (ht : β (x : M), x β t β fβ x = f x) (hx : fβ x = f x) (hβ : t β s) :
MDifferentiableWithinAt I I' fβ t x
theorem MDifferentiableWithinAt.congr {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {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'] {f : M β M'} {fβ : M β M'} {x : M} {s : Set M} [Is : ] [I's : ] (h : MDifferentiableWithinAt I I' f s x) (ht : β (x : M), x β s β fβ x = f x) (hx : fβ x = f x) :
MDifferentiableWithinAt I I' fβ s x
theorem MDifferentiableOn.congr_mono {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {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'] {f : M β M'} {fβ : M β M'} {s : Set M} {t : Set M} [Is : ] [I's : ] (h : MDifferentiableOn I I' f s) (h' : β (x : M), x β t β fβ x = f x) (hβ : t β s) :
MDifferentiableOn I I' fβ t
theorem MDifferentiableAt.congr_of_eventuallyEq {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {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'] {f : M β M'} {fβ : M β M'} {x : M} [Is : ] [I's : ] (h : MDifferentiableAt I I' f x) (hL : fβ =αΆ [nhds x] f) :
MDifferentiableAt I I' fβ x
theorem MDifferentiableWithinAt.mfderivWithin_congr_mono {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {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'] {f : M β M'} {fβ : M β M'} {x : M} {s : Set M} {t : Set M} [Is : ] [I's : ] (h : MDifferentiableWithinAt I I' f s x) (hs : β (x : M), x β t β fβ x = f x) (hx : fβ x = f x) (hxt : ) (hβ : t β s) :
mfderivWithin I I' fβ t x = mfderivWithin I I' f s x
theorem Filter.EventuallyEq.mfderivWithin_eq {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {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'] {f : M β M'} {fβ : M β M'} {x : M} {s : Set M} [Is : ] [I's : ] (hs : ) (hL : fβ =αΆ [] f) (hx : fβ x = f x) :
mfderivWithin I I' fβ s x = mfderivWithin I I' f s x
theorem mfderivWithin_congr {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {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'] {f : M β M'} {fβ : M β M'} {x : M} {s : Set M} [Is : ] [I's : ] (hs : ) (hL : β (x : M), x β s β fβ x = f x) (hx : fβ x = f x) :
mfderivWithin I I' fβ s x = mfderivWithin I I' f s x
theorem tangentMapWithin_congr {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {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'] {f : M β M'} {fβ : M β M'} {s : Set M} [Is : ] [I's : ] (h : β (x : M), x β s β f x = fβ x) (p : ) (hp : p.proj β s) (hs : UniqueMDiffWithinAt I s p.proj) :
tangentMapWithin I I' f s p = tangentMapWithin I I' fβ s p
theorem Filter.EventuallyEq.mfderiv_eq {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {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'] {f : M β M'} {fβ : M β M'} {x : M} [Is : ] [I's : ] (hL : fβ =αΆ [nhds x] f) :
mfderiv I I' fβ x = mfderiv I I' f x
theorem mfderiv_congr_point {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {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'] {f : M β M'} {x : M} [Is : ] [I's : ] {x' : M} (h : x = x') :
mfderiv I I' f x = mfderiv I I' f x'

A congruence lemma for mfderiv, (ab)using the fact that TangentSpace I' (f x) is definitionally equal to E'.

theorem mfderiv_congr {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {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'] {f : M β M'} {x : M} [Is : ] [I's : ] {f' : M β M'} (h : f = f') :
mfderiv I I' f x = mfderiv I I' f' x

A congruence lemma for mfderiv, (ab)using the fact that TangentSpace I' (f x) is definitionally equal to E'.

### Composition lemmas #

theorem writtenInExtChartAt_comp {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {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'} {x : M} {s : Set M} {g : M' β M''} (h : ) :
{y | writtenInExtChartAt I I'' x (g β f) y = (writtenInExtChartAt I' I'' (f x) g β writtenInExtChartAt I I' x f) y} β nhdsWithin (β() x) (β() β»ΒΉ' s β© Set.range βI)
theorem HasMFDerivWithinAt.comp {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {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'} (x : M) {s : Set M} {g : M' β M''} {u : Set M'} [Is : ] [I's : ] [I''s : ] {f' : βL[π] TangentSpace I' (f x)} {g' : TangentSpace I' (f x) βL[π] TangentSpace I'' (g (f x))} (hg : HasMFDerivWithinAt I' I'' g u (f x) g') (hf : HasMFDerivWithinAt I I' f s x f') (hst : s β f β»ΒΉ' u) :
HasMFDerivWithinAt I I'' (g β f) s x ()
theorem HasMFDerivAt.comp {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {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'} (x : M) {g : M' β M''} [Is : ] [I's : ] [I''s : ] {f' : βL[π] TangentSpace I' (f x)} {g' : TangentSpace I' (f x) βL[π] TangentSpace I'' (g (f x))} (hg : HasMFDerivAt I' I'' g (f x) g') (hf : HasMFDerivAt I I' f x f') :
HasMFDerivAt I I'' (g β f) x ()

The chain rule.

theorem HasMFDerivAt.comp_hasMFDerivWithinAt {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {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'} (x : M) {s : Set M} {g : M' β M''} [Is : ] [I's : ] [I''s : ] {f' : βL[π] TangentSpace I' (f x)} {g' : TangentSpace I' (f x) βL[π] TangentSpace I'' (g (f x))} (hg : HasMFDerivAt I' I'' g (f x) g') (hf : HasMFDerivWithinAt I I' f s x f') :
HasMFDerivWithinAt I I'' (g β f) s x ()
theorem MDifferentiableWithinAt.comp {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {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'} (x : M) {s : Set M} {g : M' β M''} {u : Set M'} [Is : ] [I's : ] [I''s : ] (hg : MDifferentiableWithinAt I' I'' g u (f x)) (hf : MDifferentiableWithinAt I I' f s x) (h : s β f β»ΒΉ' u) :
theorem MDifferentiableAt.comp {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {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'} (x : M) {g : M' β M''} [Is : ] [I's : ] [I''s : ] (hg : MDifferentiableAt I' I'' g (f x)) (hf : MDifferentiableAt I I' f x) :
theorem mfderivWithin_comp {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {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'} (x : M) {s : Set M} {g : M' β M''} {u : Set M'} [Is : ] [I's : ] [I''s : ] (hg : MDifferentiableWithinAt I' I'' g u (f x)) (hf : MDifferentiableWithinAt I I' f s x) (h : s β f β»ΒΉ' u) (hxs : ) :
mfderivWithin I I'' (g β f) s x = ContinuousLinearMap.comp (mfderivWithin I' I'' g u (f x)) (mfderivWithin I I' f s x)
theorem mfderiv_comp {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {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'} (x : M) {g : M' β M''} [Is : ] [I's : ] [I''s : ] (hg : MDifferentiableAt I' I'' g (f x)) (hf : MDifferentiableAt I I' f x) :
mfderiv I I'' (g β f) x = ContinuousLinearMap.comp (mfderiv I' I'' g (f x)) (mfderiv I I' f x)
theorem mfderiv_comp_of_eq {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {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'} {g : M' β M''} [Is : ] [I's : ] [I''s : ] {x : M} {y : M'} (hg : MDifferentiableAt I' I'' g y) (hf : MDifferentiableAt I I' f x) (hy : f x = y) :
mfderiv I I'' (g β f) x = ContinuousLinearMap.comp (mfderiv I' I'' g (f x)) (mfderiv I I' f x)
theorem MDifferentiableOn.comp {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {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'} {s : Set M} {g : M' β M''} {u : Set M'} [Is : ] [I's : ] [I''s : ] (hg : MDifferentiableOn I' I'' g u) (hf : MDifferentiableOn I I' f s) (st : s β f β»ΒΉ' u) :
theorem MDifferentiable.comp {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {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'} {g : M' β M''} [Is : ] [I's : ] [I''s : ] (hg : MDifferentiable I' I'' g) (hf : MDifferentiable I I' f) :
theorem tangentMapWithin_comp_at {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {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'} {s : Set M} {g : M' β M''} {u : Set M'} [Is : ] [I's : ] [I''s : ] (p : ) (hg : MDifferentiableWithinAt I' I'' g u (f p.proj)) (hf : MDifferentiableWithinAt I I' f s p.proj) (h : s β f β»ΒΉ' u) (hps : UniqueMDiffWithinAt I s p.proj) :
tangentMapWithin I I'' (g β f) s p = tangentMapWithin I' I'' g u (tangentMapWithin I I' f s p)
theorem tangentMap_comp_at {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {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'} {g : M' β M''} [Is : ] [I's : ] [I''s : ] (p : ) (hg : MDifferentiableAt I' I'' g (f p.proj)) (hf : MDifferentiableAt I I' f p.proj) :
tangentMap I I'' (g β f) p = tangentMap I' I'' g (tangentMap I I' f p)
theorem tangentMap_comp {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {H : Type u_3} [] {I : ModelWithCorners π E H} {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'} {g : M' β M''} [Is : ] [I's : ] [I''s : ] (hg : MDifferentiable I' I'' g) (hf : MDifferentiable I I' f) :
tangentMap I I'' (g β f) = tangentMap I' I'' g β tangentMap I I' f

### 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} [] {E : Type u_2} [NormedSpace π E] {s : Set E} {x : E} :
theorem UniqueMDiffWithinAt.uniqueDiffWithinAt {π : Type u_1} [] {E : Type u_2} [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} [] {E : Type u_2} [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} [] {E : Type u_2} [NormedSpace π E] {s : Set E} :
theorem UniqueMDiffOn.uniqueDiffOn {π : Type u_1} [] {E : Type u_2} [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} [] {E : Type u_2} [NormedSpace π E] {s : Set E} :
UniqueDiffOn π s β UniqueMDiffOn (modelWithCornersSelf π E) s

Alias of the reverse direction of uniqueMDiffOn_iff_uniqueDiffOn.

theorem writtenInExtChartAt_model_space {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {E' : Type u_3} [] [NormedSpace π E'] {f : E β E'} {x : E} :
theorem hasMFDerivWithinAt_iff_hasFDerivWithinAt {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {E' : Type u_3} [] [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} [] {E : Type u_2} [NormedSpace π E] {E' : Type u_3} [] [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} [] {E : Type u_2} [NormedSpace π E] {E' : Type u_3} [] [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} [] {E : Type u_2} [NormedSpace π E] {E' : Type u_3} [] [NormedSpace π E'] {f : E β E'} {x : E} {f' : TangentSpace (modelWithCornersSelf π E) x βL[π] TangentSpace (modelWithCornersSelf π E') (f x)} :
theorem HasFDerivAt.hasMFDerivAt {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {E' : Type u_3} [] [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} [] {E : Type u_2} [NormedSpace π E] {E' : Type u_3} [] [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} [] {E : Type u_2} [NormedSpace π E] {E' : Type u_3} [] [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} [] {E : Type u_2} [NormedSpace π E] {E' : Type u_3} [] [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} [] {E : Type u_2} [NormedSpace π E] {E' : Type u_3} [] [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} [] {E : Type u_2} [NormedSpace π E] {E' : Type u_3} [] [NormedSpace π E'] {f : E β E'} {x : E} :

For maps between vector spaces, MDifferentiableAt and DifferentiableAt coincide

theorem DifferentiableAt.mdifferentiableAt {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {E' : Type u_3} [] [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} [] {E : Type u_2} [NormedSpace π E] {E' : Type u_3} [] [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} [] {E : Type u_2} [NormedSpace π E] {E' : Type u_3} [] [NormedSpace π E'] {f : E β E'} {s : Set E} :

For maps between vector spaces, MDifferentiableOn and DifferentiableOn coincide

theorem DifferentiableOn.mdifferentiableOn {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {E' : Type u_3} [] [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 MDifferentiableOn.differentiableOn {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {E' : Type u_3} [] [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 mdifferentiable_iff_differentiable {π : Type u_1} [] {E : Type u_2}