Weak Derivatives of Hessian Adjugates

Let $u:\mathbb{R}^n\to\mathbb{R}$ and let $T$ be a tensor giving locally $L^2$ weak directional derivatives of every Hessian entry $H_u{}_{ij}$. Assume every Hessian entry is globally in $L^{\infty}$. Then, for every coordinate direction $e_k$ and indices $i,j$, there exists a function $g$ such that

in the weak sense, and $g$ belongs locally to $L^2$ on every compact set. The declaration is a cofactor-polynomial consequence of the supplied weak Hessian data and does not assume classical differentiability of the Hessian.

Original Lean declaration header

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

theorem exists_weak_hessian_adjugate_derivative {n : ℕ}
    {u : EuclideanSpace ℝ (Fin n) → ℝ}
    {T : EuclideanSpace ℝ (Fin n) → Fin n → Fin n → Fin n → ℝ}
    (hbound : ∀ r s : Fin n, MemLp (fun x => hessianMatrix u x r s)
      (⊤ : ENNReal) (volume : Measure (EuclideanSpace ℝ (Fin n))))
    (hT : ∀ k i j : Fin n,
      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))
    (k i j : Fin n) :
    ∃ g : EuclideanSpace ℝ (Fin n) → ℝ,
      HasWeakDerivAlong (fun x => (hessianMatrix u x).adjugate i j) g
        (EuclideanSpace.basisFun (Fin n) ℝ k) ∧
      ∀ S : Set (EuclideanSpace ℝ (Fin n)), IsCompact S →
        MemLp g 2 ((volume : Measure (EuclideanSpace ℝ (Fin n))).restrict S)

Module navigation

Module: Analysis/Matrix/Piola.

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

Supporting theorems: hasWeakDerivAlong_det_of_locally_memLp_two, hasWeakDerivAlong_of_contDiff.

Previous: integrable_inv_hessianMatrix_mul_of_bounded_compact.

Source excerpt, lines 1084–1100 · Frozen source 408915f.