CH2.shift_upwards_phi_sum

theorem shift_upwards_phi_sum (ν ε : ℝ) (hν : ν > 0) (t : ℝ) (ht : 0 ≤ t) :    Phi_circ ν ε (1 + I * t) + Phi_star ν ε (1 + I * t) = Phi_star ν ε (I * t) := by  have h_re : (-2 : ℂ) * ↑π * I * (I * ↑t) + ↑ν ≠ 0 := by    intro h; apply_fun Complex.re at h; simp at h; nlinarith [Real.pi_pos, ht, hν]  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_shift (z : ℂ) : Phi_circ ν ε (z - 1) = Phi_circ ν ε z := by    have h := (Phi_circ_periodic ν ε (z - 1)).symm; rwa [sub_add_cancel] at h  have haff := phi_star_affine_periodic ν ε hν (I * ↑t) (-1) h_re (h_im (-1) (by norm_num))  simp only [Int.cast_neg, Int.cast_one, neg_mul, one_mul, sub_neg_eq_add] at haff  rw [show 1 + I * ↑t = I * ↑t + 1 by ring, ← h_circ_shift (I * ↑t + 1),      show I * ↑t + 1 - 1 = I * ↑t by ring, haff]; ring