Differentiability of functions in vector bundles #
Characterization of differentiable functions into a vector bundle. Version at a point within a set
Characterization of differentiable functions into a vector bundle. Version at a point
Characterization of differentiable sections of a vector bundle at a point within a set in terms of the preferred trivialization at that point.
Characterization of differentiable sections of a vector bundle at a point within a set in terms of the preferred trivialization at that point.
Characterization of differentiable functions into a vector bundle in terms of any trivialization. Version at a point within at set.
Characterization of differentiable functions into a vector bundle in terms of any trivialization. Version at a point.
Characterization of differentiable functions into a vector bundle in terms of any trivialization. Version at a point within at set.
Characterization of differentiable functions into a vector bundle in terms of any trivialization. Version at a point.
Differentiability of a section on s can be determined
using any trivialisation whose baseSet contains s.
For any trivialization e, the differentiability of a section on e.baseSet
can be determined using e.
The scalar product ฯ โข s of a differentiable function ฯ : M โ ๐ and a section s of a
vector bundle V โ M is differentiable once s is differentiable on an open set containing
tsupport ฯ.
See ContMDiffOn.smul_section_of_tsupport for the analogous result about C^n sections.
The sum of a locally finite collection of sections is differentiable if each section is. Version at a point within a set.
The sum of a locally finite collection of sections is differentiable at x
if each section is.
The sum of a locally finite collection of sections is differentiable on a set u
if each section is.
The sum of a locally finite collection of sections is differentiable if each section is.
Consider a differentiable map v : M โ Eโ to a vector bundle, over a basemap bโ : M โ Bโ, and
another basemap bโ : M โ Bโ. Given linear maps ฯ m : Eโ (bโ m) โ Eโ (bโ m) depending
differentiably on m, one can apply ฯ m to g m, and the resulting map is differentiable.
Note that the differentiability of ฯ cannot be always be stated as differentiability of a map
into a manifold, as the pullback bundles bโ *แต Eโ and bโ *แต Eโ only make sense when bโ
and bโ are globally smooth, but we want to apply this lemma with only local information.
Therefore, we formulate it using differentiability of ฯ read in coordinates.
Version for MDifferentiableWithinAt. We also give a version for MDifferentiableAt, but no
version for MDifferentiableOn or MDifferentiable as our assumption, written in coordinates,
only makes sense around a point.
Consider a differentiable map v : M โ Eโ to a vector bundle, over a basemap bโ : M โ Bโ, and
another basemap bโ : M โ Bโ. Given linear maps ฯ m : Eโ (bโ m) โ Eโ (bโ m) depending
differentiably on m, one can apply ฯ m to g m, and the resulting map is differentiable.
Note that the differentiability of ฯ cannot be always be stated as differentiability of a map
into a manifold, as the pullback bundles bโ *แต Eโ and bโ *แต Eโ only make sense when bโ
and bโ are globally smooth, but we want to apply this lemma with only local information.
Therefore, we formulate it using differentiability of ฯ read in coordinates.
Version for MDifferentiableAt. We also give a version for MDifferentiableWithinAt,
but no version for MDifferentiableOn or MDifferentiable as our assumption, written
in coordinates, only makes sense around a point.