Riemannian gradient and Hessian

DefinitionRiemannian gradient#✓fully proved

Let \(M\) be a \(C^1\) manifold modelled on a complete real normed space, with a Riemannian metric, and let \(f : M \to \mathbb{R}\) and \(x \in M\). The Riemannian gradient \(\operatorname{grad} f(x) = (df_x)^\sharp \in T_xM\) is the image of the differential \(df_x\) of \(f\) at \(x\) under the inverse of the Riesz isomorphism \(T_xM \to (T_xM)^*\), \(w \mapsto \langle w, \cdot \rangle\), given by the metric at \(x\). It is the unique tangent vector with \(\langle \operatorname{grad} f(x), v \rangle = df_x(v)\) for all \(v \in T_xM\).

def riemannianGradient (f : M → ℝ) (x : M) : TangentSpace I x :=
  (InnerProductSpace.toDual ℝ (TangentSpace I x)).symm (mvfderiv I f x)

Used by 4

Used byPairing of the Riemannian gradient with a tangent vector · Norm of the Riemannian gradient · Characterization of the Riemannian gradient · The Riemannian gradient on a Hilbert space

TheoremPairing of the Riemannian gradient with a tangent vector#✓fully proved

Let \(M\) be a \(C^1\) manifold modelled on a complete real normed space, with a Riemannian metric \(\langle \cdot, \cdot \rangle\), and let \(f : M \to \mathbb{R}\), \(x \in M\) and \(v \in T_xM\). Then \(\langle \operatorname{grad} f(x), v \rangle = df_x(v)\), where \(\operatorname{grad} f(x)\) is the Riemannian gradient of \(f\) at \(x\) and \(df_x\) is the differential of \(f\) at \(x\).

@[simp]
theorem inner_riemannianGradient (f : M → ℝ) (x : M) (v : TangentSpace I x) :
    inner ℝ (riemannianGradient I f x) v = (mvfderiv I f x) v

Uses 1 · Used by 2

Statement usesRiemannian gradient

Used byCharacterization of the Riemannian gradient · The Riemannian gradient on a Hilbert space

TheoremCharacterization of the Riemannian gradient#✓fully proved

Let \(M\) be a \(C^1\) manifold modelled on a complete real normed space, with a Riemannian metric \(\langle \cdot, \cdot \rangle\), and let \(f : M \to \mathbb{R}\), \(x \in M\) and \(w \in T_xM\). Then the Riemannian gradient \(\operatorname{grad} f(x)\) equals \(w\) if and only if \(\langle w, v \rangle = df_x(v)\) for every \(v \in T_xM\), where \(df_x\) is the differential of \(f\) at \(x\).

theorem riemannianGradient_eq_iff (f : M → ℝ) (x : M) (w : TangentSpace I x) :
    riemannianGradient I f x = w ↔ ∀ v, inner ℝ w v = (mvfderiv I f x) v

Uses 2

Statement usesRiemannian gradient

Proof usesPairing of the Riemannian gradient with a tangent vector

TheoremNorm of the Riemannian gradient#✓fully proved

Let \(M\) be a \(C^1\) manifold modelled on a complete real normed space, with a Riemannian metric, and let \(f : M \to \mathbb{R}\) and \(x \in M\). With \(T_xM\) normed by the metric at \(x\), the norm of the Riemannian gradient \(\operatorname{grad} f(x)\) equals the operator norm of the differential \(df_x : T_xM \to \mathbb{R}\) of \(f\) at \(x\): \(\|\operatorname{grad} f(x)\| = \|df_x\|\). This is the quantity \(|\nabla f|(x)\).

theorem norm_riemannianGradient (f : M → ℝ) (x : M) :
    ‖riemannianGradient I f x‖ = ‖mvfderiv I f x‖

Uses 1

Statement usesRiemannian gradient

DefinitionCovariant Hessian#✓fully proved

Let \(M\) be a smooth manifold modelled on a finite-dimensional real normed space, with a smooth Riemannian metric and its Levi-Civita connection \(\nabla\). For \(f : M \to \mathbb{R}\), a point \(x \in M\) and tangent vectors \(u, v \in T_xM\), let \(V\) be the extension of \(v\) to a vector field with constant coordinates in the preferred chart at \(x\), so that \(V(x) = v\). The Hessian of \(f\) at \(x\) is the real number

\[\nabla^2 f(u, v) = d\big(y \mapsto df_y(V(y))\big)_x(u) - df_x(\nabla_u V),\]

that is, \(u(Vf) - df_x(\nabla_u V)\), where \(df_y\) is the differential of \(f\) at \(y\).

This is the textbook Hessian \(\nabla^2 f = \nabla(df)\), \(\nabla^2 f(u, v) = (\nabla_u df)(v)\) (Lee, Introduction to Riemannian Manifolds, 2nd ed., GTM 176, Ch. 4), taken as a function of two tangent vectors.

def hessian (f : M → ℝ) (x : M) (u v : TangentSpace I x) : ℝ :=
  (mvfderiv I (fun y => (mvfderiv I f y) (FiberBundle.extend E v y)) x) u -
    (mvfderiv I f x)
      (CovariantDerivative.leviCivitaConnection I M (FiberBundle.extend E v) x u)

Used by 10

Used byLaplace–Beltrami operator · Laplacian of the Gaussian potential · Laplacian of the squared norm · Laplacian on a vector space as a sum of second directional derivatives · The Laplacian on a vector space is the flat Laplacian at twice-differentiable points · Gradient Ricci soliton · The Gaussian gradient Ricci soliton · Gaussian potentials that are gradient Ricci solitons · The Hessian on Euclidean space as an iterated directional derivative · The Hessian on Euclidean space is the second derivative

TheoremThe Riemannian gradient on a Hilbert space#✓fully proved

Let \(F\) be a real Hilbert space, viewed as a Riemannian manifold with the metric given by its inner product, and let \(f : F \to \mathbb{R}\) and \(x \in F\). Identifying the tangent space at \(x\) with \(F\), the Riemannian gradient of \(f\) at \(x\) is the Hilbert-space gradient \(\nabla f(x)\), the unique vector with \(\langle \nabla f(x), w \rangle = Df(x)(w)\) for all \(w \in F\), where \(Df(x)\) is the Fréchet derivative of \(f\) at \(x\).

theorem riemannianGradient_vectorSpace {F : Type*} [NormedAddCommGroup F]
    [InnerProductSpace ℝ F] [CompleteSpace F] (f : F → ℝ) (x : F) :
    riemannianGradient 𝓘(ℝ, F) f x = gradient f x

Uses 2

Statement usesRiemannian gradient

Proof usesPairing of the Riemannian gradient with a tangent vector

TheoremThe Hessian on Euclidean space as an iterated directional derivative#✓fully proved

Let \(F\) be a finite-dimensional real inner product space, viewed as a Riemannian manifold with the metric given by its inner product, let \(f : F \to \mathbb{R}\) and let \(x \in F\). For all tangent vectors \(u, v\) at \(x\), identified with vectors of \(F\), the Hessian of \(f\) at \(x\) is the derivative at \(x\) in direction \(u\) of the function \(y \mapsto Df(y)(v)\), where \(Df(y)\) is the Fréchet derivative of \(f\) at \(y\): \(\nabla^2 f(u, v) = D\big(y \mapsto Df(y)(v)\big)(x)(u)\).

A Fréchet derivative that does not exist is taken to be \(0\), so no hypothesis on \(f\) is needed.

theorem hessian_vectorSpace {F : Type*} [NormedAddCommGroup F] [InnerProductSpace ℝ F]
    [FiniteDimensional ℝ F] (f : F → ℝ) (x : F) (u v : TangentSpace 𝓘(ℝ, F) x) :
    hessian 𝓘(ℝ, F) f x u v =
      fderiv ℝ (fun y => fderiv ℝ f y ((NormedSpace.fromTangentSpace x) v)) x
        ((NormedSpace.fromTangentSpace x) u)

Uses 3 · Used by 3

Statement usesCovariant Hessian

Proof usesThe Levi-Civita connection of Euclidean space kills constant vector fields · Extending a tangent vector of a normed space gives a constant vector field

Used byLaplacian on a vector space as a sum of second directional derivatives · The Laplacian on a vector space is the flat Laplacian at twice-differentiable points · The Hessian on Euclidean space is the second derivative

TheoremThe Hessian on Euclidean space is the second derivative#✓fully proved

Let \(F\) be a finite-dimensional real inner product space, viewed as a Riemannian manifold with the metric given by its inner product, let \(f : F \to \mathbb{R}\) and let \(x \in F\). If the Fréchet derivative \(y \mapsto Df(y)\) of \(f\) is differentiable at \(x\), then for all tangent vectors \(u, v\) at \(x\), identified with vectors of \(F\), the Hessian of \(f\) at \(x\) is the second Fréchet derivative: \(\nabla^2 f(u, v) = D^2 f(x)(u)(v)\), where \(D^2 f(x)\) is the derivative of \(Df\) at \(x\).

theorem hessian_vectorSpace_eq_fderiv_fderiv {F : Type*} [NormedAddCommGroup F]
    [InnerProductSpace ℝ F] [FiniteDimensional ℝ F] (f : F → ℝ) (x : F)
    (u v : TangentSpace 𝓘(ℝ, F) x) (h : DifferentiableAt ℝ (fderiv ℝ f) x) :
    hessian 𝓘(ℝ, F) f x u v =
      (fderiv ℝ (fderiv ℝ f) x ((NormedSpace.fromTangentSpace x) u))
        ((NormedSpace.fromTangentSpace x) v)

Uses 2 · Used by 5

Statement usesCovariant Hessian

Proof usesThe Hessian on Euclidean space as an iterated directional derivative

Used byLaplacian of the Gaussian potential · Laplacian of the squared norm · The Laplacian on a vector space is the flat Laplacian at twice-differentiable points · The Gaussian gradient Ricci soliton · Gaussian potentials that are gradient Ricci solitons

8 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.