Convex Functions in ACL2(r)

Carl Kwan
(University of British Columbia)
Mark R. Greenstreet
(University of British Columbia)

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.

In Shilpi Goel and Matt Kaufmann: Proceedings of the 15th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 2018), Austin, Texas, USA, November 5-6, 2018, Electronic Proceedings in Theoretical Computer Science 280, pp. 128–142.
Published: 29th October 2018.

ArXived at: http://dx.doi.org/10.4204/EPTCS.280.10 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org