How to proof Summable?

Stream: new members

[oishi]

Hi, dose anyone know how to proof Summable ? I have no idea how to handle this.

For example:

⊢ Summable fun (n:ℕ) ↦ (((n).choose k):ℝ) * x ^ n * n

[Riccardo Brasca]

In general when proving something in Lean the first question is why it holds mathematically. So you should ask why this is true, and then translate the proof to Lean.

[Riccardo Brasca]

Also, please try to write #mwe, it helps people in helping you.