Erdos392.primeCounting_le_bound

@[blueprint  "primeCounting-le-bound"  (statement := /-- For all $n \geq 2$, one has  $$\pi(n) \leq \sqrt{n} + \frac{2n \log 4}{\log n}.$$ -/)  (proof := /-- By Chebyshev's bound, $\prod_{p \leq n} p \leq 4^n$, so$\sum_{p \leq n} \log p \leq n \log 4$. The number of primes $p \leq \sqrt{n}$ is triviallyat most $\sqrt{n}$. For primes $p > \sqrt{n}$, we have $\log p > \frac{1}{2} \log n$, hence$$\bigl(\pi(n) - \pi(\sqrt{n})\bigr) \cdot \tfrac{1}{2} \log n  < \sum_{\sqrt{n} < p \leq n} \log p \leq n \log 4,$$giving $\pi(n) - \pi(\sqrt{n}) < \frac{2n \log 4}{\log n}$. Adding $\pi(\sqrt{n}) \leq \sqrt{n}$yields the result. -/)  (latexEnv := "sublemma")]lemma primeCounting_le_bound (n : ℕ) (hn : 2 ≤ n) :    (Nat.primeCounting n : ℝ) ≤ Real.sqrt n + (2 * n * Real.log 4) / Real.log n := by  have h_sum_log_bound :      (∑ p ∈ filter Prime (Icc 1 n), Real.log p) ≤ n * Real.log 4 := by    have h_prod_le : (∏ p ∈ filter Prime (Icc 1 n), p : ℕ) ≤ 4 ^ n := by      convert primorial_le_four_pow n using 1; congr 1 with (_ | p) <;> aesop    have h_prod_le_real : (∏ p ∈ filter Prime (Icc 1 n), (p : ℝ)) ≤ 4 ^ n := by      rw [← cast_prod]; exact_mod_cast h_prod_le    rw [← log_prod fun x hx ↦ cast_ne_zero.mpr <| Nat.Prime.ne_zero <| by aesop]    have h_prod_pos : 0 < ∏ p ∈ filter Prime (Icc 1 n), (p : ℝ) :=      prod_pos fun p hp ↦ cast_pos.mpr <| Prime.pos <| by aesop    simpa using log_le_log h_prod_pos h_prod_le_real  have h_large_primes :      (∑ p ∈ filter Prime (Icc (⌊Real.sqrt n⌋₊ + 1) n), Real.log p) ≥      (primeCounting n - primeCounting ⌊Real.sqrt n⌋₊) * Real.log (Real.sqrt n) := by    have h_log_lower : ∀ p ∈ Finset.filter Prime (Icc (⌊Real.sqrt n⌋₊ + 1) n),        Real.log p ≥ Real.log (Real.sqrt n) := fun p hp ↦ log_le_log (by positivity)        (le_trans (lt_floor_add_one _ |> le_of_lt)          (mod_cast (Finset.mem_Icc.mp (mem_filter.mp hp).1).1))    refine le_trans ?_ (sum_le_sum h_log_lower)    norm_num [primeCounting, primeCounting', count_eq_card_filter_range]    rw [show Finset.filter Prime (Icc (n.sqrt + 1) n) =      Finset.filter Prime (range (n + 1)) \        filter Nat.Prime (range (n.sqrt + 1)) from ?_, card_sdiff]    · rw [cast_sub]      · rw [inter_eq_left.mpr          (filter_subset_filter _ <| range_mono <| succ_le_succ <| sqrt_le_self _)]      · exact card_mono inter_subset_right    · ext      simp [Finset.mem_Icc, Finset.mem_range, mem_sdiff]      grind  have h_combined :      (Nat.primeCounting n - Nat.primeCounting ⌊Real.sqrt n⌋₊) * Real.log (Real.sqrt n) ≤      n * Real.log 4 := by    refine le_trans h_large_primes <| h_sum_log_bound.trans' <| sum_le_sum_of_subset_of_nonneg ?_        (fun _ _ _ ↦ log_nonneg <| one_le_cast.mpr <| Prime.pos <| by aesop)    exact filter_subset_filter _ <| Icc_subset_Icc (succ_pos _) le_rfl  have h_trivial : primeCounting ⌊Real.sqrt n⌋₊ ≤ Real.sqrt n := by    have : primeCounting ⌊Real.sqrt n⌋₊ ≤ ⌊Real.sqrt n⌋₊ := by      rw [primeCounting, primeCounting', count_eq_card_filter_range]      calc (Finset.filter Prime (range (⌊Real.sqrt n⌋₊ + 1))).card          ≤ (Finset.Ico 2 (⌊Real.sqrt n⌋₊ + 1)).card :=            card_le_card fun x hx ↦ Finset.mem_Ico.mpr            ⟨Prime.two_le (mem_filter.mp hx).2, Finset.mem_range.mp (mem_filter.mp hx).1⟩        _ ≤ ⌊Real.sqrt n⌋₊ := by simp    exact le_trans (cast_le.mpr this) (floor_le (sqrt_nonneg _))  rw [log_sqrt (cast_nonneg _)] at h_combined  rw [add_div', le_div_iff₀] <;> nlinarith [log_pos <| show (n : ℝ) > 1 by norm_cast,    log_le_sub_one_of_pos <| show (n : ℝ) > 0 by positivity]