与伊莎贝尔重温高斯和

Question

我对以下论点的变体感兴趣：

"(∑ i=1..k . i) = k*(k+1) div 2"

我们知道这是从一个简单的归纳得出的，但直觉有点不同。查看此公式的一种方法是，如果对数字序列 1..k 的极值求和，您将得到

1+k = 2 + (k-1) = ...

然后乘以正确的次数即可得到完整的总和。

我想重现这个论点以证明以下不等式：

"(∑n = 1..k - 1. cmod (f (int n))) ≤ 2 * (∑n ≤ k div 2. cmod (f (int n)))"

这里我知道每个 n.

cmod (f (int k - n)) = cmod (cnj (f n))

你在 Isabelle 中看到了证明这一点的优雅方法吗？

Answer 1

以优雅的方式进行此证明的诀窍是认识到 ∑i=1..k. i 与 ∑i=1..k. k + 1 - i 相同，然后将其添加到原始总和，以便 i 抵消.这是一个简单的 re-indexing 参数：

lemma "(∑i=1..k. i :: nat) = k * (k + 1) div 2"
proof -
  have "(∑i=1..k. i) = (∑i=1..k. k + 1 - i)"
    by (rule sum.reindex_bij_witness[of _ "λi. k + 1 - i" "λi. k + 1 - i"]) auto
  hence "2 * (∑i=1..k. i) = (∑i=1..k. i) + (∑i=1..k. k + 1 - i)"
    by simp
  also have "… = k * (k + 1)"
    by (simp add: sum.distrib [symmetric])
  finally show ?thesis by simp
qed

对于您提到的另一件事，我认为最好的方法是首先将总和拆分为小于 k div 2 的元素和其余元素。然后你可以像上面那样重新索引第二个总和。然后出现不等式部分，因为如果 k 是奇数，你可能在“中间”有一个额外的剩余元素，你必须把它扔掉。

证明重要部分的简要说明：

lemma
  assumes "⋀i. f i ≥ 0"
  shows   "(∑i=1..<k. f (i::nat) :: real) = T"
proof -
  (* Separate summation domain into two disjoint parts *)
  have "(∑i=1..<k. f i) = (∑i∈{1..k div 2}∪{k div 2<..<k}. f i)"
    by (intro sum.cong) auto
  (* Pull sum apart *)
  also have "… = (∑i∈{1..k div 2}. f i) + (∑i∈{k div 2<..<k}. f i)"
    by (subst sum.union_disjoint) auto
  (* Reindex the second sum *)
  also have "(∑i∈{k div 2<..<k}. f i) = (∑i∈{1..<k - k div 2}. f (k - i))"
    by (rule sum.reindex_bij_witness[of _ "λi. k - i" "λi. k - i"]) auto
  (* Throw away the element in the middle if k is odd *)
  also have "… ≤ (∑i∈{1..k div 2}. f (k - i))"
    using assms by (intro sum_mono2) auto
  finally have "(∑i=1..<k. f i) ≤ (∑i=1..k div 2. f i + f (k - i))"
    by (simp add: sum.distrib)

弄清楚如何在 Isabelle 中以惯用的方式进行这些求和操作需要一些经验。 sum.reindex_bij_witness 是一个非常有用的规则（如您所见）。 sum.mono_neutral_left/right 之类的东西也有很大帮助。

与伊莎贝尔重温高斯和

Revisiting Gauss sum with Isabelle

isabelle