Coq 中的 Cauchy-Schwartz 不等式？

Question

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

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

Answer 1

使用 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

Answer 2

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

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

Coq 中的 Cauchy-Schwartz 不等式？

Cauchy-Schwartz Inequality in Coq?

coq

proof

coq-tactic

formal-verification

ssreflect