limiting_fourier_lim3

theorem limiting_fourier_lim3 (hG : ContinuousOn G {s | 1 ≤ s.re}) (ψ : CS 2 ℂ) (hx : 1 ≤ x) :    Tendsto (fun σ' : ℝ ↦ ∫ t : ℝ, G (σ' + t * I) * ψ t * x ^ (t * I)) (𝓝[>] 1)      (𝓝 (∫ t : ℝ, G (1 + t * I) * ψ t * x ^ (t * I))) := by   by_cases hh : tsupport ψ = ∅  · simp [tsupport_eq_empty_iff.mp hh]  obtain ⟨a₀, ha₀⟩ := Set.nonempty_iff_ne_empty.mpr hh   let S : Set ℂ := reProdIm (Icc 1 2) (tsupport ψ)  have l1 : IsCompact S := by    refine Metric.isCompact_iff_isClosed_bounded.mpr ⟨?_, ?_⟩    · exact isClosed_Icc.reProdIm (isClosed_tsupport ψ)    · exact (Metric.isBounded_Icc 1 2).reProdIm ψ.h2.isBounded  have l2 : S ⊆ {s : ℂ | 1 ≤ s.re} := fun z hz => (mem_reProdIm.mp hz).1.1  have l3 : ContinuousOn (‖G ·‖) S := (hG.mono l2).norm  have l4 : S.Nonempty := ⟨1 + a₀ * I, by simp [S, mem_reProdIm, ha₀]⟩  obtain ⟨z, -, hmax⟩ := l1.exists_isMaxOn l4 l3  let MG := ‖G z‖  let bound (a : ℝ) : ℝ := MG * ‖ψ a‖   apply tendsto_integral_filter_of_dominated_convergence (bound := bound)  · apply eventually_of_mem (U := Icc 1 2) (Icc_mem_nhdsGT_of_mem (by simp)) ; intro u hu    apply Continuous.aestronglyMeasurable    apply Continuous.mul    · exact (hG.comp_continuous (by fun_prop) (by simp [hu.1])).mul ψ.h1.continuous    · apply Continuous.const_cpow (by fun_prop) ; simp ; linarith  · apply eventually_of_mem (U := Icc 1 2) (Icc_mem_nhdsGT_of_mem (by simp))    intro u hu    apply Eventually.of_forall ; intro v    by_cases h : v ∈ tsupport ψ    · have r1 : u + v * I ∈ S := by simp [S, mem_reProdIm, hu.1, hu.2, h]      have r2 := isMaxOn_iff.mp hmax _ r1      have r4 : (x : ℂ) ≠ 0 := by simp ; linarith      have r5 : arg x = 0 := by simp [arg_eq_zero_iff] ; linarith      have r3 : ‖(x : ℂ) ^ (v * I)‖ = 1 := by simp [norm_cpow_of_ne_zero r4, r5]      simp_rw [norm_mul, r3, mul_one]      exact mul_le_mul_of_nonneg_right r2 (norm_nonneg _)    · have : v ∉ Function.support ψ := fun a ↦ h (subset_tsupport ψ a)      simp at this ; simp [this, bound]   · suffices h : Continuous bound by exact h.integrable_of_hasCompactSupport ψ.h2.norm.mul_left    have := ψ.h1.continuous ; fun_prop  · apply Eventually.of_forall ; intro t    apply Tendsto.mul_const    apply Tendsto.mul_const    refine (hG (1 + t * I) (by simp)).tendsto.comp <| tendsto_nhdsWithin_iff.mpr ⟨?_, ?_⟩    · exact ((continuous_ofReal.tendsto _).add tendsto_const_nhds).mono_left nhdsWithin_le_nhds    · exact eventually_nhdsWithin_of_forall (fun x (hx : 1 < x) => by simp [hx.le])