internlm/Lean-Github huggingface dataset:
Theorem: SelbergSieve.selbergWeights_diagonalisation
Proof state before:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ ∀ x ∈ P.divisors,
    (∑ x_1 ∈ P.divisors, if l ∣ x_1 ∧ x_1 ∣ x ∧ ↑x ^ 2 ≤ y then g x * S⁻¹ * ↑(μ x_1) else 0) =
      if ↑x ^ 2 ≤ y then (∑ d ∈ P.divisors, if l ∣ d ∧ d ∣ x then ↑(μ d) else 0) * g x * S⁻¹ else 0
Tactic:
intro k _
Proof state after:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
k : ℕ
a✝ : k ∈ P.divisors
⊢ (∑ x ∈ P.divisors, if l ∣ x ∧ x ∣ k ∧ ↑k ^ 2 ≤ y then g k * S⁻¹ * ↑(μ x) else 0) =
    if ↑k ^ 2 ≤ y then (∑ d ∈ P.divisors, if l ∣ d ∧ d ∣ k then ↑(μ d) else 0) * g k * S⁻¹ else 0
Theorem: SelbergSieve.selbergWeights_diagonalisation
Proof state before:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
k : ℕ
a✝ : k ∈ P.divisors
⊢ (∑ x ∈ P.divisors, if l ∣ x ∧ x ∣ k ∧ ↑k ^ 2 ≤ y then g k * S⁻¹ * ↑(μ x) else 0) =
    if ↑k ^ 2 ≤ y then (∑ d ∈ P.divisors, if l ∣ d ∧ d ∣ k then ↑(μ d) else 0) * g k * S⁻¹ else 0
Tactic:
apply symm
Proof state after:
case a
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
k : ℕ
a✝ : k ∈ P.divisors
⊢ (if ↑k ^ 2 ≤ y then (∑ d ∈ P.divisors, if l ∣ d ∧ d ∣ k then ↑(μ d) else 0) * g k * S⁻¹ else 0) =
    ∑ x ∈ P.divisors, if l ∣ x ∧ x ∣ k ∧ ↑k ^ 2 ≤ y then g k * S⁻¹ * ↑(μ x) else 0
Theorem: SelbergSieve.selbergWeights_diagonalisation
Proof state before:
case a
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
k : ℕ
a✝ : k ∈ P.divisors
⊢ (if ↑k ^ 2 ≤ y then (∑ d ∈ P.divisors, if l ∣ d ∧ d ∣ k then ↑(μ d) else 0) * g k * S⁻¹ else 0) =
    ∑ x ∈ P.divisors, if l ∣ x ∧ x ∣ k ∧ ↑k ^ 2 ≤ y then g k * S⁻¹ * ↑(μ x) else 0
Tactic:
rw [← boole_mul, sum_mul, sum_mul, mul_sum, sum_congr rfl]
Proof state after:
case a
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
k : ℕ
a✝ : k ∈ P.divisors
⊢ ∀ x ∈ P.divisors,
    (if ↑k ^ 2 ≤ y then 1 else 0) * ((if l ∣ x ∧ x ∣ k then ↑(μ x) else 0) * g k * S⁻¹) =
      if l ∣ x ∧ x ∣ k ∧ ↑k ^ 2 ≤ y then g k * S⁻¹ * ↑(μ x) else 0
Theorem: SelbergSieve.selbergWeights_diagonalisation
Proof state before:
case a
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
k : ℕ
a✝ : k ∈ P.divisors
⊢ ∀ x ∈ P.divisors,
    (if ↑k ^ 2 ≤ y then 1 else 0) * ((if l ∣ x ∧ x ∣ k then ↑(μ x) else 0) * g k * S⁻¹) =
      if l ∣ x ∧ x ∣ k ∧ ↑k ^ 2 ≤ y then g k * S⁻¹ * ↑(μ x) else 0
Tactic:
intro d _
Proof state after:
case a
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
k : ℕ
a✝¹ : k ∈ P.divisors
d : ℕ
a✝ : d ∈ P.divisors
⊢ (if ↑k ^ 2 ≤ y then 1 else 0) * ((if l ∣ d ∧ d ∣ k then ↑(μ d) else 0) * g k * S⁻¹) =
    if l ∣ d ∧ d ∣ k ∧ ↑k ^ 2 ≤ y then g k * S⁻¹ * ↑(μ d) else 0
Theorem: SelbergSieve.selbergWeights_diagonalisation
Proof state before:
case a
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
k : ℕ
a✝¹ : k ∈ P.divisors
d : ℕ
a✝ : d ∈ P.divisors
⊢ (if ↑k ^ 2 ≤ y then 1 else 0) * ((if l ∣ d ∧ d ∣ k then ↑(μ d) else 0) * g k * S⁻¹) =
    if l ∣ d ∧ d ∣ k ∧ ↑k ^ 2 ≤ y then g k * S⁻¹ * ↑(μ d) else 0
Tactic:
rw [ite_zero_mul, ite_zero_mul, ite_zero_mul, one_mul, ←ite_and]
Proof state after:
case a
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
k : ℕ
a✝¹ : k ∈ P.divisors
d : ℕ
a✝ : d ∈ P.divisors
⊢ (if ↑k ^ 2 ≤ y ∧ l ∣ d ∧ d ∣ k then ↑(μ d) * g k * S⁻¹ else 0) =
    if l ∣ d ∧ d ∣ k ∧ ↑k ^ 2 ≤ y then g k * S⁻¹ * ↑(μ d) else 0
Theorem: SelbergSieve.selbergWeights_diagonalisation
Proof state before:
case a
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
k : ℕ
a✝¹ : k ∈ P.divisors
d : ℕ
a✝ : d ∈ P.divisors
⊢ (if ↑k ^ 2 ≤ y ∧ l ∣ d ∧ d ∣ k then ↑(μ d) * g k * S⁻¹ else 0) =
    if l ∣ d ∧ d ∣ k ∧ ↑k ^ 2 ≤ y then g k * S⁻¹ * ↑(μ d) else 0
Tactic:
apply if_ctx_congr _ _ (fun _ => rfl)
Proof state after:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
k : ℕ
a✝¹ : k ∈ P.divisors
d : ℕ
a✝ : d ∈ P.divisors
⊢ ↑k ^ 2 ≤ y ∧ l ∣ d ∧ d ∣ k ↔ l ∣ d ∧ d ∣ k ∧ ↑k ^ 2 ≤ y

s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
k : ℕ
a✝¹ : k ∈ P.divisors
d : ℕ
a✝ : d ∈ P.divisors
⊢ l ∣ d ∧ d ∣ k ∧ ↑k ^ 2 ≤ y → ↑(μ d) * g k * S⁻¹ = g k * S⁻¹ * ↑(μ d)
Theorem: SelbergSieve.selbergWeights_diagonalisation
Proof state before:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
k : ℕ
a✝¹ : k ∈ P.divisors
d : ℕ
a✝ : d ∈ P.divisors
⊢ l ∣ d ∧ d ∣ k ∧ ↑k ^ 2 ≤ y → ↑(μ d) * g k * S⁻¹ = g k * S⁻¹ * ↑(μ d)
Tactic:
intro _
Proof state after:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
k : ℕ
a✝² : k ∈ P.divisors
d : ℕ
a✝¹ : d ∈ P.divisors
a✝ : l ∣ d ∧ d ∣ k ∧ ↑k ^ 2 ≤ y
⊢ ↑(μ d) * g k * S⁻¹ = g k * S⁻¹ * ↑(μ d)
Theorem: SelbergSieve.selbergWeights_diagonalisation
Proof state before:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
k : ℕ
a✝² : k ∈ P.divisors
d : ℕ
a✝¹ : d ∈ P.divisors
a✝ : l ∣ d ∧ d ∣ k ∧ ↑k ^ 2 ≤ y
⊢ ↑(μ d) * g k * S⁻¹ = g k * S⁻¹ * ↑(μ d)
Tactic:
ring
Proof state after:
no goals
Theorem: SelbergSieve.selbergWeights_diagonalisation
Proof state before:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
k : ℕ
a✝¹ : k ∈ P.divisors
d : ℕ
a✝ : d ∈ P.divisors
⊢ ↑k ^ 2 ≤ y ∧ l ∣ d ∧ d ∣ k ↔ l ∣ d ∧ d ∣ k ∧ ↑k ^ 2 ≤ y
Tactic:
tauto
Proof state after:
no goals
Theorem: SelbergSieve.selbergWeights_diagonalisation
Proof state before:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ (∑ k ∈ P.divisors, if ↑k ^ 2 ≤ y then (∑ d ∈ P.divisors, if l ∣ d ∧ d ∣ k then ↑(μ d) else 0) * g k * S⁻¹ else 0) =
    if ↑l ^ 2 ≤ y then g l * ↑(μ l) * S⁻¹ else 0
Tactic:
rw [Aux.sum_intro (f:=fun _ => if l^2 ≤ y then g l * μ l * S⁻¹ else 0) (divisors P) l hl]
Proof state after:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ (∑ k ∈ P.divisors, if ↑k ^ 2 ≤ y then (∑ d ∈ P.divisors, if l ∣ d ∧ d ∣ k then ↑(μ d) else 0) * g k * S⁻¹ else 0) =
    ∑ k ∈ P.divisors, if k = l then if ↑l ^ 2 ≤ y then g l * ↑(μ l) * S⁻¹ else 0 else 0
Theorem: SelbergSieve.selbergWeights_diagonalisation
Proof state before:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ (∑ k ∈ P.divisors, if ↑k ^ 2 ≤ y then (∑ d ∈ P.divisors, if l ∣ d ∧ d ∣ k then ↑(μ d) else 0) * g k * S⁻¹ else 0) =
    ∑ k ∈ P.divisors, if k = l then if ↑l ^ 2 ≤ y then g l * ↑(μ l) * S⁻¹ else 0 else 0
Tactic:
apply sum_congr rfl
Proof state after:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ ∀ x ∈ P.divisors,
    (if ↑x ^ 2 ≤ y then (∑ d ∈ P.divisors, if l ∣ d ∧ d ∣ x then ↑(μ d) else 0) * g x * S⁻¹ else 0) =
      if x = l then if ↑l ^ 2 ≤ y then g l * ↑(μ l) * S⁻¹ else 0 else 0
Theorem: SelbergSieve.selbergWeights_diagonalisation
Proof state before:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ ∀ x ∈ P.divisors,
    (if ↑x ^ 2 ≤ y then (∑ d ∈ P.divisors, if l ∣ d ∧ d ∣ x then ↑(μ d) else 0) * g x * S⁻¹ else 0) =
      if x = l then if ↑l ^ 2 ≤ y then g l * ↑(μ l) * S⁻¹ else 0 else 0
Tactic:
intro k hk
Proof state after:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
k : ℕ
hk : k ∈ P.divisors
⊢ (if ↑k ^ 2 ≤ y then (∑ d ∈ P.divisors, if l ∣ d ∧ d ∣ k then ↑(μ d) else 0) * g k * S⁻¹ else 0) =
    if k = l then if ↑l ^ 2 ≤ y then g l * ↑(μ l) * S⁻¹ else 0 else 0
Theorem: SelbergSieve.selbergWeights_diagonalisation
Proof state before:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
k : ℕ
hk : k ∈ P.divisors
⊢ (if ↑k ^ 2 ≤ y then (∑ d ∈ P.divisors, if l ∣ d ∧ d ∣ k then ↑(μ d) else 0) * g k * S⁻¹ else 0) =
    if k = l then if ↑l ^ 2 ≤ y then g l * ↑(μ l) * S⁻¹ else 0 else 0
Tactic:
rw [Aux.moebius_inv_dvd_lower_bound_real s.prodPrimes_squarefree l _ (dvd_of_mem_divisors hk),
  ←ite_and, ite_zero_mul, ite_zero_mul, ← ite_and]
Proof state after:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
k : ℕ
hk : k ∈ P.divisors
⊢ (if ↑k ^ 2 ≤ y ∧ l = k then ↑(μ l) * g k * S⁻¹ else 0) = if k = l ∧ ↑l ^ 2 ≤ y then g l * ↑(μ l) * S⁻¹ else 0
Theorem: SelbergSieve.selbergWeights_diagonalisation
Proof state before:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
k : ℕ
hk : k ∈ P.divisors
⊢ (if ↑k ^ 2 ≤ y ∧ l = k then ↑(μ l) * g k * S⁻¹ else 0) = if k = l ∧ ↑l ^ 2 ≤ y then g l * ↑(μ l) * S⁻¹ else 0
Tactic:
apply if_ctx_congr _ _ fun _ => rfl
Proof state after:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
k : ℕ
hk : k ∈ P.divisors
⊢ ↑k ^ 2 ≤ y ∧ l = k ↔ k = l ∧ ↑l ^ 2 ≤ y

s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
k : ℕ
hk : k ∈ P.divisors
⊢ k = l ∧ ↑l ^ 2 ≤ y → ↑(μ l) * g k * S⁻¹ = g l * ↑(μ l) * S⁻¹
Theorem: SelbergSieve.selbergWeights_diagonalisation
Proof state before:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
k : ℕ
hk : k ∈ P.divisors
⊢ ↑k ^ 2 ≤ y ∧ l = k ↔ k = l ∧ ↑l ^ 2 ≤ y

s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
k : ℕ
hk : k ∈ P.divisors
⊢ k = l ∧ ↑l ^ 2 ≤ y → ↑(μ l) * g k * S⁻¹ = g l * ↑(μ l) * S⁻¹
Tactic:
rw [and_comm, eq_comm]
Proof state after:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
k : ℕ
hk : k ∈ P.divisors
⊢ k = l ∧ ↑k ^ 2 ≤ y ↔ k = l ∧ ↑l ^ 2 ≤ y

s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
k : ℕ
hk : k ∈ P.divisors
⊢ k = l ∧ ↑l ^ 2 ≤ y → ↑(μ l) * g k * S⁻¹ = g l * ↑(μ l) * S⁻¹
Theorem: SelbergSieve.selbergWeights_diagonalisation
Proof state before:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
k : ℕ
hk : k ∈ P.divisors
⊢ k = l ∧ ↑k ^ 2 ≤ y ↔ k = l ∧ ↑l ^ 2 ≤ y

s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
k : ℕ
hk : k ∈ P.divisors
⊢ k = l ∧ ↑l ^ 2 ≤ y → ↑(μ l) * g k * S⁻¹ = g l * ↑(μ l) * S⁻¹
Tactic:
apply and_congr_right
Proof state after:
case h
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
k : ℕ
hk : k ∈ P.divisors
⊢ k = l → (↑k ^ 2 ≤ y ↔ ↑l ^ 2 ≤ y)

s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
k : ℕ
hk : k ∈ P.divisors
⊢ k = l ∧ ↑l ^ 2 ≤ y → ↑(μ l) * g k * S⁻¹ = g l * ↑(μ l) * S⁻¹
Theorem: SelbergSieve.selbergWeights_diagonalisation
Proof state before:
case h
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
k : ℕ
hk : k ∈ P.divisors
⊢ k = l → (↑k ^ 2 ≤ y ↔ ↑l ^ 2 ≤ y)

s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
k : ℕ
hk : k ∈ P.divisors
⊢ k = l ∧ ↑l ^ 2 ≤ y → ↑(μ l) * g k * S⁻¹ = g l * ↑(μ l) * S⁻¹
Tactic:
intro heq
Proof state after:
case h
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
k : ℕ
hk : k ∈ P.divisors
heq : k = l
⊢ ↑k ^ 2 ≤ y ↔ ↑l ^ 2 ≤ y

s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
k : ℕ
hk : k ∈ P.divisors
⊢ k = l ∧ ↑l ^ 2 ≤ y → ↑(μ l) * g k * S⁻¹ = g l * ↑(μ l) * S⁻¹
Theorem: SelbergSieve.selbergWeights_diagonalisation
Proof state before:
case h
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
k : ℕ
hk : k ∈ P.divisors
heq : k = l
⊢ ↑k ^ 2 ≤ y ↔ ↑l ^ 2 ≤ y

s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
k : ℕ
hk : k ∈ P.divisors
⊢ k = l ∧ ↑l ^ 2 ≤ y → ↑(μ l) * g k * S⁻¹ = g l * ↑(μ l) * S⁻¹
Tactic:
rw [heq]
Proof state after:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
k : ℕ
hk : k ∈ P.divisors
⊢ k = l ∧ ↑l ^ 2 ≤ y → ↑(μ l) * g k * S⁻¹ = g l * ↑(μ l) * S⁻¹
Theorem: SelbergSieve.selbergWeights_diagonalisation
Proof state before:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
k : ℕ
hk : k ∈ P.divisors
⊢ k = l ∧ ↑l ^ 2 ≤ y → ↑(μ l) * g k * S⁻¹ = g l * ↑(μ l) * S⁻¹
Tactic:
intro h
Proof state after:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
k : ℕ
hk : k ∈ P.divisors
h : k = l ∧ ↑l ^ 2 ≤ y
⊢ ↑(μ l) * g k * S⁻¹ = g l * ↑(μ l) * S⁻¹
Theorem: SelbergSieve.selbergWeights_diagonalisation
Proof state before:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
k : ℕ
hk : k ∈ P.divisors
h : k = l ∧ ↑l ^ 2 ≤ y
⊢ ↑(μ l) * g k * S⁻¹ = g l * ↑(μ l) * S⁻¹
Tactic:
rw[h.1]
Proof state after:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
k : ℕ
hk : k ∈ P.divisors
h : k = l ∧ ↑l ^ 2 ≤ y
⊢ ↑(μ l) * g l * S⁻¹ = g l * ↑(μ l) * S⁻¹
Theorem: SelbergSieve.selbergWeights_diagonalisation
Proof state before:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
k : ℕ
hk : k ∈ P.divisors
h : k = l ∧ ↑l ^ 2 ≤ y
⊢ ↑(μ l) * g l * S⁻¹ = g l * ↑(μ l) * S⁻¹
Tactic:
ring
Proof state after:
no goals
Theorem: SelbergSieve.weight_one_of_selberg
Proof state before:
s : SelbergSieve
⊢ s.selbergWeights 1 = 1
Tactic:
dsimp only [selbergWeights]
Proof state after:
s : SelbergSieve
⊢ (if 1 ∣ P then (ν 1)⁻¹ * g 1 * ↑(μ 1) * S⁻¹ * ∑ m ∈ P.divisors, if (↑1 * ↑m) ^ 2 ≤ y ∧ m.Coprime 1 then g m else 0
    else 0) =
    1
Theorem: SelbergSieve.weight_one_of_selberg
Proof state before:
s : SelbergSieve
⊢ (if 1 ∣ P then (ν 1)⁻¹ * g 1 * ↑(μ 1) * S⁻¹ * ∑ m ∈ P.divisors, if (↑1 * ↑m) ^ 2 ≤ y ∧ m.Coprime 1 then g m else 0
    else 0) =
    1
Tactic:
rw [if_pos (one_dvd P), s.nu_mult.left, s.selbergTerms_mult.left]
Proof state after:
s : SelbergSieve
⊢ (1⁻¹ * 1 * ↑(μ 1) * S⁻¹ * ∑ m ∈ P.divisors, if (↑1 * ↑m) ^ 2 ≤ y ∧ m.Coprime 1 then g m else 0) = 1
Theorem: SelbergSieve.weight_one_of_selberg
Proof state before:
s : SelbergSieve
⊢ (1⁻¹ * 1 * ↑(μ 1) * S⁻¹ * ∑ m ∈ P.divisors, if (↑1 * ↑m) ^ 2 ≤ y ∧ m.Coprime 1 then g m else 0) = 1
Tactic:
simp only [inv_one, mul_one, isUnit_one, IsUnit.squarefree, moebius_apply_of_squarefree,
  cardFactors_one, _root_.pow_zero, Int.cast_one, selbergBoundingSum, cast_pow, one_mul,
  coprime_one_right_eq_true, and_true, cast_one]
Proof state after:
s : SelbergSieve
⊢ ((∑ l ∈ P.divisors, if ↑l ^ 2 ≤ y then g l else 0)⁻¹ * ∑ l ∈ P.divisors, if ↑l ^ 2 ≤ y then g l else 0) = 1
Theorem: SelbergSieve.weight_one_of_selberg
Proof state before:
s : SelbergSieve
⊢ ((∑ l ∈ P.divisors, if ↑l ^ 2 ≤ y then g l else 0)⁻¹ * ∑ l ∈ P.divisors, if ↑l ^ 2 ≤ y then g l else 0) = 1
Tactic:
rw [inv_mul_cancel]
Proof state after:
s : SelbergSieve
⊢ (∑ l ∈ P.divisors, if ↑l ^ 2 ≤ y then g l else 0) ≠ 0
Theorem: SelbergSieve.weight_one_of_selberg
Proof state before:
s : SelbergSieve
⊢ (∑ l ∈ P.divisors, if ↑l ^ 2 ≤ y then g l else 0) ≠ 0
Tactic:
convert s.selbergBoundingSum_ne_zero
Proof state after:
no goals
Theorem: SelbergSieve.selbergμPlus_eq_zero
Proof state before:
s : SelbergSieve
d : ℕ
hd : ¬↑d ≤ y
⊢ s.selbergMuPlus d = 0
Tactic:
apply Sieve.lambdaSquared_eq_zero_of_support _ y _ d hd
Proof state after:
s : SelbergSieve
d : ℕ
hd : ¬↑d ≤ y
⊢ ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → s.selbergWeights d = 0
Theorem: SelbergSieve.selbergμPlus_eq_zero
Proof state before:
s : SelbergSieve
d : ℕ
hd : ¬↑d ≤ y
⊢ ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → s.selbergWeights d = 0
Tactic:
apply s.selbergWeights_eq_zero
Proof state after:
no goals
Theorem: SelbergSieve.mainSum_eq_diag_quad_form
Proof state before:
s : SelbergSieve
⊢ s.mainSum μ⁺ = ∑ l ∈ P.divisors, 1 / g l * (∑ d ∈ P.divisors, if l ∣ d then ν d * s.selbergWeights d else 0) ^ 2
Tactic:
apply lambdaSquared_mainSum_eq_diag_quad_form
Proof state after:
no goals
Theorem: SelbergSieve.moebius_sq_eq_one_of_squarefree
Proof state before:
s : SelbergSieve
l : ℕ
hl : Squarefree l
⊢ μ l ^ 2 = 1
Tactic:
rw [moebius_apply_of_squarefree hl, ← pow_mul, mul_comm, pow_mul, neg_one_sq, one_pow]
Proof state after:
no goals
Theorem: SelbergSieve.abs_moebius_eq_one_of_squarefree
Proof state before:
s : SelbergSieve
l : ℕ
hl : Squarefree l
⊢ |μ l| = 1
Tactic:
simp only [moebius_apply_of_squarefree hl, abs_pow, abs_neg, abs_one, one_pow]
Proof state after:
no goals
Theorem: SelbergSieve.selberg_bound_simple_mainSum
Proof state before:
s : SelbergSieve
⊢ s.mainSum μ⁺ = S⁻¹
Tactic:
rw [mainSum_eq_diag_quad_form]
Proof state after:
s : SelbergSieve
⊢ ∑ l ∈ P.divisors, 1 / g l * (∑ d ∈ P.divisors, if l ∣ d then ν d * s.selbergWeights d else 0) ^ 2 = S⁻¹
Theorem: SelbergSieve.selberg_bound_simple_mainSum
Proof state before:
s : SelbergSieve
⊢ ∑ l ∈ P.divisors, 1 / g l * (∑ d ∈ P.divisors, if l ∣ d then ν d * s.selbergWeights d else 0) ^ 2 = S⁻¹
Tactic:
trans (∑ l in divisors P, (if l ^ 2 ≤ y then g l *  (S⁻¹) ^ 2 else 0))
Proof state after:
s : SelbergSieve
⊢ ∑ l ∈ P.divisors, 1 / g l * (∑ d ∈ P.divisors, if l ∣ d then ν d * s.selbergWeights d else 0) ^ 2 =
    ∑ l ∈ P.divisors, if ↑l ^ 2 ≤ y then g l * S⁻¹ ^ 2 else 0

s : SelbergSieve
⊢ (∑ l ∈ P.divisors, if ↑l ^ 2 ≤ y then g l * S⁻¹ ^ 2 else 0) = S⁻¹
Theorem: SelbergSieve.selberg_bound_simple_mainSum
Proof state before:
s : SelbergSieve
⊢ (∑ l ∈ P.divisors, if ↑l ^ 2 ≤ y then g l * S⁻¹ ^ 2 else 0) = S⁻¹
Tactic:
conv => {lhs; congr; {skip}; {ext i; rw [← ite_zero_mul]}}
Proof state after:
s : SelbergSieve
⊢ ∑ i ∈ P.divisors, (if ↑i ^ 2 ≤ y then g i else 0) * S⁻¹ ^ 2 = S⁻¹
Theorem: SelbergSieve.selberg_bound_simple_mainSum
Proof state before:
s : SelbergSieve
⊢ ∑ i ∈ P.divisors, (if ↑i ^ 2 ≤ y then g i else 0) * S⁻¹ ^ 2 = S⁻¹
Tactic:
dsimp only [selbergBoundingSum]
Proof state after:
s : SelbergSieve
⊢ ∑ i ∈ P.divisors, (if ↑i ^ 2 ≤ y then g i else 0) * (∑ l ∈ P.divisors, if ↑l ^ 2 ≤ y then g l else 0)⁻¹ ^ 2 =
    (∑ l ∈ P.divisors, if ↑l ^ 2 ≤ y then g l else 0)⁻¹
Theorem: SelbergSieve.selberg_bound_simple_mainSum
Proof state before:
s : SelbergSieve
⊢ ∑ i ∈ P.divisors, (if ↑i ^ 2 ≤ y then g i else 0) * (∑ l ∈ P.divisors, if ↑l ^ 2 ≤ y then g l else 0)⁻¹ ^ 2 =
    (∑ l ∈ P.divisors, if ↑l ^ 2 ≤ y then g l else 0)⁻¹
Tactic:
rw [←sum_mul, sq, ←mul_assoc, mul_inv_cancel]
Proof state after:
s : SelbergSieve
⊢ 1 * (∑ l ∈ P.divisors, if ↑l ^ 2 ≤ y then g l else 0)⁻¹ = (∑ l ∈ P.divisors, if ↑l ^ 2 ≤ y then g l else 0)⁻¹

s : SelbergSieve
⊢ (∑ i ∈ P.divisors, if ↑i ^ 2 ≤ y then g i else 0) ≠ 0
Theorem: SelbergSieve.selberg_bound_simple_mainSum
Proof state before:
s : SelbergSieve
⊢ 1 * (∑ l ∈ P.divisors, if ↑l ^ 2 ≤ y then g l else 0)⁻¹ = (∑ l ∈ P.divisors, if ↑l ^ 2 ≤ y then g l else 0)⁻¹

s : SelbergSieve
⊢ (∑ i ∈ P.divisors, if ↑i ^ 2 ≤ y then g i else 0) ≠ 0
Tactic:
ring
Proof state after:
s : SelbergSieve
⊢ (∑ i ∈ P.divisors, if ↑i ^ 2 ≤ y then g i else 0) ≠ 0
Theorem: SelbergSieve.selberg_bound_simple_mainSum
Proof state before:
s : SelbergSieve
⊢ (∑ i ∈ P.divisors, if ↑i ^ 2 ≤ y then g i else 0) ≠ 0
Tactic:
apply _root_.ne_of_gt
Proof state after:
case h
s : SelbergSieve
⊢ 0 < ∑ i ∈ P.divisors, if ↑i ^ 2 ≤ y then g i else 0
Theorem: SelbergSieve.selberg_bound_simple_mainSum
Proof state before:
case h
s : SelbergSieve
⊢ 0 < ∑ i ∈ P.divisors, if ↑i ^ 2 ≤ y then g i else 0
Tactic:
apply selbergBoundingSum_pos
Proof state after:
no goals
Theorem: SelbergSieve.selberg_bound_simple_mainSum
Proof state before:
s : SelbergSieve
⊢ ∑ l ∈ P.divisors, 1 / g l * (∑ d ∈ P.divisors, if l ∣ d then ν d * s.selbergWeights d else 0) ^ 2 =
    ∑ l ∈ P.divisors, if ↑l ^ 2 ≤ y then g l * S⁻¹ ^ 2 else 0
Tactic:
apply sum_congr rfl
Proof state after:
s : SelbergSieve
⊢ ∀ x ∈ P.divisors,
    1 / g x * (∑ d ∈ P.divisors, if x ∣ d then ν d * s.selbergWeights d else 0) ^ 2 =
      if ↑x ^ 2 ≤ y then g x * S⁻¹ ^ 2 else 0
Theorem: SelbergSieve.selberg_bound_simple_mainSum
Proof state before:
s : SelbergSieve
⊢ ∀ x ∈ P.divisors,
    1 / g x * (∑ d ∈ P.divisors, if x ∣ d then ν d * s.selbergWeights d else 0) ^ 2 =
      if ↑x ^ 2 ≤ y then g x * S⁻¹ ^ 2 else 0
Tactic:
intro l hl
Proof state after:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ 1 / g l * (∑ d ∈ P.divisors, if l ∣ d then ν d * s.selbergWeights d else 0) ^ 2 =
    if ↑l ^ 2 ≤ y then g l * S⁻¹ ^ 2 else 0
Theorem: SelbergSieve.selberg_bound_simple_mainSum
Proof state before:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ 1 / g l * (∑ d ∈ P.divisors, if l ∣ d then ν d * s.selbergWeights d else 0) ^ 2 =
    if ↑l ^ 2 ≤ y then g l * S⁻¹ ^ 2 else 0
Tactic:
rw [s.selbergWeights_diagonalisation l hl, ite_pow, zero_pow, mul_ite_zero]
Proof state after:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ (if ↑l ^ 2 ≤ y then 1 / g l * (g l * ↑(μ l) * S⁻¹) ^ 2 else 0) = if ↑l ^ 2 ≤ y then g l * S⁻¹ ^ 2 else 0

s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ 2 ≠ 0
Theorem: SelbergSieve.selberg_bound_simple_mainSum
Proof state before:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ (if ↑l ^ 2 ≤ y then 1 / g l * (g l * ↑(μ l) * S⁻¹) ^ 2 else 0) = if ↑l ^ 2 ≤ y then g l * S⁻¹ ^ 2 else 0

s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ 2 ≠ 0
Tactic:
apply if_congr Iff.rfl _ rfl
Proof state after:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ 1 / g l * (g l * ↑(μ l) * S⁻¹) ^ 2 = g l * S⁻¹ ^ 2

s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ 2 ≠ 0
Theorem: SelbergSieve.selberg_bound_simple_mainSum
Proof state before:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ 1 / g l * (g l * ↑(μ l) * S⁻¹) ^ 2 = g l * S⁻¹ ^ 2

s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ 2 ≠ 0
Tactic:
trans (1/g l * g l * g l * (μ l:ℝ)^2  * (S⁻¹) ^ 2)
Proof state after:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ 1 / g l * (g l * ↑(μ l) * S⁻¹) ^ 2 = 1 / g l * g l * g l * ↑(μ l) ^ 2 * S⁻¹ ^ 2

s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ 1 / g l * g l * g l * ↑(μ l) ^ 2 * S⁻¹ ^ 2 = g l * S⁻¹ ^ 2

s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ 2 ≠ 0
Theorem: SelbergSieve.selberg_bound_simple_mainSum
Proof state before:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ 1 / g l * g l * g l * ↑(μ l) ^ 2 * S⁻¹ ^ 2 = g l * S⁻¹ ^ 2

s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ 2 ≠ 0
Tactic:
norm_cast
Proof state after:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ 1 / g l * g l * g l * ↑(μ l ^ 2) * S⁻¹ ^ 2 = g l * S⁻¹ ^ 2

s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ 2 ≠ 0
Theorem: SelbergSieve.selberg_bound_simple_mainSum
Proof state before:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ 1 / g l * g l * g l * ↑(μ l ^ 2) * S⁻¹ ^ 2 = g l * S⁻¹ ^ 2

s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ 2 ≠ 0
Tactic:
rw [moebius_sq_eq_one_of_squarefree $ s.squarefree_of_mem_divisors_prodPrimes hl]
Proof state after:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ 1 / g l * g l * g l * ↑1 * S⁻¹ ^ 2 = g l * S⁻¹ ^ 2

s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ 2 ≠ 0
Theorem: SelbergSieve.selberg_bound_simple_mainSum
Proof state before:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ 1 / g l * g l * g l * ↑1 * S⁻¹ ^ 2 = g l * S⁻¹ ^ 2

s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ 2 ≠ 0
Tactic:
rw [one_div_mul_cancel $ _root_.ne_of_gt $ s.selbergTerms_pos l $ dvd_of_mem_divisors hl]
Proof state after:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ 1 * g l * ↑1 * S⁻¹ ^ 2 = g l * S⁻¹ ^ 2

s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ 2 ≠ 0
Theorem: SelbergSieve.selberg_bound_simple_mainSum
Proof state before:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ 1 * g l * ↑1 * S⁻¹ ^ 2 = g l * S⁻¹ ^ 2

s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ 2 ≠ 0
Tactic:
ring
Proof state after:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ 2 ≠ 0
Theorem: SelbergSieve.selberg_bound_simple_mainSum
Proof state before:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ 2 ≠ 0
Tactic:
linarith
Proof state after:
no goals
Theorem: SelbergSieve.selberg_bound_simple_mainSum
Proof state before:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ 1 / g l * (g l * ↑(μ l) * S⁻¹) ^ 2 = 1 / g l * g l * g l * ↑(μ l) ^ 2 * S⁻¹ ^ 2
Tactic:
ring
Proof state after:
no goals
Theorem: SelbergSieve.eq_gcd_mul_of_dvd_of_coprime
Proof state before:
s : SelbergSieve
k d m : ℕ
hkd : k ∣ d
hmd : m.Coprime d
hk : k ≠ 0
⊢ k = d.gcd (k * m)
Tactic:
cases' hkd with r hr
Proof state after:
case intro
s : SelbergSieve
k d m : ℕ
hmd : m.Coprime d
hk : k ≠ 0
r : ℕ
hr : d = k * r
⊢ k = d.gcd (k * m)
Theorem: SelbergSieve.eq_gcd_mul_of_dvd_of_coprime
Proof state before:
case intro
s : SelbergSieve
k d m : ℕ
hmd : m.Coprime d
hk : k ≠ 0
r : ℕ
hr : d = k * r
⊢ k = d.gcd (k * m)
Tactic:
have hrdvd : r ∣ d := by use k; rw [mul_comm]; exact hr
Proof state after:
case intro
s : SelbergSieve
k d m : ℕ
hmd : m.Coprime d
hk : k ≠ 0
r : ℕ
hr : d = k * r
hrdvd : r ∣ d
⊢ k = d.gcd (k * m)
Theorem: SelbergSieve.eq_gcd_mul_of_dvd_of_coprime
Proof state before:
case intro
s : SelbergSieve
k d m : ℕ
hmd : m.Coprime d
hk : k ≠ 0
r : ℕ
hr : d = k * r
hrdvd : r ∣ d
⊢ k = d.gcd (k * m)
Tactic:
apply symm
Proof state after:
case intro.a
s : SelbergSieve
k d m : ℕ
hmd : m.Coprime d
hk : k ≠ 0
r : ℕ
hr : d = k * r
hrdvd : r ∣ d
⊢ d.gcd (k * m) = k
Theorem: SelbergSieve.eq_gcd_mul_of_dvd_of_coprime
Proof state before:
case intro.a
s : SelbergSieve
k d m : ℕ
hmd : m.Coprime d
hk : k ≠ 0
r : ℕ
hr : d = k * r
hrdvd : r ∣ d
⊢ d.gcd (k * m) = k
Tactic:
rw [hr, Nat.gcd_mul_left, mul_eq_left₀ hk, Nat.gcd_comm]
Proof state after:
case intro.a
s : SelbergSieve
k d m : ℕ
hmd : m.Coprime d
hk : k ≠ 0
r : ℕ
hr : d = k * r
hrdvd : r ∣ d
⊢ m.gcd r = 1
Theorem: SelbergSieve.eq_gcd_mul_of_dvd_of_coprime
Proof state before:
case intro.a
s : SelbergSieve
k d m : ℕ
hmd : m.Coprime d
hk : k ≠ 0
r : ℕ
hr : d = k * r
hrdvd : r ∣ d
⊢ m.gcd r = 1
Tactic:
apply Coprime.coprime_dvd_right hrdvd hmd
Proof state after:
no goals
Theorem: SelbergSieve.eq_gcd_mul_of_dvd_of_coprime
Proof state before:
s : SelbergSieve
k d m : ℕ
hmd : m.Coprime d
hk : k ≠ 0
r : ℕ
hr : d = k * r
⊢ r ∣ d
Tactic:
use k
Proof state after:
case h
s : SelbergSieve
k d m : ℕ
hmd : m.Coprime d
hk : k ≠ 0
r : ℕ
hr : d = k * r
⊢ d = r * k
Theorem: SelbergSieve.eq_gcd_mul_of_dvd_of_coprime
Proof state before:
case h
s : SelbergSieve
k d m : ℕ
hmd : m.Coprime d
hk : k ≠ 0
r : ℕ
hr : d = k * r
⊢ d = r * k
Tactic:
rw [mul_comm]
Proof state after:
case h
s : SelbergSieve
k d m : ℕ
hmd : m.Coprime d
hk : k ≠ 0
r : ℕ
hr : d = k * r
⊢ d = k * r
Theorem: SelbergSieve.eq_gcd_mul_of_dvd_of_coprime
Proof state before:
case h
s : SelbergSieve
k d m : ℕ
hmd : m.Coprime d
hk : k ≠ 0
r : ℕ
hr : d = k * r
⊢ d = k * r
Tactic:
exact hr
Proof state after:
no goals