mu_pnt

@[blueprint  "mu-pnt"  (title := "M\\\"obius form of prime number theorem")  (statement := /-- We have $\sum_{n \leq x} \mu(n) = o(x)$. -/)  (proof := /--  From the Dirichlet convolution identity    $$ \mu(n) \log n = - \sum_{d|n} \mu(d) \Lambda(n/d)$$  and summing we obtain  $$ \sum_{n \leq x} \mu(n) \log n = - \sum_{d \leq x} \mu(d) \sum_{m \leq x/d} \Lambda(m).$$  For any $\eps>0$, we have from the prime number theorem that  $$ \sum_{m \leq x/d} \Lambda(m) = x/d + O(\eps x/d) + O_\eps(1)$$  (divide into cases depending on whether $x/d$ is large or small compared to $\eps$).  We conclude that  $$ \sum_{n \leq x} \mu(n) \log n    = - x \sum_{d \leq x} \frac{\mu(d)}{d} + O(\eps x \log x) + O_\eps(x).$$  Applying \eqref{mun} we conclude that  $$ \sum_{n \leq x} \mu(n) \log n = O(\eps x \log x) + O_\eps(x).$$  and hence  $$ \sum_{n \leq x} \mu(n) \log x    = O(\eps x \log x) + O_\eps(x) + O( \sum_{n \leq x} (\log x - \log n) ).$$  From Stirling's formula one has  $$  \sum_{n \leq x} (\log x - \log n) = O(x)$$  thus  $$ \sum_{n \leq x} \mu(n) \log x = O(\eps x \log x) + O_\eps(x)$$  and thus  $$ \sum_{n \leq x} \mu(n) = O(\eps x) + O_\eps(\frac{x}{\log x}).$$  Sending $\eps \to 0$ we obtain the claim.  -/)  (proofUses := ["WeakPNT", "mun"])  (latexEnv := "proposition")]theorem mu_pnt : (fun x : ℝ ↦ ∑ n ∈ range ⌊x⌋₊, μ n) =o[atTop] fun x ↦ x := by  have h_moebius_sum : (fun x : ℝ => ∑ n ∈ Finset.range ⌊x⌋₊, (μ n : ℝ)) =o[atTop] (fun x : ℝ => x) := by    have h_bound : (fun x : ℝ => ∑ n ∈ Finset.range ⌊x⌋₊, (μ n : ℝ)) =o[atTop] (fun x : ℝ => x) := by      have h_sum : (fun x : ℝ => ∑ n ∈ Finset.range (⌊x⌋₊ + 1), (μ n : ℝ)) =o[atTop] (fun x : ℝ => x) := by        have h_moebius_sum : (fun x : ℝ => ∑ n ∈ Finset.Iic ⌊x⌋₊, (μ n : ℝ)) =o[atTop] (fun x : ℝ => x) := by          convert! M_isLittleO using 1        simpa only [Finset.range_eq_Ico] using! h_moebius_sum      have h_mu_floor : (fun x : ℝ => (μ ⌊x⌋₊ : ℝ)) =o[atTop] (fun x : ℝ => x) := by        rw [Asymptotics.isLittleO_iff_tendsto'] <;> norm_num        · refine squeeze_zero_norm (a := fun x : ℝ => 1 / |x|) ?_ ?_          · intro x; norm_num [abs_div]            exact mul_le_of_le_one_left (by positivity) (mod_cast by exact abs_moebius_le_one)          · exact tendsto_const_nhds.div_atTop (tendsto_norm_atTop_atTop)        · exact ⟨1, by intros; linarith⟩      simpa [Finset.sum_range_succ] using h_sum.sub h_mu_floor    convert h_bound using 1  rw [Asymptotics.isLittleO_iff] at *  simp_all +decide [Norm.norm]