Designing a general library for convolutions
Logic in Computer Science
2022-10-17 v1 Mathematical Software
Functional Analysis
Abstract
We will discuss our experiences and design decisions obtained from building a formal library for the convolution of two functions. Convolution is a fundamental concept with applications throughout mathematics. We will focus on the design decisions we made to make the convolution general and easy to use, and the incorporation of this development in Lean's mathematical library mathlib.
Cite
@article{arxiv.2210.07693,
title = {Designing a general library for convolutions},
author = {Floris van Doorn},
journal= {arXiv preprint arXiv:2210.07693},
year = {2022}
}
Comments
24 pages, submitted to CPP 2023