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 ℤᵐ][bergelson1985]

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.

theorem bergelson' {α : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] {r : ENNReal} {s : ℕ → Set α} (hs : ∀ (n : ℕ), MeasurableSet (s n)) (hr₀ : r ≠ 0) (hr : ∀ (n : ℕ), r ≤ μ (s n)) : ∃ (t : Set ℕ), t.Infinite ∧ ∀ ⦃u : Set ℕ⦄, u ⊆ t → u.Finite → 0 < μ (⋂ n ∈ u, s n)

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.

theorem bergelson {ι : Type u_1} {α : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] {r : ENNReal} [Infinite ι] {s : ι → Set α} (hs : ∀ (i : ι), MeasurableSet (s i)) (hr₀ : r ≠ 0) (hr : ∀ (i : ι), r ≤ μ (s i)) : ∃ (t : Set ι), t.Infinite ∧ ∀ ⦃u : Set ι⦄, u ⊆ t → u.Finite → 0 < μ (⋂ i ∈ u, s i)

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.