Orthogonal exp of mem orthogonal

lemma orthogonal_exp_of_mem_orthogonal (f : ℝ → ℂ) (hf : MemHS f)    (hOrth : ∀ n : ℕ, ⟪HilbertSpace.mk (Q.eigenfunction_memHS n), HilbertSpace.mk hf⟫_ℂ = 0)    (c : ℝ) : ∫ x : ℝ, Complex.exp (Complex.I * c * x) *    (f x * Real.exp (- x^2 / (2 * Q.ξ^2))) = 0 := by  /- Rewriting the integrand as a limit. -/  have h1 (y : ℝ) : Filter.Tendsto (fun n => ∑ r ∈ range n,        (Complex.I * ↑c * ↑y) ^ r / r ! * (f y * Real.exp (- y^2 / (2 * Q.ξ^2))))      Filter.atTop (nhds (Complex.exp (Complex.I * c * y) *      (f y * Real.exp (- y^2 / (2 * Q.ξ^2))))) := by    simp_rw [← Finset.sum_mul]    apply Filter.Tendsto.mul_const    simp only [Complex.exp, Complex.exp']    exact CauSeq.tendsto_limit (Complex.exp' (Complex.I * c * y))  /- End of rewriting the integrand as a limit. -/  /- Rewriting the integral as a limit using dominated_convergence -/  have h1' : Filter.Tendsto (fun n => ∫ y : ℝ, ∑ r ∈ range n,      (Complex.I * ↑c * ↑y) ^ r / r ! * (f y * Real.exp (- y^2 / (2 * Q.ξ^2))))      Filter.atTop (nhds (∫ y : ℝ, Complex.exp (Complex.I * c * y) *      (f y * Real.exp (- y^2 / (2 * Q.ξ^2))))) := by    let bound : ℝ → ℝ := fun x => Real.exp (|c * x|) * norm (f x) *      (Real.exp (- x ^ 2 / (2 * Q.ξ^2)))    apply MeasureTheory.tendsto_integral_of_dominated_convergence bound    · intro n      refine aestronglyMeasurable_fun_sum (range n) fun r _ => ?_      exact (Continuous.aestronglyMeasurable (by fun_prop)).mul        ((aeStronglyMeasurable_of_memHS hf).mul (Continuous.aestronglyMeasurable (by fun_prop)))    · /- Prove the bound is integrable. -/      have hbound : bound = (fun x => Real.exp |c * x| * norm (f x) *          Real.exp (-(1/ (2 * Q.ξ^2)) * x ^ 2)) := by        simp only [neg_mul, bound]        funext x        congr        field_simp      rw [hbound]      apply HilbertSpace.exp_abs_mul_abs_mul_gaussian_integrable      · exact hf      · simp    · intro n      apply Filter.Eventually.of_forall      intro y      rw [← Finset.sum_mul]      simp only [Complex.ofReal_exp, Complex.ofReal_div, Complex.ofReal_neg,        Complex.ofReal_mul, Complex.ofReal_pow, Complex.ofReal_ofNat, norm_mul,        bound]      rw [mul_assoc]      conv_rhs =>        rw [mul_assoc]      have h1 : (norm (f y) * norm (Complex.exp (-(↑y ^ 2) / (2 * Q.ξ^2))))        = norm (f y) * Real.exp (-(y ^ 2) / (2 * Q.ξ^2)) := by        rw [Complex.norm_exp, show (-(↑y ^ 2) / (2 * (Q.ξ : ℂ)^2)) =          ((-y ^ 2 / (2 * Q.ξ^2) : ℝ) : ℂ) by push_cast; ring, Complex.ofReal_re]      rw [h1]      by_cases hf : norm (f y) = 0      · simp [hf]      rw [mul_le_mul_iff_left₀]      · have hnorm : ‖∑ i ∈ range n, (Complex.I * (↑c * ↑y)) ^ i / (i ! : ℂ)‖ ≤          Real.exp ‖Complex.I * (↑c * ↑y)‖ := by          refine (norm_sum_le_of_le _ fun i _ => le_of_eq ?_).trans            (Real.sum_le_exp_of_nonneg (norm_nonneg _) n)          rw [norm_div, norm_pow, RCLike.norm_natCast]        refine hnorm.trans_eq ?_        rw [Complex.norm_mul, Complex.norm_I, one_mul, Complex.norm_mul, Complex.norm_real,          Complex.norm_real, Real.norm_eq_abs, Real.norm_eq_abs, abs_mul]      · exact mul_pos ((norm_nonneg (f y)).lt_of_ne' hf) (Real.exp_pos _)    · apply Filter.Eventually.of_forall      intro y      exact h1 y  have h3b : (fun n => ∫ y : ℝ, ∑ r ∈ range n,      (Complex.I * ↑c * ↑y) ^ r / r ! *      (f y * Real.exp (- y^2 / (2 * Q.ξ^2)))) = fun (n : ℕ) => 0 := by    have key (r : ℕ) : (fun a => (Complex.I * ↑c * ↑a) ^ r / ↑r ! *        (f a * ↑(Real.exp (- a ^ 2 / (2 * Q.ξ^2)))))        = fun a => ((Complex.I * ↑c) ^ r / ↑r !) *        (a ^ r * (f a * ↑(Real.exp (- a ^ 2 / (2 * Q.ξ^2))))) := by      funext a      simp only [Complex.ofReal_exp, Complex.ofReal_div, Complex.ofReal_neg,        Complex.ofReal_mul, Complex.ofReal_pow, Complex.ofReal_ofNat]      ring    funext n    rw [MeasureTheory.integral_finsetSum]    · refine Finset.sum_eq_zero fun r _ => ?_      rw [key r, MeasureTheory.integral_const_mul,        Q.orthogonal_power_of_mem_orthogonal f hf hOrth r]      simp    · intro r _      rw [key r]      exact (Q.mul_power_integrable f hf r).const_mul _  rw [h3b] at h1'  apply tendsto_nhds_unique h1'  rw [tendsto_const_nhds_iff]