English
Gallagher’s ergodic theorem for AddCircle: either the set addWellApproximable(𝕊, δ) is almost everywhere false for almost all x, or it is almost everywhere true as δ tends to zero along atTop; i.e., ae-empty or ae-full dichotomy holds for this approximation property.
Русский
Эргодическая теорема Галлахера для AddCircle: либо множество addWellApproximable(𝕊, δ) почти повсюду ложно для почти всех x, либо почти повсюду истинно при δ→0; существует дуализм ae-пустоты и ae-полноты для этой аппроксимации.
LaTeX
$$$$ \\text{ae-empty} \\lor \\text{ae-full} \\quad \\text{for } \\operatorname{addWellApproximable}(\\mathbb{S}, δ). $$$$
Lean4
theorem mem_addWellApproximable_iff (δ : ℕ → ℝ) (x : UnitAddCircle) :
x ∈ addWellApproximable UnitAddCircle δ ↔ {n : ℕ | ∃ m < n, gcd m n = 1 ∧ ‖x - ↑((m : ℝ) / n)‖ < δ n}.Infinite :=
by
simp only [mem_add_wellApproximable_iff, ← Nat.cofinite_eq_atTop, cofinite.blimsup_set_eq, mem_setOf_eq]
refine iff_of_eq (congr_arg Set.Infinite <| ext fun n => ⟨fun hn => ?_, fun hn => ?_⟩)
· exact (mem_approxAddOrderOf_iff hn.1).mp hn.2
· have h : 0 < n := by obtain ⟨m, hm₁, _, _⟩ := hn; exact pos_of_gt hm₁
exact ⟨h, (mem_approxAddOrderOf_iff h).mpr hn⟩
