Derivatives of vector-valued functions #
For a function g from a manifold to a normed space F, Mathlib has two derivatives at x:
mfderiv I π(π, F) g x, with values in the tangent space TangentSpace π(π, F) (g x), and
mvfderiv I g x, with values in F itself. They differ by the identification of the tangent space
with F. The canonical identification relates their vanishing, injectivity and ranges.
Main results #
TauCeti.mvfderiv_eq_fderiv_apply: on normed spaces,mvfderivapplied to a tangent vector isfderivapplied to it.TauCeti.mvfderiv_comp_apply_of_differentiableAt: the chain rule when the outer map is between normed spaces.TauCeti.mvfderiv_scalar_comp: the chain ruled(Ο β g) = Ο'(g x) β’ dgfor scalarΟ.ContinuousLinearMap.mvfderiv_comp_apply: the chain rule when the outer map is continuous linear.MDifferentiableAt.mvfderiv_prod_eq_add_apply: the vector-valued derivative on a product is the sum of its partial derivatives.TauCeti.fderiv_comp_graph_apply_of_mdifferentiableAt: the chain rule along the graph of a manifold-valued map on a normed space.TauCeti.continuous_fderiv_of_contMDiff: the derivative in the domain variable of aCΒΉfamily along aCΒΉmanifold-valued map is continuous.TauCeti.mfderiv_apply_eq_zero_of_const_line: the derivative of a map from a normed space vanishes on a direction along which the map is constant.TauCeti.mvfderiv_apply: the derivative of a component of a function into a finite product is the component of its derivative.mvfderiv_apply_eq_mfderiv_apply: evaluatingmvfderivagrees with evaluatingmfderiv.Submodule.map_mvfderiv_eq_map_mfderiv: both derivatives have the same image of a tangent submodule.TauCeti.mvfderiv_const_smul:mvfderivcommutes with multiplication by a constant scalar.TauCeti.mvfderiv_const_smul_field: the same for a scalar in the base field, without a differentiability hypothesis.TauCeti.mvfderiv_fun_sum:mvfderivof a finite sum of differentiable functions is the sum of theirmvfderivs.Filter.EventuallyEq.mvfderiv_eq:mvfderivdepends only on the germ of the function.TauCeti.mvfderiv_apply_of_eventuallyEq_extChartAt: a map with the germ of the extended chart atxhas the identity as derivative atx.TauCeti.mvfderiv_eq_zero_iff:mvfderiv I g x = 0 β mfderiv I π(π, F) g x = 0.TauCeti.range_mvfderiv: the tangent-space identification transports derivative ranges.TauCeti.injective_mvfderiv_iff:Function.Injective (mvfderiv I g x) β Function.Injective (mfderiv I π(π, F) g x).TauCeti.mdifferentiableAt_of_mvfderiv_apply_ne_zero: a function whosemvfderivis nonzero on some tangent vector is differentiable there.TauCeti.mfderiv_neg_eq_zero_iff:mfderiv I π(π, F) (-g) x = 0 β mfderiv I π(π, F) g x = 0.
The canonical model-space tangent identification preserves the underlying vector. Use this equation explicitly: automatic simplification can change an equality's codomain from the tangent fibre to the model, whose normed-space instances are distinct.
The inverse model-space tangent identification preserves the underlying vector.
As with fromTangentSpace_apply, this equation is for explicit tangent/model conversions.
For maps between normed spaces, the vector-valued manifold derivative applied to a tangent
vector is the FrΓ©chet derivative applied to the same vector. Not @[simp]: mvfderiv_eq_fderiv
already rewrites the left-hand side.
For a normed vector-space target, evaluating mvfderiv agrees with evaluating
mfderiv under the canonical tangent-space identification.
The image of a tangent submodule under the vector-valued derivative agrees with its image under the manifold derivative into the self model of the target.
The derivative at x of a vector-valued function, read in the target space, depends only on
the germ of the function at x.
A map into the model space with the germ of the extended chart at x has the identity as
derivative at x, a tangent vector at x being read as a vector of the model space.
The chain rule for a vector-valued function on a manifold followed by a map between normed spaces that is differentiable at the relevant point, evaluated on a tangent vector.
The chain rule for a scalar function on a manifold followed by a scalar function
differentiable at the relevant point: the derivative is scaled by Ο'(g x).
The chain rule for a vector-valued function on a manifold followed by a continuous linear map,
evaluated on a tangent vector: the derivative of L β g is L applied to the derivative of g.
The vector-valued derivative on a product is the sum of its partial derivatives.
The derivative of a graph map, evaluated in the product tangent space.
The chain rule along the graph of a manifold-valued map on a normed space, splitting the result into the derivative in the domain variable and the derivative in the manifold variable.
Along a CΒΉ map u : F β M from a normed space to a manifold, the derivative in the domain
variable of a CΒΉ family f : F β M β F', taken at (y, u y), depends continuously on y. It is
a partial derivative of the CΒΉ map (w, y) β¦ f w (u y) on F Γ F.
The derivative of a vector-valued function, read in the target space, commutes with multiplication by a constant scalar acting continuously on the target, such as a complex scalar on a complex normed space regarded as a real one.
A version of TauCeti.mvfderiv_const_smul without differentiability hypothesis, for a scalar in
the base field: the derivative of a vector-valued function, read in the target space, commutes
with multiplication by any constant.
The derivative of a finite sum of vector-valued functions, read in the target space, is the
sum of their derivatives at a point where each summand is differentiable. This is the manifold
version of fderiv_fun_sum.
The range of the vector-valued derivative is the image of the manifold derivative's range under the canonical identification of the target tangent space with its model.
The derivative of a vector-valued function, read in the target space, vanishes exactly when its manifold derivative does.
The derivative of a vector-valued function, read in the target space, is injective if and only if its manifold derivative is.
A vector-valued function whose derivative does not vanish on some tangent vector is differentiable there.
The derivative of -g vanishes at x if and only if the derivative of g does.
The derivative of a component of a function into a finite product of normed spaces is the
component of its derivative, at a point where the function is differentiable. This is the
manifold version of fderiv_apply.
The derivative of a map from a normed space vanishes on a direction w along which the map is
constant.