CH2.first_contour_bottom_vanishes

lemma first_contour_bottom_vanishes (ν ε : ℝ) (x : ℝ) (hx : x > 0) :    Filter.Tendsto (fun T : ℝ ↦ ∫ t in (-1/2 : ℝ)..1/2, (fun z ↦ Phi_circ ν ε z * E (-z * x)) (t - I * T))      Filter.atTop (nhds 0) := by  let f : ℂ → ℂ := fun z ↦ Phi_circ ν ε z * E (-z * x)  have h_f_bound : ∃ C : ℝ, ∃ T₀ : ℝ, T₀ ≥ ν / (2 * π) + 1 ∧ ∀ T : ℝ, T ≥ T₀ → ∀ t ∈ Set.Icc (-1/2 : ℝ) (1/2 : ℝ), ‖f (↑t - I * ↑T)‖ ≤ C * Real.exp (-2 * π * x * T) := by    obtain ⟨C₁, hC₁⟩ := ϕ_circ_bound_left ν ν ε (-(ν / (2 * π) + 1)) (by ring_nf; linarith)    refine ⟨C₁, ν / (2 * π) + 1, le_refl _, fun T hT t ht => ?_⟩    have h_phi : ‖Phi_circ ν ε (↑t - I * ↑T)‖ ≤ C₁ :=      hC₁ ν (Set.left_mem_Icc.mpr (le_refl _)) _ (by        simp only [Complex.sub_im, Complex.ofReal_im, Complex.mul_im, Complex.I_re, Complex.I_im,                    Complex.ofReal_re, mul_zero, zero_sub, zero_add]        linarith)    have h_E : ‖E (-(↑t - I * ↑T) * ↑x)‖ = rexp (-2 * π * x * T) := by      rw [E, Complex.norm_exp]      simp only [Complex.mul_re, Complex.neg_re, Complex.sub_re, Complex.sub_im, Complex.neg_im,                  Complex.mul_im, Complex.I_re, Complex.I_im, Complex.ofReal_re, Complex.ofReal_im,                  Complex.re_ofNat, Complex.im_ofNat, mul_zero, sub_zero, zero_mul, add_zero,                  mul_one, zero_sub, zero_add]      congr 1; ring    change ‖Phi_circ ν ε (↑t - I * ↑T) * E (-(↑t - I * ↑T) * ↑x)‖ ≤ C₁ * rexp (-2 * π * x * T)    rw [norm_mul, h_E]    exact mul_le_mul_of_nonneg_right h_phi (Real.exp_nonneg _)  obtain ⟨C, T₀, hT₀_ge, hC⟩ := h_f_bound  have h_int_le (T : ℝ) (hT : T > ν / (2 * π)) (hT_T₀ : T ≥ T₀) : ‖∫ t in -1 / 2..1 / 2, f (t - I * T)‖ ≤ C * Real.exp (-2 * π * x * T) := by    calc ‖∫ (t : ℝ) in -1 / 2..1 / 2, f (↑t - I * ↑T)‖      _ ≤ ∫ (t : ℝ) in -1 / 2..1 / 2, ‖f (↑t - I * ↑T)‖ :=          intervalIntegral.norm_integral_le_integral_norm (by norm_num)      _ ≤ ∫ (t : ℝ) in -1 / 2..1 / 2, C * Real.exp (-2 * π * x * T) := by          apply intervalIntegral.integral_mono_on (by norm_num)          · apply IntervalIntegrable.norm            rw [intervalIntegrable_iff_integrableOn_Icc_of_le (by norm_num)]            apply integrable_fourier_path (f := fun t ↦ Phi_circ ν ε (↑t - I * ↑T)) (p := fun t ↦ ↑t - I * ↑T)            · intro t _              have h_anal : AnalyticAt ℂ (Phi_circ ν ε) (↑t - I * ↑T) := by                apply Phi_circ.analyticAt_of_im_ne_pole                simp only [sub_im, ofReal_im, mul_im, I_re,                  mul_zero, I_im, ofReal_re, one_mul, zero_add, zero_sub, ne_eq]                intro h                rw [gt_iff_lt, ← neg_lt_neg_iff, h] at hT                ring_nf at hT                exact lt_irrefl _ hT              have key : ContinuousAt (fun s : ℝ ↦ Phi_circ ν ε ((s : ℂ) - I * ↑T)) t := by                rw [show (fun s : ℝ ↦ Phi_circ ν ε ((s : ℂ) - I * ↑T)) =                      Phi_circ ν ε ∘ (fun s : ℝ ↦ (s : ℂ) - I * ↑T) from rfl]                apply ContinuousAt.comp                · exact h_anal.continuousAt                · exact continuous_ofReal.continuousAt.sub continuousAt_const              exact key.continuousWithinAt            · fun_prop          · exact intervalIntegrable_const          · intro t ht; exact hC T hT_T₀ t ht      _ = C * Real.exp (-2 * π * x * T) := by          simp only [intervalIntegral.integral_const]; norm_num  have h_lim : Filter.Tendsto (fun T ↦ C * Real.exp (-2 * π * x * T)) Filter.atTop (nhds 0) := by    have hk : -2 * π * x < 0 := by nlinarith [hx, Real.pi_pos]    have h_vanish : Filter.Tendsto (fun T ↦ Real.exp ((-2 * π * x) * T)) Filter.atTop (nhds 0) := by      have hu : Filter.Tendsto (fun T ↦ (2 * π * x) * T) Filter.atTop Filter.atTop :=        Filter.tendsto_id.const_mul_atTop (by nlinarith [hx, Real.pi_pos])      have h0 := Real.tendsto_pow_mul_exp_neg_atTop_nhds_zero 0      simpa [Function.comp_def, pow_zero, neg_mul] using h0.comp hu    simpa only [mul_zero] using Filter.Tendsto.const_mul C h_vanish  rw [tendsto_zero_iff_norm_tendsto_zero]  apply squeeze_zero' (Filter.Eventually.of_forall (fun T ↦ norm_nonneg _))  · filter_upwards [Filter.eventually_ge_atTop T₀] with T hT_T₀    have hT_pole : T > ν / (2 * π) := by linarith [hT₀_ge]    exact h_int_le T hT_pole hT_T₀  · exact h_lim