English
There exists a finite bound on the number of indices where a_i exceeds a positive ε, when the total sum is finite.
Русский
Существует конечная граница количества индексов, для которых a_i превышает положительный ε, если общая сумма конечна.
LaTeX
$$$\exists hf : {i : ι | ε \le a_i}.Finite, #hf.toFinset \le c / ε$ при заданных условиях.$$
Lean4
/-- A sum of extended nonnegative reals which is finite can have only finitely many terms
above any positive threshold. -/
theorem finite_const_le_of_tsum_ne_top {ι : Type*} {a : ι → ℝ≥0∞} (tsum_ne_top : ∑' i, a i ≠ ∞) {ε : ℝ≥0∞}
(ε_ne_zero : ε ≠ 0) : {i : ι | ε ≤ a i}.Finite := by
by_contra h
have := Infinite.to_subtype h
refine tsum_ne_top (top_unique ?_)
calc
∞ = ∑' _ : {i | ε ≤ a i}, ε := (tsum_const_eq_top_of_ne_zero ε_ne_zero).symm
_ ≤ ∑' i, a i :=
ENNReal.summable.tsum_le_tsum_of_inj (↑) Subtype.val_injective (fun _ _ => zero_le _) (fun i => i.2)
ENNReal.summable
