PhysLean Documentation

PhysLean.QuantumMechanics.OneDimension.HilbertSpace.Basic

Hilbert space for one dimension quantum mechanics #

source
@[reducible, inline]
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
Instances For
    source
    def QuantumMechanics.OneDimension.HilbertSpace.toBra :
    ↥HilbertSpace →ₗ⋆[ℂ] StrongDual ℂ ↥HilbertSpace

    The anti-linear map from the Hilbert space to it's dual.

    Equations
    Instances For
      source
      @[simp]
      theorem QuantumMechanics.OneDimension.HilbertSpace.toBra_apply (f g : ↥HilbertSpace) :
      (toBra f) g = inner ℂ f g
      source
      theorem QuantumMechanics.OneDimension.HilbertSpace.toBra_surjective :
      Function.Surjective ⇑toBra

      The anti-linear map, toBra, taking a ket to it's corresponding bra is surjective.

      source
      theorem QuantumMechanics.OneDimension.HilbertSpace.toBra_injective :
      Function.Injective ⇑toBra

      The anti-linear map, toBra, taking a ket to it's corresponding bra is injective.

      Member of the Hilbert space as a property #

      source
      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
      Instances For
        source
        theorem QuantumMechanics.OneDimension.HilbertSpace.aeStronglyMeasurable_of_memHS {f : ℝ → ℂ} (h : MemHS f) :
        MeasureTheory.AEStronglyMeasurable f MeasureTheory.volume
        source
        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 satisfies MemHS f if and only if it is almost everywhere strongly measurable, and square integrable.

        source
        @[simp]
        theorem QuantumMechanics.OneDimension.HilbertSpace.zero_memHS :
        MemHS 0
        source
        @[simp]
        theorem QuantumMechanics.OneDimension.HilbertSpace.zero_fun_memHS :
        MemHS fun (x : ℝ) => 0
        source
        theorem QuantumMechanics.OneDimension.HilbertSpace.memHS_add {f g : ℝ → ℂ} (hf : MemHS f) (hg : MemHS g) :
        MemHS (f + g)
        source
        theorem QuantumMechanics.OneDimension.HilbertSpace.memHS_smul {f : ℝ → ℂ} {c : ℂ} (hf : MemHS f) :
        MemHS (c • f)
        source
        theorem QuantumMechanics.OneDimension.HilbertSpace.memHS_of_ae {g : ℝ → ℂ} (f : ℝ → ℂ) (hf : MemHS f) (hfg : f =ᵐ[MeasureTheory.volume] g) :
        MemHS g

        Construction of elements of the Hilbert space #

        source
        theorem QuantumMechanics.OneDimension.HilbertSpace.aeEqFun_mk_mem_iff (f : ℝ → ℂ) (hf : MeasureTheory.AEStronglyMeasurable f MeasureTheory.volume) :
        MeasureTheory.AEEqFun.mk f hf ∈ HilbertSpace ↔ MemHS f
        source
        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
        Instances For
          source
          theorem QuantumMechanics.OneDimension.HilbertSpace.coe_hilbertSpace_memHS (f : ↥HilbertSpace) :
          MemHS ↑↑f
          source
          theorem QuantumMechanics.OneDimension.HilbertSpace.mk_surjective (f : ↥HilbertSpace) :
          ∃ (g : ℝ → ℂ) (hg : MemHS g), mk hg = f
          source
          theorem QuantumMechanics.OneDimension.HilbertSpace.coe_mk_ae {f : ℝ → ℂ} (hf : MemHS f) :
          ↑↑(mk hf) =ᵐ[MeasureTheory.volume] f
          source
          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
          source
          @[simp]
          theorem QuantumMechanics.OneDimension.HilbertSpace.eLpNorm_mk {f : ℝ → ℂ} {hf : MemHS f} :
          MeasureTheory.eLpNorm (↑↑(mk hf)) 2 MeasureTheory.volume = MeasureTheory.eLpNorm f 2 MeasureTheory.volume
          source
          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
          source
          theorem QuantumMechanics.OneDimension.HilbertSpace.mk_add {f g : ℝ → ℂ} {hf : MemHS f} {hg : MemHS g} :
          mk ⋯ = mk hf + mk hg
          source
          theorem QuantumMechanics.OneDimension.HilbertSpace.mk_smul {f : ℝ → ℂ} {c : ℂ} {hf : MemHS f} :
          mk ⋯ = c • mk hf
          source
          theorem QuantumMechanics.OneDimension.HilbertSpace.mk_eq_iff {f g : ℝ → ℂ} {hf : MemHS f} {hg : MemHS g} :
          mk hf = mk hg ↔ f =ᵐ[MeasureTheory.volume] g
          source
          theorem QuantumMechanics.OneDimension.HilbertSpace.ext_iff {f g : ↥HilbertSpace} :
          f = g ↔ ↑↑f =ᵐ[MeasureTheory.volume] ↑↑g