Unbounded operators

Note

It is likely one day the material in this file will be moved to or appear in another form within Mathlib.

def QuantumMechanics.OneDimension.UnboundedOperator {S : Type} [AddCommGroup S] [Module ℂ S] [TopologicalSpace S] (ι : S →L[ℂ] ↥HilbertSpace) : Function.Injective ⇑ι → Type

An unbounded operator on the one-dimensional Hilbert space, corresponds to a subobject ι : S →L[ℂ] HilbertSpace of the Hilbert space along with the operator op : S →L[ℂ] HilbertSpace

Equations

• QuantumMechanics.OneDimension.UnboundedOperator ι x✝ = (S →L[ℂ] ↥QuantumMechanics.OneDimension.HilbertSpace)

instance QuantumMechanics.OneDimension.UnboundedOperator.instCoeFunForallSubtypeAEEqFunRealComplexVolumeMemAddSubgroupHilbertSpace {S : Type} [AddCommGroup S] [Module ℂ S] [TopologicalSpace S] {ι : S →L[ℂ] ↥HilbertSpace} {hι : Function.Injective ⇑ι} : CoeFun (UnboundedOperator ι hι) fun (x : UnboundedOperator ι hι) => S → ↥HilbertSpace

Equations

• One or more equations did not get rendered due to their size.

def QuantumMechanics.OneDimension.UnboundedOperator.ofSelfCLM {S : Type} [AddCommGroup S] [Module ℂ S] [TopologicalSpace S] {ι : S →L[ℂ] ↥HilbertSpace} {hι : Function.Injective ⇑ι} (Op : S →L[ℂ] S) : UnboundedOperator ι hι

An unbounded operator created from a continous linear map S →L[ℂ] S.

Equations

• QuantumMechanics.OneDimension.UnboundedOperator.ofSelfCLM Op = ι.comp Op

@[simp]

theorem QuantumMechanics.OneDimension.UnboundedOperator.ofSelfCLM_apply {S : Type} [AddCommGroup S] [Module ℂ S] [TopologicalSpace S] {ι : S →L[ℂ] ↥HilbertSpace} {hι : Function.Injective ⇑ι} (Op : S →L[ℂ] S) (ψ : S) : (↑(ofSelfCLM Op)).toFun ψ = ι (Op ψ)

def QuantumMechanics.OneDimension.UnboundedOperator.IsGeneralizedEigenvector {S : Type} [AddCommGroup S] [Module ℂ S] [TopologicalSpace S] {ι : S →L[ℂ] ↥HilbertSpace} {hι : Function.Injective ⇑ι} (U : UnboundedOperator ι hι) (F : S →L[ℂ] ℂ) (c : ℂ) : Prop

A map F : S →L[ℂ] ℂ is a generalized eigenvector of an unbounded operator U on S if there is an eigenvalue c such that for all ψ, F (U ψ) = c ⬝ F ψ

Equations

• U.IsGeneralizedEigenvector F c = ∀ (ψ : S), ∃ (ψ' : S), ι ψ' = (↑U).toFun ψ ∧ F ψ' = c • F ψ

theorem QuantumMechanics.OneDimension.UnboundedOperator.isGeneralizedEigenvector_ofSelfCLM_iff {S : Type} [AddCommGroup S] [Module ℂ S] [TopologicalSpace S] {ι : S →L[ℂ] ↥HilbertSpace} {hι : Function.Injective ⇑ι} {Op : S →L[ℂ] S} (F : S →L[ℂ] ℂ) (c : ℂ) : (ofSelfCLM Op).IsGeneralizedEigenvector F c ↔ ∀ (ψ : S), F (Op ψ) = c • F ψ

def QuantumMechanics.OneDimension.UnboundedOperator.IsSelfAdjoint {S : Type} [AddCommGroup S] [Module ℂ S] [TopologicalSpace S] {ι : S →L[ℂ] ↥HilbertSpace} {hι : Function.Injective ⇑ι} (U : UnboundedOperator ι hι) : Prop

The condition on an unbounded operator to be self-adjoint.

Equations

• U.IsSelfAdjoint = ∀ (ψ1 ψ2 : S), inner ℂ ((↑U).toFun ψ1) (ι ψ2) = inner ℂ (ι ψ1) ((↑U).toFun ψ2)