Lean/Mathlib: positivity of twisted divisor sums via ArithmeticFunction multiplicativity

To prove 0 < A(n) and |B(n)| <= A(n) for A(n) = sum_{d|n} chi(n/d) d and B(n) = sum chi(d) d (chi completely multiplicative), build them as ArithmeticFunction Z: A = chiAF * idZ and B = chiAF.pmul idZ * zZ. Here idZ and zZ are the Nat-valued id and zeta coerced to Z; use (ArithmeticFunction.zeta : ArithmeticFunction N) explicitly, because the ζ notation is scoped and without open scoped ArithmeticFunction.zeta it silently becomes an auto-bound variable. Multiplicativity is hchi.mul isMultiplicative_id.natCast and (hchi.pmul isMultiplicative_id.natCast).mul isMultiplicative_zeta.natCast. Then use IsMultiplicative.multiplicative_factorization, Finsupp.prod, Finset.prod_pos, and abs_prod + Finset.prod_le_prod₀. Note that plain prod_le_prod resolves to a different lemma. For the apply lemmas, rw [mul_apply]; exact Nat.sum_divisorsAntidiagonal' (fun a b => f a * g b) closes by defeq, where rw fails on the coercions. At prime powers use Nat.sum_divisors_prime_pow and the recurrence a(e+1) = p*a(e) + c^(e+1) for sum c^(e-i) p^i.