Computeralgebra und Ungleichungen für spezielle Funktionen

Computeralgebra hat sich in den letzten Jahrzehnten zu einem essentiellen Werkzeug zum Finden und Beweisen von Summations- und Integrationsidentitaeten fuer spezielle Funktionen entwickelt. Methoden fuer das Beweisen von Ungleichungen sind derzeit aber kaum bis gar nicht vorhanden und das obwohl Ungleichungen ueber spezielle Funktionen in vielen Bereichen der Mathematik und Physik auftreten. Erste bahnbrechende Erfolge wurden von Gerhold und Kauers (2005) erzielt, die Ungleichungen fuer eine grosse Klasse spezieller Funktionen automatisch mit einem Zugang beweisen koennen, der "Cylindrical Algebraic Decomposition" (CAD) verwendet. Auch wenn diese Methode ein neues Anwendungsgebiet fuer Computeralgebra eroeffnet hat, bleiben viele wesentliche Fragen noch ungeklaert, wie zum Beispiel a priori Kriterien fuer Termination. Ziel dieses Projekts ist die Entwicklung, Implementierung und Anwendung neuer Algorithmen zum Beweisen von Ungleichungen fuer spezielle Funktionen. Dabei werden verschiedene Ansaetze verfolgt und zusammen gefuehrt: eine Weiterentwicklung klassischer Beweistechniken zu Algorithmen, was den Einsatz und Ausbau von symbolischen Summationsalgorithmen beinhaltet, sowie eine Weiterentwicklung des CAD-basierten Zugangs von Gerhold und Kauers.

Dieses Projekt hat zur Weiterentwicklung und zum besseren Verständnis von automatischen Techniken zur Behandlung von Ungleichungen (über spezielle Funktionen) beigetragen sowie zur Verbreitung dieser Techniken in Bereiche der Mathematik, die üblicherweise keine Computeralgebra verwenden.Spezielle Funktionen sind interessant, weil sie in verschiedenen Anwendungen der Mathematik oder Physik auftreten und sie werden zum Teil als speziell betrachtet, weil sie sich als sehr nützlich erwiesen haben, zum Teil weil es schöne Arten gibt sie darzustellen, wie z.B. sie über Differential- oder Differenzengleichungen zu definieren.Ungleichungen sind Probleme, die zwar einfach zu formulieren sind, aber typischerweise schwierig zu beweisen. In der klassischen Mathematik werden viele verschiedene Ansätze für diese Beweise verwendet. Ungleichungen, die spezielle Funktionen enthalten, werden seit Jahrhunderten untersucht, aber auch in der klassischen Analysis gibt es keinen methodischen Zugang um mit ihnen umzugehen. Stattdessen werden sie üblicherweise von Fall zu Fall unterschiedlich behandelt. Zur Behandlung von (Systemen von) Polynomungleichungen existieren inzwischen Methoden der Computeralgebra wie z.B. Cylindrical Algebraic Decomposition (CAD), die praktisch einsetzbar sind. Im Gegensatz dazu sind Algorithmen, die Ungleichungen über spezielle Funktionen behandeln noch immer kaum zu finden und waren bis vor kurzem gar nicht vorhanden.Im Wesentlichen die einzige bekannte Methode wurde 2005 von Gerhold und Kauers eingeführt. Ihre Methode war einer der Ausgangspunkte für dieses Projekt: wir haben sie auf verschiedene Probleme angewandt in Zusammenarbeit mit MathematikerInnen aus unterschiedlichen Gebieten der klassischen Mathematik. Außerdem haben wir die Anwendbarkeit dieser Methode analysiert und im Zuge dieser Analyse eine Variante der Prozedur eingeführt.Die Methode von Gerhold und Kauers verwendet CAD, der ein Algorithmus mit einer hohen Rechenkomplexität ist. In der Arbeit mit Ungleichungen über spezielle Funktionen werden oft die Grenzen des Machbaren erreicht sowohl in Zeit- als auch in Speicheraufwand. In diesem Projekt wurden hochdimensionale Ungleichungen aus den Bereichen Numerische Mathematik und Fuzzy Logic erfolgreich behandelt. Neben den so erzielten Resultaten wurde auch mehr Einsicht gewonnen, wie mit Problemen umgegangen werden kann, die zwar theoretisch mit CAD lösbar sind, aber in Praxis außer Reichweite erscheinen.Ein weiterer Nachteil der Methode von Gerhold und Kauers ist, dass sie als Black Box funktioniert und nur der Wahrheitswert zurück gegeben wird, aber kein nachvollziehbarer Beweis. Ein alternativer Weg, der in diesem Projekt entwickelt wurde, basiert auf dem (automatischen) Lösen von Differenzengleichungen. Es wird spezifisch nach einer Lösung gesucht, die eine endliche Linearkombination von Quadraten von speziellen Funktionen ist. Mithilfe von Methoden wie CAD können die Koeffizienten in dieser Darstellung auf Positivität untersucht werden. Es wird also automatisch eine Darstellung hergeleitet von der Positivität im Wesentlichen direkt ablesbar ist. Dieser Algorithmus wurde im Computeralgebrasystem Maple implementiert und ist zum freien Download verfügbar.