CH2.horizontal_integral_phi_fourier_vanish

lemma horizontal_integral_phi_fourier_vanish (ν ε x a b : ℝ) (hν : ν > 0) (hx : x < 0)    (hab_in : Set.Icc a b ⊆ Set.Icc (-1) 1) (hab : a ≤ b)    (f : ℂ → ℂ)    (hf_anal : ∀ T : ℝ, T ≥ 1 → ContinuousOn f (Rectangle (↑a) (↑b + I * ↑T)))    (hf_bound : ∀ T : ℝ, T ≥ 1 → ∀ t ∈ Set.Icc a b, ‖f (t + I * T)‖ ≤ (‖Phi_circ ν ε (t + I * T)‖ + ‖Phi_star ν ε (t + I * T)‖) * ‖E (-(t + I * T) * x)‖) :    Filter.Tendsto (fun T : ℝ ↦ ∫ t in a..b, f (t + I * T)) Filter.atTop (nhds 0) := by  obtain ⟨C, hC⟩ := phi_bound_upwards ν ε hν  have h_int_bound (T : ℝ) (hT : T ≥ 1) : ‖∫ t in a..b, f (t + I * T)‖ ≤ (b - a) * C * (T + 1) * Real.exp (2 * π * x * T) := by    calc ‖∫ t in a..b, f (↑t + I * ↑T)‖      _ ≤ ∫ t in a..b, ‖f (↑t + I * ↑T)‖ := intervalIntegral.norm_integral_le_integral_norm hab      _ ≤ ∫ t in a..b, C * (T + 1) * Real.exp (2 * π * x * T) := by          apply intervalIntegral.integral_mono_on hab          · refine ContinuousOn.intervalIntegrable ?_            refine ContinuousOn.norm ?_            rw [Set.uIcc_of_le hab]            have hg : Continuous (fun t : ℝ ↦ (↑t : ℂ) + I * ↑T) := by fun_prop            have h_seg_in : (fun t ↦ ↑t + I * ↑T) '' Set.Icc a b ⊆ Rectangle a (b + I * T) := by              intro z ⟨t, ht, hz⟩              subst hz              rw [mem_Rect (by simpa using hab) (by simpa using hT.trans' (by norm_num : (0 : ℝ) ≤ 1))]              simp only [Complex.add_re, Complex.ofReal_re, Complex.mul_re, Complex.I_re, Complex.I_im,                Complex.ofReal_im, Complex.add_im, Complex.mul_im, mul_zero, zero_mul, sub_zero, add_zero, zero_add]              exact ⟨ht.1, ht.2, by linarith, le_refl _⟩            exact (hf_anal T hT).mono h_seg_in |>.comp hg.continuousOn (Set.mapsTo_image _ _)          · exact intervalIntegrable_const          · intro t ht            specialize hf_bound T hT t ht            have h_phi := hC (↑t + I * T) (by simpa using hT) (hab_in (by simpa using ht))            calc ‖f (↑t + I * ↑T)‖              _ ≤ (‖Phi_circ ν ε (↑t + I * ↑T)‖ + ‖Phi_star ν ε (↑t + I * ↑T)‖) * ‖E (-(↑t + I * ↑T) * ↑x)‖ := hf_bound              _ = (‖Phi_circ ν ε (↑t + I * ↑T)‖ + ‖Phi_star ν ε (↑t + I * ↑T)‖) * Real.exp (2 * π * x * T) := by                  congr 1; dsimp [E]; rw [Complex.norm_exp]; simp; ring_nf              _ ≤ C * (T + 1) * Real.exp (2 * π * x * T) := by                  rw [Complex.add_im ↑t (I * ↑T)] at h_phi                  simpa using mul_le_mul_of_nonneg_right h_phi (Real.exp_nonneg _)      _ = (b - a) * (C * (T + 1) * Real.exp (2 * π * x * T)) := intervalIntegral.integral_const _      _ = (b - a) * C * (T + 1) * Real.exp (2 * π * x * T) := by ring  rw [tendsto_zero_iff_norm_tendsto_zero]  let h_decay : ℝ → ℝ := fun T' ↦ (b - a) * C * (T' + 1) * rexp (2 * π * x * T')  refine tendsto_of_tendsto_of_tendsto_of_le_of_le' (g := fun _ ↦ 0) (h := h_decay) tendsto_const_nhds ?_ ?_ ?_  · exact tendsto_T_plus_one_mul_exp_atTop_nhds_zero (by nlinarith [hx, Real.pi_pos]) ((b - a) * C)  · filter_upwards with T'; exact norm_nonneg _  · filter_upwards [Filter.eventually_ge_atTop 1] with T' hT    exact h_int_bound T' hT