Proof Mining in der konvexen Optimierung und verwandten Gebieten

In diesem Projekt geht es darum, beweistheoretische Verfahren aus der Logik zur Extraktion neuer Daten (wie z.B. effektiver Schranken, „proof mining“) aus prima facie inkonstruktiven Beweisen im Bereich der konvexen Optimierung (und angrenzender Gebiete) einzusetzen. Solche Verfahren, geeignete Formen sogenannter Beweisinterpretationen, wurden vom Antragsteller in den vergangenen Jahrzehnten entwickelt und erfolgreich in der Approximationstheorie, Ergodentheorie, Fixpunkttheorie und der Theorie abstrakter Cauchy-Probleme eingesetzt. In den letzten 2-3 Jahren haben wir zudem erstmals mit Anwendungen im Bereich der konvexen Optimierung begonnen. In dem vorliegenden Projekt soll diese logik-basierte Methodologie nun systematisch auf Probleme aus der konvexen Optimierung zugeschnitten und zur Analyse von Konvergenzbeweisen von in der konvexen Optimierung zentralen iterativen Verfahren eingesetzt werden. Ziel ist dabei insbesondere die Gewinnung expliziter und effektiver Raten asymptotischer Regularität, Metastabilität (im Sinne von T. Tao) und Konvergenz solcher Verfahren, aber auch die Verallgemeinerung auf andere Banachräume als Hilberträume und metrische Strukturen wie z.B. CAT(0)-Räume. Insbesondere analysieren wir Konvergenzbeweise, die Tatsachen aus der abstrakten Theorie mengenwertiger Operatoren (z.B. maximal-monotoner Operatoren) verwenden.
(DFG 04/2018, Kohlenbach)