CH2.shift_downwards_phi_diff

theorem shift_downwards_phi_diff (ν ε : ℝ) (hν : ν > 0) (t : ℝ)    (ht_pole : t ≠ ν / (2 * π)) :    Phi_circ ν ε (-1 - I * t) - Phi_star ν ε (-1 - I * t) = -Phi_star ν ε (-I * t) := by  have h_circ_periodic := Phi_circ_periodic ν ε  have h_re : (-2 : ℂ) * ↑π * I * (-I * ↑t) + ↑ν ≠ 0 := by    intro h    apply_fun Complex.re at h    rw [w_re] at h    simp at h    apply ht_pole    field_simp [Real.pi_pos.ne.symm]    linarith [Real.pi_pos]  have h_im (m : ℤ) (hm : m ≠ 0) : (-2 : ℂ) * ↑π * I * (-I * ↑t - ↑m) + ↑ν ≠ 0 := by    intro h    apply_fun Complex.im at h    simp [Real.pi_pos.ne.symm, hm] at h  have h_circ : Phi_circ ν ε (-1 - I * t) = Phi_circ ν ε (-I * t) := by    rw [show -I * t = (-1 - I * t) + 1 by ring, h_circ_periodic]  have haff : Phi_star ν ε (-1 - I * t) =      Phi_star ν ε (-I * t) + Phi_circ ν ε (-I * t) := by    have h := phi_star_affine_periodic ν ε hν (-I * t) 1 h_re (h_im 1 (by norm_num))    simp only [Int.cast_one, one_mul] at h    ring_nf at h ⊢    exact h  rw [h_circ, haff]  ring