设计用于卷积的通用形式化库
计算机科学中的逻辑
2022-10-17 v1 数学软件
泛函分析
摘要
我们将讨论在构建两个函数卷积的形式化库过程中获得的经验和设计决策。卷积是一个基础概念，在数学各领域都有应用。我们将聚焦于为使卷积具有通用性和易用性而做出的设计决策，以及该开发在Lean数学库mathlib中的集成。
引用
@article{arxiv.2210.07693,
title = {Designing a general library for convolutions},
author = {Floris van Doorn},
journal= {arXiv preprint arXiv:2210.07693},
year = {2022}
}
备注
24 pages, submitted to CPP 2023