Convex Functions in ACL2(r)

TL;DR

This paper formalizes convex functions in ACL2(r), demonstrating higher-dimensional reasoning and proving key theorems related to convexity and Lipschitz continuity, inspired by Nesterov's work.

Contribution

It presents a formalization of convex functions in ACL2(r), including theorems with equivalent conditions for convexity with Lipschitz continuous gradients, and discusses proof engineering strategies.

Findings

Formalization of convex functions in ACL2(r)

Proof of equivalent conditions for convex functions with Lipschitz gradients

Insights into proof engineering for theorem presentation

Abstract

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.