SmoothedChebyshevPull3

@[blueprint  (title := "SmoothedChebyshevPull3")  (statement := /--    We have that    $$\psi_\varepsilon(X)=\mathcal{M}(\tilde{1}_\varepsilon)(1)\,X^1+I_1-I_2+I_3+I_4+I_5.$$  -/)  (proof := /--    Pull contours and accumulate the pole of $\zeta'/\zeta$ at $s=1$.  -/)]theorem SmoothedChebyshevPull3 {SmoothingF : ℝ → ℝ} {ε : ℝ} (ε_pos : 0 < ε)    (ε_lt_one : ε < 1)    (X : ℝ) (X_gt : 3 < X)    {T : ℝ} (T_pos : 0 < T) {σ' : ℝ}    (σ'_pos : 0 < σ') (σ'_lt_one : σ' < 1)    (holoOn : HolomorphicOn (ζ' / ζ) ((Icc σ' 2) ×ℂ (Icc (-T) T) \ {1}))    (suppSmoothingF : Function.support SmoothingF ⊆ Icc (1 / 2) 2)    (SmoothingFnonneg : ∀ x > 0, 0 ≤ SmoothingF x)    (mass_one : ∫ x in Ioi 0, SmoothingF x / x = 1)    (ContDiffSmoothingF : ContDiff ℝ 1 SmoothingF) :    SmoothedChebyshev SmoothingF ε X =      I1New SmoothingF ε X T -      I2New SmoothingF ε T X σ' +      I3New SmoothingF ε T X σ' +      I4New SmoothingF ε T X σ' +      I5New SmoothingF ε X T      + 𝓜 (fun x ↦ (Smooth1 SmoothingF ε x : ℂ)) 1 * X := by    unfold SmoothedChebyshev VerticalIntegral'    have X_eq_gt_one : 1 < 1 + (Real.log X)⁻¹ := by nth_rewrite 1 [← add_zero 1]; bound    have X_eq_lt_two : (1 + (Real.log X)⁻¹) < 2 := by        rw [← one_add_one_eq_two]; gcongr; exact inv_lt_one_of_one_lt₀ <| logt_gt_one X_gt.le    have X_eq_le_two : 1 + (Real.log X)⁻¹ ≤ 2 := X_eq_lt_two.le    rw [verticalIntegral_split_three (a := -T) (b := T)]    swap    ·   exact SmoothedChebyshevPull1_aux_integrable ε_pos ε_lt_one X_gt X_eq_gt_one            X_eq_le_two suppSmoothingF SmoothingFnonneg mass_one ContDiffSmoothingF    ·   have temp : ↑(1 + (Real.log X)⁻¹) = (1 : ℂ) + ↑(Real.log X)⁻¹ := by simp        unfold I1New; simp only [smul_eq_mul, mul_add, temp, sub_eq_add_neg, add_assoc,          add_left_cancel_iff]        unfold I5New; nth_rewrite 6 [add_comm]; simp only [← add_assoc]        rw [add_right_cancel_iff, ← add_right_inj (1 / (2 * ↑π * I) *            -VIntegral (SmoothedChebyshevIntegrand SmoothingF ε X) (1 + (Real.log X)⁻¹) (-T) T),            ← mul_add, ← sub_eq_neg_add, sub_self, mul_zero]        unfold VIntegral I2New I3New I4New        simp only [smul_eq_mul, temp, ← add_assoc, ← mul_neg, ← mul_add]        let fTempRR : ℝ → ℝ → ℂ := fun x ↦ fun y ↦            SmoothedChebyshevIntegrand SmoothingF ε X ((x : ℝ) + (y : ℝ) * I)        let fTempC : ℂ → ℂ := fun z ↦ fTempRR z.re z.im        have : ∫ (y : ℝ) in -T..T,            SmoothedChebyshevIntegrand SmoothingF ε X (1 + ↑(Real.log X)⁻¹ + ↑y * I) =            ∫ (y : ℝ) in -T..T, fTempRR (1 + (Real.log X)⁻¹) y := by unfold fTempRR; simp [temp]        rw [this]        have : ∫ (σ₀ : ℝ) in σ'..1 + (Real.log X)⁻¹,            SmoothedChebyshevIntegrand SmoothingF ε X (↑σ₀ - ↑T * I) =            ∫ (x : ℝ) in σ'..1 + (Real.log X)⁻¹, fTempRR x (-T) := by            unfold fTempRR; simp [ofReal_neg, neg_mul, sub_eq_add_neg]        rw [this]        have : ∫ (t : ℝ) in -T..T,            SmoothedChebyshevIntegrand SmoothingF ε X (↑σ' + ↑t * I) =            ∫ (y : ℝ) in -T..T, fTempRR σ' y := rfl        rw [this]        have : ∫ (σ₀ : ℝ) in σ'..1 + (Real.log X)⁻¹,            SmoothedChebyshevIntegrand SmoothingF ε X (↑σ₀ + ↑T * I) =            ∫ (x : ℝ) in σ'..1 + (Real.log X)⁻¹, fTempRR x T := rfl        rw [this]        have : (((I * -∫ (y : ℝ) in -T..T, fTempRR (1 + (Real.log X)⁻¹) y) +            -∫ (x : ℝ) in σ'..1 + (Real.log X)⁻¹, fTempRR x (-T)) +            I * ∫ (y : ℝ) in -T..T, fTempRR σ' y) +            ∫ (x : ℝ) in σ'..1 + (Real.log X)⁻¹, fTempRR x T =            -(2 * ↑π * I) * RectangleIntegral' fTempC (σ' - T * I) (1 + ↑(Real.log X)⁻¹ + T * I) := by            unfold RectangleIntegral' RectangleIntegral HIntegral VIntegral fTempC            simp only [mul_neg, one_div, mul_inv_rev, inv_I, neg_mul, sub_im, ofReal_im, mul_im,              ofReal_re, I_im, mul_one, I_re, mul_zero, add_zero, zero_sub, ofReal_neg, add_re,              neg_re, mul_re, sub_self, neg_zero, add_im, neg_im, zero_add, sub_re, sub_zero,              ofReal_inv, one_re, inv_re, normSq_ofReal, div_self_mul_self', one_im, inv_im,              zero_div, ofReal_add, ofReal_one, smul_eq_mul, neg_neg]            ring_nf            simp only [I_sq, neg_mul, one_mul, ne_eq, ofReal_eq_zero, pi_ne_zero, not_false_eq_true,              mul_inv_cancel_right₀, sub_neg_eq_add, I_pow_three]            ring_nf        rw [this]        field_simp        rw [mul_comm, eq_comm, neg_add_eq_zero]        have pInRectangleInterior : (Rectangle (σ' - ↑T * I) (1 + (Real.log X)⁻¹ + T * I) ∈ nhds 1) := by            refine rectangle_mem_nhds_iff.mpr <| mem_reProdIm.mpr ?_            simp only [sub_re, ofReal_re, mul_re, I_re, mul_zero, ofReal_im, I_im, mul_one, sub_self,                sub_zero, ofReal_inv, add_re, one_re, inv_re, normSq_ofReal, div_self_mul_self', add_zero,                sub_im, mul_im, zero_sub, add_im, one_im, inv_im, neg_zero, zero_div, zero_add]            constructor            · unfold uIoo; rw [min_eq_left (by linarith), max_eq_right (by linarith)]              exact mem_Ioo.mpr ⟨σ'_lt_one, by linarith⟩            · unfold uIoo; rw [min_eq_left (by linarith), max_eq_right (by linarith)]              exact mem_Ioo.mpr ⟨by linarith, by linarith⟩        apply ResidueTheoremOnRectangleWithSimplePole'        · simp; linarith        · simp; linarith        · simp only [one_div]; exact pInRectangleInterior        ·   apply DifferentiableOn.mul            ·   apply DifferentiableOn.mul                ·   simp only [re_add_im]                    have : (fun z ↦ -ζ' z / ζ z) = -(ζ' / ζ) := by ext; simp; ring                    rw [this]; apply DifferentiableOn.neg; apply holoOn.mono                    apply Set.sdiff_subset_sdiff_left; apply reProdIm_subset_iff'.mpr; left                    simp only [sub_re, ofReal_re, mul_re, I_re, mul_zero, ofReal_im, I_im, mul_one, sub_self,                        sub_zero, one_div, ofReal_inv, add_re, one_re, inv_re, normSq_ofReal,                        div_self_mul_self', add_zero, sub_im, mul_im, zero_sub, add_im, one_im, inv_im,                        neg_zero, zero_div, zero_add]                    constructor <;> apply uIcc_subset_Icc <;> constructor <;> linarith                ·   intro s hs; apply DifferentiableAt.differentiableWithinAt; simp only [re_add_im]                    apply Smooth1MellinDifferentiable ContDiffSmoothingF suppSmoothingF ⟨ε_pos, ε_lt_one⟩ SmoothingFnonneg mass_one                    have := mem_reProdIm.mp hs.1 |>.1                    simp only [sub_re, ofReal_re, mul_re, I_re, mul_zero, ofReal_im, I_im, mul_one, sub_self,                        sub_zero, one_div, ofReal_inv, add_re, one_re, inv_re, normSq_ofReal,                        div_self_mul_self', add_zero] at this                    rw [uIcc_of_le (by linarith)] at this; linarith [this.1]            ·   intro s hs; apply DifferentiableAt.differentiableWithinAt; simp only [re_add_im]                apply DifferentiableAt.const_cpow (by fun_prop); left; norm_cast; linarith        ·   let U : Set ℂ := Rectangle (σ' - ↑T * I) (1 + (Real.log X)⁻¹ + T * I)            let f : ℂ → ℂ := fun z ↦ -ζ' z / ζ z            let g : ℂ → ℂ := fun z ↦ 𝓜 (fun x ↦ ↑(Smooth1 SmoothingF ε x)) z * ↑X ^ z            unfold fTempC fTempRR SmoothedChebyshevIntegrand            simp only [re_add_im]            have g_holc : HolomorphicOn g U := by                intro u uInU                apply DifferentiableAt.differentiableWithinAt; simp only [g]                apply DifferentiableAt.mul                ·   apply Smooth1MellinDifferentiable ContDiffSmoothingF suppSmoothingF ⟨ε_pos, ε_lt_one⟩ SmoothingFnonneg mass_one                    simp only [ofReal_inv, U] at uInU; unfold Rectangle at uInU                    rw[Complex.mem_reProdIm] at uInU; have := uInU.1                    simp only [sub_re, ofReal_re, mul_re, I_re, mul_zero, ofReal_im, I_im, mul_one, sub_self,                        sub_zero, add_re, one_re, inv_re, normSq_ofReal, div_self_mul_self', add_zero] at this                    rw [uIcc_of_le (by linarith)] at this; linarith [this.1]                ·   unfold HPow.hPow instHPow                    apply DifferentiableAt.const_cpow differentiableAt_fun_id                    left; norm_cast; linarith            have f_near_p : (f - fun (z : ℂ) => 1 * (z - 1)⁻¹) =O[nhdsWithin 1 {1}ᶜ] (1 : ℂ → ℂ) := by                simp only [one_mul, f]; exact riemannZetaLogDerivResidueBigO            convert ResidueMult g_holc pInRectangleInterior f_near_p using 1            ext; simp [f, g]; ring