Cardinality and limit of sum of indicators

This file contains results relating the cardinality of subsets of ℕ and limits, limsups of sums of indicators.

Tags

finite, indicator, limsup, tendsto

theorem Set.sum_indicator_eventually_eq_card {α : Type u_1} [AddCommMonoid α] (a : α) {s : Set ℕ} (hs : s.Finite) : ∀ᶠ (n : ℕ) in Filter.atTop, ∑ k ∈ Finset.range n, s.indicator (fun (x : ℕ) => a) k = Nat.card ↑s • a

theorem Set.infinite_iff_tendsto_sum_indicator_atTop {R : Type u_1} [AddCommMonoid R] [PartialOrder R] [IsOrderedAddMonoid R] [AddLeftStrictMono R] [Archimedean R] {r : R} (h : 0 < r) {s : Set ℕ} : s.Infinite ↔ Filter.Tendsto (fun (n : ℕ) => ∑ k ∈ Finset.range n, s.indicator (fun (x : ℕ) => r) k) Filter.atTop Filter.atTop

theorem Set.limsup_eq_tendsto_sum_indicator_atTop {α : Type u_1} {R : Type u_2} [AddCommMonoid R] [PartialOrder R] [IsOrderedAddMonoid R] [AddLeftStrictMono R] [Archimedean R] {r : R} (h : 0 < r) (s : ℕ → Set α) : Filter.limsup s Filter.atTop = {ω : α | Filter.Tendsto (fun (n : ℕ) => ∑ k ∈ Finset.range n, (s k).indicator (fun (x : α) => r) ω) Filter.atTop Filter.atTop}