gcongr
s : SelbergSieve
μPlus : UpperBoundSieve := s.selbergUbSieve
⊢ X * s.mainSum μPlus.μPlus + s.errSum μPlus.μPlus ≤ X / S + ∑ d ∈ P.divisors, if ↑d ≤ y then 3 ^ ω d * |s.rem d| else 0
case h₁
s : SelbergSieve
μPlus : UpperBoundSieve := s.selbergUbSieve
⊢ X * s.mainSum μPlus.μPlus ≤ X / S

case h₂
s : SelbergSieve
μPlus : UpperBoundSieve := s.selbergUbSieve
⊢ s.errSum μPlus.μPlus ≤ ∑ d ∈ P.divisors, if ↑d ≤ y then 3 ^ ω d * |s.rem d| else 0