Coq 中的 Cauchy-Schwartz 不等式？答案

【问题标题】：Cauchy-Schwartz Inequality in Coq?Coq 中的 Cauchy-Schwartz 不等式？
【发布时间】：2021-07-06 00:56:28
【问题描述】：

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

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

【问题讨论】：

标签： coq proof coq-tactic formal-verification ssreflect

【解决方案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

【讨论】：

感谢您的帮助。

【解决方案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).

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

【讨论】：

FTR 有限维向量空间的通用版本仍在此处等待集成：github.com/math-comp/math-comp/pull/207/…