How to show telescoping infinite series converges?

Stream: new members

[spamegg]

More generally, how to work with familiar partial sums:

import Mathlib
example : ∑' n : ℕ, ((1/(n+1) : ℚ) - 1/(n+2)) = 1 := by sorry

[spamegg]

How can I write an infinite series that starts at, say, n=17?

[Philippe Duchon]

My understanding of series convergence in Mathlib is that it is in practice absolute convergence (I am unfamiliar with filter-based convergence but this is what I understand from the comments in the library), so just proving convergence of partial sums won't be enough.

In your example the series is absolutely converging, so convergence of partial sums should be sufficient, but in general, a theorem about telescoping series would need a separate convergence hypothesis.

(Also, your example does not declare a type for the values, so they are natural numbers by default, with the wonky natural division; this is most likely not what you intended. )

[spamegg]

Yes they should be rationals.

[spamegg]

spamegg ha dicho:

How can I write an infinite series that starts at, say, n=17?

I would also like to know the correct notation for this.

[Yakov Pechersky]

Anytime you mention n, instead write n+17

[Yakov Pechersky]

Or sum over n : Set.Ici 17

[spamegg]

Yes I can do that. But I need to model a problem as closely as possible to the real thing, so that the Lean solution matches a "human solution" as closely as possible.

[Yakov Pechersky]

Can you share the larger spec you have to match?

[Yakov Pechersky]

Is the challenge to formalize the statement or the solution as close as possible?

[spamegg]

import Mathlib

example : ∑' n : ℕ, Nat.choose n 15 / Nat.choose n 17 = 272 := by sorry
-- The sum should start from 17 instead.

The solution involves getting partial fractions of 1/(n-15)(n-16) and so on.

[spamegg]

Yakov Pechersky ha dicho:

Is the challenge to formalize the statement or the solution as close as possible?

Yes.

[Yakov Pechersky]

Where are these restrictions derived from?

[spamegg]

Old math olympiad problems for teaching.
Now of course I could say "hey let's substitute u = n+17 and start from 0" but that's quite unnatural... The natural thing is to write out the binomial coefficients, cancel / simplify, then use partial fractions. That's what humans would do.

[spamegg]

Also how would one go about proving, in Lean, that the substitution actually preserves convergence?

[Yakov Pechersky]

Here's a notation macro to help with writing it differently, and a proof that they are definitionally equal.

import Mathlib

notation3 "∑' "(...)" from "i:67", "r:67:(scoped f => tsum (f ∘ (· + i))) => r

example (f : ℕ → ℝ) : ∑' n : ℕ, f (n + 17) = ∑' n : ℕ from 17, f n := rfl

[Yakov Pechersky]

For the "substitution preserves convergence", do you mean that the limit is the same, or that it converges period?

import Mathlib

example (f : ℕ → ℝ) (hf : Summable f) (n : ℕ) : Summable (f ∘ (· + n)) := by
  exact (summable_nat_add_iff _).mpr hf

[spamegg]

I guess, that one converges iff the other converges, and if they do, the limit is the same.

[Yakov Pechersky]

I don't see how an arbitrary series starting from 0, and that same series starting from 17 would converge to the same limit. I would assume that if the series a_n starting from 0 converges to A, then the series summed from 17 would be A - \Sum_{0}^{16} a_i

[spamegg]

Sorry I think the conversation got confused a little. I was talking about making a substitution like u = f(n) (like how we do in integrals).

[spamegg]

And the substitution would change the starting value of the sum.

[spamegg]

Anyway, that's not important right now.
I still need a way to work with "from 17 to infinity". Is Set.Ici the right way to go?

[spamegg]

This doesn't work:

import Mathlib

open Real
open Nat
open scoped BigOperators

example : ∑' n ∈ Set.Ici 17, (choose n 15 / choose n 17 : ℚ) = 272 := by sorry

[spamegg]

failed to synthesize
Fintype ↑(Set.Ici 17)

[spamegg]

It looks like it sees this as a finite sum.

[Aaron Liu]

Use ∑' instead to do an infinite sum.

[spamegg]

application type mismatch
∑' (_ : n ∈ Set.Ici 17), n.choose 15 / n.choose 17
argument
fun h => n.choose 15 / n.choose 17
has type
n ∈ Set.Ici 17 → ℕ : Type
but is expected to have type
?m.931 n → ℕ : Type (max ?u.12 0)

[Yakov Pechersky]

The syntax for tsum is of a type, not a membership, so:

import Mathlib

open Nat

example : ∑' n : Set.Ici 17, (choose n 15 / choose n 17 : ℚ) = 272 := by sorry

[spamegg]

Now, how to show convergence for a sum over Set.Ici, partial sums, or filters, or some other technique?

[Weiyi Wang]

I think the overall strategy could be

• Prove Summable (absolute convergence) by comparison test against zeta 2
• With Summable proved, convert the absolute sum to limit of partial sum, and then do telescoping in the partial sum and then calculate the limit

[Weiyi Wang]

Correction: comparing to zeta 2 is overkill. You can use https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/PSeries.html#Real.summable_nat_rpow_inv