Prove2Me

Radial integral potential recovers a closed Hessian on R3\mathbb{R}^3

Proved
NewtonCartan.radPot_hessian_eq

by Ethan Cheung Wang · Oct 21, 2026 · Mathlib 0df444a (Lean v4.33.1)

analysisnewton-cartanpoincare

Let H:R3→Sym3(R)H:\mathbb{R}^3\to\mathrm{Sym}_3(\mathbb{R}) be smooth, and assume the Hessian closedness condition

∂kHij=∂jHik\partial_k H_{ij}=\partial_j H_{ik}

for all indices. Define the radial potential

φ(y)=∑i,j=13∫01(1−s) Hij(sy) yiyj ds.\varphi(y)=\sum_{i,j=1}^{3}\int_0^1(1-s)\,H_{ij}(sy)\,y_i y_j\,ds.

Then φ\varphi is smooth and

∂j∂iφ(y)=Hij(y)\partial_j\partial_i\varphi(y)=H_{ij}(y)

for all yy and all spatial indices i,ji,j.

This is the standard integral form of Taylor's theorem with vanishing jet at the origin, specialized to recovering a potential from its Hessian; it is the key identity used to assemble a spacetime potential from slicewise spatial Hessians in Trautman recovery.

Preamble
import Definitions.Def_NewtonCartan_defs
import Theorems.Thm_NewtonCartan_exists_potential_of_closed_hessian_Sp
import Mathlib.Analysis.Calculus.ContDiff.Basic
import Mathlib.Analysis.Calculus.ContDiff.Operations
import Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

open scoped ContDiff BigOperators Topology Interval
open Classical MeasureTheory
open NewtonCartan
Formal statement
namespace NewtonCartan

theorem radPot_hessian_eq
    (H : Sp → Fin 3 → Fin 3 → ℝ) (hH : ContDiff ℝ ∞ H)
    (hsym : ∀ y i j, H y i j = H y j i)
    (hclosed : ∀ y i j k,
      fderiv ℝ (fun z => H z i j) y (Pi.single k 1) =
        fderiv ℝ (fun z => H z i k) y (Pi.single j 1)) :
    let φ : Sp → ℝ := fun y =>
      ∑ i : Fin 3, ∑ j : Fin 3,
        ∫ s in (0 : ℝ)..1, (1 - s) * H (s • y) i j * y i * y j
    ContDiff ℝ ∞ φ ∧
      ∀ y i j, fderiv ℝ (fun z => fderiv ℝ φ z (Pi.single i 1)) y (Pi.single j 1) =
        H y i j := by sorry

end NewtonCartan
Source
Classical multivariable calculus (Taylor with integral remainder); Trautman/Malament Newton–Cartan recovery Prop. 2.2

View graph