feat(QuantumMechanics): the basic criterion of essential self-adjoint…

[adambornemann-glitch]

…ness

Add §D to SpectralTheory/Symmetric.lean:
IsSymmetric.closure_sub_smul_surjective for symmetric, densely-defined A and non-real z, density of the range of A - z • 1 upgrades to surjectivity of A.closure - z • 1 and IsEssentiallySelfAdjoint.of_dense_range_add_sub (the basic criterion).

Downstream, this powers the essential self-adjointness of the momentum operator via density of its deficiency ranges in Fourier space.

[github-actions]

Thank you for this PR, which will now be reviewed. If submitting to ./Physlib or ./QuantumInfo, please see our review guidelines if you are not familiar with the process. You should expect a back and forth with a reviewer before your PR is merged. See also that link for how to add appropriate labels to your PR. The PR will also go through a number of automated checks. You can learn more about these here, including how to run them locally.

If you are submitting to ./PhyslibAlpha there will be a lighter review process, though your PR must still pass the automated checks.

If you want to bring attention to this PR, please write a message on this thread of the Lean Zulip.

Important: If a reviewer adds an awaiting-author label to your PR, once you have addressed the review comments, please remove that label by adding a comment with -awaiting-author. This helps us keep track of reviews.

[gloges]

Thanks, nice to have this e.s.a. theorem!
I've left some comments on closure_sub_smul_surjective to help you get a feel for how to apply a self-critical eye when stating lemmas and their hypotheses. Practice and becoming more familiar with the library over time will only make this easier :)
In this case the lemmas are improved by phrasing things in terms of submodules of H because we are dealing with linear maps rather than general functions.

edit: I should clarify that the "foo" version of IsSymmetric.closure_sub_smul_surjective that I land on below is mathematically identical to how you phrased things (after the hz : z ∈ T.regularityDomain change) thanks to LinearMap.range_eq_top and Submodule.dense_iff_topologicalClosure_eq_top but is a cleaner digitization because it doesn't involve coersions to sets or functions (which will help down the road).

In the e.s.a. proof you use IsSelfAdjoint.of_surjective_add_sub which I think would benefit from receiving the same treatment. Here's my suggest rephrasing:

lemma IsSymmetric.isSelfAdjoint_of_range_eq_top [CompleteSpace H]
    (hsym : T.IsSymmetric) (hdense : T.HasDenseDomain)
    (hadd : (T + I • 1).toFun.range = ⊤) (hsub : (T - I • 1).toFun.range = ⊤) :
    IsSelfAdjoint T := by
  sorry

It might make sense to include this change in this PR so that it gels with the e.s.a. proof; let me know what you think.

[adambornemann-glitch]

-awaiting-author

[gloges]

Hi @adambornemann-glitch, creating a carbon copy of adjoint_closure_eq_adjoint is not an appropriate solution. Please read my previous comment again.

[adambornemann-glitch]

That's on me, I couldn't see the of_le route and should have asked follow ups instead of just pushing again. I'm not sure what I was thinking honestly (I've been kinda soupy all day). It's fixed properly now: the duplicate is removed, IsUnbounded.adjoint_closure_eq_adjoint is restored, and IsSymmetric.closure sits at the end of the IsSymmetric section. Lesson learned.

Question for you: the sign identity T + I • 1 = T − (−I) • 1 now appears inline in two proofs, would you like it factored into Mathematics/LinearPMap.lean, or left as is?

[gloges]

I couldn't see the of_le route

I realize now that it doesn't work -- I was too quick and thought the inequality T ≤ T.closure would be enough but it's the wrong way around! Your proof is good :) I'll make a PR later today to move the unbounded section so that this issue doesn't arise in the future.

Question for you: the sign identity T + I • 1 = T − (−I) • 1 now appears inline in two proofs, would you like it factored into Mathematics/LinearPMap.lean, or left as is?

I think to keep this PR focused it's fine to leave it how it is. In the (near) future we should add (-c) • f = -(c • f) and c • (-f) = -(c • f) in as much generality as possible to Mathematics/LinearPMap.lean as simp lemmas (Mathlib's neg_smul and smul_neg simp lemmas don't directly work because E →ₗ.[R] F is not a group). Let me know if you want to have a crack at this, otherwise I am happy to take care of it.

[gloges]

Thanks for working out these changes - looks good!

[adambornemann-glitch]

It's on my list of things to take a crack out now, I'll still leave this PR as is while I'm working on it. 🫡