Designing a general library for convolutions
Floris van Doorn
TL;DR
This paper discusses the development of a general, user-friendly convolution library integrated into Lean's mathlib, highlighting design choices and practical implementation experiences.
Contribution
It introduces a flexible convolution library for Lean, emphasizing design decisions that enhance usability and integration into formal mathematical frameworks.
Findings
Successfully integrated convolution into Lean's mathlib.
Provided a general and easy-to-use convolution implementation.
Shared insights on design choices for formal mathematical libraries.
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsMathematics, Computing, and Information Processing · Numerical Methods and Algorithms