sum of series

Stream: new members

[vxctyxeha]

why cant i rw [tsum_coe_mul_geometric_of_norm_lt_1]

import Mathlib


theorem sum_n_over_2_pow_n' : ∑' n : ℕ, (n / 2^n : ℝ) = 2 := by
have h_norm : ‖(1/2 : ℝ)‖ < 1 := by
  rw [Real.norm_eq_abs]
  norm_num;rw [abs_of_pos]; norm_num; norm_num
rw [tsum_coe_mul_geometric_of_norm_lt_1]

[vxctyxeha]

https://github.com/leanprover-community/mathlib4/blob/8666bd82efec40b8b3a5abca02dc9b24bbdf2652/Mathlib/Analysis/SpecificLimits/Normed.lean#L364-L366

[Aaron Liu]

Well it's called tsum_coe_mul_geometric_of_norm_lt_one, not tsum_coe_mul_geometric_of_norm_lt_1

[Robin Arnez]

Here if you wonder: https://github.com/leanprover-community/mathlib4/blob/c05f2327e9fd8d4429dc98cb29f0d01abc73bfa6/Mathlib/Analysis/SpecificLimits/Normed.lean#L500-L502

[Robin Arnez]

Your link was from two years ago

[vxctyxeha]

@Robin Arnez where did you get that?

[Robin Arnez]

go to https://github.com/leanprover-community/mathlib4, then navigate to Mathlib/Analysis/SpecificLimits/Normed.lean

[Robin Arnez]

The c05... portion is just to make this link to the version how it is now even if this file were to change in the future

[Kevin Buzzard]

See also https://mathlib-changelog.org/v4/theorem/tsum_coe_mul_geometric_of_norm_lt_1