MobiusLemma.sum_sq_div_moebius_prime_pow

The function sum_sq_div_moebius is multiplicative (explicitly stated). -/ lemma sum_sq_div_moebius_is_multiplicative_explicit : (sum_sq_div_moebius 1 = 1) ∧ (∀ m n : ℕ, Nat.Coprime m n → sum_sq_div_moebius (m * n) = sum_sq_div_moebius m * sum_sq_div_moebius n) := by have h_map : ∀ m n, m.Coprime n → (Nat.divisors (m * n)).filter (fun d ↦ d ^ 2 ∣ m * n) = image (fun p : ℕ × ℕ ↦ p.1 * p.2) ((Nat.divisors m).filter (fun d ↦ d ^ 2 ∣ m) ×ˢ (Nat.divisors n).filter (fun d ↦ d ^ 2 ∣ n)) := by intro m n hmn ext d simp only [mem_filter, Nat.mem_divisors, ne_eq, mul_eq_zero, not_or, mem_image, mem_product, Prod.exists] refine ⟨fun hd ↦ ?, ?⟩ swap · rintro ⟨a, b, ⟨⟨⟨ha₁, ha₂⟩, ha₃⟩, ⟨⟨hb₁, hb₂⟩, hb₃⟩⟩, rfl⟩ exact ⟨⟨mul_dvd_mul ha₁ hb₁, ha₂, hb₂⟩, by convert! mul_dvd_mul ha₃ hb₃ using 1; ring⟩ obtain ⟨hd_div, hd_sq_div⟩ := hd obtain ⟨a, b, ha, hb, rfl⟩ : ∃ a b : ℕ, a ∣ m ∧ b ∣ n ∧ d = a * b := Exists.imp (by grind) (Nat.dvd_mul.mp hd_div.1) simp_all only [mul_pow, not_false_eq_true, and_true] exact ⟨a, b, ⟨⟨ha, (hmn.coprime_dvd_left ha).pow_left 2 |>.dvd_of_dvd_mul_right <| dvd_of_mul_right_dvd hd_sq_div⟩, hb, (hmn.symm.coprime_dvd_left hb).pow_left 2 |>.dvd_of_dvd_mul_left <| dvd_of_mul_left_dvd hd_sq_div⟩, rfl⟩ have h_sum : ∀ m n : ℕ, Nat.Coprime m n → ∑ d ∈ (Nat.divisors (m * n)).filter (fun d ↦ d ^ 2 ∣ m * n), (moebius d : ℤ) = ∑ a ∈ (Nat.divisors m).filter (fun d ↦ d ^ 2 ∣ m), ∑ b ∈ (Nat.divisors n).filter (fun d ↦ d ^ 2 ∣ n), (moebius (a * b) : ℤ) := by intro m n hmn rw [h_map m n hmn, sum_image, sum_product] intro p hp q hq h_eq have hp1_eq_q1 : p.1 = q.1 := by norm_num at * have hdvd : p.1 ∣ q.1 ∧ q.1 ∣ p.1 := ⟨(hmn.coprime_dvd_left (by grind)).coprime_dvd_right (by grind) |>.dvd_of_dvd_mul_right <| h_eq ▸ dvd_mul_right _ _, (hmn.coprime_dvd_left (by grind)).coprime_dvd_right (by grind) |>.dvd_of_dvd_mul_right <| h_eq.symm ▸ dvd_mul_right _ _⟩ exact Nat.dvd_antisymm hdvd.1 hdvd.2 aesop have h_inner : ∀ m n, m.Coprime n → ∀ a ∈ (Nat.divisors m).filter (fun d ↦ d ^ 2 ∣ m), ∀ b ∈ (Nat.divisors n).filter (fun d ↦ d ^ 2 ∣ n), (moebius (a * b) : ℤ) = (moebius a : ℤ) * (moebius b : ℤ) := by intro m n hmn a ha b hb simp only [moebius, mem_filter, Nat.mem_divisors, ne_eq, Int.reduceNeg, coe_mk, mul_ite, ite_mul, zero_mul, mul_zero] at * split_ifs with h <;> simp_all only [Nat.squarefree_mul_iff, and_self, and_true, ne_eq, Int.reduceNeg, zero_eq_mul, pow_eq_zero_iff', neg_eq_zero, one_ne_zero, cardFactors_eq_zero_iff_eq_zero_or_one, not_or, false_and, or_self, and_false] · rw [← pow_add, cardFactors_mul] · intro a; simp_all [Int.reduceNeg] · intro a; simp_all [Int.reduceNeg] · exact h (hmn.coprime_dvd_left ha.1.1 |>.coprime_dvd_right hb.1.1) dsimp only [sum_sq_div_moebius] exact ⟨by simp [sum_filter], fun m n hmn ↦ by rw [h_sum m n hmn, sum_mul] exact sum_congr rfl fun i hi ↦ by rw [mul_sum]; exact sum_congr rfl fun j hj ↦ h_inner m n hmn i hi j hj⟩

/- For a prime power p^k, sum_sq_div_moebius is 1 if k < 2 and 0 otherwise.