Real.fourierIntegral_convolution

lemma Real.fourierIntegral_convolution {f g : ℝ → ℂ} (hf : Integrable f) (hg : Integrable g) :    𝓕 (convolution f g (ContinuousLinearMap.mul ℂ ℂ) volume) = 𝓕 f * 𝓕 g := by  ext y  simp only [Pi.mul_apply, FourierTransform.fourier, MeasureTheory.convolution,    VectorFourier.fourierIntegral, ContinuousLinearMap.mul_apply']  have h_int : Integrable (fun p : ℝ × ℝ ↦ 𝐞 (-(y * p.1)) • (f p.2 * g (p.1 - p.2))) := by    simp only [Circle.smul_def, smul_eq_mul]    refine (Integrable.convolution_integrand (ContinuousLinearMap.mul ℂ ℂ) hf hg).bdd_mul      (c := 1) ?_ ?_    · exact (by continuity : Continuous _).aestronglyMeasurable    · filter_upwards with p; simp  calc ∫ v, 𝐞 (-(y * v)) • ∫ t, f t * g (v - t)      = ∫ v, ∫ t, 𝐞 (-(y * v)) • (f t * g (v - t)) := by        simp only [Circle.smul_def, smul_eq_mul, ← integral_const_mul]    _ = ∫ t, ∫ v, 𝐞 (-(y * v)) • (f t * g (v - t)) := integral_integral_swap h_int    _ = ∫ t, f t • ∫ v, 𝐞 (-(y * v)) • g (v - t) := by        simp only [Circle.smul_def, smul_eq_mul, mul_left_comm, integral_const_mul]    _ = ∫ t, f t • ∫ u, 𝐞 (-(y * (u + t))) • g u := by        congr 1; ext t        rw [← integral_add_right_eq_self (fun v ↦ 𝐞 (-(y * v)) • g (v - t)) t]; simp    _ = ∫ t, f t • ∫ u, (𝐞 (-(y * t)) * 𝐞 (-(y * u))) • g u := by        congr 2 with t; congr 1        simp only [mul_add, neg_add, mul_comm, Real.fourierChar.map_add_eq_mul]    _ = ∫ t, 𝐞 (-(y * t)) • f t • ∫ u, 𝐞 (-(y * u)) • g u := by        congr 1; ext t        simp only [mul_smul, Circle.smul_def, smul_eq_mul, integral_const_mul]; ring    _ = (∫ t, 𝐞 (-(y * t)) • f t) * ∫ u, 𝐞 (-(y * u)) • g u := by        simp only [Circle.smul_def, smul_eq_mul, ← mul_assoc, integral_mul_const]