Weak Derivative of a Composed Coordinate Derivative

This is a supporting weak-Hessian statement for the second evolution identity of Letwin (arXiv:2607.24164v1), equation (2.6).

Let $u,W:\mathbb R^n\to\mathbb R$. Assume $u\in C^1$, $u$ is globally Lipschitz, $\nabla u$ is globally Lipschitz, and $W\in C^2$. For each $a\in\mathrm{Fin}\ n$, there exists $C\in[0,\infty)$ such that $x\mapsto DW(\nabla u(x))[e_a]$ is $C$-Lipschitz. For every $j$, it has a weak derivative along $e_j$ given by

This derivative belongs to $L^2$ on every compact set. No global $L^2$ estimate or inverse-Hessian bound is asserted.

Original Lean declaration header

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

theorem exists_lipschitzWith_weak_fderiv_comp_gradient {n : ℕ}
    {u W : EuclideanSpace ℝ (Fin n) → ℝ} {L G : NNReal}
    (hu : ContDiff ℝ 1 u) (hULip : LipschitzWith L u)
    (hGradLip : LipschitzWith G (gradient u)) (hW : ContDiff ℝ 2 W)
    (a : Fin n) :
    ∃ C : NNReal,
      LipschitzWith C (fun x => fderiv ℝ W (gradient u x)
        (EuclideanSpace.basisFun (Fin n) ℝ a)) ∧
      ∀ j : Fin n,
        HasWeakDerivAlong
          (fun x => fderiv ℝ W (gradient u x) (EuclideanSpace.basisFun (Fin n) ℝ a))
          (fun x => ∑ b : Fin n, hessianMatrix u x j b * hessianMatrix W (gradient u x) b a)
          (EuclideanSpace.basisFun (Fin n) ℝ j) ∧
        ∀ S : Set (EuclideanSpace ℝ (Fin n)), IsCompact S →
          MemLp
            (fun x => ∑ b : Fin n, hessianMatrix u x j b * hessianMatrix W (gradient u x) b a)
            2 ((volume : Measure (EuclideanSpace ℝ (Fin n))).restrict S)

Module navigation

Module: Analysis/BakryEmery/IntegrationByParts/WeakHessianEvolution.

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

Supporting theorems: HasWeakDerivAlong.congr_ae, ae_fderiv_mongeAmpere_exponent, exists_lipschitzWith_neg_add_comp_gradient, hasWeakDerivAlong_of_lipschitz.

Next: hasWeakDerivAlong_mongeAmpere_first_rhs.

Source excerpt, lines 86–102 · Frozen source 408915f.