English
Let R be an ordered additive commutative monoid which is Archimedean, and let r > 0. For any subset s of natural numbers, s is infinite if and only if the partial sums of r times the indicator of s converge to infinity in R, i.e., the sequence ∑_{k=0}^{n-1} r · 1_{k∈s} tends to ∞ as n → ∞.
Русский
Пусть R — упорядоченная аддитивная коммутативная моноида, Архимедово, и пусть r > 0. Для любого подмножества s натуральных чисел множество s бесконечно, тогда частичные суммы суммы r на индикацию s расходятся к бесконечности; формально ∑_{k=0}^{n-1} r · 1_{k∈s} → ∞.
LaTeX
$$$s\\text{ is Infinite} \\iff atTop.Tendsto \\left(\\lambda n, \\sum_{k=0}^{n-1} s.indicator (\\lambda \\_ , r) k\\right) atTop$$$
Lean4
theorem infinite_iff_tendsto_sum_indicator_atTop {R : Type*} [AddCommMonoid R] [PartialOrder R] [IsOrderedAddMonoid R]
[AddLeftStrictMono R] [Archimedean R] {r : R} (h : 0 < r) {s : Set ℕ} :
s.Infinite ↔ atTop.Tendsto (fun n ↦ ∑ k ∈ Finset.range n, s.indicator (fun _ ↦ r) k) atTop :=
by
constructor
· have h_mono : Monotone fun n ↦ ∑ k ∈ Finset.range n, s.indicator (fun _ ↦ r) k :=
by
refine (sum_mono_set_of_nonneg ?_).comp range_mono
exact (fun _ ↦ indicator_nonneg (fun _ _ ↦ h.le) _)
rw [h_mono.tendsto_atTop_atTop_iff]
intro hs n
obtain ⟨n', hn'⟩ := exists_lt_nsmul h n
obtain ⟨t, t_s, t_card⟩ := hs.exists_subset_card_eq n'
obtain ⟨m, hm⟩ := t.bddAbove
refine ⟨m + 1, hn'.le.trans ?_⟩
apply (sum_le_sum fun i _ ↦ (indicator_le_indicator_of_subset t_s (fun _ ↦ h.le)) i).trans_eq'
have h : t ⊆ Finset.range (m + 1) := by
intro i i_t
rw [Finset.mem_range]
exact (hm i_t).trans_lt (lt_add_one m)
rw [sum_indicator_subset (fun _ ↦ r) h, sum_eq_card_nsmul (fun _ _ ↦ rfl), t_card]
· contrapose
intro hs
rw [not_infinite] at hs
rw [tendsto_congr' (sum_indicator_eventually_eq_card r hs), tendsto_atTop_atTop]
push_neg
obtain ⟨m, hm⟩ := exists_lt_nsmul h (Nat.card s • r)
exact ⟨m • r, fun n ↦ ⟨n, le_refl n, not_le_of_gt hm⟩⟩
