Proof Mining in Convex Optimization and related areas

在这个项目中，我们的目标是使用逻辑学中的证明论方法从凸优化及其相关领域的表面无效证明中提取新的数据(如有效界、“证明挖掘”)。在这个基于逻辑的方法的过程中，申请人在过去的几十年里已经开发出了合适的所谓证明解释的形式，并成功地应用于非线性分析。在过去三年的资助中，我们将这种方法大规模地应用于凸优化领域的问题，此外，我们还在邻近领域开展了新的案例研究，如遍历理论、逼近理论和陶伯利亚理论。在接下来的三年中，我们将把这种方法扩展到凸优化领域的进一步问题，包括那些与当前机器学习领域的工作有关的问题。在这里，我们将重点讨论利用集值算子“单调性”概念的推广的证明，这些集值算子是最近在凸优化中研究的，并在机器学习的背景下使用。这个项目的主要目的是利用集值算子的广义单调性或增生性来证明中心迭代程序的渐近正则性、亚稳定性和收敛速度，并将这些结果从Hilbert空间的设置推广到度量结构，如CAT(0)-空间和更一般的Banach空间。

In this Project we aim at using proof-theoretic methods from logic for the extraction of new data (such as effective bounds, "proof mining") from prima facie noneffective proofs in convex optimization and related areas.In the course of this logic-based methodology, suitable forms of so-called proof interpretations have been developed by the applicant during the past decades and successfully applied in nonlinear analysis. In the previous 3 years of funding we applied this at large scale to problems in the area of convex optimization and - additionally - also carried out new case studies in neighbouring areas such as ergodic theory, approximation theory and Tauberian theory.During the next 3 years we will extend this approach to further problems in convex optimization including those which have a connection to current work in the area of machine learning. Here we will focus on proofs which make use of generalizations of the concept of "monotonicity" for set-valued operators which have recently been studied in convex optimization and are used in the context of machine learning. We also intend to analyze proofs which study abstract Cauchy problems given by accretive operators.The main goal of this project is the extraction of rates of asymptotic regularity, metastability (in the sense of T. Tao) and convergence of central iterative procedures whose convergence is shown using such generalized monotonicity or accretivity properties of set-valued operators but also the generalization of such results from the setting of Hilbert spaces to metric structures, such as CAT(0)-spaces, and more general Banach spaces.