CH2.phi_sum_norm_le_linear_halfplane

theorem phi_sum_norm_le_linear_halfplane (ν ε : ℝ) (hν : ν > 0) (T : ℝ) (hT : T ≥ 1) (up : Bool)    (hsafe : if up then T > -ν / (2 * π) else -T < -ν / (2 * π)) :    ∃ C, ∀ (z : ℂ), (if up then z.im ≥ T else z.im ≤ -T) → z.re ∈ Set.Icc (-1 : ℝ) 1 →      ‖Phi_circ ν ε z‖ + ‖Phi_star ν ε z‖ ≤ C * (|z.im| + 1) := by  cases up  · have hsafe' : -T < -ν / (2 * π) := by simpa using hsafe    obtain ⟨C₁, hC₁⟩ := ϕ_circ_bound_left ν ν ε (-T) hsafe'    obtain ⟨C₂, hC₂⟩ := ϕ_star_bound_left ν ν ε (-T) hν le_rfl hsafe'    use (max 0 C₁ + 2 * max 0 C₂)    intro z hz_im hz_re    have hz_im' : z.im ≤ -T := by simpa using hz_im    apply phi_sum_norm_le_of_component_bounds hz_re (hC₁ ν (Set.left_mem_Icc.mpr le_rfl) z hz_im')      (hC₂ ν (Set.left_mem_Icc.mpr le_rfl) z hz_im') |z.im| rfl (by linarith [abs_of_nonpos (show z.im ≤ 0 by linarith)])  · have hsafe' : T > -ν / (2 * π) := by simpa using hsafe    obtain ⟨C₁, hC₁⟩ := ϕ_circ_bound_right ν ν ε T hsafe'    obtain ⟨C₂, hC₂⟩ := ϕ_star_bound_right ν ν ε T hν le_rfl hsafe'    use (max 0 C₁ + 2 * max 0 C₂)    intro z hz_im hz_re    have hz_im' : z.im ≥ T := by simpa using hz_im    apply phi_sum_norm_le_of_component_bounds hz_re (hC₁ ν (Set.left_mem_Icc.mpr le_rfl) z hz_im')      (hC₂ ν (Set.left_mem_Icc.mpr le_rfl) z hz_im') |z.im| rfl (by linarith [abs_of_nonneg (show 0 ≤ z.im by linarith)])