Theorem: BrunTitchmarsh.siftedSum_le (PrimeNumberTheoremAnd/BrunTitchmarsh.lean)

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz✝ : 1 ≤ z
hz : 1 < z
⊢ (primeInterSieve x y z ⋯).siftedSum ≤ 2 * y / z.log + 5 * z * (1 + z.log) ^ 3
Tactic:
apply le_trans (SelbergSieve.selberg_bound_simple ..)
State after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz✝ : 1 ≤ z
hz : 1 < z
⊢ ((primeInterSieve x y z ⋯).totalMass / (primeInterSieve x y z ⋯).selbergBoundingSum +
      ∑ d ∈ (primeInterSieve x y z ⋯).prodPrimes.divisors,
        if ↑d ≤ (primeInterSieve x y z ⋯).level then 3 ^ ω d * |(primeInterSieve x y z ⋯).rem d| else 0) ≤
    2 * y / z.log + 5 * z * (1 + z.log) ^ 3

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz✝ : 1 ≤ z
hz : 1 < z
⊢ ((primeInterSieve x y z ⋯).totalMass / (primeInterSieve x y z ⋯).selbergBoundingSum +
      ∑ d ∈ (primeInterSieve x y z ⋯).prodPrimes.divisors,
        if ↑d ≤ (primeInterSieve x y z ⋯).level then 3 ^ ω d * |(primeInterSieve x y z ⋯).rem d| else 0) ≤
    2 * y / z.log + 5 * z * (1 + z.log) ^ 3
Tactic:
calc _ ≤ y / (Real.log z / 2) + 5 * z * (1+Real.log z)^3 := ?_
     _ = _ := by ring
State after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz✝ : 1 ≤ z
hz : 1 < z
⊢ ((primeInterSieve x y z ⋯).totalMass / (primeInterSieve x y z ⋯).selbergBoundingSum +
      ∑ d ∈ (primeInterSieve x y z ⋯).prodPrimes.divisors,
        if ↑d ≤ (primeInterSieve x y z ⋯).level then 3 ^ ω d * |(primeInterSieve x y z ⋯).rem d| else 0) ≤
    y / (z.log / 2) + 5 * z * (1 + z.log) ^ 3

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz✝ : 1 ≤ z
hz : 1 < z
⊢ ((primeInterSieve x y z ⋯).totalMass / (primeInterSieve x y z ⋯).selbergBoundingSum +
      ∑ d ∈ (primeInterSieve x y z ⋯).prodPrimes.divisors,
        if ↑d ≤ (primeInterSieve x y z ⋯).level then 3 ^ ω d * |(primeInterSieve x y z ⋯).rem d| else 0) ≤
    y / (z.log / 2) + 5 * z * (1 + z.log) ^ 3
Tactic:
gcongr
State after:
case h₁.hd
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz✝ : 1 ≤ z
hz : 1 < z
⊢ 0 < z.log / 2

case h₁.hac
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz✝ : 1 ≤ z
hz : 1 < z
⊢ (primeInterSieve x y z ⋯).totalMass ≤ y

case h₁.hbd
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz✝ : 1 ≤ z
hz : 1 < z
⊢ z.log / 2 ≤ (primeInterSieve x y z ⋯).selbergBoundingSum

case h₂
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz✝ : 1 ≤ z
hz : 1 < z
⊢ (∑ d ∈ (primeInterSieve x y z ⋯).prodPrimes.divisors,
      if ↑d ≤ (primeInterSieve x y z ⋯).level then 3 ^ ω d * |(primeInterSieve x y z ⋯).rem d| else 0) ≤
    5 * z * (1 + z.log) ^ 3

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz✝ : 1 ≤ z
hz : 1 < z
⊢ y / (z.log / 2) + 5 * z * (1 + z.log) ^ 3 = 2 * y / z.log + 5 * z * (1 + z.log) ^ 3
Tactic:
ring
State after:
no goals

State before:
case h₁.hd
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz✝ : 1 ≤ z
hz : 1 < z
⊢ 0 < z.log / 2
Tactic:
linarith [Real.log_pos hz]
State after:
no goals

State before:
case h₁.hac
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz✝ : 1 ≤ z
hz : 1 < z
⊢ (primeInterSieve x y z ⋯).totalMass ≤ y
Tactic:
rfl
State after:
no goals

State before:
case h₁.hbd
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz✝ : 1 ≤ z
hz : 1 < z
⊢ z.log / 2 ≤ (primeInterSieve x y z ⋯).selbergBoundingSum
Tactic:
apply boudingSum_ge
State after:
no goals

State before:
case h₂
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz✝ : 1 ≤ z
hz : 1 < z
⊢ (∑ d ∈ (primeInterSieve x y z ⋯).prodPrimes.divisors,
      if ↑d ≤ (primeInterSieve x y z ⋯).level then 3 ^ ω d * |(primeInterSieve x y z ⋯).rem d| else 0) ≤
    5 * z * (1 + z.log) ^ 3
Tactic:
apply primeSieve_rem_sum_le x y z hx hy
State after:
no goals