CH2.phi_bound_downwards

theorem phi_bound_downwards (ν ε : ℝ) (hν : ν > 0) :    ∃ C T₀, T₀ ≥ ν / (2 * π) + 1 ∧ ∀ (z : ℂ), z.im ≤ -T₀ → z.re ∈ Set.Icc (-1 : ℝ) 1 →      ‖Phi_circ ν ε z‖ + ‖Phi_star ν ε z‖ ≤ C * (-z.im + 1) := by  set T₀ := max 1 (ν / (2 * π) + 1) with hT₀_def  have h_safe : -T₀ < -ν / (2 * π) := by    have : ν / (2 * π) < T₀ := by      rw [hT₀_def]      exact (lt_add_one _).trans_le (le_max_right 1 (ν / (2 * π) + 1))    have h := neg_lt_neg this    field_simp at h ⊢    exact h  obtain ⟨C, hC⟩ := phi_sum_norm_le_linear_halfplane ν ε hν T₀ (le_max_left _ _) false h_safe  refine ⟨C, T₀, le_max_right _ _, fun z hz hz_re ↦ ?_⟩  specialize hC z (by simpa using hz) hz_re  have h_abs : |z.im| = -z.im := abs_of_nonpos (by    have : T₀ ≥ 1 := le_max_left 1 (ν / (2 * π) + 1)    linarith [hz])  rwa [h_abs] at hC