I4NewBound

@[blueprint  (title := "I4NewBound")  (statement := /--    We have that    $$|I_4(\nu,\varepsilon,X,T)|\ll\frac{X}{\varepsilon\sqrt{T}}.$$  -/)  (proof := /--    By symmetry, note that    $$|I_2(\nu,\varepsilon,X,T)|=|\overline{I_4(\nu,\varepsilon,X,T)}|=|I_4(\nu,\varepsilon,X,T)|.$$    Applying Lemma \ref{I2NewBound} completes the proof.  -/)  (latexEnv := "lemma")]lemma I4NewBound {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),        let σ' := 1 - F / Real.log T        ‖I4New SmoothingF ε X T σ'‖ ≤ C * (X / (ε * Real.sqrt T)) := by    obtain ⟨C, Cnonneg, hI2NewBound⟩ := I2NewBound suppSmoothingF ContDiffSmoothingF    use C, Cnonneg    intro ε X T εinIoo Xgt3 Tgt3 σ'    have I2NewI4New : I4New SmoothingF ε X T σ' = -conj (I2New SmoothingF ε X T σ') := by        unfold I2New I4New        simp only [map_mul, map_div₀, conj_I, conj_ofReal, conj_ofNat, map_one]        rw [mul_neg, div_neg, neg_mul_comm, ← mul_neg]        congr        rw [← intervalIntegral_conj, neg_neg]        exact intervalIntegral.integral_congr fun x hx ↦ by          rw [← smoothedChebyshevIntegrand_conj (by linarith)]          simp [map_sub, map_mul, conj_I, mul_neg, sub_neg_eq_add]    rw [I2NewI4New, norm_neg, RCLike.norm_conj]    exact hI2NewBound εinIoo Xgt3 Tgt3