AddCircle.ae_empty_or_univ_of_forall_vadd_ae_eq_self

theorem AddCircle.ae_empty_or_univ_of_forall_vadd_ae_eq_self : ∀ {T : ℝ} [hT : Fact (0 < T)] {s : Set (AddCircle T)}, MeasureTheory.NullMeasurableSet s MeasureTheory.volume → ∀ {ι : Type u_1} {l : Filter ι} [inst : l.NeBot] {u : ι → AddCircle T}, (∀ (i : ι), MeasureTheory.volume.ae.EventuallyEq (u i +ᵥ s) s) → Filter.Tendsto (addOrderOf ∘ u) l Filter.atTop → MeasureTheory.volume.ae.EventuallyEq s ∅ ∨ MeasureTheory.volume.ae.EventuallyEq s Set.univ

The theorem `AddCircle.ae_empty_or_univ_of_forall_vadd_ae_eq_self` states that given a real number `T` greater than zero and a null-measurable set `s` on the additive circle with radius `T`, if this set `s` is almost invariant under rotation by a family (`u`) of elements from the circle, where these elements are indexed by some type `ι` and the addative order of these elements tends to infinity along some non-bottom filter `l`, then the set `s` is either almost empty or almost full with respect to the Lebesgue measure (which is denoted by `MeasureTheory.volume` in Lean). Here, almost invariance means that for every element in the indexing type `ι`, the rotated set `u i +ᵥ s` is almost equal to the set `s` with respect to the Lebesgue measure, and almost empty or full means that the set `s` is equal to the empty set or the universal set almost everywhere.

More concisely: Given a real number T > 0, a null-measurable set s on the additive circle with radius T, and a family u of rotations indexed by ι with their orders tending to infinity along a non-bottom filter l, if s is almost invariant under all rotations u i, then s is almost empty or almost full with respect to Lebesgue measure.