internlm/Lean-Github huggingface dataset:
Theorem: SelbergSieve.selbergBoundingSum_ge
Proof state before:
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ S ≠ 0
Tactic:
exact _root_.ne_of_gt $ s.selbergBoundingSum_pos
Proof state after:
no goals
Theorem: SelbergSieve.selberg_bound_weights
Proof state before:
s : SelbergSieve
d : ℕ
⊢ |s.selbergWeights d| ≤ 1
Tactic:
by_cases hdP : d ∣ P
Proof state after:
case pos
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ |s.selbergWeights d| ≤ 1

case neg
s : SelbergSieve
d : ℕ
hdP : ¬d ∣ P
⊢ |s.selbergWeights d| ≤ 1
Theorem: SelbergSieve.selberg_bound_weights
Proof state before:
case pos
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ |s.selbergWeights d| ≤ 1

case neg
s : SelbergSieve
d : ℕ
hdP : ¬d ∣ P
⊢ |s.selbergWeights d| ≤ 1
Tactic:
swap
Proof state after:
case neg
s : SelbergSieve
d : ℕ
hdP : ¬d ∣ P
⊢ |s.selbergWeights d| ≤ 1

case pos
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ |s.selbergWeights d| ≤ 1
Theorem: SelbergSieve.selberg_bound_weights
Proof state before:
case pos
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ |s.selbergWeights d| ≤ 1
Tactic:
have : 1*S ≥ γ d * ↑(μ d) * S := by
  rw[one_mul]
  exact s.selbergBoundingSum_ge hdP
Proof state after:
case pos
s : SelbergSieve
d : ℕ
hdP : d ∣ P
this : 1 * S ≥ s.selbergWeights d * ↑(μ d) * S
⊢ |s.selbergWeights d| ≤ 1
Theorem: SelbergSieve.selberg_bound_weights
Proof state before:
case pos
s : SelbergSieve
d : ℕ
hdP : d ∣ P
this : 1 * S ≥ s.selbergWeights d * ↑(μ d) * S
⊢ |s.selbergWeights d| ≤ 1
Tactic:
replace this : γ d * μ d ≤ 1 := by
  apply le_of_mul_le_mul_of_pos_right this (s.selbergBoundingSum_pos)
Proof state after:
case pos
s : SelbergSieve
d : ℕ
hdP : d ∣ P
this : s.selbergWeights d * ↑(μ d) ≤ 1
⊢ |s.selbergWeights d| ≤ 1
Theorem: SelbergSieve.selberg_bound_weights
Proof state before:
case pos
s : SelbergSieve
d : ℕ
hdP : d ∣ P
this : s.selbergWeights d * ↑(μ d) ≤ 1
⊢ |s.selbergWeights d| ≤ 1
Tactic:
convert this using 1
Proof state after:
case h.e'_3
s : SelbergSieve
d : ℕ
hdP : d ∣ P
this : s.selbergWeights d * ↑(μ d) ≤ 1
⊢ |s.selbergWeights d| = s.selbergWeights d * ↑(μ d)
Theorem: SelbergSieve.selberg_bound_weights
Proof state before:
case h.e'_3
s : SelbergSieve
d : ℕ
hdP : d ∣ P
this : s.selbergWeights d * ↑(μ d) ≤ 1
⊢ |s.selbergWeights d| = s.selbergWeights d * ↑(μ d)
Tactic:
rw [← abs_of_nonneg <| s.selbergWeights_mul_mu_nonneg d hdP,
  abs_mul, ←Int.cast_abs, abs_moebius_eq_one_of_squarefree <|
  (s.prodPrimes_squarefree.squarefree_of_dvd hdP), Int.cast_one, mul_one]
Proof state after:
no goals
Theorem: SelbergSieve.selberg_bound_weights
Proof state before:
case neg
s : SelbergSieve
d : ℕ
hdP : ¬d ∣ P
⊢ |s.selbergWeights d| ≤ 1
Tactic:
rw [s.selbergWeights_eq_zero_of_not_dvd hdP]
Proof state after:
case neg
s : SelbergSieve
d : ℕ
hdP : ¬d ∣ P
⊢ |0| ≤ 1
Theorem: SelbergSieve.selberg_bound_weights
Proof state before:
case neg
s : SelbergSieve
d : ℕ
hdP : ¬d ∣ P
⊢ |0| ≤ 1
Tactic:
simp only [zero_le_one, abs_zero]
Proof state after:
no goals
Theorem: SelbergSieve.selberg_bound_weights
Proof state before:
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ 1 * S ≥ s.selbergWeights d * ↑(μ d) * S
Tactic:
rw[one_mul]
Proof state after:
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ S ≥ s.selbergWeights d * ↑(μ d) * S
Theorem: SelbergSieve.selberg_bound_weights
Proof state before:
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ S ≥ s.selbergWeights d * ↑(μ d) * S
Tactic:
exact s.selbergBoundingSum_ge hdP
Proof state after:
no goals
Theorem: SelbergSieve.selberg_bound_weights
Proof state before:
s : SelbergSieve
d : ℕ
hdP : d ∣ P
this : 1 * S ≥ s.selbergWeights d * ↑(μ d) * S
⊢ s.selbergWeights d * ↑(μ d) ≤ 1
Tactic:
apply le_of_mul_le_mul_of_pos_right this (s.selbergBoundingSum_pos)
Proof state after:
no goals
Theorem: SelbergSieve.selberg_bound_muPlus
Proof 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
Proof 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
Theorem: SelbergSieve.selberg_bound_muPlus
Proof 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]
Proof 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
Theorem: SelbergSieve.selberg_bound_muPlus
Proof 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 := ?_
Proof 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
Theorem: SelbergSieve.selberg_bound_muPlus
Proof 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
Proof state after:
no goals
Theorem: SelbergSieve.selberg_bound_muPlus
Proof 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
Proof state after:
no goals
Theorem: SelbergSieve.selberg_bound_muPlus
Proof 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
Proof 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|
Theorem: SelbergSieve.selberg_bound_muPlus
Proof 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
Proof state after:
no goals
Theorem: SelbergSieve.selberg_bound_muPlus
Proof 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
Proof 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
Theorem: SelbergSieve.selberg_bound_muPlus
Proof 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]
Proof 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
Theorem: SelbergSieve.selberg_bound_muPlus
Proof 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]
Proof 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
Theorem: SelbergSieve.selberg_bound_muPlus
Proof 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
Proof 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
Theorem: SelbergSieve.selberg_bound_muPlus
Proof 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]
Proof 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
Theorem: SelbergSieve.selberg_bound_muPlus
Proof 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)
Proof 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
Theorem: SelbergSieve.selberg_bound_muPlus
Proof 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]
Proof state after:
no goals
Theorem: SelbergSieve.selberg_bound_muPlus
Proof 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']
Proof state after:
no goals
Theorem: SelbergSieve.selberg_bound_muPlus
Proof 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]
Proof state after:
no goals
Theorem: SelbergSieve.selberg_bound_muPlus
Proof 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
Proof 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
Theorem: SelbergSieve.selberg_bound_muPlus
Proof 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]
Proof state after:
no goals
Theorem: SelbergSieve.selberg_bound_simple_errSum
Proof state before:
s : SelbergSieve
⊢ s.errSum μ⁺ ≤ ∑ d ∈ P.divisors, if ↑d ≤ y then 3 ^ ω d * |s.rem d| else 0
Tactic:
dsimp only [errSum]
Proof state after:
s : SelbergSieve
⊢ ∑ d ∈ P.divisors, |s.selbergMuPlus d| * |s.rem d| ≤ ∑ d ∈ P.divisors, if ↑d ≤ y then 3 ^ ω d * |s.rem d| else 0
Theorem: SelbergSieve.selberg_bound_simple_errSum
Proof state before:
s : SelbergSieve
⊢ ∑ d ∈ P.divisors, |s.selbergMuPlus d| * |s.rem d| ≤ ∑ d ∈ P.divisors, if ↑d ≤ y then 3 ^ ω d * |s.rem d| else 0
Tactic:
gcongr with d hd
Proof state after:
case h
s : SelbergSieve
d : ℕ
hd : d ∈ P.divisors
⊢ |s.selbergMuPlus d| * |s.rem d| ≤ if ↑d ≤ y then 3 ^ ω d * |s.rem d| else 0
Theorem: SelbergSieve.selberg_bound_simple_errSum
Proof state before:
case h
s : SelbergSieve
d : ℕ
hd : d ∈ P.divisors
⊢ |s.selbergMuPlus d| * |s.rem d| ≤ if ↑d ≤ y then 3 ^ ω d * |s.rem d| else 0
Tactic:
split_ifs with h
Proof state after:
case pos
s : SelbergSieve
d : ℕ
hd : d ∈ P.divisors
h : ↑d ≤ y
⊢ |s.selbergMuPlus d| * |s.rem d| ≤ 3 ^ ω d * |s.rem d|

case neg
s : SelbergSieve
d : ℕ
hd : d ∈ P.divisors
h : ¬↑d ≤ y
⊢ |s.selbergMuPlus d| * |s.rem d| ≤ 0
Theorem: SelbergSieve.selberg_bound_simple_errSum
Proof state before:
case pos
s : SelbergSieve
d : ℕ
hd : d ∈ P.divisors
h : ↑d ≤ y
⊢ |s.selbergMuPlus d| * |s.rem d| ≤ 3 ^ ω d * |s.rem d|
Tactic:
apply mul_le_mul _ le_rfl (abs_nonneg <| R d) (pow_nonneg _ <| ω d)
Proof state after:
s : SelbergSieve
d : ℕ
hd : d ∈ P.divisors
h : ↑d ≤ y
⊢ |s.selbergMuPlus d| ≤ 3 ^ ω d

s : SelbergSieve
d : ℕ
hd : d ∈ P.divisors
h : ↑d ≤ y
⊢ 0 ≤ 3
Theorem: SelbergSieve.selberg_bound_simple_errSum
Proof state before:
s : SelbergSieve
d : ℕ
hd : d ∈ P.divisors
h : ↑d ≤ y
⊢ |s.selbergMuPlus d| ≤ 3 ^ ω d

s : SelbergSieve
d : ℕ
hd : d ∈ P.divisors
h : ↑d ≤ y
⊢ 0 ≤ 3
Tactic:
apply s.selberg_bound_muPlus d hd
Proof state after:
s : SelbergSieve
d : ℕ
hd : d ∈ P.divisors
h : ↑d ≤ y
⊢ 0 ≤ 3
Theorem: SelbergSieve.selberg_bound_simple_errSum
Proof state before:
s : SelbergSieve
d : ℕ
hd : d ∈ P.divisors
h : ↑d ≤ y
⊢ 0 ≤ 3
Tactic:
linarith
Proof state after:
no goals
Theorem: SelbergSieve.selberg_bound_simple_errSum
Proof state before:
case neg
s : SelbergSieve
d : ℕ
hd : d ∈ P.divisors
h : ¬↑d ≤ y
⊢ |s.selbergMuPlus d| * |s.rem d| ≤ 0
Tactic:
rw [s.selbergμPlus_eq_zero d h, abs_zero, zero_mul]
Proof state after:
no goals
Theorem: SelbergSieve.selberg_bound_simple
Proof state before:
s : SelbergSieve
⊢ s.siftedSum ≤ X / S + ∑ d ∈ P.divisors, if ↑d ≤ y then 3 ^ ω d * |s.rem d| else 0
Tactic:
let μPlus := s.selbergUbSieve
Proof state after:
s : SelbergSieve
μPlus : UpperBoundSieve := s.selbergUbSieve
⊢ s.siftedSum ≤ X / S + ∑ d ∈ P.divisors, if ↑d ≤ y then 3 ^ ω d * |s.rem d| else 0
Theorem: SelbergSieve.selberg_bound_simple
Proof state before:
s : SelbergSieve
μPlus : UpperBoundSieve := s.selbergUbSieve
⊢ s.siftedSum ≤ X / S + ∑ d ∈ P.divisors, if ↑d ≤ y then 3 ^ ω d * |s.rem d| else 0
Tactic:
calc
  s.siftedSum ≤ X * s.mainSum μPlus + s.errSum μPlus := s.siftedSum_le_mainSum_errSum_of_UpperBoundSieve μPlus
  _ ≤ _ := ?_
Proof state after:
s : SelbergSieve
μPlus : UpperBoundSieve := s.selbergUbSieve
⊢ X * s.mainSum μPlus.μPlus + s.errSum μPlus.μPlus ≤ X / S + ∑ d ∈ P.divisors, if ↑d ≤ y then 3 ^ ω d * |s.rem d| else 0
Theorem: SelbergSieve.selberg_bound_simple
Proof state before:
s : SelbergSieve
μPlus : UpperBoundSieve := s.selbergUbSieve
⊢ X * s.mainSum μPlus.μPlus + s.errSum μPlus.μPlus ≤ X / S + ∑ d ∈ P.divisors, if ↑d ≤ y then 3 ^ ω d * |s.rem d| else 0
Tactic:
gcongr
Proof state after:
case h₁
s : SelbergSieve
μPlus : UpperBoundSieve := s.selbergUbSieve
⊢ X * s.mainSum μPlus.μPlus ≤ X / S

case h₂
s : SelbergSieve
μPlus : UpperBoundSieve := s.selbergUbSieve
⊢ s.errSum μPlus.μPlus ≤ ∑ d ∈ P.divisors, if ↑d ≤ y then 3 ^ ω d * |s.rem d| else 0
Theorem: SelbergSieve.selberg_bound_simple
Proof state before:
case h₁
s : SelbergSieve
μPlus : UpperBoundSieve := s.selbergUbSieve
⊢ X * s.mainSum μPlus.μPlus ≤ X / S
Tactic:
erw [s.selberg_bound_simple_mainSum, div_eq_mul_inv]
Proof state after:
no goals
Theorem: SelbergSieve.selberg_bound_simple
Proof state before:
case h₂
s : SelbergSieve
μPlus : UpperBoundSieve := s.selbergUbSieve
⊢ s.errSum μPlus.μPlus ≤ ∑ d ∈ P.divisors, if ↑d ≤ y then 3 ^ ω d * |s.rem d| else 0
Tactic:
apply s.selberg_bound_simple_errSum
Proof state after:
no goals
Theorem: zeroTendstoDiff
Proof state before:
L₁ L₂ : ℂ
f : ℝ → ℂ
h : ∀ᶠ (T : ℝ) in atTop, f T = 0
h' : Tendsto f atTop (𝓝 (L₂ - L₁))
⊢ L₁ = L₂
Tactic:
rw [← zero_add L₁, ← @eq_sub_iff_add_eq]
Proof state after:
L₁ L₂ : ℂ
f : ℝ → ℂ
h : ∀ᶠ (T : ℝ) in atTop, f T = 0
h' : Tendsto f atTop (𝓝 (L₂ - L₁))
⊢ 0 = L₂ - L₁
Theorem: zeroTendstoDiff
Proof state before:
L₁ L₂ : ℂ
f : ℝ → ℂ
h : ∀ᶠ (T : ℝ) in atTop, f T = 0
h' : Tendsto f atTop (𝓝 (L₂ - L₁))
⊢ 0 = L₂ - L₁
Tactic:
exact tendsto_nhds_unique (EventuallyEq.tendsto h) h'
Proof state after:
no goals
Theorem: RectangleIntegral_tendsTo_VerticalIntegral
Proof state before:
σ σ' : ℝ
f : ℂ → ℂ
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
htop : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atTop (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
⊢ Tendsto (fun T => RectangleIntegral f (↑σ - I * ↑T) (↑σ' + I * ↑T)) atTop
    (𝓝 (VerticalIntegral f σ' - VerticalIntegral f σ))
Tactic:
simp only [RectangleIntegral, sub_re, ofReal_re, mul_re, I_re, zero_mul, I_im, ofReal_im,
  mul_zero, sub_self, sub_zero, add_re, add_zero, sub_im, mul_im, one_mul, zero_add, zero_sub,
  add_im]
Proof state after:
σ σ' : ℝ
f : ℂ → ℂ
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
htop : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atTop (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
⊢ Tendsto (fun T => HIntegral f σ σ' (-T) - HIntegral f σ σ' T + VIntegral f σ' (-T) T - VIntegral f σ (-T) T) atTop
    (𝓝 (VerticalIntegral f σ' - VerticalIntegral f σ))
Theorem: RectangleIntegral_tendsTo_VerticalIntegral
Proof state before:
σ σ' : ℝ
f : ℂ → ℂ
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
htop : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atTop (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
⊢ Tendsto (fun T => HIntegral f σ σ' (-T) - HIntegral f σ σ' T + VIntegral f σ' (-T) T - VIntegral f σ (-T) T) atTop
    (𝓝 (VerticalIntegral f σ' - VerticalIntegral f σ))
Tactic:
apply Tendsto.sub
Proof state after:
case hf
σ σ' : ℝ
f : ℂ → ℂ
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
htop : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atTop (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
⊢ Tendsto (fun x => HIntegral f σ σ' (-x) - HIntegral f σ σ' x + VIntegral f σ' (-x) x) atTop
    (𝓝 (VerticalIntegral f σ'))

case hg
σ σ' : ℝ
f : ℂ → ℂ
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
htop : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atTop (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
⊢ Tendsto (fun x => VIntegral f σ (-x) x) atTop (𝓝 (VerticalIntegral f σ))