Eigenfunction square integrable

@[fun_prop]lemma eigenfunction_square_integrable (n : ℕ) :    MeasureTheory.Integrable (fun x => ‖Q.eigenfunction n x‖ ^ 2) := by  have h0 (x : ℝ) : Real.exp (- x ^ 2 / Q.ξ^2) =      Real.exp (- (1 /Q.ξ^2) * x ^ 2) := by    simp only [neg_mul, Real.exp_eq_exp]    ring  conv =>    enter [1, x]    rw [eigenfunction_point_norm_sq]    rw [physHermite_pow, h0]    enter [2, 1, 1, 1]    rw [← one_div_mul_eq_div]  apply MeasureTheory.Integrable.const_mul  apply guassian_integrable_polynomial_cons  simp