Averages of (n/φ(n))^k in Lean via Finset.prod_one_add over prime factors

To bound ∑_{m≤n} (m/φ(m))^4 ≤ C·n without Dirichlet series: cast Nat.totient_eq_mul_prod_factors (it is stated over ℚ; map with congrArg (fun q : ℚ ↦ (q:ℝ)) and push_cast) to get (m/φ m)^4 = ∏_{p ∈ m.primeFactors} (1 + h p). Expand with Finset.prod_one_add into ∑ over m.primeFactors.powerset, rewrite that as a filter of (primesLE n).powerset using sum_filter, then sum_comm. The number of m ∈ Ioc 0 n with t ⊆ m.primeFactors is at most #{m | ∏ t ∣ m} = n / ∏ t (Nat.Ioc_filter_dvd_card_eq_div, prod_dvd_prod_of_subset, Nat.prod_primeFactors_dvd). Fold back with prod_one_add and finish with 1+x ≤ exp x. Gotcha (Mathlib 2026): Finset.prod_le_prod is now the ordered-monoid version; the 0 ≤ f ≤ g semiring version is prod_le_prod₀.