Integrability of Compact Multipliers Against Inverse Hessian Entries

This is an integrability component related to Theorem 2.5 of Letwin (arXiv:2607.24164v1).

Let $u,F,f:\operatorname{EuclideanSpace}\,\mathbb R\,(\operatorname{Fin}(n))\to\mathbb R$, let $G\in\mathbb R_{\ge0}$, and assume:

1. $\nabla u$ is Lipschitz with constant $G$;
2. $F$ is continuous;
3. almost everywhere,

$$\det(\operatorname{hessianMatrix}(u,x))=e^{F(x)};$$

4. $f$ is measurable and compactly supported;
5. there is $C\in\mathbb R$ with $\|f(x)\|\le C$ for every $x$.

Then for every $i,j$,

$$x\mapsto \bigl(\operatorname{hessianMatrix}(u,x)^{-1}\bigr)_{ij}f(x)$$

is integrable with respect to volume.

The determinant identity is only assumed almost everywhere, and the conclusion concerns individual inverse-matrix entries rather than a matrix-valued integral.

Original Lean declaration header

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

theorem integrable_inv_hessianMatrix_mul_of_bounded_compact {n : ℕ}
    {u F f : EuclideanSpace ℝ (Fin n) → ℝ}
    {G : NNReal} (hG : LipschitzWith G (gradient u)) (hF : Continuous F)
    (hdet : ∀ᵐ x ∂(volume : Measure (EuclideanSpace ℝ (Fin n))),
      (hessianMatrix u x).det = Real.exp (F x))
    (hf : Measurable f) (hfc : HasCompactSupport f)
    {C : ℝ} (hC : ∀ x, ‖f x‖ ≤ C) (i j : Fin n) :
    Integrable (fun x => (hessianMatrix u x)⁻¹ i j * f x)
      (volume : Measure (EuclideanSpace ℝ (Fin n)))

Module navigation

Module: Analysis/Matrix/Piola.

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

Previous: sum_integral_inv_hessianMatrix_mul_fderiv_eq · Next: exists_weak_hessian_adjugate_derivative.

Source excerpt, lines 1019–1027 · Frozen source 408915f.

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Matrix_Piola

open FunctionalInequalities.Probability.Stein
open MeasureTheory Set Filter

theorem FunctionalInequalities.Analysis.integrable_inv_hessianMatrix_mul_of_bounded_compact_readable {n : ℕ}
    {u F f : EuclideanSpace ℝ (Fin n) → ℝ}
    {G : NNReal} (hG : LipschitzWith G (gradient u)) (hF : Continuous F)
    (hdet : ∀ᵐ x ∂(volume : Measure (EuclideanSpace ℝ (Fin n))),
      (hessianMatrix u x).det = Real.exp (F x))
    (hf : Measurable f) (hfc : HasCompactSupport f)
    {C : ℝ} (hC : ∀ x, ‖f x‖ ≤ C) (i j : Fin n) :
    Integrable (fun x => (hessianMatrix u x)⁻¹ i j * f x)
      (volume : Measure (EuclideanSpace ℝ (Fin n))) := by sorry