Turning kets to bras is surjective

Stream: PhysLean

[Joseph Tooby-Smith]

I've over the last few days been trying to improve the API around quantum mechanics (using unbounded operators and generalized eigenvectors etc), in particular for 1d systems.

There is one result that I don't know how to prove: The conversion of a ket $|\psi\rangle$ into a bra $\langle \psi |$ is surjective.

import Mathlib.MeasureTheory.Function.L2Space
import Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

namespace QuantumMechanics

namespace OneDimension

noncomputable section

/-- The Hilbert space for a one dimensional quantum system is defined as
  the space of almost-everywhere equal equivalence classes of square integrable functions
  from `ℝ` to `ℂ`. -/
abbrev HilbertSpace := MeasureTheory.Lp (α := ℝ) ℂ 2

namespace HilbertSpace
open MeasureTheory
open InnerProductSpace

/-- The anti-linear map from the Hilbert space to it's dual. -/
def toBra : HilbertSpace →ₛₗ[starRingEnd ℂ] (Module.Dual ℂ HilbertSpace) where
  toFun f := {
    toFun g := ⟪f, g⟫_ℂ,
    map_add' g1 g2 := by simp [inner_add_right],
    map_smul' c g := by simp [inner_smul_right]
  }
  map_add' f1 f2 := by
    ext g
    simp [inner_add_left]
  map_smul' c f := by
    ext g
    simp [inner_smul_left]

/-- The anti-linear map, `toBra`, taking a ket to it's corresponding
  bra is surjective. -/
lemma toBra_surjective : Function.Surjective toBra := by
  sorry

I believe this is related to the 'Riesz representation theorem', but generally, does anyone know how one can fill in the above sorry?

[Kenny Lau]

import Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
import Mathlib.Analysis.InnerProductSpace.Dual
import Mathlib.MeasureTheory.Function.L2Space

namespace QuantumMechanics

namespace OneDimension

noncomputable section

/-- The Hilbert space for a one dimensional quantum system is defined as
  the space of almost-everywhere equal equivalence classes of square integrable functions
  from `ℝ` to `ℂ`. -/
abbrev HilbertSpace := MeasureTheory.Lp (α := ℝ) ℂ 2

namespace HilbertSpace
open MeasureTheory
open InnerProductSpace

/-- The anti-linear map from the Hilbert space to it's dual. -/
def toBra : HilbertSpace →ₛₗ[starRingEnd ℂ] NormedSpace.Dual ℂ HilbertSpace :=
  InnerProductSpace.toDual ℂ HilbertSpace

@[simp] lemma toBra_apply (f g : HilbertSpace) : toBra f g = ⟪f, g⟫_ℂ := rfl

/-- The anti-linear map, `toBra`, taking a ket to it's corresponding
  bra is surjective. -/
lemma toBra_surjective : Function.Surjective toBra :=
  (InnerProductSpace.toDual ℂ HilbertSpace).surjective

[Kenny Lau]

@Joseph Tooby-Smith it's not true if you use the Module.Dual, because that dual doesn't care about the topology; you get the correct statement using NormedSpace.Dual instead.

[Kevin Buzzard]

A few more details: most of the elements of Module.Dual are linear but non-continuous maps from HilbertSpace to $\mathbb{C}$. If you don't consider the topology, then the moment you're in infinite dimension the following phenomenon occurs. A general theorem of algebra (which needs the axiom of choice in infinite dimensions, and in Lean probably uses it in finite dimensions too) says that every vector space has an algebraic basis. More precisely, there is some collection $b_1,b_2,b_3,\ldots$ of elements of the space such that every element of the space is a finite linear combination of basis elements. Actually this is not great notation because often the basis will be uncountably infinite so can't even be indexed by the naturals. Remember that we have completely forgotten the topology here so there is not even a concept of an infinite sum because there is no notion of limit. However you can algebraically take infinite sums in the dual space, for example there's a perfectly good map from a vector space with basis $b_1,b_2,b_3,\ldots$ to the complex numbers which sends all the $b_i$ to 1, because then you can make sense of what happens to a finite linear combination of $b_i$. So "the space only has finite sums but the dual has infinite sums" -- more formally the algbebraic dual of $\bigoplus_{i\in I}\mathbb{C}$ is $\prod_{i\in I}\mathbb{C}$ which is much bigger (the first only has finite linear combinations, the second allows infinite ones). In infinite dimensions you need the topology to rescue the situation.

[Joseph Tooby-Smith]

Ok, thank you so much both! This makes sense to me, I think the fact I couldn't find this result in Mathlib was probably a hint that I was doing something wrong. Annoyingly this means I now have to go an upgrade a bunch of linear maps to continuous linear map - but so is life.

[Joseph Tooby-Smith]

I'm trying to make the necessary changes to account for the topology and one thing I am now stuck on is defining the following continuous linear map:

import Mathlib

-- SchwartzMap.toLpCLM ℂ ℂ 2 MeasureTheory.volume
-- is a injective continuous linear map with domain `SchwartzMap ℝ ℂ`.

def schwartzSubmoduleEquiv :
  LinearMap.range (SchwartzMap.toLpCLM ℂ (E := ℝ) ℂ 2 MeasureTheory.volume)
  ≃L[ℂ] SchwartzMap ℝ ℂ  := by sorry

Basically that there is a continuous linear map between the sub-module of AE equal equivalence classes of square-integrable functions that can be represented by Schwartz maps and the module of Schwartz maps itself.

Defining a continuous linear map in the inverse direction SchwartzMap ℝ ℂ to LinearMap.range _ is easy. Defining a linear map in the forward direction is also easy through choice, but I am stuck showing that this map is continuous.

I believe the existence of such a map comes down to whether or not SchwartzMap.toLpCLM is a topological embedding, but maybe I am missing something completely obvious here.

[Kevin Buzzard]

Maybe this is a question for #Is there code for X? ?

[Joseph Tooby-Smith]

(done here #Is there code for X? > Inclusion of Schwartz maps into L2 )

[Kenny Lau]

@Joseph Tooby-Smith are you sure you want this map? I tried to define it but I keep getting instance errors.

import Mathlib

-- SchwartzMap.toLpCLM ℂ ℂ 2 MeasureTheory.volume
-- is a injective continuous linear map with domain `SchwartzMap ℝ ℂ`.

open SchwartzMap MeasureTheory

noncomputable def schwartzMapEquivRange :
    𝓢(ℝ, ℂ) ≃ₗ[ℂ] LinearMap.range (toLpCLM ℂ (E := ℝ) ℂ 2 volume) :=
  LinearEquiv.ofInjective _ <| injective_toLp 2 volume

def schwartzMapCtsEquivRange :
    𝓢(ℝ, ℂ) ≃L[ℂ] LinearMap.range (toLpCLM ℂ (E := ℝ) ℂ 2 volume) where
  __ := schwartzMapEquivRange
  continuous_toFun := sorry
  continuous_invFun := sorry

(btw, you shouldn't use tactics in definitions)

And also upon investigating further, I'm now not even sure if this is true! There are two issues here:

1. This is a bit of a minor issue, but LinearMap.range gives you a subspace and subspaces might not be very well-behaved.
2. I see that the Schwarz space doesn't seem to have a norm, but rather a seminorm?
3. I looked at the norm-properties of toLpCLM (mathematically, continuous means something like preserve norm up to constant), and I only found SchwartzMap.norm_toLp_le_seminorm

∃ k C, 0 ≤ C ∧ ∀ (f : 𝓢(E, F)), ‖f.toLp p μ‖ ≤
      C * (Finset.Iic (k, 0)).sup (schwartzSeminormFamily 𝕜 E F) f

In particular, it seems like there's no bound in the other direction?

4. What is the use case of this? Why isn't toLp enough? Why do you need to make it a continuous linear equiv?

[Kenny Lau]

Mathematically, the question is, can I construct a sequence of functions whose L2 norm go to 0 but whose Schwarz seminorm go to infinity? This seems to be possible, because the L2 norm is only about the area, but the Schwarz seminorm wants to look at derivatives

[Kenny Lau]

for example, I can keep my function bounded (i.e. f(x)=0 for |x|>1), and let its area go to 0, but introduce more and more "wiggles" so that its derivative goes to infinity?

[Joseph Tooby-Smith]

(btw, you shouldn't use tactics in definitions)

Yeah - sorry the := by sorry a muscle memory to finish the line :).

Given what you and Kevin said above, I would be surprised is this is not true. I'm essentially trying to work with the rigged Hilbert space defined in this wikipedia page.

The use case is to define e.g. the momentum operator or the position operator in QM as unbounded operators, defined on the submodule of the Hilbert space

Φ  := LinearMap.range (toLpCLM ℂ (E := ℝ) ℂ 2 volume)

The current way they are defined in PhysLean are by converting elements in this submodule to Schwartz maps using schwartzSubmoduleEquiv and taking e.g. their derivative there. See here for the case of the momentum operator. But this is currently defined as a linear map not a continuous linear map, which I think is what is needed.

Basically schwartzSubmoduleEquiv lets you move away from the equivalence classes which are used to define the Lp space to concrete functions, allowing you to apply operations that physicists are typically use to.

[Kenny Lau]

@Joseph Tooby-Smith Note that the wikipedia page talks about a "finer topology", and that the "inclusion Φ⊆H is continuous", but nothing about any inverse. Note that "finer topology" means precisely that the inverse is not continuous.

For example, if you take a standard bump function B(x), then it would be bounded, so it's automatically in Schwarz. But bounded smooth functions have horrible derivatives (citation needed), so you can see that the derivatives of B(x) go to infinity.

Then, I can just take the sequence 1/n B(x), then its L2 norm will go to 0, but each norm ||1/n B(x)|| is infinity, so it doesn't converge to 0.

Demonstration:
https://www.desmos.com/calculator/cbxbi5wemf

[Matteo Cipollina]

i think in the wikipedia nothing is said (or required) about continuity of an inverse $H→Φ$ . When wikipedia stresses that Φ has a strictly stronger topology than H, it seems to mean that the inclusion $𝓢↪L2$ is the continuum-embedding, so no continuous inverse seems to be mentioned or implied/required.
And if there is no requirement for a topological equivalence between $𝓢$ and that range, there seems to be no contradiction in the fact that Lean refuses to produce a ≃L, ie the inverse

[Kenny Lau]

Joseph Tooby-Smith said:

But this is currently defined as a linear map not a continuous linear map, which I think is what is needed.

Basically schwartzSubmoduleEquiv lets you move away from the equivalence classes which are used to define the Lp space to concrete functions, allowing you to apply operations that physicists are typically use to.

You basically have to always keep in mind that there are two different norms in the picture, and when you say continuous you have to always specify with respect to which norm.

From my first look at it, it takes a derivative, so it should be continuous in the Schwarz norm but not in the L2 norm.

[Kenny Lau]

when mathematicians talk about embeddings they don't think twice about whether the original set and the embedded set is different (and in this case it actually matters, since there are two different topologies!)

In this case for your momentum operator I would even argue that it's wrong to define it on Φ. I think you should define it on 𝓢(ℝ, ℂ).

[Joseph Tooby-Smith]

Ok, I'm willing to accept this. But then I have the following conflict, which is, what is the correct definition of an unbounded continuous linear operator here?

The nlab defines it here as

An unbounded operator T on a Hilbert space ℋ is a linear operator defined on a subspace D of ℋ. D is necessarily a linear submanifold.

And specifically gives the example of Schwartz maps and differentiation on that page.

In Mathlib the definition of an unbounded (not necessarily continuous) operator is

structure LinearPMap (R : Type u) [Ring R] (E : Type v) [AddCommGroup E] [Module R E] (F : Type w)
  [AddCommGroup F] [Module R F] where
  domain : Submodule R E
  toFun : domain →ₗ[R] F

But from what I understand, the real definition we seem to want is that a continuous unbounded linear operator is a continuous linear injection $\iota : S \to M$ (the 'submodule'), along with a continuous linear map $f : S \to M$ (the operator). Is it clear to anyone whether this is in agreement with the nlab definition?

[Kenny Lau]

Yeah that sounds good to me.

[Joseph Tooby-Smith]

(I should say that this last definition makes the category theoriest inside of me happy, because a continuous linear injection is a monomorphism in the category of topological vector spaces, and therefore this is the correct definition of a subobject).

[Kenny Lau]

Someone should make a counter-example showing that derivative is not continuous in L2(R) and that the Schwarz norm is not continuous wrt the L2 norm

[Kenny Lau]

the bump function itself having infinite norm should also be a counterexample

[Joseph Tooby-Smith]

Is it even clear how you would define the derivative for $L^2(\mathbb{R})$ in general?

[Kenny Lau]

I meant, on the wrong topology on S(R;C)

[Joseph Tooby-Smith]

Ok, thanks for explaining. I agree such a counter-example would be nice to see.

[Kenny Lau]

is there even a schwarz function that doesn't blow up?? (i'm not very familiar with functional analysis)

[Kenny Lau]

even the nicest exp(-x^2) still seems to have infinite norm?