I5NewBound

@[blueprint  (title := "I5NewBound")  (statement := /--    We have that    $$|I_5(\nu,\varepsilon,X,T)|\ll\frac{X}{\varepsilon\sqrt{T}}.$$  -/)  (proof := /--    By symmetry, note that    $$|I_1(\nu,\varepsilon,X,T)|=|\overline{I_5(\nu,\varepsilon,X,T)}|=|I_5(\nu,\varepsilon,X,T)|.$$    Applying Lemma \ref{I1NewBound} completes the proof.  -/)  (latexEnv := "lemma")]lemma I5NewBound {SmoothingF : ℝ → ℝ}    (suppSmoothingF : Function.support SmoothingF ⊆ Icc (1 / 2) 2)    (ContDiffSmoothingF : ContDiff ℝ 1 SmoothingF) :    ∃ (C : ℝ) (_ : 0 ≤ C),      ∀ {ε X T : ℝ} (_ : ε ∈ Ioo 0 1) (_ : 3 < X) (_ : 3 < T),        ‖I5New SmoothingF ε X T‖ ≤ C * (X / (ε * Real.sqrt T)) := by    obtain ⟨C, Cnonneg, hI1NewBound⟩ := I1NewBound suppSmoothingF ContDiffSmoothingF    use C, Cnonneg    intro ε X T εinIoo Xgt3 Tgt3    have I1NewI5New : I5New SmoothingF ε X T = conj (I1New SmoothingF ε X T) := by        unfold I1New I5New        simp only [map_mul, map_div₀, conj_I, conj_ofReal, conj_ofNat, map_one]        rw [neg_mul, mul_neg, ← neg_mul]        congr        · ring        · rw [← integral_conj, ← integral_comp_neg_Ioi, integral_Ici_eq_integral_Ioi]          apply setIntegral_congr_fun <| measurableSet_Ioi          intro x hx; simp only []          rw [← smoothedChebyshevIntegrand_conj (by linarith)]          simp [ofReal_inv, ofReal_neg, neg_mul, map_add, map_one, map_inv₀, conj_ofReal,            map_neg, map_mul, conj_I, mul_neg, neg_neg]    rw [I1NewI5New, RCLike.norm_conj]    exact hI1NewBound εinIoo Xgt3 Tgt3