Weak Third Derivatives of the Hessian

This formalizes a weak local regularity statement associated with Theorem 2.5 of Letwin (arXiv:2607.24164v1).

For $u,V:\mathbb{R}^n\to\mathbb{R}$, assume $u$ is $C^1$ and convex, $\nabla u$ is globally Lipschitz, $V$ is $C^1$ and convex, and $-u+V\circ\nabla u$ is Lipschitz. Assume also that $K>0$, that almost everywhere

and that for some $D\in\mathbb{R}$,

for all $x,h$. Then there exists a tensor $T(x,k,i,j)$ such that every Hessian entry $H_u(x)_{ij}$ has weak derivative $T(x,k,i,j)$ in the coordinate direction $e_k$, and each such derivative belongs locally to $L^2$ on every compact set. This is a technical weak-derivative conclusion and does not assert classical third derivatives.

Original Lean declaration header

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

theorem exists_weak_third_derivative {n : ℕ} {u V : EuclideanSpace ℝ (Fin n) → ℝ}
    (hu : ContDiff ℝ 1 u) (hconv : ConvexOn ℝ univ u) {G : NNReal}
    (hG : LipschitzWith G (gradient u)) (hV : ContDiff ℝ 1 V) (hVc : ConvexOn ℝ univ V)
    {LF : NNReal} (hF : LipschitzWith LF (fun x => -u x + V (gradient u x))) {K : ℝ} (hK : 0 < K)
    (hdata : ∀ᵐ x ∂(volume : Measure (EuclideanSpace ℝ (Fin n))),
      (hessianMatrix u x).PosDef ∧
      Real.log (hessianMatrix u x).det = -u x + V (gradient u x) ∧
      (K • (1 : Matrix (Fin n) (Fin n) ℝ) - hessianMatrix u x).PosSemidef)
    {D : ℝ} (hw : ∀ x h, u (x + h) + u (x - h) - 2 * u x ≤ D * ‖h‖ ^ 2) :
    ∃ T : EuclideanSpace ℝ (Fin n) → Fin n → Fin n → Fin n → ℝ, ∀ k i j,
      HasWeakDerivAlong (fun x => hessianMatrix u x i j) (fun x => T x k i j)
          (EuclideanSpace.basisFun (Fin n) ℝ k) ∧
        ∀ S : Set (EuclideanSpace ℝ (Fin n)), IsCompact S →
          MemLp (fun x => T x k i j) 2 ((volume : Measure (EuclideanSpace ℝ (Fin n))).restrict S)

Module navigation

Module: Analysis/Convex/HessianRegularity.

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

Supporting theorems: exists_hasWeakDerivAlong_of_forall_cutoff, exists_hasWeakDerivAlong_of_sq_difference_le, exists_hessian_cutoff_sq_difference_bound, memLp_cutoff_mul_hessianMatrix_entry, norm_hessianMatrix_entry_le_of_lipschitz_gradient.

Source excerpt, lines 18–31 · Frozen source 408915f.