Source indexedtheorem · leanprover/lean4:v4.32.0

Mertens.sum_mangoldt_div_log_eq_log_log

PrimeNumberTheoremAnd.IEANTN.Mertens · PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1933 to 1950

Mathematical statement

Exact Lean statement

@[blueprint
  "Mertens-second-theorem-mangoldt-weak"
  (title := "Mertens' second theorem (weak von Mangoldt form)")
  (statement := /-- For any $x \geq 2$, one has
$$ \sum_{n \leq x} \frac{\Lambda(n)}{n \log n} = \log \log x + O(1). $$
-/)
  (proof := /-- Immediate from previous two corollaries.
  -/)
  (discussion := 1321)]
theorem sum_mangoldt_div_log_eq_log_log : ∃ C, ∀ x, 2 ≤ x →
    |∑ d ∈ Ioc 0 ⌊ x ⌋₊, (Λ d) / (d * log d) - log (log x)| ≤ C

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

@[blueprint  "Mertens-second-theorem-mangoldt-weak"  (title := "Mertens' second theorem (weak von Mangoldt form)")  (statement := /-- For any $x \geq 2$, one has$$ \sum_{n \leq x} \frac{\Lambda(n)}{n \log n} = \log \log x + O(1). $$-/)  (proof := /-- Immediate from previous two corollaries.  -/)  (discussion := 1321)]theorem sum_mangoldt_div_log_eq_log_log : ∃ C, ∀ x, 2 ≤ x →    |∑ d ∈ Ioc 0 ⌊ x ⌋₊, (Λ d) / (d * log d) - log (log x)| ≤ C := by    use (log 4 + 6)/log 2 + |eulerMascheroniConstant|    intro x hx    rw [sum_mangoldt_div_log_eq]    calc      _ = |E₂Λ x + eulerMascheroniConstant| := by ring_nf      _ ≤ (log 4 + 6)/log x + |eulerMascheroniConstant| := by grw [abs_add_le, E₂Λ.abs_le hx]      _ ≤ _ := by gcongr