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 e...
Main Authors: | , |
---|---|
Format: | Article |
Language: | English |
Published: |
Open Publishing Association
2018-10-01
|
Series: | Electronic Proceedings in Theoretical Computer Science |
Online Access: | http://arxiv.org/pdf/1810.04316v1 |
id |
doaj-5dd40e37ef3640e0badbb414c2aedd31 |
---|---|
record_format |
Article |
spelling |
doaj-5dd40e37ef3640e0badbb414c2aedd312020-11-25T01:15:32ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802018-10-01280Proc. ACL2 201812814210.4204/EPTCS.280.10:8Convex Functions in ACL2(r)Carl Kwan0Mark R. Greenstreet1 University of British Columbia 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.http://arxiv.org/pdf/1810.04316v1 |
collection |
DOAJ |
language |
English |
format |
Article |
sources |
DOAJ |
author |
Carl Kwan Mark R. Greenstreet |
spellingShingle |
Carl Kwan Mark R. Greenstreet Convex Functions in ACL2(r) Electronic Proceedings in Theoretical Computer Science |
author_facet |
Carl Kwan Mark R. Greenstreet |
author_sort |
Carl Kwan |
title |
Convex Functions in ACL2(r) |
title_short |
Convex Functions in ACL2(r) |
title_full |
Convex Functions in ACL2(r) |
title_fullStr |
Convex Functions in ACL2(r) |
title_full_unstemmed |
Convex Functions in ACL2(r) |
title_sort |
convex functions in acl2(r) |
publisher |
Open Publishing Association |
series |
Electronic Proceedings in Theoretical Computer Science |
issn |
2075-2180 |
publishDate |
2018-10-01 |
description |
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. |
url |
http://arxiv.org/pdf/1810.04316v1 |
work_keys_str_mv |
AT carlkwan convexfunctionsinacl2r AT markrgreenstreet convexfunctionsinacl2r |
_version_ |
1725152681444507648 |