Theorem: SelbergSieve.selberg_bound_simple_errSum (PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/Selberg.lean)

State before:
s : SelbergSieve
⊢ s.errSum μ⁺ ≤ ∑ d ∈ P.divisors, if ↑d ≤ y then 3 ^ ω d * |s.rem d| else 0
Tactic:
dsimp only [errSum]
State after:
s : SelbergSieve
⊢ ∑ d ∈ P.divisors, |s.selbergMuPlus d| * |s.rem d| ≤ ∑ d ∈ P.divisors, if ↑d ≤ y then 3 ^ ω d * |s.rem d| else 0

State before:
s : SelbergSieve
⊢ ∑ d ∈ P.divisors, |s.selbergMuPlus d| * |s.rem d| ≤ ∑ d ∈ P.divisors, if ↑d ≤ y then 3 ^ ω d * |s.rem d| else 0
Tactic:
gcongr with d hd
State after:
case h
s : SelbergSieve
d : ℕ
hd : d ∈ P.divisors
⊢ |s.selbergMuPlus d| * |s.rem d| ≤ if ↑d ≤ y then 3 ^ ω d * |s.rem d| else 0

State before:
case h
s : SelbergSieve
d : ℕ
hd : d ∈ P.divisors
⊢ |s.selbergMuPlus d| * |s.rem d| ≤ if ↑d ≤ y then 3 ^ ω d * |s.rem d| else 0
Tactic:
split_ifs with h
State after:
case pos
s : SelbergSieve
d : ℕ
hd : d ∈ P.divisors
h : ↑d ≤ y
⊢ |s.selbergMuPlus d| * |s.rem d| ≤ 3 ^ ω d * |s.rem d|

case neg
s : SelbergSieve
d : ℕ
hd : d ∈ P.divisors
h : ¬↑d ≤ y
⊢ |s.selbergMuPlus d| * |s.rem d| ≤ 0

State before:
case pos
s : SelbergSieve
d : ℕ
hd : d ∈ P.divisors
h : ↑d ≤ y
⊢ |s.selbergMuPlus d| * |s.rem d| ≤ 3 ^ ω d * |s.rem d|
Tactic:
apply mul_le_mul _ le_rfl (abs_nonneg <| R d) (pow_nonneg _ <| ω d)
State after:
s : SelbergSieve
d : ℕ
hd : d ∈ P.divisors
h : ↑d ≤ y
⊢ |s.selbergMuPlus d| ≤ 3 ^ ω d

s : SelbergSieve
d : ℕ
hd : d ∈ P.divisors
h : ↑d ≤ y
⊢ 0 ≤ 3

State before:
s : SelbergSieve
d : ℕ
hd : d ∈ P.divisors
h : ↑d ≤ y
⊢ |s.selbergMuPlus d| ≤ 3 ^ ω d

s : SelbergSieve
d : ℕ
hd : d ∈ P.divisors
h : ↑d ≤ y
⊢ 0 ≤ 3
Tactic:
apply s.selberg_bound_muPlus d hd
State after:
s : SelbergSieve
d : ℕ
hd : d ∈ P.divisors
h : ↑d ≤ y
⊢ 0 ≤ 3

State before:
s : SelbergSieve
d : ℕ
hd : d ∈ P.divisors
h : ↑d ≤ y
⊢ 0 ≤ 3
Tactic:
linarith
State after:
no goals

State before:
case neg
s : SelbergSieve
d : ℕ
hd : d ∈ P.divisors
h : ¬↑d ≤ y
⊢ |s.selbergMuPlus d| * |s.rem d| ≤ 0
Tactic:
rw [s.selbergμPlus_eq_zero d h, abs_zero, zero_mul]
State after:
no goals