apply sum_pos
s : SelbergSieve
⊢ 0 < ∑ a ∈ filter (fun l => ↑l ^ 2 ≤ y) P.divisors, g a
case h
s : SelbergSieve
⊢ ∀ i ∈ filter (fun l => ↑l ^ 2 ≤ y) P.divisors, 0 < g i

case hs
s : SelbergSieve
⊢ (filter (fun l => ↑l ^ 2 ≤ y) P.divisors).Nonempty