internlm/Lean-Github huggingface dataset:
Theorem: Sieve.lambdaSquared_mainSum_eq_quad_form
Proof state before:
s : Sieve
w : ℕ → ℝ
⊢ ∑ d ∈ P.divisors, (∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then w d1 * w d2 else 0) * ν d =
    ∑ d1 ∈ P.divisors, ∑ d2 ∈ P.divisors, ν d1 * w d1 * ν d2 * w d2 * (ν (d1.gcd d2))⁻¹
Tactic:
trans (∑ d in divisors P, ∑ d1 in divisors d, ∑ d2 in divisors d,
        if d = d1.lcm d2 then w d1 * w d2 * ν d else 0)
Proof state after:
s : Sieve
w : ℕ → ℝ
⊢ ∑ d ∈ P.divisors, (∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then w d1 * w d2 else 0) * ν d =
    ∑ d ∈ P.divisors, ∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then w d1 * w d2 * ν d else 0

s : Sieve
w : ℕ → ℝ
⊢ (∑ d ∈ P.divisors, ∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then w d1 * w d2 * ν d else 0) =
    ∑ d1 ∈ P.divisors, ∑ d2 ∈ P.divisors, ν d1 * w d1 * ν d2 * w d2 * (ν (d1.gcd d2))⁻¹
Theorem: Sieve.lambdaSquared_mainSum_eq_quad_form
Proof state before:
s : Sieve
w : ℕ → ℝ
⊢ (∑ d ∈ P.divisors, ∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then w d1 * w d2 * ν d else 0) =
    ∑ d1 ∈ P.divisors, ∑ d2 ∈ P.divisors, ν d1 * w d1 * ν d2 * w d2 * (ν (d1.gcd d2))⁻¹
Tactic:
trans (∑ d in divisors P, ∑ d1 in divisors P, ∑ d2 in divisors P,
        if d = d1.lcm d2 then w d1 * w d2 * ν d else 0)
Proof state after:
s : Sieve
w : ℕ → ℝ
⊢ (∑ d ∈ P.divisors, ∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then w d1 * w d2 * ν d else 0) =
    ∑ d ∈ P.divisors, ∑ d1 ∈ P.divisors, ∑ d2 ∈ P.divisors, if d = d1.lcm d2 then w d1 * w d2 * ν d else 0

s : Sieve
w : ℕ → ℝ
⊢ (∑ d ∈ P.divisors, ∑ d1 ∈ P.divisors, ∑ d2 ∈ P.divisors, if d = d1.lcm d2 then w d1 * w d2 * ν d else 0) =
    ∑ d1 ∈ P.divisors, ∑ d2 ∈ P.divisors, ν d1 * w d1 * ν d2 * w d2 * (ν (d1.gcd d2))⁻¹
Theorem: Sieve.lambdaSquared_mainSum_eq_quad_form
Proof state before:
s : Sieve
w : ℕ → ℝ
⊢ (∑ d ∈ P.divisors, ∑ d1 ∈ P.divisors, ∑ d2 ∈ P.divisors, if d = d1.lcm d2 then w d1 * w d2 * ν d else 0) =
    ∑ d1 ∈ P.divisors, ∑ d2 ∈ P.divisors, ν d1 * w d1 * ν d2 * w d2 * (ν (d1.gcd d2))⁻¹
Tactic:
rw [sum_comm, sum_congr rfl]
Proof state after:
s : Sieve
w : ℕ → ℝ
⊢ ∀ x ∈ P.divisors,
    (∑ x_1 ∈ P.divisors, ∑ d2 ∈ P.divisors, if x_1 = x.lcm d2 then w x * w d2 * ν x_1 else 0) =
      ∑ d2 ∈ P.divisors, ν x * w x * ν d2 * w d2 * (ν (x.gcd d2))⁻¹
Theorem: Sieve.lambdaSquared_mainSum_eq_quad_form
Proof state before:
s : Sieve
w : ℕ → ℝ
⊢ ∀ x ∈ P.divisors,
    (∑ x_1 ∈ P.divisors, ∑ d2 ∈ P.divisors, if x_1 = x.lcm d2 then w x * w d2 * ν x_1 else 0) =
      ∑ d2 ∈ P.divisors, ν x * w x * ν d2 * w d2 * (ν (x.gcd d2))⁻¹
Tactic:
intro d1 hd1
Proof state after:
s : Sieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ P.divisors
⊢ (∑ x ∈ P.divisors, ∑ d2 ∈ P.divisors, if x = d1.lcm d2 then w d1 * w d2 * ν x else 0) =
    ∑ d2 ∈ P.divisors, ν d1 * w d1 * ν d2 * w d2 * (ν (d1.gcd d2))⁻¹
Theorem: Sieve.lambdaSquared_mainSum_eq_quad_form
Proof state before:
s : Sieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ P.divisors
⊢ (∑ x ∈ P.divisors, ∑ d2 ∈ P.divisors, if x = d1.lcm d2 then w d1 * w d2 * ν x else 0) =
    ∑ d2 ∈ P.divisors, ν d1 * w d1 * ν d2 * w d2 * (ν (d1.gcd d2))⁻¹
Tactic:
rw [sum_comm, sum_congr rfl]
Proof state after:
s : Sieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ P.divisors
⊢ ∀ x ∈ P.divisors,
    (∑ x_1 ∈ P.divisors, if x_1 = d1.lcm x then w d1 * w x * ν x_1 else 0) = ν d1 * w d1 * ν x * w x * (ν (d1.gcd x))⁻¹
Theorem: Sieve.lambdaSquared_mainSum_eq_quad_form
Proof state before:
s : Sieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ P.divisors
⊢ ∀ x ∈ P.divisors,
    (∑ x_1 ∈ P.divisors, if x_1 = d1.lcm x then w d1 * w x * ν x_1 else 0) = ν d1 * w d1 * ν x * w x * (ν (d1.gcd x))⁻¹
Tactic:
intro d2 hd2
Proof state after:
s : Sieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ P.divisors
d2 : ℕ
hd2 : d2 ∈ P.divisors
⊢ (∑ x ∈ P.divisors, if x = d1.lcm d2 then w d1 * w d2 * ν x else 0) = ν d1 * w d1 * ν d2 * w d2 * (ν (d1.gcd d2))⁻¹
Theorem: Sieve.lambdaSquared_mainSum_eq_quad_form
Proof state before:
s : Sieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ P.divisors
d2 : ℕ
hd2 : d2 ∈ P.divisors
⊢ (∑ x ∈ P.divisors, if x = d1.lcm d2 then w d1 * w d2 * ν x else 0) = ν d1 * w d1 * ν d2 * w d2 * (ν (d1.gcd d2))⁻¹
Tactic:
have h : d1.lcm d2 ∣ P := Nat.lcm_dvd_iff.mpr ⟨dvd_of_mem_divisors hd1, dvd_of_mem_divisors hd2⟩
Proof state after:
s : Sieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ P.divisors
d2 : ℕ
hd2 : d2 ∈ P.divisors
h : d1.lcm d2 ∣ P
⊢ (∑ x ∈ P.divisors, if x = d1.lcm d2 then w d1 * w d2 * ν x else 0) = ν d1 * w d1 * ν d2 * w d2 * (ν (d1.gcd d2))⁻¹
Theorem: Sieve.lambdaSquared_mainSum_eq_quad_form
Proof state before:
s : Sieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ P.divisors
d2 : ℕ
hd2 : d2 ∈ P.divisors
h : d1.lcm d2 ∣ P
⊢ (∑ x ∈ P.divisors, if x = d1.lcm d2 then w d1 * w d2 * ν x else 0) = ν d1 * w d1 * ν d2 * w d2 * (ν (d1.gcd d2))⁻¹
Tactic:
rw [←sum_intro (divisors P) (d1.lcm d2) (mem_divisors.mpr ⟨h, s.prodPrimes_ne_zero⟩ )]
Proof state after:
s : Sieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ P.divisors
d2 : ℕ
hd2 : d2 ∈ P.divisors
h : d1.lcm d2 ∣ P
⊢ w d1 * w d2 * ν (d1.lcm d2) = ν d1 * w d1 * ν d2 * w d2 * (ν (d1.gcd d2))⁻¹
Theorem: Sieve.lambdaSquared_mainSum_eq_quad_form
Proof state before:
s : Sieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ P.divisors
d2 : ℕ
hd2 : d2 ∈ P.divisors
h : d1.lcm d2 ∣ P
⊢ w d1 * w d2 * ν (d1.lcm d2) = ν d1 * w d1 * ν d2 * w d2 * (ν (d1.gcd d2))⁻¹
Tactic:
rw [s.nu_mult.mult_lcm_eq_of_ne_zero]
Proof state after:
s : Sieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ P.divisors
d2 : ℕ
hd2 : d2 ∈ P.divisors
h : d1.lcm d2 ∣ P
⊢ w d1 * w d2 * (ν d1 * ν d2 / ν (d1.gcd d2)) = ν d1 * w d1 * ν d2 * w d2 * (ν (d1.gcd d2))⁻¹

case hf
s : Sieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ P.divisors
d2 : ℕ
hd2 : d2 ∈ P.divisors
h : d1.lcm d2 ∣ P
⊢ ν (d1.gcd d2) ≠ 0
Theorem: Sieve.lambdaSquared_mainSum_eq_quad_form
Proof state before:
s : Sieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ P.divisors
d2 : ℕ
hd2 : d2 ∈ P.divisors
h : d1.lcm d2 ∣ P
⊢ w d1 * w d2 * (ν d1 * ν d2 / ν (d1.gcd d2)) = ν d1 * w d1 * ν d2 * w d2 * (ν (d1.gcd d2))⁻¹

case hf
s : Sieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ P.divisors
d2 : ℕ
hd2 : d2 ∈ P.divisors
h : d1.lcm d2 ∣ P
⊢ ν (d1.gcd d2) ≠ 0
Tactic:
ring
Proof state after:
case hf
s : Sieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ P.divisors
d2 : ℕ
hd2 : d2 ∈ P.divisors
h : d1.lcm d2 ∣ P
⊢ ν (d1.gcd d2) ≠ 0
Theorem: Sieve.lambdaSquared_mainSum_eq_quad_form
Proof state before:
case hf
s : Sieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ P.divisors
d2 : ℕ
hd2 : d2 ∈ P.divisors
h : d1.lcm d2 ∣ P
⊢ ν (d1.gcd d2) ≠ 0
Tactic:
refine _root_.ne_of_gt (s.nu_pos_of_dvd_prodPrimes ?_)
Proof state after:
case hf
s : Sieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ P.divisors
d2 : ℕ
hd2 : d2 ∈ P.divisors
h : d1.lcm d2 ∣ P
⊢ d1.gcd d2 ∣ P
Theorem: Sieve.lambdaSquared_mainSum_eq_quad_form
Proof state before:
case hf
s : Sieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ P.divisors
d2 : ℕ
hd2 : d2 ∈ P.divisors
h : d1.lcm d2 ∣ P
⊢ d1.gcd d2 ∣ P
Tactic:
trans d1
Proof state after:
s : Sieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ P.divisors
d2 : ℕ
hd2 : d2 ∈ P.divisors
h : d1.lcm d2 ∣ P
⊢ d1.gcd d2 ∣ d1

s : Sieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ P.divisors
d2 : ℕ
hd2 : d2 ∈ P.divisors
h : d1.lcm d2 ∣ P
⊢ d1 ∣ P
Theorem: Sieve.lambdaSquared_mainSum_eq_quad_form
Proof state before:
s : Sieve
w : ℕ → ℝ
⊢ ∑ d ∈ P.divisors, (∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then w d1 * w d2 else 0) * ν d =
    ∑ d ∈ P.divisors, ∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then w d1 * w d2 * ν d else 0
Tactic:
rw [sum_congr rfl]
Proof state after:
s : Sieve
w : ℕ → ℝ
⊢ ∀ x ∈ P.divisors,
    (∑ d1 ∈ x.divisors, ∑ d2 ∈ x.divisors, if x = d1.lcm d2 then w d1 * w d2 else 0) * ν x =
      ∑ d1 ∈ x.divisors, ∑ d2 ∈ x.divisors, if x = d1.lcm d2 then w d1 * w d2 * ν x else 0
Theorem: Sieve.lambdaSquared_mainSum_eq_quad_form
Proof state before:
s : Sieve
w : ℕ → ℝ
⊢ ∀ x ∈ P.divisors,
    (∑ d1 ∈ x.divisors, ∑ d2 ∈ x.divisors, if x = d1.lcm d2 then w d1 * w d2 else 0) * ν x =
      ∑ d1 ∈ x.divisors, ∑ d2 ∈ x.divisors, if x = d1.lcm d2 then w d1 * w d2 * ν x else 0
Tactic:
intro d _
Proof state after:
s : Sieve
w : ℕ → ℝ
d : ℕ
a✝ : d ∈ P.divisors
⊢ (∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then w d1 * w d2 else 0) * ν d =
    ∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then w d1 * w d2 * ν d else 0
Theorem: Sieve.lambdaSquared_mainSum_eq_quad_form
Proof state before:
s : Sieve
w : ℕ → ℝ
d : ℕ
a✝ : d ∈ P.divisors
⊢ (∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then w d1 * w d2 else 0) * ν d =
    ∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then w d1 * w d2 * ν d else 0
Tactic:
rw [sum_mul, sum_congr rfl]
Proof state after:
s : Sieve
w : ℕ → ℝ
d : ℕ
a✝ : d ∈ P.divisors
⊢ ∀ x ∈ d.divisors,
    (∑ d2 ∈ d.divisors, if d = x.lcm d2 then w x * w d2 else 0) * ν d =
      ∑ d2 ∈ d.divisors, if d = x.lcm d2 then w x * w d2 * ν d else 0
Theorem: Sieve.lambdaSquared_mainSum_eq_quad_form
Proof state before:
s : Sieve
w : ℕ → ℝ
d : ℕ
a✝ : d ∈ P.divisors
⊢ ∀ x ∈ d.divisors,
    (∑ d2 ∈ d.divisors, if d = x.lcm d2 then w x * w d2 else 0) * ν d =
      ∑ d2 ∈ d.divisors, if d = x.lcm d2 then w x * w d2 * ν d else 0
Tactic:
intro d1 _
Proof state after:
s : Sieve
w : ℕ → ℝ
d : ℕ
a✝¹ : d ∈ P.divisors
d1 : ℕ
a✝ : d1 ∈ d.divisors
⊢ (∑ d2 ∈ d.divisors, if d = d1.lcm d2 then w d1 * w d2 else 0) * ν d =
    ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then w d1 * w d2 * ν d else 0
Theorem: Sieve.lambdaSquared_mainSum_eq_quad_form
Proof state before:
s : Sieve
w : ℕ → ℝ
d : ℕ
a✝¹ : d ∈ P.divisors
d1 : ℕ
a✝ : d1 ∈ d.divisors
⊢ (∑ d2 ∈ d.divisors, if d = d1.lcm d2 then w d1 * w d2 else 0) * ν d =
    ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then w d1 * w d2 * ν d else 0
Tactic:
rw [sum_mul, sum_congr rfl]
Proof state after:
s : Sieve
w : ℕ → ℝ
d : ℕ
a✝¹ : d ∈ P.divisors
d1 : ℕ
a✝ : d1 ∈ d.divisors
⊢ ∀ x ∈ d.divisors, (if d = d1.lcm x then w d1 * w x else 0) * ν d = if d = d1.lcm x then w d1 * w x * ν d else 0
Theorem: Sieve.lambdaSquared_mainSum_eq_quad_form
Proof state before:
s : Sieve
w : ℕ → ℝ
d : ℕ
a✝¹ : d ∈ P.divisors
d1 : ℕ
a✝ : d1 ∈ d.divisors
⊢ ∀ x ∈ d.divisors, (if d = d1.lcm x then w d1 * w x else 0) * ν d = if d = d1.lcm x then w d1 * w x * ν d else 0
Tactic:
intro d2 _
Proof state after:
s : Sieve
w : ℕ → ℝ
d : ℕ
a✝² : d ∈ P.divisors
d1 : ℕ
a✝¹ : d1 ∈ d.divisors
d2 : ℕ
a✝ : d2 ∈ d.divisors
⊢ (if d = d1.lcm d2 then w d1 * w d2 else 0) * ν d = if d = d1.lcm d2 then w d1 * w d2 * ν d else 0
Theorem: Sieve.lambdaSquared_mainSum_eq_quad_form
Proof state before:
s : Sieve
w : ℕ → ℝ
d : ℕ
a✝² : d ∈ P.divisors
d1 : ℕ
a✝¹ : d1 ∈ d.divisors
d2 : ℕ
a✝ : d2 ∈ d.divisors
⊢ (if d = d1.lcm d2 then w d1 * w d2 else 0) * ν d = if d = d1.lcm d2 then w d1 * w d2 * ν d else 0
Tactic:
rw [ite_zero_mul]
Proof state after:
no goals
Theorem: Sieve.lambdaSquared_mainSum_eq_quad_form
Proof state before:
s : Sieve
w : ℕ → ℝ
⊢ (∑ d ∈ P.divisors, ∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then w d1 * w d2 * ν d else 0) =
    ∑ d ∈ P.divisors, ∑ d1 ∈ P.divisors, ∑ d2 ∈ P.divisors, if d = d1.lcm d2 then w d1 * w d2 * ν d else 0
Tactic:
apply conv_lambda_sq_larger_sum
Proof state after:
no goals
Theorem: Sieve.lambdaSquared_mainSum_eq_quad_form
Proof state before:
s : Sieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ P.divisors
d2 : ℕ
hd2 : d2 ∈ P.divisors
h : d1.lcm d2 ∣ P
⊢ d1.gcd d2 ∣ d1
Tactic:
exact Nat.gcd_dvd_left d1 d2
Proof state after:
no goals
Theorem: Sieve.lambdaSquared_mainSum_eq_quad_form
Proof state before:
s : Sieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ P.divisors
d2 : ℕ
hd2 : d2 ∈ P.divisors
h : d1.lcm d2 ∣ P
⊢ d1 ∣ P
Tactic:
exact dvd_of_mem_divisors hd1
Proof state after:
no goals
Theorem: Sieve.lambdaSquared_mainSum_eq_diag_quad_form
Proof state before:
s : Sieve
w : ℕ → ℝ
⊢ s.mainSum (lambdaSquared w) = ∑ l ∈ P.divisors, 1 / g l * (∑ d ∈ P.divisors, if l ∣ d then ν d * w d else 0) ^ 2
Tactic:
rw [s.lambdaSquared_mainSum_eq_quad_form w]
Proof state after:
s : Sieve
w : ℕ → ℝ
⊢ ∑ d1 ∈ P.divisors, ∑ d2 ∈ P.divisors, ν d1 * w d1 * ν d2 * w d2 * (ν (d1.gcd d2))⁻¹ =
    ∑ l ∈ P.divisors, 1 / g l * (∑ d ∈ P.divisors, if l ∣ d then ν d * w d else 0) ^ 2
Theorem: Sieve.lambdaSquared_mainSum_eq_diag_quad_form
Proof state before:
s : Sieve
w : ℕ → ℝ
⊢ ∑ d1 ∈ P.divisors, ∑ d2 ∈ P.divisors, ν d1 * w d1 * ν d2 * w d2 * (ν (d1.gcd d2))⁻¹ =
    ∑ l ∈ P.divisors, 1 / g l * (∑ d ∈ P.divisors, if l ∣ d then ν d * w d else 0) ^ 2
Tactic:
trans (∑ d1 in divisors P, ∑ d2 in divisors P, (∑ l in divisors P,
        if l ∣ d1.gcd d2 then 1 / g l * (ν d1 * w d1) * (ν d2 * w d2) else 0))
Proof state after:
s : Sieve
w : ℕ → ℝ
⊢ ∑ d1 ∈ P.divisors, ∑ d2 ∈ P.divisors, ν d1 * w d1 * ν d2 * w d2 * (ν (d1.gcd d2))⁻¹ =
    ∑ d1 ∈ P.divisors,
      ∑ d2 ∈ P.divisors, ∑ l ∈ P.divisors, if l ∣ d1.gcd d2 then 1 / g l * (ν d1 * w d1) * (ν d2 * w d2) else 0

s : Sieve
w : ℕ → ℝ
⊢ (∑ d1 ∈ P.divisors,
      ∑ d2 ∈ P.divisors, ∑ l ∈ P.divisors, if l ∣ d1.gcd d2 then 1 / g l * (ν d1 * w d1) * (ν d2 * w d2) else 0) =
    ∑ l ∈ P.divisors, 1 / g l * (∑ d ∈ P.divisors, if l ∣ d then ν d * w d else 0) ^ 2
Theorem: Sieve.lambdaSquared_mainSum_eq_diag_quad_form
Proof state before:
s : Sieve
w : ℕ → ℝ
⊢ (∑ d1 ∈ P.divisors,
      ∑ d2 ∈ P.divisors, ∑ l ∈ P.divisors, if l ∣ d1.gcd d2 then 1 / g l * (ν d1 * w d1) * (ν d2 * w d2) else 0) =
    ∑ l ∈ P.divisors, 1 / g l * (∑ d ∈ P.divisors, if l ∣ d then ν d * w d else 0) ^ 2
Tactic:
trans (∑ l in divisors P, ∑ d1 in divisors P, ∑ d2 in divisors P,
      if l ∣ Nat.gcd d1 d2 then 1 / selbergTerms s l * (ν d1 * w d1) * (ν d2 * w d2) else 0)
Proof state after:
s : Sieve
w : ℕ → ℝ
⊢ (∑ d1 ∈ P.divisors,
      ∑ d2 ∈ P.divisors, ∑ l ∈ P.divisors, if l ∣ d1.gcd d2 then 1 / g l * (ν d1 * w d1) * (ν d2 * w d2) else 0) =
    ∑ l ∈ P.divisors,
      ∑ d1 ∈ P.divisors, ∑ d2 ∈ P.divisors, if l ∣ d1.gcd d2 then 1 / g l * (ν d1 * w d1) * (ν d2 * w d2) else 0

s : Sieve
w : ℕ → ℝ
⊢ (∑ l ∈ P.divisors,
      ∑ d1 ∈ P.divisors, ∑ d2 ∈ P.divisors, if l ∣ d1.gcd d2 then 1 / g l * (ν d1 * w d1) * (ν d2 * w d2) else 0) =
    ∑ l ∈ P.divisors, 1 / g l * (∑ d ∈ P.divisors, if l ∣ d then ν d * w d else 0) ^ 2
Theorem: Sieve.lambdaSquared_mainSum_eq_diag_quad_form
Proof state before:
s : Sieve
w : ℕ → ℝ
⊢ (∑ l ∈ P.divisors,
      ∑ d1 ∈ P.divisors, ∑ d2 ∈ P.divisors, if l ∣ d1.gcd d2 then 1 / g l * (ν d1 * w d1) * (ν d2 * w d2) else 0) =
    ∑ l ∈ P.divisors, 1 / g l * (∑ d ∈ P.divisors, if l ∣ d then ν d * w d else 0) ^ 2
Tactic:
apply sum_congr rfl
Proof state after:
s : Sieve
w : ℕ → ℝ
⊢ ∀ x ∈ P.divisors,
    (∑ d1 ∈ P.divisors, ∑ d2 ∈ P.divisors, if x ∣ d1.gcd d2 then 1 / g x * (ν d1 * w d1) * (ν d2 * w d2) else 0) =
      1 / g x * (∑ d ∈ P.divisors, if x ∣ d then ν d * w d else 0) ^ 2
Theorem: Sieve.lambdaSquared_mainSum_eq_diag_quad_form
Proof state before:
s : Sieve
w : ℕ → ℝ
⊢ ∀ x ∈ P.divisors,
    (∑ d1 ∈ P.divisors, ∑ d2 ∈ P.divisors, if x ∣ d1.gcd d2 then 1 / g x * (ν d1 * w d1) * (ν d2 * w d2) else 0) =
      1 / g x * (∑ d ∈ P.divisors, if x ∣ d then ν d * w d else 0) ^ 2
Tactic:
intro l _
Proof state after:
s : Sieve
w : ℕ → ℝ
l : ℕ
a✝ : l ∈ P.divisors
⊢ (∑ d1 ∈ P.divisors, ∑ d2 ∈ P.divisors, if l ∣ d1.gcd d2 then 1 / g l * (ν d1 * w d1) * (ν d2 * w d2) else 0) =
    1 / g l * (∑ d ∈ P.divisors, if l ∣ d then ν d * w d else 0) ^ 2
Theorem: Sieve.lambdaSquared_mainSum_eq_diag_quad_form
Proof state before:
s : Sieve
w : ℕ → ℝ
l : ℕ
a✝ : l ∈ P.divisors
⊢ (∑ d1 ∈ P.divisors, ∑ d2 ∈ P.divisors, if l ∣ d1.gcd d2 then 1 / g l * (ν d1 * w d1) * (ν d2 * w d2) else 0) =
    1 / g l * (∑ d ∈ P.divisors, if l ∣ d then ν d * w d else 0) ^ 2
Tactic:
rw [sq, sum_mul, mul_sum, sum_congr rfl]
Proof state after:
s : Sieve
w : ℕ → ℝ
l : ℕ
a✝ : l ∈ P.divisors
⊢ ∀ x ∈ P.divisors,
    (∑ d2 ∈ P.divisors, if l ∣ x.gcd d2 then 1 / g l * (ν x * w x) * (ν d2 * w d2) else 0) =
      1 / g l * ((if l ∣ x then ν x * w x else 0) * ∑ d ∈ P.divisors, if l ∣ d then ν d * w d else 0)
Theorem: Sieve.lambdaSquared_mainSum_eq_diag_quad_form
Proof state before:
s : Sieve
w : ℕ → ℝ
l : ℕ
a✝ : l ∈ P.divisors
⊢ ∀ x ∈ P.divisors,
    (∑ d2 ∈ P.divisors, if l ∣ x.gcd d2 then 1 / g l * (ν x * w x) * (ν d2 * w d2) else 0) =
      1 / g l * ((if l ∣ x then ν x * w x else 0) * ∑ d ∈ P.divisors, if l ∣ d then ν d * w d else 0)
Tactic:
intro d1 _
Proof state after:
s : Sieve
w : ℕ → ℝ
l : ℕ
a✝¹ : l ∈ P.divisors
d1 : ℕ
a✝ : d1 ∈ P.divisors
⊢ (∑ d2 ∈ P.divisors, if l ∣ d1.gcd d2 then 1 / g l * (ν d1 * w d1) * (ν d2 * w d2) else 0) =
    1 / g l * ((if l ∣ d1 then ν d1 * w d1 else 0) * ∑ d ∈ P.divisors, if l ∣ d then ν d * w d else 0)
Theorem: Sieve.lambdaSquared_mainSum_eq_diag_quad_form
Proof state before:
s : Sieve
w : ℕ → ℝ
l : ℕ
a✝¹ : l ∈ P.divisors
d1 : ℕ
a✝ : d1 ∈ P.divisors
⊢ (∑ d2 ∈ P.divisors, if l ∣ d1.gcd d2 then 1 / g l * (ν d1 * w d1) * (ν d2 * w d2) else 0) =
    1 / g l * ((if l ∣ d1 then ν d1 * w d1 else 0) * ∑ d ∈ P.divisors, if l ∣ d then ν d * w d else 0)
Tactic:
rw [mul_sum, mul_sum, sum_congr rfl]
Proof state after:
s : Sieve
w : ℕ → ℝ
l : ℕ
a✝¹ : l ∈ P.divisors
d1 : ℕ
a✝ : d1 ∈ P.divisors
⊢ ∀ x ∈ P.divisors,
    (if l ∣ d1.gcd x then 1 / g l * (ν d1 * w d1) * (ν x * w x) else 0) =
      1 / g l * ((if l ∣ d1 then ν d1 * w d1 else 0) * if l ∣ x then ν x * w x else 0)
Theorem: Sieve.lambdaSquared_mainSum_eq_diag_quad_form
Proof state before:
s : Sieve
w : ℕ → ℝ
l : ℕ
a✝¹ : l ∈ P.divisors
d1 : ℕ
a✝ : d1 ∈ P.divisors
⊢ ∀ x ∈ P.divisors,
    (if l ∣ d1.gcd x then 1 / g l * (ν d1 * w d1) * (ν x * w x) else 0) =
      1 / g l * ((if l ∣ d1 then ν d1 * w d1 else 0) * if l ∣ x then ν x * w x else 0)
Tactic:
intro d2 _
Proof state after:
s : Sieve
w : ℕ → ℝ
l : ℕ
a✝² : l ∈ P.divisors
d1 : ℕ
a✝¹ : d1 ∈ P.divisors
d2 : ℕ
a✝ : d2 ∈ P.divisors
⊢ (if l ∣ d1.gcd d2 then 1 / g l * (ν d1 * w d1) * (ν d2 * w d2) else 0) =
    1 / g l * ((if l ∣ d1 then ν d1 * w d1 else 0) * if l ∣ d2 then ν d2 * w d2 else 0)
Theorem: Sieve.lambdaSquared_mainSum_eq_diag_quad_form
Proof state before:
s : Sieve
w : ℕ → ℝ
l : ℕ
a✝² : l ∈ P.divisors
d1 : ℕ
a✝¹ : d1 ∈ P.divisors
d2 : ℕ
a✝ : d2 ∈ P.divisors
⊢ (if l ∣ d1.gcd d2 then 1 / g l * (ν d1 * w d1) * (ν d2 * w d2) else 0) =
    1 / g l * ((if l ∣ d1 then ν d1 * w d1 else 0) * if l ∣ d2 then ν d2 * w d2 else 0)
Tactic:
rw [ite_zero_mul_ite_zero, mul_ite_zero]
Proof state after:
s : Sieve
w : ℕ → ℝ
l : ℕ
a✝² : l ∈ P.divisors
d1 : ℕ
a✝¹ : d1 ∈ P.divisors
d2 : ℕ
a✝ : d2 ∈ P.divisors
⊢ (if l ∣ d1.gcd d2 then 1 / g l * (ν d1 * w d1) * (ν d2 * w d2) else 0) =
    if l ∣ d1 ∧ l ∣ d2 then 1 / g l * (ν d1 * w d1 * (ν d2 * w d2)) else 0
Theorem: Sieve.lambdaSquared_mainSum_eq_diag_quad_form
Proof state before:
s : Sieve
w : ℕ → ℝ
l : ℕ
a✝² : l ∈ P.divisors
d1 : ℕ
a✝¹ : d1 ∈ P.divisors
d2 : ℕ
a✝ : d2 ∈ P.divisors
⊢ (if l ∣ d1.gcd d2 then 1 / g l * (ν d1 * w d1) * (ν d2 * w d2) else 0) =
    if l ∣ d1 ∧ l ∣ d2 then 1 / g l * (ν d1 * w d1 * (ν d2 * w d2)) else 0
Tactic:
apply if_congr (Nat.dvd_gcd_iff) _ rfl
Proof state after:
s : Sieve
w : ℕ → ℝ
l : ℕ
a✝² : l ∈ P.divisors
d1 : ℕ
a✝¹ : d1 ∈ P.divisors
d2 : ℕ
a✝ : d2 ∈ P.divisors
⊢ 1 / g l * (ν d1 * w d1) * (ν d2 * w d2) = 1 / g l * (ν d1 * w d1 * (ν d2 * w d2))
Theorem: Sieve.lambdaSquared_mainSum_eq_diag_quad_form
Proof state before:
s : Sieve
w : ℕ → ℝ
l : ℕ
a✝² : l ∈ P.divisors
d1 : ℕ
a✝¹ : d1 ∈ P.divisors
d2 : ℕ
a✝ : d2 ∈ P.divisors
⊢ 1 / g l * (ν d1 * w d1) * (ν d2 * w d2) = 1 / g l * (ν d1 * w d1 * (ν d2 * w d2))
Tactic:
ring
Proof state after:
no goals
Theorem: Sieve.lambdaSquared_mainSum_eq_diag_quad_form
Proof state before:
s : Sieve
w : ℕ → ℝ
⊢ ∑ d1 ∈ P.divisors, ∑ d2 ∈ P.divisors, ν d1 * w d1 * ν d2 * w d2 * (ν (d1.gcd d2))⁻¹ =
    ∑ d1 ∈ P.divisors,
      ∑ d2 ∈ P.divisors, ∑ l ∈ P.divisors, if l ∣ d1.gcd d2 then 1 / g l * (ν d1 * w d1) * (ν d2 * w d2) else 0
Tactic:
apply sum_congr rfl
Proof state after:
s : Sieve
w : ℕ → ℝ
⊢ ∀ x ∈ P.divisors,
    ∑ d2 ∈ P.divisors, ν x * w x * ν d2 * w d2 * (ν (x.gcd d2))⁻¹ =
      ∑ d2 ∈ P.divisors, ∑ l ∈ P.divisors, if l ∣ x.gcd d2 then 1 / g l * (ν x * w x) * (ν d2 * w d2) else 0
Theorem: Sieve.lambdaSquared_mainSum_eq_diag_quad_form
Proof state before:
s : Sieve
w : ℕ → ℝ
⊢ ∀ x ∈ P.divisors,
    ∑ d2 ∈ P.divisors, ν x * w x * ν d2 * w d2 * (ν (x.gcd d2))⁻¹ =
      ∑ d2 ∈ P.divisors, ∑ l ∈ P.divisors, if l ∣ x.gcd d2 then 1 / g l * (ν x * w x) * (ν d2 * w d2) else 0
Tactic:
intro d1 hd1
Proof state after:
s : Sieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ P.divisors
⊢ ∑ d2 ∈ P.divisors, ν d1 * w d1 * ν d2 * w d2 * (ν (d1.gcd d2))⁻¹ =
    ∑ d2 ∈ P.divisors, ∑ l ∈ P.divisors, if l ∣ d1.gcd d2 then 1 / g l * (ν d1 * w d1) * (ν d2 * w d2) else 0
Theorem: Sieve.lambdaSquared_mainSum_eq_diag_quad_form
Proof state before:
s : Sieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ P.divisors
⊢ ∑ d2 ∈ P.divisors, ν d1 * w d1 * ν d2 * w d2 * (ν (d1.gcd d2))⁻¹ =
    ∑ d2 ∈ P.divisors, ∑ l ∈ P.divisors, if l ∣ d1.gcd d2 then 1 / g l * (ν d1 * w d1) * (ν d2 * w d2) else 0
Tactic:
apply sum_congr rfl
Proof state after:
s : Sieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ P.divisors
⊢ ∀ x ∈ P.divisors,
    ν d1 * w d1 * ν x * w x * (ν (d1.gcd x))⁻¹ =
      ∑ l ∈ P.divisors, if l ∣ d1.gcd x then 1 / g l * (ν d1 * w d1) * (ν x * w x) else 0
Theorem: Sieve.lambdaSquared_mainSum_eq_diag_quad_form
Proof state before:
s : Sieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ P.divisors
⊢ ∀ x ∈ P.divisors,
    ν d1 * w d1 * ν x * w x * (ν (d1.gcd x))⁻¹ =
      ∑ l ∈ P.divisors, if l ∣ d1.gcd x then 1 / g l * (ν d1 * w d1) * (ν x * w x) else 0
Tactic:
intro d2 _
Proof state after:
s : Sieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ P.divisors
d2 : ℕ
a✝ : d2 ∈ P.divisors
⊢ ν d1 * w d1 * ν d2 * w d2 * (ν (d1.gcd d2))⁻¹ =
    ∑ l ∈ P.divisors, if l ∣ d1.gcd d2 then 1 / g l * (ν d1 * w d1) * (ν d2 * w d2) else 0
Theorem: Sieve.lambdaSquared_mainSum_eq_diag_quad_form
Proof state before:
s : Sieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ P.divisors
d2 : ℕ
a✝ : d2 ∈ P.divisors
⊢ ν d1 * w d1 * ν d2 * w d2 * (ν (d1.gcd d2))⁻¹ =
    ∑ l ∈ P.divisors, if l ∣ d1.gcd d2 then 1 / g l * (ν d1 * w d1) * (ν d2 * w d2) else 0
Tactic:
have hgcd_dvd: d1.gcd d2 ∣ P := Trans.trans (Nat.gcd_dvd_left d1 d2) (dvd_of_mem_divisors hd1)
Proof state after:
s : Sieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ P.divisors
d2 : ℕ
a✝ : d2 ∈ P.divisors
hgcd_dvd : d1.gcd d2 ∣ P
⊢ ν d1 * w d1 * ν d2 * w d2 * (ν (d1.gcd d2))⁻¹ =
    ∑ l ∈ P.divisors, if l ∣ d1.gcd d2 then 1 / g l * (ν d1 * w d1) * (ν d2 * w d2) else 0
Theorem: Sieve.lambdaSquared_mainSum_eq_diag_quad_form
Proof state before:
s : Sieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ P.divisors
d2 : ℕ
a✝ : d2 ∈ P.divisors
hgcd_dvd : d1.gcd d2 ∣ P
⊢ ν d1 * w d1 * ν d2 * w d2 * (ν (d1.gcd d2))⁻¹ =
    ∑ l ∈ P.divisors, if l ∣ d1.gcd d2 then 1 / g l * (ν d1 * w d1) * (ν d2 * w d2) else 0
Tactic:
rw [s.nu_eq_conv_one_div_selbergTerms _ hgcd_dvd, mul_sum]
Proof state after:
s : Sieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ P.divisors
d2 : ℕ
a✝ : d2 ∈ P.divisors
hgcd_dvd : d1.gcd d2 ∣ P
⊢ (∑ i ∈ P.divisors, ν d1 * w d1 * ν d2 * w d2 * if i ∣ d1.gcd d2 then 1 / g i else 0) =
    ∑ l ∈ P.divisors, if l ∣ d1.gcd d2 then 1 / g l * (ν d1 * w d1) * (ν d2 * w d2) else 0
Theorem: Sieve.lambdaSquared_mainSum_eq_diag_quad_form
Proof state before:
s : Sieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ P.divisors
d2 : ℕ
a✝ : d2 ∈ P.divisors
hgcd_dvd : d1.gcd d2 ∣ P
⊢ (∑ i ∈ P.divisors, ν d1 * w d1 * ν d2 * w d2 * if i ∣ d1.gcd d2 then 1 / g i else 0) =
    ∑ l ∈ P.divisors, if l ∣ d1.gcd d2 then 1 / g l * (ν d1 * w d1) * (ν d2 * w d2) else 0
Tactic:
apply sum_congr rfl
Proof state after:
s : Sieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ P.divisors
d2 : ℕ
a✝ : d2 ∈ P.divisors
hgcd_dvd : d1.gcd d2 ∣ P
⊢ ∀ x ∈ P.divisors,
    (ν d1 * w d1 * ν d2 * w d2 * if x ∣ d1.gcd d2 then 1 / g x else 0) =
      if x ∣ d1.gcd d2 then 1 / g x * (ν d1 * w d1) * (ν d2 * w d2) else 0
Theorem: Sieve.lambdaSquared_mainSum_eq_diag_quad_form
Proof state before:
s : Sieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ P.divisors
d2 : ℕ
a✝ : d2 ∈ P.divisors
hgcd_dvd : d1.gcd d2 ∣ P
⊢ ∀ x ∈ P.divisors,
    (ν d1 * w d1 * ν d2 * w d2 * if x ∣ d1.gcd d2 then 1 / g x else 0) =
      if x ∣ d1.gcd d2 then 1 / g x * (ν d1 * w d1) * (ν d2 * w d2) else 0
Tactic:
intro l _
Proof state after:
s : Sieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ P.divisors
d2 : ℕ
a✝¹ : d2 ∈ P.divisors
hgcd_dvd : d1.gcd d2 ∣ P
l : ℕ
a✝ : l ∈ P.divisors
⊢ (ν d1 * w d1 * ν d2 * w d2 * if l ∣ d1.gcd d2 then 1 / g l else 0) =
    if l ∣ d1.gcd d2 then 1 / g l * (ν d1 * w d1) * (ν d2 * w d2) else 0