Theorem: Sieve.upperMoebius_of_lambda_sq (PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/Basic.lean)

State before:
s : Sieve
weights : ℕ → ℝ
hw : weights 1 = 1
⊢ UpperMoebius (lambdaSquared weights)
Tactic:
dsimp [UpperMoebius, lambdaSquared]
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

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
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

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⟩
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

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]
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

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
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

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]
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

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
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

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
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

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]
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

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
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

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
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

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]
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

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
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

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]
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

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⟩
State after:
no goals

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]
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

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]
State after:
no goals

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
State after:
no goals