Cauchy-Schwartz Inequality in Coq?

Question

In the ℝn - n-dimensional Euclidean space R^n with the standard inner product, which is the dot product, the Cauchy–Schwarz inequality becomes: [1]: https://i.stack.imgur.com/ZNBfx.png

Is anyone aware of an implementation for sums of Cauchy-Schwartz Inequality in Coq, e.g. infotheo?

Answer 1

Another proof is in https://github.com/math-comp/math-comp/blob/f4fb83f19cbe9503f7cfe03ba8217311744e33ac/mathcomp/character/classfun.v#L943

Lemma cfCauchySchwarz phi psi :
  `|'[phi, psi]| ^+ 2 <= '[phi] * '[psi] ?= iff ~~ free (phi :: psi).

but note that in this case the proof has not been generalized over arbitrary dot products on pre-hilbert spaces, but it would work.

Answer 2

https://github.com/roglo/cauchy_schwarz

compiles with Coq 13.1 and has the theorem

Cauchy_Schwarz_inequality
     : ∀ (u v : list R) (n : nat),
         (Σ (k = 1, n), (u.[k] * v.[k])²
          ≤ Σ (k = 1, n), ((u.[k])²) * Σ (k = 1, n), ((v.[k])²))%R