[GOAL]
⊢ (fun n => Real.log ↑n) 0 = 0
[PROOFSTEP]
simp
[GOAL]
⊢ ↑Λ 1 = 0
[PROOFSTEP]
simp [vonMangoldt_apply]
[GOAL]
n : ℕ
⊢ 0 ≤ ↑Λ n
[PROOFSTEP]
rw [vonMangoldt_apply]
[GOAL]
n : ℕ
⊢ 0 ≤ if IsPrimePow n then Real.log ↑(minFac n) else 0
[PROOFSTEP]
split_ifs
[GOAL]
case pos
n : ℕ
h✝ : IsPrimePow n
⊢ 0 ≤ Real.log ↑(minFac n)
[PROOFSTEP]
exact Real.log_nonneg (one_le_cast.2 (Nat.minFac_pos n))
[GOAL]
case neg
n : ℕ
h✝ : ¬IsPrimePow n
⊢ 0 ≤ 0
[PROOFSTEP]
rfl
[GOAL]
n k : ℕ
hk : k ≠ 0
⊢ ↑Λ (n ^ k) = ↑Λ n
[PROOFSTEP]
simp only [vonMangoldt_apply, isPrimePow_pow_iff hk, pow_minFac hk]
[GOAL]
p : ℕ
hp : Prime p
⊢ ↑Λ p = Real.log ↑p
[PROOFSTEP]
rw [vonMangoldt_apply, Prime.minFac_eq hp, if_pos hp.prime.isPrimePow]
[GOAL]
n : ℕ
⊢ ↑Λ n ≠ 0 ↔ IsPrimePow n
[PROOFSTEP]
rcases eq_or_ne n 1 with (rfl | hn)
[GOAL]
case inl
⊢ ↑Λ 1 ≠ 0 ↔ IsPrimePow 1
[PROOFSTEP]
simp [not_isPrimePow_one]
[GOAL]
case inr
n : ℕ
hn : n ≠ 1
⊢ ↑Λ n ≠ 0 ↔ IsPrimePow n
[PROOFSTEP]
exact (Real.log_pos (one_lt_cast.2 (minFac_prime hn).one_lt)).ne'.ite_ne_right_iff
[GOAL]
n : ℕ
⊢ ∑ i in divisors n, ↑Λ i = Real.log ↑n
[PROOFSTEP]
refine' recOnPrimeCoprime _ _ _ n
[GOAL]
case refine'_1
n : ℕ
⊢ ∑ i in divisors 0, ↑Λ i = Real.log ↑0
[PROOFSTEP]
simp
[GOAL]
case refine'_2
n : ℕ
⊢ ∀ (p n : ℕ), Prime p → ∑ i in divisors (p ^ n), ↑Λ i = Real.log ↑(p ^ n)
[PROOFSTEP]
intro p k hp
[GOAL]
case refine'_2
n p k : ℕ
hp : Prime p
⊢ ∑ i in divisors (p ^ k), ↑Λ i = Real.log ↑(p ^ k)
[PROOFSTEP]
rw [sum_divisors_prime_pow hp, cast_pow, Real.log_pow, Finset.sum_range_succ', pow_zero, vonMangoldt_apply_one]
[GOAL]
case refine'_2
n p k : ℕ
hp : Prime p
⊢ ∑ k in range k, ↑Λ (p ^ (k + 1)) + 0 = ↑k * Real.log ↑p
[PROOFSTEP]
simp [vonMangoldt_apply_pow (Nat.succ_ne_zero _), vonMangoldt_apply_prime hp]
[GOAL]
case refine'_3
n : ℕ
⊢ ∀ (a b : ℕ),
    1 < a →
      1 < b →
        coprime a b →
          ∑ i in divisors a, ↑Λ i = Real.log ↑a →
            ∑ i in divisors b, ↑Λ i = Real.log ↑b → ∑ i in divisors (a * b), ↑Λ i = Real.log ↑(a * b)
[PROOFSTEP]
intro a b ha' hb' hab ha hb
[GOAL]
case refine'_3
n a b : ℕ
ha' : 1 < a
hb' : 1 < b
hab : coprime a b
ha : ∑ i in divisors a, ↑Λ i = Real.log ↑a
hb : ∑ i in divisors b, ↑Λ i = Real.log ↑b
⊢ ∑ i in divisors (a * b), ↑Λ i = Real.log ↑(a * b)
[PROOFSTEP]
simp only [vonMangoldt_apply, ← sum_filter] at ha hb ⊢
[GOAL]
case refine'_3
n a b : ℕ
ha' : 1 < a
hb' : 1 < b
hab : coprime a b
ha : ∑ a in filter (fun a => IsPrimePow a) (divisors a), Real.log ↑(minFac a) = Real.log ↑a
hb : ∑ a in filter (fun a => IsPrimePow a) (divisors b), Real.log ↑(minFac a) = Real.log ↑b
⊢ ∑ a in filter (fun a => IsPrimePow a) (divisors (a * b)), Real.log ↑(minFac a) = Real.log ↑(a * b)
[PROOFSTEP]
rw [mul_divisors_filter_prime_pow hab, filter_union, sum_union (disjoint_divisors_filter_isPrimePow hab), ha, hb,
  Nat.cast_mul, Real.log_mul (cast_ne_zero.2 (pos_of_gt ha').ne') (cast_ne_zero.2 (pos_of_gt hb').ne')]
[GOAL]
⊢ Λ * ↑ζ = log
[PROOFSTEP]
ext n
[GOAL]
case h
n : ℕ
⊢ ↑(Λ * ↑ζ) n = ↑log n
[PROOFSTEP]
rw [coe_mul_zeta_apply, vonMangoldt_sum]
[GOAL]
case h
n : ℕ
⊢ Real.log ↑n = ↑log n
[PROOFSTEP]
rfl
[GOAL]
⊢ ↑ζ * Λ = log
[PROOFSTEP]
rw [mul_comm]
[GOAL]
⊢ Λ * ↑ζ = log
[PROOFSTEP]
simp
[GOAL]
⊢ log * ↑μ = Λ
[PROOFSTEP]
rw [← vonMangoldt_mul_zeta, mul_assoc, coe_zeta_mul_coe_moebius, mul_one]
[GOAL]
⊢ ↑μ * log = Λ
[PROOFSTEP]
rw [mul_comm]
[GOAL]
⊢ log * ↑μ = Λ
[PROOFSTEP]
simp
[GOAL]
n : ℕ
⊢ ∑ d in divisors n, ↑(↑μ d) * ↑log d = -↑Λ n
[PROOFSTEP]
simp only [← log_mul_moebius_eq_vonMangoldt, mul_comm log, mul_apply, log_apply, intCoe_apply, ← Finset.sum_neg_distrib,
  neg_mul_eq_mul_neg]
[GOAL]
n : ℕ
⊢ ∑ x in divisors n, ↑(↑μ x) * Real.log ↑x = ∑ x in divisorsAntidiagonal n, ↑(↑μ x.fst) * -Real.log ↑x.snd
[PROOFSTEP]
rw [sum_divisorsAntidiagonal fun i j => (μ i : ℝ) * -Real.log j]
[GOAL]
n : ℕ
⊢ ∑ x in divisors n, ↑(↑μ x) * Real.log ↑x = ∑ i in divisors n, ↑(↑μ i) * -Real.log ↑(n / i)
[PROOFSTEP]
have :
  (∑ i : ℕ in n.divisors, (μ i : ℝ) * -Real.log (n / i : ℕ)) =
    ∑ i : ℕ in n.divisors, ((μ i : ℝ) * Real.log i - μ i * Real.log n) :=
  by
  apply sum_congr rfl
  simp only [and_imp, Int.cast_eq_zero, mul_eq_mul_left_iff, Ne.def, neg_inj, mem_divisors]
  intro m mn hn
  have : (m : ℝ) ≠ 0 := by
    rw [cast_ne_zero]
    rintro rfl
    exact hn (by simpa using mn)
  rw [Nat.cast_div mn this, Real.log_div (cast_ne_zero.2 hn) this, neg_sub, mul_sub]
[GOAL]
n : ℕ
⊢ ∑ i in divisors n, ↑(↑μ i) * -Real.log ↑(n / i) = ∑ i in divisors n, (↑(↑μ i) * Real.log ↑i - ↑(↑μ i) * Real.log ↑n)
[PROOFSTEP]
apply sum_congr rfl
[GOAL]
n : ℕ
⊢ ∀ (x : ℕ), x ∈ divisors n → ↑(↑μ x) * -Real.log ↑(n / x) = ↑(↑μ x) * Real.log ↑x - ↑(↑μ x) * Real.log ↑n
[PROOFSTEP]
simp only [and_imp, Int.cast_eq_zero, mul_eq_mul_left_iff, Ne.def, neg_inj, mem_divisors]
[GOAL]
n : ℕ
⊢ ∀ (x : ℕ), x ∣ n → ¬n = 0 → ↑(↑μ x) * -Real.log ↑(n / x) = ↑(↑μ x) * Real.log ↑x - ↑(↑μ x) * Real.log ↑n
[PROOFSTEP]
intro m mn hn
[GOAL]
n m : ℕ
mn : m ∣ n
hn : ¬n = 0
⊢ ↑(↑μ m) * -Real.log ↑(n / m) = ↑(↑μ m) * Real.log ↑m - ↑(↑μ m) * Real.log ↑n
[PROOFSTEP]
have : (m : ℝ) ≠ 0 := by
  rw [cast_ne_zero]
  rintro rfl
  exact hn (by simpa using mn)
[GOAL]
n m : ℕ
mn : m ∣ n
hn : ¬n = 0
⊢ ↑m ≠ 0
[PROOFSTEP]
rw [cast_ne_zero]
[GOAL]
n m : ℕ
mn : m ∣ n
hn : ¬n = 0
⊢ m ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
n : ℕ
hn : ¬n = 0
mn : 0 ∣ n
⊢ False
[PROOFSTEP]
exact hn (by simpa using mn)
[GOAL]
n : ℕ
hn : ¬n = 0
mn : 0 ∣ n
⊢ n = 0
[PROOFSTEP]
simpa using mn
[GOAL]
n m : ℕ
mn : m ∣ n
hn : ¬n = 0
this : ↑m ≠ 0
⊢ ↑(↑μ m) * -Real.log ↑(n / m) = ↑(↑μ m) * Real.log ↑m - ↑(↑μ m) * Real.log ↑n
[PROOFSTEP]
rw [Nat.cast_div mn this, Real.log_div (cast_ne_zero.2 hn) this, neg_sub, mul_sub]
[GOAL]
n : ℕ
this :
  ∑ i in divisors n, ↑(↑μ i) * -Real.log ↑(n / i) = ∑ i in divisors n, (↑(↑μ i) * Real.log ↑i - ↑(↑μ i) * Real.log ↑n)
⊢ ∑ x in divisors n, ↑(↑μ x) * Real.log ↑x = ∑ i in divisors n, ↑(↑μ i) * -Real.log ↑(n / i)
[PROOFSTEP]
rw [this, sum_sub_distrib, ← sum_mul, ← Int.cast_sum, ← coe_mul_zeta_apply, eq_comm, sub_eq_self, moebius_mul_coe_zeta]
[GOAL]
n : ℕ
this :
  ∑ i in divisors n, ↑(↑μ i) * -Real.log ↑(n / i) = ∑ i in divisors n, (↑(↑μ i) * Real.log ↑i - ↑(↑μ i) * Real.log ↑n)
⊢ ↑(↑1 n) * Real.log ↑n = 0
[PROOFSTEP]
rcases eq_or_ne n 1 with (hn | hn)
[GOAL]
case inl
n : ℕ
this :
  ∑ i in divisors n, ↑(↑μ i) * -Real.log ↑(n / i) = ∑ i in divisors n, (↑(↑μ i) * Real.log ↑i - ↑(↑μ i) * Real.log ↑n)
hn : n = 1
⊢ ↑(↑1 n) * Real.log ↑n = 0
[PROOFSTEP]
simp [hn]
[GOAL]
case inr
n : ℕ
this :
  ∑ i in divisors n, ↑(↑μ i) * -Real.log ↑(n / i) = ∑ i in divisors n, (↑(↑μ i) * Real.log ↑i - ↑(↑μ i) * Real.log ↑n)
hn : n ≠ 1
⊢ ↑(↑1 n) * Real.log ↑n = 0
[PROOFSTEP]
simp [hn]
[GOAL]
⊢ ↑Λ 0 ≤ Real.log ↑0
[PROOFSTEP]
simp
[GOAL]
n : ℕ
⊢ ↑Λ (n + 1) ≤ Real.log ↑(n + 1)
[PROOFSTEP]
rw [← vonMangoldt_sum]
[GOAL]
n : ℕ
⊢ ↑Λ (n + 1) ≤ ∑ i in divisors (n + 1), ↑Λ i
[PROOFSTEP]
exact single_le_sum (by exact fun _ _ => vonMangoldt_nonneg) (mem_divisors_self _ n.succ_ne_zero)
[GOAL]
n : ℕ
⊢ ∀ (i : ℕ), i ∈ divisors (n + 1) → 0 ≤ ↑Λ i
[PROOFSTEP]
exact fun _ _ => vonMangoldt_nonneg
