CH2.norm_Phi_lambda_neg_one_add_I_mul_le_of_pos

theorem norm_Phi_lambda_neg_one_add_I_mul_le_of_pos (lam ε y : ℝ) (hlam : 0 < lam)    (hε : ε = 1 ∨ ε = -1) (hy : 0 ≤ y) :    ‖Phi_lambda lam ε (-1 + I * (y : ℂ))‖ ≤ y := by  have hν : 0 < |lam| := abs_pos.mpr (ne_of_gt hlam)  have hphi :      Phi_lambda lam ε (-1 + I * (y : ℂ)) = -Phi_star |lam| ε (I * (y : ℂ)) := by    have hsign_lam : (Real.sign lam : ℂ) = 1 := by simp [Real.sign_of_pos hlam]    have hsign_re : (Real.sign ((-1 + I * (y : ℂ)).re) : ℂ) = -1 := by      simp [Real.sign_of_neg (by norm_num : (-1 : ℝ) < 0)]    rw [Phi_lambda]    rw [hsign_lam, hsign_re]    simp only [one_mul, neg_mul]    rw [show Phi_circ |lam| ε (-1 + I * ↑y) + -Phi_star |lam| ε (-1 + I * ↑y) =        Phi_circ |lam| ε (-1 + I * ↑y) - Phi_star |lam| ε (-1 + I * ↑y) by ring]    exact shift_upwards_phi_diff |lam| ε hν y hy  rw [hphi, norm_neg]  exact (norm_Phi_star_I_mul_le |lam| ε y hε).trans_eq (abs_of_nonneg hy)