CH2.phi_sum_norm_le_of_component_bounds

lemma phi_sum_norm_le_of_component_bounds {ν ε : ℝ} {z : ℂ} (hz_re : z.re ∈ Set.Icc (-1 : ℝ) 1)    {C₁ C₂ : ℝ} (hC₁ : ‖Phi_circ ν ε z‖ ≤ C₁) (hC₂ : ‖Phi_star ν ε z‖ ≤ C₂ * (‖z‖ + 1))    (y : ℝ) (hy : y = |z.im|) (hy_ge : y ≥ 1) :    ‖Phi_circ ν ε z‖ + ‖Phi_star ν ε z‖ ≤ (max 0 C₁ + 2 * max 0 C₂) * (y + 1) := by  have h_norm : ‖z‖ ≤ y + 1 := by rw [hy]; exact Complex.norm_le_abs_im_add_one hz_re  set C₁' := max 0 C₁  set C₂' := max 0 C₂  have hC₁' : 0 ≤ C₁' := le_max_left 0 C₁  have hC₂' : 0 ≤ C₂' := le_max_left 0 C₂  have h1 : ‖Phi_circ ν ε z‖ ≤ C₁' := hC₁.trans (le_max_right 0 C₁)  have h2 : ‖Phi_star ν ε z‖ ≤ C₂' * (‖z‖ + 1) := hC₂.trans (mul_le_mul_of_nonneg_right (le_max_right 0 C₂) (by positivity))  calc ‖Phi_circ ν ε z‖ + ‖Phi_star ν ε z‖    _ ≤ C₁' + C₂' * (y + 2) := by        have h_z_bound : ‖z‖ + 1 ≤ y + 2 := by linarith [h_norm]        nlinarith [h1, h2, h_z_bound, hC₂']    _ ≤ (C₁' + 2 * C₂') * (y + 1) := by        have h_y_bound : y + 2 ≤ 2 * (y + 1) := by linarith [hy_ge]        nlinarith [h_y_bound, C₁', C₂', hC₁', hC₂']