Almost-Everywhere Symmetry of Weak Third Derivatives

This is a weak-coordinate symmetry statement for third derivatives.

Let $u:\operatorname{EuclideanSpace}(\mathbb R,\operatorname{Fin}(n))\to\mathbb R$ be $C^1$ with Lipschitz gradient. Let $T(x,k,i,j)$ be such that, for every $k,i,j<n$, the function $T(\cdot,k,i,j)$ is a weak derivative along $e_k$ of the Hessian entry $H_{ij}=\operatorname{hessianMatrix}(u,\cdot)_{ij}$. Then, for almost every $x$, simultaneously for all $k,i,j$,

The first equality exchanges the derivative and first Hessian indices; the second expresses symmetry in the Hessian indices. The declaration ae_weak_third_derivative_symm_readable is an almost-everywhere identification result and does not assert that a classical third derivative exists.

Original Lean declaration header

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

theorem ae_weak_third_derivative_symm {n : ℕ} {u : EuclideanSpace ℝ (Fin n) → ℝ} (hu : ContDiff ℝ 1 u)
    {G : NNReal} (hG : LipschitzWith G (gradient u))
    {T : EuclideanSpace ℝ (Fin n) → Fin n → Fin n → Fin n → ℝ}
    (hT : ∀ k i j, HasWeakDerivAlong (fun x => hessianMatrix u x i j) (fun x => T x k i j)
      (EuclideanSpace.basisFun (Fin n) ℝ k)) :
    ∀ᵐ x ∂(volume : Measure (EuclideanSpace ℝ (Fin n))),
      ∀ k i j, T x k i j = T x i k j ∧ T x k i j = T x k j i

Module navigation

Module: Analysis/BakryEmery/WeakHessian.

Definition modules: Analysis/BakryEmery/HessianOperator, Analysis/WeakDerivative/Basic.

Supporting theorems: hasWeakDerivAlong_of_lipschitz.

Next: norm_hessianMatrix_entry_le_of_lipschitz_gradient.

Source excerpt, lines 160–166 · Frozen source 408915f.