Search code examples
coqproofcoq-tacticformal-verificationssreflect

Cauchy-Schwartz Inequality in Coq?

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.sstatic.net/ZNBfx.png

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

Solution

  • 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.