Hilbert space for one dimension quantum mechanics

@[reducible, inline]

noncomputable abbrev QuantumMechanics.OneDimension.HilbertSpace : AddSubgroup (ℝ →ₘ[MeasureTheory.volume] ℂ)

The Hilbert space for a one dimensional quantum system is defined as the space of almost-everywhere equal equivalence classes of square integrable functions from ℝ to ℂ.

Equations

• QuantumMechanics.OneDimension.HilbertSpace = MeasureTheory.Lp ℂ 2 MeasureTheory.volume

def QuantumMechanics.OneDimension.HilbertSpace.MemHS (f : ℝ → ℂ) : Prop

The proposition MemHS f for a function f : ℝ → ℂ is defined to be true if the function f can be lifted to the Hilbert space.

Equations

• QuantumMechanics.OneDimension.HilbertSpace.MemHS f = MeasureTheory.MemLp f 2 MeasureTheory.volume

theorem QuantumMechanics.OneDimension.HilbertSpace.aeStronglyMeasurable_of_memHS {f : ℝ → ℂ} (h : MemHS f) : MeasureTheory.AEStronglyMeasurable f MeasureTheory.volume

theorem QuantumMechanics.OneDimension.HilbertSpace.memHS_iff {f : ℝ → ℂ} : MemHS f ↔ MeasureTheory.AEStronglyMeasurable f MeasureTheory.volume ∧ MeasureTheory.Integrable (fun (x : ℝ) => ‖f x‖ ^ 2) MeasureTheory.volume

A function f statisfies MemHS f if and only if it is almost everywhere strongly measurable, and square integrable.

theorem QuantumMechanics.OneDimension.HilbertSpace.aeEqFun_mk_mem_iff (f : ℝ → ℂ) (hf : MeasureTheory.AEStronglyMeasurable f MeasureTheory.volume) : MeasureTheory.AEEqFun.mk f hf ∈ HilbertSpace ↔ MemHS f

def QuantumMechanics.OneDimension.HilbertSpace.mk {f : ℝ → ℂ} (hf : MemHS f) : ↥HilbertSpace

Given a function f : ℝ → ℂ such that MemHS f is true via hf, then HilbertSpace.mk hf is the element of the HilbertSpace defined by f.

Equations

• QuantumMechanics.OneDimension.HilbertSpace.mk hf = ⟨MeasureTheory.AEEqFun.mk f ⋯, ⋯⟩

theorem QuantumMechanics.OneDimension.HilbertSpace.coe_hilbertSpace_memHS (f : ↥HilbertSpace) : MemHS ↑↑f

theorem QuantumMechanics.OneDimension.HilbertSpace.mk_surjective (f : ↥HilbertSpace) : ∃ (g : ℝ → ℂ) (hg : MemHS g), mk hg = f

theorem QuantumMechanics.OneDimension.HilbertSpace.coe_mk_ae {f : ℝ → ℂ} (hf : MemHS f) : ↑↑(mk hf) =ᵐ[MeasureTheory.volume] f

theorem QuantumMechanics.OneDimension.HilbertSpace.inner_mk_mk {f g : ℝ → ℂ} {hf : MemHS f} {hg : MemHS g} : inner (mk hf) (mk hg) = ∫ (x : ℝ), (starRingEnd ℂ) (f x) * g x

@[simp]

theorem QuantumMechanics.OneDimension.HilbertSpace.eLpNorm_mk {f : ℝ → ℂ} {hf : MemHS f} : MeasureTheory.eLpNorm (↑↑(mk hf)) 2 MeasureTheory.volume = MeasureTheory.eLpNorm f 2 MeasureTheory.volume

theorem QuantumMechanics.OneDimension.HilbertSpace.mem_iff' {f : ℝ → ℂ} (hf : MeasureTheory.AEStronglyMeasurable f MeasureTheory.volume) : MeasureTheory.AEEqFun.mk f hf ∈ HilbertSpace ↔ MeasureTheory.Integrable (fun (x : ℝ) => ‖f x‖ ^ 2) MeasureTheory.volume

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