Das Morse-Lemma ist ein zentrales Lemma in der Geometrie negativ gekrümmter Räume. Es besagt, dass in einem negativ gekrümmten Raum alle Quasi-Geodäten durch “kleine” Deformationen von Geodäten entstehen, und es ist so etwas wie der ultimative Grund, warum die Geometrie in negativer Krümmung sich von der in unserer flachen Welt unterscheidet. In der flachen Ebene gibt es nämlich Quasigeodäten wie die logarithmische Spirale (Bild unten), die offensichtlich nicht durch Deformation einer Geraden entstehen.
Das Morse-Lemma stammt zwar schon aus den 20er Jahren, die ultimative Form mit den bestmöglichen Abschätzungen wurde aber erst vor einigen Jahren gefunden: in einem δ-hyperbolischen Raum ist jede (λ,C)-Quasigeodäte im Abstand Kλ2(C+δ) von einer Geodäte, wobei K in dieser Arbeit mit rund 37723 bestimmt wurde.
Maschinelle Theorembeweiser können inzwischen auch recht komplexe Definitionen und Beweise nachvollziehen. Zum Beispiel hat Sebastien Gouezel in den letzten Jahren die Grundlagen der Ergodentheorie, von Lp-Räumen und eben auch von δ-hyperbolischen Räumen im Theorembeweiser Isabelle implementiert, und dabei dann auch den Beweis der optimalen Konstanten im Morse-Lemma überprüft.
Wenn man sich den ursprünglichen Beweis anschaut, dann ist es schon recht erstaunlich, dass man sowas inzwischen mit dem Computer überprüfen kann. Bemerkenswerterweise wurde dann bei der Implementation noch ein Fehler im Beweis gefunden (eine Ungleichung ging in die falsche Richtung), und noch bemerkenswerter: mit dem computerüberprüften Beweis erhielt man nun zwar im Prinzip dieselbe Ungleichung, aber mit einer bessseren Konstante, nämlich K=92 statt wie vorher rund 37723. In einem δ-hyperbolischen Raum ist also jede (λ,C)-Quasigeodäte im Abstand höchsten 92λ2(C+δ) von einer Geodäten.
Sébastien Gouëzel, Vladimir Shchur (2018).
A corrected quantitative version of the Morse lemma ArXiv : arXiv:1810.04579 [math.GT]
Kommentare (3)