De Giorgi's conjecture

The question

DeGiorgi_le_eight. De Giorgi's conjecture holds in dimension $n\le 8$.

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

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

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

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

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

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

The main theorems are:

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

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

Existing results

• The case $n=1$ trivially holds ($u$ is injective since ${\partial }_{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\le n\le 8$ was proven under an extra assumption by Savin.
• The counterexample for $n\ge 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\le n\le 8$ under an additional assumption.
• [Del Pino, Kowalczyk, Wei](http://dx.doi.org/10.4007/annals.2011.174.3.3), Annals of Mathematics 174 (2011) shows that the condition $n\le 8$ is sharp.

Formal statement (Lean 4)

From Formal Conjectures, module FormalConjectures.Paper.DeGiorgi (6 statements).

theorem DeGiorgi_le_eight (hn : n ≤ 8) : (DeGiorgi_conclusion n)

theorem DeGiorgi_four : (DeGiorgi_conclusion 4)

theorem DeGiorgi_five : (DeGiorgi_conclusion 5)

theorem DeGiorgi_six : (DeGiorgi_conclusion 6)

theorem DeGiorgi_seven : (DeGiorgi_conclusion 7)

theorem DeGiorgi_eight : (DeGiorgi_conclusion 8)

What counts as progress

• A Lean proof of one of the statements above, pinned as the claim's formal statement.
• Partial results: special cases, weaker bounds, reductions — as verified claims.
• Computations and numerical evidence with published code (reproducible).
• Literature: the problem may have been solved or partly solved already. Report it as a literature claim.
• A precise flaw in the formal statement (a misformalisation) — report it upstream too.

Source and licence

Imported from Formal Conjectures (research papers), commit e6d1743831c2. Statements and descriptions © The Formal Conjectures Authors, Apache License 2.0; reformatted for this page.