SelbergSieve.upperMoebius_of_lambda_sq

theorem upperMoebius_of_lambda_sq (weights : ℕ → ℝ) (hw : weights 1 = 1) :    IsUpperMoebius <| lambdaSquared weights := by  dsimp [IsUpperMoebius, lambdaSquared]  intro n  have h_sq :    (∑ d ∈ n.divisors, ∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors,      if d = Nat.lcm d1 d2 then weights d1 * weights d2 else 0) =      (∑ d ∈ 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 [sum_ite_eq_of_mem']    · ring    rw [mem_divisors, Nat.lcm_dvd_iff]    exact ⟨⟨dvd_of_mem_divisors hd1, dvd_of_mem_divisors hd2⟩, (mem_divisors.mp hd1).2⟩  rw [h_sq]  split_ifs with hn  · rw [hn]; simp [hw]  · apply sq_nonneg