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

State before:
s : SelbergSieve
⊢ s.mainSum μ⁺ = S⁻¹
Tactic:
rw [mainSum_eq_diag_quad_form]
State after:
s : SelbergSieve
⊢ ∑ l ∈ P.divisors, 1 / g l * (∑ d ∈ P.divisors, if l ∣ d then ν d * s.selbergWeights d else 0) ^ 2 = S⁻¹

State before:
s : SelbergSieve
⊢ ∑ l ∈ P.divisors, 1 / g l * (∑ d ∈ P.divisors, if l ∣ d then ν d * s.selbergWeights d else 0) ^ 2 = S⁻¹
Tactic:
trans (∑ l in divisors P, (if l ^ 2 ≤ y then g l *  (S⁻¹) ^ 2 else 0))
State after:
s : SelbergSieve
⊢ ∑ l ∈ P.divisors, 1 / g l * (∑ d ∈ P.divisors, if l ∣ d then ν d * s.selbergWeights d else 0) ^ 2 =
    ∑ l ∈ P.divisors, if ↑l ^ 2 ≤ y then g l * S⁻¹ ^ 2 else 0

s : SelbergSieve
⊢ (∑ l ∈ P.divisors, if ↑l ^ 2 ≤ y then g l * S⁻¹ ^ 2 else 0) = S⁻¹

State before:
s : SelbergSieve
⊢ (∑ l ∈ P.divisors, if ↑l ^ 2 ≤ y then g l * S⁻¹ ^ 2 else 0) = S⁻¹
Tactic:
conv => {lhs; congr; {skip}; {ext i; rw [← ite_zero_mul]}}
State after:
s : SelbergSieve
⊢ ∑ i ∈ P.divisors, (if ↑i ^ 2 ≤ y then g i else 0) * S⁻¹ ^ 2 = S⁻¹

State before:
s : SelbergSieve
⊢ ∑ i ∈ P.divisors, (if ↑i ^ 2 ≤ y then g i else 0) * S⁻¹ ^ 2 = S⁻¹
Tactic:
dsimp only [selbergBoundingSum]
State after:
s : SelbergSieve
⊢ ∑ i ∈ P.divisors, (if ↑i ^ 2 ≤ y then g i else 0) * (∑ l ∈ P.divisors, if ↑l ^ 2 ≤ y then g l else 0)⁻¹ ^ 2 =
    (∑ l ∈ P.divisors, if ↑l ^ 2 ≤ y then g l else 0)⁻¹

State before:
s : SelbergSieve
⊢ ∑ i ∈ P.divisors, (if ↑i ^ 2 ≤ y then g i else 0) * (∑ l ∈ P.divisors, if ↑l ^ 2 ≤ y then g l else 0)⁻¹ ^ 2 =
    (∑ l ∈ P.divisors, if ↑l ^ 2 ≤ y then g l else 0)⁻¹
Tactic:
rw [←sum_mul, sq, ←mul_assoc, mul_inv_cancel]
State after:
s : SelbergSieve
⊢ 1 * (∑ l ∈ P.divisors, if ↑l ^ 2 ≤ y then g l else 0)⁻¹ = (∑ l ∈ P.divisors, if ↑l ^ 2 ≤ y then g l else 0)⁻¹

s : SelbergSieve
⊢ (∑ i ∈ P.divisors, if ↑i ^ 2 ≤ y then g i else 0) ≠ 0

State before:
s : SelbergSieve
⊢ 1 * (∑ l ∈ P.divisors, if ↑l ^ 2 ≤ y then g l else 0)⁻¹ = (∑ l ∈ P.divisors, if ↑l ^ 2 ≤ y then g l else 0)⁻¹

s : SelbergSieve
⊢ (∑ i ∈ P.divisors, if ↑i ^ 2 ≤ y then g i else 0) ≠ 0
Tactic:
ring
State after:
s : SelbergSieve
⊢ (∑ i ∈ P.divisors, if ↑i ^ 2 ≤ y then g i else 0) ≠ 0

State before:
s : SelbergSieve
⊢ (∑ i ∈ P.divisors, if ↑i ^ 2 ≤ y then g i else 0) ≠ 0
Tactic:
apply _root_.ne_of_gt
State after:
case h
s : SelbergSieve
⊢ 0 < ∑ i ∈ P.divisors, if ↑i ^ 2 ≤ y then g i else 0

State before:
case h
s : SelbergSieve
⊢ 0 < ∑ i ∈ P.divisors, if ↑i ^ 2 ≤ y then g i else 0
Tactic:
apply selbergBoundingSum_pos
State after:
no goals

State before:
s : SelbergSieve
⊢ ∑ l ∈ P.divisors, 1 / g l * (∑ d ∈ P.divisors, if l ∣ d then ν d * s.selbergWeights d else 0) ^ 2 =
    ∑ l ∈ P.divisors, if ↑l ^ 2 ≤ y then g l * S⁻¹ ^ 2 else 0
Tactic:
apply sum_congr rfl
State after:
s : SelbergSieve
⊢ ∀ x ∈ P.divisors,
    1 / g x * (∑ d ∈ P.divisors, if x ∣ d then ν d * s.selbergWeights d else 0) ^ 2 =
      if ↑x ^ 2 ≤ y then g x * S⁻¹ ^ 2 else 0

State before:
s : SelbergSieve
⊢ ∀ x ∈ P.divisors,
    1 / g x * (∑ d ∈ P.divisors, if x ∣ d then ν d * s.selbergWeights d else 0) ^ 2 =
      if ↑x ^ 2 ≤ y then g x * S⁻¹ ^ 2 else 0
Tactic:
intro l hl
State after:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ 1 / g l * (∑ d ∈ P.divisors, if l ∣ d then ν d * s.selbergWeights d else 0) ^ 2 =
    if ↑l ^ 2 ≤ y then g l * S⁻¹ ^ 2 else 0

State before:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ 1 / g l * (∑ d ∈ P.divisors, if l ∣ d then ν d * s.selbergWeights d else 0) ^ 2 =
    if ↑l ^ 2 ≤ y then g l * S⁻¹ ^ 2 else 0
Tactic:
rw [s.selbergWeights_diagonalisation l hl, ite_pow, zero_pow, mul_ite_zero]
State after:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ (if ↑l ^ 2 ≤ y then 1 / g l * (g l * ↑(μ l) * S⁻¹) ^ 2 else 0) = if ↑l ^ 2 ≤ y then g l * S⁻¹ ^ 2 else 0

s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ 2 ≠ 0

State before:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ (if ↑l ^ 2 ≤ y then 1 / g l * (g l * ↑(μ l) * S⁻¹) ^ 2 else 0) = if ↑l ^ 2 ≤ y then g l * S⁻¹ ^ 2 else 0

s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ 2 ≠ 0
Tactic:
apply if_congr Iff.rfl _ rfl
State after:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ 1 / g l * (g l * ↑(μ l) * S⁻¹) ^ 2 = g l * S⁻¹ ^ 2

s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ 2 ≠ 0

State before:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ 1 / g l * (g l * ↑(μ l) * S⁻¹) ^ 2 = g l * S⁻¹ ^ 2

s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ 2 ≠ 0
Tactic:
trans (1/g l * g l * g l * (μ l:ℝ)^2  * (S⁻¹) ^ 2)
State after:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ 1 / g l * (g l * ↑(μ l) * S⁻¹) ^ 2 = 1 / g l * g l * g l * ↑(μ l) ^ 2 * S⁻¹ ^ 2

s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ 1 / g l * g l * g l * ↑(μ l) ^ 2 * S⁻¹ ^ 2 = g l * S⁻¹ ^ 2

s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ 2 ≠ 0

State before:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ 1 / g l * g l * g l * ↑(μ l) ^ 2 * S⁻¹ ^ 2 = g l * S⁻¹ ^ 2

s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ 2 ≠ 0
Tactic:
norm_cast
State after:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ 1 / g l * g l * g l * ↑(μ l ^ 2) * S⁻¹ ^ 2 = g l * S⁻¹ ^ 2

s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ 2 ≠ 0

State before:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ 1 / g l * g l * g l * ↑(μ l ^ 2) * S⁻¹ ^ 2 = g l * S⁻¹ ^ 2

s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ 2 ≠ 0
Tactic:
rw [moebius_sq_eq_one_of_squarefree $ s.squarefree_of_mem_divisors_prodPrimes hl]
State after:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ 1 / g l * g l * g l * ↑1 * S⁻¹ ^ 2 = g l * S⁻¹ ^ 2

s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ 2 ≠ 0

State before:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ 1 / g l * g l * g l * ↑1 * S⁻¹ ^ 2 = g l * S⁻¹ ^ 2

s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ 2 ≠ 0
Tactic:
rw [one_div_mul_cancel $ _root_.ne_of_gt $ s.selbergTerms_pos l $ dvd_of_mem_divisors hl]
State after:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ 1 * g l * ↑1 * S⁻¹ ^ 2 = g l * S⁻¹ ^ 2

s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ 2 ≠ 0

State before:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ 1 * g l * ↑1 * S⁻¹ ^ 2 = g l * S⁻¹ ^ 2

s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ 2 ≠ 0
Tactic:
ring
State after:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ 2 ≠ 0

State before:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ 2 ≠ 0
Tactic:
linarith
State after:
no goals

State before:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ 1 / g l * (g l * ↑(μ l) * S⁻¹) ^ 2 = 1 / g l * g l * g l * ↑(μ l) ^ 2 * S⁻¹ ^ 2
Tactic:
ring
State after:
no goals