I2Bound

@[blueprint  (title := "I2Bound")  (statement := /--  Assuming a bound of the form of Lemma \ref{LogDerivZetaBndUnif} we have that  $$  \left|I_{2}(\nu, \epsilon, X, T)\right| \ll \frac{X}{\epsilon T}  .  $$  -/)  (proof := /--  Unfold the definitions and apply the triangle inequality.  $$  \left|I_{2}(\nu, \epsilon, X, T, \sigma_1)\right| =  \left|\frac{1}{2\pi i} \int_{\sigma_1}^{\sigma_0}  \left(\frac{-\zeta'}\zeta(\sigma - T i) \right) \cdot  \mathcal M(\widetilde 1_\epsilon)(\sigma - T i) \cdot  X^{\sigma - T i}   \ d\sigma  \right|  $$  $$\leq  \frac{1}{2\pi}  \int_{\sigma_1}^{\sigma_0}  C \cdot \log T ^ 9  \frac{C'}{\epsilon|\sigma - T i|^2}  X^{\sigma_0}   \ d\sigma   \leq  C'' \cdot \frac{X\log T^9}{\epsilon T^2}  ,  $$  where we used Theorems \ref{MellinOfSmooth1b}, the hypothesised bound on zeta and the fact that  $X^\sigma \le X^{\sigma_0} = X\cdot X^{1/\log X}=e \cdot X$.  Since $T>3$, we have $\log T^9 \leq C''' T$.  -/)  (latexEnv := "lemma")]lemma I2Bound {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  have ⟨C₁, C₁pos, Mbd⟩ := MellinOfSmooth1b ContDiffSmoothingF suppSmoothingF  have := (IBound_aux1 3 (by norm_num) 9)  obtain ⟨C₃, ⟨C₃_gt, hC₃⟩⟩ := this   let C' : ℝ := C₁ * C₂ * C₃ * rexp 1  have : C' > 0 := by positivity  use ‖1/(2*π*I)‖ * (2 * C'), by    refine Right.mul_pos ?_ ?_    · rw[norm_pos_iff]      simp[pi_ne_zero]    · simp[this]  intro X X_gt ε ε_pos ε_lt_one T T_gt σ₁  have Xpos : 0 < X := lt_trans (by simp only [Nat.ofNat_pos]) X_gt  have Tpos : 0 < T := lt_trans (by norm_num) T_gt  unfold I₂  rw[norm_mul, mul_assoc (c := X), ← mul_div]  refine mul_le_mul_of_nonneg_left ?_ (norm_nonneg _)  have interval_length_nonneg : σ₁ ≤ 1 + (Real.log X)⁻¹ := by    dsimp[σ₁]    rw[sub_le_iff_le_add]    nth_rw 1 [← add_zero 1]    rw[add_assoc]    apply add_le_add_right    refine Left.add_nonneg ?_ ?_    · rw[inv_nonneg, log_nonneg_iff Xpos]      exact le_trans (by norm_num) (le_of_lt X_gt)    · refine div_nonneg ?_ ?_      · exact A_in.1.le      apply pow_nonneg      rw[log_nonneg_iff Tpos]      exact le_trans (by norm_num) (le_of_lt T_gt)  have σ₁pos : 0 < σ₁ := by    rw[sub_pos]    calc      A / Real.log T ^ 9 ≤ 1 / 2 / Real.log T ^ 9 := by        refine div_le_div_of_nonneg_right (A_in.2) ?_        apply pow_nonneg        rw[log_nonneg_iff Tpos]        exact le_trans (by norm_num) (le_of_lt T_gt)      _ ≤ 1 / 2 / 1 := by        refine div_le_div_of_nonneg_left (by norm_num) (by norm_num) ?_        exact one_le_pow₀ (logt_gt_one T_gt.le).le      _ < 1 := by norm_num  suffices ∀ σ ∈ Ioc σ₁ (1 + (Real.log X)⁻¹),      ‖SmoothedChebyshevIntegrand SmoothingF ε X (↑σ - ↑T * I)‖ ≤ C' * X / (ε * T) by    calc      ‖∫ (σ : ℝ) in σ₁..1 + (Real.log X)⁻¹,          SmoothedChebyshevIntegrand SmoothingF ε X (↑σ - ↑T * I)‖ ≤          C' * X / (ε * T) * |1 + (Real.log X)⁻¹ - σ₁| := by        refine intervalIntegral.norm_integral_le_of_norm_le_const ?_        convert this using 3        apply uIoc_of_le        exact interval_length_nonneg      _ ≤ C' * X / (ε * T) * 2 := by        apply mul_le_mul_of_nonneg_left        · rw[abs_of_nonneg (sub_nonneg.mpr interval_length_nonneg)]          calc            1 + (Real.log X)⁻¹ - σ₁ ≤ 1 + (Real.log X)⁻¹ := by linarith            _ ≤ 2 := (one_add_inv_log X_gt.le).le        positivity      _ = 2 * C' * X / (ε * T) := by ring  -- Now bound the integrand  intro σ hσ  unfold SmoothedChebyshevIntegrand  have log_deriv_zeta_bound : ‖ζ' (σ - T * I) / ζ (σ - T * I)‖ ≤ C₂ * (C₃ * T) := by    calc      ‖ζ' (σ - (T : ℝ) * I) / ζ (σ - (T : ℝ) * I)‖ = ‖ζ' (σ + (-T : ℝ) * I) / ζ (σ + (-T : ℝ) * I)‖ := by        have Z : σ - (T : ℝ) * I = σ + (- T : ℝ) * I := by simp; ring_nf        simp [Z]      _ ≤ C₂ * Real.log |-T| ^ 9 := has_bound σ (-T)          (by simp only [abs_neg]; rw [abs_of_pos Tpos]; exact T_gt)          (by unfold σ₁ at hσ; simp only [mem_Ioc, abs_neg, log_abs, mem_Ici,            tsub_le_iff_right] at hσ ⊢; replace hσ := hσ.1; linarith)      _ ≤ C₂ * Real.log T ^ 9 := by simp      _ ≤ C₂ * (C₃ * T) := by gcongr; exact hC₃ T (by linarith)   -- Then estimate the remaining factors.  calc    ‖-ζ' (σ - T * I) / ζ (σ - T * I) * 𝓜 (fun x ↦ (Smooth1 SmoothingF ε x : ℂ))        (σ - T * I) * X ^ (σ - T * I)‖ =        ‖-ζ' (σ - T * I) / ζ (σ - T * I)‖ * ‖𝓜 (fun x ↦ (Smooth1 SmoothingF ε x : ℂ))        (σ - T * I)‖ * ‖(X : ℂ) ^ (σ - T * I)‖ := by      repeat rw[norm_mul]    _ ≤ C₂ * (C₃ * T) * (C₁ * (ε * ‖σ - T * I‖ ^ 2)⁻¹) * (rexp 1 * X) := by      apply mul_le_mul₃      · rw[neg_div, norm_neg]        exact log_deriv_zeta_bound      · refine Mbd σ₁ σ₁pos _ ?_ ?_ ε ε_pos ε_lt_one        · simp only [mem_Ioc, sub_re, ofReal_re, mul_re, I_re, mul_zero, ofReal_im, I_im, mul_one,            sub_self, sub_zero, σ₁] at hσ ⊢          linarith        · simp only [mem_Ioc, sub_re, ofReal_re, mul_re, I_re, mul_zero, ofReal_im, I_im, mul_one,            sub_self, sub_zero, σ₁] at hσ ⊢          linarith[one_add_inv_log X_gt.le]      · rw[cpow_def_of_ne_zero]        · rw[norm_exp,← ofReal_log, re_ofReal_mul]          · simp only [sub_re, ofReal_re, mul_re, I_re, mul_zero, ofReal_im, I_im, mul_one, sub_self,              sub_zero]            rw [← le_log_iff_exp_le, Real.log_mul (exp_ne_zero 1), Real.log_exp, ← le_div_iff₀', add_comm, add_div, div_self, one_div]            · exact hσ.2            · refine (Real.log_pos ?_).ne.symm              linarith            · apply Real.log_pos              linarith            · linarith            · positivity          · positivity        · exact_mod_cast Xpos.ne.symm      · positivity      · positivity      · positivity    _ = (C' * X * T) / (ε * ‖σ - T * I‖ ^ 2) := by ring    _ ≤ C' * X / (ε * T) := by      have : ‖σ - T * I‖ ^ 2 ≥ T ^ 2 := by        calc          ‖σ - T * I‖ ^ 2 = ‖σ + (-T : ℝ) * I‖ ^ 2 := by            congr 2            push_cast            ring          _ = normSq (σ + (-T : ℝ) * I) := (normSq_eq_norm_sq _).symm          _ = σ^2 + (-T)^2 := by            rw[Complex.normSq_add_mul_I]          _ ≥ T^2 := by            rw[neg_sq]            exact le_add_of_nonneg_left (sq_nonneg _)      calc        C' * X * T / (ε * ‖↑σ - ↑T * I‖ ^ 2) ≤ C' * X * T / (ε * T ^ 2) := by          rw[div_le_div_iff_of_pos_left, mul_le_mul_iff_right₀]          · exact this          · exact ε_pos          · positivity          · apply mul_pos ε_pos            exact lt_of_lt_of_le (pow_pos Tpos 2) this          · positivity        _ = C' * X / (ε * T) := by          field_simp