Coq中的Cauchy-Schwartz不等式？

Question

在标准内积为点积的n维柯西-施瓦茨空间R^n中，柯西-施瓦茨不等式变为: 1：https://i.stack.imgur.com/ZNBfx.png

有谁知道柯西-施瓦茨不等式的和在Coq中的实现，例如infotheo？

Answer 1

另一个证据在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).

但请注意，在这种情况下，证明还没有推广到pre-hilbert空间上的任意点积上，但它可以工作。

Answer 2

https://github.com/roglo/cauchy_schwarz

使用Coq 13.1编译，并具有定理

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