Ásgeirsson's mean value theorem for the ultrahyperbolic equation

Open

TegmarkDimensionality.asgeirsson_mean_value

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

mathematical-physicspdeultrahyperbolic

Let $n\ge0$ and let $u(x,y)$ be a $C^2$ function on $\mathbb R^n\times\mathbb R^n$ solving the ultrahyperbolic equation

\nabla_x^2u(x,y)=\nabla_y^2u(x,y).

Then for all $x_0,y_0\in\mathbb R^n$ and $r\in\mathbb R$ , the mean of $u$ over the sphere of radius $r$ about $x_0$ in the first variable equals its mean over the sphere of radius $r$ about $y_0$ in the second variable:

\int_{S^{n-1}}u(x_0+r\omega,\,y_0)\,d\sigma(\omega)=\int_{S^{n-1}}u(x_0,\,y_0+r\omega)\,d\sigma(\omega),

where $\sigma$ is the surface measure on the unit sphere.

The paper uses this theorem to show that data for hyperbolic equations on non-space-like surfaces, and all data for ultrahyperbolic equations, overdetermine the solution and lead to ill-posed problems.

Formalization Note $\sigma$ is Mathlib's measure on the unit sphere induced from Lebesgue measure (volume.toSphere). Both sides use the same normalization, so integrals and means coincide up to the same factor. Global $C^2$ regularity on $\mathbb R^n\times\mathbb R^n$ is assumed.

Preamble

import Mathlib
import Definitions.Def_tegmark_laplacian
open MeasureTheory

Formal statement

namespace TegmarkDimensionality

/-- Ásgeirsson's mean value theorem: if `u(x, y)` is `C²` on `ℝⁿ × ℝⁿ` and satisfies the
ultrahyperbolic equation `∇ₓ² u = ∇_y² u`, then for all `x₀, y₀` and `r` the mean of `u`
over the sphere of radius `r` about `x₀` in the `x`-variables (with `y = y₀`) equals the mean
over the sphere of radius `r` about `y₀` in the `y`-variables (with `x = x₀`). -/
theorem asgeirsson_mean_value (n : ℕ)
    (u : EuclideanSpace ℝ (Fin n) × EuclideanSpace ℝ (Fin n) → ℝ) (hu : ContDiff ℝ 2 u)
    (hU : ∀ x y, laplacian (fun x' => u (x', y)) x = laplacian (fun y' => u (x, y')) y)
    (x₀ y₀ : EuclideanSpace ℝ (Fin n)) (r : ℝ) :
    ∫ ω : Metric.sphere (0 : EuclideanSpace ℝ (Fin n)) 1, u (x₀ + r • (ω : EuclideanSpace ℝ (Fin n)), y₀) ∂(volume.toSphere) =
      ∫ ω : Metric.sphere (0 : EuclideanSpace ℝ (Fin n)) 1, u (x₀, y₀ + r • (ω : EuclideanSpace ℝ (Fin n))) ∂(volume.toSphere) := 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, seventh paragraph ('A corollary of a remarkable theorem by Asgeirsson [13] ...') and p. L74 ('Asgeirsson's theorem also applies to the ultrahyperbolic case'); L. Ásgeirsson, Math. Ann. 113 (1936) 321

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 and $u:\mathbb R^n\times\mathbb R^n\to\mathbb R$ , written $u(x,y)$ . Assume:

$u$ is twice continuously differentiable on the product space;
for all $x,y$ : $\nabla^2[x'\mapsto u(x',y)](x)=\nabla^2[y'\mapsto u(x,y')](y)$ , i.e. the Laplacian in the first variable equals the Laplacian in the second variable.

Then for all $x_0,y_0\in\mathbb R^n$ and every real $r$ , which may be zero or negative,

\int_{S}u(x_0+r\,\omega,\,y_0)\,d\sigma(\omega)=\int_{S}u(x_0,\,y_0+r\,\omega)\,d\sigma(\omega),

where $S=\{\omega\in\mathbb R^n:\|\omega\|=1\}$ is the unit sphere and $\sigma$ is the sphere measure induced from Lebesgue measure on $\mathbb R^n$ (Mathlib's toSphere). For $n=0$ the sphere is empty and both sides are $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