CH2.second_contour_limit

@[blueprint  "second-contour-limit"  (title := "Second contour limit")  (statement := /--\[-\int_{-\frac{1}{2}-i\infty}^{-\frac{1}{2}} \Phi^{\pm,\star}_{\nu}(z)\, e(-zx)\, dz - \int_{-\frac{1}{2}}^{0} \Phi^{\pm,\star}_{\nu}(z)\, e(-zx)\, dz = \int_0^{-i\infty} \Phi^{\pm,\star}_{\nu}(z)\, e(-zx)\, dz.\]  -/)  (proof := /-- Again by Cauchy's theorem and decay as $\Im z \to -\infty$ -/)  (latexEnv := "sublemma")  (discussion := 1086)]theorem second_contour_limit (ν ε : ℝ) (hν : ν > 0) (x : ℝ) (hx : x > 0) :    Filter.atTop.Tendsto (fun T : ℝ ↦      (-(I * ∫ t in Set.Icc 0 T, ((Phi_star ν ε (-1/2 - I * t)) * E (-(-1/2 - I * ↑t) * x))))        - (∫ t in Set.Icc (-1/2 : ℝ) 0, (Phi_star ν ε t * E (-t * x)))        + (I * ∫ t in Set.Icc 0 T, ((Phi_star ν ε (-I * t)) * E (-(-I * ↑t) * x))))      (nhds 0) := by  let f : ℂ → ℂ := fun z ↦ Phi_star ν ε z * E (-z * x)  have h_anal (T : ℝ) (hT : T ≥ 0) : HolomorphicOn f (Rectangle (↑(-1/2 : ℝ)) (↑(0 : ℝ) - I * ↑T)) := by    simpa only [f] using second_contour_integrand_holomorphicOn ν ε x T hT  have h_rect_zero (T : ℝ) (hT : T ≥ 0) : RectangleIntegral f (↑(-1/2 : ℝ)) (↑(0 : ℝ) - I * ↑T) = 0 :=    HolomorphicOn.vanishesOnRectangle (h_anal T hT) subset_rfl  have h_goal_eq_bottom (T : ℝ) (hT : 0 ≤ T) :      (-(I * ∫ t in Set.Icc 0 T, f (-1/2 - I * t)))        - (∫ t in Set.Icc (-1/2 : ℝ) 0, f t)        + (I * ∫ t in Set.Icc 0 T, f (-I * t)) =      - ∫ t in (-1/2 : ℝ)..0, f (t - I * T) := by    have := h_rect_zero T hT    simp only [RectangleIntegral, HIntegral, VIntegral, smul_eq_mul] at this    push_cast at this    simp only [neg_re, neg_im, mul_re, mul_im, I_re, I_im, ofReal_re, ofReal_im,      ofReal_neg, mul_zero, mul_one, add_zero,      sub_zero, zero_sub, neg_zero, mul_comm I] at this    have h1 : ∫ t in Set.Icc (0 : ℝ) T, f (-1 / 2 - I * t) = - ∫ y in 0..-T, f (-1 / 2 + I * y) := by      rw [MeasureTheory.integral_Icc_eq_integral_Ioc, ← intervalIntegral.integral_of_le hT]      ring_nf      simp_rw [show ∀ x : ℝ, f (-1/2 - I * ↑x) = f (-1/2 + I * ↑(-x)) from        fun x => by congr 1; push_cast; ring]      rw [intervalIntegral.integral_comp_neg (fun y => f (-1/2 + I * ↑y))]      rw [intervalIntegral.integral_symm, neg_zero]    have h2 : ∫ t in Set.Icc (0 : ℝ) T, f (- I * t) = - ∫ y in 0..-T, f (I * y) := by      rw [MeasureTheory.integral_Icc_eq_integral_Ioc, ← intervalIntegral.integral_of_le hT]      simp_rw [show ∀ t : ℝ, f (-I * ↑t) = f (I * ↑(-t)) from        fun t => by congr 1; push_cast; ring]      rw [intervalIntegral.integral_comp_neg (fun y => f (I * ↑y)),          intervalIntegral.integral_symm, neg_zero]    have h3 : ∫ t in Set.Icc (-1 / 2 : ℝ) (0 : ℝ), f t = ∫ x in (-1 / 2 : ℝ)..0, f x := by      rw [MeasureTheory.integral_Icc_eq_integral_Ioc, ← intervalIntegral.integral_of_le (by norm_num)]    calc      (-(I * ∫ t in Set.Icc 0 T, f (-1 / 2 - I * ↑t)) - ∫ (t : ℝ) in Set.Icc (-1 / 2) 0, f ↑t) +          I * ∫ (t : ℝ) in Set.Icc 0 T, f (-I * ↑t)        = (I * ∫ y in 0..-T, f (-1 / 2 + I * y)) - (∫ x in -1 / 2..0, f x) - (I * ∫ y in 0..-T, f (I * y)) := by          rw [h1, h2, h3]; ring      _ = - ∫ x in -1 / 2..0, f (x - I * T) := by          simp only [show ((-1 / 2 : ℂ)).re = -1 / 2 from by norm_num,                    show ((-1 / 2 : ℂ)).im = 0 from by norm_num,                    zero_mul, add_zero, zero_add, ofReal_zero] at this          have hI1 : ∫ (y : ℝ) in 0..-T, f ((y : ℂ) * I) =                    ∫ (y : ℝ) in 0..-T, f (I * (y : ℂ)) := by            congr 1; ext (y : ℝ); ring_nf          have hI2 : ∫ (y : ℝ) in 0..-T, f ((-1 / 2 : ℂ) + (y : ℂ) * I) =                    ∫ (y : ℝ) in 0..-T, f ((-1 / 2 : ℂ) + I * (y : ℂ)) := by            congr 1; ext (y : ℝ); ring_nf          have hI3 : ∫ (x : ℝ) in -1 / 2..0, f ((x : ℂ) + -(T : ℂ) * I) =                    ∫ (x : ℝ) in -1 / 2..0, f ((x : ℂ) - I * (T : ℂ)) := by            congr 1; ext (x : ℝ); ring_nf          rw [hI1] at this          push_cast at this          rw [hI2, hI3] at this          linear_combination -this  have h_bottom : Filter.Tendsto (fun T : ℝ ↦ ∫ t in (-1/2 : ℝ)..0, f (t - I * T))      Filter.atTop (nhds 0) :=    horizontal_integral_phi_fourier_vanish_downwards ν ε x (-1/2) 0 hν hx      (Set.Icc_subset_Icc (by norm_num) (by norm_num)) (by norm_num) f      (fun T hT ↦ (h_anal T (by linarith)).continuousOn)      (Filter.Eventually.of_forall fun T t _ ↦ by        simp only [f]; rw [norm_mul]        exact mul_le_mul_of_nonneg_right (le_add_of_nonneg_left (norm_nonneg _)) (norm_nonneg _))  refine Filter.Tendsto.congr'    (f₁ := fun (T : ℝ) ↦ - ∫ t in (-1/2 : ℝ)..0, f (↑t - I * ↑T)) ?_    (by simpa using h_bottom.neg)  filter_upwards [Filter.eventually_ge_atTop 0] with T hT  simp only [f] at h_goal_eq_bottom ⊢  exact (h_goal_eq_bottom T hT).symm