Smoothed Chebyshev Pull2

@[blueprint  (title := "SmoothedChebyshevPull2")  (statement := /--  We have that  $$  I_{37} =  I_3 - I_4 + I_5 + I_6 + I_7  .  $$  -/)  (proof := /-- Mimic the proof of Lemma \ref{SmoothedChebyshevPull1}. -/)  (latexEnv := "lemma")]theorem SmoothedChebyshevPull2 {SmoothingF : ℝ → ℝ} {ε : ℝ} (ε_pos : 0 < ε) (ε_lt_one : ε < 1)    (X : ℝ) (_ : 3 < X)    {T : ℝ} (T_pos : 3 < T) {σ₁ σ₂ : ℝ}    (σ₂_pos : 0 < σ₂) (σ₁_lt_one : σ₁ < 1)    (σ₂_lt_σ₁ : σ₂ < σ₁)    (holoOn : HolomorphicOn (ζ' / ζ) ((Icc σ₁ 2) ×ℂ (Icc (-T) T) \ {1}))    (holoOn2 : HolomorphicOn (SmoothedChebyshevIntegrand SmoothingF ε X)      (Icc σ₂ 2 ×ℂ Icc (-3) 3 \ {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)    (diff_SmoothingF : ContDiff ℝ 1 SmoothingF) :    I₃₇ SmoothingF ε T X σ₁ =      I₃ SmoothingF ε T X σ₁ -      I₄ SmoothingF ε X σ₁ σ₂ +      I₅ SmoothingF ε X σ₂ +      I₆ SmoothingF ε X σ₁ σ₂ +      I₇ SmoothingF ε T X σ₁ := by  let z : ℂ := σ₂ - 3 * I  let w : ℂ := σ₁ + 3 * I  have σ₁_pos : 0 < σ₁ := by linarith  -- Step (1)  -- Show that the Rectangle is in a given subset of holomorphicity  have sub : z.Rectangle w ⊆ Icc σ₂ 2 ×ℂ Icc (-3) 3 \ {1} := by    -- for every point x in the Rectangle    intro x hx    constructor    · -- x is in the locus of holomorphicity      simp only [Rectangle, uIcc] at hx      rw [Complex.mem_reProdIm] at hx ⊢      obtain ⟨hx_re, hx_im⟩ := hx      -- the real part of x is in the correct interval      have hzw_re : z.re < w.re := by        simpa [z, w] using σ₂_lt_σ₁      have x_re_bounds : z.re ≤ x.re ∧ x.re ≤ w.re := by        exact interval_membership x.re z.re w.re hx_re hzw_re      have x_re_in_Icc : x.re ∈ Icc σ₂ 2 := by        have ⟨h_left, h_right⟩ := x_re_bounds        have h_left' : σ₂ ≤ x.re := by          simpa [z] using h_left        have h_right' : x.re ≤ 2 := by          apply le_trans h_right          have : w.re ≤ 2 := by            simp [w]            linarith          exact this        exact ⟨h_left', h_right'⟩      -- the imaginary part of x is in the correct interval      have hzw_im : z.im < w.im := by        norm_num [z, w]      have x_im_bounds : z.im ≤ x.im ∧ x.im ≤ w.im := by        exact interval_membership x.im z.im w.im hx_im hzw_im      have x_im_in_Icc : x.im ∈ Icc (-3) 3 := by        have ⟨h_left, h_right⟩ := x_im_bounds        have h_left' : -3 ≤ x.im := by          simpa [z] using h_left        have h_right' : x.im ≤ 3 := by          simpa [w] using h_right        exact ⟨h_left', h_right'⟩      exact ⟨x_re_in_Icc, x_im_in_Icc⟩    -- x is not in {1} by contradiction    · simp only [mem_singleton_iff]      -- x has real part less than 1      have x_re_upper: x.re ≤ σ₁ := by        simp only [Rectangle, uIcc] at hx        rw [Complex.mem_reProdIm] at hx        obtain ⟨hx_re, _⟩ := hx        -- the real part of x is in the interval        have hzw_re : z.re < w.re := by          simpa [z, w] using σ₂_lt_σ₁        have x_re_bounds : z.re ≤ x.re ∧ x.re ≤ w.re := by          exact interval_membership x.re z.re w.re hx_re hzw_re        have x_re_upper' : x.re ≤ w.re := x_re_bounds.2        have hw_re : w.re = σ₁ := by simp [w]        linarith      -- by contracdiction      have h_x_ne_one : x ≠ 1 := by        intro h_eq        have h_re : x.re = 1 := by rw [h_eq, Complex.one_re]        have h1 : 1 ≤ σ₁ := by          rw [← h_re]          exact x_re_upper        linarith      exact h_x_ne_one  have zero_over_box := HolomorphicOn.vanishesOnRectangle holoOn2 sub  have splitting : I₃₇ SmoothingF ε T X σ₁ =    I₃ SmoothingF ε T X σ₁ + I₅ SmoothingF ε X σ₁ + I₇ SmoothingF ε T X σ₁ := by    unfold I₃₇ I₃ I₅ I₇    apply verticalIntegral_split_three_finite'    · apply ContinuousOn.integrableOn_Icc      unfold SmoothedChebyshevIntegrand      apply ContinuousOn.mul      · apply ContinuousOn.mul        · apply SmoothedChebyshevPull2_aux1 σ₁_lt_one holoOn        · apply continuousOn_of_forall_continuousAt          intro t t_mem          have := Smooth1MellinDifferentiable diff_SmoothingF suppSmoothingF ⟨ε_pos, ε_lt_one⟩            SmoothingFnonneg mass_one (s := ↑σ₁ + ↑t * I) (by simpa)          simpa using realDiff_of_complexDiff _ this      · apply continuousOn_of_forall_continuousAt        intro t t_mem        apply ContinuousAt.comp        · refine continuousAt_const_cpow' ?_          intro h          have : σ₁ = 0 := by            have h_real : (↑σ₁ + ↑t * I).re = (0 : ℂ).re := by              rw [h]            simp only [add_re, ofReal_re, mul_re, I_re, mul_zero, ofReal_im, I_im, mul_one,              sub_self, add_zero, zero_re] at h_real            exact h_real          linarith        · -- continuity -- failed          apply ContinuousAt.add          · exact continuousAt_const          · apply ContinuousAt.mul            · apply continuous_ofReal.continuousAt            · exact continuousAt_const    · refine ⟨by linarith, by linarith, by linarith⟩  calc I₃₇ SmoothingF ε T X σ₁ =        I₃₇ SmoothingF ε T X σ₁ - (1 / (2 * π * I)) * (0 : ℂ) := by simp    _ = I₃₇ SmoothingF ε T X σ₁ - (1 / (2 * π * I)) *        (RectangleIntegral (SmoothedChebyshevIntegrand SmoothingF ε X) z w) := by rw [← zero_over_box]    _ = I₃₇ SmoothingF ε T X σ₁ - (1 / (2 * π * I)) *        (HIntegral (SmoothedChebyshevIntegrand SmoothingF ε X) z.re w.re z.im        - HIntegral (SmoothedChebyshevIntegrand SmoothingF ε X) z.re w.re w.im        + VIntegral (SmoothedChebyshevIntegrand SmoothingF ε X) w.re z.im w.im        - VIntegral (SmoothedChebyshevIntegrand SmoothingF ε X) z.re z.im w.im) := by      simp [RectangleIntegral]    _ = I₃₇ SmoothingF ε T X σ₁ -        ((1 / (2 * π * I)) * HIntegral (SmoothedChebyshevIntegrand SmoothingF ε X) z.re w.re z.im        - (1 / (2 * π * I)) * HIntegral (SmoothedChebyshevIntegrand SmoothingF ε X) z.re w.re w.im        + (1 / (2 * π * I)) * VIntegral (SmoothedChebyshevIntegrand SmoothingF ε X) w.re z.im w.im        - (1 / (2 * π * I)) *            VIntegral (SmoothedChebyshevIntegrand SmoothingF ε X) z.re z.im w.im) := by ring    _ = I₃₇ SmoothingF ε T X σ₁ - (I₄ SmoothingF ε X σ₁ σ₂    - (1 / (2 * π * I)) * HIntegral (SmoothedChebyshevIntegrand SmoothingF ε X) z.re w.re w.im    + (1 / (2 * π * I)) * VIntegral (SmoothedChebyshevIntegrand SmoothingF ε X) w.re z.im w.im    - (1 / (2 * π * I)) * VIntegral (SmoothedChebyshevIntegrand SmoothingF ε X) z.re z.im w.im) := by      simp only [one_div, mul_inv_rev, inv_I, neg_mul, HIntegral, sub_im, ofReal_im, mul_im,        re_ofNat, I_im, mul_one, im_ofNat, I_re, mul_zero, add_zero, zero_sub, ofReal_neg,        ofReal_ofNat, sub_re, ofReal_re, mul_re, sub_self, sub_zero, add_re, add_im, zero_add,        sub_neg_eq_add, I₄, sub_right_inj, add_left_inj, neg_inj, mul_eq_mul_left_iff, mul_eq_zero,        I_ne_zero, inv_eq_zero, ofReal_eq_zero, OfNat.ofNat_ne_zero, or_false, false_or, z, w]      left      rfl    _ = I₃₇ SmoothingF ε T X σ₁ - (I₄ SmoothingF ε X σ₁ σ₂    - I₆ SmoothingF ε X σ₁ σ₂    + (1 / (2 * π * I)) * VIntegral (SmoothedChebyshevIntegrand SmoothingF ε X) w.re z.im w.im    - (1 / (2 * π * I)) * VIntegral (SmoothedChebyshevIntegrand SmoothingF ε X) z.re z.im w.im) := by      simp only [one_div, mul_inv_rev, inv_I, neg_mul, HIntegral, add_im, ofReal_im, mul_im,        re_ofNat, I_im, mul_one, im_ofNat, I_re, mul_zero, add_zero, zero_add, ofReal_ofNat, sub_re,        ofReal_re, mul_re, sub_self, sub_zero, add_re, sub_neg_eq_add, sub_im, zero_sub, I₆, w, z]    _ = I₃₇ SmoothingF ε T X σ₁ - (I₄ SmoothingF ε X σ₁ σ₂    - I₆ SmoothingF ε X σ₁ σ₂    + I₅ SmoothingF ε X σ₁    - (1 / (2 * π * I)) * VIntegral (SmoothedChebyshevIntegrand SmoothingF ε X) z.re z.im w.im) := by      simp only [one_div, mul_inv_rev, inv_I, neg_mul, VIntegral, add_re, ofReal_re, mul_re,        re_ofNat, I_re, mul_zero, im_ofNat, I_im, mul_one, sub_self, add_zero, sub_im, ofReal_im,        mul_im, zero_sub, add_im, zero_add, smul_eq_mul, sub_re, sub_zero, sub_neg_eq_add, I₅,        w, z]    _ = I₃₇ SmoothingF ε T X σ₁ - (I₄ SmoothingF ε X σ₁ σ₂    - I₆ SmoothingF ε X σ₁ σ₂    + I₅ SmoothingF ε X σ₁    - I₅ SmoothingF ε X σ₂) := by      simp only [I₅, one_div, mul_inv_rev, inv_I, neg_mul, VIntegral, sub_re, ofReal_re, mul_re,        re_ofNat, I_re, mul_zero, im_ofNat, I_im, mul_one, sub_self, sub_zero, sub_im, ofReal_im,        mul_im, add_zero, zero_sub, add_im, zero_add, smul_eq_mul, sub_neg_eq_add, z, w]    --- starting from now, we split the integral `I₃₇` into `I₃ σ₂ + I₅ σ₁ + I₇ σ₁` using `verticalIntegral_split_three_finite`    _ = I₃ SmoothingF ε T X σ₁    + I₅ SmoothingF ε X σ₁    + I₇ SmoothingF ε T X σ₁    - (I₄ SmoothingF ε X σ₁ σ₂    - I₆ SmoothingF ε X σ₁ σ₂    + I₅ SmoothingF ε X σ₁    - I₅ SmoothingF ε X σ₂) := by      rw [splitting]    _ = I₃ SmoothingF ε T X σ₁    - I₄ SmoothingF ε X σ₁ σ₂    + I₅ SmoothingF ε X σ₂    + I₆ SmoothingF ε X σ₁ σ₂    + I₇ SmoothingF ε T X σ₁ := by      ring