I8Bound

@[blueprint  (title := "I8Bound")  (statement := /--  We have that  $$  \left|I_{8}(\nu, \epsilon, X, T)\right| \ll \frac{X}{\epsilon T}  .  $$  -/)  (proof := /--  We deduce this from the corresponding bound for $I_2$, using the symmetry between $I_2$ and $I_8$.  -/)  (latexEnv := "lemma")]lemma I8Bound {SmoothingF : ℝ → ℝ}    (suppSmoothingF : Function.support SmoothingF ⊆ Icc (1 / 2) 2)    (ContDiffSmoothingF : ContDiff ℝ 1 SmoothingF)    {A C₂ : ℝ} (has_bound : LogDerivZetaHasBound A C₂) (C₂_pos : 0 < C₂) (A_in : A ∈ Ioc 0 (1 / 2)) :    ∃ (C : ℝ) (_ : 0 < C),    ∀(X : ℝ) (_ : 3 < X) {ε : ℝ} (_: 0 < ε)    (_ : ε < 1)    {T : ℝ} (_ : 3 < T),    let σ₁ : ℝ := 1 - A / (Real.log T) ^ 9    ‖I₈ SmoothingF ε T X σ₁‖ ≤ C * X / (ε * T) := by   obtain ⟨C, hC, i2Bound⟩ := I2Bound suppSmoothingF ContDiffSmoothingF has_bound C₂_pos A_in  use C, hC  intro X hX ε hε0 hε1 T hT σ₁  let i2Bound := i2Bound X hX hε0 hε1 hT  rw[I8I2 hX, norm_neg, norm_conj]  exact i2Bound