Unbounded Operators & Adjoints

Stream: PhysLean

[Daniel Morrison]

I've started playing around with defining unbounded operators and their adjoints (items 4 and 5 on the QM project board) and ran into a design question I thought I'd ask about. My current definitions are:

𝕜 is RCLike, E & F have instances InnerProductSpace and NormedAddCommGroup (Hilbert spaces without completeness)

structure BoundedLinearMap extends E →ₗ[𝕜] F where
  bounded : ∃ (M : ℝ), 0 ≤ M ∧ ∀ (x : E), ‖toFun x‖ ≤ M * ‖x‖

notation E "→ᵇₗ[" 𝕜 "]" F => BoundedLinearMap 𝕜 E F

(BoundedLinearMap is maybe unnecessary since continuity is equivalent to bounded and there's already a structure ContinuousLinearMap)

structure UnboundedLinearMap extends E →ₗ[𝕜] F where
  domain : Subspace 𝕜 E
  dense : Dense (X := E) domain

notation E "→ᵘₗ[" 𝕜 "]" F => UnboundedLinearMap 𝕜 E F

The problem is when I try to define the adjoint of an unbounded operator. There several ways to characterize the domain of the adjoint all to do with the maps $y \mapsto \langle x, A y\rangle$ for fixed $x \in F$ and operator $A$, the issue is that apparently this domain is not necessarily dense but will be in practical applications.

My ideas are to either

1. Define the adjoint for all operators as just a linear map and then promote it to an operator with a density condition, but we have to carry the domain of the adjoint separate from the map.
2. Remove the density condition from the definition and add it back as a hypothesis of defining the adjoint so the adjoint is automatically an "unbounded operator", but this diverges from the expected definition.

Thoughts on my ideas or your own solution is appreciated, and feel free to comment on the definitions above. You can see all of my work so far in my fork.

[Joseph Tooby-Smith]

Hi Daniel!

First let me say: Thank you very much for working in this direction - its great to see this been done! I've looked at your fork and it looks great!

To address your question: Out of your ideas I personally think 2 is the best, because overall I think this will make things easier to work with.

Maybe one could do something like the following:

structure LinearMapWithDomain extends E →ₗ[𝕜] F where
  domain : Subspace 𝕜 E

def IsUnboundedLinearMap (f : LinearMapWithDomain) : Prop := Dense f.domain

notation E "→ᵘₗ[" 𝕜 "]" F => LinearMapWithDomain 𝕜 E F

One could maybe also define a structure UnboundedLinearMap which extends LinearMapWithDomain.

I run into problems like this quite often, so maybe someone else here can shed more light on what is best. I also think there is no harm in picking one approach and seeing if you can get it to work - we can always refactor it later (it's a pain but not the end of the world).

Once again - thanks!

Joseph

[Alex Meiburg]

If you look at https://github.com/dupuisf/LFTCM2024TraceClass/blob/master/LFTCM2024TraceClass/ContinuousLinearMap.lean I think there's similarly some good stuff to get going.

Why do you need to define "Unbounded linear map", why not just, a linear map? At very least, if your definition of UnboundedLinearMap is not equivalent to a linear map (I can't tell for sure), I'm sure there's a better name for it

[Alex Meiburg]

Oh this is for https://en.wikipedia.org/wiki/Unbounded_operator#Definitions_and_basic_properties right right silly me

[Alex Meiburg]

Well I think the dense property should be pulled out into DenselyDefinedLinearMap, which can extend UnboundedLinearMap. And then adjoints are defined for DenselyDefinedLinearMap

[Daniel Morrison]

Upon further investigation into the mathlib docs I found that this already exists... The relevant structure is LinearPMap (partially defined linear map) and you can find LinearPMap.adjoint here. On the bright side I was close to recreating what's here and it was an interesting exercise anyway. It isn't imported by anything else so there's probably work to be done developing the theory for what we need here.

[Joseph Tooby-Smith]

Just in case this helps: When I was making the project board for QM this Ref is what I was looking at regarding bounded linear maps etc.

[Daniel Morrison]

Ooh, thanks I'll take a look. I was using Quantum Theory for Mathematicians by Brian Hall

[Joseph Tooby-Smith]

There is also this Ref. But I'm sure Hall's book is equally as good as either of these.