This series can be rewritten as:

2 * lim (n → ∞) Σ (k = 0 to n) k / 2^k

The final term of this series will of course be n / 2^n. So let’s try to write each term with 2^n as its denominator:

2 * lim (n → ∞) Σ (k = 0 to n) k * 2^(n-k) / 2^n → Multiply by 2^(n-k) / 2^(n-k)

= lim (n → ∞) 1/2^(n-1) Σ (k = 0 to n) k * 2^(n-k) → Factor the denominator out of the sum, combine it with the 2 from in front of the limit

What will this sum look like, though? Its first few terms are:

0*2^n + 1*2^(n-1) + 2*2^(n-2) + … + (n-1)*2^1 + n*2^0 (my construction below works backwards, from the last term here to the first)

This can be written as a double sum: Σ (k = 0 to n-1) Σ (j = 0 to k) 2^j (which is 2^0 + 2^0 + 2^1 + 2^0 + 2^1 + 2^2 + 2^0 + 2^1 + 2^2 + 2^3 + …, so we have n copies of 2^0, n-1 copies of 2^1, etc)

So we have:

lim (n → ∞) 1/2^(n-1) Σ (k = 0 to n-1) Σ (j = 0 to k) 2^k

= lim (n → ∞) 1/2^(n-1) Σ (k = 0 to n-1) (2^(k+1) - 1) → Evaluate innermost sum, just sum of powers of 2 from 0 to k

= lim (n → ∞) 1/2^(n-1) * (2^(n+1) - 2 - n) → Evaluate next sum, which is powers of 2 from 1 to n, and don’t forget the -1 part

= lim (n → ∞) (2^(n+1) - n - 2) / 2^(n-1) → Combine leftover terms into one fraction in the limit

= lim (n → ∞) 4 - n/2^(n-1) - 1/2^(n-2) → Distribute denominator to each term

= 4 - 0 - 0 → First term is just 4, other terms go to 0

= 4

I’ve been checking and thinking about this at least a bit each day, and today’s the first day a solution came to me.

Edit: Checking your solution now, it’s obviously much nicer than this - but at this point I’m just happy I solved it at all. Obviously I knew it was 4 from just calculating partial sums from day 1, but proving it proved challenging.