Zulip Chat Archive

Stream: new members

Topic: Sum_finit


Parivash (Jan 24 2023 at 16:57):

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:
i=1nixi=x(1xn)(1x)2nxn+11x\sum_{i=1}^{n} ix^{i} = \frac{x(1-x^n)}{(1-x)^2}-\frac{nx^{n+1}}{1-x}

Kevin Buzzard (Jan 24 2023 at 17:08):

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 (Jan 24 2023 at 17:09):

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 (Jan 24 2023 at 17:22):

@Kevin Buzzard
Yeah, Thank you professor Buzzard


Last updated: Dec 20 2023 at 11:08 UTC