The Laplacian as the trace of the Hessian endomorphism #
For a scalar function f on a finite-dimensional real inner product space E, the derivative of
the gradient, TauCeti.iteratedGradientChain f 1 x : E →L[ℝ] E, is the Hessian of f at x
represented as an endomorphism of E. This file records that its trace is the Laplacian:
Δ f x = tr (D∇f x). The identity is basis-free, and holds without any differentiability
hypothesis because both sides are built from Mathlib's totalized Fréchet derivative.
It is the classical form of the statement that the Laplacian of a Sobolev function in
W^{2,p} is the trace of its weak Hessian, which identifies Δ with a bounded linear image of the
second derivatives in Lᵖ estimates.
Main declarations #
TauCeti.laplacian_eq_trace_iteratedGradientChain_one:Δ f x = tr (D∇f x).
The Laplacian is the trace of the Hessian endomorphism. For every scalar function f and
every point x, Δ f x is the trace of the derivative of the gradient of f at x. No
differentiability is needed: both sides use Mathlib's totalized Fréchet derivative.