feat(QuantumMechanics): number Hamiltonian of the harmonic oscillator, adjointness of the ladder operators - #1645
Conversation
…scillator, commutation relations Defines the lowering, raising and number operators of the d-dimensional quantum harmonic oscillator on Schwartz maps and proves their commutation relations from the canonical commutation relations: [a_i, a_j^dag] = delta_ij, [a_i, a_j] = 0, [N_i, N_j] = 0, [N_i, a_j] = -delta_ij a_j, [N_i, a_j^dag] = delta_ij a_j^dag, a_i a_i^dag = N_i + 1, and the position and momentum operators in terms of the ladder operators. Fills the first six TODO items of LadderOperators.lean; the adjointness, symmetry and Hamiltonian items remain. Co-authored-by: Claude Fable 5.1 <noreply@anthropic.com>
…, adjointness of the ladder operators Lifts the ladder and number operators to unbounded operators with the Schwartz submodule as domain, proves that the raising operator is the formal adjoint of the lowering operator and that the number operators are symmetric. Defines the Hamiltonian H_N = sum_i hbar omega_i (N_i + 1/2), proves its commutation relations with the ladder and number operators, shows that on Schwartz maps it is the kinetic-plus-potential Hamiltonian of Basic.lean, and that as unbounded operators numberHamiltonian <= hamiltonian; H_N is symmetric. Small lemmas placed next to their objects: potentialFunction_apply and its temperate growth (Basic.lean), the pointwise canonical commutation relation and id_commutation (Commutation.lean), positionCLM_inner and momentumCLM_inner. Co-authored-by: Claude Fable 5.1 <noreply@anthropic.com>
|
Thank you for this pull-request (PR). If this is your first PR, welcome to the community! Below is what will happen next. Please read carefully if you are not familiar with the process. You may open other PRs while this one is being reviewed, and can stack PRs on top of each other, so don't let these steps slow you down.
Tip: The easiest way to get have a fast review is to submit a PR that is small and self-contained, and has clear documentation explaining why things are the way they are in your chages. If you have any problems or questions, please reach out to the community on the Zulip. |
- one `namespace QuantumMechanics.HarmonicOscillator`; - `lowering`, `raising`, `number` renamed `loweringCLM`, `raisingCLM`, `numberCLM` (operators on Schwartz maps, like `positionCLM` and `momentumCLM`); - `ξ_ofReal_ne_zero` moved to `HarmonicOscillator/Basic.lean`, `ℏ_ofReal_ne_zero` to `PlanckConstant.lean`; - the `I ^ 2 = -1` and `√2 ^ 2 = 2` rewrites precede `field_simp` (after `ring_nf`). Co-authored-by: Claude Fable 5.1 <noreply@anthropic.com>
…y morrison-daniel: CLM names, moved lemmas, rewrites before field_simp)
| -/ | ||
|
|
||
| /-- The Hamiltonian in terms of the number operators, `H_N = ∑ᵢ ℏ ωᵢ (Nᵢ + ½)`, on Schwartz maps. -/ | ||
| def numberHamiltonianCLM : 𝓢(Space d, ℂ) →L[ℂ] 𝓢(Space d, ℂ) := |
There was a problem hiding this comment.
I would make this a lemma rather then a separate definition if possible
There was a problem hiding this comment.
Done in the last two commits: numberHamiltonianCLM and numberHamiltonian are gone. The Hamiltonian of Basic.lean is used directly: hamiltonian_apply_schwartz says that on a Schwartz map it acts as ∑ᵢ ℏ ωᵢ (Nᵢ + ½) (with schwartzSubmodule_le_hamiltonian_domain for the domain), and hamiltonian_inner_schwartz gives its symmetry on the Schwartz submodule. The commutation relations are stated for the sum ∑ᵢ ℏ ωᵢ (Nᵢ + ½) written out (sum_number_commutation_lowering, _raising, _number), and sum_number_apply is the pointwise identity = (1/2m) ∑ᵢ pᵢ (pᵢ ψ) + V ψ. This is my reading of "if possible"; if you would rather keep a named abbreviation for the sum, say so and I will adjust. #1646 is updated accordingly (sum_number_eigenfunction, and hamiltonian_eigenstate now goes through hamiltonian_apply_schwartz).
| -/ | ||
|
|
||
| /-- The number operator as an unbounded operator with domain the Schwartz submodule. -/ | ||
| def numberOperator : Q.HS →ₗ.[ℂ] Q.HS where |
There was a problem hiding this comment.
Would maybe give this its own file
There was a problem hiding this comment.
Done: numberOperator, numberOperator_apply, numberOperator_isSymmetric and the TODO now live in HarmonicOscillator/NumberOperator.lean (registered in Physlib.lean). numberCLM_inner stays in LadderOperators.lean, next to loweringCLM_inner and raisingCLM_inner which it is built from.
| - 2 * ((Q.ω i : ℝ) : ℂ) * ((Q.ξ i : ℝ) : ℂ) ^ 4 * 𝐩 i (𝐩 i ψ) x * ((Q.m : ℝ) : ℂ)) * I_sq | ||
|
|
||
| /-- The kinetic operator on a Schwartz map, `(1/2m) ∑ᵢ pᵢ (pᵢ f)`. -/ | ||
| lemma kineticOperator_apply_schwartz (f : 𝓢(Space d, ℂ)) |
There was a problem hiding this comment.
Move next to the definition of kineticOperator
There was a problem hiding this comment.
Done: moved to Basic.lean, right after the definition of kineticOperator.
| exact key _ | ||
|
|
||
| /-- The potential operator on a Schwartz map, almost everywhere `V f`. -/ | ||
| lemma potentialOperator_apply_schwartz (f : 𝓢(Space d, ℂ)) |
There was a problem hiding this comment.
move next to the definition of potentialOperator
There was a problem hiding this comment.
Done: moved to Basic.lean, right after the definition of potentialOperator.
|
awaiting-author |
github-actions
Bot
added
the
awaiting-author
… number Hamiltonian - move kineticOperator_apply_schwartz and potentialOperator_apply_schwartz next to the definitions of kineticOperator and potentialOperator in Basic.lean; - move the number operators as unbounded operators to NumberOperator.lean; - replace the definitions numberHamiltonianCLM and numberHamiltonian by lemmas about the Hamiltonian of Basic.lean: hamiltonian_apply_schwartz (it acts on Schwartz maps as sum_i hbar omega_i (N_i + 1/2)), schwartzSubmodule_le_hamiltonian_domain and hamiltonian_inner_schwartz; the commutation relations are stated for this sum.
…_schwartz Follows the review of leanprover-community#1645: the Hamiltonian of Basic.lean is used directly, sum_number_eigenfunction replaces numberHamiltonianCLM_eigenfunction.
|
Thanks for the review. The four points are applied (inline replies give the details):
#1646 is updated on top ( -awaiting-author |
github-actions
Bot
removed
the
awaiting-author
| @@ -201,8 +268,6 @@ def numberCLM : 𝓢(Space d, ℂ) →L[ℂ] 𝓢(Space d, ℂ) := Q.raisingCLM | |||
|
|
|||
| lemma numberCLM_eq : Q.numberCLM i = Q.raisingCLM i ∘L Q.loweringCLM i := rfl | |||
There was a problem hiding this comment.
Would likewise move numberCLM to the NumberOperator file.
There was a problem hiding this comment.
Done in 87f03321: the number operators and the Hamiltonian written through them now live in
NumberOperator.lean, so LadderOperators.lean is exactly the ladder operators.
Moved, in order: numberCLM, numberCLM_eq, number_commutation_lowering,
number_commutation_raising, number_commutation_number, lowering_comp_raising,
numberCLM_inner, then sum_number_commutation_lowering, sum_number_commutation_raising,
sum_number_commutation_number, sum_number_apply, schwartzSubmodule_le_hamiltonian_domain,
hamiltonian_apply_schwartz and hamiltonian_inner_schwartz. LadderOperators.lean
goes from 455 to 237 lines and NumberOperator.lean from 76 to 302; the sections of both files
are renumbered and the ## i. Overview, ## ii. Key results and ## iii. Table of contents
blocks rewritten on both sides.
No statement and no proof changed. The one thing the move needed is that
attribute [local instance 100] LieRing.ofAssociativeRing
attribute [local instance 100] LieAlgebra.ofAssociativeAlgebraare file-local and do not cross the module boundary, so they are repeated in
NumberOperator.lean (without them the commutator proofs fail with "simp made no progress").
lake build Physlib is clean.
One consequence for the stack: Eigenstates.lean in #1646 uses eight of the moved names, so its
public import ... HarmonicOscillator.LadderOperators becomes
public import ... HarmonicOscillator.NumberOperator (which imports LadderOperators). I will
do that when rebasing #1646 on this branch.
|
One more comment above; otherwise looks good. awaiting-author |
github-actions
Bot
added
the
awaiting-author
…nian to NumberOperator.lean Review by jstoobysmith on leanprover-community#1645: move numberCLM to the NumberOperator file. Sections B (number operators) and C (Hamiltonian on Schwartz maps) of LadderOperators.lean move to NumberOperator.lean, which already imported it; the local Lie-ring instances are repeated there. Module docstrings updated on both sides. No statement or proof changed.
|
-awaiting-author |
github-actions
Bot
removed
the
awaiting-author
One line of the module docstring rewritten in the move reached 101 characters (lint-style ERR_LIN). Paragraph rewrapped, no content change. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
jstoobysmith
left a comment
jstoobysmith
left a comment
There was a problem hiding this comment.
Many thanks for iterating on the reviews. This looks good to me. I will merge shortly.
jstoobysmith
added
the
ready-to-merge
3 participants
AI disclosure
AI disclosure. This PR was generated with Claude Fable 5.1 (Claude Code) under my
supervision, following
AI-POLICY.mdandAGENTS.md. I have read every definition and lemmastatement and vouch that they state what the docstrings say. The statements were fixed before
the proofs were written and the operator identities were checked symbolically (sympy, in the
Schrodinger representation) beforehand.
Was stacked on #1644 (
oscillator-ladder-1, now merged); master is merged in.Fills the remaining TODO items of
LadderOperators.leanexcept the last one (same quantum system,which needs essential self-adjointness; left as a TODO together with the essential self-adjointness of
the number operators). No new Hamiltonian is defined: the lemmas are about the Hamiltonian
kineticOperator + potentialOperatorofBasic.lean.LadderOperators.lean, in namespaceQuantumMechanics.HarmonicOscillator:loweringOperator,raisingOperator(unbounded operators with the Schwartz submodule asdomain, modelled on
momentumOperator),loweringCLM_inner,raisingCLM_inner,loweringOperator_isFormalAdjoint_raisingOperator:aᵢ†is the formal adjoint ofaᵢ.numberCLM_inner:⟪Nᵢ f, g⟫ = ⟪f, Nᵢ g⟫for Schwartz maps.sum_number_commutation_lowering,_raising,_number: withH_N = ∑ᵢ ℏ ωᵢ (Nᵢ + ½)written out,
[H_N, aᵢ] = -ℏ ωᵢ aᵢ,[H_N, aᵢ†] = ℏ ωᵢ aᵢ†,[H_N, Nᵢ] = 0.sum_number_apply:H_N ψ = (1/2m) ∑ᵢ pᵢ (pᵢ ψ) + V ψpointwise on Schwartz maps (thecanonical commutation relation and
ξᵢ² m ωᵢ = ℏdo the work);schwartzSubmodule_le_hamiltonian_domain(by temperate growth of the potential);
hamiltonian_apply_schwartz: on a Schwartz map the Hamiltonianof
Basic.leanacts asH_N(almost-everywhere identification of the potential operator);hamiltonian_inner_schwartz: the Hamiltonian is symmetric on the Schwartz submodule.HarmonicOscillator/NumberOperator.lean(new file):numberOperator(unbounded operator with theSchwartz submodule as domain),
numberOperator_apply,numberOperator_isSymmetric.Small lemmas placed next to the objects they are about:
HarmonicOscillator/Basic.lean:ξ_sq_mul_ofReal,potentialFunction_apply(
V(x) = ∑ᵢ ½ m ωᵢ² xᵢ²),potentialFunction_hasTemperateGrowth;kineticOperator_apply_schwartzand
potentialOperator_apply_schwartz, right after the definitions of the two operators.Operators/Commutation.lean:id_commutation,position_commutation_momentum_apply(thecanonical commutation relation pointwise).
Operators/Position.lean,Operators/Momentum.lean:positionCLM_inner,momentumCLM_inner(symmetry of
xᵢandpᵢon Schwartz maps, in terms of the continuous linear maps).Reviewer map:
loweringCLM_inner(the adjointness computation),sum_number_apply(the identityH_N = K + V), thenhamiltonian_apply_schwartz(domain inclusion and the almost-everywhereidentification of the potential operator).
Update (Sept 16). Review of Sept 15 applied: the two
_apply_schwartzlemmas moved next to theirdefinitions, the number operators as unbounded operators moved to their own file, and the separate
definitions
numberHamiltonianCLM/numberHamiltonianreplaced by lemmas about the existingHamiltonian.
🤖 Generated with Claude Code