Documentation Verification Report

TISE

📁 Source: PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/TISE.lean

Statistics

Metric	Count
Definitions `eigenValue`	1
Theorems `deriv_deriv_eigenfunction`, `deriv_deriv_eigenfunction_succ`, `deriv_deriv_eigenfunction_zero`, `deriv_eigenfunction_succ`, `deriv_eigenfunction_zero`, `deriv_eigenfunction_zero'`, `deriv_physHermite_characteristic_length`, `schrodingerOperator_eigenfunction`	8
Total	9

QuantumMechanics.OneDimension.HarmonicOscillator

Definitions

Name	Category	Theorems
`eigenValue` 📖	CompOp	1 math math: `schrodingerOperator_eigenfunction`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`deriv_deriv_eigenfunction` 📖	mathematical	—	`eigenfunction` `ξ`	—	`deriv_deriv_eigenfunction_zero` `deriv_deriv_eigenfunction_succ` `deriv_physHermite_characteristic_length` `PhysLean.physHermite_succ` `PhysLean.derivative_physHermite` `eigenfunction_eq_mul_eigenfunction_zero`
`deriv_deriv_eigenfunction_succ` 📖	mathematical	—	`eigenfunction` `ξ`	—	`deriv_eigenfunction_succ` `Complex.differentiableAt_ofReal` `PhysLean.physHermite_differentiableAt` `eigenfunction_differentiableAt` `deriv_eigenfunction_zero` `Complex.deriv_ofReal` `deriv_physHermite_characteristic_length`
`deriv_deriv_eigenfunction_zero` 📖	mathematical	—	`eigenfunction` `ξ`	—	`deriv_eigenfunction_zero` `Complex.differentiableAt_ofReal` `eigenfunction_differentiableAt` `Complex.deriv_ofReal`
`deriv_eigenfunction_succ` 📖	mathematical	—	`eigenfunction` `ξ`	—	`eigenfunction_eq_mul_eigenfunction_zero` `Complex.differentiableAt_ofReal` `PhysLean.physHermite_differentiableAt` `eigenfunction_differentiableAt` `deriv_physHermite_characteristic_length` `deriv_eigenfunction_zero`
`deriv_eigenfunction_zero` 📖	mathematical	—	`eigenfunction` `ξ`	—	`eigenfunction_zero` `Complex.differentiableAt_ofReal` `Complex.deriv_ofReal`
`deriv_eigenfunction_zero'` 📖	mathematical	—	`eigenfunction` `ξ`	—	`deriv_eigenfunction_zero` `eigenfunction_eq` `PhysLean.physHermite_one`
`deriv_physHermite_characteristic_length` 📖	mathematical	—	`ξ`	—	`PhysLean.physHermite_zero` `Complex.differentiableAt_ofReal` `PhysLean.physHermite_differentiableAt` `Complex.deriv_ofReal` `PhysLean.deriv_physHermite`
`schrodingerOperator_eigenfunction` 📖	mathematical	—	`schrodingerOperator` `eigenfunction` `eigenValue`	—	`schrodingerOperator_eq_ξ` `deriv_deriv_eigenfunction` `hm` `Constants.ℏ_ne_zero` `eigenValue.eq_1` `ξ_sq`

---

← Back to Index