feat: Position & momentum unbounded operators

[gloges]

Continues on from #957 and makes progress on #851.

Introduces schwartzEquiv, the LinearEquiv between Schwartz functions and their image in the Hilbert space, along with some basic properties. This bijection is then used to define three symmetric unbounded operators with Schwartz submodule for domain, using the previously-defined continuous linear maps on Schwartz functions. These are the position and momentum unbounded operators, defined component-wise, and the (regularized) radius operator to any real power.

There remains one sorry which will have to be revisited. Showing that the momentum operator on Schwartz functions is symmetric requires two results for Space.deriv: integration-by-parts over all of Space d and commutation through complex conjugation.

[morrison-daniel]

Apologies for not getting to this sooner, but I have been thinking about your PR. I think everything you've done here is reasonable in terms of the existing API and how the literature is written but I wonder if it makes sense for us to change up how UnboundedOperator is defined to make things smoother for Lean formalization. What doesn't feel quite right to me is

/-- The position operators defined on the Schwartz submodule. -/
def positionOperatorSchwartz : schwartzSubmodule d →ₗ[ℂ] schwartzSubmodule d :=
  (schwartzEquiv (d := d)) ∘ₗ 𝐱[i].toLinearMap ∘ₗ (schwartzEquiv (d := d)).symm

Like I said, why you'd do this makes sense with how things are designed, but needing to use schwartzEquiv to move back and forth between the Schwartz subspace seems like a complication that is going to bite us in the long run. I wonder if it would make more sense to have UnboundedOperator between two different spaces, even if we only intend to use them between the same space because Lean sees the submodule it's defined on as a different space than the entire Hilbert space. So I'm thinking it might be smart to adjust the API before we get too deep.

Unfortunately that would delay this PR but I think it might save some headaches in the long run. Does this reasoning make sense, and do you think this would be a productive change?

[jstoobysmith]

@morrison-daniel Could you give your suggested definition for UnboundedOperator here?

[gloges]

I wonder if it would make more sense to have UnboundedOperator between two different spaces, even if we only intend to use them between the same space

I think this change,

structure UnboundedOperator ... extends LinearPMap ℂ HS1 HS2 where ...

could be done relatively easily, but this wouldn't remove the need to map between Schwartz maps and their $$L^2$$ equivalence classes. Maybe I have misunderstood your comment?

[morrison-daniel]

You are correct, I realized what I was suggesting wouldn't actually remove what I wanted to remove. I have a tendency to be overly cautious to whether something is being done in the best way which is overkill at this point... Ignore my previous statement I'll review, but it's already looking pretty good!

[morrison-daniel]

Suggested change

	obtain ⟨_, rfl⟩ := schwartzEquiv_exists ψ
	obtain ⟨_, rfl⟩ := schwartzEquiv_exists ψ'
	obtain ⟨_, rfl⟩ := schwartzEquiv.surjective ψ
	obtain ⟨_, rfl⟩ := schwartzEquiv.surjective ψ'

[morrison-daniel]

Suggested change

	variable {d : ℕ}
	variable (d : ℕ)

I wonder if it'd make sense to make this explicit because, while d can be inferred when applying to a specific function, we're using it a lot for operators and need to include (d := d) a lot. I can see it either way, you can choose which you prefer.

You can also decide if you'd like to make the same change on the operators.

[morrison-daniel]

This is basically identical to schwartzEquiv.surjective so I think this is redundant.

[morrison-daniel]

Suggested change

	obtain ⟨f, rfl⟩ := schwartzEquiv_exists ψ
	obtain ⟨f', rfl⟩ := schwartzEquiv_exists ψ'
	obtain ⟨f, rfl⟩ := schwartzEquiv.surjective ψ
	obtain ⟨f', rfl⟩ := schwartzEquiv.surjective ψ'