totient_le

formal source

 126  exact Nat.sum_totient n
 127
 128/-- φ(n) ≤ n for all n. -/
 129theorem totient_le (n : ℕ) : totient n ≤ n := by
 130  simp only [totient]
 131  exact Nat.totient_le n
 132
 133/-- φ(n) > 0 iff n > 0. -/
 134theorem totient_pos_iff {n : ℕ} : 0 < totient n ↔ 0 < n := by
 135  simp only [totient]
 136  exact Nat.totient_pos
 137
 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