internlm/Lean-Github huggingface dataset:
Theorem: Sieve.conv_selbergTerms_eq_selbergTerms_mul_nu
Proof state before:
case hdl
s : Sieve
d : ℕ
hd : d ∣ P
l : ℕ
hl : l ∈ P.divisors
h : l ∣ d
⊢ l ∣ d

case hl
s : Sieve
d : ℕ
hd : d ∣ P
l : ℕ
hl : l ∈ P.divisors
h : l ∣ d
⊢ Squarefree d

case hd
s : Sieve
d : ℕ
hd : d ∣ P
l : ℕ
hl : l ∈ P.divisors
h : l ∣ d
⊢ g l ≠ 0
Tactic:
exact h
Proof state after:
case hl
s : Sieve
d : ℕ
hd : d ∣ P
l : ℕ
hl : l ∈ P.divisors
h : l ∣ d
⊢ Squarefree d

case hd
s : Sieve
d : ℕ
hd : d ∣ P
l : ℕ
hl : l ∈ P.divisors
h : l ∣ d
⊢ g l ≠ 0
Theorem: Sieve.conv_selbergTerms_eq_selbergTerms_mul_nu
Proof state before:
case hl
s : Sieve
d : ℕ
hd : d ∣ P
l : ℕ
hl : l ∈ P.divisors
h : l ∣ d
⊢ Squarefree d

case hd
s : Sieve
d : ℕ
hd : d ∣ P
l : ℕ
hl : l ∈ P.divisors
h : l ∣ d
⊢ g l ≠ 0
Tactic:
apply Squarefree.squarefree_of_dvd hd s.prodPrimes_squarefree
Proof state after:
case hd
s : Sieve
d : ℕ
hd : d ∣ P
l : ℕ
hl : l ∈ P.divisors
h : l ∣ d
⊢ g l ≠ 0
Theorem: Sieve.conv_selbergTerms_eq_selbergTerms_mul_nu
Proof state before:
case hd
s : Sieve
d : ℕ
hd : d ∣ P
l : ℕ
hl : l ∈ P.divisors
h : l ∣ d
⊢ g l ≠ 0
Tactic:
apply _root_.ne_of_gt
Proof state after:
case hd.h
s : Sieve
d : ℕ
hd : d ∣ P
l : ℕ
hl : l ∈ P.divisors
h : l ∣ d
⊢ 0 < g l
Theorem: Sieve.conv_selbergTerms_eq_selbergTerms_mul_nu
Proof state before:
case hd.h
s : Sieve
d : ℕ
hd : d ∣ P
l : ℕ
hl : l ∈ P.divisors
h : l ∣ d
⊢ 0 < g l
Tactic:
rw [mem_divisors] at hl
Proof state after:
case hd.h
s : Sieve
d : ℕ
hd : d ∣ P
l : ℕ
hl : l ∣ P ∧ P ≠ 0
h : l ∣ d
⊢ 0 < g l
Theorem: Sieve.conv_selbergTerms_eq_selbergTerms_mul_nu
Proof state before:
case hd.h
s : Sieve
d : ℕ
hd : d ∣ P
l : ℕ
hl : l ∣ P ∧ P ≠ 0
h : l ∣ d
⊢ 0 < g l
Tactic:
apply selbergTerms_pos
Proof state after:
case hd.h.hl
s : Sieve
d : ℕ
hd : d ∣ P
l : ℕ
hl : l ∣ P ∧ P ≠ 0
h : l ∣ d
⊢ l ∣ P
Theorem: Sieve.conv_selbergTerms_eq_selbergTerms_mul_nu
Proof state before:
case hd.h.hl
s : Sieve
d : ℕ
hd : d ∣ P
l : ℕ
hl : l ∣ P ∧ P ≠ 0
h : l ∣ d
⊢ l ∣ P
Tactic:
exact hl.left
Proof state after:
no goals
Theorem: Sieve.conv_selbergTerms_eq_selbergTerms_mul_nu
Proof state before:
s : Sieve
d : ℕ
hd : d ∣ P
⊢ (g d * ∑ l ∈ P.divisors, if l ∣ d then 1 / g l else 0) = g d * (ν d)⁻¹
Tactic:
rw [← s.nu_eq_conv_one_div_selbergTerms d hd]
Proof state after:
no goals
Theorem: Sieve.upper_bound_of_UpperBoundSieve
Proof state before:
s : Sieve
μPlus : UpperBoundSieve
⊢ s.siftedSum ≤ ∑ d ∈ P.divisors, μPlus.μPlus d * s.multSum d
Tactic:
have hμ : ∀ n, δ n ≤ ∑ d in n.divisors, μPlus d := μPlus.hμPlus
Proof state after:
s : Sieve
μPlus : UpperBoundSieve
hμ : ∀ (n : ℕ), δ n ≤ ∑ d ∈ n.divisors, μPlus.μPlus d
⊢ s.siftedSum ≤ ∑ d ∈ P.divisors, μPlus.μPlus d * s.multSum d
Theorem: Sieve.upper_bound_of_UpperBoundSieve
Proof state before:
s : Sieve
μPlus : UpperBoundSieve
hμ : ∀ (n : ℕ), δ n ≤ ∑ d ∈ n.divisors, μPlus.μPlus d
⊢ s.siftedSum ≤ ∑ d ∈ P.divisors, μPlus.μPlus d * s.multSum d
Tactic:
rw [siftedSum_as_delta]
Proof state after:
s : Sieve
μPlus : UpperBoundSieve
hμ : ∀ (n : ℕ), δ n ≤ ∑ d ∈ n.divisors, μPlus.μPlus d
⊢ ∑ d ∈ A, s.weights d * δ (P.gcd d) ≤ ∑ d ∈ P.divisors, μPlus.μPlus d * s.multSum d
Theorem: Sieve.upper_bound_of_UpperBoundSieve
Proof state before:
s : Sieve
μPlus : UpperBoundSieve
hμ : ∀ (n : ℕ), δ n ≤ ∑ d ∈ n.divisors, μPlus.μPlus d
⊢ ∑ d ∈ A, s.weights d * δ (P.gcd d) ≤ ∑ d ∈ P.divisors, μPlus.μPlus d * s.multSum d
Tactic:
trans (∑ n in s.support, a n * ∑ d in (Nat.gcd P n).divisors, μPlus d)
Proof state after:
s : Sieve
μPlus : UpperBoundSieve
hμ : ∀ (n : ℕ), δ n ≤ ∑ d ∈ n.divisors, μPlus.μPlus d
⊢ ∑ d ∈ A, s.weights d * δ (P.gcd d) ≤ ∑ n ∈ A, s.weights n * ∑ d ∈ (P.gcd n).divisors, μPlus.μPlus d

s : Sieve
μPlus : UpperBoundSieve
hμ : ∀ (n : ℕ), δ n ≤ ∑ d ∈ n.divisors, μPlus.μPlus d
⊢ ∑ n ∈ A, s.weights n * ∑ d ∈ (P.gcd n).divisors, μPlus.μPlus d ≤ ∑ d ∈ P.divisors, μPlus.μPlus d * s.multSum d
Theorem: Sieve.upper_bound_of_UpperBoundSieve
Proof state before:
s : Sieve
μPlus : UpperBoundSieve
hμ : ∀ (n : ℕ), δ n ≤ ∑ d ∈ n.divisors, μPlus.μPlus d
⊢ ∑ n ∈ A, s.weights n * ∑ d ∈ (P.gcd n).divisors, μPlus.μPlus d ≤ ∑ d ∈ P.divisors, μPlus.μPlus d * s.multSum d
Tactic:
apply le_of_eq
Proof state after:
case a
s : Sieve
μPlus : UpperBoundSieve
hμ : ∀ (n : ℕ), δ n ≤ ∑ d ∈ n.divisors, μPlus.μPlus d
⊢ ∑ n ∈ A, s.weights n * ∑ d ∈ (P.gcd n).divisors, μPlus.μPlus d = ∑ d ∈ P.divisors, μPlus.μPlus d * s.multSum d
Theorem: Sieve.upper_bound_of_UpperBoundSieve
Proof state before:
case a
s : Sieve
μPlus : UpperBoundSieve
hμ : ∀ (n : ℕ), δ n ≤ ∑ d ∈ n.divisors, μPlus.μPlus d
⊢ ∑ n ∈ A, s.weights n * ∑ d ∈ (P.gcd n).divisors, μPlus.μPlus d = ∑ d ∈ P.divisors, μPlus.μPlus d * s.multSum d
Tactic:
trans (∑ n in s.support, ∑ d in divisors P, if d ∣ n then a n * μPlus d else 0)
Proof state after:
s : Sieve
μPlus : UpperBoundSieve
hμ : ∀ (n : ℕ), δ n ≤ ∑ d ∈ n.divisors, μPlus.μPlus d
⊢ ∑ n ∈ A, s.weights n * ∑ d ∈ (P.gcd n).divisors, μPlus.μPlus d =
    ∑ n ∈ A, ∑ d ∈ P.divisors, if d ∣ n then s.weights n * μPlus.μPlus d else 0

s : Sieve
μPlus : UpperBoundSieve
hμ : ∀ (n : ℕ), δ n ≤ ∑ d ∈ n.divisors, μPlus.μPlus d
⊢ (∑ n ∈ A, ∑ d ∈ P.divisors, if d ∣ n then s.weights n * μPlus.μPlus d else 0) =
    ∑ d ∈ P.divisors, μPlus.μPlus d * s.multSum d
Theorem: Sieve.upper_bound_of_UpperBoundSieve
Proof state before:
s : Sieve
μPlus : UpperBoundSieve
hμ : ∀ (n : ℕ), δ n ≤ ∑ d ∈ n.divisors, μPlus.μPlus d
⊢ (∑ n ∈ A, ∑ d ∈ P.divisors, if d ∣ n then s.weights n * μPlus.μPlus d else 0) =
    ∑ d ∈ P.divisors, μPlus.μPlus d * s.multSum d
Tactic:
rw [sum_comm, sum_congr rfl]
Proof state after:
s : Sieve
μPlus : UpperBoundSieve
hμ : ∀ (n : ℕ), δ n ≤ ∑ d ∈ n.divisors, μPlus.μPlus d
⊢ ∀ x ∈ P.divisors, (∑ x_1 ∈ A, if x ∣ x_1 then s.weights x_1 * μPlus.μPlus x else 0) = μPlus.μPlus x * s.multSum x
Theorem: Sieve.upper_bound_of_UpperBoundSieve
Proof state before:
s : Sieve
μPlus : UpperBoundSieve
hμ : ∀ (n : ℕ), δ n ≤ ∑ d ∈ n.divisors, μPlus.μPlus d
⊢ ∀ x ∈ P.divisors, (∑ x_1 ∈ A, if x ∣ x_1 then s.weights x_1 * μPlus.μPlus x else 0) = μPlus.μPlus x * s.multSum x
Tactic:
intro d _
Proof state after:
s : Sieve
μPlus : UpperBoundSieve
hμ : ∀ (n : ℕ), δ n ≤ ∑ d ∈ n.divisors, μPlus.μPlus d
d : ℕ
a✝ : d ∈ P.divisors
⊢ (∑ x ∈ A, if d ∣ x then s.weights x * μPlus.μPlus d else 0) = μPlus.μPlus d * s.multSum d
Theorem: Sieve.upper_bound_of_UpperBoundSieve
Proof state before:
s : Sieve
μPlus : UpperBoundSieve
hμ : ∀ (n : ℕ), δ n ≤ ∑ d ∈ n.divisors, μPlus.μPlus d
d : ℕ
a✝ : d ∈ P.divisors
⊢ (∑ x ∈ A, if d ∣ x then s.weights x * μPlus.μPlus d else 0) = μPlus.μPlus d * s.multSum d
Tactic:
dsimp only [multSum]
Proof state after:
s : Sieve
μPlus : UpperBoundSieve
hμ : ∀ (n : ℕ), δ n ≤ ∑ d ∈ n.divisors, μPlus.μPlus d
d : ℕ
a✝ : d ∈ P.divisors
⊢ (∑ x ∈ A, if d ∣ x then s.weights x * μPlus.μPlus d else 0) =
    μPlus.μPlus d * ∑ n ∈ A, if d ∣ n then s.weights n else 0
Theorem: Sieve.upper_bound_of_UpperBoundSieve
Proof state before:
s : Sieve
μPlus : UpperBoundSieve
hμ : ∀ (n : ℕ), δ n ≤ ∑ d ∈ n.divisors, μPlus.μPlus d
d : ℕ
a✝ : d ∈ P.divisors
⊢ (∑ x ∈ A, if d ∣ x then s.weights x * μPlus.μPlus d else 0) =
    μPlus.μPlus d * ∑ n ∈ A, if d ∣ n then s.weights n else 0
Tactic:
rw [mul_sum, sum_congr rfl]
Proof state after:
s : Sieve
μPlus : UpperBoundSieve
hμ : ∀ (n : ℕ), δ n ≤ ∑ d ∈ n.divisors, μPlus.μPlus d
d : ℕ
a✝ : d ∈ P.divisors
⊢ ∀ x ∈ A, (if d ∣ x then s.weights x * μPlus.μPlus d else 0) = μPlus.μPlus d * if d ∣ x then s.weights x else 0
Theorem: Sieve.upper_bound_of_UpperBoundSieve
Proof state before:
s : Sieve
μPlus : UpperBoundSieve
hμ : ∀ (n : ℕ), δ n ≤ ∑ d ∈ n.divisors, μPlus.μPlus d
d : ℕ
a✝ : d ∈ P.divisors
⊢ ∀ x ∈ A, (if d ∣ x then s.weights x * μPlus.μPlus d else 0) = μPlus.μPlus d * if d ∣ x then s.weights x else 0
Tactic:
intro n _
Proof state after:
s : Sieve
μPlus : UpperBoundSieve
hμ : ∀ (n : ℕ), δ n ≤ ∑ d ∈ n.divisors, μPlus.μPlus d
d : ℕ
a✝¹ : d ∈ P.divisors
n : ℕ
a✝ : n ∈ A
⊢ (if d ∣ n then s.weights n * μPlus.μPlus d else 0) = μPlus.μPlus d * if d ∣ n then s.weights n else 0
Theorem: Sieve.upper_bound_of_UpperBoundSieve
Proof state before:
s : Sieve
μPlus : UpperBoundSieve
hμ : ∀ (n : ℕ), δ n ≤ ∑ d ∈ n.divisors, μPlus.μPlus d
d : ℕ
a✝¹ : d ∈ P.divisors
n : ℕ
a✝ : n ∈ A
⊢ (if d ∣ n then s.weights n * μPlus.μPlus d else 0) = μPlus.μPlus d * if d ∣ n then s.weights n else 0
Tactic:
rw [←ite_zero_mul, mul_comm]
Proof state after:
no goals
Theorem: Sieve.upper_bound_of_UpperBoundSieve
Proof state before:
s : Sieve
μPlus : UpperBoundSieve
hμ : ∀ (n : ℕ), δ n ≤ ∑ d ∈ n.divisors, μPlus.μPlus d
⊢ ∑ d ∈ A, s.weights d * δ (P.gcd d) ≤ ∑ n ∈ A, s.weights n * ∑ d ∈ (P.gcd n).divisors, μPlus.μPlus d
Tactic:
apply Finset.sum_le_sum
Proof state after:
case h
s : Sieve
μPlus : UpperBoundSieve
hμ : ∀ (n : ℕ), δ n ≤ ∑ d ∈ n.divisors, μPlus.μPlus d
⊢ ∀ i ∈ A, s.weights i * δ (P.gcd i) ≤ s.weights i * ∑ d ∈ (P.gcd i).divisors, μPlus.μPlus d
Theorem: Sieve.upper_bound_of_UpperBoundSieve
Proof state before:
case h
s : Sieve
μPlus : UpperBoundSieve
hμ : ∀ (n : ℕ), δ n ≤ ∑ d ∈ n.divisors, μPlus.μPlus d
⊢ ∀ i ∈ A, s.weights i * δ (P.gcd i) ≤ s.weights i * ∑ d ∈ (P.gcd i).divisors, μPlus.μPlus d
Tactic:
intro n _
Proof state after:
case h
s : Sieve
μPlus : UpperBoundSieve
hμ : ∀ (n : ℕ), δ n ≤ ∑ d ∈ n.divisors, μPlus.μPlus d
n : ℕ
a✝ : n ∈ A
⊢ s.weights n * δ (P.gcd n) ≤ s.weights n * ∑ d ∈ (P.gcd n).divisors, μPlus.μPlus d
Theorem: Sieve.upper_bound_of_UpperBoundSieve
Proof state before:
case h
s : Sieve
μPlus : UpperBoundSieve
hμ : ∀ (n : ℕ), δ n ≤ ∑ d ∈ n.divisors, μPlus.μPlus d
n : ℕ
a✝ : n ∈ A
⊢ s.weights n * δ (P.gcd n) ≤ s.weights n * ∑ d ∈ (P.gcd n).divisors, μPlus.μPlus d
Tactic:
exact mul_le_mul_of_nonneg_left (hμ (Nat.gcd P n)) (s.weights_nonneg n)
Proof state after:
no goals
Theorem: Sieve.upper_bound_of_UpperBoundSieve
Proof state before:
s : Sieve
μPlus : UpperBoundSieve
hμ : ∀ (n : ℕ), δ n ≤ ∑ d ∈ n.divisors, μPlus.μPlus d
⊢ ∑ n ∈ A, s.weights n * ∑ d ∈ (P.gcd n).divisors, μPlus.μPlus d =
    ∑ n ∈ A, ∑ d ∈ P.divisors, if d ∣ n then s.weights n * μPlus.μPlus d else 0
Tactic:
apply sum_congr rfl
Proof state after:
s : Sieve
μPlus : UpperBoundSieve
hμ : ∀ (n : ℕ), δ n ≤ ∑ d ∈ n.divisors, μPlus.μPlus d
⊢ ∀ x ∈ A,
    s.weights x * ∑ d ∈ (P.gcd x).divisors, μPlus.μPlus d =
      ∑ d ∈ P.divisors, if d ∣ x then s.weights x * μPlus.μPlus d else 0
Theorem: Sieve.upper_bound_of_UpperBoundSieve
Proof state before:
s : Sieve
μPlus : UpperBoundSieve
hμ : ∀ (n : ℕ), δ n ≤ ∑ d ∈ n.divisors, μPlus.μPlus d
⊢ ∀ x ∈ A,
    s.weights x * ∑ d ∈ (P.gcd x).divisors, μPlus.μPlus d =
      ∑ d ∈ P.divisors, if d ∣ x then s.weights x * μPlus.μPlus d else 0
Tactic:
intro n _
Proof state after:
s : Sieve
μPlus : UpperBoundSieve
hμ : ∀ (n : ℕ), δ n ≤ ∑ d ∈ n.divisors, μPlus.μPlus d
n : ℕ
a✝ : n ∈ A
⊢ s.weights n * ∑ d ∈ (P.gcd n).divisors, μPlus.μPlus d =
    ∑ d ∈ P.divisors, if d ∣ n then s.weights n * μPlus.μPlus d else 0
Theorem: Sieve.upper_bound_of_UpperBoundSieve
Proof state before:
s : Sieve
μPlus : UpperBoundSieve
hμ : ∀ (n : ℕ), δ n ≤ ∑ d ∈ n.divisors, μPlus.μPlus d
n : ℕ
a✝ : n ∈ A
⊢ s.weights n * ∑ d ∈ (P.gcd n).divisors, μPlus.μPlus d =
    ∑ d ∈ P.divisors, if d ∣ n then s.weights n * μPlus.μPlus d else 0
Tactic:
rw [mul_sum, sum_over_dvd_ite s.prodPrimes_ne_zero (Nat.gcd_dvd_left _ _), sum_congr rfl]
Proof state after:
s : Sieve
μPlus : UpperBoundSieve
hμ : ∀ (n : ℕ), δ n ≤ ∑ d ∈ n.divisors, μPlus.μPlus d
n : ℕ
a✝ : n ∈ A
⊢ ∀ x ∈ P.divisors,
    (if x ∣ P.gcd n then s.weights n * μPlus.μPlus x else 0) = if x ∣ n then s.weights n * μPlus.μPlus x else 0
Theorem: Sieve.upper_bound_of_UpperBoundSieve
Proof state before:
s : Sieve
μPlus : UpperBoundSieve
hμ : ∀ (n : ℕ), δ n ≤ ∑ d ∈ n.divisors, μPlus.μPlus d
n : ℕ
a✝ : n ∈ A
⊢ ∀ x ∈ P.divisors,
    (if x ∣ P.gcd n then s.weights n * μPlus.μPlus x else 0) = if x ∣ n then s.weights n * μPlus.μPlus x else 0
Tactic:
intro d hd
Proof state after:
s : Sieve
μPlus : UpperBoundSieve
hμ : ∀ (n : ℕ), δ n ≤ ∑ d ∈ n.divisors, μPlus.μPlus d
n : ℕ
a✝ : n ∈ A
d : ℕ
hd : d ∈ P.divisors
⊢ (if d ∣ P.gcd n then s.weights n * μPlus.μPlus d else 0) = if d ∣ n then s.weights n * μPlus.μPlus d else 0
Theorem: Sieve.upper_bound_of_UpperBoundSieve
Proof state before:
s : Sieve
μPlus : UpperBoundSieve
hμ : ∀ (n : ℕ), δ n ≤ ∑ d ∈ n.divisors, μPlus.μPlus d
n : ℕ
a✝ : n ∈ A
d : ℕ
hd : d ∈ P.divisors
⊢ (if d ∣ P.gcd n then s.weights n * μPlus.μPlus d else 0) = if d ∣ n then s.weights n * μPlus.μPlus d else 0
Tactic:
apply if_congr _ rfl rfl
Proof state after:
s : Sieve
μPlus : UpperBoundSieve
hμ : ∀ (n : ℕ), δ n ≤ ∑ d ∈ n.divisors, μPlus.μPlus d
n : ℕ
a✝ : n ∈ A
d : ℕ
hd : d ∈ P.divisors
⊢ d ∣ P.gcd n ↔ d ∣ n
Theorem: Sieve.upper_bound_of_UpperBoundSieve
Proof state before:
s : Sieve
μPlus : UpperBoundSieve
hμ : ∀ (n : ℕ), δ n ≤ ∑ d ∈ n.divisors, μPlus.μPlus d
n : ℕ
a✝ : n ∈ A
d : ℕ
hd : d ∈ P.divisors
⊢ d ∣ P.gcd n ↔ d ∣ n
Tactic:
rw [Nat.dvd_gcd_iff, and_iff_right (dvd_of_mem_divisors hd)]
Proof state after:
no goals
Theorem: Sieve.siftedSum_le_mainSum_errSum_of_UpperBoundSieve
Proof state before:
s : Sieve
μPlus : UpperBoundSieve
⊢ s.siftedSum ≤ X * s.mainSum μPlus.μPlus + s.errSum μPlus.μPlus
Tactic:
dsimp only [mainSum, errSum]
Proof state after:
s : Sieve
μPlus : UpperBoundSieve
⊢ s.siftedSum ≤ X * ∑ d ∈ P.divisors, μPlus.μPlus d * ν d + ∑ d ∈ P.divisors, |μPlus.μPlus d| * |s.rem d|
Theorem: Sieve.siftedSum_le_mainSum_errSum_of_UpperBoundSieve
Proof state before:
s : Sieve
μPlus : UpperBoundSieve
⊢ s.siftedSum ≤ X * ∑ d ∈ P.divisors, μPlus.μPlus d * ν d + ∑ d ∈ P.divisors, |μPlus.μPlus d| * |s.rem d|
Tactic:
trans (∑ d in divisors P, μPlus d * s.multSum d)
Proof state after:
s : Sieve
μPlus : UpperBoundSieve
⊢ s.siftedSum ≤ ∑ d ∈ P.divisors, μPlus.μPlus d * s.multSum d

s : Sieve
μPlus : UpperBoundSieve
⊢ ∑ d ∈ P.divisors, μPlus.μPlus d * s.multSum d ≤
    X * ∑ d ∈ P.divisors, μPlus.μPlus d * ν d + ∑ d ∈ P.divisors, |μPlus.μPlus d| * |s.rem d|
Theorem: Sieve.siftedSum_le_mainSum_errSum_of_UpperBoundSieve
Proof state before:
s : Sieve
μPlus : UpperBoundSieve
⊢ ∑ d ∈ P.divisors, μPlus.μPlus d * s.multSum d ≤
    X * ∑ d ∈ P.divisors, μPlus.μPlus d * ν d + ∑ d ∈ P.divisors, |μPlus.μPlus d| * |s.rem d|
Tactic:
trans ( X * ∑ d in divisors P, μPlus d * ν d + ∑ d in divisors P, μPlus d * R d )
Proof state after:
s : Sieve
μPlus : UpperBoundSieve
⊢ ∑ d ∈ P.divisors, μPlus.μPlus d * s.multSum d ≤
    X * ∑ d ∈ P.divisors, μPlus.μPlus d * ν d + ∑ d ∈ P.divisors, μPlus.μPlus d * s.rem d

s : Sieve
μPlus : UpperBoundSieve
⊢ X * ∑ d ∈ P.divisors, μPlus.μPlus d * ν d + ∑ d ∈ P.divisors, μPlus.μPlus d * s.rem d ≤
    X * ∑ d ∈ P.divisors, μPlus.μPlus d * ν d + ∑ d ∈ P.divisors, |μPlus.μPlus d| * |s.rem d|
Theorem: Sieve.siftedSum_le_mainSum_errSum_of_UpperBoundSieve
Proof state before:
s : Sieve
μPlus : UpperBoundSieve
⊢ X * ∑ d ∈ P.divisors, μPlus.μPlus d * ν d + ∑ d ∈ P.divisors, μPlus.μPlus d * s.rem d ≤
    X * ∑ d ∈ P.divisors, μPlus.μPlus d * ν d + ∑ d ∈ P.divisors, |μPlus.μPlus d| * |s.rem d|
Tactic:
apply _root_.add_le_add (le_rfl)
Proof state after:
s : Sieve
μPlus : UpperBoundSieve
⊢ ∑ d ∈ P.divisors, μPlus.μPlus d * s.rem d ≤ ∑ d ∈ P.divisors, |μPlus.μPlus d| * |s.rem d|
Theorem: Sieve.siftedSum_le_mainSum_errSum_of_UpperBoundSieve
Proof state before:
s : Sieve
μPlus : UpperBoundSieve
⊢ ∑ d ∈ P.divisors, μPlus.μPlus d * s.rem d ≤ ∑ d ∈ P.divisors, |μPlus.μPlus d| * |s.rem d|
Tactic:
apply sum_le_sum
Proof state after:
case h
s : Sieve
μPlus : UpperBoundSieve
⊢ ∀ i ∈ P.divisors, μPlus.μPlus i * s.rem i ≤ |μPlus.μPlus i| * |s.rem i|
Theorem: Sieve.siftedSum_le_mainSum_errSum_of_UpperBoundSieve
Proof state before:
case h
s : Sieve
μPlus : UpperBoundSieve
⊢ ∀ i ∈ P.divisors, μPlus.μPlus i * s.rem i ≤ |μPlus.μPlus i| * |s.rem i|
Tactic:
intro d _
Proof state after:
case h
s : Sieve
μPlus : UpperBoundSieve
d : ℕ
a✝ : d ∈ P.divisors
⊢ μPlus.μPlus d * s.rem d ≤ |μPlus.μPlus d| * |s.rem d|
Theorem: Sieve.siftedSum_le_mainSum_errSum_of_UpperBoundSieve
Proof state before:
case h
s : Sieve
μPlus : UpperBoundSieve
d : ℕ
a✝ : d ∈ P.divisors
⊢ μPlus.μPlus d * s.rem d ≤ |μPlus.μPlus d| * |s.rem d|
Tactic:
rw [←abs_mul]
Proof state after:
case h
s : Sieve
μPlus : UpperBoundSieve
d : ℕ
a✝ : d ∈ P.divisors
⊢ μPlus.μPlus d * s.rem d ≤ |μPlus.μPlus d * s.rem d|
Theorem: Sieve.siftedSum_le_mainSum_errSum_of_UpperBoundSieve
Proof state before:
case h
s : Sieve
μPlus : UpperBoundSieve
d : ℕ
a✝ : d ∈ P.divisors
⊢ μPlus.μPlus d * s.rem d ≤ |μPlus.μPlus d * s.rem d|
Tactic:
exact le_abs_self (UpperBoundSieve.μPlus μPlus d * rem s d)
Proof state after:
no goals
Theorem: Sieve.siftedSum_le_mainSum_errSum_of_UpperBoundSieve
Proof state before:
s : Sieve
μPlus : UpperBoundSieve
⊢ s.siftedSum ≤ ∑ d ∈ P.divisors, μPlus.μPlus d * s.multSum d
Tactic:
apply upper_bound_of_UpperBoundSieve
Proof state after:
no goals
Theorem: Sieve.siftedSum_le_mainSum_errSum_of_UpperBoundSieve
Proof state before:
s : Sieve
μPlus : UpperBoundSieve
⊢ ∑ d ∈ P.divisors, μPlus.μPlus d * s.multSum d ≤
    X * ∑ d ∈ P.divisors, μPlus.μPlus d * ν d + ∑ d ∈ P.divisors, μPlus.μPlus d * s.rem d
Tactic:
apply le_of_eq
Proof state after:
case a
s : Sieve
μPlus : UpperBoundSieve
⊢ ∑ d ∈ P.divisors, μPlus.μPlus d * s.multSum d =
    X * ∑ d ∈ P.divisors, μPlus.μPlus d * ν d + ∑ d ∈ P.divisors, μPlus.μPlus d * s.rem d
Theorem: Sieve.siftedSum_le_mainSum_errSum_of_UpperBoundSieve
Proof state before:
case a
s : Sieve
μPlus : UpperBoundSieve
⊢ ∑ d ∈ P.divisors, μPlus.μPlus d * s.multSum d =
    X * ∑ d ∈ P.divisors, μPlus.μPlus d * ν d + ∑ d ∈ P.divisors, μPlus.μPlus d * s.rem d
Tactic:
rw [mul_sum, ←sum_add_distrib]
Proof state after:
case a
s : Sieve
μPlus : UpperBoundSieve
⊢ ∑ d ∈ P.divisors, μPlus.μPlus d * s.multSum d =
    ∑ x ∈ P.divisors, (X * (μPlus.μPlus x * ν x) + μPlus.μPlus x * s.rem x)
Theorem: Sieve.siftedSum_le_mainSum_errSum_of_UpperBoundSieve
Proof state before:
case a
s : Sieve
μPlus : UpperBoundSieve
⊢ ∑ d ∈ P.divisors, μPlus.μPlus d * s.multSum d =
    ∑ x ∈ P.divisors, (X * (μPlus.μPlus x * ν x) + μPlus.μPlus x * s.rem x)
Tactic:
apply sum_congr rfl
Proof state after:
case a
s : Sieve
μPlus : UpperBoundSieve
⊢ ∀ x ∈ P.divisors, μPlus.μPlus x * s.multSum x = X * (μPlus.μPlus x * ν x) + μPlus.μPlus x * s.rem x
Theorem: Sieve.siftedSum_le_mainSum_errSum_of_UpperBoundSieve
Proof state before:
case a
s : Sieve
μPlus : UpperBoundSieve
⊢ ∀ x ∈ P.divisors, μPlus.μPlus x * s.multSum x = X * (μPlus.μPlus x * ν x) + μPlus.μPlus x * s.rem x
Tactic:
intro d _
Proof state after:
case a
s : Sieve
μPlus : UpperBoundSieve
d : ℕ
a✝ : d ∈ P.divisors
⊢ μPlus.μPlus d * s.multSum d = X * (μPlus.μPlus d * ν d) + μPlus.μPlus d * s.rem d
Theorem: Sieve.siftedSum_le_mainSum_errSum_of_UpperBoundSieve
Proof state before:
case a
s : Sieve
μPlus : UpperBoundSieve
d : ℕ
a✝ : d ∈ P.divisors
⊢ μPlus.μPlus d * s.multSum d = X * (μPlus.μPlus d * ν d) + μPlus.μPlus d * s.rem d
Tactic:
dsimp only [rem]
Proof state after:
case a
s : Sieve
μPlus : UpperBoundSieve
d : ℕ
a✝ : d ∈ P.divisors
⊢ μPlus.μPlus d * s.multSum d = X * (μPlus.μPlus d * ν d) + μPlus.μPlus d * (s.multSum d - ν d * X)
Theorem: Sieve.siftedSum_le_mainSum_errSum_of_UpperBoundSieve
Proof state before:
case a
s : Sieve
μPlus : UpperBoundSieve
d : ℕ
a✝ : d ∈ P.divisors
⊢ μPlus.μPlus d * s.multSum d = X * (μPlus.μPlus d * ν d) + μPlus.μPlus d * (s.multSum d - ν d * X)
Tactic:
ring
Proof state after:
no goals
Theorem: Sieve.lambdaSquared_eq_zero_of_support_wlog
Proof state before:
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
d1 d2 : ℕ
h : d = d1.lcm d2
hle : d1 ≤ d2
⊢ w d1 * w d2 = 0
Tactic:
rw [hw d2]
Proof state after:
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
d1 d2 : ℕ
h : d = d1.lcm d2
hle : d1 ≤ d2
⊢ w d1 * 0 = 0

s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
d1 d2 : ℕ
h : d = d1.lcm d2
hle : d1 ≤ d2
⊢ ¬↑d2 ^ 2 ≤ y
Theorem: Sieve.lambdaSquared_eq_zero_of_support_wlog
Proof state before:
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
d1 d2 : ℕ
h : d = d1.lcm d2
hle : d1 ≤ d2
⊢ w d1 * 0 = 0

s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
d1 d2 : ℕ
h : d = d1.lcm d2
hle : d1 ≤ d2
⊢ ¬↑d2 ^ 2 ≤ y
Tactic:
ring
Proof state after:
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
d1 d2 : ℕ
h : d = d1.lcm d2
hle : d1 ≤ d2
⊢ ¬↑d2 ^ 2 ≤ y
Theorem: Sieve.lambdaSquared_eq_zero_of_support_wlog
Proof state before:
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
d1 d2 : ℕ
h : d = d1.lcm d2
hle : d1 ≤ d2
⊢ ¬↑d2 ^ 2 ≤ y
Tactic:
by_contra hyp
Proof state after:
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
d1 d2 : ℕ
h : d = d1.lcm d2
hle : d1 ≤ d2
hyp : ↑d2 ^ 2 ≤ y
⊢ False
Theorem: Sieve.lambdaSquared_eq_zero_of_support_wlog
Proof state before:
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
d1 d2 : ℕ
h : d = d1.lcm d2
hle : d1 ≤ d2
hyp : ↑d2 ^ 2 ≤ y
⊢ False
Tactic:
apply hd
Proof state after:
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
d1 d2 : ℕ
h : d = d1.lcm d2
hle : d1 ≤ d2
hyp : ↑d2 ^ 2 ≤ y
⊢ ↑d ≤ y
Theorem: Sieve.lambdaSquared_eq_zero_of_support_wlog
Proof state before:
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
d1 d2 : ℕ
h : d = d1.lcm d2
hle : d1 ≤ d2
hyp : ↑d2 ^ 2 ≤ y
⊢ ↑d ≤ y
Tactic:
apply le_trans _ hyp
Proof state after:
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
d1 d2 : ℕ
h : d = d1.lcm d2
hle : d1 ≤ d2
hyp : ↑d2 ^ 2 ≤ y
⊢ ↑d ≤ ↑d2 ^ 2
Theorem: Sieve.lambdaSquared_eq_zero_of_support_wlog
Proof state before:
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
d1 d2 : ℕ
h : d = d1.lcm d2
hle : d1 ≤ d2
hyp : ↑d2 ^ 2 ≤ y
⊢ ↑d ≤ ↑d2 ^ 2
Tactic:
norm_cast
Proof state after:
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
d1 d2 : ℕ
h : d = d1.lcm d2
hle : d1 ≤ d2
hyp : ↑d2 ^ 2 ≤ y
⊢ d ≤ d2 ^ 2
Theorem: Sieve.lambdaSquared_eq_zero_of_support_wlog
Proof state before:
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
d1 d2 : ℕ
h : d = d1.lcm d2
hle : d1 ≤ d2
hyp : ↑d2 ^ 2 ≤ y
⊢ d ≤ d2 ^ 2
Tactic:
calc _ ≤ (d1.lcm d2) := by rw [h]
    _ ≤ (d1*d2) := Nat.div_le_self _ _
    _ ≤ _       := ?_
Proof state after:
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
d1 d2 : ℕ
h : d = d1.lcm d2
hle : d1 ≤ d2
hyp : ↑d2 ^ 2 ≤ y
⊢ d1 * d2 ≤ d2 ^ 2
Theorem: Sieve.lambdaSquared_eq_zero_of_support_wlog
Proof state before:
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
d1 d2 : ℕ
h : d = d1.lcm d2
hle : d1 ≤ d2
hyp : ↑d2 ^ 2 ≤ y
⊢ d ≤ d1.lcm d2
Tactic:
rw [h]
Proof state after:
no goals
Theorem: Sieve.lambdaSquared_eq_zero_of_support_wlog
Proof state before:
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
d1 d2 : ℕ
h : d = d1.lcm d2
hle : d1 ≤ d2
hyp : ↑d2 ^ 2 ≤ y
⊢ d1 * d2 ≤ d2 ^ 2
Tactic:
rw [sq]
Proof state after:
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
d1 d2 : ℕ
h : d = d1.lcm d2
hle : d1 ≤ d2
hyp : ↑d2 ^ 2 ≤ y
⊢ d1 * d2 ≤ d2 * d2
Theorem: Sieve.lambdaSquared_eq_zero_of_support_wlog
Proof state before:
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
d1 d2 : ℕ
h : d = d1.lcm d2
hle : d1 ≤ d2
hyp : ↑d2 ^ 2 ≤ y
⊢ d1 * d2 ≤ d2 * d2
Tactic:
gcongr
Proof state after:
no goals
Theorem: Sieve.lambdaSquared_eq_zero_of_support
Proof state before:
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
⊢ lambdaSquared w d = 0
Tactic:
dsimp only [lambdaSquared]
Proof state after:
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
⊢ (∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then w d1 * w d2 else 0) = 0