CH2.phi_fourier_ray_bound

theorem phi_fourier_ray_bound (ν ε σ x : ℝ) (hν : ν > 0) (hsigma : σ ∈ Set.Icc (-1 : ℝ) 1)    (f : ℂ → ℂ) (hf : ∀ z, ‖f z‖ ≤ (‖Phi_circ ν ε z‖ + ‖Phi_star ν ε z‖) * ‖E (-z * x)‖) :    ∃ C, ∀ (y : ℝ), y ≥ 1 →      ‖f (σ + y * I)‖ ≤ C * (y + 1) * rexp (2 * π * x * y) := by  obtain ⟨Core, hCore⟩ := phi_bound_upwards ν ε hν  refine ⟨Core, fun y hy => ?_⟩  have h_exp_eq : ‖E (-(σ + y * I) * x)‖ = rexp (2 * π * x * y) := by    rw [E, Complex.norm_exp]    simp only [Complex.add_re, Complex.neg_re, Complex.mul_re, Complex.add_im, Complex.neg_im, Complex.mul_im,      Complex.I_re, Complex.I_im, Complex.ofReal_re, Complex.ofReal_im, Complex.re_ofNat, Complex.im_ofNat,      mul_zero, sub_zero, zero_mul, add_zero, mul_one]    norm_num    ring  refine (hf (σ + y * I)).trans ?_  rw [h_exp_eq]  simpa using mul_le_mul_of_nonneg_right (hCore (σ + y * I) (by simpa using hy) (by simpa using hsigma)) (Real.exp_nonneg _)