internlm/Lean-Github huggingface dataset:
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
⊢ (∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then w d1 * w d2 else 0) = 0
Tactic:
by_cases hy : 0 ≤ y
Proof state after:
case pos
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
hy : 0 ≤ y
⊢ (∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then w d1 * w d2 else 0) = 0

case neg
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
hy : ¬0 ≤ y
⊢ (∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then w d1 * w d2 else 0) = 0
Theorem: Sieve.lambdaSquared_eq_zero_of_support
Proof state before:
case pos
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
hy : 0 ≤ y
⊢ (∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then w d1 * w d2 else 0) = 0

case neg
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
hy : ¬0 ≤ y
⊢ (∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then w d1 * w d2 else 0) = 0
Tactic:
swap
Proof state after:
case neg
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
hy : ¬0 ≤ y
⊢ (∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then w d1 * w d2 else 0) = 0

case pos
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
hy : 0 ≤ y
⊢ (∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then w d1 * w d2 else 0) = 0
Theorem: Sieve.lambdaSquared_eq_zero_of_support
Proof state before:
case pos
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
hy : 0 ≤ y
⊢ (∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then w d1 * w d2 else 0) = 0
Tactic:
apply sum_eq_zero
Proof state after:
case pos.h
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
hy : 0 ≤ y
⊢ ∀ x ∈ d.divisors, (∑ d2 ∈ d.divisors, if d = x.lcm d2 then w x * w d2 else 0) = 0
Theorem: Sieve.lambdaSquared_eq_zero_of_support
Proof state before:
case pos.h
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
hy : 0 ≤ y
⊢ ∀ x ∈ d.divisors, (∑ d2 ∈ d.divisors, if d = x.lcm d2 then w x * w d2 else 0) = 0
Tactic:
intro d1 _
Proof state after:
case pos.h
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
hy : 0 ≤ y
d1 : ℕ
a✝ : d1 ∈ d.divisors
⊢ (∑ d2 ∈ d.divisors, if d = d1.lcm d2 then w d1 * w d2 else 0) = 0
Theorem: Sieve.lambdaSquared_eq_zero_of_support
Proof state before:
case pos.h
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
hy : 0 ≤ y
d1 : ℕ
a✝ : d1 ∈ d.divisors
⊢ (∑ d2 ∈ d.divisors, if d = d1.lcm d2 then w d1 * w d2 else 0) = 0
Tactic:
apply sum_eq_zero
Proof state after:
case pos.h.h
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
hy : 0 ≤ y
d1 : ℕ
a✝ : d1 ∈ d.divisors
⊢ ∀ x ∈ d.divisors, (if d = d1.lcm x then w d1 * w x else 0) = 0
Theorem: Sieve.lambdaSquared_eq_zero_of_support
Proof state before:
case pos.h.h
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
hy : 0 ≤ y
d1 : ℕ
a✝ : d1 ∈ d.divisors
⊢ ∀ x ∈ d.divisors, (if d = d1.lcm x then w d1 * w x else 0) = 0
Tactic:
intro d2 _
Proof state after:
case pos.h.h
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
hy : 0 ≤ y
d1 : ℕ
a✝¹ : d1 ∈ d.divisors
d2 : ℕ
a✝ : d2 ∈ d.divisors
⊢ (if d = d1.lcm d2 then w d1 * w d2 else 0) = 0
Theorem: Sieve.lambdaSquared_eq_zero_of_support
Proof state before:
case pos.h.h
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
hy : 0 ≤ y
d1 : ℕ
a✝¹ : d1 ∈ d.divisors
d2 : ℕ
a✝ : d2 ∈ d.divisors
⊢ (if d = d1.lcm d2 then w d1 * w d2 else 0) = 0
Tactic:
split_ifs with h
Proof state after:
case pos
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
hy : 0 ≤ y
d1 : ℕ
a✝¹ : d1 ∈ d.divisors
d2 : ℕ
a✝ : d2 ∈ d.divisors
h : d = d1.lcm d2
⊢ w d1 * w d2 = 0

case neg
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
hy : 0 ≤ y
d1 : ℕ
a✝¹ : d1 ∈ d.divisors
d2 : ℕ
a✝ : d2 ∈ d.divisors
h : ¬d = d1.lcm d2
⊢ 0 = 0
Theorem: Sieve.lambdaSquared_eq_zero_of_support
Proof state before:
case pos
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
hy : 0 ≤ y
d1 : ℕ
a✝¹ : d1 ∈ d.divisors
d2 : ℕ
a✝ : d2 ∈ d.divisors
h : d = d1.lcm d2
⊢ w d1 * w d2 = 0

case neg
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
hy : 0 ≤ y
d1 : ℕ
a✝¹ : d1 ∈ d.divisors
d2 : ℕ
a✝ : d2 ∈ d.divisors
h : ¬d = d1.lcm d2
⊢ 0 = 0
Tactic:
swap
Proof state after:
case neg
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
hy : 0 ≤ y
d1 : ℕ
a✝¹ : d1 ∈ d.divisors
d2 : ℕ
a✝ : d2 ∈ d.divisors
h : ¬d = d1.lcm d2
⊢ 0 = 0

case pos
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
hy : 0 ≤ y
d1 : ℕ
a✝¹ : d1 ∈ d.divisors
d2 : ℕ
a✝ : d2 ∈ d.divisors
h : d = d1.lcm d2
⊢ w d1 * w d2 = 0
Theorem: Sieve.lambdaSquared_eq_zero_of_support
Proof state before:
case neg
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
hy : 0 ≤ y
d1 : ℕ
a✝¹ : d1 ∈ d.divisors
d2 : ℕ
a✝ : d2 ∈ d.divisors
h : ¬d = d1.lcm d2
⊢ 0 = 0

case pos
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
hy : 0 ≤ y
d1 : ℕ
a✝¹ : d1 ∈ d.divisors
d2 : ℕ
a✝ : d2 ∈ d.divisors
h : d = d1.lcm d2
⊢ w d1 * w d2 = 0
Tactic:
rfl
Proof state after:
case pos
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
hy : 0 ≤ y
d1 : ℕ
a✝¹ : d1 ∈ d.divisors
d2 : ℕ
a✝ : d2 ∈ d.divisors
h : d = d1.lcm d2
⊢ w d1 * w d2 = 0
Theorem: Sieve.lambdaSquared_eq_zero_of_support
Proof state before:
case pos
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
hy : 0 ≤ y
d1 : ℕ
a✝¹ : d1 ∈ d.divisors
d2 : ℕ
a✝ : d2 ∈ d.divisors
h : d = d1.lcm d2
⊢ w d1 * w d2 = 0
Tactic:
rcases Nat.le_or_le d1 d2 with hle | hle
Proof state after:
case pos.inl
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
hy : 0 ≤ y
d1 : ℕ
a✝¹ : d1 ∈ d.divisors
d2 : ℕ
a✝ : d2 ∈ d.divisors
h : d = d1.lcm d2
hle : d1 ≤ d2
⊢ w d1 * w d2 = 0

case pos.inr
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
hy : 0 ≤ y
d1 : ℕ
a✝¹ : d1 ∈ d.divisors
d2 : ℕ
a✝ : d2 ∈ d.divisors
h : d = d1.lcm d2
hle : d2 ≤ d1
⊢ w d1 * w d2 = 0
Theorem: Sieve.lambdaSquared_eq_zero_of_support
Proof state before:
case neg
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
hy : ¬0 ≤ y
⊢ (∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then w d1 * w d2 else 0) = 0
Tactic:
push_neg at hd hy
Proof state after:
case neg
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : y < ↑d
hy : y < 0
⊢ (∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then w d1 * w d2 else 0) = 0
Theorem: Sieve.lambdaSquared_eq_zero_of_support
Proof state before:
case neg
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : y < ↑d
hy : y < 0
⊢ (∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then w d1 * w d2 else 0) = 0
Tactic:
have : ∀ d' : ℕ, w d' = 0 := by
  intro d'; apply hw
  have : (0:ℝ) ≤ (d') ^ 2 := by norm_num
  linarith
Proof state after:
case neg
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : y < ↑d
hy : y < 0
this : ∀ (d' : ℕ), w d' = 0
⊢ (∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then w d1 * w d2 else 0) = 0
Theorem: Sieve.lambdaSquared_eq_zero_of_support
Proof state before:
case neg
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : y < ↑d
hy : y < 0
this : ∀ (d' : ℕ), w d' = 0
⊢ (∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then w d1 * w d2 else 0) = 0
Tactic:
apply sum_eq_zero
Proof state after:
case neg.h
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : y < ↑d
hy : y < 0
this : ∀ (d' : ℕ), w d' = 0
⊢ ∀ x ∈ d.divisors, (∑ d2 ∈ d.divisors, if d = x.lcm d2 then w x * w d2 else 0) = 0
Theorem: Sieve.lambdaSquared_eq_zero_of_support
Proof state before:
case neg.h
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : y < ↑d
hy : y < 0
this : ∀ (d' : ℕ), w d' = 0
⊢ ∀ x ∈ d.divisors, (∑ d2 ∈ d.divisors, if d = x.lcm d2 then w x * w d2 else 0) = 0
Tactic:
intro d1 _
Proof state after:
case neg.h
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : y < ↑d
hy : y < 0
this : ∀ (d' : ℕ), w d' = 0
d1 : ℕ
a✝ : d1 ∈ d.divisors
⊢ (∑ d2 ∈ d.divisors, if d = d1.lcm d2 then w d1 * w d2 else 0) = 0
Theorem: Sieve.lambdaSquared_eq_zero_of_support
Proof state before:
case neg.h
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : y < ↑d
hy : y < 0
this : ∀ (d' : ℕ), w d' = 0
d1 : ℕ
a✝ : d1 ∈ d.divisors
⊢ (∑ d2 ∈ d.divisors, if d = d1.lcm d2 then w d1 * w d2 else 0) = 0
Tactic:
apply sum_eq_zero
Proof state after:
case neg.h.h
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : y < ↑d
hy : y < 0
this : ∀ (d' : ℕ), w d' = 0
d1 : ℕ
a✝ : d1 ∈ d.divisors
⊢ ∀ x ∈ d.divisors, (if d = d1.lcm x then w d1 * w x else 0) = 0
Theorem: Sieve.lambdaSquared_eq_zero_of_support
Proof state before:
case neg.h.h
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : y < ↑d
hy : y < 0
this : ∀ (d' : ℕ), w d' = 0
d1 : ℕ
a✝ : d1 ∈ d.divisors
⊢ ∀ x ∈ d.divisors, (if d = d1.lcm x then w d1 * w x else 0) = 0
Tactic:
intro d2 _
Proof state after:
case neg.h.h
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : y < ↑d
hy : y < 0
this : ∀ (d' : ℕ), w d' = 0
d1 : ℕ
a✝¹ : d1 ∈ d.divisors
d2 : ℕ
a✝ : d2 ∈ d.divisors
⊢ (if d = d1.lcm d2 then w d1 * w d2 else 0) = 0
Theorem: Sieve.lambdaSquared_eq_zero_of_support
Proof state before:
case neg.h.h
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : y < ↑d
hy : y < 0
this : ∀ (d' : ℕ), w d' = 0
d1 : ℕ
a✝¹ : d1 ∈ d.divisors
d2 : ℕ
a✝ : d2 ∈ d.divisors
⊢ (if d = d1.lcm d2 then w d1 * w d2 else 0) = 0
Tactic:
rw [this d1, this d2]
Proof state after:
case neg.h.h
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : y < ↑d
hy : y < 0
this : ∀ (d' : ℕ), w d' = 0
d1 : ℕ
a✝¹ : d1 ∈ d.divisors
d2 : ℕ
a✝ : d2 ∈ d.divisors
⊢ (if d = d1.lcm d2 then 0 * 0 else 0) = 0
Theorem: Sieve.lambdaSquared_eq_zero_of_support
Proof state before:
case neg.h.h
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : y < ↑d
hy : y < 0
this : ∀ (d' : ℕ), w d' = 0
d1 : ℕ
a✝¹ : d1 ∈ d.divisors
d2 : ℕ
a✝ : d2 ∈ d.divisors
⊢ (if d = d1.lcm d2 then 0 * 0 else 0) = 0
Tactic:
simp only [ite_self, eq_self_iff_true, MulZeroClass.mul_zero]
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 : y < ↑d
hy : y < 0
⊢ ∀ (d' : ℕ), w d' = 0
Tactic:
intro d'
Proof state after:
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : y < ↑d
hy : y < 0
d' : ℕ
⊢ w d' = 0
Theorem: Sieve.lambdaSquared_eq_zero_of_support
Proof state before:
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : y < ↑d
hy : y < 0
d' : ℕ
⊢ w d' = 0
Tactic:
apply hw
Proof state after:
case a
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : y < ↑d
hy : y < 0
d' : ℕ
⊢ ¬↑d' ^ 2 ≤ y
Theorem: Sieve.lambdaSquared_eq_zero_of_support
Proof state before:
case a
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : y < ↑d
hy : y < 0
d' : ℕ
⊢ ¬↑d' ^ 2 ≤ y
Tactic:
have : (0:ℝ) ≤ (d') ^ 2 := by norm_num
Proof state after:
case a
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : y < ↑d
hy : y < 0
d' : ℕ
this : 0 ≤ ↑d' ^ 2
⊢ ¬↑d' ^ 2 ≤ y
Theorem: Sieve.lambdaSquared_eq_zero_of_support
Proof state before:
case a
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : y < ↑d
hy : y < 0
d' : ℕ
this : 0 ≤ ↑d' ^ 2
⊢ ¬↑d' ^ 2 ≤ y
Tactic:
linarith
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 : y < ↑d
hy : y < 0
d' : ℕ
⊢ 0 ≤ ↑d' ^ 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: Sieve.lambdaSquared_eq_zero_of_support
Proof state before:
case pos.inl
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
hy : 0 ≤ y
d1 : ℕ
a✝¹ : d1 ∈ d.divisors
d2 : ℕ
a✝ : d2 ∈ d.divisors
h : d = d1.lcm d2
hle : d1 ≤ d2
⊢ w d1 * w d2 = 0
Tactic:
apply lambdaSquared_eq_zero_of_support_wlog hw hd d1 d2 h hle
Proof state after:
no goals
Theorem: Sieve.lambdaSquared_eq_zero_of_support
Proof state before:
case pos.inr
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
hy : 0 ≤ y
d1 : ℕ
a✝¹ : d1 ∈ d.divisors
d2 : ℕ
a✝ : d2 ∈ d.divisors
h : d = d1.lcm d2
hle : d2 ≤ d1
⊢ w d1 * w d2 = 0
Tactic:
rw[mul_comm]
Proof state after:
case pos.inr
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
hy : 0 ≤ y
d1 : ℕ
a✝¹ : d1 ∈ d.divisors
d2 : ℕ
a✝ : d2 ∈ d.divisors
h : d = d1.lcm d2
hle : d2 ≤ d1
⊢ w d2 * w d1 = 0
Theorem: Sieve.lambdaSquared_eq_zero_of_support
Proof state before:
case pos.inr
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
hy : 0 ≤ y
d1 : ℕ
a✝¹ : d1 ∈ d.divisors
d2 : ℕ
a✝ : d2 ∈ d.divisors
h : d = d1.lcm d2
hle : d2 ≤ d1
⊢ w d2 * w d1 = 0
Tactic:
apply lambdaSquared_eq_zero_of_support_wlog hw hd d2 d1 (Nat.lcm_comm d1 d2 ▸ h) hle
Proof state after:
no goals
Theorem: Sieve.upperMoebius_of_lambda_sq
Proof state before:
s : Sieve
weights : ℕ → ℝ
hw : weights 1 = 1
⊢ UpperMoebius (lambdaSquared weights)
Tactic:
dsimp [UpperMoebius, lambdaSquared]
Proof state after:
s : Sieve
weights : ℕ → ℝ
hw : weights 1 = 1
⊢ ∀ (n : ℕ),
    (if n = 1 then 1 else 0) ≤
      ∑ d ∈ n.divisors, ∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then weights d1 * weights d2 else 0
Theorem: Sieve.upperMoebius_of_lambda_sq
Proof state before:
s : Sieve
weights : ℕ → ℝ
hw : weights 1 = 1
⊢ ∀ (n : ℕ),
    (if n = 1 then 1 else 0) ≤
      ∑ d ∈ n.divisors, ∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then weights d1 * weights d2 else 0
Tactic:
intro n
Proof state after:
s : Sieve
weights : ℕ → ℝ
hw : weights 1 = 1
n : ℕ
⊢ (if n = 1 then 1 else 0) ≤
    ∑ d ∈ n.divisors, ∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then weights d1 * weights d2 else 0
Theorem: Sieve.upperMoebius_of_lambda_sq
Proof state before:
s : Sieve
weights : ℕ → ℝ
hw : weights 1 = 1
n : ℕ
⊢ (if n = 1 then 1 else 0) ≤
    ∑ d ∈ n.divisors, ∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then weights d1 * weights d2 else 0
Tactic:
have h_sq :
  (∑ d in n.divisors, ∑ d1 in d.divisors, ∑ d2 in d.divisors,
    if d = Nat.lcm d1 d2 then weights d1 * weights d2 else 0) =
    (∑ d in n.divisors, weights d) ^ 2 := by
  rw [sq, mul_sum, conv_lambda_sq_larger_sum _ n, sum_comm]
  apply sum_congr rfl; intro d1 hd1
  rw [sum_mul, sum_comm]
  apply sum_congr rfl; intro d2 hd2
  rw [←Aux.sum_intro]
  ring
  rw [mem_divisors, Nat.lcm_dvd_iff]
  exact ⟨⟨dvd_of_mem_divisors hd1, dvd_of_mem_divisors hd2⟩, (mem_divisors.mp hd1).2⟩
Proof state after:
s : Sieve
weights : ℕ → ℝ
hw : weights 1 = 1
n : ℕ
h_sq :
  (∑ d ∈ n.divisors, ∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then weights d1 * weights d2 else 0) =
    (∑ d ∈ n.divisors, weights d) ^ 2
⊢ (if n = 1 then 1 else 0) ≤
    ∑ d ∈ n.divisors, ∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then weights d1 * weights d2 else 0
Theorem: Sieve.upperMoebius_of_lambda_sq
Proof state before:
s : Sieve
weights : ℕ → ℝ
hw : weights 1 = 1
n : ℕ
h_sq :
  (∑ d ∈ n.divisors, ∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then weights d1 * weights d2 else 0) =
    (∑ d ∈ n.divisors, weights d) ^ 2
⊢ (if n = 1 then 1 else 0) ≤
    ∑ d ∈ n.divisors, ∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then weights d1 * weights d2 else 0
Tactic:
rw [h_sq]
Proof state after:
s : Sieve
weights : ℕ → ℝ
hw : weights 1 = 1
n : ℕ
h_sq :
  (∑ d ∈ n.divisors, ∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then weights d1 * weights d2 else 0) =
    (∑ d ∈ n.divisors, weights d) ^ 2
⊢ (if n = 1 then 1 else 0) ≤ (∑ d ∈ n.divisors, weights d) ^ 2
Theorem: Sieve.upperMoebius_of_lambda_sq
Proof state before:
s : Sieve
weights : ℕ → ℝ
hw : weights 1 = 1
n : ℕ
h_sq :
  (∑ d ∈ n.divisors, ∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then weights d1 * weights d2 else 0) =
    (∑ d ∈ n.divisors, weights d) ^ 2
⊢ (if n = 1 then 1 else 0) ≤ (∑ d ∈ n.divisors, weights d) ^ 2
Tactic:
split_ifs with hn
Proof state after:
case pos
s : Sieve
weights : ℕ → ℝ
hw : weights 1 = 1
n : ℕ
h_sq :
  (∑ d ∈ n.divisors, ∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then weights d1 * weights d2 else 0) =
    (∑ d ∈ n.divisors, weights d) ^ 2
hn : n = 1
⊢ 1 ≤ (∑ d ∈ n.divisors, weights d) ^ 2

case neg
s : Sieve
weights : ℕ → ℝ
hw : weights 1 = 1
n : ℕ
h_sq :
  (∑ d ∈ n.divisors, ∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then weights d1 * weights d2 else 0) =
    (∑ d ∈ n.divisors, weights d) ^ 2
hn : ¬n = 1
⊢ 0 ≤ (∑ d ∈ n.divisors, weights d) ^ 2
Theorem: Sieve.upperMoebius_of_lambda_sq
Proof state before:
s : Sieve
weights : ℕ → ℝ
hw : weights 1 = 1
n : ℕ
⊢ (∑ d ∈ n.divisors, ∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then weights d1 * weights d2 else 0) =
    (∑ d ∈ n.divisors, weights d) ^ 2
Tactic:
rw [sq, mul_sum, conv_lambda_sq_larger_sum _ n, sum_comm]
Proof state after:
s : Sieve
weights : ℕ → ℝ
hw : weights 1 = 1
n : ℕ
⊢ (∑ y ∈ n.divisors, ∑ x ∈ n.divisors, ∑ d2 ∈ n.divisors, if x = y.lcm d2 then weights y * weights d2 else 0) =
    ∑ i ∈ n.divisors, (∑ d ∈ n.divisors, weights d) * weights i
Theorem: Sieve.upperMoebius_of_lambda_sq
Proof state before:
s : Sieve
weights : ℕ → ℝ
hw : weights 1 = 1
n : ℕ
⊢ (∑ y ∈ n.divisors, ∑ x ∈ n.divisors, ∑ d2 ∈ n.divisors, if x = y.lcm d2 then weights y * weights d2 else 0) =
    ∑ i ∈ n.divisors, (∑ d ∈ n.divisors, weights d) * weights i
Tactic:
apply sum_congr rfl
Proof state after:
s : Sieve
weights : ℕ → ℝ
hw : weights 1 = 1
n : ℕ
⊢ ∀ x ∈ n.divisors,
    (∑ x_1 ∈ n.divisors, ∑ d2 ∈ n.divisors, if x_1 = x.lcm d2 then weights x * weights d2 else 0) =
      (∑ d ∈ n.divisors, weights d) * weights x
Theorem: Sieve.upperMoebius_of_lambda_sq
Proof state before:
s : Sieve
weights : ℕ → ℝ
hw : weights 1 = 1
n : ℕ
⊢ ∀ x ∈ n.divisors,
    (∑ x_1 ∈ n.divisors, ∑ d2 ∈ n.divisors, if x_1 = x.lcm d2 then weights x * weights d2 else 0) =
      (∑ d ∈ n.divisors, weights d) * weights x
Tactic:
intro d1 hd1
Proof state after:
s : Sieve
weights : ℕ → ℝ
hw : weights 1 = 1
n d1 : ℕ
hd1 : d1 ∈ n.divisors
⊢ (∑ x ∈ n.divisors, ∑ d2 ∈ n.divisors, if x = d1.lcm d2 then weights d1 * weights d2 else 0) =
    (∑ d ∈ n.divisors, weights d) * weights d1
Theorem: Sieve.upperMoebius_of_lambda_sq
Proof state before:
s : Sieve
weights : ℕ → ℝ
hw : weights 1 = 1
n d1 : ℕ
hd1 : d1 ∈ n.divisors
⊢ (∑ x ∈ n.divisors, ∑ d2 ∈ n.divisors, if x = d1.lcm d2 then weights d1 * weights d2 else 0) =
    (∑ d ∈ n.divisors, weights d) * weights d1
Tactic:
rw [sum_mul, sum_comm]
Proof state after:
s : Sieve
weights : ℕ → ℝ
hw : weights 1 = 1
n d1 : ℕ
hd1 : d1 ∈ n.divisors
⊢ (∑ y ∈ n.divisors, ∑ x ∈ n.divisors, if x = d1.lcm y then weights d1 * weights y else 0) =
    ∑ i ∈ n.divisors, weights i * weights d1
Theorem: Sieve.upperMoebius_of_lambda_sq
Proof state before:
s : Sieve
weights : ℕ → ℝ
hw : weights 1 = 1
n d1 : ℕ
hd1 : d1 ∈ n.divisors
⊢ (∑ y ∈ n.divisors, ∑ x ∈ n.divisors, if x = d1.lcm y then weights d1 * weights y else 0) =
    ∑ i ∈ n.divisors, weights i * weights d1
Tactic:
apply sum_congr rfl
Proof state after:
s : Sieve
weights : ℕ → ℝ
hw : weights 1 = 1
n d1 : ℕ
hd1 : d1 ∈ n.divisors
⊢ ∀ x ∈ n.divisors, (∑ x_1 ∈ n.divisors, if x_1 = d1.lcm x then weights d1 * weights x else 0) = weights x * weights d1
Theorem: Sieve.upperMoebius_of_lambda_sq
Proof state before:
s : Sieve
weights : ℕ → ℝ
hw : weights 1 = 1
n d1 : ℕ
hd1 : d1 ∈ n.divisors
⊢ ∀ x ∈ n.divisors, (∑ x_1 ∈ n.divisors, if x_1 = d1.lcm x then weights d1 * weights x else 0) = weights x * weights d1
Tactic:
intro d2 hd2
Proof state after:
s : Sieve
weights : ℕ → ℝ
hw : weights 1 = 1
n d1 : ℕ
hd1 : d1 ∈ n.divisors
d2 : ℕ
hd2 : d2 ∈ n.divisors
⊢ (∑ x ∈ n.divisors, if x = d1.lcm d2 then weights d1 * weights d2 else 0) = weights d2 * weights d1
Theorem: Sieve.upperMoebius_of_lambda_sq
Proof state before:
s : Sieve
weights : ℕ → ℝ
hw : weights 1 = 1
n d1 : ℕ
hd1 : d1 ∈ n.divisors
d2 : ℕ
hd2 : d2 ∈ n.divisors
⊢ (∑ x ∈ n.divisors, if x = d1.lcm d2 then weights d1 * weights d2 else 0) = weights d2 * weights d1
Tactic:
rw [←Aux.sum_intro]
Proof state after:
s : Sieve
weights : ℕ → ℝ
hw : weights 1 = 1
n d1 : ℕ
hd1 : d1 ∈ n.divisors
d2 : ℕ
hd2 : d2 ∈ n.divisors
⊢ weights d1 * weights d2 = weights d2 * weights d1

case hd
s : Sieve
weights : ℕ → ℝ
hw : weights 1 = 1
n d1 : ℕ
hd1 : d1 ∈ n.divisors
d2 : ℕ
hd2 : d2 ∈ n.divisors
⊢ d1.lcm d2 ∈ n.divisors
Theorem: Sieve.upperMoebius_of_lambda_sq
Proof state before:
s : Sieve
weights : ℕ → ℝ
hw : weights 1 = 1
n d1 : ℕ
hd1 : d1 ∈ n.divisors
d2 : ℕ
hd2 : d2 ∈ n.divisors
⊢ weights d1 * weights d2 = weights d2 * weights d1

case hd
s : Sieve
weights : ℕ → ℝ
hw : weights 1 = 1
n d1 : ℕ
hd1 : d1 ∈ n.divisors
d2 : ℕ
hd2 : d2 ∈ n.divisors
⊢ d1.lcm d2 ∈ n.divisors
Tactic:
ring
Proof state after:
case hd
s : Sieve
weights : ℕ → ℝ
hw : weights 1 = 1
n d1 : ℕ
hd1 : d1 ∈ n.divisors
d2 : ℕ
hd2 : d2 ∈ n.divisors
⊢ d1.lcm d2 ∈ n.divisors
Theorem: Sieve.upperMoebius_of_lambda_sq
Proof state before:
case hd
s : Sieve
weights : ℕ → ℝ
hw : weights 1 = 1
n d1 : ℕ
hd1 : d1 ∈ n.divisors
d2 : ℕ
hd2 : d2 ∈ n.divisors
⊢ d1.lcm d2 ∈ n.divisors
Tactic:
rw [mem_divisors, Nat.lcm_dvd_iff]
Proof state after:
case hd
s : Sieve
weights : ℕ → ℝ
hw : weights 1 = 1
n d1 : ℕ
hd1 : d1 ∈ n.divisors
d2 : ℕ
hd2 : d2 ∈ n.divisors
⊢ (d1 ∣ n ∧ d2 ∣ n) ∧ n ≠ 0
Theorem: Sieve.upperMoebius_of_lambda_sq
Proof state before:
case hd
s : Sieve
weights : ℕ → ℝ
hw : weights 1 = 1
n d1 : ℕ
hd1 : d1 ∈ n.divisors
d2 : ℕ
hd2 : d2 ∈ n.divisors
⊢ (d1 ∣ n ∧ d2 ∣ n) ∧ n ≠ 0
Tactic:
exact ⟨⟨dvd_of_mem_divisors hd1, dvd_of_mem_divisors hd2⟩, (mem_divisors.mp hd1).2⟩
Proof state after:
no goals
Theorem: Sieve.upperMoebius_of_lambda_sq
Proof state before:
case pos
s : Sieve
weights : ℕ → ℝ
hw : weights 1 = 1
n : ℕ
h_sq :
  (∑ d ∈ n.divisors, ∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then weights d1 * weights d2 else 0) =
    (∑ d ∈ n.divisors, weights d) ^ 2
hn : n = 1
⊢ 1 ≤ (∑ d ∈ n.divisors, weights d) ^ 2
Tactic:
rw [hn]
Proof state after:
case pos
s : Sieve
weights : ℕ → ℝ
hw : weights 1 = 1
n : ℕ
h_sq :
  (∑ d ∈ n.divisors, ∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then weights d1 * weights d2 else 0) =
    (∑ d ∈ n.divisors, weights d) ^ 2
hn : n = 1
⊢ 1 ≤ (∑ d ∈ divisors 1, weights d) ^ 2
Theorem: Sieve.upperMoebius_of_lambda_sq
Proof state before:
case pos
s : Sieve
weights : ℕ → ℝ
hw : weights 1 = 1
n : ℕ
h_sq :
  (∑ d ∈ n.divisors, ∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then weights d1 * weights d2 else 0) =
    (∑ d ∈ n.divisors, weights d) ^ 2
hn : n = 1
⊢ 1 ≤ (∑ d ∈ divisors 1, weights d) ^ 2
Tactic:
simp [hw]
Proof state after:
no goals
Theorem: Sieve.upperMoebius_of_lambda_sq
Proof state before:
case neg
s : Sieve
weights : ℕ → ℝ
hw : weights 1 = 1
n : ℕ
h_sq :
  (∑ d ∈ n.divisors, ∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then weights d1 * weights d2 else 0) =
    (∑ d ∈ n.divisors, weights d) ^ 2
hn : ¬n = 1
⊢ 0 ≤ (∑ d ∈ n.divisors, weights d) ^ 2
Tactic:
apply sq_nonneg
Proof state after:
no goals
Theorem: Sieve.lambdaSquared_mainSum_eq_quad_form
Proof state before:
s : Sieve
w : ℕ → ℝ
⊢ s.mainSum (lambdaSquared w) = ∑ d1 ∈ P.divisors, ∑ d2 ∈ P.divisors, ν d1 * w d1 * ν d2 * w d2 * (ν (d1.gcd d2))⁻¹
Tactic:
dsimp only [mainSum, lambdaSquared]
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 =
    ∑ d1 ∈ P.divisors, ∑ d2 ∈ P.divisors, ν d1 * w d1 * ν d2 * w d2 * (ν (d1.gcd d2))⁻¹