feat(Analysis/InnerProductSpace/Basic): add PreInnerProductSpace (#14024)

add the structure `PreInnerProductSpace`, which does not assume `definite` for the inner product, with a proof of the Cauchy-Schwarz inequality using the discriminant.

Motivation: Such structures arise very often in applications, and by quotienting the kernel one obtains `InnerProductSpace.Core`.

I duplicated most of the proofs from the namespace `InnerProductSpace.Core` and put them under the namespace `PreInnerProductSpace` . Is there a better way?

Author: yoh-tanimoto