Source-pinned research
Search theorem names, mathematical ideas, modules, topics, projects, and role-labelled researchers. Open a result for its complete indexed Lean declaration and source record.
This index contains 591 research declarations. Search 10,000 more complete Mathlib declarations.
591 results
Clear filtersQuantumMechanics.OneDimension.HarmonicOscillator.deriv_eigenfunction_zero
Project documentation
The nth eigenvalues for a Harmonic oscillator is defined as (n + 1/2) * ℏ * ω. -/ noncomputable def eigenValue (n : ℕ) : ℝ := (n + 1/2) * ℏ * Q.ω /-! ## Derivatives of the eigenfunctions
Source project: Physlib
Person-level attribution pending.
QuantumMechanics.OneDimension.HarmonicOscillator.eigenfunction_completeness
Project documentation
Assuming Plancherel's theorem (which is not yet in Mathlib), the topological closure of the span of the eigenfunctions of the harmonic oscillator is the whole Hilbert space. The proof of this result relies on fourierIntegral_zero_of_mem_orthogonal and Plancherel's theorem which together give us that the norm of f x * e ^ (- x^2 / (2 * ξ^2)) is zero fo...
Source project: Physlib
Person-level attribution pending.
QuantumMechanics.OneDimension.HarmonicOscillator.eigenfunction_integrable
Plain-language statement
The eigenfunctions are integrable.
Source project: Physlib
Person-level attribution pending.
QuantumMechanics.OneDimension.HarmonicOscillator.eigenfunction_mul
Plain-language statement
A simplification of the product of two eigenfunctions.
Source project: Physlib
Person-level attribution pending.
QuantumMechanics.OneDimension.HarmonicOscillator.eigenfunction_normalized
Plain-language statement
The eigenfunction are normalized.
Source project: Physlib
Person-level attribution pending.
QuantumMechanics.OneDimension.HarmonicOscillator.eigenfunction_orthogonal
Plain-language statement
The eigenfunctions of the quantum harmonic oscillator are orthogonal.
Source project: Physlib
Person-level attribution pending.