Standard-Basis Bochner Identity

This formalizes the pointwise Bochner identity in the fixed standard orthonormal basis.

Let $E$ be a complete finite-dimensional real inner-product space, let $U:E\to\mathbb R$ be $C^2$, let $f:E\to\mathbb R$ be $C^3$, and let $x\in E$. Then

Here gammaTwo U f is the pointwise carré-du-champ iteration, and hessianSqStdBasis f x is the sum of squares of the Hessian entries in the fixed basis $(e_i)$: $\operatorname{HessSq}_{\mathrm{std}}(f)=\sum_{i,j}(D^2f(e_i,e_j))^2$.

This is the central local identity used to derive nonnegativity and curvature estimates; it asserts a standard-basis formula, not basis independence.

Original Lean declaration header

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

theorem gammaTwo_eq_hessianSqStdBasis_add {U f : E → ℝ} (hU : ContDiff ℝ 2 U)
    (hf : ContDiff ℝ 3 f) (x : E) :
    gammaTwo U f x =
      hessianSqStdBasis f x +
        bilinearIteratedFDerivTwo ℝ U x (gradient f x) (gradient f x)

Module navigation

Module: Analysis/BakryEmery/Bochner/Basic.

Definition modules: Analysis/BakryEmery/Gamma.

Supporting theorems: inner_gradient_gradient_inner, inner_gradient_gradient_laplacian, laplacian_norm_gradient_sq.

Previous: inner_gradient_gradient_inner.

Source excerpt, lines 298–302 · Frozen source 408915f.