refactor(QuantumMechanics): rename SelfAdjoint to Symmetric#1449
Conversation
…elfAdjoint to IsSymmetric `QuantumMechanics.OneDimension.UnboundedOperator.IsSelfAdjoint` is defined as the Hermitian pairing `∀ ψ1 ψ2, ⟪U ψ1, ι ψ2⟫ = ⟪ι ψ1, U ψ2⟫` — i.e. symmetry (formal self-adjointness). It carries no domain/density hypothesis, so it does not establish genuine self-adjointness (`A† = A` with equal domains), which for an unbounded operator on a proper dense core is strictly stronger. The old name invites that stronger reading. Rename the definition and the three lemmas built on it (momentum/position/parityOperatorUnbounded_isSelfAdjoint → _isSymmetric), and update the docstring and section headings to match. Verified with a clean `lake build` of the four affected modules.
|
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 |
gloges
left a comment
gloges
left a comment
There was a problem hiding this comment.
Hi @KrystianNowakowski, thanks for making your first PR and correcting this error in nomenclature. These changes look good to me!
2 participants
QuantumMechanics.OneDimension.UnboundedOperator.IsSelfAdjointinPhyslib/QuantumMechanics/Operators/OneDimension/Unbounded.leanis defined as∀ ψ1 ψ2 : S, ⟪U ψ1, ι ψ2⟫_ℂ = ⟪ι ψ1, U ψ2⟫_ℂwhich is the Hermicity — i.e. symmetry. It has no domain or density hypothesis, so it does not capture genuine self-adjointness, (
A† = A, including equality of domains). For an unbounded operator on a proper dense core the two are not equivalent (TheDDimensionsoperator API already draws this line correctly.)Therefore, the PR renames to
IsSymmetricand updates the three lemmas built on it, plus docstring/headings.