CH2.ϕ_star_bound_right

@[blueprint  "phi-star-bound-right"  (title := "Bound on $\\Phi^{\\pm,\\ast}_\\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,\star}_{\nu}(z)| \leq C (|z|+1)$.  -/)  (proof := /-- The bound on $\Phi^{\pm,\star}_{\nu}$ follows from the bound on $\Phi^{\pm,\circ}_{\nu}$ by $\Phi^{\pm,\star}(z) = \frac{1}{2\pi i}\bigl(w\,\Phi^{\pm,\circ}(w) - \nu\,\Phi^{\pm,\circ}(\nu)\bigr)$. -/)  (latexEnv := "lemma")]theorem ϕ_star_bound_right (ν₀ ν₁ ε c : ℝ) (hν₀ : 0 < ν₀) (hν₁ : ν₀ ≤ ν₁) (hc : c > -ν₀ / (2 * π)) :    ∃ C : ℝ, ∀ ν ∈ Set.Icc ν₀ ν₁, ∀ z : ℂ, z.im ≥ c → ‖Phi_star ν ε z‖ ≤ C * (‖z‖ + 1) := by  obtain ⟨C₁, hC₁⟩ := ϕ_circ_bound_right ν₀ ν₁ ε c hc  obtain ⟨C₂, hC₂⟩ : ∃ C₂ : ℝ, ∀ ν ∈ Set.Icc ν₀ ν₁, ‖B ε ν‖ ≤ C₂ := by    have hB_def : ∀ ν ∈ Set.Icc ν₀ ν₁, B ε ν =        ν * (Complex.cosh (ν / 2) / Complex.sinh (ν / 2) + ε) / 2 := by      intro ν hν      exact B_ofReal_eq ε ν (by linarith [hν.1])    have h_cont : ContinuousOn        (fun ν : ℝ => ν * (Complex.cosh (ν / 2) / Complex.sinh (ν / 2) + ε) / 2)        (Set.Icc ν₀ ν₁) := by      refine ContinuousOn.div_const ?_ _      refine ContinuousOn.mul Complex.continuous_ofReal.continuousOn        (ContinuousOn.add ?_ continuousOn_const)      refine ContinuousOn.div ?_ ?_ ?_      · fun_prop      · fun_prop      · intro x hx        simpa using sinh_ofReal_half_ne_zero (by linarith [hx.1])    obtain ⟨C₂, hC₂⟩ := IsCompact.exists_bound_of_continuousOn      CompactIccSpace.isCompact_Icc h_cont    exact ⟨C₂, fun ν hν => by aesop⟩  have h_bound : ∀ ν ∈ Set.Icc ν₀ ν₁, ∀ z : ℂ, z.im ≥ c →      ‖Phi_star ν ε z‖ ≤        (‖z‖ * (2 * Real.pi * C₁) + ν₁ * C₁ + C₂) / (2 * Real.pi) := by    intro ν hν z hz    have h_norm_B : ‖B ε (-2 * Real.pi * I * z + ν)‖ ≤        ‖z‖ * (2 * Real.pi * C₁) + ν₁ * C₁ := by      have h1 : ‖B ε (-2 * Real.pi * I * z + ν)‖ ≤          ‖-2 * Real.pi * I * z + ν‖ * C₁ := by        by_cases h : -2 * Real.pi * I * z + ν = 0 <;>        simp_all only [gt_iff_lt, Set.mem_Icc, ge_iff_le, Phi_circ, one_div, norm_inv, and_imp, B,          ↓reduceIte,Complex.norm_mul, Complex.norm_ofNat, Complex.norm_div]        · norm_num [Complex.ext_iff] at h          rw [div_lt_iff₀] at hc <;> nlinarith [Real.pi_pos]        · have := hC₁ ν hν.1 hν.2 z hz          rw [mul_div_assoc]          exact mul_le_mul_of_nonneg_left (by linarith) (norm_nonneg _)      have h2 : ‖-2 * Real.pi * I * z + ν‖ ≤ 2 * Real.pi * ‖z‖ + ν₁ := by        refine le_trans (norm_add_le ..) ?_        norm_num [abs_of_nonneg Real.pi_pos.le]        cases abs_cases ν <;> linarith [hν.1, hν.2]      nlinarith [show 0 ≤ C₁ from le_trans (norm_nonneg _) (hC₁ ν hν z hz)]    have h_eq : ‖Phi_star ν ε z‖ =        ‖B ε (-2 * Real.pi * I * z + ν) - B ε ν‖ / (2 * Real.pi) := by      unfold Phi_star      norm_num [abs_of_nonneg Real.pi_pos.le]    exact h_eq ▸ div_le_div_of_nonneg_right      (le_trans (norm_sub_le ..) (add_le_add h_norm_B (hC₂ ν hν))) (by positivity)  use (|2 * Real.pi * C₁| + |ν₁ * C₁ + C₂|) / (2 * Real.pi)  intro ν hν z hz  convert le_trans (h_bound ν hν z hz) _ using 1  rw [div_mul_eq_mul_div]  rw [div_le_div_iff_of_pos_right (by positivity)]  cases abs_cases (2 * Real.pi * C₁) <;>    cases abs_cases (ν₁ * C₁ + C₂) <;>      nlinarith [norm_nonneg z, Real.pi_pos]