feat(QuantumMechanics): adjoint of continuous operators

[gloges]

• Adds adjoint_domain_of_continuous: U†.domain = ⊤ when U is a continuous (equivalently, bounded) operator
• Adds HasDenseDomain.adjoint_add_continuous (and a sub variant): (T₁ + T₂)† = T₁† + T₂† with T₂ continuous (equivalently, bounded).
• Simplifies the proof IsUnbounded.orthogonal_closure_sub_range using adjoint_sub_continuous

Also takes the opportunity to move the IsUnbounded section of Unbounded.lean before those for IsSymmetric, etc. so that results for general unbounded operators can be used in more specialized cases.

Currently a draft since will need to merge after #1432.

[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.

[jstoobysmith]

Approved - looks good to me! I've approved, but also merged with master to make sure the bump doesn't break anything.