Theorem: Sieve.rem_sum_le_of_const (PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/SelbergBounds.lean)

State before:
s : SelbergSieve
C : ℝ
hrem : ∀ d > 0, |s.rem d| ≤ C
⊢ (∑ d ∈ s.prodPrimes.divisors, if ↑d ≤ s.level then 3 ^ ω d * |s.rem d| else 0) ≤ C * s.level * (1 + s.level.log) ^ 3
Tactic:
rw [←Finset.sum_filter]
State after:
s : SelbergSieve
C : ℝ
hrem : ∀ d > 0, |s.rem d| ≤ C
⊢ ∑ a ∈ Finset.filter (fun d => ↑d ≤ s.level) s.prodPrimes.divisors, 3 ^ ω a * |s.rem a| ≤
    C * s.level * (1 + s.level.log) ^ 3

State before:
s : SelbergSieve
C : ℝ
hrem : ∀ d > 0, |s.rem d| ≤ C
⊢ ∑ a ∈ Finset.filter (fun d => ↑d ≤ s.level) s.prodPrimes.divisors, 3 ^ ω a * |s.rem a| ≤
    C * s.level * (1 + s.level.log) ^ 3
Tactic:
trans (∑ d in  Finset.filter (fun d:ℕ => ↑d ≤ s.level) (s.toSieve.prodPrimes.divisors),  3 ^ ω d * C )
State after:
s : SelbergSieve
C : ℝ
hrem : ∀ d > 0, |s.rem d| ≤ C
⊢ ∑ a ∈ Finset.filter (fun d => ↑d ≤ s.level) s.prodPrimes.divisors, 3 ^ ω a * |s.rem a| ≤
    ∑ d ∈ Finset.filter (fun d => ↑d ≤ s.level) s.prodPrimes.divisors, 3 ^ ω d * C

s : SelbergSieve
C : ℝ
hrem : ∀ d > 0, |s.rem d| ≤ C
⊢ ∑ d ∈ Finset.filter (fun d => ↑d ≤ s.level) s.prodPrimes.divisors, 3 ^ ω d * C ≤ C * s.level * (1 + s.level.log) ^ 3

State before:
s : SelbergSieve
C : ℝ
hrem : ∀ d > 0, |s.rem d| ≤ C
⊢ ∑ d ∈ Finset.filter (fun d => ↑d ≤ s.level) s.prodPrimes.divisors, 3 ^ ω d * C ≤ C * s.level * (1 + s.level.log) ^ 3
Tactic:
rw [←Finset.sum_mul, mul_comm, mul_assoc]
State after:
s : SelbergSieve
C : ℝ
hrem : ∀ d > 0, |s.rem d| ≤ C
⊢ C * ∑ i ∈ Finset.filter (fun d => ↑d ≤ s.level) s.prodPrimes.divisors, 3 ^ ω i ≤ C * (s.level * (1 + s.level.log) ^ 3)

State before:
s : SelbergSieve
C : ℝ
hrem : ∀ d > 0, |s.rem d| ≤ C
⊢ C * ∑ i ∈ Finset.filter (fun d => ↑d ≤ s.level) s.prodPrimes.divisors, 3 ^ ω i ≤ C * (s.level * (1 + s.level.log) ^ 3)
Tactic:
gcongr
State after:
case a0
s : SelbergSieve
C : ℝ
hrem : ∀ d > 0, |s.rem d| ≤ C
⊢ 0 ≤ C

case h
s : SelbergSieve
C : ℝ
hrem : ∀ d > 0, |s.rem d| ≤ C
⊢ ∑ i ∈ Finset.filter (fun d => ↑d ≤ s.level) s.prodPrimes.divisors, 3 ^ ω i ≤ s.level * (1 + s.level.log) ^ 3

State before:
case h
s : SelbergSieve
C : ℝ
hrem : ∀ d > 0, |s.rem d| ≤ C
⊢ ∑ i ∈ Finset.filter (fun d => ↑d ≤ s.level) s.prodPrimes.divisors, 3 ^ ω i ≤ s.level * (1 + s.level.log) ^ 3
Tactic:
rw [Finset.sum_filter]
State after:
case h
s : SelbergSieve
C : ℝ
hrem : ∀ d > 0, |s.rem d| ≤ C
⊢ (∑ a ∈ s.prodPrimes.divisors, if ↑a ≤ s.level then 3 ^ ω a else 0) ≤ s.level * (1 + s.level.log) ^ 3

State before:
case h
s : SelbergSieve
C : ℝ
hrem : ∀ d > 0, |s.rem d| ≤ C
⊢ (∑ a ∈ s.prodPrimes.divisors, if ↑a ≤ s.level then 3 ^ ω a else 0) ≤ s.level * (1 + s.level.log) ^ 3
Tactic:
apply Aux.sum_pow_cardDistinctFactors_le_self_mul_log_pow (hx := s.one_le_level)
State after:
case h
s : SelbergSieve
C : ℝ
hrem : ∀ d > 0, |s.rem d| ≤ C
⊢ Squarefree s.prodPrimes

State before:
case h
s : SelbergSieve
C : ℝ
hrem : ∀ d > 0, |s.rem d| ≤ C
⊢ Squarefree s.prodPrimes
Tactic:
apply Sieve.prodPrimes_squarefree
State after:
no goals

State before:
s : SelbergSieve
C : ℝ
hrem : ∀ d > 0, |s.rem d| ≤ C
⊢ ∑ a ∈ Finset.filter (fun d => ↑d ≤ s.level) s.prodPrimes.divisors, 3 ^ ω a * |s.rem a| ≤
    ∑ d ∈ Finset.filter (fun d => ↑d ≤ s.level) s.prodPrimes.divisors, 3 ^ ω d * C
Tactic:
gcongr with d hd
State after:
case h.h
s : SelbergSieve
C : ℝ
hrem : ∀ d > 0, |s.rem d| ≤ C
d : ℕ
hd : d ∈ Finset.filter (fun d => ↑d ≤ s.level) s.prodPrimes.divisors
⊢ |s.rem d| ≤ C

State before:
case h.h
s : SelbergSieve
C : ℝ
hrem : ∀ d > 0, |s.rem d| ≤ C
d : ℕ
hd : d ∈ Finset.filter (fun d => ↑d ≤ s.level) s.prodPrimes.divisors
⊢ |s.rem d| ≤ C
Tactic:
rw [Finset.mem_filter, Nat.mem_divisors] at hd
State after:
case h.h
s : SelbergSieve
C : ℝ
hrem : ∀ d > 0, |s.rem d| ≤ C
d : ℕ
hd : (d ∣ s.prodPrimes ∧ s.prodPrimes ≠ 0) ∧ ↑d ≤ s.level
⊢ |s.rem d| ≤ C

State before:
case h.h
s : SelbergSieve
C : ℝ
hrem : ∀ d > 0, |s.rem d| ≤ C
d : ℕ
hd : (d ∣ s.prodPrimes ∧ s.prodPrimes ≠ 0) ∧ ↑d ≤ s.level
⊢ |s.rem d| ≤ C
Tactic:
apply hrem d
State after:
case h.h
s : SelbergSieve
C : ℝ
hrem : ∀ d > 0, |s.rem d| ≤ C
d : ℕ
hd : (d ∣ s.prodPrimes ∧ s.prodPrimes ≠ 0) ∧ ↑d ≤ s.level
⊢ d > 0

State before:
case h.h
s : SelbergSieve
C : ℝ
hrem : ∀ d > 0, |s.rem d| ≤ C
d : ℕ
hd : (d ∣ s.prodPrimes ∧ s.prodPrimes ≠ 0) ∧ ↑d ≤ s.level
⊢ d > 0
Tactic:
apply Nat.pos_of_ne_zero
State after:
case h.h.a
s : SelbergSieve
C : ℝ
hrem : ∀ d > 0, |s.rem d| ≤ C
d : ℕ
hd : (d ∣ s.prodPrimes ∧ s.prodPrimes ≠ 0) ∧ ↑d ≤ s.level
⊢ d ≠ 0

State before:
case h.h.a
s : SelbergSieve
C : ℝ
hrem : ∀ d > 0, |s.rem d| ≤ C
d : ℕ
hd : (d ∣ s.prodPrimes ∧ s.prodPrimes ≠ 0) ∧ ↑d ≤ s.level
⊢ d ≠ 0
Tactic:
apply ne_zero_of_dvd_ne_zero hd.1.2 hd.1.1
State after:
no goals

State before:
case a0
s : SelbergSieve
C : ℝ
hrem : ∀ d > 0, |s.rem d| ≤ C
⊢ 0 ≤ C
Tactic:
linarith [abs_nonneg <| s.rem 1, hrem 1 (by norm_num)]
State after:
no goals

State before:
s : SelbergSieve
C : ℝ
hrem : ∀ d > 0, |s.rem d| ≤ C
⊢ 1 > 0
Tactic:
norm_num
State after:
no goals