Source indexedtheorem · leanprover/lean4:v4.32.0

chebyshev_asymptotic

PrimeNumberTheoremAnd.Consequences · PrimeNumberTheoremAnd/Consequences.lean:162 to 185

Mathematical statement

Exact Lean statement

@[blueprint "chebyshev-asymptotic"
  (title := "chebyshev-asymptotic")
  (statement := /--
  One has
  $$ \sum_{p \leq x} \log p = x + o(x).$$
  -/)
  (proof := /--
  From the prime number theorem we already have
  $$ \sum_{n \leq x} \Lambda(n) = x + o(x)$$
  so it suffices to show that
  $$ \sum_{j \geq 2} \sum_{p^j \leq x} \log p = o(x).$$
  Only the terms with $j \leq \log x / \log 2$ contribute, and each $j$ contributes at most
  $\sqrt{x} \log x$ to the sum, so the left-hand side is $O( \sqrt{x} \log^2 x ) = o(x)$ as
  required.
  -/)]
theorem chebyshev_asymptotic : θ ~[atTop] id

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

@[blueprint "chebyshev-asymptotic"  (title := "chebyshev-asymptotic")  (statement := /--  One has  $$ \sum_{p \leq x} \log p = x + o(x).$$  -/)  (proof := /--  From the prime number theorem we already have  $$ \sum_{n \leq x} \Lambda(n) = x + o(x)$$  so it suffices to show that  $$ \sum_{j \geq 2} \sum_{p^j \leq x} \log p = o(x).$$  Only the terms with $j \leq \log x / \log 2$ contribute, and each $j$ contributes at most  $\sqrt{x} \log x$ to the sum, so the left-hand side is $O( \sqrt{x} \log^2 x ) = o(x)$ as  required.  -/)]theorem chebyshev_asymptotic : θ ~[atTop] id := by  refine WeakPNT''.add_isLittleO'' (IsBigO.trans_isLittleO (g := fun x ↦ 2 * x.sqrt * x.log) ?_ ?_)  · rw [isBigO_iff']; refine ⟨1, one_pos, ?_⟩    simp only [one_mul, eventually_atTop]    exact ⟨2, fun x hx ↦ by      rw [Pi.sub_apply, norm_eq_abs, norm_eq_abs, abs_of_nonneg (by bound : 0 ≤ 2 * √x * log x)]      exact (abs_of_nonneg (sub_nonneg.mpr (Chebyshev.theta_le_psi x))).symm ▸        Chebyshev.abs_psi_sub_theta_le_sqrt_mul_log (by linarith : 1 ≤ x)⟩  · simpa only [mul_assoc] using! isLittleO_sqrt_mul_log.const_mul_left 2