CH2.norm_Phi_star_neg_I_mul_le

theorem norm_Phi_star_neg_I_mul_le (ν ε t : ℝ) (hε : ε = 1 ∨ ε = -1) :    ‖Phi_star ν ε (-I * (t : ℂ))‖ ≤ |t| := by  have hphi : Phi_star ν ε (-I * (t : ℂ)) =      (B ε ((ν - 2 * π * t : ℝ) : ℂ) - B ε (ν : ℂ)) / (2 * (π : ℂ) * I) := by    rw [Phi_star]    congr 2    · congr 1      push_cast      ring_nf      simp [Complex.I_sq]  rw [hphi, norm_div, norm_B_sub_ofReal]  have hB := B_real_lipschitz_of_pm (ε := ε) (a := ν - 2 * π * t) (b := ν) hε  have hden : ‖(2 : ℂ) * (π : ℂ) * I‖ = 2 * π := by    rw [norm_mul, norm_mul, Complex.norm_ofNat, Complex.norm_real, Real.norm_eq_abs,      abs_of_pos Real.pi_pos, Complex.norm_I]    norm_num  rw [hden]  have hden_pos : 0 < 2 * π := mul_pos (by norm_num) Real.pi_pos  rw [div_le_iff₀ hden_pos]  calc |(B ε ↑(ν - 2 * π * t)).re - (B ε ↑ν).re|      ≤ |ν - 2 * π * t - ν| := hB    _ = |-(2 * π * t)| := by ring_nf    _ = |2 * π * t| := by rw [abs_neg]    _ = (2 * π) * |t| := by      rw [abs_mul, abs_mul, abs_of_pos (by norm_num : (0 : ℝ) < 2),        abs_of_pos Real.pi_pos]    _ = |t| * (2 * π) := by ring