  We present a mechanical proof of the Cauchy-Schwarz inequality in ACL2(r) and
a formalisation of the necessary mathematics to undertake such a proof. This
includes the formalisation of $\mathbb{R}^n$ as an inner product space. We also
provide an application of Cauchy-Schwarz by formalising $\mathbb R^n$ as a
metric space and exhibiting continuity for some simple functions $\mathbb
R^n\to\mathbb R$. The Cauchy-Schwarz inequality relates the magnitude of a
vector to its projection (or inner product) with another: \[|\langle
u,v\rangle| \leq \|u\| \|v\|\] with equality iff the vectors are linearly
dependent. It finds frequent use in many branches of mathematics including
linear algebra, real analysis, functional analysis, probability, etc. Indeed,
the inequality is considered to be among "The Hundred Greatest Theorems" and is
listed in the "Formalizing 100 Theorems" project. To the best of our knowledge,
our formalisation is the first published proof using ACL2(r) or any other
first-order theorem prover.
