SelbergSieve.selberg_bound_muPlus

theorem selberg_bound_muPlus (n : ℕ) (hn : n ∈ divisors P) :    |μ⁺ n| ≤ (3:ℝ) ^ ω n := by  let f : ℕ → ℕ → ℝ := fun x z : ℕ => if n = x.lcm z then 1 else 0  dsimp only [selbergMuPlus, lambdaSquared]  calc    |∑ d1 ∈ n.divisors, ∑ d2 ∈ n.divisors, if n = d1.lcm d2 then γ d1 * γ d2 else 0| ≤        ∑ d1 ∈ n.divisors, |∑ d2 ∈ n.divisors, if n = d1.lcm d2 then γ d1 * γ d2 else 0| := ?_    _ ≤ ∑ d1 ∈ n.divisors, ∑ d2 ∈ n.divisors, |if n = d1.lcm d2 then γ d1 * γ d2 else 0| := ?_    _ ≤ ∑ d1 ∈ n.divisors, ∑ d2 ∈ n.divisors, f d1 d2 := ?_    _ = (n.divisors ×ˢ n.divisors).sum fun p => f p.fst p.snd := ?_    _ = Finset.card ((n.divisors ×ˢ n.divisors).filter fun p : ℕ × ℕ => n = p.fst.lcm p.snd) := ?_    _ = (3:ℕ) ^ ω n := ?_    _ = (3:ℝ) ^ ω n := ?_  · apply abs_sum_le_sum_abs  · gcongr; apply abs_sum_le_sum_abs  · gcongr with d1 _ d2    rw [apply_ite abs, abs_zero, abs_mul]    simp only [f]    by_cases h : n = d1.lcm d2    · rw [if_pos h, if_pos h]      apply mul_le_one₀ (s.selberg_bound_weights d1) (abs_nonneg <| γ d2)        (s.selberg_bound_weights d2)    rw [if_neg h, if_neg h]  · rw [← Finset.sum_product']  · rw [← sum_filter, Finset.sum_const, smul_one_eq_cast]  · norm_cast    simp [← card_pair_lcm_eq (squarefree_of_mem_divisors_prodPrimes hn), eq_comm]  norm_num