tendsto_integral_sin_mul_smul_atTop

theorem tendsto_integral_sin_mul_smul_atTop {f : ℝ → E} (hf : Integrable f) :    Filter.Tendsto (fun T : ℝ => ∫ v : ℝ, (Real.sin (T * v) : ℂ) • f v)      Filter.atTop (nhds 0) := by  let c : ℂ := (2 : ℂ)⁻¹ * I  have hneg := tendsto_integral_exp_neg_mul_I_smul_atTop (E := E) f  have hpos := tendsto_integral_exp_pos_mul_I_smul_atTop (E := E) f  have hdiff : Filter.Tendsto      (fun T : ℝ => (∫ v : ℝ, Complex.exp (-(((T * v : ℝ) : ℂ) * I)) • f v) -        ∫ v : ℝ, Complex.exp (((T * v : ℝ) : ℂ) * I) • f v)      Filter.atTop (nhds (0 - 0)) := hneg.sub hpos  have hscaled : Filter.Tendsto      (fun T : ℝ => c • ((∫ v : ℝ,          Complex.exp (-(((T * v : ℝ) : ℂ) * I)) • f v) -        ∫ v : ℝ, Complex.exp (((T * v : ℝ) : ℂ) * I) • f v))      Filter.atTop (nhds 0) := by    simpa [c] using hdiff.const_smul c  refine hscaled.congr' ?_  filter_upwards with T  have hneg_int := integrable_exp_neg_mul_I_smul (E := E) hf T  have hpos_int := integrable_exp_pos_mul_I_smul (E := E) hf T  rw [← integral_sub hneg_int hpos_int]  rw [← integral_smul]  congr with v  rw [← sub_smul]  rw [← smul_assoc]  congr 1  dsimp [c]  change ((2 : ℂ)⁻¹ * I) *      (Complex.exp (-(((T * v : ℝ) : ℂ) * I)) - Complex.exp (((T * v : ℝ) : ℂ) * I)) =    (Real.sin (T * v) : ℂ)  symm  rw [show (Real.sin (T * v) : ℂ) = Complex.sin ((T * v : ℝ) : ℂ) by simp]  field_simp  simpa [mul_comm, mul_left_comm, mul_assoc] using (Complex.two_sin ((T * v : ℝ) : ℂ))