From 1157efb53880c735e7eda09398a2582e460a6884 Mon Sep 17 00:00:00 2001 From: Krystian Nowakowski Date: Mon, 20 Jul 2026 11:44:26 +0200 Subject: [PATCH] refactor(QuantumMechanics): rename OneDimension UnboundedOperator.IsSelfAdjoint to IsSymmetric MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `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. --- .../QuantumMechanics/Operators/OneDimension/Momentum.lean | 4 ++-- .../QuantumMechanics/Operators/OneDimension/Parity.lean | 6 +++--- .../QuantumMechanics/Operators/OneDimension/Position.lean | 6 +++--- .../Operators/OneDimension/Unbounded.lean | 8 ++++++-- 4 files changed, 14 insertions(+), 10 deletions(-) diff --git a/Physlib/QuantumMechanics/Operators/OneDimension/Momentum.lean b/Physlib/QuantumMechanics/Operators/OneDimension/Momentum.lean index 3f8781946..a904c0cbc 100644 --- a/Physlib/QuantumMechanics/Operators/OneDimension/Momentum.lean +++ b/Physlib/QuantumMechanics/Operators/OneDimension/Momentum.lean @@ -117,11 +117,11 @@ lemma planeWaveFunctional_generalized_eigenvector_momentumOperatorUnbounded (k : /-! -## The momentum operator is self adjoint +## The momentum operator is symmetric -/ -lemma momentumOperatorUnbounded_isSelfAdjoint : momentumOperatorUnbounded.IsSelfAdjoint := by +lemma momentumOperatorUnbounded_isSymmetric : momentumOperatorUnbounded.IsSymmetric := by intro ψ1 ψ2 have hint : ∀ f g : 𝓢(ℝ, ℂ), MeasureTheory.Integrable (fun x => star (f x) * g x) MeasureTheory.volume := diff --git a/Physlib/QuantumMechanics/Operators/OneDimension/Parity.lean b/Physlib/QuantumMechanics/Operators/OneDimension/Parity.lean index 7e0469e19..a1b8b9ba4 100644 --- a/Physlib/QuantumMechanics/Operators/OneDimension/Parity.lean +++ b/Physlib/QuantumMechanics/Operators/OneDimension/Parity.lean @@ -93,14 +93,14 @@ lemma parityOperatorSchwartz_parityOperatorSchwartz (ψ : 𝓢(ℝ, ℂ)) : /-! -## Parity operator is self adjoint +## Parity operator is symmetric -/ open InnerProductSpace -lemma parityOperatorUnbounded_isSelfAdjoint : - parityOperatorUnbounded.IsSelfAdjoint := by +lemma parityOperatorUnbounded_isSymmetric : + parityOperatorUnbounded.IsSymmetric := by intro ψ1 ψ2 dsimp [parityOperatorUnbounded] rw [schwartzIncl_inner, schwartzIncl_inner] diff --git a/Physlib/QuantumMechanics/Operators/OneDimension/Position.lean b/Physlib/QuantumMechanics/Operators/OneDimension/Position.lean index 722911046..e028935dc 100644 --- a/Physlib/QuantumMechanics/Operators/OneDimension/Position.lean +++ b/Physlib/QuantumMechanics/Operators/OneDimension/Position.lean @@ -93,12 +93,12 @@ lemma positionStates_generalized_eigenvector_positionOperatorUnbounded (x : ℝ) /-! -## Position operator is self adjoint +## Position operator is symmetric -/ -lemma positionOperatorUnbounded_isSelfAdjoint : - positionOperatorUnbounded.IsSelfAdjoint := by +lemma positionOperatorUnbounded_isSymmetric : + positionOperatorUnbounded.IsSymmetric := by intro ψ1 ψ2 dsimp [positionOperatorUnbounded] rw [schwartzIncl_inner, schwartzIncl_inner] diff --git a/Physlib/QuantumMechanics/Operators/OneDimension/Unbounded.lean b/Physlib/QuantumMechanics/Operators/OneDimension/Unbounded.lean index 339e6db17..f2f140975 100644 --- a/Physlib/QuantumMechanics/Operators/OneDimension/Unbounded.lean +++ b/Physlib/QuantumMechanics/Operators/OneDimension/Unbounded.lean @@ -62,8 +62,12 @@ lemma isGeneralizedEigenvector_ofSelfCLM_iff {Op : S →L[ℂ] S} open InnerProductSpace -/-- The condition on an unbounded operator to be self-adjoint. -/ -def IsSelfAdjoint : Prop := +/-- The condition for an unbounded operator to be *symmetric* (equivalently, formally +self-adjoint): `⟪U ψ1, ι ψ2⟫ = ⟪ι ψ1, U ψ2⟫` for all `ψ1 ψ2`. This is the Hermitian +pairing on the underlying space `S`; on its own it does **not** imply genuine +self-adjointness (`A† = A`, including equality of domains), which for an unbounded +operator on a proper dense core is strictly stronger. -/ +def IsSymmetric : Prop := ∀ ψ1 ψ2 : S, ⟪U ψ1, ι ψ2⟫_ℂ = ⟪ι ψ1, U ψ2⟫_ℂ end UnboundedOperator