infinite series

Stream: new members

[liu]

屏幕截图 2025-02-10 155434.png
I'm formalizing the stem of this problem, but I don't know how to handle the infinity.

[Yaël Dillies]

Infinite sums are docs#tsum

[liu]

What does this equation mean?

HasSum f a = Filter.Tendsto (fun (s : Finset β) => ∑ b ∈ s, f b) Filter.atTop (nhds a)

[liu]

I can't understand this equation.Can anyone give me an example?

HasSum f a = Filter.Tendsto (fun (s : Finset β) => ∑ b ∈ s, f b) Filter.atTop (nhds a)

[Yaël Dillies]

This is not an equation, it's a definition. HasSum f a means that $∑_{n = 0}^∞ f(n) = a$

[Yaël Dillies]

Please stop double-posting. I keep on having to move your posts around

[liu]

I'm sorry. Can these be combined?

[liu]

So how to use theHasSum f acorrectly?This is my false ideal

import Mathlib
example(n:ℕ )(h1:fun n=> n/(n^4+n)):HasSum f 3/8:=by sorry