Die vorliegende Dissertation beschäftigt sich mit Erweiterungen des Proof Mining Programms, sowohl in Bezug auf die zugrunde liegenden logischen Ansätze als auch in Bezug auf die Breite der Anwendungen auf (meist vorher unbehandelte) Bereiche der nichtlinearen Analysis und Optimierung, in beiden Fällen mit einem besonderen Fokus auf Themen welche sich auf mengenwertige Operatoren beziehen.

Dafür erweitern wir die aktuellen logischen Methoden des Proof Minings durch neue Systeme und zugehörige sogenannten logische Metatheoreme, welche diese recht involvierten Bereiche der nichtlinearen Analysis behandeln. Die meisten dieser hier entwickelten Systeme beruhen dabei in essenzieller Weise auf dem Ausnutzen von sogenannten intensionalen Methoden, das heißt der Behandlung von Mengen mit möglicherweise hoher Quantoren-Komplexität in der definierenden Matrix durch charakteristische Funktionen und Axiome welche nur die essenziellen Eigenschaften dieser Mengen beschreiben und nicht vollständig deren Elemente charakterisieren.

Die Anwendbarkeit all dieser neuen Metatheoreme wird dann durch eine Reihe von Fallstudien für die entsprechenden Bereiche begründet, welche insbesondere auch die Natürlichkeit der intensionalen Methoden als gewählten Ansatz für die entsprechenden Systeme hervorheben.

Der erste neue Bereich, welcher damit erschlossen wird, ist die Theorie der nichtlinearen Halbgruppen, induziert durch zugehörige Evolutionsgleichungen für akkretive Operatoren, in dessen Kontext wir in gewissem Sinne (neben einem initialen Vorstoß aus dem Jahr 2015) die ersten Anwendungen des Proof Minings allgemein auf die Theorie der partiellen Differentialgleichungen liefern. Konkret präsentieren wir quantitative Versionen von vier zentralen Resultaten über das asymptotische Verhalten von Lösungen solcher Gleichungen.

Der zweite neue Anwendungsbereich, welcher durch die vorliegende Thesis erschlossen wird, ist der des stetigen Dualraums eines Banachraums und der dazugehörigen Norm (welche auch durch intensionale Methoden angegangen werden). Dies beruht insbesondere auf einer beweistheoretisch-milden Behandlung von Suprema über (gewissen) beschränkten Mengen, welche auch noch später weiter angewandt wird. Jene Systeme für diese bis jetzt nicht behandelten grundlegenden Begriffe der Funktionalanalysis werden dann weiter ausgebaut um verschiedene andere Begriffe aus der konvexen Analysis wie Frechet-Ableitungen einer konvexen Funktion, Fenchel-Konjugate, Bregman-Distanzen und monotone Operatoren auf Banachraeumen im Sinne von Browder zu behandeln.

Diese Systeme werden dann eingesetzt, um Proof Mining Anwendungen im Kontext von Picard- und Halpern-artigen Iterationen von sogenannten Bregman-stark-nichtexpansiven Abbildungen abzuleiten. In diesem Zuge liefern diese Anwendungen sowohl neue quantitative als auch neue qualitative Resultate.

Zuletzt diskutieren wir in dieser Arbeit den Schlüsselbegriff der Extensionalität eines mengenwertige Operators und dessen Verhältnis zu mengentheoretischen Maximalitätsprinzipien in weiterer Tiefe (welches schon in vorherigen Arbeiten in einem gewissen Rahmen herausgestellt wurde). Dabei stellen wir ein Problem heraus, welches mit der Behandlung der vollen Extensionalität im Kontext von diesem intensionalen Ansatz zur Behandlung von mengenwertigen Operatoren generell auftritt, und präsentieren Fragmente des Extensionalitätsprinzips welche diese Probleme vermeiden.

Korrespondierend zu diesen Fragmenten diskutieren wir neue Stetigkeitsbegriffe für mengenwertige Operatoren, welche neben dem klassichen Begriff der gleichmäßigen Stetigkeit im Sinne der Hausdorff-Metrik liegen. Insbesondere benutzen wir hier wieder den vorherigen Ansatz zur beweistheoretisch-milden Behandlung von Suprema über beschränkten Mengen, um den ersten beweistheoretischen Ansatz für die Behandlung der Hausdorff-Metrik im Kontext von Systemen des Proof Minings zu entwickeln.

Die Anwendbarkeit dieser Behandlung der Hausdorff-Metrik wird dann insbesondere durch die letzte Fallstudie herausgestellt, in welcher wir quantitative Informationen für Mann-artige Iterationen von mengenwertigen Abbildungen liefern, welche nichtexpansiv im Sinne der Hausdorff-Metrik sind.