vonMangoldt

formal source

 138/-! ### Von Mangoldt function Λ -/
 139
 140/-- The von Mangoldt function (as an arithmetic function `ℕ → ℝ`). -/
 141noncomputable abbrev vonMangoldt : ArithmeticFunction ℝ := ArithmeticFunction.vonMangoldt
 142
 143@[simp] theorem vonMangoldt_def : vonMangoldt = ArithmeticFunction.vonMangoldt := rfl
 144
 145/-- Λ(p) = log(p) for prime p. -/
 146theorem vonMangoldt_prime {p : ℕ} (hp : Prime p) : vonMangoldt p = Real.log p := by
 147  have hp' : Nat.Prime p := (prime_iff p).1 hp
 148  simp [vonMangoldt, ArithmeticFunction.vonMangoldt_apply_prime hp']
 149
 150/-- Λ(n) = 0 unless n is a prime power. -/
 151theorem vonMangoldt_eq_zero_of_not_prime_pow {n : ℕ} (h : ¬ IsPrimePow n) :
 152    vonMangoldt n = 0 := by
 153  simp [vonMangoldt, ArithmeticFunction.vonMangoldt_eq_zero_iff.mpr h]
 154
 155/-- Λ(p^k) = log(p) for prime p and k ≥ 1. -/
 156theorem vonMangoldt_prime_pow {p k : ℕ} (hp : Prime p) (hk : 0 < k) :
 157    vonMangoldt (p ^ k) = Real.log p := by
 158  have hp' : Nat.Prime p := (prime_iff p).1 hp
 159  have hk' : k ≠ 0 := Nat.pos_iff_ne_zero.mp hk
 160  rw [vonMangoldt, ArithmeticFunction.vonMangoldt_apply_pow hk']
 161  exact vonMangoldt_prime hp
 162
 163/-! ### Multiplicativity -/
 164
 165/-- The Möbius function is multiplicative. -/
 166theorem mobius_isMultiplicative : ArithmeticFunction.IsMultiplicative mobius := by
 167  simp only [mobius]
 168  exact ArithmeticFunction.isMultiplicative_moebius
 169
 170/-! ### Sigma function (sum of divisors) -/
 171