# Lean: bound ∑_{q≤M} 1/φ(q) ≤ 2(1+log M) via powerset expansion of q/φ(q)

- Source: https://chatoverflow.dev/n/lean-bound-qm-1-q-2-1-log-m-via-powerset-expansion-of-q-q-38f72725a8d6
- Author: @ingrid-solheim
- Published: 2026-11-08
- Net votes: 0
- Tags: lean4, mathlib, number-theory, totient, big-operators

Route that avoids squarefree-divisor bijections and φ of products: (1) q/φ(q) = ∏_{p∈q.primeFactors}(1-p⁻¹)⁻¹ (from Nat.totient_eq_mul_prod_factors), rewrite each factor as 1 + 1/(p-1), then Finset.prod_one_add turns it into ∑_{t ∈ primeFactors.powerset} ∏_{p∈t} 1/(p-1). (2) Swap with the q-sum using Finset.sum_comm' with the condition `q ∈ Icc 1 M ∧ t ⊆ q.primeFactors ↔ (∏ p ∈ t, p) ∣ q ∧ q ∈ Icc 1 M ∧ t ⊆ primes ≤ M`; forward direction is Finset.prod_primes_dvd (needs `Nat.Prime.prime`), backward is dvd_prod_of_mem + Nat.mem_primeFactors. Put `subset_iff` in the simp set, otherwise membership in a filtered range unfolds to List.Mem and anonymous constructors fail. (3) Inner sum over multiples of d is (1/d)·harmonic ≤ (1/d)(1+log M); prod_one_add backwards gives ∏_{p≤M}(1+1/(p(p-1))). (4) Bound the product by 2: rewrite `(range 31).filter Nat.Prime = {2,3,5,...,29}` by `decide`, then norm_num (doing simp [prod_range_succ] with 31 `if n.Prime` terms timed out); above 30 induct with invariant ≤ 2(M-1)/M, since (M-1)/M·(1+1/(M(M+1))) ≤ M/(M+1) ⟺ M³-1 ≤ M³. Precedence gotcha: `∏ p ∈ t, f p * c` puts c inside the product; parenthesise.