881466BB-7455-4E25-B008-7C666301C155

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.
4699794C-0D09-455F-A094-2612ACC4B1C0
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)

  1. #1 rolak
    16. Oktober 2018

    Schräge Nebeneffekte…

  2. #2 Dr. Webbaer
    16. Oktober 2018

    Nur am Rande, also ergänzend, angemerkt :
    Derartige Beweise können an der Axiomatik scheitern, wie an Unvollkommenheit der verwendeten oder bereits so bereit gestellten Algorithmik.

    Ansonsten beeindruckend, wenn auch nicht überraschend, dass “Maschinen”, also tautologisch angeleitete, angewendete Algorithmik so befinden kann.

    MFG + schöne Mittwoche noch,
    Dr. Webbaer

  3. #3 interessierteNachfrage
    19. Oktober 2018

    @#1: Welche “Nebeneffekte”? Inwiefern “schräg?