Commit 2025-10-11 15:08 26fbcd9e

feat: introduce Gram matrices (#25883) A Gram matrix has entry ⟪v i, v j⟫ at i j : n, where v : n → α is an InnerProductSpace 𝕜 α. Give this notion and show that Gram matrices are positive semi-definite. This will be used later in order to show that the covariance matrix for Brownian Motion is positive semi-definite.