Coq 中的柯西-施瓦茨不等式？

问题描述

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

是否有人知道 Coq 中 Cauchy-Schwartz 不等式求和的实现，例如信息论？

解决方法

https://github.com/roglo/cauchy_schwarz

使用 Coq 13.1 编译并得到定理

let firstCell = tableRaw.insertCell(0);
firstCell.setAttribute("style",'border: 4px solid ' + cellStroke + '; background-color: ' + cellFill + '; max-width: 10px;');
firstCell.innerHTML = "";

,

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

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