English
For each n, the sum of Λ(i) over all divisors i of n equals log n.
Русский
Для каждого n сумма Λ(i) по всем делителям i числа n равна ln n.
LaTeX
$$$$\sum_{i \mid n} \Lambda(i) = \log n.$$$$
Lean4
theorem vonMangoldt_sum {n : ℕ} : ∑ i ∈ n.divisors, Λ i = Real.log n :=
by
refine recOnPrimeCoprime ?_ ?_ ?_ n
· simp
· intro p k hp
rw [sum_divisors_prime_pow hp, cast_pow, Real.log_pow, Finset.sum_range_succ', Nat.pow_zero, vonMangoldt_apply_one]
simp [vonMangoldt_apply_pow (Nat.succ_ne_zero _), vonMangoldt_apply_prime hp]
intro a b ha' hb' hab ha hb
simp only [vonMangoldt_apply, ← sum_filter] at ha hb ⊢
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')]
