Theorem: SmoothedChebyshevClose (PrimeNumberTheoremAnd/MediumPNT.lean)

State before:
ψ : ℝ → ℝ
ε : ℝ
ε_pos : 0 < ε
suppΨ : support ψ ⊆ Icc (1 / 2) 2
Ψnonneg : ∀ x > 0, 0 ≤ ψ x
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
⊢ (fun X => ‖SmoothedChebyshev ψ ε X - ↑(ChebyshevPsi X)‖) =O[atTop] fun X => ε * X * X.log
Tactic:
sorry
State after:
no goals