The gradient of a function on a Riemannian manifold #
On a manifold M whose tangent spaces carry a Riemannian metric, the gradient of a function
f : M → ℝ at x is the tangent vector grad f x dual to the differential df_x through the
metric: ⟪grad f x, v⟫ = df_x v for every tangent vector v. It is the fibrewise Riesz dual
Riemannian.Tensor.rieszDual of df_x.
The gradient within a subset is similarly the fibrewise Riesz dual of mvfderivWithin.
Its characteristic equations, uniqueness, vanishing, and neighbourhood-restriction laws require
only the pointwise Riemannian bundle structure.
For a C^{n+1} function and a C^n metric, the gradient is a C^n vector field: the evaluations
of df on a chart-local frame are C^n, and so is the Riesz dual of such a field of covectors
(Riemannian.Tensor.contMDiffAt_rieszDual).
Main declarations #
TauCeti.Manifold.mgradient: the gradient of a function.TauCeti.Manifold.mgradientWithin: the gradient within a subset.TauCeti.Manifold.inner_mgradient: its characteristic property⟪grad f x, v⟫ = df_x v, andTauCeti.Manifold.eq_mgradient_iff, which identifies the gradient from it.TauCeti.Manifold.mgradient_eq_zero_iff: the gradient vanishes exactly where the differential does, andTauCeti.Manifold.norm_mgradient_eq_norm_mvfderiv: it has the same length as the differential.TauCeti.Manifold.contMDiffAt_mgradient: the gradient of a function that isC^{n+1}at a point for aC^nmetric isC^nat that point.TauCeti.Manifold.contMDiff_mgradient: the gradient of aC^{n+1}function for aC^nmetric is aC^nvector field.TauCeti.Manifold.continuous_inner_mgradient: the inner product of the gradients of twoC¹functions is continuous, and so are the lengthTauCeti.Manifold.continuous_norm_mgradientand squared lengthTauCeti.Manifold.continuous_norm_sq_mgradientof the gradient.TauCeti.Manifold.mdifferentiable_mgradient: aC²function has a differentiable Riemannian gradient section.TauCeti.Manifold.contMDiff_neg_mgradient: so is the negative gradient, andTauCeti.Manifold.contMDiff_neg_mgradient_onestates itsC¹case for aC²function.TauCeti.Manifold.eventually_norm_fderiv_comp_extChartAt_symm_le_mul_norm_mgradient: for a continuous metric, the differential offread in a chart is locally bounded by a multiple of the length of the gradient. This is how coordinate estimates fordfbecome metric estimates.TauCeti.Manifold.eventually_norm_mgradient_le_mul_norm_fderiv_comp_extChartAt_symm: the sharp converse, comparing the length of the gradient nearpwith the length, for the metric atp, of the coordinate differential, up to a factor arbitrarily close to1.
The gradient of a function f : M → ℝ at x for the Riemannian metric: the tangent
vector dual to the differential df_x, so that ⟪grad f x, v⟫ = df_x v.
Instances For
The gradient is the fibrewise Riesz dual of the manifold derivative.
The characteristic property of the gradient: ⟪grad f x, v⟫ = df_x v.
The characteristic property of the gradient: ⟪v, grad f x⟫ = df_x v.
A tangent vector is the gradient exactly when its inner product with every vector v is
df_x v.
The differential of f in the direction of its gradient is the squared length of the
gradient.
The gradient vanishes exactly where the differential does.
The gradient of a compactly supported function is compactly supported, since it vanishes off the support of the function.
Pairing the gradient of a compactly supported function with any vector field gives a compactly supported scalar function. No differentiability assumption is needed.
The gradient has the same length as the differential it represents: the Riesz equivalence is an isometry.
The gradient of a constant function is zero.
The gradient is additive on differentiable functions.
The gradient satisfies the scalar product rule for differentiable functions.
The gradient commutes with multiplication by a real constant.
Along the line f + t g, the squared length of the gradient is the quadratic polynomial
‖grad f‖² + 2 t ⟪grad g, grad f⟫ + t² ‖grad g‖² in t.
The gradient of -f is the opposite of the gradient of f.
The Riemannian gradient within a set, obtained by taking the fibrewise Riesz dual of the manifold derivative within that set. Like the derivative, it is total.
Instances For
The gradient within a set is the Riesz dual of the relative differential.
Pairing the relative gradient with a tangent vector evaluates the relative differential.
The symmetric form of the relative gradient's characteristic equation.
On the whole manifold the relative gradient is the gradient.
The relative gradient is uniquely characterized by its inner products.
The relative gradient vanishes exactly where the relative differential vanishes.
Restriction to a neighbourhood does not change the gradient.
The gradient is smooth. For a C^n Riemannian metric, the gradient of a C^{n+1}
function is a C^n vector field at a point.
The gradient is smooth. For a C^n Riemannian metric, the gradient of a C^{n+1}
function is a C^n vector field.
A C² function has a differentiable Riemannian gradient section.
The negative gradient is smooth. For a C^n Riemannian metric, the negative gradient of a
C^{n+1} function is a C^n vector field.
TauCeti.Manifold.contMDiff_neg_mgradient at n = 1, with the smoothness order 1 + 1
written as 2, in the form taken by the integral-curve API.
For a C^n Riemannian metric, the inner product of the gradients of two C^{n+1}
functions is C^n.
For a C^n Riemannian metric, the squared norm of the gradient of a C^{n+1}
function is C^n.
The inner product of two gradients is continuous. For a continuous Riemannian metric, the
pointwise inner product ⟪grad f, grad g⟫ of two C¹ functions is a continuous function.
For a continuous Riemannian metric, the squared length ‖grad f‖² of the gradient of a C¹
function is continuous.
For a continuous Riemannian metric, the length ‖grad f‖ of the gradient of a C¹ function
is continuous.
Comparison with the differential in a chart #
The differential in a chart is controlled by the gradient. Near p, the Fréchet
derivative of the coordinate expression of a function f in the extended chart at p is bounded
by a fixed multiple of the Riemannian length of the gradient of f. The constant and the
neighbourhood depend only on the metric, not on f: the constant bounds the operator norm of the
inverse of the tangent chart, measured with the metric on its target, which is locally bounded
for a continuous metric.
The gradient is sharply controlled by the differential in a chart. For a continuous
metric and any r > 1, near p the Riemannian length of the gradient of f is at most r times
the length of the coordinate differential of f in the extended chart at p, transported to the
tangent space at p by the tangent chart and measured with the metric at p. The constant r
can be taken arbitrarily close to 1 because the metric read in the chart is continuous.