limiting_fourier_lim2_gt_zero

theorem limiting_fourier_lim2_gt_zero (A : ℝ) (ψ : W21) (hx : 0 < x) :    Tendsto (fun σ' ↦ A * ↑(x ^ (1 - σ')) *      ∫ u in Ici (-Real.log x), rexp (-u * (σ' - 1)) * 𝓕 (ψ : ℝ → ℂ) (u / (2 * π)))        (𝓝[>] 1) (𝓝 (A * ∫ u in Ici (-Real.log x), 𝓕 (ψ : ℝ → ℂ) (u / (2 * π)))) := by  obtain ⟨C, hC⟩ := decay_bounds_cor ψ  refine Tendsto.mul ?_ (tendsto_integral_filter_of_dominated_convergence _    (.of_forall fun _ ↦ (by continuity : Continuous _).aestronglyMeasurable) ?_    (limiting_fourier_lim2_aux x C) (.of_forall fun u ↦ ?_))  · suffices Tendsto (fun σ' : ℝ ↦ x ^ (1 - σ')) (𝓝[>] 1) (𝓝 1) by      simpa using ((continuous_ofReal.tendsto 1).comp this).const_mul ↑A    have : Tendsto (fun σ' : ℝ ↦ 1 - σ') (𝓝[>] 1) (𝓝 0) :=      tendsto_nhdsWithin_of_tendsto_nhds (by simpa using (continuous_id.tendsto (1 : ℝ)).const_sub 1)    simpa using tendsto_const_nhds.rpow this (Or.inl hx.ne')  · refine eventually_of_mem (Ioo_mem_nhdsGT_of_mem (by norm_num : (1 : ℝ) ∈ Set.Ico 1 2)) fun σ' hσ' ↦ ?_    obtain ⟨h1, h2⟩ := hσ'    rw [ae_restrict_iff' measurableSet_Ici]    refine .of_forall fun t ht ↦ ?_    simp only [norm_mul, neg_mul, ofReal_exp, ofReal_neg, ofReal_mul, ofReal_sub, ofReal_one,      norm_exp, neg_re, mul_re, ofReal_re, sub_re, one_re, ofReal_im, sub_im, one_im,      sub_self, mul_zero, sub_zero]    refine mul_le_mul ?_ (hC _) (norm_nonneg _) ((abs_nonneg x).trans (le_max_left _ _))    have hα0 : 0 ≤ σ' - 1 := by linarith    have hα1 : σ' - 1 ≤ 1 := by linarith    have hmul1 : (-x.log) * (σ' - 1) ≤ t * (σ' - 1) := mul_le_mul_of_nonneg_right ht hα0    calc Real.exp (-(t * (σ' - 1)))        ≤ Real.exp (x.log * (σ' - 1)) := Real.exp_monotone (by linarith)      _ ≤ max |x| 1 := by          by_cases hx1 : 1 ≤ x          · calc _ ≤ Real.exp x.log :=                Real.exp_monotone (mul_le_of_le_one_right (Real.log_nonneg hx1) hα1)              _ = |x| := by rw [Real.exp_log hx, abs_of_pos hx]              _ ≤ _ := le_max_left _ _          · calc _ ≤ 1 := (Real.exp_monotone (mul_nonpos_of_nonpos_of_nonneg                  ((Real.log_neg_iff hx).2 (by linarith)).le hα0)).trans_eq Real.exp_zero              _ ≤ _ := le_max_right _ _  · suffices Tendsto (fun n ↦ ((rexp (-u * (n - 1))) : ℂ)) (𝓝[>] 1) (𝓝 1) by simpa using this.mul_const _    refine Tendsto.mono_left ?_ nhdsWithin_le_nhds    have : Continuous (fun n ↦ ((rexp (-u * (n - 1))) : ℂ)) := by continuity    simpa using this.tendsto 1