CH2.tendsto_contour_shift

lemma tendsto_contour_shift {σ σ' : ℝ} {f : ℂ → ℂ}    (h_anal : ∀ (U : ℝ), U ≥ 0 → HolomorphicOn f (Rectangle σ (σ' + I * U)))    (htop : Filter.Tendsto (fun (y : ℝ) ↦ ∫ x in σ..σ', f (x + y * I)) Filter.atTop (nhds 0))    (hleft : IntegrableOn (fun (y : ℝ) ↦ f (σ + y * I)) (Set.Ici 0))    (hright : IntegrableOn (fun (y : ℝ) ↦ f (σ' + y * I)) (Set.Ici 0)) :    Filter.Tendsto (fun (U : ℝ) ↦ (I * ∫ t in Set.Icc 0 U, f (σ + I * t)) - (I * ∫ t in Set.Icc 0 U, f (σ' + I * t)))      Filter.atTop (nhds (∫ x in σ..σ', f x)) := by  have h_rect (U : ℝ) (hU : 0 ≤ U) :      RectangleIntegral f σ (σ' + I * U) =      (∫ x in σ..σ', f x) - (∫ x in σ..σ', f (x + U * I)) + (I * ∫ y in Set.Icc 0 U, f (σ' + I * y)) - (I * ∫ y in Set.Icc 0 U, f (σ + I * y)) := by    dsimp [RectangleIntegral, HIntegral, VIntegral]    have h1 : ∫ (x : ℝ) in σ..σ' + (0 * U - 1 * 0), f (↑x + 0 * I) = ∫ x in σ..σ', f ↑x := by      rw [show σ' + (0 * U - 1 * 0) = σ' by ring]; apply intervalIntegral.integral_congr; intro x _; simp    have h2 : ∫ (x : ℝ) in σ..σ' + (0 * U - 1 * 0), f (↑x + ↑(0 + (0 * 0 + 1 * U)) * I) = ∫ x in σ..σ', f (↑x + ↑U * I) := by      rw [show σ' + (0 * U - 1 * 0) = σ' by ring]; apply intervalIntegral.integral_congr; intro x _; ring_nf    have h3 : ∫ (y : ℝ) in 0..0 + (0 * 0 + 1 * U), f (↑(σ' + (0 * U - 1 * 0)) + ↑y * I) =        ∫ y in Set.Icc 0 U, f (↑σ' + I * ↑y) := by      rw [show 0 + (0 * 0 + 1 * U) = U by ring, show σ' + (0 * U - 1 * 0) = σ' by ring]      rw [intervalIntegral.integral_of_le hU, MeasureTheory.integral_Icc_eq_integral_Ioc]      congr 1; funext y; congr 1; ring    have h4 : ∫ (y : ℝ) in 0..0 + (0 * 0 + 1 * U), f (↑σ + ↑y * I) = ∫ y in Set.Icc 0 U, f (↑σ + I * ↑y) := by      rw [show 0 + (0 * 0 + 1 * U) = U by ring]      rw [intervalIntegral.integral_of_le hU, MeasureTheory.integral_Icc_eq_integral_Ioc]      congr 1; funext y; congr 1; ring    have h3' : ∫ (y : ℝ) in 0..U, f (↑σ' + ↑y * I) =        ∫ y in Set.Icc 0 U, f (↑σ' + I * ↑y) := by simpa [Complex.I_mul_re, Complex.I_mul_im] using h3    have h4' : ∫ (y : ℝ) in 0..U, f (↑σ + ↑y * I) =        ∫ y in Set.Icc 0 U, f (↑σ + I * ↑y) := by simpa [Complex.I_mul_im] using h4    simp only [Complex.I_mul_re, Complex.I_mul_im, Complex.ofReal_re, Complex.ofReal_im,      neg_zero, zero_add, add_zero]    rw [← h1, ← h2]    rw [h3', h4']    simp  have h_UpperU_zero : UpperUIntegral f σ σ' 0 = 0 := by    have h1 := RectangleIntegral_tendsTo_UpperU' htop hleft hright    have e : (↑σ + I * ↑(0:ℝ) : ℂ) = ↑σ := by simp    simp_rw [e] at h1    have h2 : Filter.Tendsto (fun (U : ℝ) ↦ RectangleIntegral f σ (σ' + I * U)) Filter.atTop (nhds 0) := by      apply tendsto_const_nhds.congr'      filter_upwards [Filter.eventually_ge_atTop 0] with U hU      exact (HolomorphicOn.vanishesOnRectangle (h_anal U hU) subset_rfl).symm    exact tendsto_nhds_unique h1 h2  have h_zero : Filter.Tendsto (fun (U : ℝ) ↦ RectangleIntegral f σ (σ' + I * U)) Filter.atTop (nhds 0) := by    have h1 := RectangleIntegral_tendsTo_UpperU' htop hleft hright    have e : (↑σ + I * ↑(0:ℝ) : ℂ) = ↑σ := by simp    simp_rw [e, h_UpperU_zero] at h1    exact h1  have h_lim := (tendsto_const_nhds (x := ∫ x in σ..σ', f x)).sub htop  have h_all := h_lim.sub h_zero  simp only [sub_zero] at h_all  refine Filter.Tendsto.congr' ?_ h_all  filter_upwards [Filter.eventually_ge_atTop 0] with U hU  rw [h_rect U hU]  ring