sigma_prime

formal source

 206  rw [Finset.sum_insert (by simp [h_ne]), Finset.sum_singleton, add_comm]
 207
 208/-- σ_k(p) = 1 + p^k for prime p. -/
 209theorem sigma_prime {k : ℕ} {p : ℕ} (hp : Prime p) : sigma k p = 1 + p ^ k := by
 210  have hp' : Nat.Prime p := (prime_iff p).1 hp
 211  simp only [sigma_apply, hp'.divisors]
 212  have h_ne : (1 : ℕ) ≠ p := hp'.one_lt.ne'.symm
 213  rw [Finset.sum_insert (by simp [h_ne]), Finset.sum_singleton, one_pow, add_comm]
 214
 215/-! ### Zeta function (constant 1) and Dirichlet convolution -/
 216
 217/-- The arithmetic zeta function ζ (constant 1 on positive integers). -/
 218abbrev zeta : ArithmeticFunction ℕ := ArithmeticFunction.zeta
 219
 220@[simp] theorem zeta_def : zeta = ArithmeticFunction.zeta := rfl
 221
 222/-- ζ(n) = 1 for n ≥ 1. -/
 223theorem zeta_apply {n : ℕ} (hn : n ≠ 0) : zeta n = 1 := by
 224  simp only [zeta, ArithmeticFunction.zeta_apply, hn, ↓reduceIte]
 225
 226/-- ζ(0) = 0. -/
 227theorem zeta_zero : zeta 0 = 0 := by
 228  simp only [zeta, ArithmeticFunction.zeta_apply, ↓reduceIte]
 229
 230/-- ζ is multiplicative. -/
 231theorem zeta_isMultiplicative : ArithmeticFunction.IsMultiplicative zeta := by
 232  simp only [zeta]
 233  exact ArithmeticFunction.isMultiplicative_zeta
 234
 235/-! ### Möbius inversion fundamentals -/
 236
 237/-- The key identity: μ * ζ = ε (the Dirichlet identity).
 238This is the foundation of Möbius inversion. -/
 239theorem moebius_mul_zeta : (mobius : ArithmeticFunction ℤ) * ↑zeta = 1 := by