Klein–Gordon initial-value problem: energy estimate on the cones of dependence

Open

TegmarkDimensionality.klein_gordon_energy_estimate

by Lucas · Oct 2, 2026 · Mathlib 0df444a (Lean v4.33.1)

mathematical-physicspdewell-posedness

Let $n\ge0$ , $\mu\in\mathbb R$ , and let $u(t,x)$ be a $C^2$ solution on $\mathbb R\times\mathbb R^n$ of the Klein–Gordon equation

\partial_t^2u=\nabla^2u-\mu^2u.

Let $e(t,x)=(\partial_tu)^2+|\nabla_xu|^2+\mu^2u^2$ be the energy density. Then for every $x_0\in\mathbb R^n$ and all $t,R$ with $|t|\le R$ ,

\int_{|x-x_0|<R-|t|}e(t,x)\,dx\;\le\;\int_{|x-x_0|<R}e(0,x)\,dx.

The data $(u,\partial_tu)$ at $t=0$ on the disk $|x-x_0|<R$ therefore control the solution, with finite error bars, throughout the two cones $|x-x_0|<R-|t|$ (future and past). Applied to the difference of two solutions, the inequality shows that such data determine the solution uniquely in those cones. This is the well-posedness of the hyperbolic initial-value problem described in the paper.

Preamble

import Mathlib
import Definitions.Def_tegmark_laplacian
open MeasureTheory

Formal statement

namespace TegmarkDimensionality

/-- Well-posedness of the initial-value problem for the Klein–Gordon equation
`u_tt = ∇²u - μ² u` on `ℝ × ℝⁿ`: the energy of a `C²` solution in the ball of radius
`R - |t|` about `x₀` at time `t` is bounded by the energy of the initial data in the ball
of radius `R` about `x₀`, for `|t| ≤ R`.  In particular the data `(u, u_t)` on the disk
`|x - x₀| < R` at `t = 0` determine `u` in the two cones `|x - x₀| < R - |t|`. -/
theorem klein_gordon_energy_estimate (n : ℕ) (μ : ℝ)
    (u : ℝ → EuclideanSpace ℝ (Fin n) → ℝ)
    (hu : ContDiff ℝ 2 (fun p : ℝ × EuclideanSpace ℝ (Fin n) => u p.1 p.2))
    (hKG : ∀ t x, deriv (fun s => deriv (fun s' => u s' x) s) t =
      laplacian (u t) x - μ ^ 2 * u t x)
    (x₀ : EuclideanSpace ℝ (Fin n)) (R t : ℝ) (ht : |t| ≤ R) :
    ∫ x in Metric.ball x₀ (R - |t|),
        ((deriv (fun s => u s x) t) ^ 2 + ‖fderiv ℝ (u t) x‖ ^ 2 + μ ^ 2 * (u t x) ^ 2) ≤
      ∫ x in Metric.ball x₀ R,
        ((deriv (fun s => u s x) 0) ^ 2 + ‖fderiv ℝ (u 0) x‖ ^ 2 + μ ^ 2 * (u 0 x) ^ 2) := by sorry

end TegmarkDimensionality

Source

M. Tegmark, *On the dimensionality of spacetime*, Class. Quantum Grav. 14 (1997) L69–L75, https://doi.org/10.1088/0264-9381/14/4/002, p. L73, sixth paragraph ('Hyperbolic equations ... allow well-posed initial-value problems ... specifying initial data (u and u̇) for the Klein–Gordon equation on the shaded disk in figure 3 determines the solution in the volumes bounded by the two cones')

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic)

NON-BLIND READ-BACK — NOT INDEPENDENT TESTIMONY. This read-back was written by the same agent (Aristotle, by Harmonic) that drafted the Lean statement below, with full knowledge of the source paper and of the intended meaning. It was not produced by a blind, independent auditor, so it may share the drafter's blind spots. Reviewers must not treat it as independent confirmation of faithfulness; compare the Lean code against the source directly.

Let $n$ be a natural number, $\mu$ a real number, and $u:\mathbb R\times\mathbb R^n\to\mathbb R$ , written $u(t,x)$ . Assume:

$(t,x)\mapsto u(t,x)$ is twice continuously differentiable;
for all $t,x$ : $\partial_t^2u(t,x)=\nabla^2_x u(t,x)-\mu^2u(t,x)$ , where $\partial_t^2$ is the iterated one-variable derivative in $t$ and $\nabla^2_x$ is the Laplacian in $x$ (sum of pure second derivatives along the standard basis).

Let $x_0\in\mathbb R^n$ and $R,t\in\mathbb R$ with $|t|\le R$ . The theorem asserts

\int_{B(x_0,R-|t|)}\Big((\partial_tu(t,x))^2+\|D_xu(t,x)\|^2+\mu^2u(t,x)^2\Big)dx\ \le\ \int_{B(x_0,R)}\Big((\partial_tu(0,x))^2+\|D_xu(0,x)\|^2+\mu^2u(0,x)^2\Big)dx,

where $B(x_0,\rho)$ is the open Euclidean ball, empty if $\rho\le0$ , $\|D_xu\|$ is the operator norm of the spatial derivative (equal to the length of the spatial gradient), and the integrals are against Lebesgue measure. When $|t|=R$ the left side is an integral over the empty set, hence $0$ .

Human review

Endorsed by Shuze Chen · Oct 2, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 2, 2026
Confirmed by the mission captain (proposal self-audit).

View graph