diff --git a/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/API-map.yaml b/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/API-map.yaml new file mode 100644 index 000000000..c356e0c08 --- /dev/null +++ b/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/API-map.yaml @@ -0,0 +1,99 @@ +version: v0.1 + +Title: Hilbert spaces on Space + +Overview: | + The Hilbert space on Space with measure μ is the $L^2$ space consisting of μ-a.e. equal + equivalence classes of complex functions which are square-integrable with respect to μ. + These Hilbert spaces are used extensively in non-relativistic quantum mechanics. + +ParentAPIs: + - Space (Physlib/SpaceAndTime/Space) + +References: + +Requirements: + + - description: > + Defines Hilbert spaces on Space as instances of MeasureTheory.Lp + with MeasurableSpace.volume as the default measure. + done: true + location: Physlib/QuantumMechanics/HilbertSpaces/SpaceD/Basic.lean (SpaceDHilbertSpace) + + - description: > + Includes a proposition describing when a function can be interpreted + as an element of a Hilbert space on Space. + done: true + location: Physlib/QuantumMechanics/HilbertSpaces/SpaceD/Basic.lean (MemHS) + + - description: + Defines the subspace corresponding to complex Schwartz maps on Space + and provides functions for moving back and forth between the Schwartz maps + and their equivalence classes in the Hilbert space. + done: true + location: > + Physlib/QuantumMechanics/HilbertSpaces/SpaceD/SchwartzSubmodule.lean + (SchwartzSubmodule, schwartzIncl, schwartzEquiv) + + - description: Defines the Fourier transform as a unitary map from the Hilbert space to itself. + done: true + location: Physlib/QuantumMechanics/HilbertSpaces/SpaceD/Fourier.lean (fourierUnitary) + + - description: Defines the Sobolev subspaces. + done: false + location: N/A + + - description: > + Defines sub-Hilbert spaces consisting of functions with support contained + in a subset of Space. + done: true + location: Physlib/QuantumMechanics/HilbertSpaces/SpaceD/Basic.lean + (SpaceDHilbertSpaceOn, subspaceIncl, subspaceProjection) + + - description: > + Defines subspaces corresponding to elements of the Hilbert space satisfying + homogeneous Dirichlet boundary conditions on a subset of Space. + done: true + location: + Physlib/QuantumMechanics/HilbertSpaces/SpaceD/DirichletSubmodule.lean (DirichletSubmoduleOn) + + - description: > + Defines subspaces corresponding to elements of the Hilbert space satisfying + homogeneous Neumann boundary conditions on a subset of Space. + done: false + location: N/A + + - description: > + Defines subspaces corresponding to elements of the Hilbert space satisfying + homogeneous mixed boundary conditions on a subset of Space. + done: false + location: N/A + + - description: + Defines multiplication operators with maximal domain for any complex function of position. + done: true + location: Physlib/QuantumMechanics/Operators/Multiplication.lean (mulOperator) + + - description: + Defines position operators as instances of multiplication operators with maximal domain. + done: true + location: Physlib/QuantumMechanics/Operators/Position.lean (positionOperator) + + - description: + Defines derivative operators with maximal domain for any complex function of the wavenumber. + done: false + location: N/A + + - description: > + Defines momentum and momentum-squared operators as instances of derivative operators + with maximal domain. + done: false + location: N/A + + - description: Defines angular momentum and angular momentum-squared operators. + done: false + location: N/A + + - description: Defines the reflection operator through a general hyperplane. + done: false + location: N/A diff --git a/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/Basic.lean b/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/Basic.lean index b0f807143..43aefe2aa 100644 --- a/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/Basic.lean +++ b/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/Basic.lean @@ -14,12 +14,17 @@ public import Physlib.SpaceAndTime.Space.Module ## i. Overview -The Hilbert spaces appropriate for doing quantum mechanics on `Space d` are the $$L^2$$-spaces +The Hilbert spaces appropriate for doing quantum mechanics on `Space d` are the $L^2$-spaces `SpaceDHilbertSpace d μ := Lp ℂ 2 μ`, where `μ` is some measure on `Space d`. Elements of `SpaceDHilbertSpace d μ` are _equivalence classes_ of functions `Space d → ℂ` which are square-integrable with respect to `μ`, i.e. `∫ x, ‖f x‖ ^ 2 ∂μ` is finite, and where `f` and `g` are in the same equivalence class if they are `μ`-a.e. equal. +The ability of a function to be interpreted as an element of `SpaceDHilbertSpace d μ` is captured +by the property `MemHS`. If one has `hf : MemHS f μ` for a function `f : Space d → ℂ` this means +that `f` is `μ`-a.e. strongly measurable and square-integrable; `mk hf` constructs the corresponding +equivalence class of `f` in `SpaceDHilbertSpace d μ`. + Given `SpaceDHilbertSpace d μ` and `Ω : Set (Space d)`, the Hilbert space `SpaceDHilbertSpaceOn Ω μ ≔ SpaceDHilbertSpace d (μ.restrict Ω)` may be interpreted as the sub-Hilbert space consisting of those vectors with domain contained in `Ω`. @@ -28,17 +33,19 @@ The reason is that for each `ψ` in `SpaceDHilbertSpaceOn Ω μ` we have contains a representative which vanishes on the complement of `Ω`. The linear isometry `restrictIncl Ω μ` describes this sub-Hilbert space relationship by mapping each `ψ` to this special representative in its equivalence class. - Similarly, we may project `SpaceDHilbertSpace d μ` onto `SpaceDHilbertSpaceOn Ω μ` by enlarging the equivalence classes, essentially dropping information about the functions on the complement of `Ω`. ## ii. Key results -- `SpaceDHilbertSpace d μ` : The $$L^2$$-space on `Space d` with respect to the measure `μ`. +- `SpaceDHilbertSpace d μ` : The $L^2$-space on `Space d` with respect to the measure `μ`. - `toBra` : The linear equivalence between the Hilbert space and its dual. This is the map which sends each ket to its corresponding bra and _vice versa_. -- `MemHS f μ` : The proposition capturing exactly when the function `f : Space d → ℂ` can be lifted +- `MemHS f μ` : The proposition capturing exactly when a function `f : Space d → ℂ` can be lifted to an element of the Hilbert space. +- `SpaceDHilbertSpaceOn Ω μ` : An abbreviation for the Hilbert space + `SpaceDHilbertSpace d (μ.restrict Ω)` appropriate for describing the $L^2$-space of complex + functions on a subset of `Space d`. - `subspaceProjection` : The projection of `SpaceDHilbertSpace d μ` onto `SpaceDHilbertSpaceOn Ω μ`. - `subspaceIncl` : The linear isometry including `SpaceDHilbertSpaceOn Ω μ` as a sub-Hilbert space of `SpaceDHilbertspace d μ`. @@ -69,9 +76,8 @@ open Function InnerProductSpace MeasureTheory Measure Set ## A. SpaceDHilbertSpace -/ -/-- The Hilbert space for single-particle quantum mechanics on `Space d` with measure `μ` - is defined to be `L²(Space d, ℂ; μ)`, the space of `μ`-a.e. equal equivalence classes - of functions `f : Space d → ℂ` for which `∫ x, ‖f x‖² ∂μ` is finite. -/ +/-- The L²-space of `μ`-a.e. equal equivalence classes of functions `f : Space d → ℂ` + for which `∫ x, ‖f x‖² ∂μ` is finite. -/ abbrev SpaceDHilbertSpace (d : ℕ) (μ : Measure (Space d) := volume) := Lp ℂ 2 μ namespace SpaceDHilbertSpace @@ -147,7 +153,7 @@ lemma MemHS.indicator {Ω : Set (Space d)} (hΩ : MeasurableSet Ω) (hf : MemHS MemHS (Ω.indicator f) μ := MemLp.indicator hΩ hf -/-- If `f` is a member of the Hilbert space `SpaceDHilbertSpaceOn Ω μ` then the representative +/-- If `f` is a member of the Hilbert space with measure restricted to `Ω` then the representative `Ω.indicator f` which vanishes outside `Ω` is a member of `SpaceDHilbertSpace d μ`. -/ lemma MemHS.indicator_of_restrict {Ω : Set (Space d)} (hΩ : MeasurableSet Ω) (hf : MemHS f (μ.restrict Ω)) : @@ -182,13 +188,13 @@ lemma mk_sub : mk (hf.sub hg) = mk hf - mk hg := rfl @[simp] lemma mk_const_smul (c : ℂ) : mk (hf.const_smul c) = c • mk hf := rfl -lemma coeFn_mk : mk hf =ᵐ[μ] f := AEEqFun.coeFn_mk f hf.1 - lemma mk_eq_iff : mk hf = mk hg ↔ f =ᵐ[μ] g := by simp [mk] lemma mk_surjective : ∃ (f : Space d → ℂ) (hf : MemHS f μ), mk hf = ψ := ⟨ψ, memHS_coe ψ, by simp [mk]⟩ +lemma coeFn_mk : mk hf =ᵐ[μ] f := AEEqFun.coeFn_mk f hf.1 + lemma inner_mk_mk : ⟪mk hf, mk hg⟫_ℂ = ∫ x, starRingEnd ℂ (f x) * g x ∂μ := by apply integral_congr_ae filter_upwards [coeFn_mk hf, coeFn_mk hg] @@ -239,9 +245,10 @@ end SpaceDHilbertSpace TODO "Upgrade subspaceProjection to a ContinuousLinearMap when Lp.LpToLpOfMeasureLeSMul becomes available." -/-- The Hilbert space for single-particle quantum mechanics on a set `Ω ⊆ Space d` with measure `μ` - is defined to be `SpaceDHilbertSpace d (μ.restrict Ω)`, the space of `μ`-a.e. equal on `Ω` - equivalence classes of functions `f : Space d → ℂ` for which `∫ x on Ω, ‖f x‖² ∂μ` is finite. -/ +/-- The L²-space `SpaceDHilbertSpace d (μ.restrict Ω)`. + + Elements are equivalence classes of functions which agree `μ`-a.e. on `Ω` and which have + `∫ x in Ω, ‖f x‖ ^ 2 ∂μ` finite. -/ abbrev SpaceDHilbertSpaceOn {d : ℕ} (Ω : Set (Space d)) (μ : Measure (Space d) := volume) := SpaceDHilbertSpace d (μ.restrict Ω)