apply boundingSum_ge_log
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (primeInterSieve x y z hz).selbergBoundingSum ≥ z.log / 2
case hnu
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (primeInterSieve x y z hz).nu = (↑ζ).pdiv ↑ArithmeticFunction.id

case hP
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ ∀ (p : ℕ), p.Prime → ↑p ≤ (primeInterSieve x y z hz).level → p ∣ (primeInterSieve x y z hz).prodPrimes