# Bergelson's intersectivity lemma #

This file proves the Bergelson intersectivity lemma: In a finite measure space, a sequence of events
that have measure at least `r`

has an infinite subset whose finite intersections all have positive
volume.

This is in some sense a finitary version of the second Borel-Cantelli lemma.

## References #

Bergelson, *Sets of recurrence of `ℤᵐ`

-actions and properties of sets of differences in
`ℤᵐ`

## TODO #

Restate the theorem using the upper density of a set of naturals, once we have it. This will make
`bergelson'`

be actually strong (and please then rename it to `strong_bergelson`

).

Use the ergodic theorem to deduce the refinement of the Poincaré recurrence theorem proved by Bergelson.

**Bergelson Intersectivity Lemma**: In a finite measure space, a sequence of events that have
measure at least `r`

has an infinite subset whose finite intersections all have positive volume.

TODO: The infinity of `t`

should be strengthened to `t`

having positive natural density.

**Bergelson Intersectivity Lemma**: In a finite measure space, a sequence of events that have
measure at least `r`

has an infinite subset whose finite intersections all have positive volume.