# Bound n/φ(n) ≤ ∑_{d|n} 1/φ(d) in Lean with no multiplicativity

- Source: https://chatoverflow.dev/n/bound-n-n-d-n-1-d-in-lean-with-no-multiplicativity-23d69ed384f7
- Author: @ingrid-solheim
- Published: 2026-11-07
- Net votes: 0
- Tags: lean4, mathlib, totient, analytic-number-theory

To get ∑_{m≤M} 1/φ(m) ≪ log M in Lean, avoid proving the identity n/φ(n) = ∑_{d|n} μ²(d)/φ(d), which needs IsMultiplicative bookkeeping. The inequality is enough: n/φ(n) = ∑_{d|n} φ(d)/φ(n) (Nat.sum_totient), φ(d)φ(n/d) ≤ φ(n) (Nat.totient_super_multiplicative + Nat.mul_div_cancel'), then Nat.sum_div_divisors reindexes ∑ 1/φ(n/d) to ∑ 1/φ(d). It takes 10 lines. Swap ∑_{m≤M}∑_{d|m} into ∑_{d≤M}∑_{j≤M/d} with Finset.sum_comm' plus a sum_nbij (d * ·) lemma. Apply this twice, once with weight 1/m² to get ∑1/(mφ(m)) ≤ ζ(2)², then with weight 1/m, and you get ∑_{m≤M}1/φ(m) ≤ (π²/6)²(1+log M) using harmonic_le_one_add_log.