has_sum for consecutive reciprocals

Stream: Is there code for X?

[Nikolas Kuhn]

Is there a lemma stating that the sum of consecutive reciprocals is one? E.g. like this
Edit : See the correction by Kevin Buzzard below, still looking for an answer.

import topology.algebra.infinite_sum

lemma has_sum_cons_rec:
  has_sum (λ (k: ℕ), 1/(k.succ*(k.succ.succ)))  1 :=
begin
  sorry,
end

[Kevin Buzzard]

As you state it, the sum will be zero ;-) because Lean will by default assume that 1/(k.succ*(k.succ.succ)) is a natural number, and division in the natural numbers rounds down, so it's a sum of zeros.

[Kevin Buzzard]

This should be true though:

import topology.algebra.infinite_sum
import topology.instances.real

lemma has_sum_cons_rec:
  has_sum (λ (k: ℕ), (1/((k+1)*(k+2)) : ℝ)) 1 :=
begin
  sorry,
end

and you can even sum 1/(k*(k+1)) because in the reals 1/0 is defined to be a junk value, which happens to be zero.

[Bhavik Mehta]

Not in mathlib, but I have this in the unit fractions project! Along with the versions starting from any natural, to get sum 1/k

[Joseph Myers]

The partial sums are essentially the result of archive/100-theorems-list/42_inverse_triangle_sum.lean, so if any results like this go in mathlib proper, maybe that file should be refactored to use them (unless something about handling the infinite sum makes things fundamentally different).