Documentation Verification Report

PlaneWaves

📁 Source: PhysLean/QuantumMechanics/OneDimension/HilbertSpace/PlaneWaves.lean

Statistics

MetricCount
DefinitionsplanewaveFunctional
1
Theoremseq_of_eq_planewaveFunctional, planewaveFunctional_apply
2
Total3

QuantumMechanics.OneDimension.HilbertSpace

Definitions

NameCategoryTheorems
planewaveFunctional 📖CompOp
2 mathmath: QuantumMechanics.OneDimension.planeWaveFunctional_generalized_eigenvector_momentumOperatorUnbounded, planewaveFunctional_apply

Theorems

NameKindAssumesProvesValidatesDepends On
eq_of_eq_planewaveFunctional 📖planewaveFunctional
planewaveFunctional_apply 📖mathematicalplanewaveFunctional

---

← Back to Index