Guassians and the hilbert space

Gaussians

theorem QuantumMechanics.OneDimension.HilbertSpace.gaussian_integrable {b : ℝ} (c : ℝ) (hb : 0 < b) : MeasureTheory.Integrable (fun (x : ℝ) => ↑(Real.exp (-b * (x - c) ^ 2))) MeasureTheory.volume

theorem QuantumMechanics.OneDimension.HilbertSpace.gaussian_aestronglyMeasurable {b : ℝ} (c : ℝ) (hb : 0 < b) : MeasureTheory.AEStronglyMeasurable (fun (x : ℝ) => ↑(Real.exp (-b * (x - c) ^ 2))) MeasureTheory.volume

theorem QuantumMechanics.OneDimension.HilbertSpace.gaussian_memHS {b : ℝ} (c : ℝ) (hb : 0 < b) : MemHS fun (x : ℝ) => ↑(Real.exp (-b * (x - c) ^ 2))

theorem QuantumMechanics.OneDimension.HilbertSpace.exp_mul_gaussian_integrable (b c : ℝ) (hb : 0 < b) : MeasureTheory.Integrable (fun (x : ℝ) => Real.exp (c * x) * Real.exp (-b * x ^ 2)) MeasureTheory.volume

theorem QuantumMechanics.OneDimension.HilbertSpace.exp_abs_mul_gaussian_integrable (b c : ℝ) (hb : 0 < b) : MeasureTheory.Integrable (fun (x : ℝ) => Real.exp |c * x| * Real.exp (-b * x ^ 2)) MeasureTheory.volume

theorem QuantumMechanics.OneDimension.HilbertSpace.mul_gaussian_mem_Lp_one (f : ℝ → ℂ) (hf : MemHS f) (b c : ℝ) (hb : 0 < b) : MeasureTheory.MemLp (fun (x : ℝ) => f x * ↑(Real.exp (-b * (x - c) ^ 2))) 1 MeasureTheory.volume

theorem QuantumMechanics.OneDimension.HilbertSpace.mul_gaussian_mem_Lp_two (f : ℝ → ℂ) (hf : MemHS f) (b c : ℝ) (hb : 0 < b) : MeasureTheory.MemLp (fun (x : ℝ) => f x * ↑(Real.exp (-b * (x - c) ^ 2))) 2 MeasureTheory.volume

theorem QuantumMechanics.OneDimension.HilbertSpace.abs_mul_gaussian_integrable (f : ℝ → ℂ) (hf : MemHS f) (b c : ℝ) (hb : 0 < b) : MeasureTheory.Integrable (fun (x : ℝ) => ‖f x‖ * Real.exp (-b * (x - c) ^ 2)) MeasureTheory.volume

theorem QuantumMechanics.OneDimension.HilbertSpace.exp_mul_abs_mul_gaussian_integrable (f : ℝ → ℂ) (hf : MemHS f) (b c : ℝ) (hb : 0 < b) : MeasureTheory.Integrable (fun (x : ℝ) => Real.exp (c * x) * ‖f x‖ * Real.exp (-b * x ^ 2)) MeasureTheory.volume

theorem QuantumMechanics.OneDimension.HilbertSpace.exp_abs_mul_abs_mul_gaussian_integrable (f : ℝ → ℂ) (hf : MemHS f) (b c : ℝ) (hb : 0 < b) : MeasureTheory.Integrable (fun (x : ℝ) => Real.exp |c * x| * ‖f x‖ * Real.exp (-b * x ^ 2)) MeasureTheory.volume