Momentum

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

Statistics

Metric	Count
Definitions momentumOperator, momentumOperatorSqr, «term𝐩[_]», «term𝐩²»	4
Theorems momentumOperatorSqr_apply, momentumOperator_apply, momentumOperator_apply_fun	3
Total	7

QuantumMechanics

Definitions

Name	Category	Theorems
momentumOperator 📖	CompOp	10 math math: momentum_momentum_eq, momentum_commutation_momentum, angularMomentumOperator_apply_fun, momentumSqr_commutation_momentum, position_commutation_momentum, momentumOperatorSqr_apply, momentumOperator_apply, momentumOperator_apply_fun, angularMomentumOperator_apply, angularMomentum_commutation_momentum
momentumOperatorSqr 📖	CompOp	2 math math: momentumSqr_commutation_momentum, momentumOperatorSqr_apply
«term𝐩[_]» 📖	CompOp	—
«term𝐩²» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
momentumOperatorSqr_apply 📖	mathematical	—	Space Space.instNormedAddCommGroup Space.instInnerProductSpaceReal momentumOperatorSqr momentumOperator	—	—
momentumOperator_apply 📖	mathematical	—	Space Space.instNormedAddCommGroup Space.instInnerProductSpaceReal momentumOperator Constants.ℏ Space.deriv	—	—
momentumOperator_apply_fun 📖	mathematical	—	Space Space.instNormedAddCommGroup Space.instInnerProductSpaceReal momentumOperator Constants.ℏ Space.deriv	—	—

---

← Back to Index