Convolution Hessian Quadratic Form Integral Formula

This is a technical identity relating the Hessian of a convolution to an integral of directional second derivatives.

Let $n\in\mathbb N$, let $\rho,u:\mathbb R^n\to\mathbb R$, and assume that $\rho$ is $C^2$ with compact support and that $u$ is continuous. For every $x,v\in\mathbb R^n$, the quadratic form of the coordinate Hessian of the convolution $\rho*u$ satisfies

Here hessianMatrix denotes the coordinate Hessian and convolution uses Lebesgue volume measure. The result provides the integral representation needed to transfer pointwise second-order information through mollification.

Original Lean declaration header

Within namespace FunctionalInequalities.Analysis. Shown in its original module context. Proof omitted.

private lemma convolution_hessian_integral {n : ℕ}
    {ρ u : EuclideanSpace ℝ (Fin n) → ℝ}
    (hρ : ContDiff ℝ 2 ρ) (hρc : HasCompactSupport ρ) (hu : Continuous u)
    (x v : EuclideanSpace ℝ (Fin n)) :
    ⟪v, Matrix.toEuclideanLin
      (hessianMatrix (convolution ρ u (ContinuousLinearMap.lsmul ℝ ℝ) volume) x) v⟫ =
      ∫ y, u y * iteratedFDeriv ℝ 2 (fun z => ρ (x - z)) y (fun _ => v)

Module navigation

Module: Analysis/Convex/Viscosity.

Definition modules: Analysis/BakryEmery/HessianOperator.

Supporting theorems: tendsto_integral_secondDifference_mul, expansion_secondDifference, hessianMatrix_quadratic, local_taylor_two.

Previous: expansion_secondDifference · Next: trace_integral_bound.

Source excerpt, lines 1091–1097 · Frozen source 408915f.