PhysLean Documentation

PhysLean.QuantumMechanics.OneDimension.HarmonicOscillator.Eigenfunction

Eigenfunction of the Harmonic Oscillator #

source
noncomputable def QuantumMechanics.OneDimension.HarmonicOscillator.eigenfunction (Q : HarmonicOscillator) (n : ℕ) :
ℝ → ℂ

The nth eigenfunction of the Harmonic oscillator is defined as the function ℝ → ℂ taking x : ℝ to

1/√(2^n n!) 1/√(√π ξ) * physHermite n (x / ξ) * e ^ (- x²/ (2 ξ²)).

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem QuantumMechanics.OneDimension.HarmonicOscillator.eigenfunction_eq (Q : HarmonicOscillator) (n : ℕ) :
    Q.eigenfunction n = fun (x : ℝ) => 1 / ↑√(2 ^ n * ↑n.factorial) * (1 / ↑√(√Real.pi * Q.ξ)) * ↑((fun (x : ℝ) => (Polynomial.aeval x) (PhysLean.physHermite n)) (x / Q.ξ) * Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2)))
    source
    theorem QuantumMechanics.OneDimension.HarmonicOscillator.eigenfunction_zero (Q : HarmonicOscillator) :
    Q.eigenfunction 0 = fun (x : ℝ) => 1 / ↑√(√Real.pi * Q.ξ) * Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))
    source
    theorem QuantumMechanics.OneDimension.HarmonicOscillator.eigenfunction_eq_mul_eigenfunction_zero (Q : HarmonicOscillator) (n : ℕ) :
    Q.eigenfunction n = fun (x : ℝ) => ↑(1 / √(2 ^ n * ↑n.factorial)) * ↑((fun (x : ℝ) => (Polynomial.aeval x) (PhysLean.physHermite n)) (x / Q.ξ)) * Q.eigenfunction 0 x

    Basic properties of the eigenfunctions #

    source
    theorem QuantumMechanics.OneDimension.HarmonicOscillator.eigenfunction_integrable (Q : HarmonicOscillator) (n : ℕ) :
    MeasureTheory.Integrable (Q.eigenfunction n) MeasureTheory.volume

    The eigenfunctions are integrable.

    source
    @[simp]
    theorem QuantumMechanics.OneDimension.HarmonicOscillator.eigenfunction_conj (Q : HarmonicOscillator) (n : ℕ) (x : ℝ) :
    (starRingEnd ℂ) (Q.eigenfunction n x) = Q.eigenfunction n x

    The eigenfunctions are real.

    source
    theorem QuantumMechanics.OneDimension.HarmonicOscillator.eigenfunction_point_norm (Q : HarmonicOscillator) (n : ℕ) (x : ℝ) :
    ‖Q.eigenfunction n x‖ = 1 / √(2 ^ n * ↑n.factorial) * (1 / √(√Real.pi * Q.ξ)) * (|(fun (x : ℝ) => (Polynomial.aeval x) (PhysLean.physHermite n)) (x / Q.ξ)| * Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2)))
    source
    theorem QuantumMechanics.OneDimension.HarmonicOscillator.eigenfunction_point_norm_sq (Q : HarmonicOscillator) (n : ℕ) (x : ℝ) :
    ‖Q.eigenfunction n x‖ ^ 2 = (1 / √(2 ^ n * ↑n.factorial) * (1 / √(√Real.pi * Q.ξ))) ^ 2 * ((fun (x : ℝ) => (Polynomial.aeval x) (PhysLean.physHermite n)) (x / Q.ξ) ^ 2 * Real.exp (-x ^ 2 / Q.ξ ^ 2))
    source
    theorem QuantumMechanics.OneDimension.HarmonicOscillator.eigenfunction_square_integrable (Q : HarmonicOscillator) (n : ℕ) :
    MeasureTheory.Integrable (fun (x : ℝ) => ‖Q.eigenfunction n x‖ ^ 2) MeasureTheory.volume

    The eigenfunctions are square integrable.

    source
    theorem QuantumMechanics.OneDimension.HarmonicOscillator.eigenfunction_aeStronglyMeasurable (Q : HarmonicOscillator) (n : ℕ) :
    MeasureTheory.AEStronglyMeasurable (Q.eigenfunction n) MeasureTheory.volume

    The eigenfunctions are almost everywhere strongly measurable.

    source
    theorem QuantumMechanics.OneDimension.HarmonicOscillator.eigenfunction_memHS (Q : HarmonicOscillator) (n : ℕ) :
    HilbertSpace.MemHS (Q.eigenfunction n)

    The eigenfunctions are members of the Hilbert space.

    source
    theorem QuantumMechanics.OneDimension.HarmonicOscillator.eigenfunction_differentiableAt (Q : HarmonicOscillator) (x : ℝ) (n : ℕ) :
    DifferentiableAt ℝ (Q.eigenfunction n) x

    The eigenfunctions are differentiable.

    source
    theorem QuantumMechanics.OneDimension.HarmonicOscillator.eigenfunction_continuous (Q : HarmonicOscillator) (n : ℕ) :
    Continuous (Q.eigenfunction n)

    The eigenfunctions are continuous.

    source
    theorem QuantumMechanics.OneDimension.HarmonicOscillator.eigenfunction_parity (Q : HarmonicOscillator) (n : ℕ) :
    HilbertSpace.parity (Q.eigenfunction n) = (-1) ^ n * Q.eigenfunction n

    The nth eigenfunction is an eigenfunction of the parity operator with the eigenvalue (-1) ^ n.

    Orthnormality #

    source
    theorem QuantumMechanics.OneDimension.HarmonicOscillator.eigenfunction_mul (Q : HarmonicOscillator) {x : ℝ} (n p : ℕ) :
    Q.eigenfunction n x * Q.eigenfunction p x = 1 / ↑√(2 ^ n * ↑n.factorial) * 1 / ↑√(2 ^ p * ↑p.factorial) * (1 / (↑√Real.pi * ↑Q.ξ)) * ↑((fun (x : ℝ) => (Polynomial.aeval x) (PhysLean.physHermite n)) (x / Q.ξ) * (fun (x : ℝ) => (Polynomial.aeval x) (PhysLean.physHermite p)) (x / Q.ξ) * Real.exp (-x ^ 2 / Q.ξ ^ 2))

    A simplification of the product of two eigen-functions.

    source
    theorem QuantumMechanics.OneDimension.HarmonicOscillator.eigenfunction_mul_self (Q : HarmonicOscillator) {x : ℝ} (n : ℕ) :
    Q.eigenfunction n x * Q.eigenfunction n x = 1 / (2 ^ n * ↑n.factorial) * (1 / (↑√Real.pi * ↑Q.ξ)) * ↑((fun (x : ℝ) => (Polynomial.aeval x) (PhysLean.physHermite n)) (x / Q.ξ) ^ 2 * Real.exp (-x ^ 2 / Q.ξ ^ 2))
    source
    theorem QuantumMechanics.OneDimension.HarmonicOscillator.eigenfunction_normalized (Q : HarmonicOscillator) (n : ℕ) :
    inner (HilbertSpace.mk ⋯) (HilbertSpace.mk ⋯) = 1

    The eigenfunction are normalized.

    source
    theorem QuantumMechanics.OneDimension.HarmonicOscillator.eigenfunction_orthogonal (Q : HarmonicOscillator) {n p : ℕ} (hnp : n ≠ p) :
    inner (HilbertSpace.mk ⋯) (HilbertSpace.mk ⋯) = 0

    The eigen-functions of the quantum harmonic oscillator are orthogonal.

    source
    theorem QuantumMechanics.OneDimension.HarmonicOscillator.eigenfunction_orthonormal (Q : HarmonicOscillator) :
    Orthonormal ℂ fun (n : ℕ) => HilbertSpace.mk ⋯

    The eigenfunctions are orthonormal within the Hilbert space.

    source
    theorem QuantumMechanics.OneDimension.HarmonicOscillator.eigenfunction_linearIndependent (Q : HarmonicOscillator) :
    LinearIndependent ℂ fun (n : ℕ) => HilbertSpace.mk ⋯

    The eigenfunctions are linearly independent.