I1NewBound

@[blueprint  (title := "I1NewBound")  (statement := /--    We have that    $$|I_1(\nu,\varepsilon,X,T)|\ll\frac{X}{\varepsilon\sqrt{T}}.$$  -/)  (proof := /--    Note that $|I_1(\nu,\varepsilon,X,T)|=$    $$\left|\frac{1}{2\pi i}\int_{-\infty}^{-T}\left(-\frac{\zeta'}{\zeta}(\sigma+it)\right)      \,\mathcal{M}(\tilde{1}_\varepsilon)(\sigma+it)\,X^{\sigma+it}\,dt\right|      \ll\int_{-\infty}^{-T}\left|\frac{\zeta'}{\zeta}(\sigma+it)\right|      \cdot|\mathcal{M}(\tilde{1}_\varepsilon)(\sigma+it)|\cdot X^\sigma\,dt.$$    Applying Theorem \ref{LogDerivZetaUniformLogSquaredBound} and Lemma \ref{MellinOfSmooth1b},    we have that    $$|I_1(\nu,\varepsilon,X,T)|      \ll\int_{-\infty}^{-T}\log^2|t|\cdot\frac{X^\sigma}{\varepsilon\,|\sigma+it|^2}\,dt      \ll\frac{X}{\varepsilon}\int_T^\infty\frac{\sqrt{t}\,dt}{t^2}      \ll\frac{X}{\varepsilon\sqrt{T}}.$$    Here we are using the fact that $\log^2 t$ grows slower than $\sqrt{t}$,    $|\sigma+it|^2\geq t^2$, and $X^\sigma=X\cdot X^{1/\log X}=eX$.  -/)  (proofUses := ["LogDerivZetaUniformLogSquaredBound", "MellinOfSmooth1b"])  (latexEnv := "lemma")]lemma I1NewBound {SmoothingF : ℝ → ℝ}    (suppSmoothingF : Function.support SmoothingF ⊆ Icc (1 / 2) 2)    (ContDiffSmoothingF : ContDiff ℝ 1 SmoothingF) : ∃ (C : ℝ) (_Cnonneg : 0 ≤ C),    ∀ {ε X T : ℝ} (_εinIoo : ε ∈ Ioo 0 1) (_Xgt3 : 3 < X) (_Tgt3 : 3 < T),    ‖I1New SmoothingF ε X T‖ ≤ C * (X / (ε * Real.sqrt T)) := by    have h_I1New_bound : ∃ C > 0, ∀ {ε X T : ℝ} (εinIoo : ε ∈ Set.Ioo 0 1) (Xgt3 : 3 < X)        (Tgt3 : 3 < T),        ‖∫ t in Set.Iic (-T),          SmoothedChebyshevIntegrand SmoothingF ε X (1 + (Real.log X)⁻¹ + t * I)‖ ≤          C * (X / ε) * (1 / Real.sqrt T) := by            obtain ⟨C₁, hC₁_pos, hC₁⟩ : ∃ C₁ > 0, ∀ {ε X T : ℝ} (εinIoo : ε ∈ Set.Ioo 0 1)                (Xgt3 : 3 < X) (Tgt3 : 3 < T)                (t : ℝ) (ht : t ≤ -T),                ‖SmoothedChebyshevIntegrand SmoothingF ε X (1 + (Real.log X)⁻¹ + t * I)‖ ≤                C₁ * (X / ε) * (Real.log (-t))^2 / (-t)^2 :=              I1NewIntegrandBound suppSmoothingF ContDiffSmoothingF            obtain ⟨C₂, hC₂_pos, hC₂⟩ : ∃ C₂ > 0, ∀ {T : ℝ} (Tgt3 : 3 < T),                ∫ t in Set.Ici T, (Real.log t)^2 / t^2 ≤ C₂ / Real.sqrt T :=                  IntegralLogSqOverTSqBound            refine ⟨C₁ * C₂, mul_pos hC₁_pos hC₂_pos,              fun {ε X T} εinIoo Xgt3 Tgt3 ↦                (MeasureTheory.norm_integral_le_integral_norm _).trans ?_⟩            refine (MeasureTheory.integral_mono_of_nonneg              (g := fun t ↦ C₁ * (X / ε) * Real.log (-t) ^ 2 / (-t) ^ 2) ?_ ?_ ?_).trans ?_            · exact Filter.Eventually.of_forall fun x ↦ norm_nonneg _            · have h_integrable :                  MeasureTheory.IntegrableOn (fun t ↦ (Real.log t)^2 / t^2) (Set.Ici T) := by                have h_integrable :                    MeasureTheory.IntegrableOn                      (fun t ↦ (Real.log t)^2 / t^2) (Set.Ioi T) := by                  have h_bound : ∀ t, t > T → (Real.log t)^2 / t^2 ≤ 4 / t^(3/2 : ℝ) := by                    intro t ht                    have h_log_bound : Real.log t ≤ 2 * t^(1/4 : ℝ) := by                      have := Real.log_le_sub_one_of_pos (show 0 < t ^ (1 / 4 : ℝ) / 2 by                        exact div_pos (Real.rpow_pos_of_pos (by linarith) _) zero_lt_two)                      rw [Real.log_div (by exact ne_of_gt (Real.rpow_pos_of_pos (by linarith) _))                        (by norm_num), Real.log_rpow (by linarith)] at this                      have := Real.log_two_lt_d9; norm_num at *; linarith                    rw [div_le_div_iff₀ (by nlinarith)                      (Real.rpow_pos_of_pos (by linarith) (3 / 2))]                    refine (mul_le_mul_of_nonneg_right (pow_le_pow_left₀                      (Real.log_nonneg (by linarith)) h_log_bound 2)                      (by exact Real.rpow_nonneg (by linarith) _)).trans ?_                    ring_nf                    norm_num                    rw [← Real.rpow_natCast, ← Real.rpow_mul (by linarith),                      ← Real.rpow_add (by linarith)]                    norm_num                  have h_integrable :                      MeasureTheory.IntegrableOn (fun t ↦ 4 / t^(3/2 : ℝ)) (Set.Ioi T) := by                    have h_integrable :                        MeasureTheory.IntegrableOn (fun t ↦ t ^ (-3 / 2 : ℝ)) (Set.Ioi T) :=                      integrableOn_Ioi_rpow_of_lt (by norm_num) (by linarith)                    norm_num [div_eq_mul_inv] at *                    exact MeasureTheory.Integrable.const_mul (h_integrable.congr_fun                      (fun x hx ↦ by simp only []; rw [Real.rpow_neg (by linarith [hx.out])])                      measurableSet_Ioi) _                  refine h_integrable.mono' ?_ ?_                  · refine ContinuousOn.aestronglyMeasurable ?_ measurableSet_Ioi                    have hne : ∀ t ∈ Set.Ioi T, t ≠ 0 := fun t ht ↦ by linarith [ht.out]                    have hsq : ∀ t ∈ Set.Ioi T, t ^ 2 ≠ 0 := fun t ht ↦ pow_ne_zero 2 (hne t ht)                    fun_prop (discharger := assumption)                  · filter_upwards [MeasureTheory.ae_restrict_mem measurableSet_Ioi]                      with t ht using by                        rw [Real.norm_of_nonneg (by positivity)]                        exact h_bound t ht                rw [MeasureTheory.IntegrableOn, MeasureTheory.Measure.restrict_congr_set                  MeasureTheory.Ioi_ae_eq_Ici] at *                simp_all only [one_div, mem_Ioo, ofReal_inv, Complex.norm_mul, Complex.norm_div,                  norm_neg, log_neg_eq_log, even_two, Even.neg_pow]              have h_integrable : MeasureTheory.IntegrableOn (fun t ↦                  (Real.log (-t))^2 / (-t)^2) (Set.Iic (-T)) := by                convert h_integrable.comp_neg using 1; norm_num [Set.indicator]              simpa only [mul_div_assoc] using h_integrable.const_mul _            · filter_upwards [MeasureTheory.ae_restrict_mem measurableSet_Iic] with t ht                using hC₁ εinIoo Xgt3 Tgt3 t ht            · convert mul_le_mul_of_nonneg_left (hC₂ Tgt3) (show 0 ≤ C₁ * (X / ε) by                exact mul_nonneg hC₁_pos.le                  (div_nonneg (by positivity) (by linarith [εinIoo.1]))) using 1 <;> ring_nf              rw [← MeasureTheory.integral_const_mul, MeasureTheory.integral_Ici_eq_integral_Ioi,                ← neg_neg T, ← integral_comp_neg_Iic]              norm_num              ring_nf    obtain ⟨C, hC₀, hC⟩ := h_I1New_bound; use C / (2 * Real.pi)    refine ⟨by positivity, fun {ε X T} hε hX hT ↦ ?_⟩    simp_all [div_eq_mul_inv, mul_assoc, mul_comm, mul_left_comm]    ring_nf at *    convert! mul_le_mul_of_nonneg_right (hC hε.1 hε.2 hX hT)      (show (0 : ℝ) ≤ Real.pi⁻¹ * (1 / 2) by positivity) using 1    · simp only [I1New, SmoothedChebyshevIntegrand, norm_mul, norm_inv, Complex.norm_I,        Complex.norm_two, mul_one, one_mul, one_div]      rw [show ∀ a b : ℝ, (2 * a)⁻¹ * b = b * (a⁻¹ * 2⁻¹) by intro _ _; ring]      congr 1      · apply congr_arg        apply MeasureTheory.setIntegral_congr_fun measurableSet_Iic fun t _ ↦ by          rw [show (↑t : ℂ) * I = I * ↑t by ring, div_eq_mul_inv, neg_mul,              show (↑(Real.log X)⁻¹ : ℂ) = (↑(Real.log X))⁻¹ from Complex.ofReal_inv _]          ring      · rw [show ‖(↑π : ℂ)‖ = π from (RCLike.norm_ofReal π).trans (abs_of_pos Real.pi_pos)]    · ring