Smooth functions between smooth manifolds #
We define Cⁿ
functions between smooth manifolds, as functions which are Cⁿ
in charts, and prove
basic properties of these notions.
Main definitions and statements #
Let M
and M'
be two smooth manifolds, with respect to model with corners I
and I'
. Let
f : M → M'
.
ContMDiffWithinAt I I' n f s x
states that the functionf
isCⁿ
within the sets
around the pointx
.ContMDiffAt I I' n f x
states that the functionf
isCⁿ
aroundx
.ContMDiffOn I I' n f s
states that the functionf
isCⁿ
on the sets
ContMDiff I I' n f
states that the functionf
isCⁿ
.
We also give some basic properties of smooth functions between manifolds, following the API of
smooth functions between vector spaces.
See Basic.lean
for further basic properties of smooth functions between smooth manifolds,
NormedSpace.lean
for the equivalence of manifold-smoothness to usual smoothness,
Product.lean
for smoothness results related to the product of manifolds and
Atlas.lean
for smoothness of atlas members and local structomorphisms.
Implementation details #
Many properties follow for free from the corresponding properties of functions in vector spaces,
as being Cⁿ
is a local property invariant under the smooth groupoid. We take advantage of the
general machinery developed in LocalInvariantProperties.lean
to get these properties
automatically. For instance, the fact that being Cⁿ
does not depend on the chart one considers
is given by liftPropWithinAt_indep_chart
.
For this to work, the definition of ContMDiffWithinAt
and friends has to
follow definitionally the setup of local invariant properties. Still, we recast the definition
in terms of extended charts in contMDiffOn_iff
and contMDiff_iff
.
Definition of smooth functions between manifolds #
Property in the model space of a model with corners of being C^n
within at set at a point,
when read in the model vector space. This property will be lifted to manifolds to define smooth
functions between manifolds.
Equations
- ContDiffWithinAtProp I I' n f s x = ContDiffWithinAt 𝕜 (↑n) (↑I' ∘ f ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ Set.range ↑I) (↑I x)
Instances For
Being Cⁿ
in the model space is a local property, invariant under smooth maps. Therefore,
it will lift nicely to manifolds.
A function is n
times continuously differentiable within a set at a point in a manifold if
it is continuous and it is n
times continuously differentiable in this set around this point, when
read in the preferred chart at this point.
Equations
- ContMDiffWithinAt I I' n f s x = ChartedSpace.LiftPropWithinAt (ContDiffWithinAtProp I I' n) f s x
Instances For
Alias of ContMDiffWithinAt
.
A function is n
times continuously differentiable within a set at a point in a manifold if
it is continuous and it is n
times continuously differentiable in this set around this point, when
read in the preferred chart at this point.
Equations
Instances For
A function is n
times continuously differentiable at a point in a manifold if
it is continuous and it is n
times continuously differentiable around this point, when
read in the preferred chart at this point.
Equations
- ContMDiffAt I I' n f x = ContMDiffWithinAt I I' n f Set.univ x
Instances For
Alias of ContMDiffAt
.
A function is n
times continuously differentiable at a point in a manifold if
it is continuous and it is n
times continuously differentiable around this point, when
read in the preferred chart at this point.
Equations
Instances For
A function is n
times continuously differentiable in a set of a manifold if it is continuous
and, for any pair of points, it is n
times continuously differentiable on this set in the charts
around these points.
Equations
- ContMDiffOn I I' n f s = ∀ x ∈ s, ContMDiffWithinAt I I' n f s x
Instances For
Alias of ContMDiffOn
.
A function is n
times continuously differentiable in a set of a manifold if it is continuous
and, for any pair of points, it is n
times continuously differentiable on this set in the charts
around these points.
Equations
Instances For
A function is n
times continuously differentiable in a manifold if it is continuous
and, for any pair of points, it is n
times continuously differentiable in the charts
around these points.
Equations
- ContMDiff I I' n f = ∀ (x : M), ContMDiffAt I I' n f x
Instances For
Alias of ContMDiff
.
A function is n
times continuously differentiable in a manifold if it is continuous
and, for any pair of points, it is n
times continuously differentiable in the charts
around these points.
Instances For
Deducing smoothness from higher smoothness #
Basic properties of smooth functions between manifolds #
Alias of ContMDiff.of_le
.
Alias of ContMDiff.of_le
.
Alias of ContMDiffOn.of_le
.
Alias of ContMDiffOn.of_le
.
Alias of ContMDiffAt.of_le
.
Alias of ContMDiffOn.of_le
.
Alias of ContMDiffWithinAt.of_le
.
Alias of ContMDiffWithinAt.of_le
.
Alias of ContMDiff.contMDiffAt
.
Alias of contMDiffWithinAt_univ
.
Alias of contMDiffOn_univ
.
One can reformulate smoothness within a set at a point as continuity within this set at this point, and smoothness in the corresponding extended chart.
One can reformulate smoothness within a set at a point as continuity within this set at this
point, and smoothness in the corresponding extended chart. This form states smoothness of f
written in such a way that the set is restricted to lie within the domain/codomain of the
corresponding charts.
Even though this expression is more complicated than the one in contMDiffWithinAt_iff
, it is
a smaller set, but their germs at extChartAt I x x
are equal. It is sometimes useful to rewrite
using this in the goal.
One can reformulate smoothness within a set at a point as continuity within this set at this point, and smoothness in the corresponding extended chart in the target.
Alias of contMDiffWithinAt_iff
.
One can reformulate smoothness within a set at a point as continuity within this set at this point, and smoothness in the corresponding extended chart.
Alias of contMDiffWithinAt_iff_target
.
One can reformulate smoothness within a set at a point as continuity within this set at this point, and smoothness in the corresponding extended chart in the target.
Alias of contMDiffAt_iff_target
.
An alternative formulation of contMDiffWithinAt_iff_of_mem_maximalAtlas
if the set if s
lies in e.source
.
One can reformulate smoothness within a set at a point as continuity within this set at this point, and smoothness in any chart containing that point.
If the set where you want f
to be smooth lies entirely in a single chart, and f
maps it
into a single chart, the smoothness of f
on that set can be expressed by purely looking in
these charts.
Note: this lemma uses extChartAt I x '' s
instead of (extChartAt I x).symm ⁻¹' s
to ensure
that this set lies in (extChartAt I x).target
.
If the set where you want f
to be smooth lies entirely in a single chart, and f
maps it
into a single chart, the smoothness of f
on that set can be expressed by purely looking in
these charts.
Note: this lemma uses extChartAt I x '' s
instead of (extChartAt I x).symm ⁻¹' s
to ensure
that this set lies in (extChartAt I x).target
.
One can reformulate smoothness on a set as continuity on this set, and smoothness in any extended chart.
One can reformulate smoothness on a set as continuity on this set, and smoothness in any extended chart in the target.
Alias of contMDiffOn_iff
.
One can reformulate smoothness on a set as continuity on this set, and smoothness in any extended chart.
Alias of contMDiffOn_iff_target
.
One can reformulate smoothness on a set as continuity on this set, and smoothness in any extended chart in the target.
One can reformulate smoothness as continuity and smoothness in any extended chart.
One can reformulate smoothness as continuity and smoothness in any extended chart in the target.
Alias of contMDiff_iff
.
One can reformulate smoothness as continuity and smoothness in any extended chart.
Alias of contMDiff_iff_target
.
One can reformulate smoothness as continuity and smoothness in any extended chart in the target.
Deducing smoothness from smoothness one step beyond #
Deducing continuity from smoothness #
C^∞
smoothness #
Restriction to a smaller set #
Alias of ContMDiffWithinAt.mono_of_mem_nhdsWithin
.
Alias of contMDiffWithinAt_congr_set
.
Alias of the forward direction of contMDiffWithinAt_insert_self
.
Being C^n
in a set only depends on the germ of the set. Version where one only requires
the two sets to coincide locally in the complement of a point y
.
Alias of ContMDiffAt.contMDiffWithinAt
.
Alias of ContMDiff.contMDiffOn
.
Alias of ContMDiffWithinAt.contMDiffAt
.
Alias of ContMDiffOn.contMDiffAt
.
A function is C^n
within a set at a point, for n : ℕ
, if and only if it is C^n
on
a neighborhood of this point.
If a function is C^m
within a set at a point, for some finite m
, then it is C^m
within
this set on an open set around the basepoint.
If a function is C^m
within a set at a point, for some finite m
, then it is C^m
within
this set on a neighborhood of the basepoint.
A function is C^n
at a point, for n : ℕ
, if and only if it is C^n
on
a neighborhood of this point.
Note: This does not hold for n = ∞
. f
being C^∞
at x
means that for every n
, f
is
C^n
on some neighborhood of x
, but this neighborhood can depend on n
.
Note: This does not hold for n = ∞
. f
being C^∞
at x
means that for every n
, f
is
C^n
on some neighborhood of x
, but this neighborhood can depend on n
.
Congruence lemmas #
Locality #
Being C^n
is a local property.