CH2.third_contour_limit

@[blueprint  "third-contour-limit"  (title := "Third contour limit")  (statement := /--\[\int_0^{\frac{1}{2}} \Phi^{\pm,\star}_{\nu}(z)\, e(-zx)\, dz + \int_{\frac{1}{2}}^{\frac{1}{2}-i\infty} \Phi^{\pm,\star}_{\nu}(z)\, e(-zx)\, dz = -\int_{-i\infty}^{0} \Phi^{\pm,\star}_{\nu}(z)\, e(-zx)\, dz.\]  -/)  (proof := /-- Similar to previous. -/)  (latexEnv := "sublemma")  (discussion := 1087)]theorem third_contour_limit (ν ε : ℝ) (hν : ν > 0) (x : ℝ) (hx : x > 0) :    Filter.atTop.Tendsto (fun T:ℝ ↦      (∫ t in Set.Icc 0 (1/2:ℝ), (Phi_star ν ε t * E (-t * x)))        - (I * ∫ t in Set.Icc 0 T, ((Phi_star ν ε (1/2 - I * t)) * E (- (1/2 - I * ↑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 hf_anal : ∀ (U : ℝ), U ≥ 0 → HolomorphicOn f (Rectangle (0 : ℂ) (1/2 - I * U)) := by    intro U hU; exact third_contour_integrand_holomorphicOn ν ε x U hU  have h_bottom : Filter.Tendsto (fun T : ℝ ↦ ∫ t in (0:ℝ)..(1/2:ℝ), f (↑t - I * ↑T))      Filter.atTop (nhds 0) := by    apply horizontal_integral_phi_fourier_vanish_downwards ν ε x 0 (1/2) hν hx      (Set.Icc_subset_Icc (by norm_num) (by norm_num)) (by norm_num) f    · intro T hT      convert! (hf_anal T (by linarith)).continuousOn using 2      push_cast; rfl    · filter_upwards with T; intro t ht      simp only [f, norm_mul]      apply mul_le_mul_of_nonneg_right _ (norm_nonneg _)      linarith [norm_nonneg (Phi_circ ν ε (↑t - I * ↑T))]  have h_shift : Filter.Tendsto (fun (T : ℝ) ↦ (I * ∫ t in Set.Icc 0 T, f (1/2 - I * t)) - (I * ∫ t in Set.Icc 0 T, f (0 - I * t)))      Filter.atTop (nhds (∫ t in (0:ℝ)..(1/2:ℝ), f t)) := by    let σ : ℝ := 0    let σ' : ℝ := 1/2    have hf_anal_rect : ∀ (U : ℝ), U ≥ 0 → HolomorphicOn f (Rectangle (σ : ℂ) (σ' - I * U)) := by      intro U hU; convert! third_contour_integrand_holomorphicOn ν ε x U hU; simp [σ']    convert! tendsto_contour_shift_downwards (σ := σ) (σ' := σ') hf_anal_rect h_bottom    simp [σ']  convert ((tendsto_const_nhds (x := ∫ t in (0:ℝ)..(1/2:ℝ), f t)).sub h_shift).congr' ?_ using 1  · simp  · filter_upwards [] with T    rw [intervalIntegral.integral_of_le (by norm_num : (0:ℝ) ≤ 1/2),        ← MeasureTheory.integral_Icc_eq_integral_Ioc]    calc      (∫ (t : ℝ) in Set.Icc 0 (1 / 2), f t) - ((I * ∫ t in Set.Icc 0 T, f (1 / 2 - I * t)) - (I * ∫ t in Set.Icc 0 T, f (0 - I * t)))      _ = (∫ (t : ℝ) in Set.Icc 0 (1 / 2), Phi_star ν ε t * E (-t * x)) -          ((I * ∫ t in Set.Icc 0 T, Phi_star ν ε (1 / 2 - I * t) * E (-(1 / 2 - I * t) * x)) -          (I * ∫ t in Set.Icc 0 T, Phi_star ν ε (-I * t) * E (-(-I * t) * x))) := by        simp only [f]; simp only [zero_sub, neg_neg]        have hC : ∫ t in Set.Icc 0 T, Phi_star ν ε (-(I * ↑t)) * E (I * ↑t * ↑x) =            ∫ t in Set.Icc 0 T, Phi_star ν ε (-I * ↑t) * E (-(-I * ↑t) * ↑x) := by            congr 1; ext t; simp only [neg_mul, neg_neg]        rw [hC]      _ = (∫ (t : ℝ) in Set.Icc 0 (1 / 2), Phi_star ν ε t * E (-(x * t))) -          ((I * ∫ t in Set.Icc 0 T, Phi_star ν ε (1 / 2 - I * t) * E (x * (-1 / 2) + x * I * t)) -          (I * ∫ t in Set.Icc 0 T, Phi_star ν ε (-I * t) * E (x * I * t))) := by        congr 1        · apply MeasureTheory.integral_congr_ae; refine Filter.Eventually.of_forall (fun t ↦ ?_)          ring_nf        · congr 1          · apply congr_arg (fun z ↦ I * z)            apply MeasureTheory.integral_congr_ae; refine Filter.Eventually.of_forall (fun t ↦ ?_)            ring_nf          · apply congr_arg (fun z ↦ I * z)            apply MeasureTheory.integral_congr_ae; refine Filter.Eventually.of_forall (fun t ↦ ?_)            ring_nf      _ = _ := by        ring_nf