Weak Inverse-Hessian Row Divergence

This formalizes a supporting weak inverse-Hessian identity, cited as a partial formalization of Lemma 2.4 of Letwin (arXiv:2607.24164v1).

Let $u,F:\operatorname{EuclideanSpace}(\mathbb R,\operatorname{Fin}(n))\to\mathbb R$. Assume:

1. $u$ is $C^1$ with Lipschitz gradient, $F$ is Lipschitz, and almost everywhere $\det H=e^F$, where $H=\operatorname{hessianMatrix}(u,\cdot)$.
2. A tensor $T(x,k,a,b)$ is supplied together with weak directional derivatives of each entry $H(x)^{-1}_{ij}$, namely the derivative along $e_k$ is

$$-\bigl(H(x)^{-1}T(x,k)H(x)^{-1}\bigr)_{ij}.$$

3. These weak derivatives and inverse entries have the stated local $L^2$ and local $L^\infty$ (ENNReal exponent $\top$) membership on every compact set.

Then, for every row $b$, the vector field

$$x\mapsto\sum_a H(x)^{-1}_{ba}\,DF(x)e_a$$

belongs to $L^2$ on every compact set, and almost everywhere

$$\sum_a-\bigl(H(x)^{-1}T(x,a)H(x)^{-1}\bigr)_{ba} =-\sum_a H(x)^{-1}_{ba}\,DF(x)e_a.$$

The declaration ae_inverse_hessian_row_divergence_of_weak_derivative_readable is an interface theorem for a fixed weak inverse-derivative object; it does not construct $T$.

Original Lean conclusion excerpt

Within namespace FunctionalInequalities.Analysis. Shown in its original module context. Earlier hypotheses and the proof are omitted from this excerpt; the complete verified statement remains below.

          ((volume : Measure (EuclideanSpace ℝ (Fin n))).restrict S)) :
    ∀ b : Fin n,
      (∀ S : Set (EuclideanSpace ℝ (Fin n)), IsCompact S →
        MemLp
          (fun x => ∑ a : Fin n, (hessianMatrix u x)⁻¹ b a *
            fderiv ℝ F x (EuclideanSpace.basisFun (Fin n) ℝ a))
          2 ((volume : Measure (EuclideanSpace ℝ (Fin n))).restrict S)) ∧
      ∀ᵐ x ∂(volume : Measure (EuclideanSpace ℝ (Fin n))),
        (∑ a : Fin n, -(((hessianMatrix u x)⁻¹ *
          (Matrix.of fun c d => T x a c d) * (hessianMatrix u x)⁻¹) b a)) =
        -(∑ a : Fin n, (hessianMatrix u x)⁻¹ b a *
          fderiv ℝ F x (EuclideanSpace.basisFun (Fin n) ℝ a))

Module navigation

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

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

Supporting theorems: sum_integral_inv_hessianMatrix_mul_fderiv_eq.

Previous: integral_mul_generator_eq_neg_energy_of_contDiff_one.

Source excerpt, lines 1211–1222 · Frozen source 408915f.

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_BakryEmery_IntegrationByParts_InverseHessian_Weak

open MeasureTheory Set
open FunctionalInequalities.Probability.Stein

theorem FunctionalInequalities.Analysis.ae_inverse_hessian_row_divergence_of_weak_derivative_readable {n : ℕ}
    {u F : EuclideanSpace ℝ (Fin n) → ℝ}
    (hC1 : ContDiff ℝ 1 u) {G : NNReal} (hG : LipschitzWith G (gradient u))
    {LF : NNReal} (hF : LipschitzWith LF F)
    (hdet : ∀ᵐ x ∂(volume : Measure (EuclideanSpace ℝ (Fin n))),
      (hessianMatrix u x).det = Real.exp (F x))
    (T : EuclideanSpace ℝ (Fin n) → Fin n → Fin n → Fin n → ℝ)
    (hInv : ∀ 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)) :
    ∀ b : Fin n,
      (∀ S : Set (EuclideanSpace ℝ (Fin n)), IsCompact S →
        MemLp
          (fun x => ∑ a : Fin n, (hessianMatrix u x)⁻¹ b a *
            fderiv ℝ F x (EuclideanSpace.basisFun (Fin n) ℝ a))
          2 ((volume : Measure (EuclideanSpace ℝ (Fin n))).restrict S)) ∧
      ∀ᵐ x ∂(volume : Measure (EuclideanSpace ℝ (Fin n))),
        (∑ a : Fin n, -(((hessianMatrix u x)⁻¹ *
          (Matrix.of fun c d => T x a c d) * (hessianMatrix u x)⁻¹) b a)) =
        -(∑ a : Fin n, (hessianMatrix u x)⁻¹ b a *
          fderiv ℝ F x (EuclideanSpace.basisFun (Fin n) ℝ a)) := by sorry