Θ₄ term imag axis real

lemma Θ₄_term_imag_axis_real (n : ℤ) (t : ℝ) (ht : 0 < t) :    (Θ₄_term n ⟨I * t, by simp [ht]⟩).im = 0 := by  unfold Θ₄_term  change ((-1 : ℂ) ^ n * cexp (Real.pi * I * (n : ℂ) ^ 2 * (I * t))).im = 0  -- Simplify the exponent: π * I * n² * (I*t) = -π * n² * t  have hexpr : Real.pi * I * (n : ℂ) ^ 2 * (I * t) =      (-(Real.pi * (n : ℝ) ^ 2 * t) : ℝ) := by    have hI : I ^ 2 = -1 := I_sq    push_cast    ring_nf    simp only [hI]    ring  rw [hexpr]  -- Now we have (-1)^n * exp(real), both are real  have hexp_real : (cexp (-(Real.pi * (n : ℝ) ^ 2 * t) : ℝ)).im = 0 := exp_ofReal_im _  have hneg_one_real : ((-1 : ℂ) ^ n).im = 0 := neg_one_zpow_im_eq_zero n  simp only [Complex.mul_im, hneg_one_real, hexp_real, mul_zero, zero_mul, add_zero]