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

State before:
s : SelbergSieve
d : ℕ
hd : ¬↑d ^ 2 ≤ y
⊢ s.selbergWeights d = 0
Tactic:
dsimp only [selbergWeights]
State after:
s : SelbergSieve
d : ℕ
hd : ¬↑d ^ 2 ≤ y
⊢ (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) =
    0

State before:
s : SelbergSieve
d : ℕ
hd : ¬↑d ^ 2 ≤ y
⊢ (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) =
    0
Tactic:
split_ifs with h
State after:
case pos
s : SelbergSieve
d : ℕ
hd : ¬↑d ^ 2 ≤ y
h : d ∣ P
⊢ ((ν d)⁻¹ * g d * ↑(μ d) * S⁻¹ * ∑ m ∈ P.divisors, if (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0) = 0

case neg
s : SelbergSieve
d : ℕ
hd : ¬↑d ^ 2 ≤ y
h : ¬d ∣ P
⊢ 0 = 0

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

State before:
case pos
s : SelbergSieve
d : ℕ
hd : ¬↑d ^ 2 ≤ y
h : d ∣ P
⊢ (∑ m ∈ P.divisors, if (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0) = 0
Tactic:
apply Finset.sum_eq_zero
State after:
case pos.h
s : SelbergSieve
d : ℕ
hd : ¬↑d ^ 2 ≤ y
h : d ∣ P
⊢ ∀ x ∈ P.divisors, (if (↑d * ↑x) ^ 2 ≤ y ∧ x.Coprime d then g x else 0) = 0

State before:
case pos.h
s : SelbergSieve
d : ℕ
hd : ¬↑d ^ 2 ≤ y
h : d ∣ P
⊢ ∀ x ∈ P.divisors, (if (↑d * ↑x) ^ 2 ≤ y ∧ x.Coprime d then g x else 0) = 0
Tactic:
refine fun m hm => if_neg ?_
State after:
case pos.h
s : SelbergSieve
d : ℕ
hd : ¬↑d ^ 2 ≤ y
h : d ∣ P
m : ℕ
hm : m ∈ P.divisors
⊢ ¬((↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d)

State before:
case pos.h
s : SelbergSieve
d : ℕ
hd : ¬↑d ^ 2 ≤ y
h : d ∣ P
m : ℕ
hm : m ∈ P.divisors
⊢ ¬((↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d)
Tactic:
intro hyp
State after:
case pos.h
s : SelbergSieve
d : ℕ
hd : ¬↑d ^ 2 ≤ y
h : d ∣ P
m : ℕ
hm : m ∈ P.divisors
hyp : (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d
⊢ False

State before:
case pos.h
s : SelbergSieve
d : ℕ
hd : ¬↑d ^ 2 ≤ y
h : d ∣ P
m : ℕ
hm : m ∈ P.divisors
hyp : (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d
⊢ False
Tactic:
have : (d^2:ℝ) ≤ (d*m)^2 := by
  norm_cast;
  refine Nat.pow_le_pow_of_le_left ?h 2
  exact Nat.le_mul_of_pos_right _ (Nat.pos_of_mem_divisors hm)
State after:
case pos.h
s : SelbergSieve
d : ℕ
hd : ¬↑d ^ 2 ≤ y
h : d ∣ P
m : ℕ
hm : m ∈ P.divisors
hyp : (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d
this : ↑d ^ 2 ≤ (↑d * ↑m) ^ 2
⊢ False

State before:
case pos.h
s : SelbergSieve
d : ℕ
hd : ¬↑d ^ 2 ≤ y
h : d ∣ P
m : ℕ
hm : m ∈ P.divisors
hyp : (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d
this : ↑d ^ 2 ≤ (↑d * ↑m) ^ 2
⊢ False
Tactic:
linarith [hyp.1]
State after:
no goals

State before:
s : SelbergSieve
d : ℕ
hd : ¬↑d ^ 2 ≤ y
h : d ∣ P
m : ℕ
hm : m ∈ P.divisors
hyp : (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d
⊢ ↑d ^ 2 ≤ (↑d * ↑m) ^ 2
Tactic:
norm_cast
State after:
s : SelbergSieve
d : ℕ
hd : ¬↑d ^ 2 ≤ y
h : d ∣ P
m : ℕ
hm : m ∈ P.divisors
hyp : (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d
⊢ d ^ 2 ≤ (d * m) ^ 2

State before:
s : SelbergSieve
d : ℕ
hd : ¬↑d ^ 2 ≤ y
h : d ∣ P
m : ℕ
hm : m ∈ P.divisors
hyp : (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d
⊢ d ^ 2 ≤ (d * m) ^ 2
Tactic:
refine Nat.pow_le_pow_of_le_left ?h 2
State after:
case h
s : SelbergSieve
d : ℕ
hd : ¬↑d ^ 2 ≤ y
h : d ∣ P
m : ℕ
hm : m ∈ P.divisors
hyp : (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d
⊢ d ≤ d * m

State before:
case h
s : SelbergSieve
d : ℕ
hd : ¬↑d ^ 2 ≤ y
h : d ∣ P
m : ℕ
hm : m ∈ P.divisors
hyp : (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d
⊢ d ≤ d * m
Tactic:
exact Nat.le_mul_of_pos_right _ (Nat.pos_of_mem_divisors hm)
State after:
no goals

State before:
case neg
s : SelbergSieve
d : ℕ
hd : ¬↑d ^ 2 ≤ y
h : ¬d ∣ P
⊢ 0 = 0
Tactic:
rfl
State after:
no goals