CH2.ϕ_circ_bound_right

@[blueprint  "phi-circ-bound-right"  (title := "Bound on $\\Phi^{\\pm,\\circ}_\\nu$ from above")  (statement := /--  Let $0 < \nu_0 \leq \nu_1$ and $c > - \nu_0/2\pi$, then there exists $C$ such that for all $\nu \in [\nu_0, \nu_1]$, $\Im z \geq c$ one has $|\Phi^{\pm,\circ}_{\nu}(z)| \leq C$.  -/)  (proof := /-- The function $\coth w = 1 + \frac{2}{e^{2w}-1}$ is bounded away from the imaginary line $\Re w = 0$, that is, it is bounded on $\Re w \geq \kappa$ and $\Re w \leq -\kappa$ for any $\kappa > 0$. The map $w(z) = \nu - 2\pi i z$ sends the line $\Im z = -\frac{\nu}{2\pi}$ to the imaginary line, and the region $\Im z \geq c$ is sent to $\Re w \geq 2\pi c + \nu$. -/)  (latexEnv := "lemma")]theorem ϕ_circ_bound_right (ν₀ ν₁ ε c : ℝ) (hc : c > -ν₀ / (2 * π)) :    ∃ C : ℝ, ∀ ν ∈ Set.Icc ν₀ ν₁, ∀ z : ℂ, z.im ≥ c → ‖Phi_circ ν ε z‖ ≤ C := by  let κ := Real.pi * c + ν₀ / 2  have hκ : κ > 0 := by    norm_num +zetaDelta at *    rw [div_lt_iff₀] at hc <;> nlinarith [Real.pi_pos]  have hcoth_bound : ∀ u : ℂ, u.re ≥ κ → ‖(Complex.tanh u)⁻¹‖ ≤ (Real.tanh κ)⁻¹ := by    intros u hu    have htanh_sq : ‖Complex.tanh u‖ ^ 2 ≥ (Real.sinh u.re / Real.cosh u.re) ^ 2 := by      have htanh_sq : ‖Complex.tanh u‖ ^ 2 = (Real.sinh u.re ^ 2 + Real.sin u.im ^ 2) /          (Real.cosh u.re ^ 2 - Real.sin u.im ^ 2) := by        norm_num [Complex.normSq, Complex.norm_def, Complex.exp_re, Complex.exp_im,          Complex.sinh, Complex.cosh, Complex.tanh]        field_simp        rw [Real.sq_sqrt <| by positivity, Real.sq_sqrt <| by positivity]        rw [Real.sinh_eq, Real.cosh_eq]; ring_nf        norm_num [Real.sin_sq, Real.exp_neg]; ring_nf        rw [show (-2 + Real.cos u.im ^ 2 * 4 + Real.exp u.re ^ 2 + (Real.exp u.re)⁻¹ ^ 2) =          (-1 / 2 + Real.cos u.im ^ 2 + Real.exp u.re ^ 2 * (1 / 4) +            (Real.exp u.re)⁻¹ ^ 2 * (1 / 4)) * 4 by ring]        norm_num; ring      field_simp      rw [htanh_sq, mul_div]      rw [le_div_iff₀]      · nlinarith only [Real.sin_sq_le_one u.im, Real.sinh_sq u.re]      · nlinarith only [Real.sin_sq_add_cos_sq u.im, Real.cosh_sq' u.re,          Real.sinh_pos_iff.mpr (show 0 < u.re by nlinarith [Real.pi_pos])]    have htanh_ge_tanhκ : Real.sinh u.re / Real.cosh u.re ≥ Real.sinh κ / Real.cosh κ := by      have htanh_ge_tanhκ : ∀ u v : ℝ, 0 ≤ u → u ≤ v →          Real.sinh u / Real.cosh u ≤ Real.sinh v / Real.cosh v := by        intros u v hu hv        rw [div_le_div_iff₀ (Real.cosh_pos _) (Real.cosh_pos _)]; ring_nf        rw [show v = u + (v - u) by ring, Real.sinh_add, Real.cosh_add]        ring_nf; norm_num [Real.sinh_sq]; ring_nf; aesop      exact htanh_ge_tanhκ _ _ hκ.le hu    simp_all only [ge_iff_le, norm_inv, Real.tanh_eq_sinh_div_cosh]    apply inv_anti₀ (div_pos (Real.sinh_pos_iff.mpr hκ) (Real.cosh_pos _))    calc Real.sinh κ / Real.cosh κ        _ ≤ Real.sinh u.re / Real.cosh u.re := htanh_ge_tanhκ        _ ≤ ‖Complex.tanh u‖ := by            rw [← Real.sqrt_sq (div_nonneg (Real.sinh_nonneg_iff.mpr              (hκ.le.trans hu)) (Real.cosh_pos _ |>.le))]            exact Real.sqrt_le_sqrt (by rw [Complex.sq_norm] at htanh_sq; exact htanh_sq)  use (1 / 2) * ((Real.tanh κ)⁻¹ + |ε|)  intros ν hν z hz  have h_w : ‖(Complex.tanh ((-2 * Real.pi * Complex.I * z + ν) / 2))⁻¹‖ ≤      (Real.tanh κ)⁻¹ := by    convert hcoth_bound _ _ using 2    simp only [Complex.div_re, Complex.add_re, Complex.mul_re,      Complex.ofReal_re, Complex.ofReal_im, Complex.I_re, Complex.I_im, Complex.add_im,      Complex.mul_im]    norm_num    have h1 := hν.1    have h2 : π * c ≤ π * z.im := mul_le_mul_of_nonneg_left hz (le_of_lt Real.pi_pos)    change π * c + ν₀ / 2 ≤ (2 * π * z.im + ν) * 2 / 4    linarith  unfold Phi_circ  norm_num [coth]  exact le_trans (norm_add_le _ _) (add_le_add (by simpa using h_w)    (by norm_num [Complex.norm_def, Complex.normSq]))