PhysLean Documentation

PhysLean.QuantumMechanics.DDimensions.SpaceDHilbertSpace.Basic

Hilbert space for quantum mechanics on Space d #

source
@[reducible, inline]
abbrev QuantumMechanics.SpaceDHilbertSpace (d : ℕ) :
AddSubgroup (Space d →ₘ[MeasureTheory.volume] ℂ)

The Hilbert space for single-particle quantum mechanics on Space d is defined to be L²(Space d, ℂ), the space of almost-everywhere equal equivalence classes of square-integrable functions from Space d to ℂ.

Equations
Instances For
    source
    def QuantumMechanics.SpaceDHilbertSpace.toBra {d : ℕ} :
    ↥(SpaceDHilbertSpace d) →ₗ⋆[ℂ] StrongDual ℂ ↥(SpaceDHilbertSpace d)

    The anti-linear map from the Hilbert space to its dual.

    Equations
    Instances For
      source
      @[simp]
      theorem QuantumMechanics.SpaceDHilbertSpace.toBra_apply {d : ℕ} (f g : ↥(SpaceDHilbertSpace d)) :
      (toBra f) g = inner ℂ f g
      source
      theorem QuantumMechanics.SpaceDHilbertSpace.toBra_surjective {d : ℕ} :
      Function.Surjective ⇑toBra

      The anti-linear map toBra taking a ket to its corresponding bra is surjective.

      source
      theorem QuantumMechanics.SpaceDHilbertSpace.toBra_injective {d : ℕ} :
      Function.Injective ⇑toBra

      The anti-linear map toBra taking a ket to its corresponding bra is injective.

      Member of the Hilbert space as a property #

      source
      def QuantumMechanics.SpaceDHilbertSpace.MemHS {d : ℕ} (f : Space d → ℂ) :
      Prop

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

      Equations
      Instances For
        source
        theorem QuantumMechanics.SpaceDHilbertSpace.aeStronglyMeasurable_of_memHS {d : ℕ} {f : Space d → ℂ} (h : MemHS f) :
        MeasureTheory.AEStronglyMeasurable f MeasureTheory.volume
        source
        theorem QuantumMechanics.SpaceDHilbertSpace.memHS_iff {d : ℕ} {f : Space d → ℂ} :
        MemHS f ↔ MeasureTheory.AEStronglyMeasurable f MeasureTheory.volume ∧ MeasureTheory.Integrable (fun (x : Space d) => ‖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.SpaceDHilbertSpace.zero_memHS {d : ℕ} :
        MemHS 0
        source
        @[simp]
        theorem QuantumMechanics.SpaceDHilbertSpace.zero_fun_memHS {d : ℕ} :
        MemHS fun (x : Space d) => 0
        source
        theorem QuantumMechanics.SpaceDHilbertSpace.memHS_add {d : ℕ} {f g : Space d → ℂ} (hf : MemHS f) (hg : MemHS g) :
        MemHS (f + g)
        source
        theorem QuantumMechanics.SpaceDHilbertSpace.memHS_const_smul {d : ℕ} {f : Space d → ℂ} {c : ℂ} (hf : MemHS f) :
        MemHS (c • f)
        source
        theorem QuantumMechanics.SpaceDHilbertSpace.memHS_of_ae {d : ℕ} {g : Space d → ℂ} (f : Space d → ℂ) (hf : MemHS f) (hfg : f =ᵐ[MeasureTheory.volume] g) :
        MemHS g

        Construction of elements of the Hilbert space #

        source
        theorem QuantumMechanics.SpaceDHilbertSpace.aeEqFun_mk_mem_iff {d : ℕ} (f : Space d → ℂ) (hf : MeasureTheory.AEStronglyMeasurable f MeasureTheory.volume) :
        MeasureTheory.AEEqFun.mk f hf ∈ SpaceDHilbertSpace d ↔ MemHS f
        source
        def QuantumMechanics.SpaceDHilbertSpace.mk {d : ℕ} {f : Space d → ℂ} (hf : MemHS f) :
        ↥(SpaceDHilbertSpace d)

        Given a function f : Space d → ℂ such that MemHS f is true via hf, SpaceDHilbertSpace.mk f is the element of the Hilbert space defined by f.

        Equations
        Instances For
          source
          theorem QuantumMechanics.SpaceDHilbertSpace.coe_hilbertSpace_memHS {d : ℕ} (f : ↥(SpaceDHilbertSpace d)) :
          MemHS ↑↑f
          source
          theorem QuantumMechanics.SpaceDHilbertSpace.mk_surjective {d : ℕ} (f : ↥(SpaceDHilbertSpace d)) :
          ∃ (g : Space d → ℂ) (hg : MemHS g), mk hg = f
          source
          theorem QuantumMechanics.SpaceDHilbertSpace.coe_mk_ae {d : ℕ} {f : Space d → ℂ} (hf : MemHS f) :
          ↑↑(mk hf) =ᵐ[MeasureTheory.volume] f
          source
          theorem QuantumMechanics.SpaceDHilbertSpace.inner_mk_mk {d : ℕ} {f g : Space d → ℂ} (hf : MemHS f) (hg : MemHS g) :
          inner ℂ (mk hf) (mk hg) = ∫ (x : Space d), (starRingEnd ℂ) (f x) * g x
          source
          @[simp]
          theorem QuantumMechanics.SpaceDHilbertSpace.eLpNorm_mk {d : ℕ} {f : Space d → ℂ} {hf : MemHS f} :
          MeasureTheory.eLpNorm (↑↑(mk hf)) 2 MeasureTheory.volume = MeasureTheory.eLpNorm f 2 MeasureTheory.volume
          source
          theorem QuantumMechanics.SpaceDHilbertSpace.mem_iff {d : ℕ} {f : Space d → ℂ} (hf : MeasureTheory.AEStronglyMeasurable f MeasureTheory.volume) :
          MeasureTheory.AEEqFun.mk f hf ∈ SpaceDHilbertSpace d ↔ MeasureTheory.Integrable (fun (x : Space d) => ‖f x‖ ^ 2) MeasureTheory.volume
          source
          @[simp]
          theorem QuantumMechanics.SpaceDHilbertSpace.mk_add {d : ℕ} {f g : Space d → ℂ} {hf : MemHS f} {hg : MemHS g} :
          mk ⋯ = mk hf + mk hg
          source
          @[simp]
          theorem QuantumMechanics.SpaceDHilbertSpace.mk_const_smul {d : ℕ} {f : Space d → ℂ} {c : ℂ} {hf : MemHS f} :
          mk ⋯ = c • mk hf
          source
          theorem QuantumMechanics.SpaceDHilbertSpace.mk_eq_iff {d : ℕ} {f g : Space d → ℂ} {hf : MemHS f} {hg : MemHS g} :
          mk hf = mk hg ↔ f =ᵐ[MeasureTheory.volume] g
          source
          theorem QuantumMechanics.SpaceDHilbertSpace.ext_iff {d : ℕ} {f g : ↥(SpaceDHilbertSpace d)} :
          f = g ↔ ↑↑f =ᵐ[MeasureTheory.volume] ↑↑g