Prove2Me

A decaying solution of the FFR drift equation vanishes

Proved
FlatlyFoliated.decaying_drift_eq_zero

by fizzyinc3 · Oct 17, 2026 · Mathlib 0df444a (Lean v4.33.1)

elliptic-pdemathematical-physics

Let η,u:R3→R\eta,u:\mathbb R^3\to\mathbb R be smooth functions, with η(x)>0\eta(x)>0 everywhere. If

η Δu=⟨∇η,∇u⟩,lim⁡∣x∣→∞u(x)=0,\eta\,\Delta u=\langle\nabla\eta,\nabla u\rangle, \qquad \lim_{|x|\to\infty}u(x)=0,

then

u(x)=0for every x∈R3.u(x)=0\quad\text{for every }x\in\mathbb R^3.

This is the maximum-principle implication used after equation (45) in the proof of Theorem 2. Taking u=∇⋅ζu=\nabla\cdot\zeta makes the elliptic FFR system divergence-free and permits recovery of the original FFR equations.

Formalization Note The equation is multiplied by the positive coefficient η\eta. The limit is along the cobounded filter on Euclidean three-space.

Preamble
import Definitions.Def_FlatlyFoliatedRelativity_basic

open scoped ContDiff
Formal statement
namespace FlatlyFoliated

theorem decaying_drift_eq_zero (η u : R3 → ℝ)
    (hη : ContDiff ℝ ∞ η) (hu : ContDiff ℝ ∞ u) (hηpos : ∀ x, 0 < η x)
    (heq : ∀ x, η x * lap u x = ∑ i, pd i η x * pd i u x)
    (hinf : Filter.Tendsto u (Bornology.cobounded R3) (nhds 0)) :
    ∀ x, u x = 0 := by sorry

end FlatlyFoliated
Source
Bray, Hamm, Hirsch, Wheeler, Zhang, Flatly Foliated Relativity, arXiv:1911.00967v2, p.10, proof of Theorem 2, equation (45) and the maximum-principle implication immediately following it. https://arxiv.org/html/1911.00967v2#Thmtheorem2

View graph