CH2.ϕ_circ_bound_left

@[blueprint  "phi-circ-bound-left"  (title := "Bound on $\\Phi^{\\pm,\\circ}_\\nu$ from below")  (statement := /--  Let $0 < \nu_0 \leq \nu_1$ and $c < - \nu_1/2\pi$, then there exists $C$ such that for all $\nu \in [\nu_0, \nu_1]$, $\Im z \leq c$ one has $|\Phi^{\pm,\circ}_{\nu}(z)| \leq C$.  -/)  (proof := /-- Similar to previous lemma. -/)  (latexEnv := "lemma")]theorem ϕ_circ_bound_left (ν₀ ν₁ ε c : ℝ) (hc : c < -ν₁ / (2 * π)) :    ∃ C : ℝ, ∀ ν ∈ Set.Icc ν₀ ν₁, ∀ z : ℂ, z.im ≤ c → ‖Phi_circ ν ε z‖ ≤ C := by  set κ := -(ν₁ + 2 * Real.pi * c) / 2 with hκ_def  have hκ_pos : 0 < κ := by    rw [lt_div_iff₀] at hc <;> nlinarith [Real.pi_pos]  have hRe_w : ∀ ν ∈ Set.Icc ν₀ ν₁, ∀ z : ℂ, z.im ≤ c →      Complex.re ((-2 * Real.pi * Complex.I * z + (ν : ℂ)) / 2) ≤ -κ := by    norm_num [hκ_def]; intros; nlinarith [Real.pi_pos]  have hcoth_bound : ∀ z : ℂ, Complex.re z ≤ -κ →      ‖Complex.cosh z / Complex.sinh z‖ ≤        (Real.exp κ + Real.exp (-κ)) / (Real.exp κ - Real.exp (-κ)) := by    intros z hz    have hsinh : ‖Complex.sinh z‖ ≥ (Real.exp (-z.re) - Real.exp z.re) / 2 := by      norm_num [Complex.sinh, Complex.norm_def, Complex.normSq]      norm_num [Complex.exp_re, Complex.exp_im]      gcongr      refine Real.le_sqrt_of_sq_le ?_      nlinarith [Real.sin_sq_add_cos_sq z.im, Real.exp_pos z.re, Real.exp_pos (-z.re),        mul_pos (Real.exp_pos z.re) (Real.exp_pos (-z.re))]    have hcosh : ‖Complex.cosh z‖ ≤ (Real.exp z.re + Real.exp (-z.re)) / 2 := by      norm_num [Complex.cosh, Complex.exp_re, Complex.exp_im]      gcongr      exact le_trans (norm_add_le ..) (by norm_num [Complex.norm_exp])    rw [norm_div]    rw [div_le_div_iff₀] <;>      try linarith [Real.exp_pos κ, Real.exp_lt_exp.mpr (show -κ < κ by linarith)]    · have h_exp_bounds : Real.exp z.re ≤ Real.exp (-κ) ∧ Real.exp (-z.re) ≥ Real.exp κ :=        ⟨Real.exp_le_exp.mpr hz, Real.exp_le_exp.mpr (by linarith)⟩      nlinarith [Real.exp_pos κ, Real.exp_pos (-κ),        Real.exp_lt_exp.2 (show -κ < κ by linarith)]    · exact lt_of_lt_of_le        (div_pos (sub_pos.mpr (Real.exp_lt_exp.mpr (by linarith))) zero_lt_two) hsinh  use (1 / 2) * ((Real.exp κ + Real.exp (-κ)) / (Real.exp κ - Real.exp (-κ)) + |ε|)  intros ν hν z hz  have hcoth_w : ‖Complex.cosh ((-2 * Real.pi * Complex.I * z + (ν : ℂ)) / 2) /      Complex.sinh ((-2 * Real.pi * Complex.I * z + (ν : ℂ)) / 2)‖ ≤      (Real.exp κ + Real.exp (-κ)) / (Real.exp κ - Real.exp (-κ)) :=    hcoth_bound _ (hRe_w ν hν z hz)  have h_triangle : ‖(1 / 2) * (Complex.cosh ((-2 * Real.pi * Complex.I * z + (ν : ℂ)) / 2) /      Complex.sinh ((-2 * Real.pi * Complex.I * z + (ν : ℂ)) / 2) + ε)‖ ≤      (1 / 2) * ((Real.exp κ + Real.exp (-κ)) / (Real.exp κ - Real.exp (-κ)) + |ε|) := by    norm_num at *    exact le_trans (norm_add_le ..) (add_le_add (by simpa using hcoth_w) (by norm_num))  convert h_triangle using 1  unfold Phi_circ coth  norm_num [Complex.tanh_eq_sinh_div_cosh]