CH2.ϕ_star_bound_left

@[blueprint  "phi-star-bound-left"  (title := "Bound on $\\Phi^{\\pm,\\ast}_\\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,\star}_{\nu}(z)| \leq C (|z|+1)$.  -/)  (proof := /-- Similar to previous lemma. -/)  (latexEnv := "lemma")]theorem ϕ_star_bound_left (ν₀ ν₁ ε 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_left ν₀ ν₁ ε c hc  obtain ⟨M, hM⟩ : ∃ M : ℝ, ∀ ν ∈ Set.Icc ν₀ ν₁, ‖B ε ν‖ ≤ M := by    have hB_def : ∀ ν : ℝ, ν ≠ 0 →        B ε ν = ν * (Complex.cosh (ν / 2) / Complex.sinh (ν / 2) + ε) / 2 := by      exact B_ofReal_eq ε    have hB_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₁ hx₂        have hx_ne : x ≠ 0 := ne_of_gt (lt_of_lt_of_le hν₀ hx₁.1)        exact sinh_ofReal_half_ne_zero hx_ne hx₂    obtain ⟨M, hM⟩ := IsCompact.exists_bound_of_continuousOn      CompactIccSpace.isCompact_Icc hB_cont    refine ⟨M, fun ν hν => ?_⟩    specialize hB_def ν (by linarith [hν.1])    grind  have hB : ∀ ν ∈ Set.Icc ν₀ ν₁, ∀ z : ℂ, z.im ≤ c →      ‖B ε (-2 * Real.pi * I * z + ν)‖ ≤ (2 * Real.pi * ‖z‖ + ν₁) * C₁ := by    intro ν hν z hz    have hB_eq : B ε (-2 * Real.pi * I * z + ν) =        (-2 * Real.pi * I * z + ν) * Phi_circ ν ε z := by      unfold B Phi_circ      split_ifs <;> simp_all [Complex.ext_iff]      · rw [lt_div_iff₀] at hc <;> nlinarith [Real.pi_pos]      · constructor <;> ring    rw [hB_eq, norm_mul]    gcongr    · exact add_nonneg (mul_nonneg (mul_nonneg zero_le_two Real.pi_pos.le) (norm_nonneg _))        (by linarith)    · refine le_trans (norm_add_le _ _) ?_      norm_num [abs_of_nonneg Real.pi_pos.le]      cases abs_cases ν <;> linarith [hν.1, hν.2]    · exact hC₁ ν hν z hz  have hPhi_star_bound : ∀ ν ∈ Set.Icc ν₀ ν₁, ∀ z : ℂ, z.im ≤ c →      ‖Phi_star ν ε z‖ ≤ ((2 * Real.pi * ‖z‖ + ν₁) * C₁ + M) / (2 * Real.pi) := by    intros ν hν z hz    have h : ‖Phi_star ν ε z‖ ≤        (‖B ε (-2 * Real.pi * I * z + ν)‖ + ‖B ε ν‖) / (2 * Real.pi) := by      rw [CH2.Phi_star]      norm_num [abs_of_nonneg Real.pi_pos.le]      bound    exact h.trans (by gcongr <;> linarith [hB ν hν z hz, hM ν hν])  exact ⟨((2 * Real.pi * 0 + ν₁) * C₁ + M) / (2 * Real.pi) +    (2 * Real.pi * C₁) / (2 * Real.pi), fun ν hν z hz =>    le_trans (hPhi_star_bound ν hν z hz) (by      ring_nf; norm_num [Real.pi_pos.ne']      norm_num [mul_assoc, mul_comm, mul_left_comm, Real.pi_ne_zero]      linarith [        show 0 ≤ C₁ from le_trans (norm_nonneg _) (hC₁ ν hν z hz),        show 0 ≤ M from le_trans (norm_nonneg _) (hM ν hν),        show 0 ≤ C₁ * (ν₁ * (Real.pi⁻¹ * (‖z‖ * (1 / 2)))) from          mul_nonneg (le_trans (norm_nonneg _) (hC₁ ν hν z hz))            (mul_nonneg (by linarith) (mul_nonneg (inv_nonneg.2 Real.pi_pos.le)              (mul_nonneg (norm_nonneg _) (by norm_num)))),        show 0 ≤ M * (Real.pi⁻¹ * (‖z‖ * (1 / 2))) from by          apply mul_nonneg (le_trans (norm_nonneg _) (hM ν hν))          positivity      ])⟩