internlm/Lean-Github huggingface dataset:
Theorem: SelbergSieve.selbergBoundingSum_ge
Proof 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
Proof 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
Theorem: SelbergSieve.selbergBoundingSum_ge
Proof 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
Proof 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
Theorem: SelbergSieve.selbergBoundingSum_ge
Proof 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]
Proof 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
Theorem: SelbergSieve.selbergBoundingSum_ge
Proof 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
Proof state after:
no goals
Theorem: SelbergSieve.selbergBoundingSum_ge
Proof 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
Proof 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
Theorem: SelbergSieve.selbergBoundingSum_ge
Proof 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
Proof 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)
Theorem: SelbergSieve.selbergBoundingSum_ge
Proof 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
Proof 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
Theorem: SelbergSieve.selbergBoundingSum_ge
Proof 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
Proof 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
Theorem: SelbergSieve.selbergBoundingSum_ge
Proof 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
Proof 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
Theorem: SelbergSieve.selbergBoundingSum_ge
Proof 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
Proof 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
Theorem: SelbergSieve.selbergBoundingSum_ge
Proof 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)
Proof state after:
no goals
Theorem: SelbergSieve.selbergBoundingSum_ge
Proof 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
Proof 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
Theorem: SelbergSieve.selbergBoundingSum_ge
Proof 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 _
Proof 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
Theorem: SelbergSieve.selbergBoundingSum_ge
Proof 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
Proof 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
Theorem: SelbergSieve.selbergBoundingSum_ge
Proof 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
Proof 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
Theorem: SelbergSieve.selbergBoundingSum_ge
Proof 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
Proof 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
Theorem: SelbergSieve.selbergBoundingSum_ge
Proof 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)
Proof 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
Theorem: SelbergSieve.selbergBoundingSum_ge
Proof 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
Proof 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
Theorem: SelbergSieve.selbergBoundingSum_ge
Proof 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
Proof 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
Theorem: SelbergSieve.selbergBoundingSum_ge
Proof 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'
Proof 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
Theorem: SelbergSieve.selbergBoundingSum_ge
Proof 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
Proof 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
Theorem: SelbergSieve.selbergBoundingSum_ge
Proof 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
Proof 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
Theorem: SelbergSieve.selbergBoundingSum_ge
Proof 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
Proof 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
Theorem: SelbergSieve.selbergBoundingSum_ge
Proof 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
Proof state after:
no goals
Theorem: SelbergSieve.selbergBoundingSum_ge
Proof 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
Proof 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
Theorem: SelbergSieve.selbergBoundingSum_ge
Proof 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'
Proof 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
Theorem: SelbergSieve.selbergBoundingSum_ge
Proof 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⟩
Proof 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
Theorem: SelbergSieve.selbergBoundingSum_ge
Proof 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:ℝ)
Proof 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
Theorem: SelbergSieve.selbergBoundingSum_ge
Proof 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
Proof state after:
no goals
Theorem: SelbergSieve.selbergBoundingSum_ge
Proof 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
Proof 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
Theorem: SelbergSieve.selbergBoundingSum_ge
Proof 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
Proof 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
Theorem: SelbergSieve.selbergBoundingSum_ge
Proof 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
Proof 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
Theorem: SelbergSieve.selbergBoundingSum_ge
Proof 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
Proof 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
Theorem: SelbergSieve.selbergBoundingSum_ge
Proof 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
Proof state after:
no goals
Theorem: SelbergSieve.selbergBoundingSum_ge
Proof 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
Proof state after:
no goals
Theorem: SelbergSieve.selbergBoundingSum_ge
Proof 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
Proof state after:
no goals
Theorem: SelbergSieve.selbergBoundingSum_ge
Proof 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
Proof state after:
no goals
Theorem: SelbergSieve.selbergBoundingSum_ge
Proof 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
Proof state after:
no goals
Theorem: SelbergSieve.selbergBoundingSum_ge
Proof 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]
Proof 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
Theorem: SelbergSieve.selbergBoundingSum_ge
Proof 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]
Proof 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
Theorem: SelbergSieve.selbergBoundingSum_ge
Proof 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))
Proof 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
Theorem: SelbergSieve.selbergBoundingSum_ge
Proof 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]
Proof 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
Theorem: SelbergSieve.selbergBoundingSum_ge
Proof 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]
Proof 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
Theorem: SelbergSieve.selbergBoundingSum_ge
Proof 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
Proof state after:
no goals
Theorem: SelbergSieve.selbergBoundingSum_ge
Proof 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]
Proof 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
Theorem: SelbergSieve.selbergBoundingSum_ge
Proof 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
Proof state after:
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ Squarefree d

s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ S ≠ 0
Theorem: SelbergSieve.selbergBoundingSum_ge
Proof 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
Proof state after:
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ S ≠ 0