SmoothedChebyshevClose

@[blueprint  (title := "SmoothedChebyshevClose")  (statement := /--  We have that  $$\psi_{\epsilon}(X) = \psi(X) + O(\epsilon X \log X).$$  -/)  (proof := /--  Take the difference. By Lemma \ref{Smooth1Properties_above} and \ref{Smooth1Properties_below},  the sums agree except when $1-c \epsilon \leq n/X \leq 1+c \epsilon$. This is an interval of  length $\ll \epsilon X$, and the summands are bounded by $\Lambda(n) \ll \log X$.   %[No longer relevant, as we will do better than any power of log savings...: This is not enough,  %as it loses a log! (Which is fine if our target is the strong PNT, with  %exp-root-log savings, but not here with the ``softer'' approach.) So we will need something like  %the Selberg sieve (already in Mathlib? Or close?) to conclude that the number of primes in this  %interval is $\ll \epsilon X / \log X + 1$.  %(The number of prime powers is $\ll X^{1/2}$.)  %And multiplying that by $\Lambda (n) \ll \log X$ gives the desired bound.]  -/)]theorem SmoothedChebyshevClose {SmoothingF : ℝ → ℝ}    (diffSmoothingF : ContDiff ℝ 1 SmoothingF)    (suppSmoothingF : Function.support SmoothingF ⊆ Icc (1 / 2) 2)    (SmoothingFnonneg : ∀ x > 0, 0 ≤ SmoothingF x)    (mass_one : ∫ x in Ioi 0, SmoothingF x / x = 1) :    ∃ C > 0, ∀ (X : ℝ) (_ : 3 < X) (ε : ℝ) (_ : 0 < ε) (_ : ε < 1) (_ : 2 < X * ε),    ‖SmoothedChebyshev SmoothingF ε X - ψ X‖ ≤ C * ε * X * Real.log X := by  obtain ⟨c₁, c₁_pos, c₁_eq, hc₁⟩ := Smooth1Properties_below suppSmoothingF mass_one   obtain ⟨c₂, c₂_pos, c₂_eq, hc₂⟩ := Smooth1Properties_above suppSmoothingF   have c₁_lt : c₁ < 1 := by    rw[c₁_eq]    exact lt_trans (Real.log_two_lt_d9) (by norm_num)   have c₂_lt : c₂ < 2 := by    rw[c₂_eq]    nth_rewrite 3 [← mul_one 2]    apply mul_lt_mul'    · rfl    · exact lt_trans (Real.log_two_lt_d9) (by norm_num)    · exact Real.log_nonneg (by norm_num)    · positivity   let C : ℝ := 6 * (3 * c₁ + c₂)  have C_eq : C = 6 * (3 * c₁ + c₂) := rfl   clear_value C   have Cpos : 0 < C := by    rw [C_eq]    positivity   refine ⟨C, Cpos, fun X X_ge_C ε εpos ε_lt_one ↦ ?_⟩   have X_gt_zero : (0 : ℝ) < X := by linarith   have n_on_X_pos {n : ℕ} (npos : 0 < n) :      0 < n / X := by    have : (0 : ℝ) < n := by exact_mod_cast npos    positivity   have smooth1BddAbove (n : ℕ) (npos : 0 < n) :      Smooth1 SmoothingF ε (n / X) ≤ 1 :=    Smooth1LeOne SmoothingFnonneg mass_one εpos (n_on_X_pos npos)   have smooth1BddBelow (n : ℕ) (npos : 0 < n) :      Smooth1 SmoothingF ε (n / X) ≥ 0 :=    Smooth1Nonneg SmoothingFnonneg (n_on_X_pos npos) εpos   have smoothIs1 (n : ℕ) (npos : 0 < n) (n_le : n ≤ X * (1 - c₁ * ε)) :      Smooth1 SmoothingF ε (↑n / X) = 1 := by    apply hc₁ (ε := ε) (n / X) εpos (n_on_X_pos npos)    exact (div_le_iff₀' X_gt_zero).mpr n_le   have smoothIs0 (n : ℕ) (n_le : (1 + c₂ * ε) ≤ n / X) :=    hc₂ (ε := ε) (n / X) ⟨εpos, ε_lt_one⟩ n_le   have ε_pos: ε > 0 := by linarith  have X_pos: X > 0 := by linarith  have X_gt_three : 3 < X := by linarith   intro X_bound   have X_bound_1 : 1 ≤ X * ε * c₁ := by    rw[c₁_eq, ← div_le_iff₀]    · have : 1 / Real.log 2 < 2 := by        nth_rewrite 2 [← one_div_one_div 2]        rw[one_div_lt_one_div]        · exact lt_of_le_of_lt (by norm_num) (Real.log_two_gt_d9)        · exact Real.log_pos (by norm_num)        norm_num      exact le_of_lt (gt_trans X_bound this)    exact Real.log_pos (by norm_num)   have X_bound_2 : 1 ≤ X * ε * c₂ := by    rw[c₂_eq, ← div_le_iff₀]    · have : 1 / (2 * Real.log 2) < 2 := by        nth_rewrite 3 [← one_div_one_div 2]        · rw[one_div_lt_one_div, ← one_mul (1 / 2)]          · apply mul_lt_mul            · norm_num            · apply le_of_lt              exact lt_trans (by norm_num) (Real.log_two_gt_d9)            repeat norm_num          · norm_num            exact Real.log_pos (by norm_num)          · norm_num      exact le_of_lt (gt_trans X_bound this)    norm_num    exact Real.log_pos (by norm_num)   rw [SmoothedChebyshevDirichlet diffSmoothingF SmoothingFnonneg suppSmoothingF    mass_one (by linarith) εpos ε_lt_one]   convert SmoothedChebyshevClose_aux SmoothingF c₁ c₁_pos c₁_lt c₂ c₂_pos c₂_lt hc₂ C C_eq ε    ε_pos ε_lt_one X X_pos X_gt_three X_bound_1 X_bound_2 smooth1BddAbove smooth1BddBelow    smoothIs1 smoothIs0