dsimp only [selbergMuPlus, lambdaSquared]
s : SelbergSieve
n : ℕ
hn : n ∈ P.divisors
f : ℕ → ℕ → ℝ := fun x z => if n = x.lcm z then 1 else 0
⊢ |s.selbergMuPlus n| ≤ 3 ^ ω n
s : SelbergSieve
n : ℕ
hn : n ∈ P.divisors
f : ℕ → ℕ → ℝ := fun x z => if n = x.lcm z then 1 else 0
⊢ |∑ d1 ∈ n.divisors, ∑ d2 ∈ n.divisors, if n = d1.lcm d2 then s.selbergWeights d1 * s.selbergWeights d2 else 0| ≤
    3 ^ ω n