internlm/Lean-Github huggingface dataset:
Theorem: Sieve.selbergBoundingSum_ge_sum_div
Proof state before:
case calc_2
s : SelbergSieve
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
hnu : CompletelyMultiplicative s.nu
hnu_nonneg : ∀ (n : ℕ), 0 ≤ s.nu n
hnu_lt : ∀ (p : ℕ), p.Prime → p ∣ s.prodPrimes → s.nu p < 1
i j : ℕ
hij : i ≠ j
t : Finset ℕ
x : ℕ
hx : x ∈ t
hti : (x ∣ i ^ ⌊s.level⌋₊ ∧ i ^ ⌊s.level⌋₊ ≠ 0) ∧ i ∣ x
htj : (x ∣ j ^ ⌊s.level⌋₊ ∧ j ^ ⌊s.level⌋₊ ≠ 0) ∧ j ∣ x
hi : (i ∣ s.prodPrimes ∧ s.prodPrimes ≠ 0) ∧ ↑i ^ 2 ≤ s.level
hj : (j ∣ s.prodPrimes ∧ s.prodPrimes ≠ 0) ∧ ↑j ^ 2 ≤ s.level
h : ∀ (i j : ℕ) {n : ℕ}, i ∣ s.prodPrimes → i ∣ x → x ∣ j ^ n → i ∣ j
⊢ False
Tactic:
have hidvdj : i ∣ j := by
  apply h i j hi.1.1 hti.2 htj.1.1
Proof state after:
case calc_2
s : SelbergSieve
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
hnu : CompletelyMultiplicative s.nu
hnu_nonneg : ∀ (n : ℕ), 0 ≤ s.nu n
hnu_lt : ∀ (p : ℕ), p.Prime → p ∣ s.prodPrimes → s.nu p < 1
i j : ℕ
hij : i ≠ j
t : Finset ℕ
x : ℕ
hx : x ∈ t
hti : (x ∣ i ^ ⌊s.level⌋₊ ∧ i ^ ⌊s.level⌋₊ ≠ 0) ∧ i ∣ x
htj : (x ∣ j ^ ⌊s.level⌋₊ ∧ j ^ ⌊s.level⌋₊ ≠ 0) ∧ j ∣ x
hi : (i ∣ s.prodPrimes ∧ s.prodPrimes ≠ 0) ∧ ↑i ^ 2 ≤ s.level
hj : (j ∣ s.prodPrimes ∧ s.prodPrimes ≠ 0) ∧ ↑j ^ 2 ≤ s.level
h : ∀ (i j : ℕ) {n : ℕ}, i ∣ s.prodPrimes → i ∣ x → x ∣ j ^ n → i ∣ j
hidvdj : i ∣ j
⊢ False
Theorem: Sieve.selbergBoundingSum_ge_sum_div
Proof state before:
case calc_2
s : SelbergSieve
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
hnu : CompletelyMultiplicative s.nu
hnu_nonneg : ∀ (n : ℕ), 0 ≤ s.nu n
hnu_lt : ∀ (p : ℕ), p.Prime → p ∣ s.prodPrimes → s.nu p < 1
i j : ℕ
hij : i ≠ j
t : Finset ℕ
x : ℕ
hx : x ∈ t
hti : (x ∣ i ^ ⌊s.level⌋₊ ∧ i ^ ⌊s.level⌋₊ ≠ 0) ∧ i ∣ x
htj : (x ∣ j ^ ⌊s.level⌋₊ ∧ j ^ ⌊s.level⌋₊ ≠ 0) ∧ j ∣ x
hi : (i ∣ s.prodPrimes ∧ s.prodPrimes ≠ 0) ∧ ↑i ^ 2 ≤ s.level
hj : (j ∣ s.prodPrimes ∧ s.prodPrimes ≠ 0) ∧ ↑j ^ 2 ≤ s.level
h : ∀ (i j : ℕ) {n : ℕ}, i ∣ s.prodPrimes → i ∣ x → x ∣ j ^ n → i ∣ j
hidvdj : i ∣ j
⊢ False
Tactic:
have hjdvdi : j ∣ i := by
  apply h j i hj.1.1 htj.2 hti.1.1
Proof state after:
case calc_2
s : SelbergSieve
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
hnu : CompletelyMultiplicative s.nu
hnu_nonneg : ∀ (n : ℕ), 0 ≤ s.nu n
hnu_lt : ∀ (p : ℕ), p.Prime → p ∣ s.prodPrimes → s.nu p < 1
i j : ℕ
hij : i ≠ j
t : Finset ℕ
x : ℕ
hx : x ∈ t
hti : (x ∣ i ^ ⌊s.level⌋₊ ∧ i ^ ⌊s.level⌋₊ ≠ 0) ∧ i ∣ x
htj : (x ∣ j ^ ⌊s.level⌋₊ ∧ j ^ ⌊s.level⌋₊ ≠ 0) ∧ j ∣ x
hi : (i ∣ s.prodPrimes ∧ s.prodPrimes ≠ 0) ∧ ↑i ^ 2 ≤ s.level
hj : (j ∣ s.prodPrimes ∧ s.prodPrimes ≠ 0) ∧ ↑j ^ 2 ≤ s.level
h : ∀ (i j : ℕ) {n : ℕ}, i ∣ s.prodPrimes → i ∣ x → x ∣ j ^ n → i ∣ j
hidvdj : i ∣ j
hjdvdi : j ∣ i
⊢ False
Theorem: Sieve.selbergBoundingSum_ge_sum_div
Proof state before:
case calc_2
s : SelbergSieve
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
hnu : CompletelyMultiplicative s.nu
hnu_nonneg : ∀ (n : ℕ), 0 ≤ s.nu n
hnu_lt : ∀ (p : ℕ), p.Prime → p ∣ s.prodPrimes → s.nu p < 1
i j : ℕ
hij : i ≠ j
t : Finset ℕ
x : ℕ
hx : x ∈ t
hti : (x ∣ i ^ ⌊s.level⌋₊ ∧ i ^ ⌊s.level⌋₊ ≠ 0) ∧ i ∣ x
htj : (x ∣ j ^ ⌊s.level⌋₊ ∧ j ^ ⌊s.level⌋₊ ≠ 0) ∧ j ∣ x
hi : (i ∣ s.prodPrimes ∧ s.prodPrimes ≠ 0) ∧ ↑i ^ 2 ≤ s.level
hj : (j ∣ s.prodPrimes ∧ s.prodPrimes ≠ 0) ∧ ↑j ^ 2 ≤ s.level
h : ∀ (i j : ℕ) {n : ℕ}, i ∣ s.prodPrimes → i ∣ x → x ∣ j ^ n → i ∣ j
hidvdj : i ∣ j
hjdvdi : j ∣ i
⊢ False
Tactic:
exact hij $ Nat.dvd_antisymm hidvdj hjdvdi
Proof state after:
no goals
Theorem: Sieve.selbergBoundingSum_ge_sum_div
Proof state before:
s : SelbergSieve
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
hnu : CompletelyMultiplicative s.nu
hnu_nonneg : ∀ (n : ℕ), 0 ≤ s.nu n
hnu_lt : ∀ (p : ℕ), p.Prime → p ∣ s.prodPrimes → s.nu p < 1
i j : ℕ
hij : i ≠ j
t : Finset ℕ
x : ℕ
hx : x ∈ t
hti : (x ∣ i ^ ⌊s.level⌋₊ ∧ i ^ ⌊s.level⌋₊ ≠ 0) ∧ i ∣ x
htj : (x ∣ j ^ ⌊s.level⌋₊ ∧ j ^ ⌊s.level⌋₊ ≠ 0) ∧ j ∣ x
hi : (i ∣ s.prodPrimes ∧ s.prodPrimes ≠ 0) ∧ ↑i ^ 2 ≤ s.level
hj : (j ∣ s.prodPrimes ∧ s.prodPrimes ≠ 0) ∧ ↑j ^ 2 ≤ s.level
⊢ ∀ (i j : ℕ) {n : ℕ}, i ∣ s.prodPrimes → i ∣ x → x ∣ j ^ n → i ∣ j
Tactic:
intro i j n hiP hix hij
Proof state after:
s : SelbergSieve
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
hnu : CompletelyMultiplicative s.nu
hnu_nonneg : ∀ (n : ℕ), 0 ≤ s.nu n
hnu_lt : ∀ (p : ℕ), p.Prime → p ∣ s.prodPrimes → s.nu p < 1
i✝ j✝ : ℕ
hij✝ : i✝ ≠ j✝
t : Finset ℕ
x : ℕ
hx : x ∈ t
hti : (x ∣ i✝ ^ ⌊s.level⌋₊ ∧ i✝ ^ ⌊s.level⌋₊ ≠ 0) ∧ i✝ ∣ x
htj : (x ∣ j✝ ^ ⌊s.level⌋₊ ∧ j✝ ^ ⌊s.level⌋₊ ≠ 0) ∧ j✝ ∣ x
hi : (i✝ ∣ s.prodPrimes ∧ s.prodPrimes ≠ 0) ∧ ↑i✝ ^ 2 ≤ s.level
hj : (j✝ ∣ s.prodPrimes ∧ s.prodPrimes ≠ 0) ∧ ↑j✝ ^ 2 ≤ s.level
i j n : ℕ
hiP : i ∣ s.prodPrimes
hix : i ∣ x
hij : x ∣ j ^ n
⊢ i ∣ j
Theorem: Sieve.selbergBoundingSum_ge_sum_div
Proof state before:
s : SelbergSieve
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
hnu : CompletelyMultiplicative s.nu
hnu_nonneg : ∀ (n : ℕ), 0 ≤ s.nu n
hnu_lt : ∀ (p : ℕ), p.Prime → p ∣ s.prodPrimes → s.nu p < 1
i✝ j✝ : ℕ
hij✝ : i✝ ≠ j✝
t : Finset ℕ
x : ℕ
hx : x ∈ t
hti : (x ∣ i✝ ^ ⌊s.level⌋₊ ∧ i✝ ^ ⌊s.level⌋₊ ≠ 0) ∧ i✝ ∣ x
htj : (x ∣ j✝ ^ ⌊s.level⌋₊ ∧ j✝ ^ ⌊s.level⌋₊ ≠ 0) ∧ j✝ ∣ x
hi : (i✝ ∣ s.prodPrimes ∧ s.prodPrimes ≠ 0) ∧ ↑i✝ ^ 2 ≤ s.level
hj : (j✝ ∣ s.prodPrimes ∧ s.prodPrimes ≠ 0) ∧ ↑j✝ ^ 2 ≤ s.level
i j n : ℕ
hiP : i ∣ s.prodPrimes
hix : i ∣ x
hij : x ∣ j ^ n
⊢ i ∣ j
Tactic:
apply Nat.squarefree_dvd_pow i j n (s.squarefree_of_dvd_prodPrimes hiP)
Proof state after:
s : SelbergSieve
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
hnu : CompletelyMultiplicative s.nu
hnu_nonneg : ∀ (n : ℕ), 0 ≤ s.nu n
hnu_lt : ∀ (p : ℕ), p.Prime → p ∣ s.prodPrimes → s.nu p < 1
i✝ j✝ : ℕ
hij✝ : i✝ ≠ j✝
t : Finset ℕ
x : ℕ
hx : x ∈ t
hti : (x ∣ i✝ ^ ⌊s.level⌋₊ ∧ i✝ ^ ⌊s.level⌋₊ ≠ 0) ∧ i✝ ∣ x
htj : (x ∣ j✝ ^ ⌊s.level⌋₊ ∧ j✝ ^ ⌊s.level⌋₊ ≠ 0) ∧ j✝ ∣ x
hi : (i✝ ∣ s.prodPrimes ∧ s.prodPrimes ≠ 0) ∧ ↑i✝ ^ 2 ≤ s.level
hj : (j✝ ∣ s.prodPrimes ∧ s.prodPrimes ≠ 0) ∧ ↑j✝ ^ 2 ≤ s.level
i j n : ℕ
hiP : i ∣ s.prodPrimes
hix : i ∣ x
hij : x ∣ j ^ n
⊢ i ∣ j ^ n
Theorem: Sieve.selbergBoundingSum_ge_sum_div
Proof state before:
s : SelbergSieve
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
hnu : CompletelyMultiplicative s.nu
hnu_nonneg : ∀ (n : ℕ), 0 ≤ s.nu n
hnu_lt : ∀ (p : ℕ), p.Prime → p ∣ s.prodPrimes → s.nu p < 1
i✝ j✝ : ℕ
hij✝ : i✝ ≠ j✝
t : Finset ℕ
x : ℕ
hx : x ∈ t
hti : (x ∣ i✝ ^ ⌊s.level⌋₊ ∧ i✝ ^ ⌊s.level⌋₊ ≠ 0) ∧ i✝ ∣ x
htj : (x ∣ j✝ ^ ⌊s.level⌋₊ ∧ j✝ ^ ⌊s.level⌋₊ ≠ 0) ∧ j✝ ∣ x
hi : (i✝ ∣ s.prodPrimes ∧ s.prodPrimes ≠ 0) ∧ ↑i✝ ^ 2 ≤ s.level
hj : (j✝ ∣ s.prodPrimes ∧ s.prodPrimes ≠ 0) ∧ ↑j✝ ^ 2 ≤ s.level
i j n : ℕ
hiP : i ∣ s.prodPrimes
hix : i ∣ x
hij : x ∣ j ^ n
⊢ i ∣ j ^ n
Tactic:
exact Trans.trans hix hij
Proof state after:
no goals
Theorem: Sieve.selbergBoundingSum_ge_sum_div
Proof state before:
s : SelbergSieve
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
hnu : CompletelyMultiplicative s.nu
hnu_nonneg : ∀ (n : ℕ), 0 ≤ s.nu n
hnu_lt : ∀ (p : ℕ), p.Prime → p ∣ s.prodPrimes → s.nu p < 1
i j : ℕ
hij : i ≠ j
t : Finset ℕ
x : ℕ
hx : x ∈ t
hti : (x ∣ i ^ ⌊s.level⌋₊ ∧ i ^ ⌊s.level⌋₊ ≠ 0) ∧ i ∣ x
htj : (x ∣ j ^ ⌊s.level⌋₊ ∧ j ^ ⌊s.level⌋₊ ≠ 0) ∧ j ∣ x
hi : (i ∣ s.prodPrimes ∧ s.prodPrimes ≠ 0) ∧ ↑i ^ 2 ≤ s.level
hj : (j ∣ s.prodPrimes ∧ s.prodPrimes ≠ 0) ∧ ↑j ^ 2 ≤ s.level
h : ∀ (i j : ℕ) {n : ℕ}, i ∣ s.prodPrimes → i ∣ x → x ∣ j ^ n → i ∣ j
⊢ i ∣ j
Tactic:
apply h i j hi.1.1 hti.2 htj.1.1
Proof state after:
no goals
Theorem: Sieve.selbergBoundingSum_ge_sum_div
Proof state before:
s : SelbergSieve
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
hnu : CompletelyMultiplicative s.nu
hnu_nonneg : ∀ (n : ℕ), 0 ≤ s.nu n
hnu_lt : ∀ (p : ℕ), p.Prime → p ∣ s.prodPrimes → s.nu p < 1
i j : ℕ
hij : i ≠ j
t : Finset ℕ
x : ℕ
hx : x ∈ t
hti : (x ∣ i ^ ⌊s.level⌋₊ ∧ i ^ ⌊s.level⌋₊ ≠ 0) ∧ i ∣ x
htj : (x ∣ j ^ ⌊s.level⌋₊ ∧ j ^ ⌊s.level⌋₊ ≠ 0) ∧ j ∣ x
hi : (i ∣ s.prodPrimes ∧ s.prodPrimes ≠ 0) ∧ ↑i ^ 2 ≤ s.level
hj : (j ∣ s.prodPrimes ∧ s.prodPrimes ≠ 0) ∧ ↑j ^ 2 ≤ s.level
h : ∀ (i j : ℕ) {n : ℕ}, i ∣ s.prodPrimes → i ∣ x → x ∣ j ^ n → i ∣ j
hidvdj : i ∣ j
⊢ j ∣ i
Tactic:
apply h j i hj.1.1 htj.2 hti.1.1
Proof state after:
no goals
Theorem: Sieve.boundingSum_ge_sum
Proof state before:
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ s.selbergBoundingSum ≥ ∑ m ∈ Finset.Icc 1 ⌊√s.level⌋₊, 1 / ↑m
Tactic:
trans ∑ m in Finset.Icc 1 (Nat.floor $ Real.sqrt s.level), (ζ : ArithmeticFunction ℝ).pdiv .id m
Proof state after:
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ s.selbergBoundingSum ≥ ∑ m ∈ Finset.Icc 1 ⌊√s.level⌋₊, ((↑ζ).pdiv ↑ArithmeticFunction.id) m

s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ ∑ m ∈ Finset.Icc 1 ⌊√s.level⌋₊, ((↑ζ).pdiv ↑ArithmeticFunction.id) m ≥ ∑ m ∈ Finset.Icc 1 ⌊√s.level⌋₊, 1 / ↑m
Theorem: Sieve.boundingSum_ge_sum
Proof state before:
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ s.selbergBoundingSum ≥ ∑ m ∈ Finset.Icc 1 ⌊√s.level⌋₊, ((↑ζ).pdiv ↑ArithmeticFunction.id) m

s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ ∑ m ∈ Finset.Icc 1 ⌊√s.level⌋₊, ((↑ζ).pdiv ↑ArithmeticFunction.id) m ≥ ∑ m ∈ Finset.Icc 1 ⌊√s.level⌋₊, 1 / ↑m
Tactic:
rw[←hnu]
Proof state after:
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ s.selbergBoundingSum ≥ ∑ m ∈ Finset.Icc 1 ⌊√s.level⌋₊, s.nu m

s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ ∑ m ∈ Finset.Icc 1 ⌊√s.level⌋₊, ((↑ζ).pdiv ↑ArithmeticFunction.id) m ≥ ∑ m ∈ Finset.Icc 1 ⌊√s.level⌋₊, 1 / ↑m
Theorem: Sieve.boundingSum_ge_sum
Proof state before:
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ s.selbergBoundingSum ≥ ∑ m ∈ Finset.Icc 1 ⌊√s.level⌋₊, s.nu m

s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ ∑ m ∈ Finset.Icc 1 ⌊√s.level⌋₊, ((↑ζ).pdiv ↑ArithmeticFunction.id) m ≥ ∑ m ∈ Finset.Icc 1 ⌊√s.level⌋₊, 1 / ↑m
Tactic:
apply selbergBoundingSum_ge_sum_div
Proof state after:
case hP
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes

case hnu
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ CompletelyMultiplicative s.nu

case hnu_nonneg
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ ∀ (n : ℕ), 0 ≤ s.nu n

case hnu_lt
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ ∀ (p : ℕ), p.Prime → p ∣ s.prodPrimes → s.nu p < 1

s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ ∑ m ∈ Finset.Icc 1 ⌊√s.level⌋₊, ((↑ζ).pdiv ↑ArithmeticFunction.id) m ≥ ∑ m ∈ Finset.Icc 1 ⌊√s.level⌋₊, 1 / ↑m
Theorem: Sieve.boundingSum_ge_sum
Proof state before:
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ ∑ m ∈ Finset.Icc 1 ⌊√s.level⌋₊, ((↑ζ).pdiv ↑ArithmeticFunction.id) m ≥ ∑ m ∈ Finset.Icc 1 ⌊√s.level⌋₊, 1 / ↑m
Tactic:
apply le_of_eq
Proof state after:
case a
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ ∑ m ∈ Finset.Icc 1 ⌊√s.level⌋₊, 1 / ↑m = ∑ m ∈ Finset.Icc 1 ⌊√s.level⌋₊, ((↑ζ).pdiv ↑ArithmeticFunction.id) m
Theorem: Sieve.boundingSum_ge_sum
Proof state before:
case a
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ ∑ m ∈ Finset.Icc 1 ⌊√s.level⌋₊, 1 / ↑m = ∑ m ∈ Finset.Icc 1 ⌊√s.level⌋₊, ((↑ζ).pdiv ↑ArithmeticFunction.id) m
Tactic:
apply Finset.sum_congr rfl
Proof state after:
case a
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ ∀ x ∈ Finset.Icc 1 ⌊√s.level⌋₊, 1 / ↑x = ((↑ζ).pdiv ↑ArithmeticFunction.id) x
Theorem: Sieve.boundingSum_ge_sum
Proof state before:
case a
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ ∀ x ∈ Finset.Icc 1 ⌊√s.level⌋₊, 1 / ↑x = ((↑ζ).pdiv ↑ArithmeticFunction.id) x
Tactic:
intro m hm
Proof state after:
case a
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
m : ℕ
hm : m ∈ Finset.Icc 1 ⌊√s.level⌋₊
⊢ 1 / ↑m = ((↑ζ).pdiv ↑ArithmeticFunction.id) m
Theorem: Sieve.boundingSum_ge_sum
Proof state before:
case a
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
m : ℕ
hm : m ∈ Finset.Icc 1 ⌊√s.level⌋₊
⊢ 1 / ↑m = ((↑ζ).pdiv ↑ArithmeticFunction.id) m
Tactic:
rw [Finset.mem_Icc] at hm
Proof state after:
case a
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
m : ℕ
hm : 1 ≤ m ∧ m ≤ ⌊√s.level⌋₊
⊢ 1 / ↑m = ((↑ζ).pdiv ↑ArithmeticFunction.id) m
Theorem: Sieve.boundingSum_ge_sum
Proof state before:
case a
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
m : ℕ
hm : 1 ≤ m ∧ m ≤ ⌊√s.level⌋₊
⊢ 1 / ↑m = ((↑ζ).pdiv ↑ArithmeticFunction.id) m
Tactic:
simp only [one_div, ArithmeticFunction.pdiv_apply, ArithmeticFunction.natCoe_apply,
  ArithmeticFunction.zeta_apply_ne (show m ≠ 0 by omega), Nat.cast_ite, CharP.cast_eq_zero, Nat.cast_one,
  ArithmeticFunction.id_apply]
Proof state after:
no goals
Theorem: Sieve.boundingSum_ge_sum
Proof state before:
case hP
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
Tactic:
intro p hpp hple
Proof state after:
case hP
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
p : ℕ
hpp : p.Prime
hple : ↑p ≤ s.level
⊢ p ∣ s.prodPrimes
Theorem: Sieve.boundingSum_ge_sum
Proof state before:
case hP
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
p : ℕ
hpp : p.Prime
hple : ↑p ≤ s.level
⊢ p ∣ s.prodPrimes
Tactic:
apply hP p hpp hple
Proof state after:
no goals
Theorem: Sieve.boundingSum_ge_sum
Proof state before:
case hnu
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ CompletelyMultiplicative s.nu
Tactic:
rw[hnu]
Proof state after:
case hnu
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ CompletelyMultiplicative ((↑ζ).pdiv ↑ArithmeticFunction.id)
Theorem: Sieve.boundingSum_ge_sum
Proof state before:
case hnu
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ CompletelyMultiplicative ((↑ζ).pdiv ↑ArithmeticFunction.id)
Tactic:
exact CompletelyMultiplicative.zeta.pdiv CompletelyMultiplicative.id
Proof state after:
no goals
Theorem: Sieve.boundingSum_ge_sum
Proof state before:
case hnu_nonneg
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ ∀ (n : ℕ), 0 ≤ s.nu n
Tactic:
intro n
Proof state after:
case hnu_nonneg
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
n : ℕ
⊢ 0 ≤ s.nu n
Theorem: Sieve.boundingSum_ge_sum
Proof state before:
case hnu_nonneg
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
n : ℕ
⊢ 0 ≤ s.nu n
Tactic:
rw[hnu]
Proof state after:
case hnu_nonneg
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
n : ℕ
⊢ 0 ≤ ((↑ζ).pdiv ↑ArithmeticFunction.id) n
Theorem: Sieve.boundingSum_ge_sum
Proof state before:
case hnu_nonneg
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
n : ℕ
⊢ 0 ≤ ((↑ζ).pdiv ↑ArithmeticFunction.id) n
Tactic:
apply div_nonneg
Proof state after:
case hnu_nonneg.ha
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
n : ℕ
⊢ 0 ≤ ↑ζ n

case hnu_nonneg.hb
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
n : ℕ
⊢ 0 ≤ ↑ArithmeticFunction.id n
Theorem: Sieve.boundingSum_ge_sum
Proof state before:
case hnu_nonneg.hb
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
n : ℕ
⊢ 0 ≤ ↑ArithmeticFunction.id n
Tactic:
simp
Proof state after:
no goals
Theorem: Sieve.boundingSum_ge_sum
Proof state before:
case hnu_nonneg.ha
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
n : ℕ
⊢ 0 ≤ ↑ζ n
Tactic:
by_cases h : n = 0 <;> simp[h]
Proof state after:
no goals
Theorem: Sieve.boundingSum_ge_sum
Proof state before:
case hnu_lt
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ ∀ (p : ℕ), p.Prime → p ∣ s.prodPrimes → s.nu p < 1
Tactic:
intro p hpp _
Proof state after:
case hnu_lt
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
p : ℕ
hpp : p.Prime
a✝ : p ∣ s.prodPrimes
⊢ s.nu p < 1
Theorem: Sieve.boundingSum_ge_sum
Proof state before:
case hnu_lt
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
p : ℕ
hpp : p.Prime
a✝ : p ∣ s.prodPrimes
⊢ s.nu p < 1
Tactic:
rw[hnu]
Proof state after:
case hnu_lt
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
p : ℕ
hpp : p.Prime
a✝ : p ∣ s.prodPrimes
⊢ ((↑ζ).pdiv ↑ArithmeticFunction.id) p < 1
Theorem: Sieve.boundingSum_ge_sum
Proof state before:
case hnu_lt
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
p : ℕ
hpp : p.Prime
a✝ : p ∣ s.prodPrimes
⊢ ((↑ζ).pdiv ↑ArithmeticFunction.id) p < 1
Tactic:
simp only [ArithmeticFunction.pdiv_apply, ArithmeticFunction.natCoe_apply,
  ArithmeticFunction.zeta_apply, Nat.cast_ite, CharP.cast_eq_zero, Nat.cast_one,
  ArithmeticFunction.id_apply]
Proof state after:
case hnu_lt
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
p : ℕ
hpp : p.Prime
a✝ : p ∣ s.prodPrimes
⊢ (if p = 0 then 0 else 1) / ↑p < 1
Theorem: Sieve.boundingSum_ge_sum
Proof state before:
case hnu_lt
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
p : ℕ
hpp : p.Prime
a✝ : p ∣ s.prodPrimes
⊢ (if p = 0 then 0 else 1) / ↑p < 1
Tactic:
rw [if_neg, one_div]
Proof state after:
case hnu_lt
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
p : ℕ
hpp : p.Prime
a✝ : p ∣ s.prodPrimes
⊢ (↑p)⁻¹ < 1

case hnu_lt.hnc
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
p : ℕ
hpp : p.Prime
a✝ : p ∣ s.prodPrimes
⊢ ¬p = 0
Theorem: Sieve.boundingSum_ge_sum
Proof state before:
case hnu_lt
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
p : ℕ
hpp : p.Prime
a✝ : p ∣ s.prodPrimes
⊢ (↑p)⁻¹ < 1

case hnu_lt.hnc
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
p : ℕ
hpp : p.Prime
a✝ : p ∣ s.prodPrimes
⊢ ¬p = 0
Tactic:
apply inv_lt_one
Proof state after:
case hnu_lt.ha
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
p : ℕ
hpp : p.Prime
a✝ : p ∣ s.prodPrimes
⊢ 1 < ↑p

case hnu_lt.hnc
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
p : ℕ
hpp : p.Prime
a✝ : p ∣ s.prodPrimes
⊢ ¬p = 0
Theorem: Sieve.boundingSum_ge_sum
Proof state before:
case hnu_lt.ha
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
p : ℕ
hpp : p.Prime
a✝ : p ∣ s.prodPrimes
⊢ 1 < ↑p

case hnu_lt.hnc
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
p : ℕ
hpp : p.Prime
a✝ : p ∣ s.prodPrimes
⊢ ¬p = 0
Tactic:
norm_cast
Proof state after:
case hnu_lt.ha
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
p : ℕ
hpp : p.Prime
a✝ : p ∣ s.prodPrimes
⊢ 1 < p

case hnu_lt.hnc
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
p : ℕ
hpp : p.Prime
a✝ : p ∣ s.prodPrimes
⊢ ¬p = 0
Theorem: Sieve.boundingSum_ge_sum
Proof state before:
case hnu_lt.ha
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
p : ℕ
hpp : p.Prime
a✝ : p ∣ s.prodPrimes
⊢ 1 < p

case hnu_lt.hnc
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
p : ℕ
hpp : p.Prime
a✝ : p ∣ s.prodPrimes
⊢ ¬p = 0
Tactic:
exact hpp.one_lt
Proof state after:
case hnu_lt.hnc
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
p : ℕ
hpp : p.Prime
a✝ : p ∣ s.prodPrimes
⊢ ¬p = 0
Theorem: Sieve.boundingSum_ge_sum
Proof state before:
case hnu_lt.hnc
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
p : ℕ
hpp : p.Prime
a✝ : p ∣ s.prodPrimes
⊢ ¬p = 0
Tactic:
exact hpp.ne_zero
Proof state after:
no goals
Theorem: Sieve.boundingSum_ge_sum
Proof state before:
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
m : ℕ
hm : 1 ≤ m ∧ m ≤ ⌊√s.level⌋₊
⊢ m ≠ 0
Tactic:
omega
Proof state after:
no goals
Theorem: Sieve.boundingSum_ge_log
Proof state before:
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ s.selbergBoundingSum ≥ s.level.log / 2
Tactic:
trans (∑ m in Finset.Icc 1 (Nat.floor $ Real.sqrt s.level), 1 / (m:ℝ))
Proof state after:
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ s.selbergBoundingSum ≥ ∑ m ∈ Finset.Icc 1 ⌊√s.level⌋₊, 1 / ↑m

s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ ∑ m ∈ Finset.Icc 1 ⌊√s.level⌋₊, 1 / ↑m ≥ s.level.log / 2
Theorem: Sieve.boundingSum_ge_log
Proof state before:
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ ∑ m ∈ Finset.Icc 1 ⌊√s.level⌋₊, 1 / ↑m ≥ s.level.log / 2
Tactic:
trans (Real.log $ Real.sqrt s.level)
Proof state after:
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ ∑ m ∈ Finset.Icc 1 ⌊√s.level⌋₊, 1 / ↑m ≥ (√s.level).log

s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ (√s.level).log ≥ s.level.log / 2