!3#18732 Bergelson intersectivity

Stream: PR reviews

[Yaël Dillies]

This PR proving the Bergelson intersectivity lemma has been sitting for a little while (that's British for a long while). I'm only noticing today that it was erroneously marked as too-late. Could one of our resident measure theorists have a look?

[Yaël Dillies]

@Yury G. Kudryashov has already reviewed. So maybe @Sebastien Gouezel will have thoughts?

[Yury G. Kudryashov]

I have 1 remaining concern: strong_bergelson doesn't look like a mathlib name.

[Yury G. Kudryashov]

But I don't have better suggesions.

[Yury G. Kudryashov]

BTW, about density: should we have names for liminf, limsup, and the filter "s has lower density 1"?

[Yury G. Kudryashov]

With theorems like "frequently (filter) p iff liminf density > 0"

[Yaël Dillies]

Hmm, I'm having trouble parsing your message. Can you be more explicit? But I suspect the answer is "Yes, but once Yaël has written the general density API because it will generalise to a lot of densities".

[Yury G. Kudryashov]

What API do you have in mind?

[Yury G. Kudryashov]

E.g., how general is it going to be?

[Yaël Dillies]

Bhavik and I want to formalise the general framework coming from this paper. Not all densities fit into this framework (eg, the Schnirelmann density), but enough that I think it's worth it.