Weak Derivative of the Inverse Hessian

Let $u,F:\mathbb{R}^n\to\mathbb{R}$, let $\nabla u$ be Lipschitz, let $F$ be Lipschitz, and assume that almost everywhere the Hessian $H_u$ is positive definite and

Suppose a tensor $T$ gives locally $L^2$ weak directional derivatives of the entries of $H_u$. Then, for every coordinate direction $e_k$ and indices $i,j$, the inverse Hessian has weak derivative

and this derivative is locally in $L^2$ on compact sets. The inverse-Hessian entries themselves are locally in $L^{\infty}$ on compact sets. This is a weak calculus statement and does not assume $C^2$ regularity.

Original Lean declaration header

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

theorem hasWeakDerivAlong_inverse_hessian_of_logdet {n : ℕ}
    {u F : EuclideanSpace ℝ (Fin n) → ℝ} {G LF : NNReal}
    {T : EuclideanSpace ℝ (Fin n) → Fin n → Fin n → Fin n → ℝ}
    (hG : LipschitzWith G (gradient u)) (hF : LipschitzWith LF F)
    (hdata : ∀ᵐ x ∂(volume : Measure (EuclideanSpace ℝ (Fin n))),
      (hessianMatrix u x).PosDef ∧ Real.log (hessianMatrix u x).det = F x)
    (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,
      HasWeakDerivAlong (fun x => (hessianMatrix u x)⁻¹ i j)
        (fun x => -(((hessianMatrix u x)⁻¹ *
          (Matrix.of fun a b => T x k a b) * (hessianMatrix u x)⁻¹) i j))
        (EuclideanSpace.basisFun (Fin n) ℝ k) ∧
      (∀ S : Set (EuclideanSpace ℝ (Fin n)), IsCompact S →
        MemLp (fun x => -(((hessianMatrix u x)⁻¹ *
          (Matrix.of fun a b => T x k a b) * (hessianMatrix u x)⁻¹) i j)) 2
          ((volume : Measure (EuclideanSpace ℝ (Fin n))).restrict S)) ∧
      ∀ S : Set (EuclideanSpace ℝ (Fin n)), IsCompact S →
        MemLp (fun x => (hessianMatrix u x)⁻¹ i j) (⊤ : ENNReal)
          ((volume : Measure (EuclideanSpace ℝ (Fin n))).restrict S)

Module navigation

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

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

Selected supporting theorems: HasWeakDerivAlong.congr_ae, HasWeakDerivAlong.mul_of_locally_bounded, ae_weak_matrix_inverse_derivative, exists_weak_hessian_adjugate_derivative, hasWeakDerivAlong_exp_neg_of_lipschitz.

Previous: integrable_weak_generator_densities · Next: integral_mul_generator_eq_neg_energy_of_contDiff_one.

Source excerpt, lines 1053–1076 · Frozen source 408915f.