internlm/Lean-Github huggingface dataset:
Theorem: ArithmeticFunction.sum_range_mul_zeta
Proof state before:
case a
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N y : ℕ
x✝ : y ∈ range (N + 1)
a : ℕ
⊢ a ∈ filter (fun x => x ≠ 0) (range (N + 1)) ↔ a ∈ Ioc 0 N
Tactic:
rw [mem_filter, mem_Ioc, mem_range, pos_iff_ne_zero, lt_succ, and_comm]
Proof state after:
no goals
Theorem: ArithmeticFunction.sum_Icc_mul_zeta
Proof state before:
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N : ℕ
⊢ ∑ d ∈ Icc 1 N, (f * ↑ζ) d = ∑ d ∈ Icc 1 N, (N / d) • f d
Tactic:
have := sum_range_mul_zeta f N
Proof state after:
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N : ℕ
this : ∑ d ∈ range (N + 1), (f * ↑ζ) d = ∑ d ∈ range (N + 1), (N / d) • f d
⊢ ∑ d ∈ Icc 1 N, (f * ↑ζ) d = ∑ d ∈ Icc 1 N, (N / d) • f d
Theorem: ArithmeticFunction.sum_Icc_mul_zeta
Proof state before:
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N : ℕ
this : ∑ d ∈ range (N + 1), (f * ↑ζ) d = ∑ d ∈ range (N + 1), (N / d) • f d
⊢ ∑ d ∈ Icc 1 N, (f * ↑ζ) d = ∑ d ∈ Icc 1 N, (N / d) • f d
Tactic:
rw [range_eq_Ico, ← Ico_insert_succ_left, sum_insert, sum_insert] at this
Proof state after:
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N : ℕ
this : (f * ↑ζ) 0 + ∑ x ∈ Ico (succ 0) (N + 1), (f * ↑ζ) x = (N / 0) • f 0 + ∑ x ∈ Ico (succ 0) (N + 1), (N / x) • f x
⊢ ∑ d ∈ Icc 1 N, (f * ↑ζ) d = ∑ d ∈ Icc 1 N, (N / d) • f d

R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N : ℕ
this : (f * ↑ζ) 0 + ∑ x ∈ Ico (succ 0) (N + 1), (f * ↑ζ) x = ∑ d ∈ insert 0 (Ico (succ 0) (N + 1)), (N / d) • f d
⊢ 0 ∉ Ico (succ 0) (N + 1)

R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N : ℕ
this : ∑ d ∈ insert 0 (Ico (succ 0) (N + 1)), (f * ↑ζ) d = ∑ d ∈ insert 0 (Ico (succ 0) (N + 1)), (N / d) • f d
⊢ 0 ∉ Ico (succ 0) (N + 1)

R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N : ℕ
this : ∑ d ∈ Ico 0 (N + 1), (f * ↑ζ) d = ∑ d ∈ Ico 0 (N + 1), (N / d) • f d
⊢ 0 < N + 1
Theorem: ArithmeticFunction.sum_Icc_mul_zeta
Proof state before:
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N : ℕ
this : (f * ↑ζ) 0 + ∑ x ∈ Ico (succ 0) (N + 1), (f * ↑ζ) x = (N / 0) • f 0 + ∑ x ∈ Ico (succ 0) (N + 1), (N / x) • f x
⊢ ∑ d ∈ Icc 1 N, (f * ↑ζ) d = ∑ d ∈ Icc 1 N, (N / d) • f d

R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N : ℕ
this : (f * ↑ζ) 0 + ∑ x ∈ Ico (succ 0) (N + 1), (f * ↑ζ) x = ∑ d ∈ insert 0 (Ico (succ 0) (N + 1)), (N / d) • f d
⊢ 0 ∉ Ico (succ 0) (N + 1)

R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N : ℕ
this : ∑ d ∈ insert 0 (Ico (succ 0) (N + 1)), (f * ↑ζ) d = ∑ d ∈ insert 0 (Ico (succ 0) (N + 1)), (N / d) • f d
⊢ 0 ∉ Ico (succ 0) (N + 1)

R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N : ℕ
this : ∑ d ∈ Ico 0 (N + 1), (f * ↑ζ) d = ∑ d ∈ Ico 0 (N + 1), (N / d) • f d
⊢ 0 < N + 1
Tactic:
simp only [Ico_succ_right, reduceSucc, Nat.div_zero, smul_zero, map_zero, zero_add] at this
Proof state after:
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N : ℕ
this : ∑ x ∈ Icc 1 N, (f * ↑ζ) x = ∑ x ∈ Icc 1 N, (N / x) • f x
⊢ ∑ d ∈ Icc 1 N, (f * ↑ζ) d = ∑ d ∈ Icc 1 N, (N / d) • f d

R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N : ℕ
this : (f * ↑ζ) 0 + ∑ x ∈ Ico (succ 0) (N + 1), (f * ↑ζ) x = ∑ d ∈ insert 0 (Ico (succ 0) (N + 1)), (N / d) • f d
⊢ 0 ∉ Ico (succ 0) (N + 1)

R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N : ℕ
this : ∑ d ∈ insert 0 (Ico (succ 0) (N + 1)), (f * ↑ζ) d = ∑ d ∈ insert 0 (Ico (succ 0) (N + 1)), (N / d) • f d
⊢ 0 ∉ Ico (succ 0) (N + 1)

R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N : ℕ
this : ∑ d ∈ Ico 0 (N + 1), (f * ↑ζ) d = ∑ d ∈ Ico 0 (N + 1), (N / d) • f d
⊢ 0 < N + 1
Theorem: ArithmeticFunction.sum_Icc_mul_zeta
Proof state before:
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N : ℕ
this : ∑ x ∈ Icc 1 N, (f * ↑ζ) x = ∑ x ∈ Icc 1 N, (N / x) • f x
⊢ ∑ d ∈ Icc 1 N, (f * ↑ζ) d = ∑ d ∈ Icc 1 N, (N / d) • f d

R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N : ℕ
this : (f * ↑ζ) 0 + ∑ x ∈ Ico (succ 0) (N + 1), (f * ↑ζ) x = ∑ d ∈ insert 0 (Ico (succ 0) (N + 1)), (N / d) • f d
⊢ 0 ∉ Ico (succ 0) (N + 1)

R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N : ℕ
this : ∑ d ∈ insert 0 (Ico (succ 0) (N + 1)), (f * ↑ζ) d = ∑ d ∈ insert 0 (Ico (succ 0) (N + 1)), (N / d) • f d
⊢ 0 ∉ Ico (succ 0) (N + 1)

R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N : ℕ
this : ∑ d ∈ Ico 0 (N + 1), (f * ↑ζ) d = ∑ d ∈ Ico 0 (N + 1), (N / d) • f d
⊢ 0 < N + 1
Tactic:
rw [this]
Proof state after:
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N : ℕ
this : (f * ↑ζ) 0 + ∑ x ∈ Ico (succ 0) (N + 1), (f * ↑ζ) x = ∑ d ∈ insert 0 (Ico (succ 0) (N + 1)), (N / d) • f d
⊢ 0 ∉ Ico (succ 0) (N + 1)

R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N : ℕ
this : ∑ d ∈ insert 0 (Ico (succ 0) (N + 1)), (f * ↑ζ) d = ∑ d ∈ insert 0 (Ico (succ 0) (N + 1)), (N / d) • f d
⊢ 0 ∉ Ico (succ 0) (N + 1)

R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N : ℕ
this : ∑ d ∈ Ico 0 (N + 1), (f * ↑ζ) d = ∑ d ∈ Ico 0 (N + 1), (N / d) • f d
⊢ 0 < N + 1
Theorem: ArithmeticFunction.sum_Icc_mul_zeta
Proof state before:
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N : ℕ
this : (f * ↑ζ) 0 + ∑ x ∈ Ico (succ 0) (N + 1), (f * ↑ζ) x = ∑ d ∈ insert 0 (Ico (succ 0) (N + 1)), (N / d) • f d
⊢ 0 ∉ Ico (succ 0) (N + 1)

R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N : ℕ
this : ∑ d ∈ insert 0 (Ico (succ 0) (N + 1)), (f * ↑ζ) d = ∑ d ∈ insert 0 (Ico (succ 0) (N + 1)), (N / d) • f d
⊢ 0 ∉ Ico (succ 0) (N + 1)

R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N : ℕ
this : ∑ d ∈ Ico 0 (N + 1), (f * ↑ζ) d = ∑ d ∈ Ico 0 (N + 1), (N / d) • f d
⊢ 0 < N + 1
Tactic:
all_goals simp
Proof state after:
no goals
Theorem: ArithmeticFunction.sum_Icc_mul_zeta
Proof state before:
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N : ℕ
this : ∑ d ∈ Ico 0 (N + 1), (f * ↑ζ) d = ∑ d ∈ Ico 0 (N + 1), (N / d) • f d
⊢ 0 < N + 1
Tactic:
simp
Proof state after:
no goals
Theorem: SelbergSieve.selbergBoundingSum_pos
Proof state before:
s : SelbergSieve
⊢ 0 < S
Tactic:
dsimp only [selbergBoundingSum]
Proof state after:
s : SelbergSieve
⊢ 0 < ∑ l ∈ P.divisors, if ↑l ^ 2 ≤ y then g l else 0
Theorem: SelbergSieve.selbergBoundingSum_pos
Proof state before:
s : SelbergSieve
⊢ 0 < ∑ l ∈ P.divisors, if ↑l ^ 2 ≤ y then g l else 0
Tactic:
rw [← sum_filter]
Proof state after:
s : SelbergSieve
⊢ 0 < ∑ a ∈ filter (fun l => ↑l ^ 2 ≤ y) P.divisors, g a
Theorem: SelbergSieve.selbergBoundingSum_pos
Proof state before:
s : SelbergSieve
⊢ 0 < ∑ a ∈ filter (fun l => ↑l ^ 2 ≤ y) P.divisors, g a
Tactic:
apply sum_pos
Proof state after:
case h
s : SelbergSieve
⊢ ∀ i ∈ filter (fun l => ↑l ^ 2 ≤ y) P.divisors, 0 < g i

case hs
s : SelbergSieve
⊢ (filter (fun l => ↑l ^ 2 ≤ y) P.divisors).Nonempty
Theorem: SelbergSieve.selbergBoundingSum_pos
Proof state before:
case h
s : SelbergSieve
⊢ ∀ i ∈ filter (fun l => ↑l ^ 2 ≤ y) P.divisors, 0 < g i
Tactic:
intro l hl
Proof state after:
case h
s : SelbergSieve
l : ℕ
hl : l ∈ filter (fun l => ↑l ^ 2 ≤ y) P.divisors
⊢ 0 < g l
Theorem: SelbergSieve.selbergBoundingSum_pos
Proof state before:
case h
s : SelbergSieve
l : ℕ
hl : l ∈ filter (fun l => ↑l ^ 2 ≤ y) P.divisors
⊢ 0 < g l
Tactic:
rw [mem_filter, mem_divisors] at hl
Proof state after:
case h
s : SelbergSieve
l : ℕ
hl : (l ∣ P ∧ P ≠ 0) ∧ ↑l ^ 2 ≤ y
⊢ 0 < g l
Theorem: SelbergSieve.selbergBoundingSum_pos
Proof state before:
case h
s : SelbergSieve
l : ℕ
hl : (l ∣ P ∧ P ≠ 0) ∧ ↑l ^ 2 ≤ y
⊢ 0 < g l
Tactic:
apply s.selbergTerms_pos _ (hl.1.1)
Proof state after:
no goals
Theorem: SelbergSieve.selbergBoundingSum_pos
Proof state before:
case hs
s : SelbergSieve
⊢ (filter (fun l => ↑l ^ 2 ≤ y) P.divisors).Nonempty
Tactic:
simp_rw [Finset.Nonempty, mem_filter]
Proof state after:
case hs
s : SelbergSieve
⊢ ∃ x ∈ P.divisors, ↑x ^ 2 ≤ y
Theorem: SelbergSieve.selbergBoundingSum_pos
Proof state before:
case hs
s : SelbergSieve
⊢ ∃ x ∈ P.divisors, ↑x ^ 2 ≤ y
Tactic:
use 1
Proof state after:
case h
s : SelbergSieve
⊢ 1 ∈ P.divisors ∧ ↑1 ^ 2 ≤ y
Theorem: SelbergSieve.selbergBoundingSum_pos
Proof state before:
case h
s : SelbergSieve
⊢ 1 ∈ P.divisors ∧ ↑1 ^ 2 ≤ y
Tactic:
constructor
Proof state after:
case h.left
s : SelbergSieve
⊢ 1 ∈ P.divisors

case h.right
s : SelbergSieve
⊢ ↑1 ^ 2 ≤ y
Theorem: SelbergSieve.selbergBoundingSum_pos
Proof state before:
case h.right
s : SelbergSieve
⊢ ↑1 ^ 2 ≤ y
Tactic:
rw [cast_one, one_pow]
Proof state after:
case h.right
s : SelbergSieve
⊢ 1 ≤ y
Theorem: SelbergSieve.selbergBoundingSum_pos
Proof state before:
case h.right
s : SelbergSieve
⊢ 1 ≤ y
Tactic:
exact s.one_le_level
Proof state after:
no goals
Theorem: SelbergSieve.selbergBoundingSum_pos
Proof state before:
case h.left
s : SelbergSieve
⊢ 1 ∈ P.divisors
Tactic:
apply one_mem_divisors.mpr s.prodPrimes_ne_zero
Proof state after:
no goals
Theorem: SelbergSieve.selbergBoundingSum_ne_zero
Proof state before:
s : SelbergSieve
⊢ S ≠ 0
Tactic:
apply _root_.ne_of_gt
Proof state after:
case h
s : SelbergSieve
⊢ 0 < S
Theorem: SelbergSieve.selbergBoundingSum_ne_zero
Proof state before:
case h
s : SelbergSieve
⊢ 0 < S
Tactic:
exact s.selbergBoundingSum_pos
Proof state after:
no goals
Theorem: SelbergSieve.selbergWeights_eq_zero_of_not_dvd
Proof state before:
s : SelbergSieve
d : ℕ
hd : ¬d ∣ P
⊢ s.selbergWeights d = 0
Tactic:
rw [selbergWeights, if_neg hd]
Proof state after:
no goals
Theorem: SelbergSieve.selbergWeights_eq_zero
Proof state before:
s : SelbergSieve
d : ℕ
hd : ¬↑d ^ 2 ≤ y
⊢ s.selbergWeights d = 0
Tactic:
dsimp only [selbergWeights]
Proof 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
Theorem: SelbergSieve.selbergWeights_eq_zero
Proof 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
Proof 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
Theorem: SelbergSieve.selbergWeights_eq_zero
Proof 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 _]
Proof 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
Theorem: SelbergSieve.selbergWeights_eq_zero
Proof 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
Proof 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
Theorem: SelbergSieve.selbergWeights_eq_zero
Proof 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 ?_
Proof 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)
Theorem: SelbergSieve.selbergWeights_eq_zero
Proof 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
Proof 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
Theorem: SelbergSieve.selbergWeights_eq_zero
Proof 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)
Proof 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
Theorem: SelbergSieve.selbergWeights_eq_zero
Proof 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]
Proof state after:
no goals
Theorem: SelbergSieve.selbergWeights_eq_zero
Proof 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
Proof 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
Theorem: SelbergSieve.selbergWeights_eq_zero
Proof 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
Proof 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
Theorem: SelbergSieve.selbergWeights_eq_zero
Proof 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)
Proof state after:
no goals
Theorem: SelbergSieve.selbergWeights_eq_zero
Proof state before:
case neg
s : SelbergSieve
d : ℕ
hd : ¬↑d ^ 2 ≤ y
h : ¬d ∣ P
⊢ 0 = 0
Tactic:
rfl
Proof state after:
no goals
Theorem: SelbergSieve.selbergWeights_mul_mu_nonneg
Proof state before:
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ 0 ≤ s.selbergWeights d * ↑(μ d)
Tactic:
dsimp only [selbergWeights]
Proof 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)
Theorem: SelbergSieve.selbergWeights_mul_mu_nonneg
Proof 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]
Proof 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))
Theorem: SelbergSieve.selbergWeights_mul_mu_nonneg
Proof 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)
Proof 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))
Theorem: SelbergSieve.selbergWeights_mul_mu_nonneg
Proof 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
Proof 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
Theorem: SelbergSieve.selbergWeights_mul_mu_nonneg
Proof 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
Proof 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
Theorem: SelbergSieve.selbergWeights_mul_mu_nonneg
Proof 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
Proof 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
Theorem: SelbergSieve.selbergWeights_mul_mu_nonneg
Proof 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
Proof 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
Theorem: SelbergSieve.selbergWeights_mul_mu_nonneg
Proof 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
Proof 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
Theorem: SelbergSieve.selbergWeights_mul_mu_nonneg
Proof 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
Proof 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
Theorem: SelbergSieve.selbergWeights_mul_mu_nonneg
Proof 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
Proof 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
Theorem: SelbergSieve.selbergWeights_mul_mu_nonneg
Proof 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
Proof 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
Theorem: SelbergSieve.selbergWeights_mul_mu_nonneg
Proof 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
Proof 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
Theorem: SelbergSieve.selbergWeights_mul_mu_nonneg
Proof 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
Proof 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
Theorem: SelbergSieve.selbergWeights_mul_mu_nonneg
Proof state before:
case ha.ha.ha.ha
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ 0 ≤ ↑(μ d) ^ 2
Tactic:
apply sq_nonneg
Proof state after:
no goals
Theorem: SelbergSieve.selbergWeights_mul_mu_nonneg
Proof state before:
case ha.ha.ha.hb
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ 0 ≤ (ν d)⁻¹
Tactic:
rw [inv_nonneg]
Proof state after:
case ha.ha.ha.hb
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ 0 ≤ ν d
Theorem: SelbergSieve.selbergWeights_mul_mu_nonneg
Proof 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
Proof state after:
no goals
Theorem: SelbergSieve.selbergWeights_mul_mu_nonneg
Proof 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
Proof state after:
no goals
Theorem: SelbergSieve.selbergWeights_mul_mu_nonneg
Proof state before:
case ha.hb
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ 0 ≤ S
Tactic:
exact s.selbergBoundingSum_nonneg
Proof state after:
no goals
Theorem: SelbergSieve.selbergWeights_mul_mu_nonneg
Proof 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)
Proof state after:
no goals
Theorem: SelbergSieve.selbergWeights_mul_mu_nonneg
Proof 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
Proof state after:
no goals
Theorem: SelbergSieve.sum_mul_subst
Proof state before:
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
⊢ ∑ l ∈ n.divisors, f l = ∑ m ∈ n.divisors, if k * m ∣ n then f (k * m) else 0
Tactic:
by_cases hn: n = 0
Proof state after:
case pos
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : n = 0
⊢ ∑ l ∈ n.divisors, f l = ∑ m ∈ n.divisors, if k * m ∣ n then f (k * m) else 0

case neg
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
⊢ ∑ l ∈ n.divisors, f l = ∑ m ∈ n.divisors, if k * m ∣ n then f (k * m) else 0