Proof Mining in Convex Optimization and related areas

• Applicant: Professor Dr. Ulrich Kohlenbach
• Subject Area: Mathematics ; Theoretical Computer Science
• Term: from 2017 to 2024
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 400007828

• Final Report Year: 2024

Final Report Abstract

In den letzten 25 Jahren hat sich, wesentlich durch die Arbeiten des Berichterstatters und seiner Mitarbeiter, eine angewandte Form von Beweistheorie („Proof Mining“) als ein neues Teilgebiet der Logik etabliert. Hierbei geht es um die Extraktion effektiver Schranken aus prima facie inkonstruktiven Beweisen mittels logik-basierten Methoden aus der Beweistheorie. In diesem Projekt stand die Analyse von Beweisen in der konvexen Optimierung, Ergodentheorie sowie im Bereich abstrakter Cauchy-Probleme im Vordergrund. Ein besonderer Schwerpunkt lag hierbei auf Beweisen, die wesentlich die abstrakte Theorie monotoner und akkretiver mengenwertiger Abbildungen in Hilbert- und Banachräumen verwenden. Parallel zu zahlreichen Fallstudien wurden auch die bislang existierenden logischen Metatheoreme, die a priori die Extraktion effektiver Schranken in geeigneten Daten garantieren, erweitert. Diese Erweiterungen betreffen die Einbeziehung maximal monotoner und akkretiver Operatoren und deren Resolventen, Dualräume, monotone Operatoren im Sinne Browders in Banachräumen, abstrakte Halbgruppen nichtexpansiver Abbildungen, Fréchet-Ableitungen und Gradienten, Fenchel-Konjugierte, Bregman-Projektionen, Wahrscheinlichkeitsräume, Daniell-Integrale und vieles mehr. Neben diesen Beiträgen zu den beweistheoretischen Grundlagen der Proof-Mining-Methodologie war ein Hauptthema des Projekts die Anwendungen der genannten Methoden auf konkrete Beweise in der kontinuierlichen Optimierung, PDE-Theorie, Ergodentheorie und im Bereich von pursuit-evasion Spielen. Hierbei gelang es, Reichs fundamentales Konvergenzresultat für eine implizit durch pseudokontraktive Operatoren definierte Folgen in gleichmäßig konvexen und glatten Banachräumen vollständig quantitativ zu analysieren, was zu effektiven Metastabilitätsraten (im Sinne von T. Tao) für zahlreiche Algorithmen wie Halpern-type Proximal Point Algorithmen oder Chidumes „gradient descent“ Algorithmus geführt hat. Die Einbeziehung von Dualräumen, Gradienten und Fenchel-Konjugierten in den logischen Formalismus hat ferner die Analysis von auf Bregman-Projektionen basierenden Algorithmen für monotone Operatoren in Banachräumen ermöglicht. Schließlich konnten Konvergenzraten für zentrale Theoreme über das asymptotische Verhalten von Lösungen abstrakter Cauchy-Probleme, die durch akkretive Operatoren gegeben sind, gewonnen werden. Weitere Resultate waren die Bestimmung einer expliziten Konvergenzrate für die „ε-capture“-Eigenschaft im „Lion-Man“-game in allgemeinen metrischen Räumen, die eine gleichmäßige „betweenness“-Bedingung erfüllen, sowie für ein zentrales asymptotisches Regularitätsresultat von Bruck für ergodentheoretische Mittel in gleichmäßig konvexen Banachräumen. Für ein in den letzten Jahren stark untersuchtes Tikhonov-Mann-Verfahren zur Bestimmung von Fixpunkten nichtexpansiver Abbildungen konnten im Kontext allgemeiner hyperbolischer Räume lineare Raten asymptotischer Regularität erzielt werden, die selbst für Hilberträume neu sind. Im Rahmen des Projekts wurden erstmals auch logische Metatheoreme für Anwendungen in der Wahrscheinlichkeitsrechnung entwickelt und in Fallstudien angewandt. Alle diese Resultate wurden in führenden Fachzeitschriften der entsprechenden Gebiete veröffentlicht. Einige mehr theoretischen Resultate zu den logischen Grundlagen des „Proof Mining“ wurden in spezialisierten Fachzeitschriften im Bereich der Logik veröffentlicht. Über die Resultate dieses Projekts wurde auf mehr als 25 internationalen Tagungen vorgetragen sowie in zahlreichen Seminar- und Kolloquiumsvorträgen.

Publications

• Rates of convergence for iterative solutions of equations involving set-valued accretive operators. Computers & Mathematics with Applications, 80(3), 490-503.
  Kohlenbach, Ulrich & Powell, Thomas
  
• The finitary content of sunny nonexpansive retractions. Communications in Contemporary Mathematics, 23(01), 1950093.
  Kohlenbach, Ulrich & Sipoş, Andrei
  
• A uniform betweenness property in metric spaces and its role in the quantitative analysis of the “Lion-Man” game. Pacific Journal of Mathematics, 310(1), 181-212.
  Kohlenbach, Ulrich; López-Acedo, Genaro & Nicolae, Adriana
  
• Bounds for a nonlinear ergodic theorem for Banach spaces. Ergodic Theory and Dynamical Systems, 43(5), 1570-1593.
  Freund, Anton & Kohlenbach, Ulrich
  
• On computational properties of Cauchy problems generated by accretive operators. Documenta Mathematica, 28(5), 1235-1274.
  Pinto, Pedro & Pischke, Nicholas
  
• On Modified Halpern and Tikhonov–Mann Iterations. Journal of Optimization Theory and Applications, 197(1), 233-251.
  Cheval, Horaţiu; Kohlenbach, Ulrich & Leuştean, Laurenţiu
  
• Proof theory and non-smooth analysis. Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences, 381(2248).
  Kohlenbach, Ulrich & Pischke, Nicholas
  
• Strong Convergence for the Alternating Halpern–Mann Iteration in CAT(0) Spaces. SIAM Journal on Optimization, 33(2), 785-815.
  Dinis, Bruno & Pinto, Pedro
  
• Generalized Fejér monotone sequences and their finitary content. Optimization, 74(14), 3771-3838.
  Pischke, Nicholas
  
• Proof mining for the dual of a Banach space with extensions for uniformly Fréchet differentiable functions. Transactions of the American Mathematical Society.
  Pischke, Nicholas
  
• Proof-Theoretical Aspects of Nonlinear and Set-Valued Analysis. Technische Universit¨ t Darmstadt, Darmstadt [Ph.D. Thesis]
  Pischke, Nicholas