Almost-Everywhere Hessian Chain Rule for a Profile

This is an almost-everywhere chain rule for Hessians.

Let $u:\mathbb R^n\to\mathbb R$ be $C^1$ with Lipschitz gradient, and let $\zeta:\mathbb R\to\mathbb R$ be $C^2$. Then, for almost every $x$ and all $i,j\in\operatorname{Fin} n$,

In Lean, the Hessian is the coordinate matrix hessianMatrix, and the first derivatives are expressed using fderiv on the Euclidean basis. This identity supports the inverse-Hessian cutoff calculations.

Original Lean declaration header

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

private theorem ae_hessianMatrix_comp_profile {n : ℕ}
    {u : EuclideanSpace ℝ (Fin n) → ℝ} {ζ : ℝ → ℝ} {G : NNReal}
    (hu : ContDiff ℝ 1 u) (hG : LipschitzWith G (gradient u))
    (hζ : ContDiff ℝ 2 ζ) :
    ∀ᵐ x ∂(volume : Measure (EuclideanSpace ℝ (Fin n))), ∀ i j : Fin n,
      hessianMatrix (fun y => ζ (u y)) x i j =
        deriv ζ (u x) * hessianMatrix u x i j +
          deriv (deriv ζ) (u x) *
            fderiv ℝ u x (EuclideanSpace.basisFun (Fin n) ℝ i) *
            fderiv ℝ u x (EuclideanSpace.basisFun (Fin n) ℝ j)

Module navigation

Module: Analysis/BakryEmery/IntegrationByParts/InverseHessian/WeakCutoff.

Definition modules: Analysis/BakryEmery/HessianOperator.

Previous: integral_profile_inverse_energy_eq_drift · Next: exists_C1_height_generator_defect_bound.

Source excerpt, lines 373–382 · Frozen source 408915f.