PhysLean Documentation

PhysLean.QuantumMechanics.DDimensions.SpaceDHilbertSpace.SchwartzSubmodule

Schwartz submodule of the Hilbert space #

source
def QuantumMechanics.SpaceDHilbertSpace.schwartzIncl {d : ℕ} :
SchwartzMap (Space d) ℂ →L[ℂ] ↥(SpaceDHilbertSpace d)

The continuous linear map including Schwartz functions into SpaceDHilbertSpace d.

Equations
Instances For
    source
    @[reducible, inline]
    abbrev QuantumMechanics.SpaceDHilbertSpace.schwartzSubmodule (d : ℕ) :
    Submodule ℂ ↥(SpaceDHilbertSpace d)

    The submodule of SpaceDHilbertSpace d consisting of Schwartz functions.

    Equations
    Instances For
      source
      instance QuantumMechanics.SpaceDHilbertSpace.instCoeFunSubtypeAEEqFunSpaceComplexVolumeMemAddSubgroupSubmoduleSchwartzSubmoduleForall {d : ℕ} :
      CoeFun ↥(schwartzSubmodule d) fun (x : ↥(schwartzSubmodule d)) => Space d → ℂ
      Equations
      • One or more equations did not get rendered due to their size.
      source
      @[simp]
      theorem QuantumMechanics.SpaceDHilbertSpace.val_eq_coe {d : ℕ} (ψ : ↥(schwartzSubmodule d)) (x : Space d) :
      ↑↑↑ψ x = ↑↑↑ψ x
      source
      theorem QuantumMechanics.SpaceDHilbertSpace.schwartzSubmodule_dense (d : ℕ) :
      Dense ↑(schwartzSubmodule d)
      source
      def QuantumMechanics.SpaceDHilbertSpace.schwartzEquiv {d : ℕ} :
      SchwartzMap (Space d) ℂ ≃ₗ[ℂ] ↥(schwartzSubmodule d)

      The linear equivalence between the Schwartz functions 𝓢(Space d, ℂ) and the Schwartz submodule of SpaceDHilbertSpace d.

      Equations
      Instances For
        source
        theorem QuantumMechanics.SpaceDHilbertSpace.schwartzEquiv_coe_ae {d : ℕ} (f : SchwartzMap (Space d) ℂ) :
        ↑↑↑(schwartzEquiv f) =ᵐ[MeasureTheory.volume] ⇑f
        source
        theorem QuantumMechanics.SpaceDHilbertSpace.schwartzEquiv_inner {d : ℕ} (f g : SchwartzMap (Space d) ℂ) :
        inner ℂ (schwartzEquiv f) (schwartzEquiv g) = ∫ (x : Space d), (starRingEnd ℂ) (f x) * g x
        source
        theorem QuantumMechanics.SpaceDHilbertSpace.schwartzEquiv_ae_eq {d : ℕ} (f g : SchwartzMap (Space d) ℂ) (h : ↑↑↑(schwartzEquiv f) =ᵐ[MeasureTheory.volume] ↑↑↑(schwartzEquiv g)) :
        f = g