How to prove sum of geometric series

Stream: Is there code for X?

[Colin Jones ⚛️]

I have here an example of what I'm trying to prove, but I'm sure how to do it. It won't let me even define the righthand side. Can anyone help?

import Mathlib.Data.Real.Basic
import Mathlib.Topology.Algebra.InfiniteSum.Basic
import Mathlib.Analysis.Normed.Group.Basic
import Mathlib.Analysis.SpecificLimits.Normed

example {x : ℕ} {n : ℝ} (H : ‖n‖ < 1):
∑' (x : ℕ), (↑x + 1) * n ^ (x + 1) = x / (1 - x) ^ 2 :=
by apply tsum_coe_mul_geometric_of_norm_lt_1

[Timo Carlin-Burns]

Hi! It would be a little easier to read your code if you formatted it with #backticks

[Timo Carlin-Burns]

The error you're getting has to do with the fact that x on the right hand side is a natural number. Did you mean to write n instead?

[Timo Carlin-Burns]

It's a little bit confusing that you're calling the real number variable n and the natural number variable x :)

[Timo Carlin-Burns]

This version of the statement might make more sense? I don't actually know much about geometric series so I don't know if this is right

example {x : ℝ} (H : ‖x‖ < 1) :
    ∑' (n : ℕ), (↑n + 1) * x ^ (n + 1) = x / (1 - x) ^ 2 :=
  by sorry

[Timo Carlin-Burns]

This should do the trick!

example {x : ℝ} (H : ‖x‖ < 1) :
    ∑' (n : ℕ), (n + 1) * x ^ (n + 1) = x / (1 - x) ^ 2 := by
  convert tsum_coe_mul_geometric_of_norm_lt_1 H using 1
  have : Function.support (fun n => n * x ^ (n : ℕ)) ⊆ Set.range Nat.succ := by
    rw [Function.support_subset_iff']
    simp
  calc ∑' (n : ℕ), (n + 1) * x ^ (n + 1)
    = ∑' (n : ℕ), n.succ * x ^ n.succ := by simp
  _ = ∑' (n : Set.range Nat.succ), n * x ^ (n : ℕ) := (tsum_range (fun (n : ℕ) => n * x ^ n) Nat.succ_injective).symm
  _ = ∑' (n : ℕ), n * x ^ (n : ℕ) := tsum_subtype_eq_of_support_subset this

[Timo Carlin-Burns]

Or a bit more concisely

example {x : ℝ} (H : ‖x‖ < 1) :
    ∑' (n : ℕ), (n + 1) * x ^ (n + 1) = x / (1 - x) ^ 2 := by
  convert tsum_coe_mul_geometric_of_norm_lt_1 H using 1
  have : Function.support (fun n => n * x ^ (n : ℕ)) ⊆ Set.range Nat.succ := by
    rw [Function.support_subset_iff']
    simp
  rw [←tsum_subtype_eq_of_support_subset this,
    tsum_range (fun (n : ℕ) => n * x ^ n) Nat.succ_injective]
  simp

[Colin Jones ⚛️]

Thank you