2022/10/14 by van Doorn, Floris
Computer Science · #42A85 #44A35 #68V20 #F.4.1 #FOS: Computer and information sciences #FOS: Mathematics #Functional Analysis (math.FA) #G.3 #Logic in Computer Science (cs.LO) #Mathematical Software (cs.MS) #Mathematics, Computing, and Information Processing #Numerical Methods and Algorithms
paper · pdf · doi:10.48550/arxiv.2210.07693
openalex publication_date 2022/10/14 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.