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

State before:
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ S = ∑ k ∈ P.divisors, ∑ l ∈ P.divisors, if k = d.gcd l ∧ ↑l ^ 2 ≤ y then g l else 0
Tactic:
dsimp only [selbergBoundingSum]
State after:
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ (∑ l ∈ P.divisors, if ↑l ^ 2 ≤ y then g l else 0) =
    ∑ k ∈ P.divisors, ∑ l ∈ P.divisors, if k = d.gcd l ∧ ↑l ^ 2 ≤ y then g l else 0

State before:
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ (∑ l ∈ P.divisors, if ↑l ^ 2 ≤ y then g l else 0) =
    ∑ k ∈ P.divisors, ∑ l ∈ P.divisors, if k = d.gcd l ∧ ↑l ^ 2 ≤ y then g l else 0
Tactic:
rw [sum_comm, sum_congr rfl]
State after:
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ ∀ x ∈ P.divisors, (if ↑x ^ 2 ≤ y then g x else 0) = ∑ x_1 ∈ P.divisors, if x_1 = d.gcd x ∧ ↑x ^ 2 ≤ y then g x else 0

State before:
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ ∀ x ∈ P.divisors, (if ↑x ^ 2 ≤ y then g x else 0) = ∑ x_1 ∈ P.divisors, if x_1 = d.gcd x ∧ ↑x ^ 2 ≤ y then g x else 0
Tactic:
intro l _
State after:
s : SelbergSieve
d : ℕ
hdP : d ∣ P
l : ℕ
a✝ : l ∈ P.divisors
⊢ (if ↑l ^ 2 ≤ y then g l else 0) = ∑ x ∈ P.divisors, if x = d.gcd l ∧ ↑l ^ 2 ≤ y then g l else 0

State before:
s : SelbergSieve
d : ℕ
hdP : d ∣ P
l : ℕ
a✝ : l ∈ P.divisors
⊢ (if ↑l ^ 2 ≤ y then g l else 0) = ∑ x ∈ P.divisors, if x = d.gcd l ∧ ↑l ^ 2 ≤ y then g l else 0
Tactic:
simp_rw [ite_and]
State after:
s : SelbergSieve
d : ℕ
hdP : d ∣ P
l : ℕ
a✝ : l ∈ P.divisors
⊢ (if ↑l ^ 2 ≤ y then g l else 0) = ∑ x ∈ P.divisors, if x = d.gcd l then if ↑l ^ 2 ≤ y then g l else 0 else 0

State before:
s : SelbergSieve
d : ℕ
hdP : d ∣ P
l : ℕ
a✝ : l ∈ P.divisors
⊢ (if ↑l ^ 2 ≤ y then g l else 0) = ∑ x ∈ P.divisors, if x = d.gcd l then if ↑l ^ 2 ≤ y then g l else 0 else 0
Tactic:
rw [←Aux.sum_intro]
State after:
case hd
s : SelbergSieve
d : ℕ
hdP : d ∣ P
l : ℕ
a✝ : l ∈ P.divisors
⊢ d.gcd l ∈ P.divisors

State before:
case hd
s : SelbergSieve
d : ℕ
hdP : d ∣ P
l : ℕ
a✝ : l ∈ P.divisors
⊢ d.gcd l ∈ P.divisors
Tactic:
rw [mem_divisors]
State after:
case hd
s : SelbergSieve
d : ℕ
hdP : d ∣ P
l : ℕ
a✝ : l ∈ P.divisors
⊢ d.gcd l ∣ P ∧ P ≠ 0

State before:
case hd
s : SelbergSieve
d : ℕ
hdP : d ∣ P
l : ℕ
a✝ : l ∈ P.divisors
⊢ d.gcd l ∣ P ∧ P ≠ 0
Tactic:
exact ⟨(Nat.gcd_dvd_left d l).trans (hdP), s.prodPrimes_ne_zero⟩
State after:
no goals

State before:
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ (∑ k ∈ P.divisors, ∑ l ∈ P.divisors, if k = d.gcd l ∧ ↑l ^ 2 ≤ y then g l else 0) =
    ∑ k ∈ P.divisors, if k ∣ d then g k * ∑ m ∈ P.divisors, if (↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0 else 0
Tactic:
apply sum_congr rfl
State after:
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ ∀ x ∈ P.divisors,
    (∑ l ∈ P.divisors, if x = d.gcd l ∧ ↑l ^ 2 ≤ y then g l else 0) =
      if x ∣ d then g x * ∑ m ∈ P.divisors, if (↑x * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0 else 0

State before:
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ ∀ x ∈ P.divisors,
    (∑ l ∈ P.divisors, if x = d.gcd l ∧ ↑l ^ 2 ≤ y then g l else 0) =
      if x ∣ d then g x * ∑ m ∈ P.divisors, if (↑x * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0 else 0
Tactic:
intro k hk
State after:
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
⊢ (∑ l ∈ P.divisors, if k = d.gcd l ∧ ↑l ^ 2 ≤ y then g l else 0) =
    if k ∣ d then g k * ∑ m ∈ P.divisors, if (↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0 else 0

State before:
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
⊢ (∑ l ∈ P.divisors, if k = d.gcd l ∧ ↑l ^ 2 ≤ y then g l else 0) =
    if k ∣ d then g k * ∑ m ∈ P.divisors, if (↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0 else 0
Tactic:
rw [mul_sum]
State after:
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
⊢ (∑ l ∈ P.divisors, if k = d.gcd l ∧ ↑l ^ 2 ≤ y then g l else 0) =
    if k ∣ d then ∑ i ∈ P.divisors, g k * if (↑k * ↑i) ^ 2 ≤ y ∧ i.Coprime d then g i else 0 else 0

State before:
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
⊢ (∑ l ∈ P.divisors, if k = d.gcd l ∧ ↑l ^ 2 ≤ y then g l else 0) =
    if k ∣ d then ∑ i ∈ P.divisors, g k * if (↑k * ↑i) ^ 2 ≤ y ∧ i.Coprime d then g i else 0 else 0
Tactic:
split_ifs with hkd
State after:
case pos
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : k ∣ d
⊢ (∑ l ∈ P.divisors, if k = d.gcd l ∧ ↑l ^ 2 ≤ y then g l else 0) =
    ∑ i ∈ P.divisors, g k * if (↑k * ↑i) ^ 2 ≤ y ∧ i.Coprime d then g i else 0

case neg
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : ¬k ∣ d
⊢ (∑ l ∈ P.divisors, if k = d.gcd l ∧ ↑l ^ 2 ≤ y then g l else 0) = 0

State before:
case pos
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : k ∣ d
⊢ (∑ l ∈ P.divisors, if k = d.gcd l ∧ ↑l ^ 2 ≤ y then g l else 0) =
    ∑ i ∈ P.divisors, g k * if (↑k * ↑i) ^ 2 ≤ y ∧ i.Coprime d then g i else 0

case neg
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : ¬k ∣ d
⊢ (∑ l ∈ P.divisors, if k = d.gcd l ∧ ↑l ^ 2 ≤ y then g l else 0) = 0
Tactic:
swap
State after:
case neg
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : ¬k ∣ d
⊢ (∑ l ∈ P.divisors, if k = d.gcd l ∧ ↑l ^ 2 ≤ y then g l else 0) = 0

case pos
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : k ∣ d
⊢ (∑ l ∈ P.divisors, if k = d.gcd l ∧ ↑l ^ 2 ≤ y then g l else 0) =
    ∑ i ∈ P.divisors, g k * if (↑k * ↑i) ^ 2 ≤ y ∧ i.Coprime d then g i else 0

State before:
case pos
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : k ∣ d
⊢ (∑ l ∈ P.divisors, if k = d.gcd l ∧ ↑l ^ 2 ≤ y then g l else 0) =
    ∑ i ∈ P.divisors, g k * if (↑k * ↑i) ^ 2 ≤ y ∧ i.Coprime d then g i else 0
Tactic:
rw [sum_mul_subst k P, sum_congr rfl]
State after:
case pos
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : k ∣ d
⊢ ∀ x ∈ P.divisors,
    (if k * x ∣ P then if k = d.gcd (k * x) ∧ ↑(k * x) ^ 2 ≤ y then g (k * x) else 0 else 0) =
      g k * if (↑k * ↑x) ^ 2 ≤ y ∧ x.Coprime d then g x else 0

case pos
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : k ∣ d
⊢ ∀ (l : ℕ), l ∣ P → ¬k ∣ l → (if k = d.gcd l ∧ ↑l ^ 2 ≤ y then g l else 0) = 0

State before:
case pos
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : k ∣ d
⊢ ∀ x ∈ P.divisors,
    (if k * x ∣ P then if k = d.gcd (k * x) ∧ ↑(k * x) ^ 2 ≤ y then g (k * x) else 0 else 0) =
      g k * if (↑k * ↑x) ^ 2 ≤ y ∧ x.Coprime d then g x else 0

case pos
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : k ∣ d
⊢ ∀ (l : ℕ), l ∣ P → ¬k ∣ l → (if k = d.gcd l ∧ ↑l ^ 2 ≤ y then g l else 0) = 0
Tactic:
intro m hm
State after:
case pos
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : k ∣ d
m : ℕ
hm : m ∈ P.divisors
⊢ (if k * m ∣ P then if k = d.gcd (k * m) ∧ ↑(k * m) ^ 2 ≤ y then g (k * m) else 0 else 0) =
    g k * if (↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0

case pos
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : k ∣ d
⊢ ∀ (l : ℕ), l ∣ P → ¬k ∣ l → (if k = d.gcd l ∧ ↑l ^ 2 ≤ y then g l else 0) = 0

State before:
case pos
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : k ∣ d
m : ℕ
hm : m ∈ P.divisors
⊢ (if k * m ∣ P then if k = d.gcd (k * m) ∧ ↑(k * m) ^ 2 ≤ y then g (k * m) else 0 else 0) =
    g k * if (↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0

case pos
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : k ∣ d
⊢ ∀ (l : ℕ), l ∣ P → ¬k ∣ l → (if k = d.gcd l ∧ ↑l ^ 2 ≤ y then g l else 0) = 0
Tactic:
rw [mul_ite_zero, ← ite_and]
State after:
case pos
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : k ∣ d
m : ℕ
hm : m ∈ P.divisors
⊢ (if k * m ∣ P ∧ k = d.gcd (k * m) ∧ ↑(k * m) ^ 2 ≤ y then g (k * m) else 0) =
    if (↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g k * g m else 0

case pos
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : k ∣ d
⊢ ∀ (l : ℕ), l ∣ P → ¬k ∣ l → (if k = d.gcd l ∧ ↑l ^ 2 ≤ y then g l else 0) = 0

State before:
case pos
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : k ∣ d
m : ℕ
hm : m ∈ P.divisors
⊢ (if k * m ∣ P ∧ k = d.gcd (k * m) ∧ ↑(k * m) ^ 2 ≤ y then g (k * m) else 0) =
    if (↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g k * g m else 0

case pos
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : k ∣ d
⊢ ∀ (l : ℕ), l ∣ P → ¬k ∣ l → (if k = d.gcd l ∧ ↑l ^ 2 ≤ y then g l else 0) = 0
Tactic:
apply if_ctx_congr _ _ fun _ => rfl
State after:
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : k ∣ d
m : ℕ
hm : m ∈ P.divisors
⊢ k * m ∣ P ∧ k = d.gcd (k * m) ∧ ↑(k * m) ^ 2 ≤ y ↔ (↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d

s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : k ∣ d
m : ℕ
hm : m ∈ P.divisors
⊢ (↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d → g (k * m) = g k * g m

case pos
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : k ∣ d
⊢ ∀ (l : ℕ), l ∣ P → ¬k ∣ l → (if k = d.gcd l ∧ ↑l ^ 2 ≤ y then g l else 0) = 0

State before:
case neg
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : ¬k ∣ d
⊢ (∑ l ∈ P.divisors, if k = d.gcd l ∧ ↑l ^ 2 ≤ y then g l else 0) = 0
Tactic:
rw [sum_eq_zero]
State after:
case neg
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : ¬k ∣ d
⊢ ∀ x ∈ P.divisors, (if k = d.gcd x ∧ ↑x ^ 2 ≤ y then g x else 0) = 0

State before:
case neg
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : ¬k ∣ d
⊢ ∀ x ∈ P.divisors, (if k = d.gcd x ∧ ↑x ^ 2 ≤ y then g x else 0) = 0
Tactic:
intro l _
State after:
case neg
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : ¬k ∣ d
l : ℕ
a✝ : l ∈ P.divisors
⊢ (if k = d.gcd l ∧ ↑l ^ 2 ≤ y then g l else 0) = 0

State before:
case neg
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : ¬k ∣ d
l : ℕ
a✝ : l ∈ P.divisors
⊢ (if k = d.gcd l ∧ ↑l ^ 2 ≤ y then g l else 0) = 0
Tactic:
rw [if_neg]
State after:
case neg.hnc
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : ¬k ∣ d
l : ℕ
a✝ : l ∈ P.divisors
⊢ ¬(k = d.gcd l ∧ ↑l ^ 2 ≤ y)

State before:
case neg.hnc
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : ¬k ∣ d
l : ℕ
a✝ : l ∈ P.divisors
⊢ ¬(k = d.gcd l ∧ ↑l ^ 2 ≤ y)
Tactic:
push_neg
State after:
case neg.hnc
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : ¬k ∣ d
l : ℕ
a✝ : l ∈ P.divisors
⊢ k = d.gcd l → y < ↑l ^ 2

State before:
case neg.hnc
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : ¬k ∣ d
l : ℕ
a✝ : l ∈ P.divisors
⊢ k = d.gcd l → y < ↑l ^ 2
Tactic:
intro h
State after:
case neg.hnc
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : ¬k ∣ d
l : ℕ
a✝ : l ∈ P.divisors
h : k = d.gcd l
⊢ y < ↑l ^ 2

State before:
case neg.hnc
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : ¬k ∣ d
l : ℕ
a✝ : l ∈ P.divisors
h : k = d.gcd l
⊢ y < ↑l ^ 2
Tactic:
exfalso
State after:
case neg.hnc
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : ¬k ∣ d
l : ℕ
a✝ : l ∈ P.divisors
h : k = d.gcd l
⊢ False

State before:
case neg.hnc
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : ¬k ∣ d
l : ℕ
a✝ : l ∈ P.divisors
h : k = d.gcd l
⊢ False
Tactic:
rw [h] at hkd
State after:
case neg.hnc
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
l : ℕ
hkd : ¬d.gcd l ∣ d
a✝ : l ∈ P.divisors
h : k = d.gcd l
⊢ False

State before:
case neg.hnc
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
l : ℕ
hkd : ¬d.gcd l ∣ d
a✝ : l ∈ P.divisors
h : k = d.gcd l
⊢ False
Tactic:
exact hkd $ Nat.gcd_dvd_left d l
State after:
no goals

State before:
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : k ∣ d
m : ℕ
hm : m ∈ P.divisors
⊢ k * m ∣ P ∧ k = d.gcd (k * m) ∧ ↑(k * m) ^ 2 ≤ y ↔ (↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d
Tactic:
exact_mod_cast s._helper hkd hk hm
State after:
no goals

State before:
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : k ∣ d
m : ℕ
hm : m ∈ P.divisors
⊢ (↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d → g (k * m) = g k * g m
Tactic:
intro h
State after:
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : k ∣ d
m : ℕ
hm : m ∈ P.divisors
h : (↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d
⊢ g (k * m) = g k * g m

State before:
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : k ∣ d
m : ℕ
hm : m ∈ P.divisors
h : (↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d
⊢ g (k * m) = g k * g m
Tactic:
apply s.selbergTerms_mult.2
State after:
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : k ∣ d
m : ℕ
hm : m ∈ P.divisors
h : (↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d
⊢ k.Coprime m

State before:
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : k ∣ d
m : ℕ
hm : m ∈ P.divisors
h : (↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d
⊢ k.Coprime m
Tactic:
rw [coprime_comm]
State after:
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : k ∣ d
m : ℕ
hm : m ∈ P.divisors
h : (↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d
⊢ m.Coprime k

State before:
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : k ∣ d
m : ℕ
hm : m ∈ P.divisors
h : (↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d
⊢ m.Coprime k
Tactic:
apply h.2.coprime_dvd_right hkd
State after:
no goals

State before:
case pos
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : k ∣ d
⊢ ∀ (l : ℕ), l ∣ P → ¬k ∣ l → (if k = d.gcd l ∧ ↑l ^ 2 ≤ y then g l else 0) = 0
Tactic:
intro l _ hkl
State after:
case pos
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : k ∣ d
l : ℕ
a✝ : l ∣ P
hkl : ¬k ∣ l
⊢ (if k = d.gcd l ∧ ↑l ^ 2 ≤ y then g l else 0) = 0

State before:
case pos
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : k ∣ d
l : ℕ
a✝ : l ∣ P
hkl : ¬k ∣ l
⊢ (if k = d.gcd l ∧ ↑l ^ 2 ≤ y then g l else 0) = 0
Tactic:
apply if_neg
State after:
case pos.hnc
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : k ∣ d
l : ℕ
a✝ : l ∣ P
hkl : ¬k ∣ l
⊢ ¬(k = d.gcd l ∧ ↑l ^ 2 ≤ y)

State before:
case pos.hnc
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : k ∣ d
l : ℕ
a✝ : l ∣ P
hkl : ¬k ∣ l
⊢ ¬(k = d.gcd l ∧ ↑l ^ 2 ≤ y)
Tactic:
push_neg
State after:
case pos.hnc
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : k ∣ d
l : ℕ
a✝ : l ∣ P
hkl : ¬k ∣ l
⊢ k = d.gcd l → y < ↑l ^ 2

State before:
case pos.hnc
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : k ∣ d
l : ℕ
a✝ : l ∣ P
hkl : ¬k ∣ l
⊢ k = d.gcd l → y < ↑l ^ 2
Tactic:
intro h
State after:
case pos.hnc
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : k ∣ d
l : ℕ
a✝ : l ∣ P
hkl : ¬k ∣ l
h : k = d.gcd l
⊢ y < ↑l ^ 2

State before:
case pos.hnc
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : k ∣ d
l : ℕ
a✝ : l ∣ P
hkl : ¬k ∣ l
h : k = d.gcd l
⊢ y < ↑l ^ 2
Tactic:
exfalso
State after:
case pos.hnc
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : k ∣ d
l : ℕ
a✝ : l ∣ P
hkl : ¬k ∣ l
h : k = d.gcd l
⊢ False

State before:
case pos.hnc
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : k ∣ d
l : ℕ
a✝ : l ∣ P
hkl : ¬k ∣ l
h : k = d.gcd l
⊢ False
Tactic:
rw [h] at hkl
State after:
case pos.hnc
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : k ∣ d
l : ℕ
a✝ : l ∣ P
hkl : ¬d.gcd l ∣ l
h : k = d.gcd l
⊢ False

State before:
case pos.hnc
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : k ∣ d
l : ℕ
a✝ : l ∣ P
hkl : ¬d.gcd l ∣ l
h : k = d.gcd l
⊢ False
Tactic:
exact hkl (Nat.gcd_dvd_right d l)
State after:
no goals

State before:
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ (∑ k ∈ P.divisors, if k ∣ d then g k * ∑ m ∈ P.divisors, if (↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0 else 0) ≥
    ∑ k ∈ P.divisors, if k ∣ d then g k * ∑ m ∈ P.divisors, if (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0 else 0
Tactic:
apply sum_le_sum
State after:
case h
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ ∀ i ∈ P.divisors,
    (if i ∣ d then g i * ∑ m ∈ P.divisors, if (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0 else 0) ≤
      if i ∣ d then g i * ∑ m ∈ P.divisors, if (↑i * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0 else 0

State before:
case h
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ ∀ i ∈ P.divisors,
    (if i ∣ d then g i * ∑ m ∈ P.divisors, if (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0 else 0) ≤
      if i ∣ d then g i * ∑ m ∈ P.divisors, if (↑i * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0 else 0
Tactic:
intro k _
State after:
case h
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
a✝ : k ∈ P.divisors
⊢ (if k ∣ d then g k * ∑ m ∈ P.divisors, if (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0 else 0) ≤
    if k ∣ d then g k * ∑ m ∈ P.divisors, if (↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0 else 0

State before:
case h
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
a✝ : k ∈ P.divisors
⊢ (if k ∣ d then g k * ∑ m ∈ P.divisors, if (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0 else 0) ≤
    if k ∣ d then g k * ∑ m ∈ P.divisors, if (↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0 else 0
Tactic:
split_ifs with hkd
State after:
case pos
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
a✝ : k ∈ P.divisors
hkd : k ∣ d
⊢ (g k * ∑ m ∈ P.divisors, if (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0) ≤
    g k * ∑ m ∈ P.divisors, if (↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0

case neg
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
a✝ : k ∈ P.divisors
hkd : ¬k ∣ d
⊢ 0 ≤ 0

State before:
case pos
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
a✝ : k ∈ P.divisors
hkd : k ∣ d
⊢ (g k * ∑ m ∈ P.divisors, if (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0) ≤
    g k * ∑ m ∈ P.divisors, if (↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0

case neg
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
a✝ : k ∈ P.divisors
hkd : ¬k ∣ d
⊢ 0 ≤ 0
Tactic:
swap
State after:
case neg
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
a✝ : k ∈ P.divisors
hkd : ¬k ∣ d
⊢ 0 ≤ 0

case pos
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
a✝ : k ∈ P.divisors
hkd : k ∣ d
⊢ (g k * ∑ m ∈ P.divisors, if (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0) ≤
    g k * ∑ m ∈ P.divisors, if (↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0

State before:
case neg
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
a✝ : k ∈ P.divisors
hkd : ¬k ∣ d
⊢ 0 ≤ 0

case pos
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
a✝ : k ∈ P.divisors
hkd : k ∣ d
⊢ (g k * ∑ m ∈ P.divisors, if (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0) ≤
    g k * ∑ m ∈ P.divisors, if (↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0
Tactic:
rfl
State after:
case pos
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
a✝ : k ∈ P.divisors
hkd : k ∣ d
⊢ (g k * ∑ m ∈ P.divisors, if (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0) ≤
    g k * ∑ m ∈ P.divisors, if (↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0

State before:
case pos
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
a✝ : k ∈ P.divisors
hkd : k ∣ d
⊢ (g k * ∑ m ∈ P.divisors, if (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0) ≤
    g k * ∑ m ∈ P.divisors, if (↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0
Tactic:
apply mul_le_mul le_rfl _ _ (le_of_lt $ s.selbergTerms_pos k $ Trans.trans hkd hdP)
State after:
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
a✝ : k ∈ P.divisors
hkd : k ∣ d
⊢ (∑ m ∈ P.divisors, if (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0) ≤
    ∑ m ∈ P.divisors, if (↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0

s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
a✝ : k ∈ P.divisors
hkd : k ∣ d
⊢ 0 ≤ ∑ m ∈ P.divisors, if (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0

State before:
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
a✝ : k ∈ P.divisors
hkd : k ∣ d
⊢ (∑ m ∈ P.divisors, if (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0) ≤
    ∑ m ∈ P.divisors, if (↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0

s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
a✝ : k ∈ P.divisors
hkd : k ∣ d
⊢ 0 ≤ ∑ m ∈ P.divisors, if (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0
Tactic:
apply sum_le_sum
State after:
case h
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
a✝ : k ∈ P.divisors
hkd : k ∣ d
⊢ ∀ i ∈ P.divisors,
    (if (↑d * ↑i) ^ 2 ≤ y ∧ i.Coprime d then g i else 0) ≤ if (↑k * ↑i) ^ 2 ≤ y ∧ i.Coprime d then g i else 0

s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
a✝ : k ∈ P.divisors
hkd : k ∣ d
⊢ 0 ≤ ∑ m ∈ P.divisors, if (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0

State before:
case h
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
a✝ : k ∈ P.divisors
hkd : k ∣ d
⊢ ∀ i ∈ P.divisors,
    (if (↑d * ↑i) ^ 2 ≤ y ∧ i.Coprime d then g i else 0) ≤ if (↑k * ↑i) ^ 2 ≤ y ∧ i.Coprime d then g i else 0

s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
a✝ : k ∈ P.divisors
hkd : k ∣ d
⊢ 0 ≤ ∑ m ∈ P.divisors, if (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0
Tactic:
intro m hm
State after:
case h
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
a✝ : k ∈ P.divisors
hkd : k ∣ d
m : ℕ
hm : m ∈ P.divisors
⊢ (if (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0) ≤ if (↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0

s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
a✝ : k ∈ P.divisors
hkd : k ∣ d
⊢ 0 ≤ ∑ m ∈ P.divisors, if (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0

State before:
case h
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
a✝ : k ∈ P.divisors
hkd : k ∣ d
m : ℕ
hm : m ∈ P.divisors
⊢ (if (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0) ≤ if (↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0

s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
a✝ : k ∈ P.divisors
hkd : k ∣ d
⊢ 0 ≤ ∑ m ∈ P.divisors, if (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0
Tactic:
split_ifs with h h' h'
State after:
case pos
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
a✝ : k ∈ P.divisors
hkd : k ∣ d
m : ℕ
hm : m ∈ P.divisors
h : (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d
h' : (↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d
⊢ g m ≤ g m

case neg
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
a✝ : k ∈ P.divisors
hkd : k ∣ d
m : ℕ
hm : m ∈ P.divisors
h : (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d
h' : ¬((↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d)
⊢ g m ≤ 0

case pos
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
a✝ : k ∈ P.divisors
hkd : k ∣ d
m : ℕ
hm : m ∈ P.divisors
h : ¬((↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d)
h' : (↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d
⊢ 0 ≤ g m

case neg
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
a✝ : k ∈ P.divisors
hkd : k ∣ d
m : ℕ
hm : m ∈ P.divisors
h : ¬((↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d)
h' : ¬((↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d)
⊢ 0 ≤ 0

s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
a✝ : k ∈ P.divisors
hkd : k ∣ d
⊢ 0 ≤ ∑ m ∈ P.divisors, if (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0

State before:
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
a✝ : k ∈ P.divisors
hkd : k ∣ d
⊢ 0 ≤ ∑ m ∈ P.divisors, if (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0
Tactic:
apply sum_nonneg
State after:
case h
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
a✝ : k ∈ P.divisors
hkd : k ∣ d
⊢ ∀ i ∈ P.divisors, 0 ≤ if (↑d * ↑i) ^ 2 ≤ y ∧ i.Coprime d then g i else 0

State before:
case h
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
a✝ : k ∈ P.divisors
hkd : k ∣ d
⊢ ∀ i ∈ P.divisors, 0 ≤ if (↑d * ↑i) ^ 2 ≤ y ∧ i.Coprime d then g i else 0
Tactic:
intro m hm
State after:
case h
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
a✝ : k ∈ P.divisors
hkd : k ∣ d
m : ℕ
hm : m ∈ P.divisors
⊢ 0 ≤ if (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0

State before:
case h
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
a✝ : k ∈ P.divisors
hkd : k ∣ d
m : ℕ
hm : m ∈ P.divisors
⊢ 0 ≤ if (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0
Tactic:
split_ifs
State after:
case pos
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
a✝ : k ∈ P.divisors
hkd : k ∣ d
m : ℕ
hm : m ∈ P.divisors
h✝ : (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d
⊢ 0 ≤ g m

case neg
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
a✝ : k ∈ P.divisors
hkd : k ∣ d
m : ℕ
hm : m ∈ P.divisors
h✝ : ¬((↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d)
⊢ 0 ≤ 0

State before:
case pos
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
a✝ : k ∈ P.divisors
hkd : k ∣ d
m : ℕ
hm : m ∈ P.divisors
h : (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d
h' : (↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d
⊢ g m ≤ g m
Tactic:
rfl
State after:
no goals

State before:
case neg
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
a✝ : k ∈ P.divisors
hkd : k ∣ d
m : ℕ
hm : m ∈ P.divisors
h : (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d
h' : ¬((↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d)
⊢ g m ≤ 0
Tactic:
exfalso
State after:
case neg
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
a✝ : k ∈ P.divisors
hkd : k ∣ d
m : ℕ
hm : m ∈ P.divisors
h : (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d
h' : ¬((↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d)
⊢ False

State before:
case neg
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
a✝ : k ∈ P.divisors
hkd : k ∣ d
m : ℕ
hm : m ∈ P.divisors
h : (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d
h' : ¬((↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d)
⊢ False
Tactic:
apply h'
State after:
case neg
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
a✝ : k ∈ P.divisors
hkd : k ∣ d
m : ℕ
hm : m ∈ P.divisors
h : (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d
h' : ¬((↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d)
⊢ (↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d

State before:
case neg
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
a✝ : k ∈ P.divisors
hkd : k ∣ d
m : ℕ
hm : m ∈ P.divisors
h : (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d
h' : ¬((↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d)
⊢ (↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d
Tactic:
refine ⟨?_, h.2⟩
State after:
case neg
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
a✝ : k ∈ P.divisors
hkd : k ∣ d
m : ℕ
hm : m ∈ P.divisors
h : (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d
h' : ¬((↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d)
⊢ (↑k * ↑m) ^ 2 ≤ y

State before:
case neg
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
a✝ : k ∈ P.divisors
hkd : k ∣ d
m : ℕ
hm : m ∈ P.divisors
h : (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d
h' : ¬((↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d)
⊢ (↑k * ↑m) ^ 2 ≤ y
Tactic:
trans ((d*m)^2:ℝ)
State after:
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
a✝ : k ∈ P.divisors
hkd : k ∣ d
m : ℕ
hm : m ∈ P.divisors
h : (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d
h' : ¬((↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d)
⊢ (↑k * ↑m) ^ 2 ≤ (↑d * ↑m) ^ 2

s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
a✝ : k ∈ P.divisors
hkd : k ∣ d
m : ℕ
hm : m ∈ P.divisors
h : (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d
h' : ¬((↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d)
⊢ (↑d * ↑m) ^ 2 ≤ y

State before:
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
a✝ : k ∈ P.divisors
hkd : k ∣ d
m : ℕ
hm : m ∈ P.divisors
h : (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d
h' : ¬((↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d)
⊢ (↑d * ↑m) ^ 2 ≤ y
Tactic:
exact h.1
State after:
no goals

State before:
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
a✝ : k ∈ P.divisors
hkd : k ∣ d
m : ℕ
hm : m ∈ P.divisors
h : (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d
h' : ¬((↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d)
⊢ (↑k * ↑m) ^ 2 ≤ (↑d * ↑m) ^ 2
Tactic:
norm_cast
State after:
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
a✝ : k ∈ P.divisors
hkd : k ∣ d
m : ℕ
hm : m ∈ P.divisors
h : (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d
h' : ¬((↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d)
⊢ (k * m) ^ 2 ≤ (d * m) ^ 2

State before:
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
a✝ : k ∈ P.divisors
hkd : k ∣ d
m : ℕ
hm : m ∈ P.divisors
h : (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d
h' : ¬((↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d)
⊢ (k * m) ^ 2 ≤ (d * m) ^ 2
Tactic:
gcongr
State after:
case hab.bc
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
a✝ : k ∈ P.divisors
hkd : k ∣ d
m : ℕ
hm : m ∈ P.divisors
h : (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d
h' : ¬((↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d)
⊢ k ≤ d

State before:
case hab.bc
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
a✝ : k ∈ P.divisors
hkd : k ∣ d
m : ℕ
hm : m ∈ P.divisors
h : (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d
h' : ¬((↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d)
⊢ k ≤ d
Tactic:
refine Nat.le_of_dvd ?_ hkd
State after:
case hab.bc
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
a✝ : k ∈ P.divisors
hkd : k ∣ d
m : ℕ
hm : m ∈ P.divisors
h : (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d
h' : ¬((↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d)
⊢ 0 < d

State before:
case hab.bc
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
a✝ : k ∈ P.divisors
hkd : k ∣ d
m : ℕ
hm : m ∈ P.divisors
h : (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d
h' : ¬((↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d)
⊢ 0 < d
Tactic:
apply Nat.pos_of_ne_zero
State after:
case hab.bc.a
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
a✝ : k ∈ P.divisors
hkd : k ∣ d
m : ℕ
hm : m ∈ P.divisors
h : (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d
h' : ¬((↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d)
⊢ d ≠ 0

State before:
case hab.bc.a
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
a✝ : k ∈ P.divisors
hkd : k ∣ d
m : ℕ
hm : m ∈ P.divisors
h : (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d
h' : ¬((↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d)
⊢ d ≠ 0
Tactic:
apply ne_zero_of_dvd_ne_zero s.prodPrimes_ne_zero hdP
State after:
no goals

State before:
case pos
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
a✝ : k ∈ P.divisors
hkd : k ∣ d
m : ℕ
hm : m ∈ P.divisors
h : ¬((↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d)
h' : (↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d
⊢ 0 ≤ g m
Tactic:
refine le_of_lt $ s.selbergTerms_pos m $ dvd_of_mem_divisors hm
State after:
no goals

State before:
case neg
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
a✝ : k ∈ P.divisors
hkd : k ∣ d
m : ℕ
hm : m ∈ P.divisors
h : ¬((↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d)
h' : ¬((↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d)
⊢ 0 ≤ 0
Tactic:
rfl
State after:
no goals

State before:
case pos
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
a✝ : k ∈ P.divisors
hkd : k ∣ d
m : ℕ
hm : m ∈ P.divisors
h✝ : (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d
⊢ 0 ≤ g m
Tactic:
apply le_of_lt $ s.selbergTerms_pos m $ dvd_of_mem_divisors hm
State after:
no goals

State before:
case neg
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
a✝ : k ∈ P.divisors
hkd : k ∣ d
m : ℕ
hm : m ∈ P.divisors
h✝ : ¬((↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d)
⊢ 0 ≤ 0
Tactic:
rfl
State after:
no goals

State before:
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ (∑ k ∈ P.divisors, if k ∣ d then g k * ∑ m ∈ P.divisors, if (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0 else 0) =
    s.selbergWeights d * ↑(μ d) * S
Tactic:
conv => enter [1, 2, k]; rw [← ite_zero_mul]
State after:
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ (∑ k ∈ P.divisors,
      (if k ∣ d then g k else 0) * ∑ m ∈ P.divisors, if (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0) =
    s.selbergWeights d * ↑(μ d) * S

State before:
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ (∑ k ∈ P.divisors,
      (if k ∣ d then g k else 0) * ∑ m ∈ P.divisors, if (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0) =
    s.selbergWeights d * ↑(μ d) * S
Tactic:
rw [←sum_mul, s.conv_selbergTerms_eq_selbergTerms_mul_nu hdP]
State after:
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ (g d * (ν d)⁻¹ * ∑ m ∈ P.divisors, if (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0) =
    s.selbergWeights d * ↑(μ d) * S

State before:
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ (g d * (ν d)⁻¹ * ∑ m ∈ P.divisors, if (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0) =
    s.selbergWeights d * ↑(μ d) * S
Tactic:
trans (S * S⁻¹ * (μ d:ℝ)^2 * (ν d)⁻¹ * g d * (∑ m in divisors P, if (d*m) ^ 2 ≤ y ∧ Coprime m d then g m else 0))
State after:
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ (g d * (ν d)⁻¹ * ∑ m ∈ P.divisors, if (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0) =
    S * S⁻¹ * ↑(μ d) ^ 2 * (ν d)⁻¹ * g d * ∑ m ∈ P.divisors, if (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0

s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ (S * S⁻¹ * ↑(μ d) ^ 2 * (ν d)⁻¹ * g d * ∑ m ∈ P.divisors, if (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0) =
    s.selbergWeights d * ↑(μ d) * S

State before:
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ (S * S⁻¹ * ↑(μ d) ^ 2 * (ν d)⁻¹ * g d * ∑ m ∈ P.divisors, if (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0) =
    s.selbergWeights d * ↑(μ d) * S
Tactic:
dsimp only [selbergWeights]
State after:
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ (S * S⁻¹ * ↑(μ d) ^ 2 * (ν d)⁻¹ * g d * ∑ m ∈ P.divisors, if (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0) =
    (if d ∣ P then (ν d)⁻¹ * g d * ↑(μ d) * S⁻¹ * ∑ m ∈ P.divisors, if (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0
        else 0) *
        ↑(μ d) *
      S

State before:
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ (S * S⁻¹ * ↑(μ d) ^ 2 * (ν d)⁻¹ * g d * ∑ m ∈ P.divisors, if (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0) =
    (if d ∣ P then (ν d)⁻¹ * g d * ↑(μ d) * S⁻¹ * ∑ m ∈ P.divisors, if (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0
        else 0) *
        ↑(μ d) *
      S
Tactic:
rw [if_pos hdP]
State after:
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ (S * S⁻¹ * ↑(μ d) ^ 2 * (ν d)⁻¹ * g d * ∑ m ∈ P.divisors, if (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0) =
    ((ν d)⁻¹ * g d * ↑(μ d) * S⁻¹ * ∑ m ∈ P.divisors, if (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0) * ↑(μ d) * S

State before:
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ (S * S⁻¹ * ↑(μ d) ^ 2 * (ν d)⁻¹ * g d * ∑ m ∈ P.divisors, if (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0) =
    ((ν d)⁻¹ * g d * ↑(μ d) * S⁻¹ * ∑ m ∈ P.divisors, if (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0) * ↑(μ d) * S
Tactic:
ring
State after:
no goals

State before:
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ (g d * (ν d)⁻¹ * ∑ m ∈ P.divisors, if (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0) =
    S * S⁻¹ * ↑(μ d) ^ 2 * (ν d)⁻¹ * g d * ∑ m ∈ P.divisors, if (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0
Tactic:
rw [mul_inv_cancel, ←Int.cast_pow, moebius_sq_eq_one_of_squarefree]
State after:
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ (g d * (ν d)⁻¹ * ∑ m ∈ P.divisors, if (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0) =
    1 * ↑1 * (ν d)⁻¹ * g d * ∑ m ∈ P.divisors, if (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0

s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ Squarefree d

s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ S ≠ 0

State before:
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ (g d * (ν d)⁻¹ * ∑ m ∈ P.divisors, if (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0) =
    1 * ↑1 * (ν d)⁻¹ * g d * ∑ m ∈ P.divisors, if (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0

s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ Squarefree d

s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ S ≠ 0
Tactic:
ring
State after:
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ Squarefree d

s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ S ≠ 0

State before:
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ Squarefree d

s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ S ≠ 0
Tactic:
exact Squarefree.squarefree_of_dvd hdP s.prodPrimes_squarefree
State after:
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ S ≠ 0

State before:
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ S ≠ 0
Tactic:
exact _root_.ne_of_gt $ s.selbergBoundingSum_pos
State after:
no goals