English
For a fixed r > 0 in an ordered additive monoid and a function s from natural numbers to sets, the limsup of the sets s(n) equals the set of those points ω for which the sequence of indicator sums ∑_{k<n} 1_{s(k)}(ω) · r converges to the top filter, i.e., diverges to ∞ along n.
Русский
Для фиксированного r > 0 в упорядоченном аддитивном моноиду и функции s: ℕ → множества, limsup(s(n)) совпадает с множеством тех ω, для которых последовательность сумм-индикаторов ∑_{k<n} 1_{s(k)}(ω) · r расходится к бесконечности при n → ∞.
LaTeX
$$$\\text{atTop}.\\operatorname{limsup} s = \\{\\omega \\;|\\; atTop.Tendsto (\\lambda n, \\sum_{k \\in \\mathrm{Finset}.range n} (s(k)).indicator( (\\lambda \\_, r) ) \\omega) atTop\\, atTop\\}$$$
Lean4
theorem limsup_eq_tendsto_sum_indicator_atTop {α R : Type*} [AddCommMonoid R] [PartialOrder R] [IsOrderedAddMonoid R]
[AddLeftStrictMono R] [Archimedean R] {r : R} (h : 0 < r) (s : ℕ → Set α) :
atTop.limsup s = {ω | atTop.Tendsto (fun n ↦ ∑ k ∈ Finset.range n, (s k).indicator (fun _ ↦ r) ω) atTop} :=
by
nth_rw 1 [← Nat.cofinite_eq_atTop, cofinite.limsup_set_eq]
ext ω
rw [mem_setOf_eq, mem_setOf_eq, infinite_iff_tendsto_sum_indicator_atTop h, iff_eq_eq]
congr
