Documentation Verification Report

Eigenfunction

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

Statistics

Metric	Count
Definitions `eigenfunction`	1
Theorems `eigenfunction_aeStronglyMeasurable`, `eigenfunction_conj`, `eigenfunction_continuous`, `eigenfunction_differentiableAt`, `eigenfunction_eq`, `eigenfunction_eq_mul_eigenfunction_zero`, `eigenfunction_integrable`, `eigenfunction_linearIndependent`, `eigenfunction_memHS`, `eigenfunction_mul`, `eigenfunction_mul_self`, `eigenfunction_normalized`, `eigenfunction_orthogonal`, `eigenfunction_orthonormal`, `eigenfunction_parity`, `eigenfunction_point_norm`, `eigenfunction_point_norm_sq`, `eigenfunction_square_integrable`, `eigenfunction_zero`	19
Total	20

QuantumMechanics.OneDimension.HarmonicOscillator

Definitions

Name	Category	Theorems
`eigenfunction` 📖	CompOp	28 math math: `mul_eigenfunction_integrable`, `eigenfunction_linearIndependent`, `eigenfunction_point_norm`, `deriv_deriv_eigenfunction`, `eigenfunction_square_integrable`, `eigenfunction_zero`, `eigenfunction_conj`, `eigenfunction_memHS`, `schrodingerOperator_eigenfunction`, `eigenfunction_orthonormal`, `eigenfunction_integrable`, `eigenfunction_differentiableAt`, `deriv_eigenfunction_succ`, `deriv_eigenfunction_zero'`, `deriv_deriv_eigenfunction_zero`, `deriv_deriv_eigenfunction_succ`, `eigenfunction_normalized`, `deriv_eigenfunction_zero`, `eigenfunction_completeness`, `eigenfunction_continuous`, `eigenfunction_mul`, `eigenfunction_eq`, `eigenfunction_mul_self`, `eigenfunction_eq_mul_eigenfunction_zero`, `eigenfunction_orthogonal`, `eigenfunction_parity`, `eigenfunction_aeStronglyMeasurable`, `eigenfunction_point_norm_sq`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eigenfunction_aeStronglyMeasurable` 📖	mathematical	—	`eigenfunction`	—	`eigenfunction_integrable`
`eigenfunction_conj` 📖	mathematical	—	`eigenfunction`	—	`eigenfunction_eq`
`eigenfunction_continuous` 📖	mathematical	—	`eigenfunction`	—	`eigenfunction_eq`
`eigenfunction_differentiableAt` 📖	mathematical	—	`eigenfunction`	—	`eigenfunction_eq` `Complex.differentiableAt_ofReal` `PhysLean.physHermite_differentiableAt`
`eigenfunction_eq` 📖	mathematical	—	`eigenfunction` `ξ`	—	—
`eigenfunction_eq_mul_eigenfunction_zero` 📖	mathematical	—	`eigenfunction` `ξ`	—	—
`eigenfunction_integrable` 📖	mathematical	—	`eigenfunction`	—	`eigenfunction_eq` `PhysLean.guassian_integrable_polynomial_cons`
`eigenfunction_linearIndependent` 📖	mathematical	—	`QuantumMechanics.OneDimension.HilbertSpace` `eigenfunction` `eigenfunction_memHS`	—	`eigenfunction_memHS` `eigenfunction_orthonormal`
`eigenfunction_memHS` 📖	mathematical	—	`QuantumMechanics.OneDimension.HilbertSpace.MemHS` `eigenfunction`	—	`QuantumMechanics.OneDimension.HilbertSpace.memHS_iff` `eigenfunction_aeStronglyMeasurable` `eigenfunction_square_integrable`
`eigenfunction_mul` 📖	mathematical	—	`eigenfunction` `ξ`	—	—
`eigenfunction_mul_self` 📖	mathematical	—	`eigenfunction` `ξ`	—	`eigenfunction_mul`
`eigenfunction_normalized` 📖	mathematical	—	`QuantumMechanics.OneDimension.HilbertSpace` `eigenfunction` `eigenfunction_memHS`	—	`eigenfunction_memHS` `eigenfunction_conj` `eigenfunction_mul_self` `PhysLean.physHermite_norm_cons` `ξ_abs` `ξ_pos`
`eigenfunction_orthogonal` 📖	mathematical	—	`QuantumMechanics.OneDimension.HilbertSpace` `eigenfunction` `eigenfunction_memHS`	—	`eigenfunction_memHS` `eigenfunction_conj` `eigenfunction_mul` `PhysLean.physHermite_orthogonal_cons`
`eigenfunction_orthonormal` 📖	mathematical	—	`QuantumMechanics.OneDimension.HilbertSpace` `eigenfunction` `eigenfunction_memHS`	—	`eigenfunction_memHS` `eigenfunction_normalized` `eigenfunction_orthogonal`
`eigenfunction_parity` 📖	mathematical	—	`QuantumMechanics.OneDimension.HilbertSpace.parityOperator` `eigenfunction`	—	`eigenfunction_eq` `PhysLean.physHermite_eq_aeval` `PhysLean.physHermite_parity`
`eigenfunction_point_norm` 📖	mathematical	—	`eigenfunction` `ξ`	—	`eigenfunction_eq`
`eigenfunction_point_norm_sq` 📖	mathematical	—	`eigenfunction` `ξ`	—	`eigenfunction_point_norm`
`eigenfunction_square_integrable` 📖	mathematical	—	`eigenfunction`	—	`eigenfunction_point_norm_sq` `PhysLean.physHermite_pow` `PhysLean.guassian_integrable_polynomial_cons`
`eigenfunction_zero` 📖	mathematical	—	`eigenfunction` `ξ`	—	—

---

← Back to Index