Sum_finit

Stream: new members

[Parivash]

Hi,
Is there any thought for proving the following formula:

import algebra.big_operators.order
import data.real.basic
open finset mul_opposite
open_locale big_operators
theorem sum_finit
{x : ℝ} (hx: x ≠ 1)(n : ℕ )
:
∑ i in range n, (i: ℝ)*(x^(i)) = (x*(1-x^n))/(1-x)^2-(n*x^(n+1))/(1-x)
:=
begin
  sorry,
end

Latex:
$\sum_{i=1}^{n} ix^{i} = \frac{x(1-x^n)}{(1-x)^2}-\frac{nx^{n+1}}{1-x}$

[Kevin Buzzard]

The proof should go like this:

import algebra.big_operators.order
import data.real.basic
import tactic -- added this line to get `ring_exp`

open finset mul_opposite
open_locale big_operators
theorem sum_finit
{x : ℝ} (hx: x ≠ 1)(n : ℕ )
:
∑ i in range n, (i: ℝ)*(x^(i)) = (x*(1-x^n))/(1-x)^2-(n*x^(n+1))/(1-x)
:=
begin
  -- denominators aren't 0
  have helpful : 1 - x ≠ 0 := sub_ne_zero.mpr hx.symm,
  -- clear denominators
  field_simp,
  -- now induction on n
  induction n with d hd,
  { -- base case trivial
    simp, },
  { -- inductive step, we need to use the inductive hypothesis
    rw [finset.sum_range_succ, add_mul],
    -- now we can
    rw hd,
    -- and now it should be easy
    simp [nat.succ_eq_add_one],
    ring_exp,
    -- ... except that the proof doesn't work :-(
    sorry }
end

but it doesn't work, so my guess is that your theorem is not correct as it stands. If you fix it up then my proof strategy should work.

Oh I see your problem: range n is 0 to (n-1), not 1 to n.

[Kevin Buzzard]

Yeah, changing the is on the LHS to i+1 (so that we're still summing for i=0 to n-1 but we're using i+1 everywhere) fixes it.

import algebra.big_operators.order
import data.real.basic
import tactic -- added this line to get `ring_exp`

open finset mul_opposite
open_locale big_operators
theorem sum_finit
{x : ℝ} (hx: x ≠ 1)(n : ℕ )
:
∑ i in range n, (i + 1 : ℝ)*(x^(i+1)) = (x*(1-x^n))/(1-x)^2-(n*x^(n+1))/(1-x)
:=
begin
  -- denominators aren't 0
  have helpful : 1 - x ≠ 0 := sub_ne_zero.mpr hx.symm,
  -- clear denominators
  field_simp,
  -- now induction on n
  induction n with d hd,
  { -- base case trivial
    simp, },
  { -- inductive step, we need to use the inductive hypothesis
    rw [finset.sum_range_succ, add_mul],
    -- now we can
    rw hd,
    -- and now it should be easy
    simp [nat.succ_eq_add_one],
    ring_exp, },
end

[Parivash]

@Kevin Buzzard
Yeah, Thank you professor Buzzard