CH2.horizontal_integral_phi_fourier_vanish_downwards

lemma horizontal_integral_phi_fourier_vanish_downwards (ν ε 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 : ℝ) in Filter.atTop, ∀ (t : ℝ), 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, T₀, hT₀_bound, hC⟩ := phi_bound_downwards ν ε hν  obtain ⟨T_bound, hf_bound'⟩ := Filter.eventually_atTop.mp hf_bound  let T_max := max (max 1 T₀) T_bound  have h_int_bound (T : ℝ) (hT : T ≥ T_max) :      ‖∫ 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          · apply ContinuousOn.intervalIntegrable            · refine ContinuousOn.norm ?_              rw [Set.uIcc_of_le hab]              apply ContinuousOn.congr (f := f ∘ fun (x : ℝ) ↦ (x : ℂ) - I * (T : ℂ))              · apply ContinuousOn.comp                · exact hf_anal T (by linarith [hT, le_max_left (max 1 T₀) T_bound, le_max_left 1 T₀])                · exact (continuous_ofReal.sub continuous_const).continuousOn                · intro u hu                  simp only [Rectangle, ofReal_re, sub_re, mul_re, I_re, zero_mul, I_im, ofReal_im,                    mul_zero, sub_self, sub_zero, sub_im, mul_im, one_mul, zero_add, zero_sub]                  constructor                  · simp only [Set.mem_preimage, sub_re, ofReal_re, mul_re, I_re, zero_mul, I_im,                    ofReal_im, mul_zero, sub_self, sub_zero]                    rw [Set.uIcc_of_le hab]; exact hu                  · simp              · intro x _; rfl          · exact intervalIntegrable_const          · intro t ht            calc ‖f (↑t - I * ↑T)‖              _ ≤ (‖Phi_circ ν ε (↑t - I * ↑T)‖ + ‖Phi_star ν ε (↑t - I * ↑T)‖) * ‖E (-(↑t - I * ↑T) * ↑x)‖ := hf_bound' T (by linarith [hT, le_max_right (max 1 T₀) T_bound]) t ht              _ = (‖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 * (1 - (↑t - I * T).im) * Real.exp (-2 * π * x * T) := by                  apply mul_le_mul_of_nonneg_right _ (by positivity)                  norm_cast                  rw [show 1 - (↑t - I * ↑T).im = -(↑t - I * ↑T).im + 1 by ring]                  apply hC                  · simp                    linarith [hT, le_max_left (max 1 T₀) T_bound, le_max_right 1 T₀]                  · simp only [sub_re, ofReal_re, mul_re, I_re, zero_mul, I_im, ofReal_im,                    mul_zero, sub_self, sub_zero, Set.mem_Icc]                    exact_mod_cast hab_in ht              _ = C * (T + 1) * Real.exp (-2 * π * x * T) := by simp [Complex.sub_im]; ring_nf; simp      _ = (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)  · exact Filter.Eventually.of_forall fun T' ↦ norm_nonneg _  · exact (Filter.eventually_ge_atTop T_max).mono h_int_bound