tendsto_tsum_compl_atTop_zero — Mathlib

English

As the finite complement grows to cover all of α, the sum over the complement tends to 0.

Русский

По мере того как дополнительное множество растет, сумма над комплементом стремится к нулю.

LaTeX

$$Tendsto (s : Finset α) (sum' b : { b // b ∉ s }, f b) atTop (nhds 0)$$

Lean4

/-- The sum over the complement of a finset tends to `0` when the finset grows to cover the whole
space. This does not need a summability assumption, as otherwise all sums are zero. -/
nonrec theorem tendsto_tsum_compl_atTop_zero {α : Type*} (f : α → ℝ≥0) :
    Tendsto (fun s : Finset α => ∑' b : { x // x ∉ s }, f b) atTop (𝓝 0) :=
  by
  simp_rw [← tendsto_coe, coe_tsum, NNReal.coe_zero]
  exact tendsto_tsum_compl_atTop_zero fun a : α => (f a : ℝ)

Похожие утверждения