rw in a sum

Stream: new members

[Harold Cooper]

I came back to working on this proof and am stuck again, any tips would be appreciated.

Overall I'm trying to prove $\sum_{k=1}^n k (n - k) = n \sum_{k=1}^n k - \sum_{k=1}^n k^2 = n \frac{n(n+1)}{2} - \frac{n(n+1)(2n+1)}{6} = {n + 1 \choose 3}$

I'm able to rewrite $\sum k^2$ using docs#sum_range_pow

But my attempts to rewrite $\sum k$ using either sum_range_pow again or docs#finset.sum_range_id are failing.

Here are my two attempts. In the first, I'm unable to use rw ← pow_one to rewrite $\sum k$ as $\sum k^1$ so I can apply sum_range_pow. And in the second, I'm unable to use sum_range_id.

import algebra.big_operators.basic
import data.rat.basic
import number_theory.bernoulli

open_locale big_operators
open finset (range)

example {n : ℕ} : ∑ k in range (n+1), (k*(n-k) : ℚ) = (n+1).choose 3 :=
begin
  simp_rw mul_sub,
  rw [finset.sum_sub_distrib, ← finset.sum_mul],
  conv { congr, congr, skip, congr, skip, funext, rw ← sq, },
  rw sum_range_pow,
  conv { congr, congr, congr, congr, skip, funext, rw ← pow_one, },
end

example {n : ℕ} : ∑ k in range (n+1), (k*(n-k) : ℚ) = (n+1).choose 3 :=
begin
  simp_rw mul_sub,
  rw [finset.sum_sub_distrib, ← finset.sum_mul],
  simp_rw ← sq,
  rw sum_range_pow,
  simp_rw finset.sum_range_id,
end

(I know I could probably also prove this by induction, but I think fixing these will teach me some stuff.)

[Notification Bot]

Harold Cooper has marked this topic as unresolved.

[Kevin Buzzard]

rw ← pow_one (x : ℚ) works for the first one

[Kevin Buzzard]

For the second one I don't understand the question. sum_range_id is about $\sum_{i<n}i$ which I don't see in your goal, so the rewrite fails as expected.

[Harold Cooper]

here's a shorter example of the second issue. the goal contains (∑ (x : ℕ) in range (n + 1), ↑x) which I was hoping sum_range_id could do something with

import algebra.big_operators.basic
import data.rat.basic
import number_theory.bernoulli

open_locale big_operators
open finset (range)

example {n : ℕ} : ∑ k in range (n+1), (k*(n-k) : ℚ) = (n+1).choose 3 :=
begin
  simp_rw mul_sub,
  rw [finset.sum_sub_distrib, ← finset.sum_mul],
  rw finset.sum_range_id,
end

maybe the coercion is the issue? or that the sum is being multiplied by something?

[Kevin Buzzard]

No, ↑x is not equal to x, so the rewrite will fail. Theorem provers are picky! The lemma is about a sum of naturals, you have a sum of rationals.

[Harold Cooper]

okay yeah that's fair

[Kevin Buzzard]

You'll first have to rewrite the lemma saying that the sum of the coercions equals the coercion of the sums.

[Kevin Buzzard]

but finset.sum_range_id is evil, because it contains natural division. You'd be better off proving the result you want (the sum of the rationals is what it is) yourself (by induction) and then rewriting that.

[Harold Cooper]

haha yeah it is starting to look like this will all be much easier with induction

[Harold Cooper]

thanks for the help!

[Kevin Buzzard]

If you rewrite "sum of coercions equals coercion of sums" and then sum_range_id you then won't be able to put the coercion back, because natural division and rational division don't commute with the coercion.

[Kevin Buzzard]

I would say that this question, whether you do it over the rationals or naturals, is quite tricky to do in Lean for a beginner. You'll need to know how to do algebra under a sum -- the easy rearrangements which humans do can be done by automation like ring -- but rewrites won't work under a binder which makes this one a bit annoying.

[Kevin Buzzard]

My (pretty messy) solution

import tactic.ring
import algebra.big_operators.basic
import data.rat.basic

open_locale big_operators
open finset

lemma sum_coe {n : ℕ} : ∑ k in range n, (k : ℚ) = n * (n - 1) / 2 :=
begin
  induction n with d hd,
  { simp },
  { rw [sum_range_succ, hd], push_cast, ring}
end

example {n : ℕ} : ∑ k in range (n+1), (k*(n-k) : ℚ) = (n-1)*n*(n+1)/6 :=
begin
  induction n with d hd,
  { simp },
  { rw [sum_range_succ, nat.succ_eq_add_one,
      nat.cast_add, nat.cast_one],
    -- most is this next line is changing x(d+1-x) to x(d-x)+x using only
    -- axioms, because my usual trick `rw (show x*(d+1-x)=x*(d-x)+x, by ring)`
    -- doesn't work under a binder
    simp_rw [mul_sub, mul_add, mul_one, add_comm, add_sub_assoc,
      ← mul_sub, sum_add_distrib, hd, sum_coe],
    push_cast,
    ring },
end