OAI/Geometry/RCD/Sobolev/HessianActionInput.lean

finite-span Hessian action bounds

Gigli, arXiv:1407.0809v1, equation (3.1.9), p. 99, and Theorem 3.3.8, equations (3.3.18)--(3.3.19), p. 110, give the three-term Hessian action and its Hilbert--Schmidt bound. Han, JGA 28 (2018), Proposition 3.2, p. 1302, and Theorem 3.3, p. 1305, give the top-dimensional trace identity and the strengthened Bochner inequality on every local-dimensional stratum. Completing the trace-defect square gives the shifted-square bound also when the local dimension is less than n. Tensor Cauchy--Schwarz then gives the displayed product of the two direction bounds.

This input retains only the n+2-dimensional local Poisson span. It is separate from the integrated Hessian input, because the commutator needs actions in arbitrary gradient directions, not only zero-boundary tests.