Zulip Chat Archive

Stream: new members

Topic: Simple induction proof


view this post on Zulip André Beyer (Jan 16 2021 at 15:08):

I'm struggling to complete this simple inductive proof below:

example (n i : ) : 2 * ( k in finset.range n, i) = n * (n + 1) :=
begin
  induction n with d hd,
  { simp, },
  {
    rw [ nat.add_one, finset.sum_range_succ, mul_add, hd],
    simp,
    sorry,
  }
end

I'll end up at the following state:

2 * i + d * (d + 1) = (d + 1) * (d + 2)

I'm particularly confused about finset.sum_range_succ. I was expecting to get d + 1 instead of i. Thanks in advance!

view this post on Zulip Shing Tak Lam (Jan 16 2021 at 15:11):

Is the statement correct? What you have is 2k=0n1i=n(n+1)2\sum_{k=0}^{n-1} i = n(n+1), not 2k=0nk=n(n+1)2\sum_{k=0}^{n} k = n(n+1) (which is ∑ k in finset.range n.succ, k)

view this post on Zulip André Beyer (Jan 16 2021 at 16:05):

Right - embarrassingly. Thanks!

I'm still stuck after correction:

2 * d + d * (d + 1) = (d + 1) * (d + 2)

What would easily work is:

2 * (d + 1) + d * (d + 1) = (d + 1) * (d + 2)

I still don't understand why it's d and not d+1.

view this post on Zulip Bryan Gin-ge Chen (Jan 16 2021 at 16:10):

The i in the sum should be a k (and then i can be removed completely):

import algebra.big_operators.basic
import tactic

open_locale big_operators
example (n : ) : 2 * ( k in finset.range (n + 1), k) = n * (n + 1) :=
begin
  induction n with d hd,
  { simp, },
  { rw [ nat.add_one, finset.sum_range_succ, mul_add, hd],
    ring, }
end

view this post on Zulip André Beyer (Jan 16 2021 at 16:33):

Thanks, that works.

I still have problems understanding it though. I wanted to proof

2k=1nk=n(n+1)2 \cdot \sum_{k=1}^n k = n (n + 1)

I would translate the working version as follows though:

2k=1n+1k=n(n+1)2 \cdot \sum_{k=1}^{n+1} k = n (n + 1)

In what range does finset.range operate? Is it usually from 0 to n-1 and thus we'd write n + 1?

view this post on Zulip Bryan Gin-ge Chen (Jan 16 2021 at 16:35):

finset.range n is the finite set of numbers {0,1,2,,n1}\{0,1,2,\dots,n-1\} (cf. docs#finset.range), so the sum in my code (2 * (∑ k in finset.range (n + 1), k)) translates to:

2k=0nk=n(n+1)2 \cdot \sum_{k=0}^n k = n (n + 1)

view this post on Zulip André Beyer (Jan 16 2021 at 16:43):

Nice, thank you!


Last updated: May 14 2021 at 07:19 UTC