# 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'`

.

Various related results are proven in separate files: see

`Basic.lean`

for basic properties of the`mfderiv`

, mimicking the API of the FrΓ©chet derivative,`FDeriv.lean`

for the equivalence of the manifold notions with the usual FrΓ©chet derivative for functions between vector spaces,`SpecificFunctions.lean`

for results on the differential of the identity, constant functions, products and arithmetic operators (like addition or scalar multiplication),`Atlas.lean`

for differentiability of charts, models with corners and extended charts,`UniqueDifferential.lean`

for various properties of unique differentiability sets in manifolds.

## 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 subtlety 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".

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.

## Equations

- DifferentiableWithinAtProp I I' f s x = DifferentiableWithinAt π (βI' β f β β(ModelWithCorners.symm I)) (β(ModelWithCorners.symm I) β»ΒΉ' s β© Set.range βI) (βI x)

## Instances For

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

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.

## Equations

- UniqueMDiffWithinAt I s x = UniqueDiffWithinAt π (β(PartialEquiv.symm (extChartAt I x)) β»ΒΉ' s β© Set.range βI) (β(extChartAt I x) x)

## Instances For

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

## Equations

- UniqueMDiffOn I s = β x β s, UniqueMDiffWithinAt I s x

## Instances For

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

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

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

## Equations

- MDifferentiableAt I I' f x = (ContinuousAt f x β§ DifferentiableWithinAt π (writtenInExtChartAt I I' x f) (Set.range βI) (β(extChartAt I x) x))

## Instances For

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

## Equations

- MDifferentiableOn I I' f s = β x β s, MDifferentiableWithinAt I I' f s x

## Instances For

`MDifferentiable I I' f`

indicates that the function `f`

between manifolds
has a derivative everywhere.
This is a generalization of `Differentiable`

to manifolds.

## Equations

- MDifferentiable I I' f = β (x : M), MDifferentiableAt I I' f x

## Instances For

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

## Equations

- PartialHomeomorph.MDifferentiable I I' f = (MDifferentiableOn I I' (βf) f.source β§ MDifferentiableOn I' I (β(PartialHomeomorph.symm f)) f.target)

## Instances For

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

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

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

## Equations

- HasMFDerivAt I I' f x f' = (ContinuousAt f x β§ HasFDerivWithinAt (writtenInExtChartAt I I' x f) f' (Set.range βI) (β(extChartAt I x) x))

## Instances For

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`

.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

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`

.

## Equations

- mfderiv I I' f x = if MDifferentiableAt I I' f x then fderivWithin π (writtenInExtChartAt I I' x f) (Set.range βI) (β(extChartAt I x) x) else 0

## Instances For

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

## Equations

- tangentMapWithin I I' f s p = { proj := f p.proj, snd := (mfderivWithin I I' f s p.proj) p.snd }

## Instances For

The derivative, as a map between the tangent bundles

## Equations

- tangentMap I I' f p = { proj := f p.proj, snd := (mfderiv I I' f p.proj) p.snd }