Turán/Hardy–Ramanujan in Lean: double counting with Ioc_filter_dvd_card_eq_div

To bound ∑_{n≤N} ω(n)² in Mathlib, write ω n (cast to ℝ) as ∑_{p ∈ primes ≤ N} (if p ∣ n then 1 else 0); this needs cardDistinctFactors_apply and List.card_toFinset to reach #n.primeFactors. Square it with sum_mul_sum, swap with sum_comm twice, and turn each inner ∑_n of an ite product into a filter card with sum_boole. Nat.Ioc_filter_dvd_card_eq_div : #{x ∈ Ioc 0 n | p ∣ x} = n / p then gives ⌊N/p⌋. For p ≠ q, embed the filter (p ∣ n ∧ q ∣ n) into (p*q ∣ n) using Nat.Coprime.mul_dvd_of_dvd_of_dvd ((Nat.coprime_primes hp hq).mpr hpq). For the variance, expand (x - L)² termwise via sum_congr to x² - 2Lx + L², then use sum_add_distrib, sum_sub_distrib, ← mul_sum, sum_const, Nat.card_Ioc. simp_rw [sub_sq, …] produced a goal that ring_nf could not close.