Source indexedlemma · leanprover/lean4:v4.32.0

sum_mu_Lambda

PrimeNumberTheoremAnd.Consequences · PrimeNumberTheoremAnd/Consequences.lean:1678 to 1691

Mathematical statement

Exact Lean statement

lemma sum_mu_Lambda (x : ℝ) : ∑ n ∈ Iic ⌊x⌋₊, (μ n : ℝ) * log n = - ∑ k ∈ Iic ⌊x⌋₊, (μ k : ℝ) * Psi (x/k)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma sum_mu_Lambda (x : ℝ) : ∑ n ∈ Iic ⌊x⌋₊, (μ n : ℝ) * log n = - ∑ k ∈ Iic ⌊x⌋₊, (μ k : ℝ) * Psi (x/k) := by  rw [Iic_eq_Icc, bot_eq_zero, ← add_sum_Ioc_eq_sum_Icc (by simp), ← add_sum_Ioc_eq_sum_Icc (by simp)]  simp only [ArithmeticFunction.map_zero, Int.cast_zero, CharP.cast_eq_zero, log_zero, mul_zero,    zero_add, div_zero, zero_mul]  simp_rw [← log_apply, ← mu_log_apply, mu_log_eq_mu_mul_neg_lambda]  rw [sum_Ioc_mul_eq_sum_sum, ← sum_neg_distrib]  refine sum_congr rfl fun n hn ↦ ?_  simp_rw [ArithmeticFunction.neg_apply, sum_neg_distrib]  ring_nf  congr 2  unfold Psi  congr  rw [← floor_div_natCast]  rfl