Convex Functions in ACL2(r)
This paper builds upon our prior formalisation of R^n in ACL2(r) by presenting a set of theorems for reasoning about convex functions. This is a demonstration of the higher-dimensional analytical reasoning possible in our metric space formalisation of R^n. Among the introduced theorems is a set of equivalent conditions for convex functions with Lipschitz continuous gradients from Yurii Nesterov's classic text on convex optimisation. To the best of our knowledge a full proof of the theorem has yet to be published in a single piece of literature. We also explore "proof engineering" issues, such as how to state Nesterov's theorem in a manner that is both clear and useful.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
Learning and Testing Convex Functions
We consider the problems of \emph{learning} and \emph{testing} real-valued convex functions over Gaussian space. Despite the extensive study of function convexity across mathematics, statistics, and computer science, its…
Novel convex decomposition of piecewise affine functions
In this paper, we present a novel approach to decompose a given piecewise affine (PWA) function into two convex PWA functions. Convex decompositions are useful to speed up or distribute evaluations of PWA functions. Diff…
Optimal and Efficient Algorithms for Decentralized Online Convex Optimization
We investigate decentralized online convex optimization (D-OCO), in which a set of local learners are required to minimize a sequence of global loss functions using only local computations and communications. Previous st…
Distributed Optimization of Convex Sum of Non-Convex Functions
We present a distributed solution to optimizing a convex function composed of several non-convex functions. Each non-convex function is privately stored with an agent while the agents communicate with neighbors to form a…
Distributed OptimizationKatyusha X: Simple Momentum Method for Stochastic Sum-of-Nonconvex Optimization
The problem of minimizing sum-of-nonconvex functions (i.e., convex functions that are average of non-convex ones) is becoming increasing important in machine learning, and is the core machinery for PCA, SVD, regular…