From b595b0b25c3fbdea4e6ac0141303becb99b3d60a Mon Sep 17 00:00:00 2001 From: Zhuoran Li Date: Wed, 23 Sep 2026 17:05:37 +0800 Subject: [PATCH 1/2] feat: add angular momentum squared and ladder operators AI assistance: Codex (GPT-6 Astra). Co-authored-by: GPT-6 Astra --- Physlib.lean | 1 + .../QuantumMechanics/Operators/API-map.yaml | 14 +- .../Operators/AngularMomentum.lean | 86 ++++ .../AngularMomentum/ThreeDimensional.lean | 416 ++++++++++++++++++ 4 files changed, 516 insertions(+), 1 deletion(-) create mode 100644 Physlib/QuantumMechanics/Operators/AngularMomentum/ThreeDimensional.lean diff --git a/Physlib.lean b/Physlib.lean index 87750fed4..7fff1b83a 100644 --- a/Physlib.lean +++ b/Physlib.lean @@ -357,6 +357,7 @@ public import Physlib.QuantumMechanics.Hydrogen.Basic public import Physlib.QuantumMechanics.Hydrogen.LaplaceRungeLenzVector public import Physlib.QuantumMechanics.InfiniteSquareWell.Basic public import Physlib.QuantumMechanics.Operators.AngularMomentum +public import Physlib.QuantumMechanics.Operators.AngularMomentum.ThreeDimensional public import Physlib.QuantumMechanics.Operators.Commutation public import Physlib.QuantumMechanics.Operators.Covariance public import Physlib.QuantumMechanics.Operators.Examples diff --git a/Physlib/QuantumMechanics/Operators/API-map.yaml b/Physlib/QuantumMechanics/Operators/API-map.yaml index 0704f8563..bb1570ad2 100644 --- a/Physlib/QuantumMechanics/Operators/API-map.yaml +++ b/Physlib/QuantumMechanics/Operators/API-map.yaml @@ -141,7 +141,19 @@ Requirements: done: true location: "Physlib/QuantumMechanics/Operators/AngularMomentum.lean (angularMomentumOperator, angularMomentumOperator_domain_eq, angularMomentumOperator_apply, angularMomentumOperator_apply_ae, angularMomentumOperator_range, angularMomentumOperator_hasDenseDomain, angularMomentumCLM_eq_momentum_position, angularMomentumOperator_isSymmetric, angularMomentumOperator_isUnbounded)" - - description: "The API shall extend angular momentum from its Schwartz domain to self-adjoint operators on the Hilbert space, with their spectra, the raising and lowering operators, the eigenvalues ℏ² l (l + 1) of 𝐋² and ℏ m of a chosen component, and the spherical harmonics as the corresponding eigenfunctions." + - description: "Angular momentum squared is lifted to the Hilbert space with invariant dense Schwartz domain, agrees with the half-sum of component squares, and is symmetric and closable." + done: true + location: "Physlib/QuantumMechanics/Operators/AngularMomentum.lean (angularMomentumSqOperator, angularMomentumSqOperator_apply, angularMomentumSqOperator_apply_ae, angularMomentumSqOperator_range, angularMomentumSqOperator_apply_eq_sum, angularMomentumSqOperator_hasDenseDomain, angularMomentumSqr_inner, angularMomentumSqOperator_isSymmetric, angularMomentumSqOperator_isUnbounded)" + + - description: "The right-handed Cartesian components in three dimensions act on the invariant Schwartz domain, satisfy the Levi-Civita and cyclic commutation relations, and their three squares sum to angular momentum squared." + done: true + location: "Physlib/QuantumMechanics/Operators/AngularMomentum/ThreeDimensional.lean (angularMomentum3DOperator, angularMomentum3DOperator_isSymmetric, angularMomentumOperatorSqr_eq_sum_3D, angularMomentumSqOperator_apply_eq_sum_3D, angularMomentum3D_commutation, angularMomentum3D_commutation_xy, angularMomentum3D_commutation_yz, angularMomentum3D_commutation_zx, angularMomentum3DOperator_commutation, angularMomentumSqOperator_commutation_3D)" + + - description: "Angular momentum ladder operators LΒ± = Lx Β± i Ly are defined on Schwartz maps and lifted to the Hilbert space with invariant dense Schwartz domain, where [Lz, LΒ±] = ±ℏ LΒ± and [LΒ², LΒ±] = 0." + done: true + location: "Physlib/QuantumMechanics/Operators/AngularMomentum/ThreeDimensional.lean (angularMomentumRaisingCLM, angularMomentumLoweringCLM, angularMomentumRaisingOperator, angularMomentumLoweringOperator, angularMomentumZ_commutation_raising, angularMomentumZ_commutation_lowering, angularMomentumSqr_commutation_raising, angularMomentumSqr_commutation_lowering, angularMomentumZOperator_commutation_raising, angularMomentumZOperator_commutation_lowering, angularMomentumSqOperator_commutation_raising, angularMomentumSqOperator_commutation_lowering)" + + - description: "The API shall extend angular momentum from its Schwartz domain to self-adjoint operators on the Hilbert space, with their spectra, the eigenvalues ℏ² l (l + 1) of 𝐋² and ℏ m of a chosen component, and the spherical harmonics as the corresponding eigenfunctions." done: false location: N/A diff --git a/Physlib/QuantumMechanics/Operators/AngularMomentum.lean b/Physlib/QuantumMechanics/Operators/AngularMomentum.lean index 1ba32f8de..7c7920ece 100644 --- a/Physlib/QuantumMechanics/Operators/AngularMomentum.lean +++ b/Physlib/QuantumMechanics/Operators/AngularMomentum.lean @@ -27,9 +27,11 @@ Definitions: - `angularMomentumOperator3D` : the (pseudo)vector angular momentum operator for `d = 3`. - `angularMomentumOperator` : each component as a partially defined operator on `SpaceDHilbertSpace d`, preserving the dense Schwartz submodule. +- `angularMomentumSqOperator` : angular momentum squared on the same Schwartz domain. Lemmas: - `angularMomentumOperator_isSymmetric` : angular momentum is symmetric on the Schwartz domain. +- `angularMomentumSqOperator_isSymmetric` : its sum of component squares is also symmetric. - `angularMomentum_commutation_angularMomentum` : angular momenta generate an `𝔰𝔬(d)` algebra. Notation: @@ -43,6 +45,7 @@ Notation: - B. Angular momentum squared operator - C. Special cases in low dimensions - D. Hilbert-space angular momentum operator + - D.1. Angular momentum squared on the Hilbert space - E. Commutation relations - E.1. Angular momentum / position - E.2. Angular momentum / momentum @@ -156,6 +159,7 @@ def angularMomentumOperator3D (i : Fin 3) : 𝓒(Space 3, β„‚) β†’L[β„‚] 𝓒(Sp -/ open MeasureTheory SpaceDHilbertSpace SchwartzSubmodule +open scoped InnerProductSpace variable {d : β„•} (i j : Fin d) @@ -207,6 +211,88 @@ lemma angularMomentumOperator_isUnbounded : (angularMomentumOperator_isSymmetric i j).isUnbounded_iff_hasDenseDomain.mpr (angularMomentumOperator_hasDenseDomain i j) +/-- The component symmetry identity, expressed directly on Schwartz maps. -/ +lemma angularMomentumCLM_inner (f g : 𝓒(Space d, β„‚)) : + βŸͺ(schwartzEquiv volume (𝐋 i j f) : SpaceDHilbertSpace d), schwartzEquiv volume g⟫_β„‚ = + βŸͺ(schwartzEquiv volume f : SpaceDHilbertSpace d), schwartzEquiv volume (𝐋 i j g)⟫_β„‚ := by + simpa only [angularMomentumOperator_apply, LinearEquiv.symm_apply_apply] using + angularMomentumOperator_isSymmetric i j (schwartzEquiv volume f) (schwartzEquiv volume g) + +/-! +### D.1. Angular momentum squared on the Hilbert space +-/ + +/-- Angular momentum squared on the Hilbert space, with the invariant Schwartz domain. +This transports the existing Schwartz operator `𝐋²`, including its factor `1/2`. -/ +def angularMomentumSqOperator : SpaceDHilbertSpace d β†’β‚—.[β„‚] SpaceDHilbertSpace d where + domain := SchwartzSubmodule d + toFun := (schwartzIncl volume).1 βˆ˜β‚— (𝐋²).1 βˆ˜β‚— (schwartzEquiv volume).symm.1 + +@[inherit_doc QuantumMechanics.angularMomentumSqOperator] +scoped[AngularMomentum] notation "𝓛²" => QuantumMechanics.angularMomentumSqOperator + +lemma angularMomentumSqOperator_domain_eq : + (angularMomentumSqOperator (d := d)).domain = SchwartzSubmodule d := rfl + +lemma angularMomentumSqOperator_apply (ψ : SchwartzSubmodule d) : + angularMomentumSqOperator ψ = + schwartzEquiv volume (𝐋² ((schwartzEquiv volume).symm ψ)) := rfl + +lemma angularMomentumSqOperator_apply_ae (ψ : SchwartzSubmodule d) : + angularMomentumSqOperator ψ =ᡐ[volume] 𝐋² ((schwartzEquiv volume).symm ψ) := + schwartzEquiv_coe_ae _ + +lemma angularMomentumSqOperator_range (ψ : SchwartzSubmodule d) : + angularMomentumSqOperator ψ ∈ SchwartzSubmodule d := by + simp [angularMomentumSqOperator_apply] + +/-- The squared operator is the sum of squares of Hilbert-space components on their +common invariant domain. The inner applications land in Schwartz by `angularMomentumOperator_range`. +-/ +lemma angularMomentumSqOperator_apply_eq_sum (ψ : SchwartzSubmodule d) : + angularMomentumSqOperator ψ = (2 : β„‚)⁻¹ β€’ βˆ‘ i, βˆ‘ j, + angularMomentumOperator i j + ⟨angularMomentumOperator i j ψ, angularMomentumOperator_range i j ψ⟩ := by + obtain ⟨f, rfl⟩ := (schwartzEquiv volume).surjective ψ + simp only [angularMomentumSqOperator_apply, angularMomentumOperator_apply, + LinearEquiv.symm_apply_apply, angularMomentumOperatorSqr_apply_fun, + map_smul, map_sum, Submodule.coe_sum, Submodule.coe_smul] + congr 1 + apply Finset.sum_congr rfl + intro i _ + apply Finset.sum_congr rfl + intro j _ + change _ = schwartzIncl volume + (𝐋 i j ((schwartzEquiv volume).symm (schwartzEquiv volume (𝐋 i j f)))) + rw [LinearEquiv.symm_apply_apply] + rfl + +lemma angularMomentumSqOperator_hasDenseDomain : + (angularMomentumSqOperator (d := d)).HasDenseDomain := SchwartzSubmodule.dense d _ + +/-- Symmetry of `𝐋²` follows by moving each component across the inner product twice. -/ +lemma angularMomentumSqr_inner (f g : 𝓒(Space d, β„‚)) : + βŸͺ(schwartzEquiv volume (𝐋² f) : SpaceDHilbertSpace d), schwartzEquiv volume g⟫_β„‚ = + βŸͺ(schwartzEquiv volume f : SpaceDHilbertSpace d), schwartzEquiv volume (𝐋² g)⟫_β„‚ := by + simp only [angularMomentumOperatorSqr_apply_fun, map_smul, map_sum, + Submodule.coe_smul, Submodule.coe_sum, inner_smul_left, inner_smul_right, + sum_inner, inner_sum, angularMomentumCLM_inner, map_invβ‚€, map_ofNat] + +/-- Angular momentum squared is symmetric on the Schwartz domain. -/ +lemma angularMomentumSqOperator_isSymmetric : + (angularMomentumSqOperator (d := d)).IsSymmetric := by + intro ψ Ο† + obtain ⟨f, rfl⟩ := (schwartzEquiv volume).surjective ψ + obtain ⟨g, rfl⟩ := (schwartzEquiv volume).surjective Ο† + simpa only [angularMomentumSqOperator_apply, LinearEquiv.symm_apply_apply] using + angularMomentumSqr_inner f g + +/-- In Physlib terminology, the squared operator is densely defined and closable. -/ +lemma angularMomentumSqOperator_isUnbounded : + (angularMomentumSqOperator (d := d)).IsUnbounded := + angularMomentumSqOperator_isSymmetric.isUnbounded_iff_hasDenseDomain.mpr + angularMomentumSqOperator_hasDenseDomain + /-! ## E. Commutation relations -/ diff --git a/Physlib/QuantumMechanics/Operators/AngularMomentum/ThreeDimensional.lean b/Physlib/QuantumMechanics/Operators/AngularMomentum/ThreeDimensional.lean new file mode 100644 index 000000000..c1ccb7288 --- /dev/null +++ b/Physlib/QuantumMechanics/Operators/AngularMomentum/ThreeDimensional.lean @@ -0,0 +1,416 @@ +/- +Copyright (c) 2026 Zhuoran Li. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Zhuoran Li +-/ +module + +public import Physlib.QuantumMechanics.Operators.AngularMomentum +public import Physlib.Mathematics.LeviCivita.Basic + +/-! +# Three-dimensional angular momentum + +## i. Overview + +The Cartesian components use the right-handed convention +`Lx = L₁₂`, `Ly = Lβ‚‚β‚€`, `Lz = L₀₁`, with coordinate indices `0, 1, 2`. +The Schwartz operators are the existing `angularMomentumOperator3D`; the Hilbert-space +operators have the common invariant domain `SchwartzSubmodule 3`. +Their commutation algebra and the raising/lowering operators are proved first on Schwartz maps +and then transported to this Hilbert-space domain. In particular, a zero commutator means zero +on that domain; it is not an equality with the everywhere-defined zero `LinearPMap`. + +## ii. Key results + +- `angularMomentum3DOperator`: the Hilbert-space Cartesian components. +- `angularMomentumOperatorSqr_eq_sum_3D`: `LΒ² = LxΒ² + LyΒ² + LzΒ²` on Schwartz maps. +- `angularMomentum3DOperator_isSymmetric`: symmetry of each Cartesian component. +- `angularMomentum3D_commutation`: `[Li, Lj] = iℏ βˆ‘k Ξ΅ijk Lk`. +- `angularMomentumRaisingCLM`, `angularMomentumLoweringCLM`: `Lx Β± i Ly` on Schwartz maps. +- `angularMomentumRaisingOperator`, `angularMomentumLoweringOperator`: their Hilbert-space lifts. +- `angularMomentumZOperator_commutation_raising`, `angularMomentumZOperator_commutation_lowering`: + `[Lz, LΒ±] = ±ℏ LΒ±` on the Schwartz domain. +- `angularMomentumSqOperator_commutation_raising`, `angularMomentumSqOperator_commutation_lowering`: + `[LΒ², LΒ±] = 0` on that domain. + +Open the `AngularMomentum` scope for `𝐋x`, `𝐋y`, `𝐋z` on Schwartz maps and +`𝓛x`, `𝓛y`, `𝓛z`, `𝓛²` on the Hilbert space. +The same scope provides `𝐋⁺`, `𝐋⁻` and `𝓛⁺`, `𝓛⁻` for the ladder operators. + +## iii. Table of contents + +- A. Cartesian components + - A.1. Hilbert-space transport + - A.2. Sum of the three squares +- B. Commutation algebra +- C. Ladder operators + - C.1. Hilbert-space ladder operators + - C.2. Hilbert-space commutation relations on the invariant domain + +## iv. References + +* None. +-/ + +@[expose] public section + +namespace QuantumMechanics +noncomputable section + +open Complex Constants SchwartzMap ContinuousLinearMap MeasureTheory +open SpaceDHilbertSpace SchwartzSubmodule +open scoped InnerProductSpace + +/-! +## A. Cartesian components +-/ + +@[inherit_doc QuantumMechanics.angularMomentumOperator3D] +scoped[AngularMomentum] notation "𝐋x" => QuantumMechanics.angularMomentumOperator3D 0 +@[inherit_doc QuantumMechanics.angularMomentumOperator3D] +scoped[AngularMomentum] notation "𝐋y" => QuantumMechanics.angularMomentumOperator3D 1 +@[inherit_doc QuantumMechanics.angularMomentumOperator3D] +scoped[AngularMomentum] notation "𝐋z" => QuantumMechanics.angularMomentumOperator3D 2 + +/-- The Cartesian Hilbert-space components, ordered as `x, y, z`. -/ +def angularMomentum3DOperator (i : Fin 3) : + SpaceDHilbertSpace 3 β†’β‚—.[β„‚] SpaceDHilbertSpace 3 where + domain := SchwartzSubmodule 3 + toFun := (schwartzIncl volume).1 βˆ˜β‚— (angularMomentumOperator3D i).1 βˆ˜β‚— + (schwartzEquiv volume).symm.1 + +@[inherit_doc QuantumMechanics.angularMomentum3DOperator] +scoped[AngularMomentum] notation "𝓛x" => QuantumMechanics.angularMomentum3DOperator 0 +@[inherit_doc QuantumMechanics.angularMomentum3DOperator] +scoped[AngularMomentum] notation "𝓛y" => QuantumMechanics.angularMomentum3DOperator 1 +@[inherit_doc QuantumMechanics.angularMomentum3DOperator] +scoped[AngularMomentum] notation "𝓛z" => QuantumMechanics.angularMomentum3DOperator 2 + +open scoped AngularMomentum + +lemma angularMomentumOperator3D_x : 𝐋x = 𝐋 1 2 := rfl +lemma angularMomentumOperator3D_y : 𝐋y = 𝐋 2 0 := rfl +lemma angularMomentumOperator3D_z : 𝐋z = 𝐋 0 1 := rfl + +lemma angularMomentum3DOperator_x : 𝓛x = angularMomentumOperator 1 2 := rfl +lemma angularMomentum3DOperator_y : 𝓛y = angularMomentumOperator 2 0 := rfl +lemma angularMomentum3DOperator_z : 𝓛z = angularMomentumOperator 0 1 := rfl + +/-! +### A.1. Hilbert-space transport +-/ + +variable (i : Fin 3) + +lemma angularMomentum3DOperator_domain_eq : + (angularMomentum3DOperator i).domain = SchwartzSubmodule 3 := rfl + +lemma angularMomentum3DOperator_apply (ψ : SchwartzSubmodule 3) : + angularMomentum3DOperator i ψ = + schwartzEquiv volume (angularMomentumOperator3D i ((schwartzEquiv volume).symm ψ)) := rfl + +lemma angularMomentum3DOperator_apply_ae (ψ : SchwartzSubmodule 3) : + angularMomentum3DOperator i ψ =ᡐ[volume] + angularMomentumOperator3D i ((schwartzEquiv volume).symm ψ) := schwartzEquiv_coe_ae _ + +lemma angularMomentum3DOperator_range (ψ : SchwartzSubmodule 3) : + angularMomentum3DOperator i ψ ∈ SchwartzSubmodule 3 := by + simp [angularMomentum3DOperator_apply] + +/-- Composing two components stays on the common Schwartz domain. -/ +lemma angularMomentum3DOperator_apply_apply (j : Fin 3) (ψ : SchwartzSubmodule 3) : + angularMomentum3DOperator i + ⟨angularMomentum3DOperator j ψ, angularMomentum3DOperator_range j ψ⟩ = + schwartzEquiv volume (angularMomentumOperator3D i + (angularMomentumOperator3D j ((schwartzEquiv volume).symm ψ))) := by + change schwartzIncl volume (angularMomentumOperator3D i ((schwartzEquiv volume).symm + (schwartzEquiv volume (angularMomentumOperator3D j ((schwartzEquiv volume).symm ψ))))) = _ + rw [LinearEquiv.symm_apply_apply] + rfl + +lemma angularMomentum3DOperator_hasDenseDomain : + (angularMomentum3DOperator i).HasDenseDomain := SchwartzSubmodule.dense 3 _ + +lemma angularMomentum3DOperator_isSymmetric : + (angularMomentum3DOperator i).IsSymmetric := by + fin_cases i <;> exact angularMomentumOperator_isSymmetric _ _ + +lemma angularMomentum3DOperator_isUnbounded : + (angularMomentum3DOperator i).IsUnbounded := + (angularMomentum3DOperator_isSymmetric i).isUnbounded_iff_hasDenseDomain.mpr + (angularMomentum3DOperator_hasDenseDomain i) + +/-! +### A.2. Sum of the three squares +-/ + +/-- The antisymmetric-index definition agrees with the Cartesian sum of squares. -/ +lemma angularMomentumOperatorSqr_eq_sum_3D : + 𝐋²[3] = βˆ‘ i : Fin 3, angularMomentumOperator3D i ∘L angularMomentumOperator3D i := by + simp only [angularMomentumOperatorSqr, Fin.sum_univ_three, angularMomentumOperator3D, + angularMomentumCLM_eq_zero, angularMomentumCLM_antisymm (0 : Fin 3) 2, + angularMomentumCLM_antisymm (1 : Fin 3) 0, angularMomentumCLM_antisymm (2 : Fin 3) 1, + comp_zero, neg_comp, comp_neg, neg_neg, add_zero, zero_add] + module + +/-- The same Cartesian sum of squares, evaluated on a Hilbert-space Schwartz vector. -/ +lemma angularMomentumSqOperator_apply_eq_sum_3D (ψ : SchwartzSubmodule 3) : + angularMomentumSqOperator ψ = βˆ‘ i : Fin 3, angularMomentum3DOperator i + ⟨angularMomentum3DOperator i ψ, angularMomentum3DOperator_range i ψ⟩ := by + simp [angularMomentumSqOperator_apply, angularMomentumOperatorSqr_eq_sum_3D, + angularMomentum3DOperator_apply_apply] + +/-! +## B. Commutation algebra + +The bracket below is the existing commutator of continuous linear maps on Schwartz space. +Hilbert-space statements are evaluated on `SchwartzSubmodule 3`, with explicit membership +proofs for intermediate vectors. They make no claims about domains of closed extensions. +-/ + +open KroneckerDelta + +attribute [local instance 100] LieRing.ofAssociativeRing +attribute [local instance 100] LieAlgebra.ofAssociativeAlgebra + +set_option backward.isDefEq.respectTransparency false in +/-- The Cartesian angular momentum algebra, with the right-handed Levi-Civita symbol. -/ +lemma angularMomentum3D_commutation (j : Fin 3) : + ⁅angularMomentumOperator3D i, angularMomentumOperator3D j⁆ = + (I * ℏ) β€’ βˆ‘ k : Fin 3, (leviCivitaSymbol ![i, j, k] : β„‚) β€’ + angularMomentumOperator3D k := by + simp only [leviCivitaSymbol_eq_det, Matrix.det_fin_three] + fin_cases i <;> fin_cases j <;> + norm_num [angularMomentumOperator3D, angularMomentum_commutation_angularMomentum, + kroneckerDelta, Fin.sum_univ_three, angularMomentumCLM_eq_zero, + angularMomentumCLM_antisymm (0 : Fin 3) 2, angularMomentumCLM_antisymm (1 : Fin 3) 0, + angularMomentumCLM_antisymm (2 : Fin 3) 1] + +/-- `[Lx, Ly] = iℏ Lz`. -/ +lemma angularMomentum3D_commutation_xy : ⁅𝐋x, 𝐋y⁆ = (I * ℏ) β€’ 𝐋z := by + simpa [angularMomentumOperator3D, kroneckerDelta, + angularMomentumCLM_antisymm (1 : Fin 3) 0] using + angularMomentum_commutation_angularMomentum (d := 3) 1 2 2 0 + +/-- `[Ly, Lz] = iℏ Lx`. -/ +lemma angularMomentum3D_commutation_yz : ⁅𝐋y, 𝐋z⁆ = (I * ℏ) β€’ 𝐋x := by + simpa [angularMomentumOperator3D, kroneckerDelta, + angularMomentumCLM_antisymm (2 : Fin 3) 1] using + angularMomentum_commutation_angularMomentum (d := 3) 2 0 0 1 + +/-- `[Lz, Lx] = iℏ Ly`. -/ +lemma angularMomentum3D_commutation_zx : ⁅𝐋z, 𝐋x⁆ = (I * ℏ) β€’ 𝐋y := by + simpa [angularMomentumOperator3D, kroneckerDelta, + angularMomentumCLM_antisymm (0 : Fin 3) 2] using + angularMomentum_commutation_angularMomentum (d := 3) 0 1 1 2 + +/-- Angular momentum squared commutes with every Cartesian component on Schwartz maps. -/ +lemma angularMomentumSqr_commutation_3D : ⁅𝐋²[3], angularMomentumOperator3D i⁆ = 0 := by + fin_cases i <;> exact angularMomentumSqr_commutation_angularMomentum _ _ + +/-- The Cartesian commutation algebra on the common Hilbert-space Schwartz domain. -/ +lemma angularMomentum3DOperator_commutation (j : Fin 3) (ψ : SchwartzSubmodule 3) : + angularMomentum3DOperator i + ⟨angularMomentum3DOperator j ψ, angularMomentum3DOperator_range j ψ⟩ - + angularMomentum3DOperator j + ⟨angularMomentum3DOperator i ψ, angularMomentum3DOperator_range i ψ⟩ = + (I * ℏ) β€’ βˆ‘ k : Fin 3, (leviCivitaSymbol ![i, j, k] : β„‚) β€’ + angularMomentum3DOperator k ψ := by + rw [angularMomentum3DOperator_apply_apply, angularMomentum3DOperator_apply_apply] + have h := congrArg + (fun A : 𝓒(Space 3, β„‚) β†’L[β„‚] 𝓒(Space 3, β„‚) => + schwartzIncl volume (A ((schwartzEquiv volume).symm ψ))) + (angularMomentum3D_commutation i j) + simpa only [Ring.lie_def, ContinuousLinearMap.mul_def, sub_apply, comp_apply, smul_apply, + _root_.sum_apply, map_sub, map_smul, map_sum, + angularMomentum3DOperator_apply, schwartzEquiv_apply_coe] using h + +/-- `[LΒ², Li] = 0` on the common invariant Hilbert-space domain. -/ +lemma angularMomentumSqOperator_commutation_3D (ψ : SchwartzSubmodule 3) : + angularMomentumSqOperator + ⟨angularMomentum3DOperator i ψ, angularMomentum3DOperator_range i ψ⟩ - + angularMomentum3DOperator i + ⟨angularMomentumSqOperator ψ, angularMomentumSqOperator_range ψ⟩ = 0 := by + change schwartzIncl volume (𝐋² ((schwartzEquiv volume).symm + (schwartzEquiv volume (angularMomentumOperator3D i ((schwartzEquiv volume).symm ψ))))) - + schwartzIncl volume (angularMomentumOperator3D i ((schwartzEquiv volume).symm + (schwartzEquiv volume (𝐋² ((schwartzEquiv volume).symm ψ))))) = 0 + simp only [LinearEquiv.symm_apply_apply] + have h := congrArg + (fun A : 𝓒(Space 3, β„‚) β†’L[β„‚] 𝓒(Space 3, β„‚) => + schwartzIncl volume (A ((schwartzEquiv volume).symm ψ))) + (angularMomentumSqr_commutation_3D i) + simpa only [Ring.lie_def, ContinuousLinearMap.mul_def, sub_apply, comp_apply, zero_apply, + map_sub, map_zero] using h + +/-! +## C. Ladder operators + +These operators act on arbitrary Schwartz vectors. No eigenstate or spectral assumptions +are used in their commutation relations. +-/ + +/-- The angular momentum raising operator `Lβ‚Š = Lx + i Ly` on Schwartz maps. -/ +def angularMomentumRaisingCLM : 𝓒(Space 3, β„‚) β†’L[β„‚] 𝓒(Space 3, β„‚) := 𝐋x + I β€’ 𝐋y + +/-- The angular momentum lowering operator `Lβ‚‹ = Lx - i Ly` on Schwartz maps. -/ +def angularMomentumLoweringCLM : 𝓒(Space 3, β„‚) β†’L[β„‚] 𝓒(Space 3, β„‚) := 𝐋x - I β€’ 𝐋y + +@[inherit_doc QuantumMechanics.angularMomentumRaisingCLM] +scoped[AngularMomentum] notation "𝐋⁺" => QuantumMechanics.angularMomentumRaisingCLM +@[inherit_doc QuantumMechanics.angularMomentumLoweringCLM] +scoped[AngularMomentum] notation "𝐋⁻" => QuantumMechanics.angularMomentumLoweringCLM + +/-- `[Lz, Lβ‚Š] = ℏ Lβ‚Š`. -/ +lemma angularMomentumZ_commutation_raising : ⁅𝐋z, 𝐋⁺⁆ = (ℏ : β„‚) β€’ 𝐋⁺ := by + rw [angularMomentumRaisingCLM, lie_add, lie_smul, angularMomentum3D_commutation_zx, + ← lie_skew 𝐋z 𝐋y, angularMomentum3D_commutation_yz] + simp only [smul_neg, smul_smul, ← mul_assoc, I_mul_I, neg_one_mul] + module + +/-- `[Lz, Lβ‚‹] = -ℏ Lβ‚‹`. -/ +lemma angularMomentumZ_commutation_lowering : ⁅𝐋z, 𝐋⁻⁆ = -(ℏ : β„‚) β€’ 𝐋⁻ := by + rw [angularMomentumLoweringCLM, lie_sub, lie_smul, angularMomentum3D_commutation_zx, + ← lie_skew 𝐋z 𝐋y, angularMomentum3D_commutation_yz] + simp only [smul_neg, smul_smul, ← mul_assoc, I_mul_I, neg_one_mul] + module + +/-- Angular momentum squared commutes with the raising operator. -/ +lemma angularMomentumSqr_commutation_raising : ⁅𝐋²[3], 𝐋⁺⁆ = 0 := by + simp [angularMomentumRaisingCLM, lie_add, lie_smul, angularMomentumSqr_commutation_3D] + +/-- Angular momentum squared commutes with the lowering operator. -/ +lemma angularMomentumSqr_commutation_lowering : ⁅𝐋²[3], 𝐋⁻⁆ = 0 := by + simp [angularMomentumLoweringCLM, lie_sub, lie_smul, angularMomentumSqr_commutation_3D] + +/-! +### C.1. Hilbert-space ladder operators +-/ + +/-- The raising operator on the Hilbert space, with Schwartz domain. -/ +def angularMomentumRaisingOperator : SpaceDHilbertSpace 3 β†’β‚—.[β„‚] SpaceDHilbertSpace 3 where + domain := SchwartzSubmodule 3 + toFun := (schwartzIncl volume).1 βˆ˜β‚— (𝐋⁺).1 βˆ˜β‚— (schwartzEquiv volume).symm.1 + +/-- The lowering operator on the Hilbert space, with Schwartz domain. -/ +def angularMomentumLoweringOperator : SpaceDHilbertSpace 3 β†’β‚—.[β„‚] SpaceDHilbertSpace 3 where + domain := SchwartzSubmodule 3 + toFun := (schwartzIncl volume).1 βˆ˜β‚— (𝐋⁻).1 βˆ˜β‚— (schwartzEquiv volume).symm.1 + +@[inherit_doc QuantumMechanics.angularMomentumRaisingOperator] +scoped[AngularMomentum] notation "𝓛⁺" => QuantumMechanics.angularMomentumRaisingOperator +@[inherit_doc QuantumMechanics.angularMomentumLoweringOperator] +scoped[AngularMomentum] notation "𝓛⁻" => QuantumMechanics.angularMomentumLoweringOperator + +lemma angularMomentumRaisingOperator_domain_eq : (𝓛⁺).domain = SchwartzSubmodule 3 := rfl +lemma angularMomentumLoweringOperator_domain_eq : (𝓛⁻).domain = SchwartzSubmodule 3 := rfl + +lemma angularMomentumRaisingOperator_apply (ψ : SchwartzSubmodule 3) : + 𝓛⁺ ψ = schwartzEquiv volume (𝐋⁺ ((schwartzEquiv volume).symm ψ)) := rfl + +lemma angularMomentumLoweringOperator_apply (ψ : SchwartzSubmodule 3) : + 𝓛⁻ ψ = schwartzEquiv volume (𝐋⁻ ((schwartzEquiv volume).symm ψ)) := rfl + +lemma angularMomentumRaisingOperator_apply_eq (ψ : SchwartzSubmodule 3) : + 𝓛⁺ ψ = 𝓛x ψ + I β€’ 𝓛y ψ := by + simp [angularMomentumRaisingOperator_apply, angularMomentumRaisingCLM, + angularMomentum3DOperator_apply] + +lemma angularMomentumLoweringOperator_apply_eq (ψ : SchwartzSubmodule 3) : + 𝓛⁻ ψ = 𝓛x ψ - I β€’ 𝓛y ψ := by + simp [angularMomentumLoweringOperator_apply, angularMomentumLoweringCLM, + angularMomentum3DOperator_apply] + +lemma angularMomentumRaisingOperator_apply_ae (ψ : SchwartzSubmodule 3) : + 𝓛⁺ ψ =ᡐ[volume] 𝐋⁺ ((schwartzEquiv volume).symm ψ) := schwartzEquiv_coe_ae _ + +lemma angularMomentumLoweringOperator_apply_ae (ψ : SchwartzSubmodule 3) : + 𝓛⁻ ψ =ᡐ[volume] 𝐋⁻ ((schwartzEquiv volume).symm ψ) := schwartzEquiv_coe_ae _ + +lemma angularMomentumRaisingOperator_range (ψ : SchwartzSubmodule 3) : + 𝓛⁺ ψ ∈ SchwartzSubmodule 3 := by + simp [angularMomentumRaisingOperator_apply] + +lemma angularMomentumLoweringOperator_range (ψ : SchwartzSubmodule 3) : + 𝓛⁻ ψ ∈ SchwartzSubmodule 3 := by + simp [angularMomentumLoweringOperator_apply] + +lemma angularMomentumRaisingOperator_hasDenseDomain : (𝓛⁺).HasDenseDomain := + SchwartzSubmodule.dense 3 _ + +lemma angularMomentumLoweringOperator_hasDenseDomain : (𝓛⁻).HasDenseDomain := + SchwartzSubmodule.dense 3 _ + +/-! +### C.2. Hilbert-space commutation relations on the invariant domain +-/ + +/-- `[Lz, Lβ‚Š] ψ = ℏ Lβ‚Š ψ` for every Schwartz vector in the Hilbert space. -/ +lemma angularMomentumZOperator_commutation_raising (ψ : SchwartzSubmodule 3) : + 𝓛z βŸ¨π“›βΊ ψ, angularMomentumRaisingOperator_range ψ⟩ - + 𝓛⁺ βŸ¨π“›z ψ, angularMomentum3DOperator_range 2 ψ⟩ = (ℏ : β„‚) β€’ 𝓛⁺ ψ := by + change schwartzIncl volume (𝐋z ((schwartzEquiv volume).symm + (schwartzEquiv volume (𝐋⁺ ((schwartzEquiv volume).symm ψ))))) - + schwartzIncl volume (𝐋⁺ ((schwartzEquiv volume).symm + (schwartzEquiv volume (𝐋z ((schwartzEquiv volume).symm ψ))))) = + (ℏ : β„‚) β€’ schwartzIncl volume (𝐋⁺ ((schwartzEquiv volume).symm ψ)) + simp only [LinearEquiv.symm_apply_apply] + have h := congrArg + (fun A : 𝓒(Space 3, β„‚) β†’L[β„‚] 𝓒(Space 3, β„‚) => + schwartzIncl volume (A ((schwartzEquiv volume).symm ψ))) + angularMomentumZ_commutation_raising + simpa only [Ring.lie_def, ContinuousLinearMap.mul_def, sub_apply, comp_apply, smul_apply, + map_sub, map_smul] using h + +/-- `[Lz, Lβ‚‹] ψ = -ℏ Lβ‚‹ ψ` for every Schwartz vector in the Hilbert space. -/ +lemma angularMomentumZOperator_commutation_lowering (ψ : SchwartzSubmodule 3) : + 𝓛z βŸ¨π“›β» ψ, angularMomentumLoweringOperator_range ψ⟩ - + 𝓛⁻ βŸ¨π“›z ψ, angularMomentum3DOperator_range 2 ψ⟩ = -(ℏ : β„‚) β€’ 𝓛⁻ ψ := by + change schwartzIncl volume (𝐋z ((schwartzEquiv volume).symm + (schwartzEquiv volume (𝐋⁻ ((schwartzEquiv volume).symm ψ))))) - + schwartzIncl volume (𝐋⁻ ((schwartzEquiv volume).symm + (schwartzEquiv volume (𝐋z ((schwartzEquiv volume).symm ψ))))) = + -(ℏ : β„‚) β€’ schwartzIncl volume (𝐋⁻ ((schwartzEquiv volume).symm ψ)) + simp only [LinearEquiv.symm_apply_apply] + have h := congrArg + (fun A : 𝓒(Space 3, β„‚) β†’L[β„‚] 𝓒(Space 3, β„‚) => + schwartzIncl volume (A ((schwartzEquiv volume).symm ψ))) + angularMomentumZ_commutation_lowering + simpa only [Ring.lie_def, ContinuousLinearMap.mul_def, sub_apply, comp_apply, smul_apply, + map_sub, map_smul] using h + +/-- `[LΒ², Lβ‚Š] ψ = 0` on the common invariant Schwartz domain. -/ +lemma angularMomentumSqOperator_commutation_raising (ψ : SchwartzSubmodule 3) : + 𝓛² βŸ¨π“›βΊ ψ, angularMomentumRaisingOperator_range ψ⟩ - + 𝓛⁺ βŸ¨π“›Β² ψ, angularMomentumSqOperator_range ψ⟩ = 0 := by + change schwartzIncl volume (𝐋² ((schwartzEquiv volume).symm + (schwartzEquiv volume (𝐋⁺ ((schwartzEquiv volume).symm ψ))))) - + schwartzIncl volume (𝐋⁺ ((schwartzEquiv volume).symm + (schwartzEquiv volume (𝐋² ((schwartzEquiv volume).symm ψ))))) = 0 + simp only [LinearEquiv.symm_apply_apply] + have h := congrArg + (fun A : 𝓒(Space 3, β„‚) β†’L[β„‚] 𝓒(Space 3, β„‚) => + schwartzIncl volume (A ((schwartzEquiv volume).symm ψ))) + angularMomentumSqr_commutation_raising + simpa only [Ring.lie_def, ContinuousLinearMap.mul_def, sub_apply, comp_apply, zero_apply, + map_sub, map_zero] using h + +/-- `[LΒ², Lβ‚‹] ψ = 0` on the common invariant Schwartz domain. -/ +lemma angularMomentumSqOperator_commutation_lowering (ψ : SchwartzSubmodule 3) : + 𝓛² βŸ¨π“›β» ψ, angularMomentumLoweringOperator_range ψ⟩ - + 𝓛⁻ βŸ¨π“›Β² ψ, angularMomentumSqOperator_range ψ⟩ = 0 := by + change schwartzIncl volume (𝐋² ((schwartzEquiv volume).symm + (schwartzEquiv volume (𝐋⁻ ((schwartzEquiv volume).symm ψ))))) - + schwartzIncl volume (𝐋⁻ ((schwartzEquiv volume).symm + (schwartzEquiv volume (𝐋² ((schwartzEquiv volume).symm ψ))))) = 0 + simp only [LinearEquiv.symm_apply_apply] + have h := congrArg + (fun A : 𝓒(Space 3, β„‚) β†’L[β„‚] 𝓒(Space 3, β„‚) => + schwartzIncl volume (A ((schwartzEquiv volume).symm ψ))) + angularMomentumSqr_commutation_lowering + simpa only [Ring.lie_def, ContinuousLinearMap.mul_def, sub_apply, comp_apply, zero_apply, + map_sub, map_zero] using h + +end +end QuantumMechanics From af77d68832629e68f40a42ddbcba68ed2a603483 Mon Sep 17 00:00:00 2001 From: Zhuoran Li Date: Thu, 24 Sep 2026 18:19:28 +0800 Subject: [PATCH 2/2] refactor: unify three-dimensional angular momentum API Use indexed notation and DimThree names for the new component API. Generalize crossProductVee to arbitrary coefficients and reuse it with the transpose that preserves the angular-momentum sign convention. AI assistance: Codex (GPT-6 Astra). Co-authored-by: GPT-6 Astra --- Physlib.lean | 2 +- Physlib/Mathematics/CrossProductMatrix.lean | 8 +- .../QuantumMechanics/Operators/API-map.yaml | 4 +- .../Operators/AngularMomentum.lean | 9 +- .../{ThreeDimensional.lean => DimThree.lean} | 206 +++++++++--------- 5 files changed, 111 insertions(+), 118 deletions(-) rename Physlib/QuantumMechanics/Operators/AngularMomentum/{ThreeDimensional.lean => DimThree.lean} (66%) diff --git a/Physlib.lean b/Physlib.lean index 7fff1b83a..68f17525d 100644 --- a/Physlib.lean +++ b/Physlib.lean @@ -357,7 +357,7 @@ public import Physlib.QuantumMechanics.Hydrogen.Basic public import Physlib.QuantumMechanics.Hydrogen.LaplaceRungeLenzVector public import Physlib.QuantumMechanics.InfiniteSquareWell.Basic public import Physlib.QuantumMechanics.Operators.AngularMomentum -public import Physlib.QuantumMechanics.Operators.AngularMomentum.ThreeDimensional +public import Physlib.QuantumMechanics.Operators.AngularMomentum.DimThree public import Physlib.QuantumMechanics.Operators.Commutation public import Physlib.QuantumMechanics.Operators.Covariance public import Physlib.QuantumMechanics.Operators.Examples diff --git a/Physlib/Mathematics/CrossProductMatrix.lean b/Physlib/Mathematics/CrossProductMatrix.lean index e48a8c101..06b1943fc 100644 --- a/Physlib/Mathematics/CrossProductMatrix.lean +++ b/Physlib/Mathematics/CrossProductMatrix.lean @@ -16,6 +16,8 @@ public import Mathlib.LinearAlgebra.Matrix.Notation The hat map sends a vector `Ο‰ : Fin 3 β†’ ℝ` to the skew-symmetric matrix `[Ο‰]β‚“` characterised by `[Ο‰]β‚“ *α΅₯ v = Ο‰ ⨯₃ v`. It realises the correspondence between `ℝ³` and the skew-symmetric `3 Γ— 3` matrices (the Lie algebra `π–˜π–”(3)`), and underlies the angular velocity of a rigid body. +The vee map only selects matrix entries and is defined for arbitrary coefficient types, +including operator-valued matrices. -/ @@ -43,8 +45,10 @@ lemma crossProductMatrix_transpose (Ο‰ : Fin 3 β†’ ℝ) : ext i j fin_cases i <;> fin_cases j <;> simp [crossProductMatrix] -/-- The vee map: reads the vector off a `3 Γ— 3` matrix. It is a left inverse of the hat map. -/ -def crossProductVee (A : Matrix (Fin 3) (Fin 3) ℝ) : Fin 3 β†’ ℝ := ![A 2 1, A 0 2, A 1 0] +/-- The vee map: reads the vector off a `3 Γ— 3` matrix with arbitrary coefficients. +For real coefficients, it is a left inverse of the hat map. -/ +def crossProductVee {Ξ± : Type*} (A : Matrix (Fin 3) (Fin 3) Ξ±) : Fin 3 β†’ Ξ± := + ![A 2 1, A 0 2, A 1 0] /-- The vee map is a left inverse of the hat map. -/ @[simp] diff --git a/Physlib/QuantumMechanics/Operators/API-map.yaml b/Physlib/QuantumMechanics/Operators/API-map.yaml index bb1570ad2..4820c8ea9 100644 --- a/Physlib/QuantumMechanics/Operators/API-map.yaml +++ b/Physlib/QuantumMechanics/Operators/API-map.yaml @@ -147,11 +147,11 @@ Requirements: - description: "The right-handed Cartesian components in three dimensions act on the invariant Schwartz domain, satisfy the Levi-Civita and cyclic commutation relations, and their three squares sum to angular momentum squared." done: true - location: "Physlib/QuantumMechanics/Operators/AngularMomentum/ThreeDimensional.lean (angularMomentum3DOperator, angularMomentum3DOperator_isSymmetric, angularMomentumOperatorSqr_eq_sum_3D, angularMomentumSqOperator_apply_eq_sum_3D, angularMomentum3D_commutation, angularMomentum3D_commutation_xy, angularMomentum3D_commutation_yz, angularMomentum3D_commutation_zx, angularMomentum3DOperator_commutation, angularMomentumSqOperator_commutation_3D)" + location: "Physlib/QuantumMechanics/Operators/AngularMomentum/DimThree.lean (angularMomentumDimThreeOperator, angularMomentumDimThreeOperator_isSymmetric, angularMomentumOperatorSqr_eq_sum_dimThree, angularMomentumSqOperator_apply_eq_sum_dimThree, angularMomentumDimThree_commutation, angularMomentumDimThree_commutation_xy, angularMomentumDimThree_commutation_yz, angularMomentumDimThree_commutation_zx, angularMomentumDimThreeOperator_commutation, angularMomentumSqOperator_commutation_dimThree)" - description: "Angular momentum ladder operators LΒ± = Lx Β± i Ly are defined on Schwartz maps and lifted to the Hilbert space with invariant dense Schwartz domain, where [Lz, LΒ±] = ±ℏ LΒ± and [LΒ², LΒ±] = 0." done: true - location: "Physlib/QuantumMechanics/Operators/AngularMomentum/ThreeDimensional.lean (angularMomentumRaisingCLM, angularMomentumLoweringCLM, angularMomentumRaisingOperator, angularMomentumLoweringOperator, angularMomentumZ_commutation_raising, angularMomentumZ_commutation_lowering, angularMomentumSqr_commutation_raising, angularMomentumSqr_commutation_lowering, angularMomentumZOperator_commutation_raising, angularMomentumZOperator_commutation_lowering, angularMomentumSqOperator_commutation_raising, angularMomentumSqOperator_commutation_lowering)" + location: "Physlib/QuantumMechanics/Operators/AngularMomentum/DimThree.lean (angularMomentumRaisingCLM, angularMomentumLoweringCLM, angularMomentumRaisingOperator, angularMomentumLoweringOperator, angularMomentumZ_commutation_raising, angularMomentumZ_commutation_lowering, angularMomentumSqr_commutation_raising, angularMomentumSqr_commutation_lowering, angularMomentumZOperator_commutation_raising, angularMomentumZOperator_commutation_lowering, angularMomentumSqOperator_commutation_raising, angularMomentumSqOperator_commutation_lowering)" - description: "The API shall extend angular momentum from its Schwartz domain to self-adjoint operators on the Hilbert space, with their spectra, the eigenvalues ℏ² l (l + 1) of 𝐋² and ℏ m of a chosen component, and the spherical harmonics as the corresponding eigenfunctions." done: false diff --git a/Physlib/QuantumMechanics/Operators/AngularMomentum.lean b/Physlib/QuantumMechanics/Operators/AngularMomentum.lean index 7c7920ece..41acc00ca 100644 --- a/Physlib/QuantumMechanics/Operators/AngularMomentum.lean +++ b/Physlib/QuantumMechanics/Operators/AngularMomentum.lean @@ -6,6 +6,7 @@ Authors: Gregory J. Loges module public import Physlib.QuantumMechanics.Operators.Commutation +public import Physlib.Mathematics.CrossProductMatrix /-! # Angular momentum operator @@ -147,12 +148,10 @@ lemma angularMomentumOperator1D_trivial : 𝐋[1] = 0 := by /-- The angular momentum (pseudo)scalar operator in two dimensions, `𝐋 ≔ 𝐋₀₁`. -/ def angularMomentumOperator2D : 𝓒(Space 2, β„‚) β†’L[β„‚] 𝓒(Space 2, β„‚) := 𝐋 0 1 -/-- The angular momentum (pseudo)vector operator in three dimension, `𝐋ᡒ ≔ Β½ βˆ‘β±Όβ‚– Ξ΅α΅’β±Όβ‚– 𝐋ⱼₖ`. -/ +/-- The angular momentum (pseudo)vector operator in three dimensions, `𝐋ᡒ ≔ Β½ βˆ‘β±Όβ‚– Ξ΅α΅’β±Όβ‚– 𝐋ⱼₖ`. +The transpose matches the convention of `Matrix.crossProductVee`, giving `(𝐋₁₂, 𝐋₂₀, 𝐋₀₁)`. -/ def angularMomentumOperator3D (i : Fin 3) : 𝓒(Space 3, β„‚) β†’L[β„‚] 𝓒(Space 3, β„‚) := - match i with - | 0 => 𝐋 1 2 - | 1 => 𝐋 2 0 - | 2 => 𝐋 0 1 + Matrix.crossProductVee (Matrix.transpose 𝐋[3]) i /-! ## D. Hilbert-space angular momentum operator diff --git a/Physlib/QuantumMechanics/Operators/AngularMomentum/ThreeDimensional.lean b/Physlib/QuantumMechanics/Operators/AngularMomentum/DimThree.lean similarity index 66% rename from Physlib/QuantumMechanics/Operators/AngularMomentum/ThreeDimensional.lean rename to Physlib/QuantumMechanics/Operators/AngularMomentum/DimThree.lean index c1ccb7288..455cafbab 100644 --- a/Physlib/QuantumMechanics/Operators/AngularMomentum/ThreeDimensional.lean +++ b/Physlib/QuantumMechanics/Operators/AngularMomentum/DimThree.lean @@ -23,10 +23,10 @@ on that domain; it is not an equality with the everywhere-defined zero `LinearPM ## ii. Key results -- `angularMomentum3DOperator`: the Hilbert-space Cartesian components. -- `angularMomentumOperatorSqr_eq_sum_3D`: `LΒ² = LxΒ² + LyΒ² + LzΒ²` on Schwartz maps. -- `angularMomentum3DOperator_isSymmetric`: symmetry of each Cartesian component. -- `angularMomentum3D_commutation`: `[Li, Lj] = iℏ βˆ‘k Ξ΅ijk Lk`. +- `angularMomentumDimThreeOperator`: the Hilbert-space Cartesian components. +- `angularMomentumOperatorSqr_eq_sum_dimThree`: `LΒ² = LxΒ² + LyΒ² + LzΒ²` on Schwartz maps. +- `angularMomentumDimThreeOperator_isSymmetric`: symmetry of each Cartesian component. +- `angularMomentumDimThree_commutation`: `[Li, Lj] = iℏ βˆ‘k Ξ΅ijk Lk`. - `angularMomentumRaisingCLM`, `angularMomentumLoweringCLM`: `Lx Β± i Ly` on Schwartz maps. - `angularMomentumRaisingOperator`, `angularMomentumLoweringOperator`: their Hilbert-space lifts. - `angularMomentumZOperator_commutation_raising`, `angularMomentumZOperator_commutation_lowering`: @@ -34,8 +34,9 @@ on that domain; it is not an equality with the everywhere-defined zero `LinearPM - `angularMomentumSqOperator_commutation_raising`, `angularMomentumSqOperator_commutation_lowering`: `[LΒ², LΒ±] = 0` on that domain. -Open the `AngularMomentum` scope for `𝐋x`, `𝐋y`, `𝐋z` on Schwartz maps and -`𝓛x`, `𝓛y`, `𝓛z`, `𝓛²` on the Hilbert space. +Open the `AngularMomentum` scope for `𝐋₃ i` on Schwartz maps and `𝓛₃ i` on the Hilbert space, +where `i : Fin 3` and indices `0`, `1`, `2` correspond to `x`, `y`, `z`. +The notation `𝓛²` denotes the Hilbert-space square. The same scope provides `𝐋⁺`, `𝐋⁻` and `𝓛⁺`, `𝓛⁻` for the ladder operators. ## iii. Table of contents @@ -67,35 +68,27 @@ open scoped InnerProductSpace -/ @[inherit_doc QuantumMechanics.angularMomentumOperator3D] -scoped[AngularMomentum] notation "𝐋x" => QuantumMechanics.angularMomentumOperator3D 0 -@[inherit_doc QuantumMechanics.angularMomentumOperator3D] -scoped[AngularMomentum] notation "𝐋y" => QuantumMechanics.angularMomentumOperator3D 1 -@[inherit_doc QuantumMechanics.angularMomentumOperator3D] -scoped[AngularMomentum] notation "𝐋z" => QuantumMechanics.angularMomentumOperator3D 2 +scoped[AngularMomentum] notation "𝐋₃" => QuantumMechanics.angularMomentumOperator3D /-- The Cartesian Hilbert-space components, ordered as `x, y, z`. -/ -def angularMomentum3DOperator (i : Fin 3) : +def angularMomentumDimThreeOperator (i : Fin 3) : SpaceDHilbertSpace 3 β†’β‚—.[β„‚] SpaceDHilbertSpace 3 where domain := SchwartzSubmodule 3 toFun := (schwartzIncl volume).1 βˆ˜β‚— (angularMomentumOperator3D i).1 βˆ˜β‚— (schwartzEquiv volume).symm.1 -@[inherit_doc QuantumMechanics.angularMomentum3DOperator] -scoped[AngularMomentum] notation "𝓛x" => QuantumMechanics.angularMomentum3DOperator 0 -@[inherit_doc QuantumMechanics.angularMomentum3DOperator] -scoped[AngularMomentum] notation "𝓛y" => QuantumMechanics.angularMomentum3DOperator 1 -@[inherit_doc QuantumMechanics.angularMomentum3DOperator] -scoped[AngularMomentum] notation "𝓛z" => QuantumMechanics.angularMomentum3DOperator 2 +@[inherit_doc QuantumMechanics.angularMomentumDimThreeOperator] +scoped[AngularMomentum] notation "𝓛₃" => QuantumMechanics.angularMomentumDimThreeOperator open scoped AngularMomentum -lemma angularMomentumOperator3D_x : 𝐋x = 𝐋 1 2 := rfl -lemma angularMomentumOperator3D_y : 𝐋y = 𝐋 2 0 := rfl -lemma angularMomentumOperator3D_z : 𝐋z = 𝐋 0 1 := rfl +lemma angularMomentumDimThreeCLM_x : 𝐋₃ 0 = 𝐋 1 2 := rfl +lemma angularMomentumDimThreeCLM_y : 𝐋₃ 1 = 𝐋 2 0 := rfl +lemma angularMomentumDimThreeCLM_z : 𝐋₃ 2 = 𝐋 0 1 := rfl -lemma angularMomentum3DOperator_x : 𝓛x = angularMomentumOperator 1 2 := rfl -lemma angularMomentum3DOperator_y : 𝓛y = angularMomentumOperator 2 0 := rfl -lemma angularMomentum3DOperator_z : 𝓛z = angularMomentumOperator 0 1 := rfl +lemma angularMomentumDimThreeOperator_x : 𝓛₃ 0 = angularMomentumOperator 1 2 := rfl +lemma angularMomentumDimThreeOperator_y : 𝓛₃ 1 = angularMomentumOperator 2 0 := rfl +lemma angularMomentumDimThreeOperator_z : 𝓛₃ 2 = angularMomentumOperator 0 1 := rfl /-! ### A.1. Hilbert-space transport @@ -103,63 +96,60 @@ lemma angularMomentum3DOperator_z : 𝓛z = angularMomentumOperator 0 1 := rfl variable (i : Fin 3) -lemma angularMomentum3DOperator_domain_eq : - (angularMomentum3DOperator i).domain = SchwartzSubmodule 3 := rfl +lemma angularMomentumDimThreeOperator_domain_eq : + (𝓛₃ i).domain = SchwartzSubmodule 3 := rfl -lemma angularMomentum3DOperator_apply (ψ : SchwartzSubmodule 3) : - angularMomentum3DOperator i ψ = - schwartzEquiv volume (angularMomentumOperator3D i ((schwartzEquiv volume).symm ψ)) := rfl +lemma angularMomentumDimThreeOperator_apply (ψ : SchwartzSubmodule 3) : + 𝓛₃ i ψ = schwartzEquiv volume (𝐋₃ i ((schwartzEquiv volume).symm ψ)) := rfl -lemma angularMomentum3DOperator_apply_ae (ψ : SchwartzSubmodule 3) : - angularMomentum3DOperator i ψ =ᡐ[volume] - angularMomentumOperator3D i ((schwartzEquiv volume).symm ψ) := schwartzEquiv_coe_ae _ +lemma angularMomentumDimThreeOperator_apply_ae (ψ : SchwartzSubmodule 3) : + 𝓛₃ i ψ =ᡐ[volume] 𝐋₃ i ((schwartzEquiv volume).symm ψ) := schwartzEquiv_coe_ae _ -lemma angularMomentum3DOperator_range (ψ : SchwartzSubmodule 3) : - angularMomentum3DOperator i ψ ∈ SchwartzSubmodule 3 := by - simp [angularMomentum3DOperator_apply] +lemma angularMomentumDimThreeOperator_range (ψ : SchwartzSubmodule 3) : + 𝓛₃ i ψ ∈ SchwartzSubmodule 3 := by + simp [angularMomentumDimThreeOperator_apply] /-- Composing two components stays on the common Schwartz domain. -/ -lemma angularMomentum3DOperator_apply_apply (j : Fin 3) (ψ : SchwartzSubmodule 3) : - angularMomentum3DOperator i - ⟨angularMomentum3DOperator j ψ, angularMomentum3DOperator_range j ψ⟩ = - schwartzEquiv volume (angularMomentumOperator3D i - (angularMomentumOperator3D j ((schwartzEquiv volume).symm ψ))) := by - change schwartzIncl volume (angularMomentumOperator3D i ((schwartzEquiv volume).symm - (schwartzEquiv volume (angularMomentumOperator3D j ((schwartzEquiv volume).symm ψ))))) = _ +lemma angularMomentumDimThreeOperator_apply_apply (j : Fin 3) (ψ : SchwartzSubmodule 3) : + 𝓛₃ i βŸ¨π“›β‚ƒ j ψ, angularMomentumDimThreeOperator_range j ψ⟩ = + schwartzEquiv volume (𝐋₃ i (𝐋₃ j ((schwartzEquiv volume).symm ψ))) := by + change schwartzIncl volume (𝐋₃ i ((schwartzEquiv volume).symm + (schwartzEquiv volume (𝐋₃ j ((schwartzEquiv volume).symm ψ))))) = _ rw [LinearEquiv.symm_apply_apply] rfl -lemma angularMomentum3DOperator_hasDenseDomain : - (angularMomentum3DOperator i).HasDenseDomain := SchwartzSubmodule.dense 3 _ +lemma angularMomentumDimThreeOperator_hasDenseDomain : + (𝓛₃ i).HasDenseDomain := SchwartzSubmodule.dense 3 _ -lemma angularMomentum3DOperator_isSymmetric : - (angularMomentum3DOperator i).IsSymmetric := by +lemma angularMomentumDimThreeOperator_isSymmetric : + (𝓛₃ i).IsSymmetric := by fin_cases i <;> exact angularMomentumOperator_isSymmetric _ _ -lemma angularMomentum3DOperator_isUnbounded : - (angularMomentum3DOperator i).IsUnbounded := - (angularMomentum3DOperator_isSymmetric i).isUnbounded_iff_hasDenseDomain.mpr - (angularMomentum3DOperator_hasDenseDomain i) +lemma angularMomentumDimThreeOperator_isUnbounded : + (𝓛₃ i).IsUnbounded := + (angularMomentumDimThreeOperator_isSymmetric i).isUnbounded_iff_hasDenseDomain.mpr + (angularMomentumDimThreeOperator_hasDenseDomain i) /-! ### A.2. Sum of the three squares -/ /-- The antisymmetric-index definition agrees with the Cartesian sum of squares. -/ -lemma angularMomentumOperatorSqr_eq_sum_3D : - 𝐋²[3] = βˆ‘ i : Fin 3, angularMomentumOperator3D i ∘L angularMomentumOperator3D i := by - simp only [angularMomentumOperatorSqr, Fin.sum_univ_three, angularMomentumOperator3D, +lemma angularMomentumOperatorSqr_eq_sum_dimThree : + 𝐋²[3] = βˆ‘ i : Fin 3, 𝐋₃ i ∘L 𝐋₃ i := by + simp only [angularMomentumOperatorSqr, Fin.sum_univ_three, + angularMomentumDimThreeCLM_x, angularMomentumDimThreeCLM_y, angularMomentumDimThreeCLM_z, angularMomentumCLM_eq_zero, angularMomentumCLM_antisymm (0 : Fin 3) 2, angularMomentumCLM_antisymm (1 : Fin 3) 0, angularMomentumCLM_antisymm (2 : Fin 3) 1, comp_zero, neg_comp, comp_neg, neg_neg, add_zero, zero_add] module /-- The same Cartesian sum of squares, evaluated on a Hilbert-space Schwartz vector. -/ -lemma angularMomentumSqOperator_apply_eq_sum_3D (ψ : SchwartzSubmodule 3) : - angularMomentumSqOperator ψ = βˆ‘ i : Fin 3, angularMomentum3DOperator i - ⟨angularMomentum3DOperator i ψ, angularMomentum3DOperator_range i ψ⟩ := by - simp [angularMomentumSqOperator_apply, angularMomentumOperatorSqr_eq_sum_3D, - angularMomentum3DOperator_apply_apply] +lemma angularMomentumSqOperator_apply_eq_sum_dimThree (ψ : SchwartzSubmodule 3) : + angularMomentumSqOperator ψ = βˆ‘ i : Fin 3, 𝓛₃ i + βŸ¨π“›β‚ƒ i ψ, angularMomentumDimThreeOperator_range i ψ⟩ := by + simp [angularMomentumSqOperator_apply, angularMomentumOperatorSqr_eq_sum_dimThree, + angularMomentumDimThreeOperator_apply_apply] /-! ## B. Commutation algebra @@ -176,71 +166,71 @@ attribute [local instance 100] LieAlgebra.ofAssociativeAlgebra set_option backward.isDefEq.respectTransparency false in /-- The Cartesian angular momentum algebra, with the right-handed Levi-Civita symbol. -/ -lemma angularMomentum3D_commutation (j : Fin 3) : - ⁅angularMomentumOperator3D i, angularMomentumOperator3D j⁆ = - (I * ℏ) β€’ βˆ‘ k : Fin 3, (leviCivitaSymbol ![i, j, k] : β„‚) β€’ - angularMomentumOperator3D k := by +lemma angularMomentumDimThree_commutation (j : Fin 3) : + ⁅𝐋₃ i, 𝐋₃ j⁆ = + (I * ℏ) β€’ βˆ‘ k : Fin 3, (leviCivitaSymbol ![i, j, k] : β„‚) β€’ 𝐋₃ k := by simp only [leviCivitaSymbol_eq_det, Matrix.det_fin_three] fin_cases i <;> fin_cases j <;> - norm_num [angularMomentumOperator3D, angularMomentum_commutation_angularMomentum, + norm_num [angularMomentumDimThreeCLM_x, angularMomentumDimThreeCLM_y, + angularMomentumDimThreeCLM_z, angularMomentum_commutation_angularMomentum, kroneckerDelta, Fin.sum_univ_three, angularMomentumCLM_eq_zero, angularMomentumCLM_antisymm (0 : Fin 3) 2, angularMomentumCLM_antisymm (1 : Fin 3) 0, angularMomentumCLM_antisymm (2 : Fin 3) 1] /-- `[Lx, Ly] = iℏ Lz`. -/ -lemma angularMomentum3D_commutation_xy : ⁅𝐋x, 𝐋y⁆ = (I * ℏ) β€’ 𝐋z := by - simpa [angularMomentumOperator3D, kroneckerDelta, +lemma angularMomentumDimThree_commutation_xy : ⁅𝐋₃ 0, 𝐋₃ 1⁆ = (I * ℏ) β€’ 𝐋₃ 2 := by + simpa [angularMomentumDimThreeCLM_x, angularMomentumDimThreeCLM_y, + angularMomentumDimThreeCLM_z, kroneckerDelta, angularMomentumCLM_antisymm (1 : Fin 3) 0] using angularMomentum_commutation_angularMomentum (d := 3) 1 2 2 0 /-- `[Ly, Lz] = iℏ Lx`. -/ -lemma angularMomentum3D_commutation_yz : ⁅𝐋y, 𝐋z⁆ = (I * ℏ) β€’ 𝐋x := by - simpa [angularMomentumOperator3D, kroneckerDelta, +lemma angularMomentumDimThree_commutation_yz : ⁅𝐋₃ 1, 𝐋₃ 2⁆ = (I * ℏ) β€’ 𝐋₃ 0 := by + simpa [angularMomentumDimThreeCLM_x, angularMomentumDimThreeCLM_y, + angularMomentumDimThreeCLM_z, kroneckerDelta, angularMomentumCLM_antisymm (2 : Fin 3) 1] using angularMomentum_commutation_angularMomentum (d := 3) 2 0 0 1 /-- `[Lz, Lx] = iℏ Ly`. -/ -lemma angularMomentum3D_commutation_zx : ⁅𝐋z, 𝐋x⁆ = (I * ℏ) β€’ 𝐋y := by - simpa [angularMomentumOperator3D, kroneckerDelta, +lemma angularMomentumDimThree_commutation_zx : ⁅𝐋₃ 2, 𝐋₃ 0⁆ = (I * ℏ) β€’ 𝐋₃ 1 := by + simpa [angularMomentumDimThreeCLM_x, angularMomentumDimThreeCLM_y, + angularMomentumDimThreeCLM_z, kroneckerDelta, angularMomentumCLM_antisymm (0 : Fin 3) 2] using angularMomentum_commutation_angularMomentum (d := 3) 0 1 1 2 /-- Angular momentum squared commutes with every Cartesian component on Schwartz maps. -/ -lemma angularMomentumSqr_commutation_3D : ⁅𝐋²[3], angularMomentumOperator3D i⁆ = 0 := by +lemma angularMomentumSqr_commutation_dimThree : ⁅𝐋²[3], 𝐋₃ i⁆ = 0 := by fin_cases i <;> exact angularMomentumSqr_commutation_angularMomentum _ _ /-- The Cartesian commutation algebra on the common Hilbert-space Schwartz domain. -/ -lemma angularMomentum3DOperator_commutation (j : Fin 3) (ψ : SchwartzSubmodule 3) : - angularMomentum3DOperator i - ⟨angularMomentum3DOperator j ψ, angularMomentum3DOperator_range j ψ⟩ - - angularMomentum3DOperator j - ⟨angularMomentum3DOperator i ψ, angularMomentum3DOperator_range i ψ⟩ = - (I * ℏ) β€’ βˆ‘ k : Fin 3, (leviCivitaSymbol ![i, j, k] : β„‚) β€’ - angularMomentum3DOperator k ψ := by - rw [angularMomentum3DOperator_apply_apply, angularMomentum3DOperator_apply_apply] +lemma angularMomentumDimThreeOperator_commutation (j : Fin 3) (ψ : SchwartzSubmodule 3) : + 𝓛₃ i βŸ¨π“›β‚ƒ j ψ, angularMomentumDimThreeOperator_range j ψ⟩ - + 𝓛₃ j βŸ¨π“›β‚ƒ i ψ, angularMomentumDimThreeOperator_range i ψ⟩ = + (I * ℏ) β€’ βˆ‘ k : Fin 3, (leviCivitaSymbol ![i, j, k] : β„‚) β€’ 𝓛₃ k ψ := by + rw [angularMomentumDimThreeOperator_apply_apply, angularMomentumDimThreeOperator_apply_apply] have h := congrArg (fun A : 𝓒(Space 3, β„‚) β†’L[β„‚] 𝓒(Space 3, β„‚) => schwartzIncl volume (A ((schwartzEquiv volume).symm ψ))) - (angularMomentum3D_commutation i j) + (angularMomentumDimThree_commutation i j) simpa only [Ring.lie_def, ContinuousLinearMap.mul_def, sub_apply, comp_apply, smul_apply, _root_.sum_apply, map_sub, map_smul, map_sum, - angularMomentum3DOperator_apply, schwartzEquiv_apply_coe] using h + angularMomentumDimThreeOperator_apply, schwartzEquiv_apply_coe] using h /-- `[LΒ², Li] = 0` on the common invariant Hilbert-space domain. -/ -lemma angularMomentumSqOperator_commutation_3D (ψ : SchwartzSubmodule 3) : +lemma angularMomentumSqOperator_commutation_dimThree (ψ : SchwartzSubmodule 3) : angularMomentumSqOperator - ⟨angularMomentum3DOperator i ψ, angularMomentum3DOperator_range i ψ⟩ - - angularMomentum3DOperator i + βŸ¨π“›β‚ƒ i ψ, angularMomentumDimThreeOperator_range i ψ⟩ - + 𝓛₃ i ⟨angularMomentumSqOperator ψ, angularMomentumSqOperator_range ψ⟩ = 0 := by change schwartzIncl volume (𝐋² ((schwartzEquiv volume).symm - (schwartzEquiv volume (angularMomentumOperator3D i ((schwartzEquiv volume).symm ψ))))) - - schwartzIncl volume (angularMomentumOperator3D i ((schwartzEquiv volume).symm + (schwartzEquiv volume (𝐋₃ i ((schwartzEquiv volume).symm ψ))))) - + schwartzIncl volume (𝐋₃ i ((schwartzEquiv volume).symm (schwartzEquiv volume (𝐋² ((schwartzEquiv volume).symm ψ))))) = 0 simp only [LinearEquiv.symm_apply_apply] have h := congrArg (fun A : 𝓒(Space 3, β„‚) β†’L[β„‚] 𝓒(Space 3, β„‚) => schwartzIncl volume (A ((schwartzEquiv volume).symm ψ))) - (angularMomentumSqr_commutation_3D i) + (angularMomentumSqr_commutation_dimThree i) simpa only [Ring.lie_def, ContinuousLinearMap.mul_def, sub_apply, comp_apply, zero_apply, map_sub, map_zero] using h @@ -252,10 +242,10 @@ are used in their commutation relations. -/ /-- The angular momentum raising operator `Lβ‚Š = Lx + i Ly` on Schwartz maps. -/ -def angularMomentumRaisingCLM : 𝓒(Space 3, β„‚) β†’L[β„‚] 𝓒(Space 3, β„‚) := 𝐋x + I β€’ 𝐋y +def angularMomentumRaisingCLM : 𝓒(Space 3, β„‚) β†’L[β„‚] 𝓒(Space 3, β„‚) := 𝐋₃ 0 + I β€’ 𝐋₃ 1 /-- The angular momentum lowering operator `Lβ‚‹ = Lx - i Ly` on Schwartz maps. -/ -def angularMomentumLoweringCLM : 𝓒(Space 3, β„‚) β†’L[β„‚] 𝓒(Space 3, β„‚) := 𝐋x - I β€’ 𝐋y +def angularMomentumLoweringCLM : 𝓒(Space 3, β„‚) β†’L[β„‚] 𝓒(Space 3, β„‚) := 𝐋₃ 0 - I β€’ 𝐋₃ 1 @[inherit_doc QuantumMechanics.angularMomentumRaisingCLM] scoped[AngularMomentum] notation "𝐋⁺" => QuantumMechanics.angularMomentumRaisingCLM @@ -263,26 +253,26 @@ scoped[AngularMomentum] notation "𝐋⁺" => QuantumMechanics.angularMomentumRa scoped[AngularMomentum] notation "𝐋⁻" => QuantumMechanics.angularMomentumLoweringCLM /-- `[Lz, Lβ‚Š] = ℏ Lβ‚Š`. -/ -lemma angularMomentumZ_commutation_raising : ⁅𝐋z, 𝐋⁺⁆ = (ℏ : β„‚) β€’ 𝐋⁺ := by - rw [angularMomentumRaisingCLM, lie_add, lie_smul, angularMomentum3D_commutation_zx, - ← lie_skew 𝐋z 𝐋y, angularMomentum3D_commutation_yz] +lemma angularMomentumZ_commutation_raising : ⁅𝐋₃ 2, 𝐋⁺⁆ = (ℏ : β„‚) β€’ 𝐋⁺ := by + rw [angularMomentumRaisingCLM, lie_add, lie_smul, angularMomentumDimThree_commutation_zx, + ← lie_skew (𝐋₃ 2) (𝐋₃ 1), angularMomentumDimThree_commutation_yz] simp only [smul_neg, smul_smul, ← mul_assoc, I_mul_I, neg_one_mul] module /-- `[Lz, Lβ‚‹] = -ℏ Lβ‚‹`. -/ -lemma angularMomentumZ_commutation_lowering : ⁅𝐋z, 𝐋⁻⁆ = -(ℏ : β„‚) β€’ 𝐋⁻ := by - rw [angularMomentumLoweringCLM, lie_sub, lie_smul, angularMomentum3D_commutation_zx, - ← lie_skew 𝐋z 𝐋y, angularMomentum3D_commutation_yz] +lemma angularMomentumZ_commutation_lowering : ⁅𝐋₃ 2, 𝐋⁻⁆ = -(ℏ : β„‚) β€’ 𝐋⁻ := by + rw [angularMomentumLoweringCLM, lie_sub, lie_smul, angularMomentumDimThree_commutation_zx, + ← lie_skew (𝐋₃ 2) (𝐋₃ 1), angularMomentumDimThree_commutation_yz] simp only [smul_neg, smul_smul, ← mul_assoc, I_mul_I, neg_one_mul] module /-- Angular momentum squared commutes with the raising operator. -/ lemma angularMomentumSqr_commutation_raising : ⁅𝐋²[3], 𝐋⁺⁆ = 0 := by - simp [angularMomentumRaisingCLM, lie_add, lie_smul, angularMomentumSqr_commutation_3D] + simp [angularMomentumRaisingCLM, lie_add, lie_smul, angularMomentumSqr_commutation_dimThree] /-- Angular momentum squared commutes with the lowering operator. -/ lemma angularMomentumSqr_commutation_lowering : ⁅𝐋²[3], 𝐋⁻⁆ = 0 := by - simp [angularMomentumLoweringCLM, lie_sub, lie_smul, angularMomentumSqr_commutation_3D] + simp [angularMomentumLoweringCLM, lie_sub, lie_smul, angularMomentumSqr_commutation_dimThree] /-! ### C.1. Hilbert-space ladder operators @@ -313,14 +303,14 @@ lemma angularMomentumLoweringOperator_apply (ψ : SchwartzSubmodule 3) : 𝓛⁻ ψ = schwartzEquiv volume (𝐋⁻ ((schwartzEquiv volume).symm ψ)) := rfl lemma angularMomentumRaisingOperator_apply_eq (ψ : SchwartzSubmodule 3) : - 𝓛⁺ ψ = 𝓛x ψ + I β€’ 𝓛y ψ := by + 𝓛⁺ ψ = 𝓛₃ 0 ψ + I β€’ 𝓛₃ 1 ψ := by simp [angularMomentumRaisingOperator_apply, angularMomentumRaisingCLM, - angularMomentum3DOperator_apply] + angularMomentumDimThreeOperator_apply] lemma angularMomentumLoweringOperator_apply_eq (ψ : SchwartzSubmodule 3) : - 𝓛⁻ ψ = 𝓛x ψ - I β€’ 𝓛y ψ := by + 𝓛⁻ ψ = 𝓛₃ 0 ψ - I β€’ 𝓛₃ 1 ψ := by simp [angularMomentumLoweringOperator_apply, angularMomentumLoweringCLM, - angularMomentum3DOperator_apply] + angularMomentumDimThreeOperator_apply] lemma angularMomentumRaisingOperator_apply_ae (ψ : SchwartzSubmodule 3) : 𝓛⁺ ψ =ᡐ[volume] 𝐋⁺ ((schwartzEquiv volume).symm ψ) := schwartzEquiv_coe_ae _ @@ -348,12 +338,12 @@ lemma angularMomentumLoweringOperator_hasDenseDomain : (𝓛⁻).HasDenseDomain /-- `[Lz, Lβ‚Š] ψ = ℏ Lβ‚Š ψ` for every Schwartz vector in the Hilbert space. -/ lemma angularMomentumZOperator_commutation_raising (ψ : SchwartzSubmodule 3) : - 𝓛z βŸ¨π“›βΊ ψ, angularMomentumRaisingOperator_range ψ⟩ - - 𝓛⁺ βŸ¨π“›z ψ, angularMomentum3DOperator_range 2 ψ⟩ = (ℏ : β„‚) β€’ 𝓛⁺ ψ := by - change schwartzIncl volume (𝐋z ((schwartzEquiv volume).symm + 𝓛₃ 2 βŸ¨π“›βΊ ψ, angularMomentumRaisingOperator_range ψ⟩ - + 𝓛⁺ βŸ¨π“›β‚ƒ 2 ψ, angularMomentumDimThreeOperator_range 2 ψ⟩ = (ℏ : β„‚) β€’ 𝓛⁺ ψ := by + change schwartzIncl volume (𝐋₃ 2 ((schwartzEquiv volume).symm (schwartzEquiv volume (𝐋⁺ ((schwartzEquiv volume).symm ψ))))) - schwartzIncl volume (𝐋⁺ ((schwartzEquiv volume).symm - (schwartzEquiv volume (𝐋z ((schwartzEquiv volume).symm ψ))))) = + (schwartzEquiv volume (𝐋₃ 2 ((schwartzEquiv volume).symm ψ))))) = (ℏ : β„‚) β€’ schwartzIncl volume (𝐋⁺ ((schwartzEquiv volume).symm ψ)) simp only [LinearEquiv.symm_apply_apply] have h := congrArg @@ -365,12 +355,12 @@ lemma angularMomentumZOperator_commutation_raising (ψ : SchwartzSubmodule 3) : /-- `[Lz, Lβ‚‹] ψ = -ℏ Lβ‚‹ ψ` for every Schwartz vector in the Hilbert space. -/ lemma angularMomentumZOperator_commutation_lowering (ψ : SchwartzSubmodule 3) : - 𝓛z βŸ¨π“›β» ψ, angularMomentumLoweringOperator_range ψ⟩ - - 𝓛⁻ βŸ¨π“›z ψ, angularMomentum3DOperator_range 2 ψ⟩ = -(ℏ : β„‚) β€’ 𝓛⁻ ψ := by - change schwartzIncl volume (𝐋z ((schwartzEquiv volume).symm + 𝓛₃ 2 βŸ¨π“›β» ψ, angularMomentumLoweringOperator_range ψ⟩ - + 𝓛⁻ βŸ¨π“›β‚ƒ 2 ψ, angularMomentumDimThreeOperator_range 2 ψ⟩ = -(ℏ : β„‚) β€’ 𝓛⁻ ψ := by + change schwartzIncl volume (𝐋₃ 2 ((schwartzEquiv volume).symm (schwartzEquiv volume (𝐋⁻ ((schwartzEquiv volume).symm ψ))))) - schwartzIncl volume (𝐋⁻ ((schwartzEquiv volume).symm - (schwartzEquiv volume (𝐋z ((schwartzEquiv volume).symm ψ))))) = + (schwartzEquiv volume (𝐋₃ 2 ((schwartzEquiv volume).symm ψ))))) = -(ℏ : β„‚) β€’ schwartzIncl volume (𝐋⁻ ((schwartzEquiv volume).symm ψ)) simp only [LinearEquiv.symm_apply_apply] have h := congrArg