De Giorgi's conjecture

This file states a conjecture of De Giorgi about entire solutions to $Δ u + u - u^3 = 0$. The conjecture is a rigidity theorem: in spatial dimension $n ≤ 8$, the level sets of bounded solutions which satisfy $∂₁u > 0$ everywhere are hyperplanes. It has been shown that the condition $n ≤ 8$ is sharp.

The main theorems are:

• DeGiorgi_le_eight: the conjecture holds in dimension $n ≤ 8$.
• DeGiorgi_ge_nine: the conclusion of the conjecture does not hold if $n ≥ 9$.

The cases $1 ≤ n ≤ 8$ are also listed individually to enable partial solutions. The cases $1 ≤ n ≤ 3$ are solved, while $4 ≤ n ≤ 8$ remains open.

Existing results

• The case $n = 1$ trivially holds ($u$ is injective since $∂_1 u > 0$).
• The case $n = 2$ was proven by Ghoussoub and Gui.
• The case $n = 3$ was proven by Ambrosio and Cabré.
• The case $4 ≤ n ≤ 8$ was proven under an extra assumption by Savin.
• The counterexample for $n ≥ 9$ was proven by Del Pino, Kowalczyk, and Wei.

References

• Ghoussoub, Gui, Mathematische Annalen 311 (1998) proves the conjecture for $n = 2$.
• Ambrosio, Cabré, Journal of the American Mathematical Society 13 (2000) proves the conjecture for $n = 3$.
• Savin, Annals of Mathematics 169 (2009) proves the case $4 ≤ n ≤ 8$ under an additional assumption.
• Del Pino, Kowalczyk, Wei, Annals of Mathematics 174 (2011) shows that the condition $n ≤ 8$ is sharp.

structure DeGiorgi.IsBoundedSolution {n : ℕ} (u : EuclideanSpace ℝ (Fin n) → ℝ) : Prop

The function $u : ℝ^n → ℝ$ is a bounded classical solution to $Δ u + u - u^3 = 0$.

• regular : ContDiff ℝ 2 u
• bounded : ∃ (C : ℝ), ∀ (x : EuclideanSpace ℝ (Fin n)), |u x| ≤ C
• solution (x : EuclideanSpace ℝ (Fin n)) : Laplacian.laplacian u x + u x - u x ^ 3 = 0

def DeGiorgi.HasPositiveDeriv {n : ℕ} [NeZero n] (u : EuclideanSpace ℝ (Fin n) → ℝ) : Prop

The first partial derivative of $u : ℝ^n → ℝ$ is strictly positive.

Equations

• DeGiorgi.HasPositiveDeriv u = ∀ (x : EuclideanSpace ℝ (Fin n)), 0 < lineDeriv ℝ u x (EuclideanSpace.single 0 1)

def DeGiorgi.HasHyperplaneLevelSets {n : ℕ} (u : EuclideanSpace ℝ (Fin n) → ℝ) : Prop

The level sets of $u : ℝ^n → ℝ$ are hyperplanes. This is expressed by stating that there exists some affine subspace with rank $n - 1$ which coincides with the level set.

Equations

• DeGiorgi.HasHyperplaneLevelSets u = ∀ y ∈ Set.range u, ∃ (S : AffineSubspace ℝ (EuclideanSpace ℝ (Fin n))), u ⁻¹' {y} = ↑S ∧ Module.finrank ℝ ↥S.direction = n - 1

def DeGiorgi.DeGiorgi_conclusion (n : ℕ) [NeZero n] : Prop

The conclusion to De Giorgi's conjecture: if $u : ℝ^n → ℝ$ is a bounded classical solution to $Δ u + u - u^3 = 0$ satisfying $∂₁u > 0$ everywhere, then the level sets of $u$ are hyperplanes.

Equations

• DeGiorgi.DeGiorgi_conclusion n = ∀ (u : EuclideanSpace ℝ (Fin n) → ℝ), DeGiorgi.IsBoundedSolution u ∧ DeGiorgi.HasPositiveDeriv u → DeGiorgi.HasHyperplaneLevelSets u

theorem DeGiorgi.DeGiorgi_le_eight {n : ℕ} [NeZero n] (hn : n ≤ 8) : DeGiorgi_conclusion n

De Giorgi's conjecture holds in dimension $n ≤ 8$.

theorem DeGiorgi.DeGiorgi_ge_nine {n : ℕ} [NeZero n] (hn : n ≥ 9) : ¬DeGiorgi_conclusion n

In dimension $n ≥ 9$, the conclusion of De Giorgi's conjecture does not hold.

theorem DeGiorgi.DeGiorgi_one : DeGiorgi_conclusion 1

De Giorgi's conjecture trivially holds in dimension $n = 1$.

theorem DeGiorgi.DeGiorgi_two : DeGiorgi_conclusion 2

De Giorgi's conjecture holds in dimension $n = 2$.

theorem DeGiorgi.DeGiorgi_three : DeGiorgi_conclusion 3

De Giorgi's conjecture holds in dimension $n = 3$.

theorem DeGiorgi.DeGiorgi_four : DeGiorgi_conclusion 4

De Giorgi's conjecture holds in dimension $n = 4$.

theorem DeGiorgi.DeGiorgi_five : DeGiorgi_conclusion 5

De Giorgi's conjecture holds in dimension $n = 5$.

theorem DeGiorgi.DeGiorgi_six : DeGiorgi_conclusion 6

De Giorgi's conjecture holds in dimension $n = 6$.

theorem DeGiorgi.DeGiorgi_seven : DeGiorgi_conclusion 7

De Giorgi's conjecture holds in dimension $n = 7$.

theorem DeGiorgi.DeGiorgi_eight : DeGiorgi_conclusion 8

De Giorgi's conjecture holds in dimension $n = 8$.