Documentation Verification Report

Momentum

📁 Source: PhysLean/QuantumMechanics/OneDimension/Operators/Momentum.lean

Statistics

Metric	Count
Definitions `momentumOperator`, `momentumOperatorSchwartz`, `momentumOperatorUnbounded`	3
Theorems `continuous_momentumOperator`, `momentumOperatorSchwartz_apply`, `momentumOperatorUnbounded_isSelfAdjoint`, `momentumOperator_add`, `momentumOperator_eq_smul`, `momentumOperator_smul`, `planeWaveFunctional_generalized_eigenvector_momentumOperatorUnbounded`	7
Total	10

QuantumMechanics.OneDimension

Definitions

Name	Category	Theorems
`momentumOperator` 📖	CompOp	5 math math: `momentumOperator_smul`, `momentumOperator_eq_smul`, `momentumOperator_linear`, `continuous_momentumOperator`, `momentumOperator_add`
`momentumOperatorSchwartz` 📖	CompOp	4 math math: `positionOperatorSchwartz_momentumOperatorSchwartz_eq`, `momentumOperatorSchwartz_positionOperatorSchwartz_eq`, `momentumOperatorSchwartz_apply`, `positionOperatorSchwartz_commutation_momentumOperatorSchwartz`
`momentumOperatorUnbounded` 📖	CompOp	2 math math: `momentumOperatorUnbounded_isSelfAdjoint`, `planeWaveFunctional_generalized_eigenvector_momentumOperatorUnbounded`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuous_momentumOperator` 📖	mathematical	—	`momentumOperator`	—	`momentumOperator_eq_smul`
`momentumOperatorSchwartz_apply` 📖	mathematical	—	`momentumOperatorSchwartz` `Constants.ℏ`	—	`momentumOperatorSchwartz.eq_1`
`momentumOperatorUnbounded_isSelfAdjoint` 📖	mathematical	—	`UnboundedOperator.IsSelfAdjoint` `HilbertSpace.schwartzIncl` `HilbertSpace.schwartzIncl_injective` `momentumOperatorUnbounded`	—	`HilbertSpace.schwartzIncl_inner` `momentumOperatorSchwartz_apply`
`momentumOperator_add` 📖	mathematical	—	`momentumOperator`	—	`momentumOperator_eq_smul`
`momentumOperator_eq_smul` 📖	mathematical	—	`momentumOperator` `Constants.ℏ`	—	—
`momentumOperator_smul` 📖	mathematical	—	`momentumOperator`	—	`momentumOperator_eq_smul`
`planeWaveFunctional_generalized_eigenvector_momentumOperatorUnbounded` 📖	mathematical	—	`UnboundedOperator.IsGeneralizedEigenvector` `HilbertSpace.schwartzIncl` `HilbertSpace.schwartzIncl_injective` `momentumOperatorUnbounded` `HilbertSpace.planewaveFunctional` `Constants.ℏ`	—	`HilbertSpace.schwartzIncl_injective` `UnboundedOperator.isGeneralizedEigenvector_ofSelfCLM_iff`

---

← Back to Index