English
Conditional summation over ℕ is given by limits over finite intervals, i.e., (conditional ℕ).filter = atTop.map Finset.range.
Русский
Условное суммирование над ℕ задаётся предельными суммами по конечным интервалам; (conditional ℕ).filter = atTop.map Finset.range.
LaTeX
$$$(conditional \\mathbb{N}).\\mathrm{filter} = atTop.map Finset.range$$$
Lean4
/-- Conditional summation over `ℕ` is given by limits of sums over `Finset.range n` as `n → ∞`. -/
@[simp high + 1] -- want this to be prioritized over `conditional_filter_eq_map_Ici`
theorem conditional_filter_eq_map_range : (conditional ℕ).filter = atTop.map Finset.range :=
by
have (n : ℕ) : Finset.Iic n = Finset.range (n + 1) := by ext x; simp [Nat.lt_succ]
simp only [conditional_filter_eq_map_Iic, funext this]
apply le_antisymm <;> rw [← Tendsto] <;> simp only [tendsto_atTop', mem_map, mem_atTop_sets, mem_preimage] <;>
rintro s ⟨a, ha⟩
· exact ⟨a + 1, fun b hb ↦ ha (b + 1) (by omega)⟩
· exact ⟨a + 1, fun b hb ↦ by convert ha (b - 1) (by omega); omega⟩
