coq - Coq 中的 Cauchy-Schwartz 不等式？

Question

在ℝn-n维欧几里得空间R^n与标准内积，即点积，Cauchy-Schwarz不等式变为：[1]：https ://i.stack.imgur.com/ZNBfx.png

有没有人知道 Coq 中 Cauchy-Schwartz 不等式总和的实现，例如 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).

但请注意，在这种情况下，该证明并未推广到前希尔伯特空间上的任意点积，但它会起作用。

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