CH2.fourier_real

@[blueprint  "fourier-real"  (title := "Fourier transform of $\\varphi$ real")  (statement := /--$\widehat{\varphi^{\pm}_{\nu}}(x)$ is real.  -/)  (proof := /-- This follows from the symmetries of $\varphi^{\pm}_{\nu}$. -/)  (latexEnv := "lemma")  (discussion := 1225)]theorem fourier_real (ν ε : ℝ) (hlam : ν ≠ 0) (x : ℝ) : (𝓕 (ϕ_pm ν ε) x).im = 0 := by  rw [varphi_fourier_ident ν ε hlam]  set I_pos := ∫ t in Set.Icc 0 (1 : ℝ),      (Phi_circ ν ε (↑t : ℂ) + Phi_star ν ε (↑t : ℂ)) * E (-(↑t : ℂ) * ↑x)  have h_conj : ∫ t in Set.Icc (-1 : ℝ) 0,      (Phi_circ ν ε (↑t : ℂ) - Phi_star ν ε (↑t : ℂ)) * E (-(↑t : ℂ) * ↑x) =      starRingEnd ℂ I_pos := by    rw [integral_neg_one_zero_eq_zero_one]    rw [show (starRingEnd ℂ) I_pos = ∫ t in Set.Icc 0 (1 : ℝ),        starRingEnd ℂ ((Phi_circ ν ε (↑t : ℂ) + Phi_star ν ε (↑t : ℂ)) * E (-(↑t : ℂ) * ↑x))      from integral_conj.symm]    apply MeasureTheory.setIntegral_congr_fun measurableSet_Icc    intro t _    simp only [Phi_star_conj_symm, Phi_circ_conj_symm, E_conj_symm, push_cast,           map_mul, map_add, neg_mul, neg_neg, sub_neg_eq_add]  simp only [Complex.add_im]  have hstar_im : (starRingEnd ℂ I_pos).im = -I_pos.im := by rw [Complex.conj_im]  linarith [h_conj ▸ hstar_im]