Completeness

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

Statistics

Metric	Count
Definitions	0
Theorems eigenfunction_completeness, fourierIntegral_zero_of_mem_orthogonal, mul_eigenfunction_integrable, mul_physHermite_integrable, mul_polynomial_integrable, mul_power_integrable, orthogonal_eigenfunction_of_mem_orthogonal, orthogonal_exp_of_mem_orthogonal, orthogonal_physHermite_of_mem_orthogonal, orthogonal_polynomial_of_mem_orthogonal, orthogonal_power_of_mem_orthogonal, zero_of_orthogonal_eigenVector, zero_of_orthogonal_mk	13
Total	13

QuantumMechanics.OneDimension.HarmonicOscillator

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eigenfunction_completeness 📖	mathematical	—	QuantumMechanics.OneDimension.HilbertSpace eigenfunction eigenfunction_memHS	—	eigenfunction_memHS zero_of_orthogonal_eigenVector
fourierIntegral_zero_of_mem_orthogonal 📖	mathematical	QuantumMechanics.OneDimension.HilbertSpace.MemHS QuantumMechanics.OneDimension.HilbertSpace eigenfunction eigenfunction_memHS	ξ	—	eigenfunction_memHS orthogonal_exp_of_mem_orthogonal
mul_eigenfunction_integrable 📖	mathematical	QuantumMechanics.OneDimension.HilbertSpace.MemHS	eigenfunction	—	eigenfunction_memHS QuantumMechanics.OneDimension.HilbertSpace.coe_mk_ae eigenfunction_conj
mul_physHermite_integrable 📖	mathematical	QuantumMechanics.OneDimension.HilbertSpace.MemHS	ξ	—	eigenfunction_eq mul_eigenfunction_integrable ξ_pos
mul_polynomial_integrable 📖	mathematical	QuantumMechanics.OneDimension.HilbertSpace.MemHS	ξ	—	PhysLean.polynomial_mem_physHermite_span mul_physHermite_integrable
mul_power_integrable 📖	mathematical	QuantumMechanics.OneDimension.HilbertSpace.MemHS	ξ	—	mul_polynomial_integrable mul_physHermite_integrable
orthogonal_eigenfunction_of_mem_orthogonal 📖	—	QuantumMechanics.OneDimension.HilbertSpace.MemHS QuantumMechanics.OneDimension.HilbertSpace eigenfunction eigenfunction_memHS	—	—	eigenfunction_memHS eigenfunction_conj
orthogonal_exp_of_mem_orthogonal 📖	mathematical	QuantumMechanics.OneDimension.HilbertSpace.MemHS QuantumMechanics.OneDimension.HilbertSpace eigenfunction eigenfunction_memHS	ξ	—	eigenfunction_memHS QuantumMechanics.OneDimension.HilbertSpace.aeStronglyMeasurable_of_memHS PhysLean.guassian_integrable_polynomial QuantumMechanics.OneDimension.HilbertSpace.exp_abs_mul_abs_mul_gaussian_integrable mul_power_integrable orthogonal_power_of_mem_orthogonal
orthogonal_physHermite_of_mem_orthogonal 📖	mathematical	QuantumMechanics.OneDimension.HilbertSpace.MemHS QuantumMechanics.OneDimension.HilbertSpace eigenfunction eigenfunction_memHS	ξ	—	eigenfunction_memHS orthogonal_eigenfunction_of_mem_orthogonal eigenfunction_eq ξ_pos
orthogonal_polynomial_of_mem_orthogonal 📖	mathematical	QuantumMechanics.OneDimension.HilbertSpace.MemHS QuantumMechanics.OneDimension.HilbertSpace eigenfunction eigenfunction_memHS	ξ	—	eigenfunction_memHS PhysLean.polynomial_mem_physHermite_span mul_physHermite_integrable orthogonal_physHermite_of_mem_orthogonal
orthogonal_power_of_mem_orthogonal 📖	mathematical	QuantumMechanics.OneDimension.HilbertSpace.MemHS QuantumMechanics.OneDimension.HilbertSpace eigenfunction eigenfunction_memHS	ξ	—	eigenfunction_memHS orthogonal_polynomial_of_mem_orthogonal orthogonal_physHermite_of_mem_orthogonal
zero_of_orthogonal_eigenVector 📖	—	QuantumMechanics.OneDimension.HilbertSpace eigenfunction eigenfunction_memHS	—	—	eigenfunction_memHS QuantumMechanics.OneDimension.HilbertSpace.mk_surjective
zero_of_orthogonal_mk 📖	—	QuantumMechanics.OneDimension.HilbertSpace.MemHS QuantumMechanics.OneDimension.HilbertSpace eigenfunction eigenfunction_memHS	—	—	eigenfunction_memHS QuantumMechanics.OneDimension.HilbertSpace.mul_gaussian_mem_Lp_one QuantumMechanics.OneDimension.HilbertSpace.mul_gaussian_mem_Lp_two fourierIntegral_zero_of_mem_orthogonal QuantumMechanics.OneDimension.HilbertSpace.aeStronglyMeasurable_of_memHS

---

← Back to Index