Documentation Verification Report

Momentum

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

Statistics

Metric	Count
Definitions `momentumOperator`, `momentumOperatorSchwartz`, `momentumOperatorSqr`, `momentumUnboundedOperator`, `«term𝐩[_]»`, `«term𝐩²»`	6
Theorems `momentumOperatorSchwartz_isSymmetric`, `momentumOperatorSqr_apply`, `momentumOperatorSqr_eq`, `momentumOperator_apply`, `momentumOperator_apply_fun`	5
Total	11

QuantumMechanics

Definitions

Name	Category	Theorems
`momentumOperator` 📖	CompOp	24 math math: `radiusRegPow_commutation_momentumSqr`, `position_commutation_momentum_momentum`, `momentum_comp_angularMomentum_eq`, `momentum_commutation_momentum`, `radiusRegPow_commutation_momentum`, `angularMomentumOperator_apply_fun`, `momentumSqr_commutation_momentum`, `HydrogenAtom.lrlOperator_eq''`, `momentumSqr_comp_momentum_commute`, `position_commutation_momentum`, `momentum_comp_position_eq`, `position_commutation_momentumSqr`, `HydrogenAtom.hamiltonianReg_commutation_lrl`, `momentumOperatorSqr_apply`, `HydrogenAtom.lrlOperator_eq'`, `position_position_commutation_momentum`, `momentumOperator_apply`, `HydrogenAtom.lrlOperator_eq`, `momentumOperator_apply_fun`, `angularMomentumOperator_apply`, `momentum_comp_radiusRegPow_eq`, `momentum_comp_commute`, `momentumOperatorSqr_eq`, `angularMomentum_commutation_momentum`
`momentumOperatorSchwartz` 📖	CompOp	1 math math: `momentumOperatorSchwartz_isSymmetric`
`momentumOperatorSqr` 📖	CompOp	10 math math: `radiusRegPow_commutation_momentumSqr`, `momentumSqr_commutation_momentum`, `momentumSqr_comp_momentum_commute`, `position_commutation_momentumSqr`, `momentumOperatorSqr_apply`, `angularMomentumSqr_commutation_momentumSqr`, `momentumSqr_comp_angularMomentum_commute`, `HydrogenAtom.lrlOperator_eq`, `angularMomentum_commutation_momentumSqr`, `momentumOperatorSqr_eq`
`momentumUnboundedOperator` 📖	CompOp	—
`«term𝐩[_]»` 📖	CompOp	—
`«term𝐩²»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`momentumOperatorSchwartz_isSymmetric` 📖	mathematical	—	`Space` `Space.instNormedAddCommGroup` `Space.instInnerProductSpaceReal` `Space.instFiniteDimensionalReal` `Space.instMeasurableSpace` `Space.instBorelSpace` `SpaceDHilbertSpace` `SpaceDHilbertSpace.schwartzSubmodule` `momentumOperatorSchwartz`	—	`Space.instFiniteDimensionalReal` `Space.instBorelSpace` `SpaceDHilbertSpace.schwartzEquiv_inner` `Space.deriv_eq`
`momentumOperatorSqr_apply` 📖	mathematical	—	`Space` `Space.instNormedAddCommGroup` `Space.instInnerProductSpaceReal` `momentumOperatorSqr` `momentumOperator`	—	—
`momentumOperatorSqr_eq` 📖	mathematical	—	`momentumOperatorSqr` `Space` `Space.instNormedAddCommGroup` `Space.instInnerProductSpaceReal` `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