Θ₂ imag axis re pos

lemma Θ₂_imag_axis_re_pos (t : ℝ) (ht : 0 < t) :    0 < (Θ₂ ⟨I * t, by simp [ht]⟩).re := by  -- Θ₂(it) = ∑ₙ exp(-π(n+1/2)²t) where each term is positive real  -- The sum of positive terms (at least one nonzero) is positive  let z : ℍ := ⟨I * t, by simp [ht]⟩  -- Summability of the complex series  have hsum : Summable fun n : ℤ => Θ₂_term n z := by    simp_rw [Θ₂_term_as_jacobiTheta₂_term]    apply Summable.mul_left    rw [summable_jacobiTheta₂_term_iff]    exact z.im_pos  -- Convert complex tsum to real part of tsum  unfold Θ₂  rw [Complex.re_tsum hsum]  -- Summability of the real series  have hsum_re : Summable fun n : ℤ => (Θ₂_term n z).re := by    obtain ⟨x, hx⟩ := hsum    exact ⟨x.re, Complex.hasSum_re hx⟩  -- Each term is positive  have hpos : ∀ n : ℤ, 0 < (Θ₂_term n z).re := fun n => Θ₂_term_imag_axis_re_pos n t ht  -- Use that sum of positive terms is positive  exact Summable.tsum_pos hsum_re (fun n => le_of_lt (hpos n)) 0 (hpos 0)