Zeta Box Eval

@[blueprint  (title := "ZetaBoxEval")  (statement := /--  For all $\epsilon > 0$ sufficiently close to $0$, the rectangle integral over $[1-\delta,2] \times_{ℂ} [-T,T]$ of the integrand in  $\psi_{\epsilon}$ is  $$  \frac{X^{1}}{1}\mathcal{M}(\widetilde{1_{\epsilon}})(1)  = X(1+O(\epsilon))  ,$$  where the implicit constant is independent of $X$.  -/)  (proof := /-- Unfold the definitions and apply Lemma \ref{MellinOfSmooth1c}. -/)]theorem ZetaBoxEval {SmoothingF : ℝ → ℝ}    (suppSmoothingF : Function.support SmoothingF ⊆ Icc (1 / 2) 2)    (mass_one : ∫ x in Ioi 0, SmoothingF x / x = 1)    (ContDiffSmoothingF : ContDiff ℝ 1 SmoothingF) :    ∃ C, ∀ᶠ ε in (nhdsWithin 0 (Ioi 0)), ∀ X : ℝ, 0 ≤ X →    ‖𝓜 (fun x ↦ (Smooth1 SmoothingF ε x : ℂ)) 1 * X - X‖ ≤ C * ε * X := by  have := MellinOfSmooth1c ContDiffSmoothingF suppSmoothingF mass_one  clear suppSmoothingF mass_one ContDiffSmoothingF  rw[Asymptotics.isBigO_iff] at this  obtain ⟨C, hC⟩ := this  use C  have εpos : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Ioi 0), ε > 0 :=    eventually_mem_of_tendsto_nhdsWithin fun ⦃U⦄ hU ↦ hU  filter_upwards [hC, εpos] with ε hC εpos  rw[id_eq, norm_of_nonneg (le_of_lt εpos)] at hC  intro X Xnne  nth_rw 2 [← one_mul (X : ℂ)]  rw[← sub_mul, norm_mul, norm_real, norm_of_nonneg Xnne]  exact mul_le_mul_of_nonneg_right hC Xnne