Documentation

Mathlib.MeasureTheory.Function.Intersectivity

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 tu.Finite0 < μ (nu, 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 tu.Finite0 < μ (iu, 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.