Hilbert space and unbounded operators

Stream: PhysLean

[Gregory Loges]

I think I can take care of issue#851 as part of my 'quest' to formalize the spectrum of hydrogen, but I have a couple of questions about design.

HilbertSpace/Basic.lean and HilbertSpace/SchwartzSubmodule.lean for one dimension carry over to Space d essentially unchanged. However, should we consider a more descriptive name since there are other common Hilbert spaces in physics besides $L^2(\mathbb{R}^d,\mathbb{C})$?

Also, I think there is an opportunity to 'mathlib-ify' Operators/Unbounded.lean. For example, an unbounded operator could be defined as a special case of docs#LinearPMap:

-- A `LinearPMap R E F` or `E →ₗ.[R] F` is a linear map from a submodule of `E` to `F`.
/-- An `UnboundedOperator` is a linear map from a submodule of `HilbertSpace d` to `HilbertSpace d`. -/
abbrev UnboundedOperator {d : ℕ} := LinearPMap ℂ (HilbertSpace d) (HilbertSpace d)

namespace UnboundedOperator

def mk {d : ℕ}
    (domain : Submodule ℂ (HilbertSpace d))
    (toFun : domain →ₗ[ℂ] HilbertSpace d) :
    UnboundedOperator (d := d) := LinearPMap.mk domain toFun

-- etc.

end UnboundedOperator

Is there any reason not to take this approach?

[Daniel Morrison]

I think in the future we will want HilbertSpace to be an instance that gets placed on a specific type because, as you said, there are other Hilbert spaces. However, at the moment we're happy with incremental improvements so I think doing this kind of upgrade isn't a bad thing as long as you realize it'll probably get changed again.

I agree LinearPMap is probably the thing to use, but I think it would be smart to create a structure with a LinearPMap and a prop that the domain is dense since that seems to be a common assumption for operators that isn't in LinearPMap and is important to other nice properties of things like the adjoint.

But all of this doesn't need to happen at once. I was thinking about this as well, so feel free to make whatever progress you want and more can be done later.

[Gregory Loges]

Thanks, makes sense. Would a continuity assumption in the structure also be appropriate?

[Joseph Tooby-Smith]

I think in the future we will want HilbertSpace to be an instance that gets placed on a specific type because,

I'm somewhat surprised that Mathlib hasn't taken this approach.

However, should we consider a more descriptive name since there are other common Hilbert spaces in physics besides $L2(Rd,C)$?

I agree that a new name would be better @Gregory Loges , do you have any suggestions?

[Daniel Morrison]

Gregory Loges said:

Thanks, makes sense. Would a continuity assumption in the structure also be appropriate?

My understanding is the answer to that is no, because for linear maps continuity is equivalent to bounded which we specifically don't want.

[Daniel Morrison]

Joseph Tooby-Smith said:

I think in the future we will want HilbertSpace to be an instance that gets placed on a specific type because,

I'm somewhat surprised that Mathlib hasn't taken this approach.

I suspect the reason is that right now you can write down a Hilbert Space using inner product space + complete space instances and don't need to define another instance. I think for physics it makes sense to combine them, but I could also be wrong.

[Gregory Loges]

Joseph Tooby-Smith said:

do you have any suggestions?

Maybe something like HilbertSpaceL2SpaceD or just simply L2SpaceD to highlight the domain? I am envisioning also $L^2([a,b])$ for the infinite square well and other subsets of Space d in the future, with analogous names like HilbertSpaceL2Interval or HilbertSpaceL2Circle.

[Joseph Tooby-Smith]

or SpaceDHilbertSpace? Do you think we need the L2 in there as well?

[Gregory Loges]

Joseph Tooby-Smith said:

Do you think we need the L2 in there as well?

My first thought was the amusing HilbertSpaceSpaceD so I thought to break it up a bit. But I like SpaceDHilbertSpace much more!