ACL2(r) 中的实向量空间与柯西-施瓦茨不等式

我们在 ACL2(r) 中给出了柯西-施瓦茨不等式的机械证明，并形式化了进行此类证明所需的数学基础。这包括将 $\mathbb{R}^n$ 形式化为内积空间。我们还通过将 $\mathbb R^n$ 形式化为度量空间并展示一些简单函数 $\mathbb R^n\to\mathbb R$ 的连续性，给出了柯西-施瓦茨不等式的一个应用。柯西-施瓦茨不等式将一个向量的模长与其和另一向量的投影（或内积）联系起来：$$|\langle u,v\rangle| \leq \|u\| \|v\|$$ 当且仅当向量线性相关时取等号。它在线性代数、实分析、泛函分析、概率论等许多数学分支中频繁使用。事实上，该不等式被认为是“一百个最伟大的定理”之一，并列入“形式化 100 定理”项目。据我们所知，我们的形式化是使用 ACL2(r) 或任何其他一阶定理证明器的首个已发表证明。