Eq. (7.31) — $\int(\nabla_i\nabla_j\chi)^2 = \int(\nabla^2\chi)^2$

Proved

Verlinde2016.hessian_sq_integral_eq_laplacian_sq

by Lucas · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

emergent-gravitymathematical-physicsverlinde-2016

For a function $\chi$ on $n$ -dimensional Euclidean space that falls off fast enough that no boundary terms arise, a double integration by parts gives (summation over $i,j$ )

\int (\nabla_i\nabla_j\chi)^2\,dV = \int (\nabla^2\chi)^2\,dV .

Formalization: "falls off rapidly enough" is taken as $\chi$ being $C^\infty$ with compact support, a sufficient condition for the absence of boundary terms.

Preamble

import Mathlib
import Definitions.Def_Verlinde2016_Defs

open Real

Formal statement

namespace Verlinde2016

theorem hessian_sq_integral_eq_laplacian_sq {n : ℕ} (χ : EuclideanSpace ℝ (Fin n) → ℝ)
    (hχ : ContDiff ℝ (⊤ : ℕ∞) χ) (hχ_supp : HasCompactSupport χ) :
    ∑ i, ∑ j, ∫ x, partialDeriv i (partialDeriv j χ) x ^ 2
      = ∫ x, (∑ i, partialDeriv i (partialDeriv i χ) x) ^ 2 := by sorry

end Verlinde2016

Source

E. Verlinde, Emergent Gravity and the Dark Universe, SciPost Phys. 2, 016 (2017), arXiv:1611.02269v2, https://arxiv.org/abs/1611.02269, p. 35, eq. (7.31)

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) - same agent as drafter, non-blind

Non-blind read-back — not independent testimony. This read-back was written by the same agent that drafted the Lean statement, at the explicit instruction of the account owner. It was not produced blind by an independent auditor, and the author had seen the source paper and the intended meaning while writing it. Reviewers should not treat it as independent evidence of faithfulness and should check the Lean code directly.

Let $n$ be any natural number (including $0$ ) and let $\chi:\mathbb R^n\to\mathbb R$ , with $\mathbb R^n$ carrying its Euclidean structure, be

infinitely differentiable ( $C^\infty$ ) on all of $\mathbb R^n$ , and
of compact support (the closure of $\{x:\chi(x)\neq0\}$ is compact).

Write $\partial_i$ for the partial derivative in the direction of the $i$ -th standard basis vector (defined as the Fréchet derivative applied to $e_i$ , and $0$ where not differentiable). Then

\sum_{i=1}^{n}\sum_{j=1}^{n}\int_{\mathbb R^n}\big(\partial_i(\partial_j\chi)(x)\big)^2\,dx \;=\; \int_{\mathbb R^n}\Big(\sum_{i=1}^{n}\partial_i(\partial_i\chi)(x)\Big)^2\,dx,

with Lebesgue measure on $\mathbb R^n$ (Bochner integrals, which by convention are $0$ for non-integrable integrands). On the left each integral is taken separately and then summed. For $n=0$ both sides are $0$ .

View graph

Eq. (7.31) — ∫(∇i∇jχ)2=∫(∇2χ)2\int(\nabla_i\nabla_j\chi)^2 = \int(\nabla^2\chi)^2∫(∇i​∇j​χ)2=∫(∇2χ)2

Eq. (7.31) — $\int(\nabla_i\nabla_j\chi)^2 = \int(\nabla^2\chi)^2$