Documentation Verification Report

Basic

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

Statistics

Metric	Count
Definitions `HarmonicOscillator`, `m`, `schrodingerOperator`, `«termPᵒᵖ»`, `«termXᵒᵖ»`, `ξ`, `ω`	7
Theorems `deriv_ofReal`, `differentiableAt_ofReal`, `ofReal_hasDerivAt`, `hm`, `hω`, `m_mul_ω_div_two_ℏ_pos`, `m_mul_ω_div_ℏ_pos`, `m_ne_zero`, `one_over_ξ`, `one_over_ξ_sq`, `schrodingerOperator_add`, `schrodingerOperator_eq`, `schrodingerOperator_eq_ξ`, `schrodingerOperator_parity`, `schrodingerOperator_smul`, `ξ_abs`, `ξ_inverse`, `ξ_ne_zero`, `ξ_nonneg`, `ξ_pos`, `ξ_sq`	21
Total	28

Complex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`deriv_ofReal` 📖	—	—	—	—	`ofReal_hasDerivAt`
`differentiableAt_ofReal` 📖	—	—	—	—	`ofReal_hasDerivAt`
`ofReal_hasDerivAt` 📖	—	—	—	—	—

QuantumMechanics.OneDimension

Definitions

Name	Category	Theorems
`HarmonicOscillator` 📖	CompData	—

QuantumMechanics.OneDimension.HarmonicOscillator

Definitions

Name	Category	Theorems
`m` 📖	CompOp	9 math math: `one_over_ξ`, `ξ_inverse`, `schrodingerOperator_eq_ξ`, `one_over_ξ_sq`, `m_mul_ω_div_two_ℏ_pos`, `ξ_sq`, `hm`, `schrodingerOperator_eq`, `m_mul_ω_div_ℏ_pos`
`schrodingerOperator` 📖	CompOp	6 math math: `schrodingerOperator_add`, `schrodingerOperator_eigenfunction`, `schrodingerOperator_eq_ξ`, `schrodingerOperator_smul`, `schrodingerOperator_parity`, `schrodingerOperator_eq`
`«termPᵒᵖ»` 📖	CompOp	—
`«termXᵒᵖ»` 📖	CompOp	—
`ξ` 📖	CompOp	30 math math: `one_over_ξ`, `orthogonal_exp_of_mem_orthogonal`, `mul_polynomial_integrable`, `eigenfunction_point_norm`, `deriv_deriv_eigenfunction`, `eigenfunction_zero`, `mul_physHermite_integrable`, `fourierIntegral_zero_of_mem_orthogonal`, `mul_power_integrable`, `ξ_inverse`, `deriv_physHermite_characteristic_length`, `schrodingerOperator_eq_ξ`, `ξ_nonneg`, `orthogonal_physHermite_of_mem_orthogonal`, `deriv_eigenfunction_succ`, `deriv_eigenfunction_zero'`, `deriv_deriv_eigenfunction_zero`, `one_over_ξ_sq`, `deriv_deriv_eigenfunction_succ`, `deriv_eigenfunction_zero`, `eigenfunction_mul`, `ξ_sq`, `eigenfunction_eq`, `eigenfunction_mul_self`, `eigenfunction_eq_mul_eigenfunction_zero`, `orthogonal_polynomial_of_mem_orthogonal`, `orthogonal_power_of_mem_orthogonal`, `ξ_pos`, `ξ_abs`, `eigenfunction_point_norm_sq`
`ω` 📖	CompOp	8 math math: `one_over_ξ`, `ξ_inverse`, `one_over_ξ_sq`, `m_mul_ω_div_two_ℏ_pos`, `ξ_sq`, `hω`, `schrodingerOperator_eq`, `m_mul_ω_div_ℏ_pos`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hm` 📖	mathematical	—	`m`	—	—
`hω` 📖	mathematical	—	`ω`	—	—
`m_mul_ω_div_two_ℏ_pos` 📖	mathematical	—	`m` `ω` `Constants.ℏ`	—	`hm` `hω` `Constants.ℏ_pos`
`m_mul_ω_div_ℏ_pos` 📖	mathematical	—	`m` `ω` `Constants.ℏ`	—	`hm` `hω` `Constants.ℏ_pos`
`m_ne_zero` 📖	—	—	—	—	`hm`
`one_over_ξ` 📖	mathematical	—	`ξ` `m` `ω` `Constants.ℏ`	—	`Constants.ℏ_pos`
`one_over_ξ_sq` 📖	mathematical	—	`ξ` `m` `ω` `Constants.ℏ`	—	`one_over_ξ` `m_mul_ω_div_ℏ_pos`
`schrodingerOperator_add` 📖	mathematical	—	`schrodingerOperator`	—	—
`schrodingerOperator_eq` 📖	mathematical	—	`schrodingerOperator` `Constants.ℏ` `m` `ω`	—	—
`schrodingerOperator_eq_ξ` 📖	mathematical	—	`schrodingerOperator` `Constants.ℏ` `m` `ξ`	—	`schrodingerOperator_eq` `ξ_sq` `m_ne_zero` `Constants.ℏ_ne_zero`
`schrodingerOperator_parity` 📖	mathematical	—	`schrodingerOperator` `QuantumMechanics.OneDimension.HilbertSpace.parityOperator`	—	—
`schrodingerOperator_smul` 📖	mathematical	—	`schrodingerOperator`	—	—
`ξ_abs` 📖	mathematical	—	`ξ`	—	`ξ_nonneg`
`ξ_inverse` 📖	mathematical	—	`ξ` `m` `ω` `Constants.ℏ`	—	`one_over_ξ`
`ξ_ne_zero` 📖	—	—	—	—	`ξ_pos`
`ξ_nonneg` 📖	mathematical	—	`ξ`	—	—
`ξ_pos` 📖	mathematical	—	`ξ`	—	`ξ.eq_1` `Constants.ℏ_pos` `hm` `hω`
`ξ_sq` 📖	mathematical	—	`ξ` `Constants.ℏ` `m` `ω`	—	`ξ.eq_1` `Constants.ℏ_nonneg` `hm` `hω`

---

← Back to Index