Commutation

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

Statistics

Metric	Count
Definitions	0
Theorems angularMomentumSqr_commutation_angularMomentum, angularMomentumSqr_commutation_momentumSqr, angularMomentumSqr_commutation_radiusRegPow, angularMomentum_commutation_angularMomentum, angularMomentum_commutation_momentum, angularMomentum_commutation_momentumSqr, angularMomentum_commutation_position, angularMomentum_commutation_radiusRegPow, comp_eq_comp_add_commute, comp_eq_comp_sub_commute, leibniz_lie, lie_leibniz, momentumSqr_commutation_momentum, momentumSqr_comp_angularMomentum_commute, momentumSqr_comp_momentum_commute, momentum_commutation_momentum, momentum_comp_angularMomentum_eq, momentum_comp_commute, momentum_comp_position_eq, momentum_comp_radiusRegPow_eq, position_commutation_momentum, position_commutation_momentumSqr, position_commutation_momentum_momentum, position_commutation_position, position_commutation_radiusRegPow, position_comp_commute, position_comp_radiusRegPow_commute, position_position_commutation_momentum, radiusRegPow_commutation_momentum, radiusRegPow_commutation_momentumSqr, radiusRegPow_commutation_radiusRegPow	31
Total	31

QuantumMechanics

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
angularMomentumSqr_commutation_angularMomentum 📖	mathematical	—	Space Space.instNormedAddCommGroup Space.instInnerProductSpaceReal angularMomentumOperatorSqr angularMomentumOperator	—	leibniz_lie angularMomentum_commutation_angularMomentum
angularMomentumSqr_commutation_momentumSqr 📖	mathematical	—	Space Space.instNormedAddCommGroup Space.instInnerProductSpaceReal angularMomentumOperatorSqr momentumOperatorSqr	—	leibniz_lie angularMomentum_commutation_momentumSqr
angularMomentumSqr_commutation_radiusRegPow 📖	mathematical	—	Space Space.instNormedAddCommGroup Space.instInnerProductSpaceReal angularMomentumOperatorSqr radiusRegPowOperator	—	leibniz_lie angularMomentum_commutation_radiusRegPow
angularMomentum_commutation_angularMomentum 📖	mathematical	—	Space Space.instNormedAddCommGroup Space.instInnerProductSpaceReal angularMomentumOperator Constants.ℏ KroneckerDelta.kroneckerDelta	—	angularMomentumOperator.eq_1 lie_leibniz angularMomentum_commutation_momentum angularMomentum_commutation_position
angularMomentum_commutation_momentum 📖	mathematical	—	Space Space.instNormedAddCommGroup Space.instInnerProductSpaceReal angularMomentumOperator momentumOperator Constants.ℏ KroneckerDelta.kroneckerDelta	—	leibniz_lie momentum_commutation_momentum position_commutation_momentum
angularMomentum_commutation_momentumSqr 📖	mathematical	—	Space Space.instNormedAddCommGroup Space.instInnerProductSpaceReal angularMomentumOperator momentumOperatorSqr	—	lie_leibniz angularMomentum_commutation_momentum KroneckerDelta.sum_smul
angularMomentum_commutation_position 📖	mathematical	—	Space Space.instNormedAddCommGroup Space.instInnerProductSpaceReal angularMomentumOperator positionOperator Constants.ℏ KroneckerDelta.kroneckerDelta	—	leibniz_lie position_commutation_position position_commutation_momentum KroneckerDelta.symm
angularMomentum_commutation_radiusRegPow 📖	mathematical	—	Space Space.instNormedAddCommGroup Space.instInnerProductSpaceReal angularMomentumOperator radiusRegPowOperator	—	leibniz_lie position_commutation_radiusRegPow radiusRegPow_commutation_momentum position_comp_commute
comp_eq_comp_add_commute 📖	mathematical	—	Space Space.instNormedAddCommGroup Space.instInnerProductSpaceReal	—	—
comp_eq_comp_sub_commute 📖	mathematical	—	Space Space.instNormedAddCommGroup Space.instInnerProductSpaceReal	—	—
leibniz_lie 📖	mathematical	—	Space Space.instNormedAddCommGroup Space.instInnerProductSpaceReal	—	—
lie_leibniz 📖	mathematical	—	Space Space.instNormedAddCommGroup Space.instInnerProductSpaceReal	—	—
momentumSqr_commutation_momentum 📖	mathematical	—	Space Space.instNormedAddCommGroup Space.instInnerProductSpaceReal momentumOperatorSqr momentumOperator	—	leibniz_lie momentum_commutation_momentum
momentumSqr_comp_angularMomentum_commute 📖	mathematical	—	Space Space.instNormedAddCommGroup Space.instInnerProductSpaceReal momentumOperatorSqr angularMomentumOperator	—	comp_eq_comp_sub_commute angularMomentum_commutation_momentumSqr
momentumSqr_comp_momentum_commute 📖	mathematical	—	Space Space.instNormedAddCommGroup Space.instInnerProductSpaceReal momentumOperatorSqr momentumOperator	—	comp_eq_comp_add_commute momentumSqr_commutation_momentum
momentum_commutation_momentum 📖	mathematical	—	Space Space.instNormedAddCommGroup Space.instInnerProductSpaceReal momentumOperator	—	Space.deriv_differentiable Space.deriv_const_smul Space.deriv_commute
momentum_comp_angularMomentum_eq 📖	mathematical	—	Space Space.instNormedAddCommGroup Space.instInnerProductSpaceReal momentumOperator angularMomentumOperator Constants.ℏ KroneckerDelta.kroneckerDelta	—	comp_eq_comp_sub_commute angularMomentum_commutation_momentum
momentum_comp_commute 📖	mathematical	—	Space Space.instNormedAddCommGroup Space.instInnerProductSpaceReal momentumOperator	—	comp_eq_comp_add_commute momentum_commutation_momentum
momentum_comp_position_eq 📖	mathematical	—	Space Space.instNormedAddCommGroup Space.instInnerProductSpaceReal momentumOperator positionOperator Constants.ℏ KroneckerDelta.kroneckerDelta	—	comp_eq_comp_sub_commute position_commutation_momentum
momentum_comp_radiusRegPow_eq 📖	mathematical	—	Space Space.instNormedAddCommGroup Space.instInnerProductSpaceReal momentumOperator radiusRegPowOperator Constants.ℏ positionOperator	—	comp_eq_comp_sub_commute radiusRegPow_commutation_momentum
position_commutation_momentum 📖	mathematical	—	Space Space.instNormedAddCommGroup Space.instInnerProductSpaceReal positionOperator momentumOperator Constants.ℏ KroneckerDelta.kroneckerDelta	—	positionOperator_apply positionOperator_apply_fun Space.deriv_smul Space.eval_differentiable Space.deriv_component KroneckerDelta.eq_one_of_same KroneckerDelta.eq_zero_of_ne
position_commutation_momentumSqr 📖	mathematical	—	Space Space.instNormedAddCommGroup Space.instInnerProductSpaceReal positionOperator momentumOperatorSqr Constants.ℏ momentumOperator	—	lie_leibniz position_commutation_momentum KroneckerDelta.sum_smul
position_commutation_momentum_momentum 📖	mathematical	—	Space Space.instNormedAddCommGroup Space.instInnerProductSpaceReal positionOperator momentumOperator Constants.ℏ KroneckerDelta.kroneckerDelta	—	lie_leibniz position_commutation_momentum
position_commutation_position 📖	mathematical	—	Space Space.instNormedAddCommGroup Space.instInnerProductSpaceReal positionOperator	—	positionOperator_apply
position_commutation_radiusRegPow 📖	mathematical	—	Space Space.instNormedAddCommGroup Space.instInnerProductSpaceReal positionOperator radiusRegPowOperator	—	positionOperator_apply radiusRegPowOperator_apply
position_comp_commute 📖	mathematical	—	Space Space.instNormedAddCommGroup Space.instInnerProductSpaceReal positionOperator	—	comp_eq_comp_add_commute position_commutation_position
position_comp_radiusRegPow_commute 📖	mathematical	—	Space Space.instNormedAddCommGroup Space.instInnerProductSpaceReal positionOperator radiusRegPowOperator	—	comp_eq_comp_add_commute position_commutation_radiusRegPow
position_position_commutation_momentum 📖	mathematical	—	Space Space.instNormedAddCommGroup Space.instInnerProductSpaceReal positionOperator momentumOperator Constants.ℏ KroneckerDelta.kroneckerDelta	—	leibniz_lie position_commutation_momentum
radiusRegPow_commutation_momentum 📖	mathematical	—	Space Space.instNormedAddCommGroup Space.instInnerProductSpaceReal radiusRegPowOperator momentumOperator Constants.ℏ positionOperator	—	norm_sq_add_unit_sq_pos Space.norm_sq_differentiable radiusRegPowOperator_apply_fun positionOperator_apply Space.deriv_smul Space.deriv_eq Space.inner_basis
radiusRegPow_commutation_momentumSqr 📖	mathematical	—	Space Space.instNormedAddCommGroup Space.instInnerProductSpaceReal radiusRegPowOperator momentumOperatorSqr Constants.ℏ positionOperator momentumOperator	—	lie_leibniz radiusRegPow_commutation_momentum momentum_comp_radiusRegPow_eq momentum_comp_position_eq KroneckerDelta.eq_one_of_same positionOperatorSqr_eq radiusRegPowOperator_comp_eq
radiusRegPow_commutation_radiusRegPow 📖	mathematical	—	Space Space.instNormedAddCommGroup Space.instInnerProductSpaceReal radiusRegPowOperator	—	radiusRegPowOperator_comp_eq

---

← Back to Index