Lemma 1 — spherical symmetrization increases $(\Delta f)^2-\|f_{ij}\|^2$

Proved

FlatlyFoliated.lemma1_symmetrization

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

elliptic-pdegeneral-relativitymathematical-physics

Let $\Lambda>0$ and let $f$ be smooth on $\mathbb R^3$ with $\Delta f>0$ (arrow-of-time convention), approximately spherically symmetric at infinity, and satisfying

(\Delta f)^2-\|f_{ij}\|^2=2\Lambda\quad\text{on }\mathbb R^3 .

Then its spherical symmetrization $\bar f$ satisfies

(\Delta\bar f)^2-\|\bar f_{ij}\|^2\ \ge\ 2\Lambda\quad\text{on }\mathbb R^3,

and equality holds everywhere if and only if $f$ is spherically symmetric.

Preamble

import Mathlib
import Definitions.Def_FlatlyFoliatedRelativity_basic

open scoped ContDiff

Formal statement

namespace FlatlyFoliated

/-- Lemma 1: symmetrization increases `(Δf)² − ‖fᵢⱼ‖²`, with equality iff `f` is
spherically symmetric. -/
theorem lemma1_symmetrization (Λ : ℝ) (hΛ : 0 < Λ) (f : R3 → ℝ) (hf : ContDiff ℝ ∞ f)
    (hconv : ∀ x, 0 < lap f x) (happrox : ApproxSphSymmAtInfty f)
    (heq : ∀ x, lap f x ^ 2 - hessNormSq f x = 2 * Λ) :
    (∀ x, 2 * Λ ≤ lap (sphSymmetrization f) x ^ 2 - hessNormSq (sphSymmetrization f) x) ∧
    ((∀ x, lap (sphSymmetrization f) x ^ 2 - hessNormSq (sphSymmetrization f) x = 2 * Λ) ↔
      IsSphSymm f) := by sorry

end FlatlyFoliated

Source

Bray, Hamm, Hirsch, Wheeler, Zhang, Flatly Foliated Relativity, arXiv:1911.00967v2, https://arxiv.org/abs/1911.00967, p. 17, Lemma 1 (eqs. (78)–(81))

Human review

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

View graph

Lemma 1 — spherical symmetrization increases (Δf)2−∥fij∥2(\Delta f)^2-\|f_{ij}\|^2(Δf)2−∥fij​∥2

Lemma 1 — spherical symmetrization increases $(\Delta f)^2-\|f_{ij}\|^2$