Proof Mining in Convex Optimization and related areas

在这个项目中，我们的目标是使用逻辑中的证明理论方法从凸优化和相关领域的初步无效证明中提取新数据（如有效界，“证明挖掘”）。在这种基于逻辑的方法论的过程中，在过去的几十年里，申请人开发了所谓的证明解释的适当形式，并成功地应用于非线性分析。在前3年的资助中，我们大规模地将其应用于凸优化领域的问题，此外，我们还在邻近的领域进行了新的案例研究，如遍历理论、近似理论和陶伯利理论。在接下来的三年里，我们将把这种方法扩展到凸优化的进一步问题，包括那些与当前机器学习领域的工作有关的问题。在这里，我们将重点关注利用集值算子的“单调性”概念的推广的证明，该概念最近在凸优化中得到了研究，并用于机器学习的背景下。我们还打算分析研究由加算子给出的抽象柯西问题的证明。本项目的主要目标是提取中心迭代过程的渐近正则性，亚稳态（在T. Tao的意义上）和收敛率，其收敛性是利用集值算子的这种广义单调性或活动性来显示的，但也将这种结果从希尔伯特空间的设置推广到度量结构，如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.