Skolem–Mahler–Lech theorem

Stream: Is there code for X?

[Ardith El-Kareh]

Does some form of the Skolem–Mahler–Lech theorem exist in Mathlib4?

[Kevin Buzzard]

I don't think that we have it.

It's already an interesting question deciding how to state it in the most useful way.

[Bhavik Mehta]

docs#LinearRecurrence is a possible starting point for the hypotheses, but doesn't help much for the goal.

[Junyan Xu]

Imo2024Q3.EventuallyPeriodic could be upstreamed to mathlib (not sure whether it should be generalized and in what way; Function.Periodic is pretty general), then you can state that the sequence (· = 0) of propositions is eventually periodic.

[Weiyi Wang]

I am also somewhat interested in this theorem, though I don't know what application it has and the best form for it

[Aaron Liu]

Junyan Xu said:

Imo2024Q3.EventuallyPeriodic could be upstreamed to mathlib (not sure whether it should be generalized and in what way; Function.Periodic is pretty general), then you can state that the sequence (· = 0) of propositions is eventually periodic.

How about PeriodicOnFilter and then specialize the filter to atTop?

[Kevin Buzzard]

IIRC there is a stronger statement of the form "other than in some degenerate cases, the zeros are not just ultimately periodic but actually full arithmetic progressions plus finitely many extra ones" so "eventually periodic" would not be strong enough to state this variant (which I hope I'm not making up)

[Antoine Chambert-Loir]

Unpopular opinion: Singletons are arithmetic progressions

[Antoine Chambert-Loir]

Also, unless I am mistaken, arithmetic progressions form a basis of closed subsets for a topology on the natural numbers, so that the SML theorem says that zeroes of linear recurrence sequences are closed sets for this topology.

[Kevin Buzzard]

I am a bit confused by this claim. I've seen the claim made for the integers but here I am a bit unclear about whether {3,4,5,6,7,8,...} counts as an AP; if it does then given any singleton {n} it's going to be open because it's the complement of the finitely many APs {0,n+1,2n+2,...},{1,n+2,2n+3,...},...,{n-1,2n,3n+1,...} and finally {2n+1,3n+2,...} (all APs with difference n+1 but this last AP skipping n and starting at 2n+1), so any set will be open.

[Antoine Chambert-Loir]

So I was mistaken, and the claim was true, but not the useful one.