Documentation Verification Report

Position

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

Statistics

Metric	Count
Definitions `positionOperator`, `positionOperatorSchwartz`, `positionOperatorUnbounded`	3
Theorems `positionOperatorSchwartz_apply`, `positionOperatorSchwartz_apply_fun`, `positionOperatorUnbounded_isSelfAdjoint`, `positionStates_generalized_eigenvector_positionOperatorUnbounded`	4
Total	7

QuantumMechanics.OneDimension

Definitions

Name	Category	Theorems
`positionOperator` 📖	CompOp	—
`positionOperatorSchwartz` 📖	CompOp	5 math math: `positionOperatorSchwartz_momentumOperatorSchwartz_eq`, `positionOperatorSchwartz_apply_fun`, `positionOperatorSchwartz_apply`, `momentumOperatorSchwartz_positionOperatorSchwartz_eq`, `positionOperatorSchwartz_commutation_momentumOperatorSchwartz`
`positionOperatorUnbounded` 📖	CompOp	2 math math: `positionStates_generalized_eigenvector_positionOperatorUnbounded`, `positionOperatorUnbounded_isSelfAdjoint`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`positionOperatorSchwartz_apply` 📖	mathematical	—	`positionOperatorSchwartz`	—	—
`positionOperatorSchwartz_apply_fun` 📖	mathematical	—	`positionOperatorSchwartz`	—	—
`positionOperatorUnbounded_isSelfAdjoint` 📖	mathematical	—	`UnboundedOperator.IsSelfAdjoint` `HilbertSpace.schwartzIncl` `HilbertSpace.schwartzIncl_injective` `positionOperatorUnbounded`	—	`HilbertSpace.schwartzIncl_inner` `positionOperatorSchwartz_apply`
`positionStates_generalized_eigenvector_positionOperatorUnbounded` 📖	mathematical	—	`UnboundedOperator.IsGeneralizedEigenvector` `HilbertSpace.schwartzIncl` `HilbertSpace.schwartzIncl_injective` `positionOperatorUnbounded` `HilbertSpace.positionState`	—	`HilbertSpace.schwartzIncl_injective` `UnboundedOperator.isGeneralizedEigenvector_ofSelfCLM_iff` `positionOperatorSchwartz_apply`

---

← Back to Index