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

State before:
s : SelbergSieve
n : ℕ
hn : n ∈ P.divisors
⊢ |s.selbergMuPlus n| ≤ 3 ^ ω n
Tactic:
let f : ℕ → ℕ → ℝ := fun x z : ℕ => if n = x.lcm z then 1 else 0
State after:
s : SelbergSieve
n : ℕ
hn : n ∈ P.divisors
f : ℕ → ℕ → ℝ := fun x z => if n = x.lcm z then 1 else 0
⊢ |s.selbergMuPlus n| ≤ 3 ^ ω n

State before:
s : SelbergSieve
n : ℕ
hn : n ∈ P.divisors
f : ℕ → ℕ → ℝ := fun x z => if n = x.lcm z then 1 else 0
⊢ |s.selbergMuPlus n| ≤ 3 ^ ω n
Tactic:
dsimp only [selbergMuPlus, lambdaSquared]
State after:
s : SelbergSieve
n : ℕ
hn : n ∈ P.divisors
f : ℕ → ℕ → ℝ := fun x z => if n = x.lcm z then 1 else 0
⊢ |∑ d1 ∈ n.divisors, ∑ d2 ∈ n.divisors, if n = d1.lcm d2 then s.selbergWeights d1 * s.selbergWeights d2 else 0| ≤
    3 ^ ω n

State before:
s : SelbergSieve
n : ℕ
hn : n ∈ P.divisors
f : ℕ → ℕ → ℝ := fun x z => if n = x.lcm z then 1 else 0
⊢ |∑ d1 ∈ n.divisors, ∑ d2 ∈ n.divisors, if n = d1.lcm d2 then s.selbergWeights d1 * s.selbergWeights d2 else 0| ≤
    3 ^ ω n
Tactic:
calc
  |∑ d1 in n.divisors, ∑ d2 in n.divisors, if n = d1.lcm d2 then γ d1 * γ d2 else 0| ≤
      ∑ d1 in n.divisors, |∑ d2 in n.divisors, if n = d1.lcm d2 then γ d1 * γ d2 else 0| := ?_
  _ ≤ ∑ d1 in n.divisors, ∑ d2 in n.divisors, |if n = d1.lcm d2 then γ d1 * γ d2 else 0| := ?_
  _ ≤ ∑ d1 in n.divisors, ∑ d2 in n.divisors, f d1 d2 := ?_
  _ = (n.divisors ×ˢ n.divisors).sum fun p => f p.fst p.snd := ?_
  _ = Finset.card ((n.divisors ×ˢ n.divisors).filter fun p : ℕ × ℕ => n = p.fst.lcm p.snd) := ?_
  _ = (3:ℕ) ^ ω n := ?_
  _ = (3:ℝ) ^ ω n := ?_
State after:
case calc_1
s : SelbergSieve
n : ℕ
hn : n ∈ P.divisors
f : ℕ → ℕ → ℝ := fun x z => if n = x.lcm z then 1 else 0
⊢ |∑ d1 ∈ n.divisors, ∑ d2 ∈ n.divisors, if n = d1.lcm d2 then s.selbergWeights d1 * s.selbergWeights d2 else 0| ≤
    ∑ d1 ∈ n.divisors, |∑ d2 ∈ n.divisors, if n = d1.lcm d2 then s.selbergWeights d1 * s.selbergWeights d2 else 0|

case calc_2
s : SelbergSieve
n : ℕ
hn : n ∈ P.divisors
f : ℕ → ℕ → ℝ := fun x z => if n = x.lcm z then 1 else 0
⊢ ∑ d1 ∈ n.divisors, |∑ d2 ∈ n.divisors, if n = d1.lcm d2 then s.selbergWeights d1 * s.selbergWeights d2 else 0| ≤
    ∑ d1 ∈ n.divisors, ∑ d2 ∈ n.divisors, |if n = d1.lcm d2 then s.selbergWeights d1 * s.selbergWeights d2 else 0|

case calc_3
s : SelbergSieve
n : ℕ
hn : n ∈ P.divisors
f : ℕ → ℕ → ℝ := fun x z => if n = x.lcm z then 1 else 0
⊢ ∑ d1 ∈ n.divisors, ∑ d2 ∈ n.divisors, |if n = d1.lcm d2 then s.selbergWeights d1 * s.selbergWeights d2 else 0| ≤
    ∑ d1 ∈ n.divisors, ∑ d2 ∈ n.divisors, f d1 d2

case calc_4
s : SelbergSieve
n : ℕ
hn : n ∈ P.divisors
f : ℕ → ℕ → ℝ := fun x z => if n = x.lcm z then 1 else 0
⊢ ∑ d1 ∈ n.divisors, ∑ d2 ∈ n.divisors, f d1 d2 = ∑ p ∈ n.divisors ×ˢ n.divisors, f p.1 p.2

case calc_5
s : SelbergSieve
n : ℕ
hn : n ∈ P.divisors
f : ℕ → ℕ → ℝ := fun x z => if n = x.lcm z then 1 else 0
⊢ ∑ p ∈ n.divisors ×ˢ n.divisors, f p.1 p.2 = ↑(filter (fun p => n = p.1.lcm p.2) (n.divisors ×ˢ n.divisors)).card

case calc_6
s : SelbergSieve
n : ℕ
hn : n ∈ P.divisors
f : ℕ → ℕ → ℝ := fun x z => if n = x.lcm z then 1 else 0
⊢ ↑(filter (fun p => n = p.1.lcm p.2) (n.divisors ×ˢ n.divisors)).card = ↑3 ^ ω n

case calc_7
s : SelbergSieve
n : ℕ
hn : n ∈ P.divisors
f : ℕ → ℕ → ℝ := fun x z => if n = x.lcm z then 1 else 0
⊢ ↑3 ^ ω n = 3 ^ ω n

State before:
case calc_7
s : SelbergSieve
n : ℕ
hn : n ∈ P.divisors
f : ℕ → ℕ → ℝ := fun x z => if n = x.lcm z then 1 else 0
⊢ ↑3 ^ ω n = 3 ^ ω n
Tactic:
norm_num
State after:
no goals

State before:
case calc_1
s : SelbergSieve
n : ℕ
hn : n ∈ P.divisors
f : ℕ → ℕ → ℝ := fun x z => if n = x.lcm z then 1 else 0
⊢ |∑ d1 ∈ n.divisors, ∑ d2 ∈ n.divisors, if n = d1.lcm d2 then s.selbergWeights d1 * s.selbergWeights d2 else 0| ≤
    ∑ d1 ∈ n.divisors, |∑ d2 ∈ n.divisors, if n = d1.lcm d2 then s.selbergWeights d1 * s.selbergWeights d2 else 0|
Tactic:
apply abs_sum_le_sum_abs
State after:
no goals

State before:
case calc_2
s : SelbergSieve
n : ℕ
hn : n ∈ P.divisors
f : ℕ → ℕ → ℝ := fun x z => if n = x.lcm z then 1 else 0
⊢ ∑ d1 ∈ n.divisors, |∑ d2 ∈ n.divisors, if n = d1.lcm d2 then s.selbergWeights d1 * s.selbergWeights d2 else 0| ≤
    ∑ d1 ∈ n.divisors, ∑ d2 ∈ n.divisors, |if n = d1.lcm d2 then s.selbergWeights d1 * s.selbergWeights d2 else 0|
Tactic:
gcongr
State after:
case calc_2.h
s : SelbergSieve
n : ℕ
hn : n ∈ P.divisors
f : ℕ → ℕ → ℝ := fun x z => if n = x.lcm z then 1 else 0
i✝ : ℕ
a✝ : i✝ ∈ n.divisors
⊢ |∑ d2 ∈ n.divisors, if n = i✝.lcm d2 then s.selbergWeights i✝ * s.selbergWeights d2 else 0| ≤
    ∑ d2 ∈ n.divisors, |if n = i✝.lcm d2 then s.selbergWeights i✝ * s.selbergWeights d2 else 0|

State before:
case calc_2.h
s : SelbergSieve
n : ℕ
hn : n ∈ P.divisors
f : ℕ → ℕ → ℝ := fun x z => if n = x.lcm z then 1 else 0
i✝ : ℕ
a✝ : i✝ ∈ n.divisors
⊢ |∑ d2 ∈ n.divisors, if n = i✝.lcm d2 then s.selbergWeights i✝ * s.selbergWeights d2 else 0| ≤
    ∑ d2 ∈ n.divisors, |if n = i✝.lcm d2 then s.selbergWeights i✝ * s.selbergWeights d2 else 0|
Tactic:
apply abs_sum_le_sum_abs
State after:
no goals

State before:
case calc_3
s : SelbergSieve
n : ℕ
hn : n ∈ P.divisors
f : ℕ → ℕ → ℝ := fun x z => if n = x.lcm z then 1 else 0
⊢ ∑ d1 ∈ n.divisors, ∑ d2 ∈ n.divisors, |if n = d1.lcm d2 then s.selbergWeights d1 * s.selbergWeights d2 else 0| ≤
    ∑ d1 ∈ n.divisors, ∑ d2 ∈ n.divisors, f d1 d2
Tactic:
gcongr with d1 _ d2
State after:
case calc_3.h.h
s : SelbergSieve
n : ℕ
hn : n ∈ P.divisors
f : ℕ → ℕ → ℝ := fun x z => if n = x.lcm z then 1 else 0
d1 : ℕ
a✝¹ : d1 ∈ n.divisors
d2 : ℕ
a✝ : d2 ∈ n.divisors
⊢ |if n = d1.lcm d2 then s.selbergWeights d1 * s.selbergWeights d2 else 0| ≤ f d1 d2

State before:
case calc_3.h.h
s : SelbergSieve
n : ℕ
hn : n ∈ P.divisors
f : ℕ → ℕ → ℝ := fun x z => if n = x.lcm z then 1 else 0
d1 : ℕ
a✝¹ : d1 ∈ n.divisors
d2 : ℕ
a✝ : d2 ∈ n.divisors
⊢ |if n = d1.lcm d2 then s.selbergWeights d1 * s.selbergWeights d2 else 0| ≤ f d1 d2
Tactic:
rw [apply_ite abs, abs_zero, abs_mul]
State after:
case calc_3.h.h
s : SelbergSieve
n : ℕ
hn : n ∈ P.divisors
f : ℕ → ℕ → ℝ := fun x z => if n = x.lcm z then 1 else 0
d1 : ℕ
a✝¹ : d1 ∈ n.divisors
d2 : ℕ
a✝ : d2 ∈ n.divisors
⊢ (if n = d1.lcm d2 then |s.selbergWeights d1| * |s.selbergWeights d2| else 0) ≤ f d1 d2

State before:
case calc_3.h.h
s : SelbergSieve
n : ℕ
hn : n ∈ P.divisors
f : ℕ → ℕ → ℝ := fun x z => if n = x.lcm z then 1 else 0
d1 : ℕ
a✝¹ : d1 ∈ n.divisors
d2 : ℕ
a✝ : d2 ∈ n.divisors
⊢ (if n = d1.lcm d2 then |s.selbergWeights d1| * |s.selbergWeights d2| else 0) ≤ f d1 d2
Tactic:
simp only [f]
State after:
case calc_3.h.h
s : SelbergSieve
n : ℕ
hn : n ∈ P.divisors
f : ℕ → ℕ → ℝ := fun x z => if n = x.lcm z then 1 else 0
d1 : ℕ
a✝¹ : d1 ∈ n.divisors
d2 : ℕ
a✝ : d2 ∈ n.divisors
⊢ (if n = d1.lcm d2 then |s.selbergWeights d1| * |s.selbergWeights d2| else 0) ≤ if n = d1.lcm d2 then 1 else 0

State before:
case calc_3.h.h
s : SelbergSieve
n : ℕ
hn : n ∈ P.divisors
f : ℕ → ℕ → ℝ := fun x z => if n = x.lcm z then 1 else 0
d1 : ℕ
a✝¹ : d1 ∈ n.divisors
d2 : ℕ
a✝ : d2 ∈ n.divisors
⊢ (if n = d1.lcm d2 then |s.selbergWeights d1| * |s.selbergWeights d2| else 0) ≤ if n = d1.lcm d2 then 1 else 0
Tactic:
by_cases h : n = d1.lcm d2
State after:
case pos
s : SelbergSieve
n : ℕ
hn : n ∈ P.divisors
f : ℕ → ℕ → ℝ := fun x z => if n = x.lcm z then 1 else 0
d1 : ℕ
a✝¹ : d1 ∈ n.divisors
d2 : ℕ
a✝ : d2 ∈ n.divisors
h : n = d1.lcm d2
⊢ (if n = d1.lcm d2 then |s.selbergWeights d1| * |s.selbergWeights d2| else 0) ≤ if n = d1.lcm d2 then 1 else 0

case neg
s : SelbergSieve
n : ℕ
hn : n ∈ P.divisors
f : ℕ → ℕ → ℝ := fun x z => if n = x.lcm z then 1 else 0
d1 : ℕ
a✝¹ : d1 ∈ n.divisors
d2 : ℕ
a✝ : d2 ∈ n.divisors
h : ¬n = d1.lcm d2
⊢ (if n = d1.lcm d2 then |s.selbergWeights d1| * |s.selbergWeights d2| else 0) ≤ if n = d1.lcm d2 then 1 else 0

State before:
case pos
s : SelbergSieve
n : ℕ
hn : n ∈ P.divisors
f : ℕ → ℕ → ℝ := fun x z => if n = x.lcm z then 1 else 0
d1 : ℕ
a✝¹ : d1 ∈ n.divisors
d2 : ℕ
a✝ : d2 ∈ n.divisors
h : n = d1.lcm d2
⊢ (if n = d1.lcm d2 then |s.selbergWeights d1| * |s.selbergWeights d2| else 0) ≤ if n = d1.lcm d2 then 1 else 0

case neg
s : SelbergSieve
n : ℕ
hn : n ∈ P.divisors
f : ℕ → ℕ → ℝ := fun x z => if n = x.lcm z then 1 else 0
d1 : ℕ
a✝¹ : d1 ∈ n.divisors
d2 : ℕ
a✝ : d2 ∈ n.divisors
h : ¬n = d1.lcm d2
⊢ (if n = d1.lcm d2 then |s.selbergWeights d1| * |s.selbergWeights d2| else 0) ≤ if n = d1.lcm d2 then 1 else 0
Tactic:
rw [if_pos h, if_pos h]
State after:
case pos
s : SelbergSieve
n : ℕ
hn : n ∈ P.divisors
f : ℕ → ℕ → ℝ := fun x z => if n = x.lcm z then 1 else 0
d1 : ℕ
a✝¹ : d1 ∈ n.divisors
d2 : ℕ
a✝ : d2 ∈ n.divisors
h : n = d1.lcm d2
⊢ |s.selbergWeights d1| * |s.selbergWeights d2| ≤ 1

case neg
s : SelbergSieve
n : ℕ
hn : n ∈ P.divisors
f : ℕ → ℕ → ℝ := fun x z => if n = x.lcm z then 1 else 0
d1 : ℕ
a✝¹ : d1 ∈ n.divisors
d2 : ℕ
a✝ : d2 ∈ n.divisors
h : ¬n = d1.lcm d2
⊢ (if n = d1.lcm d2 then |s.selbergWeights d1| * |s.selbergWeights d2| else 0) ≤ if n = d1.lcm d2 then 1 else 0

State before:
case pos
s : SelbergSieve
n : ℕ
hn : n ∈ P.divisors
f : ℕ → ℕ → ℝ := fun x z => if n = x.lcm z then 1 else 0
d1 : ℕ
a✝¹ : d1 ∈ n.divisors
d2 : ℕ
a✝ : d2 ∈ n.divisors
h : n = d1.lcm d2
⊢ |s.selbergWeights d1| * |s.selbergWeights d2| ≤ 1

case neg
s : SelbergSieve
n : ℕ
hn : n ∈ P.divisors
f : ℕ → ℕ → ℝ := fun x z => if n = x.lcm z then 1 else 0
d1 : ℕ
a✝¹ : d1 ∈ n.divisors
d2 : ℕ
a✝ : d2 ∈ n.divisors
h : ¬n = d1.lcm d2
⊢ (if n = d1.lcm d2 then |s.selbergWeights d1| * |s.selbergWeights d2| else 0) ≤ if n = d1.lcm d2 then 1 else 0
Tactic:
apply mul_le_one (s.selberg_bound_weights d1) (abs_nonneg <| γ d2)
  (s.selberg_bound_weights d2)
State after:
case neg
s : SelbergSieve
n : ℕ
hn : n ∈ P.divisors
f : ℕ → ℕ → ℝ := fun x z => if n = x.lcm z then 1 else 0
d1 : ℕ
a✝¹ : d1 ∈ n.divisors
d2 : ℕ
a✝ : d2 ∈ n.divisors
h : ¬n = d1.lcm d2
⊢ (if n = d1.lcm d2 then |s.selbergWeights d1| * |s.selbergWeights d2| else 0) ≤ if n = d1.lcm d2 then 1 else 0

State before:
case neg
s : SelbergSieve
n : ℕ
hn : n ∈ P.divisors
f : ℕ → ℕ → ℝ := fun x z => if n = x.lcm z then 1 else 0
d1 : ℕ
a✝¹ : d1 ∈ n.divisors
d2 : ℕ
a✝ : d2 ∈ n.divisors
h : ¬n = d1.lcm d2
⊢ (if n = d1.lcm d2 then |s.selbergWeights d1| * |s.selbergWeights d2| else 0) ≤ if n = d1.lcm d2 then 1 else 0
Tactic:
rw [if_neg h, if_neg h]
State after:
no goals

State before:
case calc_4
s : SelbergSieve
n : ℕ
hn : n ∈ P.divisors
f : ℕ → ℕ → ℝ := fun x z => if n = x.lcm z then 1 else 0
⊢ ∑ d1 ∈ n.divisors, ∑ d2 ∈ n.divisors, f d1 d2 = ∑ p ∈ n.divisors ×ˢ n.divisors, f p.1 p.2
Tactic:
rw [← Finset.sum_product']
State after:
no goals

State before:
case calc_5
s : SelbergSieve
n : ℕ
hn : n ∈ P.divisors
f : ℕ → ℕ → ℝ := fun x z => if n = x.lcm z then 1 else 0
⊢ ∑ p ∈ n.divisors ×ˢ n.divisors, f p.1 p.2 = ↑(filter (fun p => n = p.1.lcm p.2) (n.divisors ×ˢ n.divisors)).card
Tactic:
rw [← sum_filter, Finset.sum_const, smul_one_eq_cast]
State after:
no goals

State before:
case calc_6
s : SelbergSieve
n : ℕ
hn : n ∈ P.divisors
f : ℕ → ℕ → ℝ := fun x z => if n = x.lcm z then 1 else 0
⊢ ↑(filter (fun p => n = p.1.lcm p.2) (n.divisors ×ˢ n.divisors)).card = ↑3 ^ ω n
Tactic:
norm_cast
State after:
case calc_6
s : SelbergSieve
n : ℕ
hn : n ∈ P.divisors
f : ℕ → ℕ → ℝ := fun x z => if n = x.lcm z then 1 else 0
⊢ (filter (fun p => n = p.1.lcm p.2) (n.divisors ×ˢ n.divisors)).card = 3 ^ ω n

State before:
case calc_6
s : SelbergSieve
n : ℕ
hn : n ∈ P.divisors
f : ℕ → ℕ → ℝ := fun x z => if n = x.lcm z then 1 else 0
⊢ (filter (fun p => n = p.1.lcm p.2) (n.divisors ×ˢ n.divisors)).card = 3 ^ ω n
Tactic:
simp [← card_lcm_eq (s.squarefree_of_mem_divisors_prodPrimes hn), eq_comm]
State after:
no goals