Erdos392.Params.initial.bound_score_5

@[blueprint  "bound-score-5"  (statement := /-- If $n$ sufficiently large depending on $M, L, \varepsilon$, then$\sum_{p \leq L} (M \log n + M L \pi(n)) \log L \leq \varepsilon n$. -/)  (proof := /-- Use the prime number theorem (or the Chebyshev bound). -/)  (discussion := 518)  (latexEnv := "sublemma")]theorem Params.initial.bound_score_5 (ε : ℝ) (hε : ε > 0) (M L : ℕ) :    ∀ᶠ n in Filter.atTop, ∀ P : Params,      P.M = M → P.L = L → P.n = n → ∑ _p ∈ Finset.filter (·.Prime) (Finset.Iic P.L),          (P.M * Real.log P.n + P.M * P.L^2 * primeCounting P.n) * Real.log P.L ≤ ε * P.n := by  have tendsto_log_div_atTop : Filter.Tendsto      (fun n : ℕ ↦ Real.log n / (n : ℝ)) .atTop (nhds 0) := by    suffices h : Filter.Tendsto        (fun y : ℝ ↦ y * Real.log (1 / y))        (.map (1 / ·) .atTop) (nhds 0) by      exact (h.comp (Filter.map_mono tendsto_natCast_atTop_atTop)).congr fun _ ↦ by grind    norm_num at *    exact tendsto_nhdsWithin_of_tendsto_nhds      (by simpa using Real.continuous_mul_log.fun_neg.tendsto 0)  have h_pi_div_n_zero : Filter.Tendsto (fun n : ℕ ↦ (Nat.primeCounting n : ℝ) / n)      .atTop (nhds 0) := tendsto_primeCounting_div_id_zero  have h_sum_bound : Filter.Tendsto (fun n : ℕ ↦      ((Nat.primeCounting L : ℝ) * (M * Real.log n + M * L ^ 2 * (Nat.primeCounting n : ℝ)) *        Real.log L) / n) .atTop (nhds 0) := by    convert Filter.Tendsto.const_mul ((primeCounting L : ℝ) * M * Real.log L)      ((tendsto_log_div_atTop.const_mul 1).add        (h_pi_div_n_zero.const_mul (L ^ 2 : ℝ))) using 2 <;>      ring  filter_upwards [h_sum_bound.eventually (gt_mem_nhds hε),    Filter.eventually_gt_atTop 0] with n hn hn' P hM hL hn''  rw [div_lt_iff₀ (by positivity)] at hn  simp_all only [gt_iff_lt, mul_comm, mul_left_comm, mul_add, mul_assoc, sum_const]  convert! hn.le using 1  · norm_num [primeCounting]    ring_nf    rw [primeCounting', count_eq_card_filter_range]    norm_num [add_comm, Finset.sum_range_succ]    ring_nf    rw [show count Nat.Prime (1 + L) = (Finset.filter Nat.Prime (Iic L)).card from ?_]    · ring_nf    · rw [count_eq_card_filter_range, add_comm, range_eq_Ico]; rfl