English
For an infinite index set ι and a family of measurable sets s_i in a finite measure space with each μ(s_i) ≥ r > 0, there exists an infinite subset t of ι such that any finite intersection of the s_i (i ∈ u ⊆ t) has positive measure.
Русский
Для бесконечного множества индексов ι и семейства измеримых множеств s_i в пространстве скрorea, где каждая мера не меньше r > 0, существует бесконечное подмножество t such that для любой конечной подмножества u ⊆ t имеют место положительные меровые пересечения.
LaTeX
$$$$ \exists t \subset ι: t \text{ бесконечно}, \forall u \subset t, \ u \text{ конечное} \Rightarrow 0 < μ(\bigcap_{i \in u} s_i). $$$$
Lean4
/-- **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. -/
theorem bergelson [Infinite ι] {s : ι → Set α} (hs : ∀ i, MeasurableSet (s i)) (hr₀ : r ≠ 0) (hr : ∀ i, r ≤ μ (s i)) :
∃ t : Set ι, t.Infinite ∧ ∀ ⦃u⦄, u ⊆ t → u.Finite → 0 < μ (⋂ i ∈ u, s i) :=
by
obtain ⟨t, ht, h⟩ := bergelson' (fun n ↦ hs <| Infinite.natEmbedding _ n) hr₀ (fun n ↦ hr _)
refine
⟨_, ht.image <| (Infinite.natEmbedding _).injective.injOn, fun u hut hu ↦
(h (preimage_subset_of_surjOn (Infinite.natEmbedding _).injective hut) <|
hu.preimage (Embedding.injective _).injOn).trans_le <|
measure_mono <| subset_iInter₂ fun i hi ↦ ?_⟩
obtain ⟨n, -, rfl⟩ := hut hi
exact iInter₂_subset n hi
