Erdos392.Params.initial.bound_score_4

@[blueprint  "bound-score-4"  (statement := /-- If $n$ sufficiently large depending on $L, \varepsilon$, then$\sum_{n/L < p \leq n} \frac{n}{p} \log \frac{n}{p} \leq \varepsilon n$. -/)  (proof := /-- Bound $\frac{n}{p}$ by $L$ and use the prime  number theorem (or the Chebyshev bound). -/)  (discussion := 517)  (latexEnv := "sublemma")]theorem Params.initial.bound_score_4 (ε : ℝ) (hε : ε > 0) (L : ℕ) :    ∀ᶠ n in .atTop, ∀ P : Params, P.L = L → P.n = n →      ∑ p ∈ filter (·.Prime) (Icc (P.n / P.L + 1) P.n),      (P.n / p) * Real.log (P.n / p) ≤ ε * P.n := by  have h_term_bound : ∀ (n L : ℕ), 0 < n → 0 < L →      ∀ p ∈ Finset.filter (·.Prime) (Icc (n / L + 1) n),      ((n : ℝ) / p) * Real.log (n / p) ≤ L * Real.log L := by    intro n L hn hL p hp    have hp_Icc := Finset.mem_Icc.mp (mem_filter.mp hp).1    have hp_prime : p.Prime := (mem_filter.mp hp).2    have h_div_bound : (n / p : ℝ) ≤ L := by      rw [div_le_iff₀ (cast_pos.mpr hp_prime.pos)]      norm_cast      nlinarith [Nat.div_add_mod n L, Nat.mod_lt n hL, hp_Icc.1, hp_Icc.2]    gcongr    · exact log_nonneg <| by        rw [le_div_iff₀ (cast_pos.mpr hp_prime.pos)]        norm_cast        grind    · exact div_pos (cast_pos.mpr hn) (cast_pos.mpr hp_prime.pos)  have h_num_terms : ∀ (n L : ℕ), 0 < n → 0 < L →      (Finset.filter (·.Prime) (Icc (n / L + 1) n)).card ≤ primeCounting n := by    intro n L _ _    rw [primeCounting, primeCounting', count_eq_card_filter_range]    exact card_mono fun x hx ↦ Finset.mem_filter.mpr ⟨Finset.mem_range.mpr (by      linarith [Finset.mem_Icc.mp (Finset.mem_filter.mp hx).1]), (mem_filter.mp hx).2⟩  have h_bound : ∀ᶠ n in .atTop, ∀ P : Params, P.L = L → P.n = n →      (∑ p ∈ filter (·.Prime) (Icc (P.n / P.L + 1) P.n),        ((P.n : ℝ) / p) * Real.log (P.n / p))        ≤ (primeCounting P.n) * L * Real.log L := by    filter_upwards [Filter.eventually_gt_atTop 0] with n hn P hP₁ hP₂    refine le_trans (Finset.sum_le_sum fun x hx ↦ h_term_bound _ _ (by linarith) P.hL_pos _ hx) ?_    · simp_all only [gt_iff_lt, Finset.mem_filter, Finset.mem_Icc,        and_imp, sum_const, nsmul_eq_mul, mul_assoc]      exact mul_le_mul_of_nonneg_right (mod_cast h_num_terms n L hn (by linarith [P.hL_pos]))        (mul_nonneg (cast_nonneg _) (log_natCast_nonneg _))  have h_tendsto : Filter.Tendsto      (fun n ↦ (primeCounting n : ℝ) * L * Real.log L / n)      .atTop (nhds 0) := by    have := primeCounting_is_o_id    rw [isLittleO_iff_tendsto] at this    · convert this.const_mul (L * Real.log L) using 2 <;> ring    · aesop  have h_pi_bound : ∀ᶠ n in .atTop, (primeCounting n : ℝ) * L * Real.log L ≤ ε * n := by    filter_upwards [h_tendsto.eventually (gt_mem_nhds (show 0 < ε by positivity)),      Filter.eventually_gt_atTop 0] with n hn hn'    rw [div_lt_iff₀ (by positivity : (0 : ℝ) < n)] at hn    linarith  filter_upwards [h_bound, h_pi_bound] with n hn hn' P hP hP'  exact le_trans (hn P hP hP') (by simpa [hP'] using hn')