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

State before:
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ 0 ≤ s.selbergWeights d * ↑(μ d)
Tactic:
dsimp only [selbergWeights]
State after:
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ 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)

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

State before:
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ 0 ≤ (ν d)⁻¹ * g d * ↑(μ d) * S⁻¹ * ((∑ m ∈ P.divisors, if (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0) * ↑(μ d))
Tactic:
trans ((μ d :ℝ)^2 * (ν d)⁻¹ * g d * S⁻¹ * ∑ 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
⊢ 0 ≤ ↑(μ d) ^ 2 * (ν d)⁻¹ * g d * S⁻¹ * ∑ m ∈ P.divisors, if (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0

s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ (↑(μ d) ^ 2 * (ν d)⁻¹ * g d * S⁻¹ * ∑ 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))

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

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

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

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

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

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

State before:
case ha
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ 0 ≤ ↑(μ d) ^ 2 * (ν d)⁻¹ * g d * S⁻¹

case hb
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ 0 ≤ ∑ m ∈ P.divisors, if (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0
Tactic:
apply div_nonneg
State after:
case ha.ha
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ 0 ≤ ↑(μ d) ^ 2 * (ν d)⁻¹ * g d

case ha.hb
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ 0 ≤ S

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

State before:
case ha.ha
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ 0 ≤ ↑(μ d) ^ 2 * (ν d)⁻¹ * g d

case ha.hb
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ 0 ≤ S

case hb
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ 0 ≤ ∑ m ∈ P.divisors, if (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0
Tactic:
apply mul_nonneg
State after:
case ha.ha.ha
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ 0 ≤ ↑(μ d) ^ 2 * (ν d)⁻¹

case ha.ha.hb
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ 0 ≤ g d

case ha.hb
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ 0 ≤ S

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

State before:
case ha.ha.ha
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ 0 ≤ ↑(μ d) ^ 2 * (ν d)⁻¹

case ha.ha.hb
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ 0 ≤ g d

case ha.hb
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ 0 ≤ S

case hb
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ 0 ≤ ∑ m ∈ P.divisors, if (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0
Tactic:
apply mul_nonneg
State after:
case ha.ha.ha.ha
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ 0 ≤ ↑(μ d) ^ 2

case ha.ha.ha.hb
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ 0 ≤ (ν d)⁻¹

case ha.ha.hb
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ 0 ≤ g d

case ha.hb
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ 0 ≤ S

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

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

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

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

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

State before:
case ha.ha.ha.ha
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ 0 ≤ ↑(μ d) ^ 2
Tactic:
apply sq_nonneg
State after:
no goals

State before:
case ha.ha.ha.hb
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ 0 ≤ (ν d)⁻¹
Tactic:
rw [inv_nonneg]
State after:
case ha.ha.ha.hb
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ 0 ≤ ν d

State before:
case ha.ha.ha.hb
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ 0 ≤ ν d
Tactic:
exact le_of_lt $ s.nu_pos_of_dvd_prodPrimes hdP
State after:
no goals

State before:
case ha.ha.hb
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ 0 ≤ g d
Tactic:
exact le_of_lt $ s.selbergTerms_pos d hdP
State after:
no goals

State before:
case ha.hb
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ 0 ≤ S
Tactic:
exact s.selbergBoundingSum_nonneg
State after:
no goals

State before:
case pos
s : SelbergSieve
d : ℕ
hdP : d ∣ P
m : ℕ
hm : m ∈ P.divisors
h : (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d
⊢ 0 ≤ g m
Tactic:
exact 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
m : ℕ
hm : m ∈ P.divisors
h : ¬((↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d)
⊢ 0 ≤ 0
Tactic:
rfl
State after:
no goals