Physlib.QuantumMechanics.HarmonicOscillator.OneDimension.Eigenfunction

Imports

/-
Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
module

public import Physlib.QuantumMechanics.HarmonicOscillator.OneDimension.Basic
public import Physlib.Mathematics.SpecialFunctions.PhysHermite

Eigenfunction of the Harmonic Oscillator

              @[expose] public sectionlemma eigenfunction_eq (n : ℕ) :
    Q.eigenfunction n = fun (x : ℝ) => (1/√(2 ^ n * n !) * (1/ √(√Real.pi * Q.ξ))) *
    Complex.ofReal (physHermite n (x / Q.ξ) * Real.exp (- x^2 / (2 * Q.ξ^2))) := byQ:HarmonicOscillatorn:ℕ⊢ Q.eigenfunction n = fun x =>
  1 / ↑√(2 ^ n * ↑n !) * (1 / ↑√(√Real.pi * Q.ξ)) * ↑(↑(physHermite n) (x / Q.ξ) * Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2)))
  funext xQ:HarmonicOscillatorn:ℕx:ℝ⊢ Q.eigenfunction n x =
  1 / ↑√(2 ^ n * ↑n !) * (1 / ↑√(√Real.pi * Q.ξ)) * ↑(↑(physHermite n) (x / Q.ξ) * Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2)))
  simp only [eigenfunction, ofNat_nonneg, pow_nonneg, Real.sqrt_mul, Complex.ofReal_mul, one_div,
    mul_inv_rev, Complex.ofReal_exp, Complex.ofReal_div, Complex.ofReal_neg,
    Complex.ofReal_pow, Complex.ofReal_ofNat]Q:HarmonicOscillatorn:ℕx:ℝ⊢ (↑√↑n !)⁻¹ * (↑√(2 ^ n))⁻¹ * (↑√(√Real.pi * Q.ξ))⁻¹ * ↑(↑(physHermite n) (x / Q.ξ)) *
    Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2)) =
  (↑√↑n !)⁻¹ * (↑√(2 ^ n))⁻¹ * (↑√(√Real.pi * Q.ξ))⁻¹ *
    (↑(↑(physHermite n) (x / Q.ξ)) * Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2)))
  ringAll goals completed! 🐙lemma eigenfunction_zero : Q.eigenfunction 0 = fun (x : ℝ) =>
    (1/ √(√Real.pi * Q.ξ)) * Complex.exp (- x^2 / (2 * Q.ξ^2)) := byQ:HarmonicOscillator⊢ Q.eigenfunction 0 = fun x => 1 / ↑√(√Real.pi * Q.ξ) * Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))
  funext xQ:HarmonicOscillatorx:ℝ⊢ Q.eigenfunction 0 x = 1 / ↑√(√Real.pi * Q.ξ) * Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))
  simp [eigenfunction]All goals completed! 🐙lemma eigenfunction_eq_mul_eigenfunction_zero (n : ℕ) :
    Q.eigenfunction n = fun x => Complex.ofReal (1/√(2 ^ n * n !))
    * Complex.ofReal (physHermite n (x / Q.ξ)) * Q.eigenfunction 0 x := byQ:HarmonicOscillatorn:ℕ⊢ Q.eigenfunction n = fun x => ↑(1 / √(2 ^ n * ↑n !)) * ↑(↑(physHermite n) (x / Q.ξ)) * Q.eigenfunction 0 x
  match n with
  | 0 =>Q:HarmonicOscillatorn:ℕ⊢ Q.eigenfunction 0 = fun x => ↑(1 / √(2 ^ 0 * ↑0!)) * ↑(↑(physHermite 0) (x / Q.ξ)) * Q.eigenfunction 0 x
    simpAll goals completed! 🐙
  | n + 1 =>Q:HarmonicOscillatorn✝:ℕn:ℕ⊢ Q.eigenfunction (n + 1) = fun x =>
  ↑(1 / √(2 ^ (n + 1) * ↑(n + 1)!)) * ↑(↑(physHermite (n + 1)) (x / Q.ξ)) * Q.eigenfunction 0 x
    funext xQ:HarmonicOscillatorn✝:ℕn:ℕx:ℝ⊢ Q.eigenfunction (n + 1) x =
  ↑(1 / √(2 ^ (n + 1) * ↑(n + 1)!)) * ↑(↑(physHermite (n + 1)) (x / Q.ξ)) * Q.eigenfunction 0 x
    simp only [eigenfunction, one_div, Complex.ofReal_inv, pow_zero, factorial_zero, cast_one,
      mul_one, Real.sqrt_one, Complex.ofReal_one, ne_eq, one_ne_zero, not_false_eq_true, div_self,
      one_mul, physHermite_zero, map_one]Q:HarmonicOscillatorn✝:ℕn:ℕx:ℝ⊢ (↑√(2 ^ (n + 1) * ↑(n + 1)!))⁻¹ * (↑√(√Real.pi * Q.ξ))⁻¹ * ↑(↑(physHermite (n + 1)) (x / Q.ξ)) *
    ↑(Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))) =
  (↑√(2 ^ (n + 1) * ↑(n + 1)!))⁻¹ * ↑(↑(physHermite (n + 1)) (x / Q.ξ)) *
    ((↑√(√Real.pi * Q.ξ))⁻¹ * ↑(Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))))
    field_simpAll goals completed! 🐙

Basic properties of the eigenfunctions

The eigenfunctions are integrable.


@[fun_prop]
lemma eigenfunction_integrable (n : ℕ) : Integrable (Q.eigenfunction n) := byQ:HarmonicOscillatorn:ℕ⊢ Integrable (Q.eigenfunction n) volume
  rw [eigenfunction_eqQ:HarmonicOscillatorn:ℕ⊢ Integrable
  (fun x =>
    1 / ↑√(2 ^ n * ↑n !) * (1 / ↑√(√Real.pi * Q.ξ)) * ↑(↑(physHermite n) (x / Q.ξ) * Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))))
  volumeQ:HarmonicOscillatorn:ℕ⊢ Integrable
  (fun x =>
    1 / ↑√(2 ^ n * ↑n !) * (1 / ↑√(√Real.pi * Q.ξ)) * ↑(↑(physHermite n) (x / Q.ξ) * Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))))
  volume]Q:HarmonicOscillatorn:ℕ⊢ Integrable
  (fun x =>
    1 / ↑√(2 ^ n * ↑n !) * (1 / ↑√(√Real.pi * Q.ξ)) * ↑(↑(physHermite n) (x / Q.ξ) * Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))))
  volume
  apply Integrable.const_mulQ:HarmonicOscillatorn:ℕ⊢ Integrable (fun x => ↑(↑(physHermite n) (x / Q.ξ) * Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2)))) volume
  apply Integrable.ofRealQ:HarmonicOscillatorn:ℕ⊢ Integrable (fun x => Real.mul✝ (↑(physHermite n) (x / Q.ξ)) (Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2)))) volume
  change Integrable (fun x => physHermite n (x / Q.ξ) * Real.exp (- x^2 / (2 * Q.ξ^2)))Q:HarmonicOscillatorn:ℕ⊢ Integrable (fun x => ↑(physHermite n) (x / Q.ξ) * Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))) volume
  have h1 : (fun x => physHermite n (x / Q.ξ) * Real.exp (- x^2 / (2 * Q.ξ^2))) =
      (fun x => physHermite n (1/Q.ξ * x) * Real.exp (- (1 / (2 * Q.ξ^2)) * x ^ 2)) := byQ:HarmonicOscillatorn:ℕ⊢ Integrable (Q.eigenfunction n) volumeQ:HarmonicOscillatorn:ℕh1:(fun x => ↑(physHermite n) (x / Q.ξ) * Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))) = fun x =>
  ↑(physHermite n) (1 / Q.ξ * x) * Real.exp (-(1 / (2 * Q.ξ ^ 2)) * x ^ 2)⊢ Integrable (fun x => ↑(physHermite n) (x / Q.ξ) * Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))) volume
    funext xQ:HarmonicOscillatorn:ℕx:ℝ⊢ ↑(physHermite n) (x / Q.ξ) * Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2)) =
  ↑(physHermite n) (1 / Q.ξ * x) * Real.exp (-(1 / (2 * Q.ξ ^ 2)) * x ^ 2)Q:HarmonicOscillatorn:ℕh1:(fun x => ↑(physHermite n) (x / Q.ξ) * Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))) = fun x =>
  ↑(physHermite n) (1 / Q.ξ * x) * Real.exp (-(1 / (2 * Q.ξ ^ 2)) * x ^ 2)⊢ Integrable (fun x => ↑(physHermite n) (x / Q.ξ) * Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))) volume
    ring_nfQ:HarmonicOscillatorn:ℕh1:(fun x => ↑(physHermite n) (x / Q.ξ) * Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))) = fun x =>
  ↑(physHermite n) (1 / Q.ξ * x) * Real.exp (-(1 / (2 * Q.ξ ^ 2)) * x ^ 2)⊢ Integrable (fun x => ↑(physHermite n) (x / Q.ξ) * Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))) volumeQ:HarmonicOscillatorn:ℕh1:(fun x => ↑(physHermite n) (x / Q.ξ) * Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))) = fun x =>
  ↑(physHermite n) (1 / Q.ξ * x) * Real.exp (-(1 / (2 * Q.ξ ^ 2)) * x ^ 2)⊢ Integrable (fun x => ↑(physHermite n) (x / Q.ξ) * Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))) volume
  rw [h1Q:HarmonicOscillatorn:ℕh1:(fun x => ↑(physHermite n) (x / Q.ξ) * Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))) = fun x =>
  ↑(physHermite n) (1 / Q.ξ * x) * Real.exp (-(1 / (2 * Q.ξ ^ 2)) * x ^ 2)⊢ Integrable (fun x => ↑(physHermite n) (1 / Q.ξ * x) * Real.exp (-(1 / (2 * Q.ξ ^ 2)) * x ^ 2)) volumeQ:HarmonicOscillatorn:ℕh1:(fun x => ↑(physHermite n) (x / Q.ξ) * Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))) = fun x =>
  ↑(physHermite n) (1 / Q.ξ * x) * Real.exp (-(1 / (2 * Q.ξ ^ 2)) * x ^ 2)⊢ Integrable (fun x => ↑(physHermite n) (1 / Q.ξ * x) * Real.exp (-(1 / (2 * Q.ξ ^ 2)) * x ^ 2)) volume]Q:HarmonicOscillatorn:ℕh1:(fun x => ↑(physHermite n) (x / Q.ξ) * Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))) = fun x =>
  ↑(physHermite n) (1 / Q.ξ * x) * Real.exp (-(1 / (2 * Q.ξ ^ 2)) * x ^ 2)⊢ Integrable (fun x => ↑(physHermite n) (1 / Q.ξ * x) * Real.exp (-(1 / (2 * Q.ξ ^ 2)) * x ^ 2)) volume
  apply guassian_integrable_polynomial_consQ:HarmonicOscillatorn:ℕh1:(fun x => ↑(physHermite n) (x / Q.ξ) * Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))) = fun x =>
  ↑(physHermite n) (1 / Q.ξ * x) * Real.exp (-(1 / (2 * Q.ξ ^ 2)) * x ^ 2)⊢ 0 < 1 / (2 * Q.ξ ^ 2)
  simpAll goals completed! 🐙

The eigenfunctions are real.


@[simp]
lemma eigenfunction_conj (n : ℕ) (x : ℝ) :
    (starRingEnd ℂ) (Q.eigenfunction n x) = Q.eigenfunction n x := byQ:HarmonicOscillatorn:ℕx:ℝ⊢ (starRingEnd ℂ) (Q.eigenfunction n x) = Q.eigenfunction n x
  rw [eigenfunction_eqQ:HarmonicOscillatorn:ℕx:ℝ⊢ (starRingEnd ℂ)
    ((fun x =>
        1 / ↑√(2 ^ n * ↑n !) * (1 / ↑√(√Real.pi * Q.ξ)) *
          ↑(↑(physHermite n) (x / Q.ξ) * Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))))
      x) =
  (fun x =>
      1 / ↑√(2 ^ n * ↑n !) * (1 / ↑√(√Real.pi * Q.ξ)) *
        ↑(↑(physHermite n) (x / Q.ξ) * Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))))
    xQ:HarmonicOscillatorn:ℕx:ℝ⊢ (starRingEnd ℂ)
    ((fun x =>
        1 / ↑√(2 ^ n * ↑n !) * (1 / ↑√(√Real.pi * Q.ξ)) *
          ↑(↑(physHermite n) (x / Q.ξ) * Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))))
      x) =
  (fun x =>
      1 / ↑√(2 ^ n * ↑n !) * (1 / ↑√(√Real.pi * Q.ξ)) *
        ↑(↑(physHermite n) (x / Q.ξ) * Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))))
    x]Q:HarmonicOscillatorn:ℕx:ℝ⊢ (starRingEnd ℂ)
    ((fun x =>
        1 / ↑√(2 ^ n * ↑n !) * (1 / ↑√(√Real.pi * Q.ξ)) *
          ↑(↑(physHermite n) (x / Q.ξ) * Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))))
      x) =
  (fun x =>
      1 / ↑√(2 ^ n * ↑n !) * (1 / ↑√(√Real.pi * Q.ξ)) *
        ↑(↑(physHermite n) (x / Q.ξ) * Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))))
    x
  simp [-Complex.ofReal_exp]All goals completed! 🐙



lemma eigenfunction_point_norm (n : ℕ) (x : ℝ) :
    ‖Q.eigenfunction n x‖ = (1/√(2 ^ n * n !) * (1/ √(√Real.pi * Q.ξ))) *
    (|physHermite n (x / Q.ξ)| * Real.exp (- x ^ 2 / (2 * Q.ξ ^ 2))) := byQ:HarmonicOscillatorn:ℕx:ℝ⊢ ‖Q.eigenfunction n x‖ =
  1 / √(2 ^ n * ↑n !) * (1 / √(√Real.pi * Q.ξ)) * (|↑(physHermite n) (x / Q.ξ)| * Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2)))
  rw [eigenfunction_eqQ:HarmonicOscillatorn:ℕx:ℝ⊢ ‖(fun x =>
        1 / ↑√(2 ^ n * ↑n !) * (1 / ↑√(√Real.pi * Q.ξ)) *
          ↑(↑(physHermite n) (x / Q.ξ) * Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))))
      x‖ =
  1 / √(2 ^ n * ↑n !) * (1 / √(√Real.pi * Q.ξ)) * (|↑(physHermite n) (x / Q.ξ)| * Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2)))Q:HarmonicOscillatorn:ℕx:ℝ⊢ ‖(fun x =>
        1 / ↑√(2 ^ n * ↑n !) * (1 / ↑√(√Real.pi * Q.ξ)) *
          ↑(↑(physHermite n) (x / Q.ξ) * Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))))
      x‖ =
  1 / √(2 ^ n * ↑n !) * (1 / √(√Real.pi * Q.ξ)) * (|↑(physHermite n) (x / Q.ξ)| * Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2)))]Q:HarmonicOscillatorn:ℕx:ℝ⊢ ‖(fun x =>
        1 / ↑√(2 ^ n * ↑n !) * (1 / ↑√(√Real.pi * Q.ξ)) *
          ↑(↑(physHermite n) (x / Q.ξ) * Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))))
      x‖ =
  1 / √(2 ^ n * ↑n !) * (1 / √(√Real.pi * Q.ξ)) * (|↑(physHermite n) (x / Q.ξ)| * Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2)))
  simp only [Complex.ofReal_mul]Q:HarmonicOscillatorn:ℕx:ℝ⊢ ‖1 / ↑√(2 ^ n * ↑n !) * (1 / ↑√(√Real.pi * Q.ξ)) *
      (↑(↑(physHermite n) (x / Q.ξ)) * ↑(Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))))‖ =
  1 / √(2 ^ n * ↑n !) * (1 / √(√Real.pi * Q.ξ)) * (|↑(physHermite n) (x / Q.ξ)| * Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2)))
  rw [norm_mul,Q:HarmonicOscillatorn:ℕx:ℝ⊢ ‖1 / ↑√(2 ^ n * ↑n !) * (1 / ↑√(√Real.pi * Q.ξ))‖ *
    ‖↑(↑(physHermite n) (x / Q.ξ)) * ↑(Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2)))‖ =
  1 / √(2 ^ n * ↑n !) * (1 / √(√Real.pi * Q.ξ)) * (|↑(physHermite n) (x / Q.ξ)| * Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2)))Q:HarmonicOscillatorn:ℕx:ℝ⊢ ‖1 / ↑√(2 ^ n * ↑n !)‖ * ‖1 / ↑√(√Real.pi * Q.ξ)‖ *
    ‖↑(↑(physHermite n) (x / Q.ξ)) * ↑(Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2)))‖ =
  1 / √(2 ^ n * ↑n !) * (1 / √(√Real.pi * Q.ξ)) * (|↑(physHermite n) (x / Q.ξ)| * Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))) norm_mulQ:HarmonicOscillatorn:ℕx:ℝ⊢ ‖1 / ↑√(2 ^ n * ↑n !)‖ * ‖1 / ↑√(√Real.pi * Q.ξ)‖ *
    ‖↑(↑(physHermite n) (x / Q.ξ)) * ↑(Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2)))‖ =
  1 / √(2 ^ n * ↑n !) * (1 / √(√Real.pi * Q.ξ)) * (|↑(physHermite n) (x / Q.ξ)| * Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2)))Q:HarmonicOscillatorn:ℕx:ℝ⊢ ‖1 / ↑√(2 ^ n * ↑n !)‖ * ‖1 / ↑√(√Real.pi * Q.ξ)‖ *
    ‖↑(↑(physHermite n) (x / Q.ξ)) * ↑(Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2)))‖ =
  1 / √(2 ^ n * ↑n !) * (1 / √(√Real.pi * Q.ξ)) * (|↑(physHermite n) (x / Q.ξ)| * Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2)))]Q:HarmonicOscillatorn:ℕx:ℝ⊢ ‖1 / ↑√(2 ^ n * ↑n !)‖ * ‖1 / ↑√(√Real.pi * Q.ξ)‖ *
    ‖↑(↑(physHermite n) (x / Q.ξ)) * ↑(Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2)))‖ =
  1 / √(2 ^ n * ↑n !) * (1 / √(√Real.pi * Q.ξ)) * (|↑(physHermite n) (x / Q.ξ)| * Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2)))
  congre_a.e_aQ:HarmonicOscillatorn:ℕx:ℝ⊢ ‖1 / ↑√(2 ^ n * ↑n !)‖ = 1 / √(2 ^ n * ↑n !)e_a.e_aQ:HarmonicOscillatorn:ℕx:ℝ⊢ ‖1 / ↑√(√Real.pi * Q.ξ)‖ = 1 / √(√Real.pi * Q.ξ)e_aQ:HarmonicOscillatorn:ℕx:ℝ⊢ ‖↑(↑(physHermite n) (x / Q.ξ)) * ↑(Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2)))‖ =
  |↑(physHermite n) (x / Q.ξ)| * Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))
  ·e_a.e_aQ:HarmonicOscillatorn:ℕx:ℝ⊢ ‖1 / ↑√(2 ^ n * ↑n !)‖ = 1 / √(2 ^ n * ↑n !) simp [Real.sqrt_nonneg, abs_of_nonneg]All goals completed! 🐙
  ·e_a.e_aQ:HarmonicOscillatorn:ℕx:ℝ⊢ ‖1 / ↑√(√Real.pi * Q.ξ)‖ = 1 / √(√Real.pi * Q.ξ) simp [Real.sqrt_nonneg, abs_of_nonneg]All goals completed! 🐙
  ·e_aQ:HarmonicOscillatorn:ℕx:ℝ⊢ ‖↑(↑(physHermite n) (x / Q.ξ)) * ↑(Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2)))‖ =
  |↑(physHermite n) (x / Q.ξ)| * Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2)) rw [norm_mule_aQ:HarmonicOscillatorn:ℕx:ℝ⊢ ‖↑(↑(physHermite n) (x / Q.ξ))‖ * ‖↑(Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2)))‖ =
  |↑(physHermite n) (x / Q.ξ)| * Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))e_aQ:HarmonicOscillatorn:ℕx:ℝ⊢ ‖↑(↑(physHermite n) (x / Q.ξ))‖ * ‖↑(Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2)))‖ =
  |↑(physHermite n) (x / Q.ξ)| * Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))]e_aQ:HarmonicOscillatorn:ℕx:ℝ⊢ ‖↑(↑(physHermite n) (x / Q.ξ))‖ * ‖↑(Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2)))‖ =
  |↑(physHermite n) (x / Q.ξ)| * Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))
    congr 1e_a.e_aQ:HarmonicOscillatorn:ℕx:ℝ⊢ ‖↑(↑(physHermite n) (x / Q.ξ))‖ = |↑(physHermite n) (x / Q.ξ)|e_a.e_aQ:HarmonicOscillatorn:ℕx:ℝ⊢ ‖↑(Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2)))‖ = Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))
    ·e_a.e_aQ:HarmonicOscillatorn:ℕx:ℝ⊢ ‖↑(↑(physHermite n) (x / Q.ξ))‖ = |↑(physHermite n) (x / Q.ξ)| simpAll goals completed! 🐙
    ·e_a.e_aQ:HarmonicOscillatorn:ℕx:ℝ⊢ ‖↑(Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2)))‖ = Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2)) rw [Complex.norm_reale_a.e_aQ:HarmonicOscillatorn:ℕx:ℝ⊢ ‖Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))‖ = Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))e_a.e_aQ:HarmonicOscillatorn:ℕx:ℝ⊢ ‖Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))‖ = Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))]e_a.e_aQ:HarmonicOscillatorn:ℕx:ℝ⊢ ‖Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))‖ = Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))
      simpAll goals completed! 🐙



lemma eigenfunction_point_norm_sq (n : ℕ) (x : ℝ) :
    ‖Q.eigenfunction n x‖ ^ 2 = (1/√(2 ^ n * n !) * (1/ √(√Real.pi * Q.ξ))) ^ 2 *
    ((physHermite n (x / Q.ξ)) ^ 2 * Real.exp (- x^2 / Q.ξ ^ 2)) := byQ:HarmonicOscillatorn:ℕx:ℝ⊢ ‖Q.eigenfunction n x‖ ^ 2 =
  (1 / √(2 ^ n * ↑n !) * (1 / √(√Real.pi * Q.ξ))) ^ 2 * (↑(physHermite n) (x / Q.ξ) ^ 2 * Real.exp (-x ^ 2 / Q.ξ ^ 2))
  trans (1/√(2 ^ n * n !) * (1/ √(√Real.pi * Q.ξ))) ^ 2 *
    (|physHermite n (x/Q.ξ)| ^ 2 * Real.exp (- x^2 / (2 * Q.ξ ^2)) ^ (2 : ℝ))Q:HarmonicOscillatorn:ℕx:ℝ⊢ ‖Q.eigenfunction n x‖ ^ 2 =
  (1 / √(2 ^ n * ↑n !) * (1 / √(√Real.pi * Q.ξ))) ^ 2 *
    (|↑(physHermite n) (x / Q.ξ)| ^ 2 * Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2)) ^ 2)Q:HarmonicOscillatorn:ℕx:ℝ⊢ (1 / √(2 ^ n * ↑n !) * (1 / √(√Real.pi * Q.ξ))) ^ 2 *
    (|↑(physHermite n) (x / Q.ξ)| ^ 2 * Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2)) ^ 2) =
  (1 / √(2 ^ n * ↑n !) * (1 / √(√Real.pi * Q.ξ))) ^ 2 * (↑(physHermite n) (x / Q.ξ) ^ 2 * Real.exp (-x ^ 2 / Q.ξ ^ 2))
  ·Q:HarmonicOscillatorn:ℕx:ℝ⊢ ‖Q.eigenfunction n x‖ ^ 2 =
  (1 / √(2 ^ n * ↑n !) * (1 / √(√Real.pi * Q.ξ))) ^ 2 *
    (|↑(physHermite n) (x / Q.ξ)| ^ 2 * Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2)) ^ 2) simp only [Real.rpow_two]Q:HarmonicOscillatorn:ℕx:ℝ⊢ ‖Q.eigenfunction n x‖ ^ 2 =
  (1 / √(2 ^ n * ↑n !) * (1 / √(√Real.pi * Q.ξ))) ^ 2 *
    (|↑(physHermite n) (x / Q.ξ)| ^ 2 * Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2)) ^ 2)
    rw [eigenfunction_point_normQ:HarmonicOscillatorn:ℕx:ℝ⊢ (1 / √(2 ^ n * ↑n !) * (1 / √(√Real.pi * Q.ξ)) * (|↑(physHermite n) (x / Q.ξ)| * Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2)))) ^
    2 =
  (1 / √(2 ^ n * ↑n !) * (1 / √(√Real.pi * Q.ξ))) ^ 2 *
    (|↑(physHermite n) (x / Q.ξ)| ^ 2 * Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2)) ^ 2)Q:HarmonicOscillatorn:ℕx:ℝ⊢ (1 / √(2 ^ n * ↑n !) * (1 / √(√Real.pi * Q.ξ)) * (|↑(physHermite n) (x / Q.ξ)| * Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2)))) ^
    2 =
  (1 / √(2 ^ n * ↑n !) * (1 / √(√Real.pi * Q.ξ))) ^ 2 *
    (|↑(physHermite n) (x / Q.ξ)| ^ 2 * Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2)) ^ 2)]Q:HarmonicOscillatorn:ℕx:ℝ⊢ (1 / √(2 ^ n * ↑n !) * (1 / √(√Real.pi * Q.ξ)) * (|↑(physHermite n) (x / Q.ξ)| * Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2)))) ^
    2 =
  (1 / √(2 ^ n * ↑n !) * (1 / √(√Real.pi * Q.ξ))) ^ 2 *
    (|↑(physHermite n) (x / Q.ξ)| ^ 2 * Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2)) ^ 2)
    ringAll goals completed! 🐙
  ·Q:HarmonicOscillatorn:ℕx:ℝ⊢ (1 / √(2 ^ n * ↑n !) * (1 / √(√Real.pi * Q.ξ))) ^ 2 *
    (|↑(physHermite n) (x / Q.ξ)| ^ 2 * Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2)) ^ 2) =
  (1 / √(2 ^ n * ↑n !) * (1 / √(√Real.pi * Q.ξ))) ^ 2 * (↑(physHermite n) (x / Q.ξ) ^ 2 * Real.exp (-x ^ 2 / Q.ξ ^ 2)) congr 2e_a.e_aQ:HarmonicOscillatorn:ℕx:ℝ⊢ |↑(physHermite n) (x / Q.ξ)| ^ 2 = ↑(physHermite n) (x / Q.ξ) ^ 2e_a.e_aQ:HarmonicOscillatorn:ℕx:ℝ⊢ Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2)) ^ 2 = Real.exp (-x ^ 2 / Q.ξ ^ 2)
    ·e_a.e_aQ:HarmonicOscillatorn:ℕx:ℝ⊢ |↑(physHermite n) (x / Q.ξ)| ^ 2 = ↑(physHermite n) (x / Q.ξ) ^ 2 exact sq_abs (physHermite n _)All goals completed! 🐙
    ·e_a.e_aQ:HarmonicOscillatorn:ℕx:ℝ⊢ Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2)) ^ 2 = Real.exp (-x ^ 2 / Q.ξ ^ 2) rw [← Real.exp_mule_a.e_aQ:HarmonicOscillatorn:ℕx:ℝ⊢ Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2) * 2) = Real.exp (-x ^ 2 / Q.ξ ^ 2)e_a.e_aQ:HarmonicOscillatorn:ℕx:ℝ⊢ Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2) * 2) = Real.exp (-x ^ 2 / Q.ξ ^ 2)]e_a.e_aQ:HarmonicOscillatorn:ℕx:ℝ⊢ Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2) * 2) = Real.exp (-x ^ 2 / Q.ξ ^ 2)
      congr 1e_a.e_aQ:HarmonicOscillatorn:ℕx:ℝ⊢ -x ^ 2 / (2 * Q.ξ ^ 2) * 2 = -x ^ 2 / Q.ξ ^ 2
      ringAll goals completed! 🐙

The eigenfunctions are square integrable.


@[fun_prop]
lemma eigenfunction_square_integrable (n : ℕ) :
    MeasureTheory.Integrable (fun x => ‖Q.eigenfunction n x‖ ^ 2) := byQ:HarmonicOscillatorn:ℕ⊢ Integrable (fun x => ‖Q.eigenfunction n x‖ ^ 2) volume
  have h0 (x : ℝ) : Real.exp (- x ^ 2 / Q.ξ^2) =
      Real.exp (- (1 /Q.ξ^2) * x ^ 2) := by
    simp only [neg_mul, Real.exp_eq_exp]Q:HarmonicOscillatorn:ℕx:ℝ⊢ -x ^ 2 / Q.ξ ^ 2 = -(1 / Q.ξ ^ 2 * x ^ 2)Q:HarmonicOscillatorn:ℕh0:∀ (x : ℝ), Real.exp (-x ^ 2 / Q.ξ ^ 2) = Real.exp (-(1 / Q.ξ ^ 2) * x ^ 2)⊢ Integrable (fun x => ‖Q.eigenfunction n x‖ ^ 2) volume
    ringQ:HarmonicOscillatorn:ℕh0:∀ (x : ℝ), Real.exp (-x ^ 2 / Q.ξ ^ 2) = Real.exp (-(1 / Q.ξ ^ 2) * x ^ 2)⊢ Integrable (fun x => ‖Q.eigenfunction n x‖ ^ 2) volumeQ:HarmonicOscillatorn:ℕh0:∀ (x : ℝ), Real.exp (-x ^ 2 / Q.ξ ^ 2) = Real.exp (-(1 / Q.ξ ^ 2) * x ^ 2)⊢ Integrable (fun x => ‖Q.eigenfunction n x‖ ^ 2) volume
  conv =>Q:HarmonicOscillatorn:ℕh0:∀ (x : ℝ), Real.exp (-x ^ 2 / Q.ξ ^ 2) = Real.exp (-(1 / Q.ξ ^ 2) * x ^ 2)| Integrable (fun x => ‖Q.eigenfunction n x‖ ^ 2) volume
    enter [1, x]Q:HarmonicOscillatorn:ℕh0:∀ (x : ℝ), Real.exp (-x ^ 2 / Q.ξ ^ 2) = Real.exp (-(1 / Q.ξ ^ 2) * x ^ 2)x:ℝ| ‖Q.eigenfunction n x‖ ^ 2
    rw [eigenfunction_point_norm_sq]Q:HarmonicOscillatorn:ℕh0:∀ (x : ℝ), Real.exp (-x ^ 2 / Q.ξ ^ 2) = Real.exp (-(1 / Q.ξ ^ 2) * x ^ 2)x:ℝ| (1 / √(2 ^ n * ↑n !) * (1 / √(√Real.pi * Q.ξ))) ^ 2 * (↑(physHermite n) (x / Q.ξ) ^ 2 * Real.exp (-x ^ 2 / Q.ξ ^ 2))
    rw [← map_pow, h0]Q:HarmonicOscillatorn:ℕh0:∀ (x : ℝ), Real.exp (-x ^ 2 / Q.ξ ^ 2) = Real.exp (-(1 / Q.ξ ^ 2) * x ^ 2)x:ℝ| (1 / √(2 ^ n * ↑n !) * (1 / √(√Real.pi * Q.ξ))) ^ 2 *
  ((aeval (x / Q.ξ)) (physHermite n ^ 2) * Real.exp (-(1 / Q.ξ ^ 2) * x ^ 2))
    enter [2, 1, 1, 1]Q:HarmonicOscillatorn:ℕh0:∀ (x : ℝ), Real.exp (-x ^ 2 / Q.ξ ^ 2) = Real.exp (-(1 / Q.ξ ^ 2) * x ^ 2)x:ℝ| x / Q.ξ
    rw [← one_div_mul_eq_div]Q:HarmonicOscillatorn:ℕh0:∀ (x : ℝ), Real.exp (-x ^ 2 / Q.ξ ^ 2) = Real.exp (-(1 / Q.ξ ^ 2) * x ^ 2)x:ℝ| 1 / Q.ξ * x
  apply MeasureTheory.Integrable.const_mulQ:HarmonicOscillatorn:ℕh0:∀ (x : ℝ), Real.exp (-x ^ 2 / Q.ξ ^ 2) = Real.exp (-(1 / Q.ξ ^ 2) * x ^ 2)⊢ Integrable (fun x => (aeval (1 / Q.ξ * x)) (physHermite n ^ 2) * Real.exp (-(1 / Q.ξ ^ 2) * x ^ 2)) volume
  apply guassian_integrable_polynomial_consQ:HarmonicOscillatorn:ℕh0:∀ (x : ℝ), Real.exp (-x ^ 2 / Q.ξ ^ 2) = Real.exp (-(1 / Q.ξ ^ 2) * x ^ 2)⊢ 0 < 1 / Q.ξ ^ 2
  simpAll goals completed! 🐙

The eigenfunctions are almost everywhere strongly measurable.

@[fun_prop]
lemma eigenfunction_aeStronglyMeasurable (n : ℕ) :
    MeasureTheory.AEStronglyMeasurable (Q.eigenfunction n) :=
  (Q.eigenfunction_integrable n).aestronglyMeasurable

The eigenfunctions are members of the Hilbert space.


lemma eigenfunction_memHS (n : ℕ) : MemHS (Q.eigenfunction n) := byQ:HarmonicOscillatorn:ℕ⊢ MemHS (Q.eigenfunction n)
  rw [memHS_iffQ:HarmonicOscillatorn:ℕ⊢ AEStronglyMeasurable (Q.eigenfunction n) volume ∧ Integrable (fun x => ‖Q.eigenfunction n x‖ ^ 2) volumeQ:HarmonicOscillatorn:ℕ⊢ AEStronglyMeasurable (Q.eigenfunction n) volume ∧ Integrable (fun x => ‖Q.eigenfunction n x‖ ^ 2) volume]Q:HarmonicOscillatorn:ℕ⊢ AEStronglyMeasurable (Q.eigenfunction n) volume ∧ Integrable (fun x => ‖Q.eigenfunction n x‖ ^ 2) volume
  apply And.introleftQ:HarmonicOscillatorn:ℕ⊢ AEStronglyMeasurable (Q.eigenfunction n) volumerightQ:HarmonicOscillatorn:ℕ⊢ Integrable (fun x => ‖Q.eigenfunction n x‖ ^ 2) volume <;>leftQ:HarmonicOscillatorn:ℕ⊢ AEStronglyMeasurable (Q.eigenfunction n) volumerightQ:HarmonicOscillatorn:ℕ⊢ Integrable (fun x => ‖Q.eigenfunction n x‖ ^ 2) volume fun_propAll goals completed! 🐙

The eigenfunctions are differentiable.


@[fun_prop]
lemma eigenfunction_differentiableAt (x : ℝ) (n : ℕ) :
    DifferentiableAt ℝ (Q.eigenfunction n) x := byQ:HarmonicOscillatorx:ℝn:ℕ⊢ DifferentiableAt ℝ (Q.eigenfunction n) x
  rw [eigenfunction_eqQ:HarmonicOscillatorx:ℝn:ℕ⊢ DifferentiableAt ℝ
  (fun x =>
    1 / ↑√(2 ^ n * ↑n !) * (1 / ↑√(√Real.pi * Q.ξ)) * ↑(↑(physHermite n) (x / Q.ξ) * Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))))
  xQ:HarmonicOscillatorx:ℝn:ℕ⊢ DifferentiableAt ℝ
  (fun x =>
    1 / ↑√(2 ^ n * ↑n !) * (1 / ↑√(√Real.pi * Q.ξ)) * ↑(↑(physHermite n) (x / Q.ξ) * Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))))
  x]Q:HarmonicOscillatorx:ℝn:ℕ⊢ DifferentiableAt ℝ
  (fun x =>
    1 / ↑√(2 ^ n * ↑n !) * (1 / ↑√(√Real.pi * Q.ξ)) * ↑(↑(physHermite n) (x / Q.ξ) * Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))))
  x
  fun_propAll goals completed! 🐙

The eigenfunctions are continuous.


@[fun_prop]
lemma eigenfunction_continuous (n : ℕ) : Continuous (Q.eigenfunction n) := byQ:HarmonicOscillatorn:ℕ⊢ Continuous (Q.eigenfunction n)
  rw [eigenfunction_eqQ:HarmonicOscillatorn:ℕ⊢ Continuous fun x =>
  1 / ↑√(2 ^ n * ↑n !) * (1 / ↑√(√Real.pi * Q.ξ)) * ↑(↑(physHermite n) (x / Q.ξ) * Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2)))Q:HarmonicOscillatorn:ℕ⊢ Continuous fun x =>
  1 / ↑√(2 ^ n * ↑n !) * (1 / ↑√(√Real.pi * Q.ξ)) * ↑(↑(physHermite n) (x / Q.ξ) * Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2)))]Q:HarmonicOscillatorn:ℕ⊢ Continuous fun x =>
  1 / ↑√(2 ^ n * ↑n !) * (1 / ↑√(√Real.pi * Q.ξ)) * ↑(↑(physHermite n) (x / Q.ξ) * Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2)))
  fun_propAll goals completed! 🐙

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


lemma eigenfunction_parity (n : ℕ) :
    parityOperator (Q.eigenfunction n) = (-1) ^ n * Q.eigenfunction n := byQ:HarmonicOscillatorn:ℕ⊢ parityOperator (Q.eigenfunction n) = (-1) ^ n * Q.eigenfunction n
  funext xQ:HarmonicOscillatorn:ℕx:ℝ⊢ parityOperator (Q.eigenfunction n) x = ((-1) ^ n * Q.eigenfunction n) x
  rw [eigenfunction_eqQ:HarmonicOscillatorn:ℕx:ℝ⊢ parityOperator
    (fun x =>
      1 / ↑√(2 ^ n * ↑n !) * (1 / ↑√(√Real.pi * Q.ξ)) *
        ↑(↑(physHermite n) (x / Q.ξ) * Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))))
    x =
  ((-1) ^ n * fun x =>
      1 / ↑√(2 ^ n * ↑n !) * (1 / ↑√(√Real.pi * Q.ξ)) *
        ↑(↑(physHermite n) (x / Q.ξ) * Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))))
    xQ:HarmonicOscillatorn:ℕx:ℝ⊢ parityOperator
    (fun x =>
      1 / ↑√(2 ^ n * ↑n !) * (1 / ↑√(√Real.pi * Q.ξ)) *
        ↑(↑(physHermite n) (x / Q.ξ) * Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))))
    x =
  ((-1) ^ n * fun x =>
      1 / ↑√(2 ^ n * ↑n !) * (1 / ↑√(√Real.pi * Q.ξ)) *
        ↑(↑(physHermite n) (x / Q.ξ) * Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))))
    x]Q:HarmonicOscillatorn:ℕx:ℝ⊢ parityOperator
    (fun x =>
      1 / ↑√(2 ^ n * ↑n !) * (1 / ↑√(√Real.pi * Q.ξ)) *
        ↑(↑(physHermite n) (x / Q.ξ) * Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))))
    x =
  ((-1) ^ n * fun x =>
      1 / ↑√(2 ^ n * ↑n !) * (1 / ↑√(√Real.pi * Q.ξ)) *
        ↑(↑(physHermite n) (x / Q.ξ) * Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))))
    x
  simp only [parityOperator, LinearMap.coe_mk, AddHom.coe_mk, Pi.mul_apply, Pi.pow_apply,
    Pi.neg_apply, Pi.one_apply]Q:HarmonicOscillatorn:ℕx:ℝ⊢ 1 / ↑√(2 ^ n * ↑n !) * (1 / ↑√(√Real.pi * Q.ξ)) *
    ↑(↑(physHermite n) (-x / Q.ξ) * Real.exp (-(-x) ^ 2 / (2 * Q.ξ ^ 2))) =
  (-1) ^ n *
    (1 / ↑√(2 ^ n * ↑n !) * (1 / ↑√(√Real.pi * Q.ξ)) *
      ↑(↑(physHermite n) (x / Q.ξ) * Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))))
  rw [show -x / Q.ξ = - (x / Q.ξ) byQ:HarmonicOscillatorn:ℕ⊢ parityOperator (Q.eigenfunction n) = (-1) ^ n * Q.eigenfunction nQ:HarmonicOscillatorn:ℕx:ℝ⊢ 1 / ↑√(2 ^ n * ↑n !) * (1 / ↑√(√Real.pi * Q.ξ)) *
    ↑(↑(physHermite n) (-(x / Q.ξ)) * Real.exp (-(-x) ^ 2 / (2 * Q.ξ ^ 2))) =
  (-1) ^ n *
    (1 / ↑√(2 ^ n * ↑n !) * (1 / ↑√(√Real.pi * Q.ξ)) *
      ↑(↑(physHermite n) (x / Q.ξ) * Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2)))) ringAll goals completed! 🐙Q:HarmonicOscillatorn:ℕx:ℝ⊢ 1 / ↑√(2 ^ n * ↑n !) * (1 / ↑√(√Real.pi * Q.ξ)) *
    ↑(↑(physHermite n) (-(x / Q.ξ)) * Real.exp (-(-x) ^ 2 / (2 * Q.ξ ^ 2))) =
  (-1) ^ n *
    (1 / ↑√(2 ^ n * ↑n !) * (1 / ↑√(√Real.pi * Q.ξ)) *
      ↑(↑(physHermite n) (x / Q.ξ) * Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))))]Q:HarmonicOscillatorn:ℕx:ℝ⊢ 1 / ↑√(2 ^ n * ↑n !) * (1 / ↑√(√Real.pi * Q.ξ)) *
    ↑(↑(physHermite n) (-(x / Q.ξ)) * Real.exp (-(-x) ^ 2 / (2 * Q.ξ ^ 2))) =
  (-1) ^ n *
    (1 / ↑√(2 ^ n * ↑n !) * (1 / ↑√(√Real.pi * Q.ξ)) *
      ↑(↑(physHermite n) (x / Q.ξ) * Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))))
  rw [physHermite_negQ:HarmonicOscillatorn:ℕx:ℝ⊢ 1 / ↑√(2 ^ n * ↑n !) * (1 / ↑√(√Real.pi * Q.ξ)) *
    ↑((-1) ^ n * ↑(physHermite n) (x / Q.ξ) * Real.exp (-(-x) ^ 2 / (2 * Q.ξ ^ 2))) =
  (-1) ^ n *
    (1 / ↑√(2 ^ n * ↑n !) * (1 / ↑√(√Real.pi * Q.ξ)) *
      ↑(↑(physHermite n) (x / Q.ξ) * Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))))Q:HarmonicOscillatorn:ℕx:ℝ⊢ 1 / ↑√(2 ^ n * ↑n !) * (1 / ↑√(√Real.pi * Q.ξ)) *
    ↑((-1) ^ n * ↑(physHermite n) (x / Q.ξ) * Real.exp (-(-x) ^ 2 / (2 * Q.ξ ^ 2))) =
  (-1) ^ n *
    (1 / ↑√(2 ^ n * ↑n !) * (1 / ↑√(√Real.pi * Q.ξ)) *
      ↑(↑(physHermite n) (x / Q.ξ) * Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))))]Q:HarmonicOscillatorn:ℕx:ℝ⊢ 1 / ↑√(2 ^ n * ↑n !) * (1 / ↑√(√Real.pi * Q.ξ)) *
    ↑((-1) ^ n * ↑(physHermite n) (x / Q.ξ) * Real.exp (-(-x) ^ 2 / (2 * Q.ξ ^ 2))) =
  (-1) ^ n *
    (1 / ↑√(2 ^ n * ↑n !) * (1 / ↑√(√Real.pi * Q.ξ)) *
      ↑(↑(physHermite n) (x / Q.ξ) * Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))))
  simp only [Complex.ofReal_mul, Complex.ofReal_pow, Complex.ofReal_neg, Complex.ofReal_one]Q:HarmonicOscillatorn:ℕx:ℝ⊢ 1 / ↑√(2 ^ n * ↑n !) * (1 / ↑√(√Real.pi * Q.ξ)) *
    ((-1) ^ n * ↑(↑(physHermite n) (x / Q.ξ)) * ↑(Real.exp (-(-x) ^ 2 / (2 * Q.ξ ^ 2)))) =
  (-1) ^ n *
    (1 / ↑√(2 ^ n * ↑n !) * (1 / ↑√(√Real.pi * Q.ξ)) *
      (↑(↑(physHermite n) (x / Q.ξ)) * ↑(Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2)))))
  ring_nfAll goals completed! 🐙

Orthonormality

A simplification of the product of two eigenfunctions.


lemma eigenfunction_mul (n p : ℕ) :
    (Q.eigenfunction n x) * (Q.eigenfunction p x) =
    1/√(2 ^ n * n !) * 1/√(2 ^ p * p !) * (1/ (√Real.pi * Q.ξ)) * Complex.ofReal
    (physHermite n (x / Q.ξ) * physHermite p (x / Q.ξ) * Real.exp (- x^2 / Q.ξ^2)) := byQ:HarmonicOscillatorx:ℝn:ℕp:ℕ⊢ Q.eigenfunction n x * Q.eigenfunction p x =
  1 / ↑√(2 ^ n * ↑n !) * 1 / ↑√(2 ^ p * ↑p !) * (1 / (↑√Real.pi * ↑Q.ξ)) *
    ↑(↑(physHermite n) (x / Q.ξ) * ↑(physHermite p) (x / Q.ξ) * Real.exp (-x ^ 2 / Q.ξ ^ 2))
  calc Q.eigenfunction n x * Q.eigenfunction p x
    _ = (1/√(2 ^ n * n !) * 1/√(2 ^ p * p !)) * ((1/ ((√(√Real.pi * Q.ξ)) * √(√Real.pi * Q.ξ)))) *
        (physHermite n (x/Q.ξ) * physHermite p (x/Q.ξ)) *
        (Real.exp (- x^2 / (2 * Q.ξ^2)) * Real.exp (- x^2 / (2 * Q.ξ^2))) := byQ:HarmonicOscillatorx:ℝn:ℕp:ℕ⊢ Q.eigenfunction n x * Q.eigenfunction p x =
  1 / ↑√(2 ^ n * ↑n !) * 1 / ↑√(2 ^ p * ↑p !) * (1 / (↑√(√Real.pi * Q.ξ) * ↑√(√Real.pi * Q.ξ))) *
      (↑(↑(physHermite n) (x / Q.ξ)) * ↑(↑(physHermite p) (x / Q.ξ))) *
    (↑(Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))) * ↑(Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))))
      simp only [eigenfunction, ofNat_nonneg, pow_nonneg, Real.sqrt_mul, Complex.ofReal_mul,
        one_div, mul_inv_rev, Complex.ofReal_exp, Complex.ofReal_div, Complex.ofReal_neg,
        Complex.ofReal_pow, Complex.ofReal_ofNat, mul_one]Q:HarmonicOscillatorx:ℝn:ℕp:ℕ⊢ (↑√↑n !)⁻¹ * (↑√(2 ^ n))⁻¹ * (↑√(√Real.pi * Q.ξ))⁻¹ * ↑(↑(physHermite n) (x / Q.ξ)) *
      Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2)) *
    ((↑√↑p !)⁻¹ * (↑√(2 ^ p))⁻¹ * (↑√(√Real.pi * Q.ξ))⁻¹ * ↑(↑(physHermite p) (x / Q.ξ)) *
      Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))) =
  (↑√↑n !)⁻¹ * (↑√(2 ^ n))⁻¹ / (↑√(2 ^ p) * ↑√↑p !) * ((↑√(√Real.pi * Q.ξ))⁻¹ * (↑√(√Real.pi * Q.ξ))⁻¹) *
      (↑(↑(physHermite n) (x / Q.ξ)) * ↑(↑(physHermite p) (x / Q.ξ))) *
    (Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2)) * Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2)))
      ringAll goals completed! 🐙
    _ = (1/√(2 ^ n * n !) * 1/√(2 ^ p * p !)) * (1/ (√Real.pi * Q.ξ)) *
        (physHermite n (x / Q.ξ) * physHermite p (x / Q.ξ)) * (Real.exp (- x^2 / Q.ξ^2)) := byQ:HarmonicOscillatorx:ℝn:ℕp:ℕ⊢ 1 / ↑√(2 ^ n * ↑n !) * 1 / ↑√(2 ^ p * ↑p !) * (1 / (↑√(√Real.pi * Q.ξ) * ↑√(√Real.pi * Q.ξ))) *
      (↑(↑(physHermite n) (x / Q.ξ)) * ↑(↑(physHermite p) (x / Q.ξ))) *
    (↑(Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))) * ↑(Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2)))) =
  1 / ↑√(2 ^ n * ↑n !) * 1 / ↑√(2 ^ p * ↑p !) * (1 / (↑√Real.pi * ↑Q.ξ)) *
      (↑(↑(physHermite n) (x / Q.ξ)) * ↑(↑(physHermite p) (x / Q.ξ))) *
    ↑(Real.exp (-x ^ 2 / Q.ξ ^ 2))
      congr 1e_aQ:HarmonicOscillatorx:ℝn:ℕp:ℕ⊢ 1 / ↑√(2 ^ n * ↑n !) * 1 / ↑√(2 ^ p * ↑p !) * (1 / (↑√(√Real.pi * Q.ξ) * ↑√(√Real.pi * Q.ξ))) *
    (↑(↑(physHermite n) (x / Q.ξ)) * ↑(↑(physHermite p) (x / Q.ξ))) =
  1 / ↑√(2 ^ n * ↑n !) * 1 / ↑√(2 ^ p * ↑p !) * (1 / (↑√Real.pi * ↑Q.ξ)) *
    (↑(↑(physHermite n) (x / Q.ξ)) * ↑(↑(physHermite p) (x / Q.ξ)))e_aQ:HarmonicOscillatorx:ℝn:ℕp:ℕ⊢ ↑(Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))) * ↑(Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))) = ↑(Real.exp (-x ^ 2 / Q.ξ ^ 2))
      ·e_aQ:HarmonicOscillatorx:ℝn:ℕp:ℕ⊢ 1 / ↑√(2 ^ n * ↑n !) * 1 / ↑√(2 ^ p * ↑p !) * (1 / (↑√(√Real.pi * Q.ξ) * ↑√(√Real.pi * Q.ξ))) *
    (↑(↑(physHermite n) (x / Q.ξ)) * ↑(↑(physHermite p) (x / Q.ξ))) =
  1 / ↑√(2 ^ n * ↑n !) * 1 / ↑√(2 ^ p * ↑p !) * (1 / (↑√Real.pi * ↑Q.ξ)) *
    (↑(↑(physHermite n) (x / Q.ξ)) * ↑(↑(physHermite p) (x / Q.ξ))) congr 1e_a.e_aQ:HarmonicOscillatorx:ℝn:ℕp:ℕ⊢ 1 / ↑√(2 ^ n * ↑n !) * 1 / ↑√(2 ^ p * ↑p !) * (1 / (↑√(√Real.pi * Q.ξ) * ↑√(√Real.pi * Q.ξ))) =
  1 / ↑√(2 ^ n * ↑n !) * 1 / ↑√(2 ^ p * ↑p !) * (1 / (↑√Real.pi * ↑Q.ξ))
        ·e_a.e_aQ:HarmonicOscillatorx:ℝn:ℕp:ℕ⊢ 1 / ↑√(2 ^ n * ↑n !) * 1 / ↑√(2 ^ p * ↑p !) * (1 / (↑√(√Real.pi * Q.ξ) * ↑√(√Real.pi * Q.ξ))) =
  1 / ↑√(2 ^ n * ↑n !) * 1 / ↑√(2 ^ p * ↑p !) * (1 / (↑√Real.pi * ↑Q.ξ)) congr 1e_a.e_a.e_aQ:HarmonicOscillatorx:ℝn:ℕp:ℕ⊢ 1 / (↑√(√Real.pi * Q.ξ) * ↑√(√Real.pi * Q.ξ)) = 1 / (↑√Real.pi * ↑Q.ξ)
          ·e_a.e_a.e_aQ:HarmonicOscillatorx:ℝn:ℕp:ℕ⊢ 1 / (↑√(√Real.pi * Q.ξ) * ↑√(√Real.pi * Q.ξ)) = 1 / (↑√Real.pi * ↑Q.ξ) congr 1e_a.e_a.e_a.e_aQ:HarmonicOscillatorx:ℝn:ℕp:ℕ⊢ ↑√(√Real.pi * Q.ξ) * ↑√(√Real.pi * Q.ξ) = ↑√Real.pi * ↑Q.ξ
            rw [← Complex.ofReal_mul,e_a.e_a.e_a.e_aQ:HarmonicOscillatorx:ℝn:ℕp:ℕ⊢ ↑(√(√Real.pi * Q.ξ) * √(√Real.pi * Q.ξ)) = ↑√Real.pi * ↑Q.ξe_a.e_a.e_a.e_aQ:HarmonicOscillatorx:ℝn:ℕp:ℕ⊢ ↑(√Real.pi * Q.ξ) = ↑√Real.pi * ↑Q.ξe_a.e_a.e_a.e_aQ:HarmonicOscillatorx:ℝn:ℕp:ℕ⊢ 0 ≤ √Real.pi * Q.ξ Real.mul_self_sqrte_a.e_a.e_a.e_aQ:HarmonicOscillatorx:ℝn:ℕp:ℕ⊢ ↑(√Real.pi * Q.ξ) = ↑√Real.pi * ↑Q.ξe_a.e_a.e_a.e_aQ:HarmonicOscillatorx:ℝn:ℕp:ℕ⊢ 0 ≤ √Real.pi * Q.ξe_a.e_a.e_a.e_aQ:HarmonicOscillatorx:ℝn:ℕp:ℕ⊢ ↑(√Real.pi * Q.ξ) = ↑√Real.pi * ↑Q.ξe_a.e_a.e_a.e_aQ:HarmonicOscillatorx:ℝn:ℕp:ℕ⊢ 0 ≤ √Real.pi * Q.ξ]e_a.e_a.e_a.e_aQ:HarmonicOscillatorx:ℝn:ℕp:ℕ⊢ ↑(√Real.pi * Q.ξ) = ↑√Real.pi * ↑Q.ξe_a.e_a.e_a.e_aQ:HarmonicOscillatorx:ℝn:ℕp:ℕ⊢ 0 ≤ √Real.pi * Q.ξ
            ·e_a.e_a.e_a.e_aQ:HarmonicOscillatorx:ℝn:ℕp:ℕ⊢ ↑(√Real.pi * Q.ξ) = ↑√Real.pi * ↑Q.ξ simpAll goals completed! 🐙
            ·e_a.e_a.e_a.e_aQ:HarmonicOscillatorx:ℝn:ℕp:ℕ⊢ 0 ≤ √Real.pi * Q.ξ simpAll goals completed! 🐙
      ·e_aQ:HarmonicOscillatorx:ℝn:ℕp:ℕ⊢ ↑(Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))) * ↑(Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))) = ↑(Real.exp (-x ^ 2 / Q.ξ ^ 2)) rw [← Complex.ofReal_mule_aQ:HarmonicOscillatorx:ℝn:ℕp:ℕ⊢ ↑(Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2)) * Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))) = ↑(Real.exp (-x ^ 2 / Q.ξ ^ 2))e_aQ:HarmonicOscillatorx:ℝn:ℕp:ℕ⊢ ↑(Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2)) * Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))) = ↑(Real.exp (-x ^ 2 / Q.ξ ^ 2))]e_aQ:HarmonicOscillatorx:ℝn:ℕp:ℕ⊢ ↑(Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2)) * Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))) = ↑(Real.exp (-x ^ 2 / Q.ξ ^ 2))
        congre_aQ:HarmonicOscillatorx:ℝn:ℕp:ℕ⊢ Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2)) * Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2)) = Real.exp (-x ^ 2 / Q.ξ ^ 2)
        rw [← Real.exp_adde_aQ:HarmonicOscillatorx:ℝn:ℕp:ℕ⊢ Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2) + -x ^ 2 / (2 * Q.ξ ^ 2)) = Real.exp (-x ^ 2 / Q.ξ ^ 2)e_aQ:HarmonicOscillatorx:ℝn:ℕp:ℕ⊢ Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2) + -x ^ 2 / (2 * Q.ξ ^ 2)) = Real.exp (-x ^ 2 / Q.ξ ^ 2)]e_aQ:HarmonicOscillatorx:ℝn:ℕp:ℕ⊢ Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2) + -x ^ 2 / (2 * Q.ξ ^ 2)) = Real.exp (-x ^ 2 / Q.ξ ^ 2)
        simp only [Real.exp_eq_exp]e_aQ:HarmonicOscillatorx:ℝn:ℕp:ℕ⊢ -x ^ 2 / (2 * Q.ξ ^ 2) + -x ^ 2 / (2 * Q.ξ ^ 2) = -x ^ 2 / Q.ξ ^ 2
        field_simpe_aQ:HarmonicOscillatorx:ℝn:ℕp:ℕ⊢ x ^ 2 * (-1 + -1) = -(x ^ 2 * 2)
        ringAll goals completed! 🐙
  simp only [ofNat_nonneg, pow_nonneg, Real.sqrt_mul, Complex.ofReal_mul, one_div, mul_inv_rev,
    mul_one, Complex.ofReal_exp, Complex.ofReal_div, Complex.ofReal_neg,
    Complex.ofReal_pow]calc.stepQ:HarmonicOscillatorx:ℝn:ℕp:ℕ⊢ (↑√↑n !)⁻¹ * (↑√(2 ^ n))⁻¹ / (↑√(2 ^ p) * ↑√↑p !) * ((↑Q.ξ)⁻¹ * (↑√Real.pi)⁻¹) *
      (↑(↑(physHermite n) (x / Q.ξ)) * ↑(↑(physHermite p) (x / Q.ξ))) *
    Complex.exp (-↑x ^ 2 / ↑Q.ξ ^ 2) =
  (↑√↑n !)⁻¹ * (↑√(2 ^ n))⁻¹ / (↑√(2 ^ p) * ↑√↑p !) * ((↑Q.ξ)⁻¹ * (↑√Real.pi)⁻¹) *
    (↑(↑(physHermite n) (x / Q.ξ)) * ↑(↑(physHermite p) (x / Q.ξ)) * Complex.exp (-↑x ^ 2 / ↑Q.ξ ^ 2))
  ringAll goals completed! 🐙



lemma eigenfunction_mul_self (n : ℕ) : (Q.eigenfunction n x) * (Q.eigenfunction n x) =
    (1/ (2 ^ n * n !) * (1/ (√Real.pi * Q.ξ))) *
    Complex.ofReal ((physHermite n (x / Q.ξ))^2 * Real.exp (- x^2 / Q.ξ^2)) := byQ:HarmonicOscillatorx:ℝn:ℕ⊢ Q.eigenfunction n x * Q.eigenfunction n x =
  1 / (2 ^ n * ↑n !) * (1 / (↑√Real.pi * ↑Q.ξ)) * ↑(↑(physHermite n) (x / Q.ξ) ^ 2 * Real.exp (-x ^ 2 / Q.ξ ^ 2))
  rw [eigenfunction_mulQ:HarmonicOscillatorx:ℝn:ℕ⊢ 1 / ↑√(2 ^ n * ↑n !) * 1 / ↑√(2 ^ n * ↑n !) * (1 / (↑√Real.pi * ↑Q.ξ)) *
    ↑(↑(physHermite n) (x / Q.ξ) * ↑(physHermite n) (x / Q.ξ) * Real.exp (-x ^ 2 / Q.ξ ^ 2)) =
  1 / (2 ^ n * ↑n !) * (1 / (↑√Real.pi * ↑Q.ξ)) * ↑(↑(physHermite n) (x / Q.ξ) ^ 2 * Real.exp (-x ^ 2 / Q.ξ ^ 2))Q:HarmonicOscillatorx:ℝn:ℕ⊢ 1 / ↑√(2 ^ n * ↑n !) * 1 / ↑√(2 ^ n * ↑n !) * (1 / (↑√Real.pi * ↑Q.ξ)) *
    ↑(↑(physHermite n) (x / Q.ξ) * ↑(physHermite n) (x / Q.ξ) * Real.exp (-x ^ 2 / Q.ξ ^ 2)) =
  1 / (2 ^ n * ↑n !) * (1 / (↑√Real.pi * ↑Q.ξ)) * ↑(↑(physHermite n) (x / Q.ξ) ^ 2 * Real.exp (-x ^ 2 / Q.ξ ^ 2))]Q:HarmonicOscillatorx:ℝn:ℕ⊢ 1 / ↑√(2 ^ n * ↑n !) * 1 / ↑√(2 ^ n * ↑n !) * (1 / (↑√Real.pi * ↑Q.ξ)) *
    ↑(↑(physHermite n) (x / Q.ξ) * ↑(physHermite n) (x / Q.ξ) * Real.exp (-x ^ 2 / Q.ξ ^ 2)) =
  1 / (2 ^ n * ↑n !) * (1 / (↑√Real.pi * ↑Q.ξ)) * ↑(↑(physHermite n) (x / Q.ξ) ^ 2 * Real.exp (-x ^ 2 / Q.ξ ^ 2))
  congr 2e_a.e_aQ:HarmonicOscillatorx:ℝn:ℕ⊢ 1 / ↑√(2 ^ n * ↑n !) * 1 / ↑√(2 ^ n * ↑n !) = 1 / (2 ^ n * ↑n !)e_aQ:HarmonicOscillatorx:ℝn:ℕ⊢ ↑(physHermite n) (x / Q.ξ) * ↑(physHermite n) (x / Q.ξ) * Real.exp (-x ^ 2 / Q.ξ ^ 2) =
  ↑(physHermite n) (x / Q.ξ) ^ 2 * Real.exp (-x ^ 2 / Q.ξ ^ 2)
  ·e_a.e_aQ:HarmonicOscillatorx:ℝn:ℕ⊢ 1 / ↑√(2 ^ n * ↑n !) * 1 / ↑√(2 ^ n * ↑n !) = 1 / (2 ^ n * ↑n !) trans 1 / ↑(√(2 ^ n * ↑n !) * ↑√(2 ^ n * ↑n !))Q:HarmonicOscillatorx:ℝn:ℕ⊢ 1 / ↑√(2 ^ n * ↑n !) * 1 / ↑√(2 ^ n * ↑n !) = 1 / ↑(√(2 ^ n * ↑n !) * √(2 ^ n * ↑n !))Q:HarmonicOscillatorx:ℝn:ℕ⊢ 1 / ↑(√(2 ^ n * ↑n !) * √(2 ^ n * ↑n !)) = 1 / (2 ^ n * ↑n !)
    ·Q:HarmonicOscillatorx:ℝn:ℕ⊢ 1 / ↑√(2 ^ n * ↑n !) * 1 / ↑√(2 ^ n * ↑n !) = 1 / ↑(√(2 ^ n * ↑n !) * √(2 ^ n * ↑n !)) simp only [ofNat_nonneg, pow_nonneg, Real.sqrt_mul, Complex.ofReal_mul, one_div, mul_inv_rev,
      mul_one]Q:HarmonicOscillatorx:ℝn:ℕ⊢ (↑√↑n !)⁻¹ * (↑√(2 ^ n))⁻¹ / (↑√(2 ^ n) * ↑√↑n !) = (↑√↑n !)⁻¹ * (↑√(2 ^ n))⁻¹ * ((↑√↑n !)⁻¹ * (↑√(2 ^ n))⁻¹)
      field_simpAll goals completed! 🐙
    congre_aQ:HarmonicOscillatorx:ℝn:ℕ⊢ ↑(√(2 ^ n * ↑n !) * √(2 ^ n * ↑n !)) = 2 ^ n * ↑n !
    trans Complex.ofReal ((2 ^ n * ↑n !))Q:HarmonicOscillatorx:ℝn:ℕ⊢ ↑(√(2 ^ n * ↑n !) * √(2 ^ n * ↑n !)) = ↑(2 ^ n * ↑n !)Q:HarmonicOscillatorx:ℝn:ℕ⊢ ↑(2 ^ n * ↑n !) = 2 ^ n * ↑n !
    ·Q:HarmonicOscillatorx:ℝn:ℕ⊢ ↑(√(2 ^ n * ↑n !) * √(2 ^ n * ↑n !)) = ↑(2 ^ n * ↑n !) congr 1Q:HarmonicOscillatorx:ℝn:ℕ⊢ √(2 ^ n * ↑n !) * √(2 ^ n * ↑n !) = 2 ^ n * ↑n !
      refine Real.mul_self_sqrt ?_Q:HarmonicOscillatorx:ℝn:ℕ⊢ 0 ≤ 2 ^ n * ↑n !
      refine Left.mul_nonneg ?_ (cast_nonneg' n !)Q:HarmonicOscillatorx:ℝn:ℕ⊢ 0 ≤ 2 ^ n
      refine pow_nonneg ?_ nQ:HarmonicOscillatorx:ℝn:ℕ⊢ 0 ≤ 2
      simp only [ofNat_nonneg]All goals completed! 🐙
    ·Q:HarmonicOscillatorx:ℝn:ℕ⊢ ↑(2 ^ n * ↑n !) = 2 ^ n * ↑n ! simpAll goals completed! 🐙
  ·e_aQ:HarmonicOscillatorx:ℝn:ℕ⊢ ↑(physHermite n) (x / Q.ξ) * ↑(physHermite n) (x / Q.ξ) * Real.exp (-x ^ 2 / Q.ξ ^ 2) =
  ↑(physHermite n) (x / Q.ξ) ^ 2 * Real.exp (-x ^ 2 / Q.ξ ^ 2) congr 1e_a.e_aQ:HarmonicOscillatorx:ℝn:ℕ⊢ ↑(physHermite n) (x / Q.ξ) * ↑(physHermite n) (x / Q.ξ) = ↑(physHermite n) (x / Q.ξ) ^ 2
    exact (pow_two ((fun x => (Polynomial.aeval x) (physHermite n)) (x / Q.ξ))).symmAll goals completed! 🐙

The eigenfunction are normalized.


lemma eigenfunction_normalized (n : ℕ) : ⟪HilbertSpace.mk (Q.eigenfunction_memHS n),
    HilbertSpace.mk (Q.eigenfunction_memHS n)⟫_ℂ = 1 := byQ:HarmonicOscillatorn:ℕ⊢ ⟪HilbertSpace.mk ⋯, HilbertSpace.mk ⋯⟫_ℂ = 1
  rw [inner_mk_mkQ:HarmonicOscillatorn:ℕ⊢ ∫ (x : ℝ), (starRingEnd ℂ) (Q.eigenfunction n x) * Q.eigenfunction n x = 1Q:HarmonicOscillatorn:ℕ⊢ ∫ (x : ℝ), (starRingEnd ℂ) (Q.eigenfunction n x) * Q.eigenfunction n x = 1]Q:HarmonicOscillatorn:ℕ⊢ ∫ (x : ℝ), (starRingEnd ℂ) (Q.eigenfunction n x) * Q.eigenfunction n x = 1
  conv_lhs =>
    enter [2, x]Q:HarmonicOscillatorn:ℕx:ℝ| (starRingEnd ℂ) (Q.eigenfunction n x) * Q.eigenfunction n x
    rw [eigenfunction_conj, Q.eigenfunction_mul_self]Q:HarmonicOscillatorn:ℕx:ℝ| 1 / (2 ^ n * ↑n !) * (1 / (↑√Real.pi * ↑Q.ξ)) * ↑(↑(physHermite n) (x / Q.ξ) ^ 2 * Real.exp (-x ^ 2 / Q.ξ ^ 2))
  rw [MeasureTheory.integral_const_mul,Q:HarmonicOscillatorn:ℕ⊢ 1 / (2 ^ n * ↑n !) * (1 / (↑√Real.pi * ↑Q.ξ)) *
    ∫ (a : ℝ), ↑(↑(physHermite n) (a / Q.ξ) ^ 2 * Real.exp (-a ^ 2 / Q.ξ ^ 2)) =
  1Q:HarmonicOscillatorn:ℕ⊢ 1 / (2 ^ n * ↑n !) * (1 / (↑√Real.pi * ↑Q.ξ)) *
    ↑(∫ (x : ℝ), ↑(physHermite n) (x / Q.ξ) ^ 2 * Real.exp (-x ^ 2 / Q.ξ ^ 2)) =
  1 integral_complex_ofRealQ:HarmonicOscillatorn:ℕ⊢ 1 / (2 ^ n * ↑n !) * (1 / (↑√Real.pi * ↑Q.ξ)) *
    ↑(∫ (x : ℝ), ↑(physHermite n) (x / Q.ξ) ^ 2 * Real.exp (-x ^ 2 / Q.ξ ^ 2)) =
  1Q:HarmonicOscillatorn:ℕ⊢ 1 / (2 ^ n * ↑n !) * (1 / (↑√Real.pi * ↑Q.ξ)) *
    ↑(∫ (x : ℝ), ↑(physHermite n) (x / Q.ξ) ^ 2 * Real.exp (-x ^ 2 / Q.ξ ^ 2)) =
  1]Q:HarmonicOscillatorn:ℕ⊢ 1 / (2 ^ n * ↑n !) * (1 / (↑√Real.pi * ↑Q.ξ)) *
    ↑(∫ (x : ℝ), ↑(physHermite n) (x / Q.ξ) ^ 2 * Real.exp (-x ^ 2 / Q.ξ ^ 2)) =
  1
  have hc : (∫ (x : ℝ), physHermite n (x /Q.ξ) ^ 2 * Real.exp (- x ^ 2 / Q.ξ^2))
      = ∫ (x : ℝ), (physHermite n (1/Q.ξ * x) *
      physHermite n (1/Q.ξ * x)) * Real.exp (- (1/Q.ξ)^2 * x ^ 2) := byQ:HarmonicOscillatorn:ℕ⊢ ⟪HilbertSpace.mk ⋯, HilbertSpace.mk ⋯⟫_ℂ = 1Q:HarmonicOscillatorn:ℕhc:∫ (x : ℝ), ↑(physHermite n) (x / Q.ξ) ^ 2 * Real.exp (-x ^ 2 / Q.ξ ^ 2) =
  ∫ (x : ℝ), ↑(physHermite n) (1 / Q.ξ * x) * ↑(physHermite n) (1 / Q.ξ * x) * Real.exp (-(1 / Q.ξ) ^ 2 * x ^ 2)⊢ 1 / (2 ^ n * ↑n !) * (1 / (↑√Real.pi * ↑Q.ξ)) *
    ↑(∫ (x : ℝ), ↑(physHermite n) (x / Q.ξ) ^ 2 * Real.exp (-x ^ 2 / Q.ξ ^ 2)) =
  1
    congre_fQ:HarmonicOscillatorn:ℕ⊢ (fun x => ↑(physHermite n) (x / Q.ξ) ^ 2 * Real.exp (-x ^ 2 / Q.ξ ^ 2)) = fun x =>
  ↑(physHermite n) (1 / Q.ξ * x) * ↑(physHermite n) (1 / Q.ξ * x) * Real.exp (-(1 / Q.ξ) ^ 2 * x ^ 2)Q:HarmonicOscillatorn:ℕhc:∫ (x : ℝ), ↑(physHermite n) (x / Q.ξ) ^ 2 * Real.exp (-x ^ 2 / Q.ξ ^ 2) =
  ∫ (x : ℝ), ↑(physHermite n) (1 / Q.ξ * x) * ↑(physHermite n) (1 / Q.ξ * x) * Real.exp (-(1 / Q.ξ) ^ 2 * x ^ 2)⊢ 1 / (2 ^ n * ↑n !) * (1 / (↑√Real.pi * ↑Q.ξ)) *
    ↑(∫ (x : ℝ), ↑(physHermite n) (x / Q.ξ) ^ 2 * Real.exp (-x ^ 2 / Q.ξ ^ 2)) =
  1
    funext xe_fQ:HarmonicOscillatorn:ℕx:ℝ⊢ ↑(physHermite n) (x / Q.ξ) ^ 2 * Real.exp (-x ^ 2 / Q.ξ ^ 2) =
  ↑(physHermite n) (1 / Q.ξ * x) * ↑(physHermite n) (1 / Q.ξ * x) * Real.exp (-(1 / Q.ξ) ^ 2 * x ^ 2)Q:HarmonicOscillatorn:ℕhc:∫ (x : ℝ), ↑(physHermite n) (x / Q.ξ) ^ 2 * Real.exp (-x ^ 2 / Q.ξ ^ 2) =
  ∫ (x : ℝ), ↑(physHermite n) (1 / Q.ξ * x) * ↑(physHermite n) (1 / Q.ξ * x) * Real.exp (-(1 / Q.ξ) ^ 2 * x ^ 2)⊢ 1 / (2 ^ n * ↑n !) * (1 / (↑√Real.pi * ↑Q.ξ)) *
    ↑(∫ (x : ℝ), ↑(physHermite n) (x / Q.ξ) ^ 2 * Real.exp (-x ^ 2 / Q.ξ ^ 2)) =
  1
    ring_nfQ:HarmonicOscillatorn:ℕhc:∫ (x : ℝ), ↑(physHermite n) (x / Q.ξ) ^ 2 * Real.exp (-x ^ 2 / Q.ξ ^ 2) =
  ∫ (x : ℝ), ↑(physHermite n) (1 / Q.ξ * x) * ↑(physHermite n) (1 / Q.ξ * x) * Real.exp (-(1 / Q.ξ) ^ 2 * x ^ 2)⊢ 1 / (2 ^ n * ↑n !) * (1 / (↑√Real.pi * ↑Q.ξ)) *
    ↑(∫ (x : ℝ), ↑(physHermite n) (x / Q.ξ) ^ 2 * Real.exp (-x ^ 2 / Q.ξ ^ 2)) =
  1Q:HarmonicOscillatorn:ℕhc:∫ (x : ℝ), ↑(physHermite n) (x / Q.ξ) ^ 2 * Real.exp (-x ^ 2 / Q.ξ ^ 2) =
  ∫ (x : ℝ), ↑(physHermite n) (1 / Q.ξ * x) * ↑(physHermite n) (1 / Q.ξ * x) * Real.exp (-(1 / Q.ξ) ^ 2 * x ^ 2)⊢ 1 / (2 ^ n * ↑n !) * (1 / (↑√Real.pi * ↑Q.ξ)) *
    ↑(∫ (x : ℝ), ↑(physHermite n) (x / Q.ξ) ^ 2 * Real.exp (-x ^ 2 / Q.ξ ^ 2)) =
  1
  rw [hc,Q:HarmonicOscillatorn:ℕhc:∫ (x : ℝ), ↑(physHermite n) (x / Q.ξ) ^ 2 * Real.exp (-x ^ 2 / Q.ξ ^ 2) =
  ∫ (x : ℝ), ↑(physHermite n) (1 / Q.ξ * x) * ↑(physHermite n) (1 / Q.ξ * x) * Real.exp (-(1 / Q.ξ) ^ 2 * x ^ 2)⊢ 1 / (2 ^ n * ↑n !) * (1 / (↑√Real.pi * ↑Q.ξ)) *
    ↑(∫ (x : ℝ), ↑(physHermite n) (1 / Q.ξ * x) * ↑(physHermite n) (1 / Q.ξ * x) * Real.exp (-(1 / Q.ξ) ^ 2 * x ^ 2)) =
  1Q:HarmonicOscillatorn:ℕhc:∫ (x : ℝ), ↑(physHermite n) (x / Q.ξ) ^ 2 * Real.exp (-x ^ 2 / Q.ξ ^ 2) =
  ∫ (x : ℝ), ↑(physHermite n) (1 / Q.ξ * x) * ↑(physHermite n) (1 / Q.ξ * x) * Real.exp (-(1 / Q.ξ) ^ 2 * x ^ 2)⊢ 1 / (2 ^ n * ↑n !) * (1 / (↑√Real.pi * ↑Q.ξ)) * ↑(|(1 / Q.ξ)⁻¹| • (↑n ! * 2 ^ n * √Real.pi)) = 1 physHermite_norm_consQ:HarmonicOscillatorn:ℕhc:∫ (x : ℝ), ↑(physHermite n) (x / Q.ξ) ^ 2 * Real.exp (-x ^ 2 / Q.ξ ^ 2) =
  ∫ (x : ℝ), ↑(physHermite n) (1 / Q.ξ * x) * ↑(physHermite n) (1 / Q.ξ * x) * Real.exp (-(1 / Q.ξ) ^ 2 * x ^ 2)⊢ 1 / (2 ^ n * ↑n !) * (1 / (↑√Real.pi * ↑Q.ξ)) * ↑(|(1 / Q.ξ)⁻¹| • (↑n ! * 2 ^ n * √Real.pi)) = 1Q:HarmonicOscillatorn:ℕhc:∫ (x : ℝ), ↑(physHermite n) (x / Q.ξ) ^ 2 * Real.exp (-x ^ 2 / Q.ξ ^ 2) =
  ∫ (x : ℝ), ↑(physHermite n) (1 / Q.ξ * x) * ↑(physHermite n) (1 / Q.ξ * x) * Real.exp (-(1 / Q.ξ) ^ 2 * x ^ 2)⊢ 1 / (2 ^ n * ↑n !) * (1 / (↑√Real.pi * ↑Q.ξ)) * ↑(|(1 / Q.ξ)⁻¹| • (↑n ! * 2 ^ n * √Real.pi)) = 1]Q:HarmonicOscillatorn:ℕhc:∫ (x : ℝ), ↑(physHermite n) (x / Q.ξ) ^ 2 * Real.exp (-x ^ 2 / Q.ξ ^ 2) =
  ∫ (x : ℝ), ↑(physHermite n) (1 / Q.ξ * x) * ↑(physHermite n) (1 / Q.ξ * x) * Real.exp (-(1 / Q.ξ) ^ 2 * x ^ 2)⊢ 1 / (2 ^ n * ↑n !) * (1 / (↑√Real.pi * ↑Q.ξ)) * ↑(|(1 / Q.ξ)⁻¹| • (↑n ! * 2 ^ n * √Real.pi)) = 1
  simp only [one_div, mul_inv_rev, inv_inv, ξ_abs]Q:HarmonicOscillatorn:ℕhc:∫ (x : ℝ), ↑(physHermite n) (x / Q.ξ) ^ 2 * Real.exp (-x ^ 2 / Q.ξ ^ 2) =
  ∫ (x : ℝ), ↑(physHermite n) (1 / Q.ξ * x) * ↑(physHermite n) (1 / Q.ξ * x) * Real.exp (-(1 / Q.ξ) ^ 2 * x ^ 2)⊢ (↑n !)⁻¹ * (2 ^ n)⁻¹ * ((↑Q.ξ)⁻¹ * (↑√Real.pi)⁻¹) * ↑(Q.ξ • (↑n ! * 2 ^ n * √Real.pi)) = 1
  have : (n ! : ℂ) ≠ 0 := Complex.ne_zero_of_re_pos <| byQ:HarmonicOscillatorn:ℕhc:∫ (x : ℝ), ↑(physHermite n) (x / Q.ξ) ^ 2 * Real.exp (-x ^ 2 / Q.ξ ^ 2) =
  ∫ (x : ℝ), ↑(physHermite n) (1 / Q.ξ * x) * ↑(physHermite n) (1 / Q.ξ * x) * Real.exp (-(1 / Q.ξ) ^ 2 * x ^ 2)⊢ 0 < (↑n !).reQ:HarmonicOscillatorn:ℕhc:∫ (x : ℝ), ↑(physHermite n) (x / Q.ξ) ^ 2 * Real.exp (-x ^ 2 / Q.ξ ^ 2) =
  ∫ (x : ℝ), ↑(physHermite n) (1 / Q.ξ * x) * ↑(physHermite n) (1 / Q.ξ * x) * Real.exp (-(1 / Q.ξ) ^ 2 * x ^ 2)this:↑n ! ≠ 0⊢ (↑n !)⁻¹ * (2 ^ n)⁻¹ * ((↑Q.ξ)⁻¹ * (↑√Real.pi)⁻¹) * ↑(Q.ξ • (↑n ! * 2 ^ n * √Real.pi)) = 1 simpa using factorial_pos nQ:HarmonicOscillatorn:ℕhc:∫ (x : ℝ), ↑(physHermite n) (x / Q.ξ) ^ 2 * Real.exp (-x ^ 2 / Q.ξ ^ 2) =
  ∫ (x : ℝ), ↑(physHermite n) (1 / Q.ξ * x) * ↑(physHermite n) (1 / Q.ξ * x) * Real.exp (-(1 / Q.ξ) ^ 2 * x ^ 2)this:↑n ! ≠ 0⊢ (↑n !)⁻¹ * (2 ^ n)⁻¹ * ((↑Q.ξ)⁻¹ * (↑√Real.pi)⁻¹) * ↑(Q.ξ • (↑n ! * 2 ^ n * √Real.pi)) = 1Q:HarmonicOscillatorn:ℕhc:∫ (x : ℝ), ↑(physHermite n) (x / Q.ξ) ^ 2 * Real.exp (-x ^ 2 / Q.ξ ^ 2) =
  ∫ (x : ℝ), ↑(physHermite n) (1 / Q.ξ * x) * ↑(physHermite n) (1 / Q.ξ * x) * Real.exp (-(1 / Q.ξ) ^ 2 * x ^ 2)this:↑n ! ≠ 0⊢ (↑n !)⁻¹ * (2 ^ n)⁻¹ * ((↑Q.ξ)⁻¹ * (↑√Real.pi)⁻¹) * ↑(Q.ξ • (↑n ! * 2 ^ n * √Real.pi)) = 1
  have := Complex.ofReal_ne_zero.mpr (ne_of_gt Q.ξ_pos)Q:HarmonicOscillatorn:ℕhc:∫ (x : ℝ), ↑(physHermite n) (x / Q.ξ) ^ 2 * Real.exp (-x ^ 2 / Q.ξ ^ 2) =
  ∫ (x : ℝ), ↑(physHermite n) (1 / Q.ξ * x) * ↑(physHermite n) (1 / Q.ξ * x) * Real.exp (-(1 / Q.ξ) ^ 2 * x ^ 2)this✝:↑n ! ≠ 0this:↑Q.ξ ≠ 0⊢ (↑n !)⁻¹ * (2 ^ n)⁻¹ * ((↑Q.ξ)⁻¹ * (↑√Real.pi)⁻¹) * ↑(Q.ξ • (↑n ! * 2 ^ n * √Real.pi)) = 1
  have := Complex.ofReal_ne_zero.mpr (Real.sqrt_ne_zero'.mpr Real.pi_pos)Q:HarmonicOscillatorn:ℕhc:∫ (x : ℝ), ↑(physHermite n) (x / Q.ξ) ^ 2 * Real.exp (-x ^ 2 / Q.ξ ^ 2) =
  ∫ (x : ℝ), ↑(physHermite n) (1 / Q.ξ * x) * ↑(physHermite n) (1 / Q.ξ * x) * Real.exp (-(1 / Q.ξ) ^ 2 * x ^ 2)this✝¹:↑n ! ≠ 0this✝:↑Q.ξ ≠ 0this:↑√Real.pi ≠ 0⊢ (↑n !)⁻¹ * (2 ^ n)⁻¹ * ((↑Q.ξ)⁻¹ * (↑√Real.pi)⁻¹) * ↑(Q.ξ • (↑n ! * 2 ^ n * √Real.pi)) = 1
  simp only [smul_eq_mul, Complex.ofReal_mul, Complex.ofReal_natCast, Complex.ofReal_pow,
    Complex.ofReal_ofNat]Q:HarmonicOscillatorn:ℕhc:∫ (x : ℝ), ↑(physHermite n) (x / Q.ξ) ^ 2 * Real.exp (-x ^ 2 / Q.ξ ^ 2) =
  ∫ (x : ℝ), ↑(physHermite n) (1 / Q.ξ * x) * ↑(physHermite n) (1 / Q.ξ * x) * Real.exp (-(1 / Q.ξ) ^ 2 * x ^ 2)this✝¹:↑n ! ≠ 0this✝:↑Q.ξ ≠ 0this:↑√Real.pi ≠ 0⊢ (↑n !)⁻¹ * (2 ^ n)⁻¹ * ((↑Q.ξ)⁻¹ * (↑√Real.pi)⁻¹) * (↑Q.ξ * (↑n ! * 2 ^ n * ↑√Real.pi)) = 1
  field_simpAll goals completed! 🐙

The eigenfunctions of the quantum harmonic oscillator are orthogonal.


lemma eigenfunction_orthogonal {n p : ℕ} (hnp : n ≠ p) :
    ⟪HilbertSpace.mk (Q.eigenfunction_memHS n),
      HilbertSpace.mk (Q.eigenfunction_memHS p)⟫_ℂ = 0 := byQ:HarmonicOscillatorn:ℕp:ℕhnp:n ≠ p⊢ ⟪HilbertSpace.mk ⋯, HilbertSpace.mk ⋯⟫_ℂ = 0
  rw [inner_mk_mkQ:HarmonicOscillatorn:ℕp:ℕhnp:n ≠ p⊢ ∫ (x : ℝ), (starRingEnd ℂ) (Q.eigenfunction n x) * Q.eigenfunction p x = 0Q:HarmonicOscillatorn:ℕp:ℕhnp:n ≠ p⊢ ∫ (x : ℝ), (starRingEnd ℂ) (Q.eigenfunction n x) * Q.eigenfunction p x = 0]Q:HarmonicOscillatorn:ℕp:ℕhnp:n ≠ p⊢ ∫ (x : ℝ), (starRingEnd ℂ) (Q.eigenfunction n x) * Q.eigenfunction p x = 0
  conv_lhs =>
    enter [2, x]Q:HarmonicOscillatorn:ℕp:ℕhnp:n ≠ px:ℝ| (starRingEnd ℂ) (Q.eigenfunction n x) * Q.eigenfunction p x
    rw [eigenfunction_conj, Q.eigenfunction_mul n p]Q:HarmonicOscillatorn:ℕp:ℕhnp:n ≠ px:ℝ| 1 / ↑√(2 ^ n * ↑n !) * 1 / ↑√(2 ^ p * ↑p !) * (1 / (↑√Real.pi * ↑Q.ξ)) *
  ↑(↑(physHermite n) (x / Q.ξ) * ↑(physHermite p) (x / Q.ξ) * Real.exp (-x ^ 2 / Q.ξ ^ 2))
  rw [MeasureTheory.integral_const_mul,Q:HarmonicOscillatorn:ℕp:ℕhnp:n ≠ p⊢ 1 / ↑√(2 ^ n * ↑n !) * 1 / ↑√(2 ^ p * ↑p !) * (1 / (↑√Real.pi * ↑Q.ξ)) *
    ∫ (a : ℝ), ↑(↑(physHermite n) (a / Q.ξ) * ↑(physHermite p) (a / Q.ξ) * Real.exp (-a ^ 2 / Q.ξ ^ 2)) =
  0Q:HarmonicOscillatorn:ℕp:ℕhnp:n ≠ p⊢ 1 / ↑√(2 ^ n * ↑n !) * 1 / ↑√(2 ^ p * ↑p !) * (1 / (↑√Real.pi * ↑Q.ξ)) *
    ↑(∫ (x : ℝ), ↑(physHermite n) (x / Q.ξ) * ↑(physHermite p) (x / Q.ξ) * Real.exp (-x ^ 2 / Q.ξ ^ 2)) =
  0 integral_complex_ofRealQ:HarmonicOscillatorn:ℕp:ℕhnp:n ≠ p⊢ 1 / ↑√(2 ^ n * ↑n !) * 1 / ↑√(2 ^ p * ↑p !) * (1 / (↑√Real.pi * ↑Q.ξ)) *
    ↑(∫ (x : ℝ), ↑(physHermite n) (x / Q.ξ) * ↑(physHermite p) (x / Q.ξ) * Real.exp (-x ^ 2 / Q.ξ ^ 2)) =
  0Q:HarmonicOscillatorn:ℕp:ℕhnp:n ≠ p⊢ 1 / ↑√(2 ^ n * ↑n !) * 1 / ↑√(2 ^ p * ↑p !) * (1 / (↑√Real.pi * ↑Q.ξ)) *
    ↑(∫ (x : ℝ), ↑(physHermite n) (x / Q.ξ) * ↑(physHermite p) (x / Q.ξ) * Real.exp (-x ^ 2 / Q.ξ ^ 2)) =
  0]Q:HarmonicOscillatorn:ℕp:ℕhnp:n ≠ p⊢ 1 / ↑√(2 ^ n * ↑n !) * 1 / ↑√(2 ^ p * ↑p !) * (1 / (↑√Real.pi * ↑Q.ξ)) *
    ↑(∫ (x : ℝ), ↑(physHermite n) (x / Q.ξ) * ↑(physHermite p) (x / Q.ξ) * Real.exp (-x ^ 2 / Q.ξ ^ 2)) =
  0
  have hc : (∫ (x : ℝ), (physHermite n (x/Q.ξ) * physHermite p (x/Q.ξ)) * Real.exp (-x ^ 2 / Q.ξ^2))
      = ∫ (x : ℝ), (physHermite n (1/Q.ξ * x) * physHermite p (1/Q.ξ * x)) *
      Real.exp (- (1/Q.ξ)^2 * x ^ 2) := byQ:HarmonicOscillatorn:ℕp:ℕhnp:n ≠ p⊢ ⟪HilbertSpace.mk ⋯, HilbertSpace.mk ⋯⟫_ℂ = 0Q:HarmonicOscillatorn:ℕp:ℕhnp:n ≠ phc:∫ (x : ℝ), ↑(physHermite n) (x / Q.ξ) * ↑(physHermite p) (x / Q.ξ) * Real.exp (-x ^ 2 / Q.ξ ^ 2) =
  ∫ (x : ℝ), ↑(physHermite n) (1 / Q.ξ * x) * ↑(physHermite p) (1 / Q.ξ * x) * Real.exp (-(1 / Q.ξ) ^ 2 * x ^ 2)⊢ 1 / ↑√(2 ^ n * ↑n !) * 1 / ↑√(2 ^ p * ↑p !) * (1 / (↑√Real.pi * ↑Q.ξ)) *
    ↑(∫ (x : ℝ), ↑(physHermite n) (x / Q.ξ) * ↑(physHermite p) (x / Q.ξ) * Real.exp (-x ^ 2 / Q.ξ ^ 2)) =
  0
    congre_fQ:HarmonicOscillatorn:ℕp:ℕhnp:n ≠ p⊢ (fun x => ↑(physHermite n) (x / Q.ξ) * ↑(physHermite p) (x / Q.ξ) * Real.exp (-x ^ 2 / Q.ξ ^ 2)) = fun x =>
  ↑(physHermite n) (1 / Q.ξ * x) * ↑(physHermite p) (1 / Q.ξ * x) * Real.exp (-(1 / Q.ξ) ^ 2 * x ^ 2)Q:HarmonicOscillatorn:ℕp:ℕhnp:n ≠ phc:∫ (x : ℝ), ↑(physHermite n) (x / Q.ξ) * ↑(physHermite p) (x / Q.ξ) * Real.exp (-x ^ 2 / Q.ξ ^ 2) =
  ∫ (x : ℝ), ↑(physHermite n) (1 / Q.ξ * x) * ↑(physHermite p) (1 / Q.ξ * x) * Real.exp (-(1 / Q.ξ) ^ 2 * x ^ 2)⊢ 1 / ↑√(2 ^ n * ↑n !) * 1 / ↑√(2 ^ p * ↑p !) * (1 / (↑√Real.pi * ↑Q.ξ)) *
    ↑(∫ (x : ℝ), ↑(physHermite n) (x / Q.ξ) * ↑(physHermite p) (x / Q.ξ) * Real.exp (-x ^ 2 / Q.ξ ^ 2)) =
  0
    funext xe_fQ:HarmonicOscillatorn:ℕp:ℕhnp:n ≠ px:ℝ⊢ ↑(physHermite n) (x / Q.ξ) * ↑(physHermite p) (x / Q.ξ) * Real.exp (-x ^ 2 / Q.ξ ^ 2) =
  ↑(physHermite n) (1 / Q.ξ * x) * ↑(physHermite p) (1 / Q.ξ * x) * Real.exp (-(1 / Q.ξ) ^ 2 * x ^ 2)Q:HarmonicOscillatorn:ℕp:ℕhnp:n ≠ phc:∫ (x : ℝ), ↑(physHermite n) (x / Q.ξ) * ↑(physHermite p) (x / Q.ξ) * Real.exp (-x ^ 2 / Q.ξ ^ 2) =
  ∫ (x : ℝ), ↑(physHermite n) (1 / Q.ξ * x) * ↑(physHermite p) (1 / Q.ξ * x) * Real.exp (-(1 / Q.ξ) ^ 2 * x ^ 2)⊢ 1 / ↑√(2 ^ n * ↑n !) * 1 / ↑√(2 ^ p * ↑p !) * (1 / (↑√Real.pi * ↑Q.ξ)) *
    ↑(∫ (x : ℝ), ↑(physHermite n) (x / Q.ξ) * ↑(physHermite p) (x / Q.ξ) * Real.exp (-x ^ 2 / Q.ξ ^ 2)) =
  0
    ring_nfQ:HarmonicOscillatorn:ℕp:ℕhnp:n ≠ phc:∫ (x : ℝ), ↑(physHermite n) (x / Q.ξ) * ↑(physHermite p) (x / Q.ξ) * Real.exp (-x ^ 2 / Q.ξ ^ 2) =
  ∫ (x : ℝ), ↑(physHermite n) (1 / Q.ξ * x) * ↑(physHermite p) (1 / Q.ξ * x) * Real.exp (-(1 / Q.ξ) ^ 2 * x ^ 2)⊢ 1 / ↑√(2 ^ n * ↑n !) * 1 / ↑√(2 ^ p * ↑p !) * (1 / (↑√Real.pi * ↑Q.ξ)) *
    ↑(∫ (x : ℝ), ↑(physHermite n) (x / Q.ξ) * ↑(physHermite p) (x / Q.ξ) * Real.exp (-x ^ 2 / Q.ξ ^ 2)) =
  0Q:HarmonicOscillatorn:ℕp:ℕhnp:n ≠ phc:∫ (x : ℝ), ↑(physHermite n) (x / Q.ξ) * ↑(physHermite p) (x / Q.ξ) * Real.exp (-x ^ 2 / Q.ξ ^ 2) =
  ∫ (x : ℝ), ↑(physHermite n) (1 / Q.ξ * x) * ↑(physHermite p) (1 / Q.ξ * x) * Real.exp (-(1 / Q.ξ) ^ 2 * x ^ 2)⊢ 1 / ↑√(2 ^ n * ↑n !) * 1 / ↑√(2 ^ p * ↑p !) * (1 / (↑√Real.pi * ↑Q.ξ)) *
    ↑(∫ (x : ℝ), ↑(physHermite n) (x / Q.ξ) * ↑(physHermite p) (x / Q.ξ) * Real.exp (-x ^ 2 / Q.ξ ^ 2)) =
  0
  rw [hc,Q:HarmonicOscillatorn:ℕp:ℕhnp:n ≠ phc:∫ (x : ℝ), ↑(physHermite n) (x / Q.ξ) * ↑(physHermite p) (x / Q.ξ) * Real.exp (-x ^ 2 / Q.ξ ^ 2) =
  ∫ (x : ℝ), ↑(physHermite n) (1 / Q.ξ * x) * ↑(physHermite p) (1 / Q.ξ * x) * Real.exp (-(1 / Q.ξ) ^ 2 * x ^ 2)⊢ 1 / ↑√(2 ^ n * ↑n !) * 1 / ↑√(2 ^ p * ↑p !) * (1 / (↑√Real.pi * ↑Q.ξ)) *
    ↑(∫ (x : ℝ), ↑(physHermite n) (1 / Q.ξ * x) * ↑(physHermite p) (1 / Q.ξ * x) * Real.exp (-(1 / Q.ξ) ^ 2 * x ^ 2)) =
  0Q:HarmonicOscillatorn:ℕp:ℕhnp:n ≠ phc:∫ (x : ℝ), ↑(physHermite n) (x / Q.ξ) * ↑(physHermite p) (x / Q.ξ) * Real.exp (-x ^ 2 / Q.ξ ^ 2) =
  ∫ (x : ℝ), ↑(physHermite n) (1 / Q.ξ * x) * ↑(physHermite p) (1 / Q.ξ * x) * Real.exp (-(1 / Q.ξ) ^ 2 * x ^ 2)⊢ 1 / ↑√(2 ^ n * ↑n !) * 1 / ↑√(2 ^ p * ↑p !) * (1 / (↑√Real.pi * ↑Q.ξ)) * ↑0 = 0 physHermite_orthogonal_cons hnpQ:HarmonicOscillatorn:ℕp:ℕhnp:n ≠ phc:∫ (x : ℝ), ↑(physHermite n) (x / Q.ξ) * ↑(physHermite p) (x / Q.ξ) * Real.exp (-x ^ 2 / Q.ξ ^ 2) =
  ∫ (x : ℝ), ↑(physHermite n) (1 / Q.ξ * x) * ↑(physHermite p) (1 / Q.ξ * x) * Real.exp (-(1 / Q.ξ) ^ 2 * x ^ 2)⊢ 1 / ↑√(2 ^ n * ↑n !) * 1 / ↑√(2 ^ p * ↑p !) * (1 / (↑√Real.pi * ↑Q.ξ)) * ↑0 = 0Q:HarmonicOscillatorn:ℕp:ℕhnp:n ≠ phc:∫ (x : ℝ), ↑(physHermite n) (x / Q.ξ) * ↑(physHermite p) (x / Q.ξ) * Real.exp (-x ^ 2 / Q.ξ ^ 2) =
  ∫ (x : ℝ), ↑(physHermite n) (1 / Q.ξ * x) * ↑(physHermite p) (1 / Q.ξ * x) * Real.exp (-(1 / Q.ξ) ^ 2 * x ^ 2)⊢ 1 / ↑√(2 ^ n * ↑n !) * 1 / ↑√(2 ^ p * ↑p !) * (1 / (↑√Real.pi * ↑Q.ξ)) * ↑0 = 0]Q:HarmonicOscillatorn:ℕp:ℕhnp:n ≠ phc:∫ (x : ℝ), ↑(physHermite n) (x / Q.ξ) * ↑(physHermite p) (x / Q.ξ) * Real.exp (-x ^ 2 / Q.ξ ^ 2) =
  ∫ (x : ℝ), ↑(physHermite n) (1 / Q.ξ * x) * ↑(physHermite p) (1 / Q.ξ * x) * Real.exp (-(1 / Q.ξ) ^ 2 * x ^ 2)⊢ 1 / ↑√(2 ^ n * ↑n !) * 1 / ↑√(2 ^ p * ↑p !) * (1 / (↑√Real.pi * ↑Q.ξ)) * ↑0 = 0
  simp only [ofNat_nonneg, pow_nonneg, Real.sqrt_mul, Complex.ofReal_mul, one_div, mul_inv_rev,
    mul_one, Complex.ofReal_zero, mul_zero]All goals completed! 🐙

The eigenfunctions are orthonormal within the Hilbert space.


lemma eigenfunction_orthonormal :
    Orthonormal ℂ (fun n => HilbertSpace.mk (Q.eigenfunction_memHS n)) := byQ:HarmonicOscillator⊢ Orthonormal ℂ fun n => HilbertSpace.mk ⋯
  rw [orthonormal_iff_iteQ:HarmonicOscillator⊢ ∀ (i j : ℕ), ⟪HilbertSpace.mk ⋯, HilbertSpace.mk ⋯⟫_ℂ = if i = j then 1 else 0Q:HarmonicOscillator⊢ ∀ (i j : ℕ), ⟪HilbertSpace.mk ⋯, HilbertSpace.mk ⋯⟫_ℂ = if i = j then 1 else 0]Q:HarmonicOscillator⊢ ∀ (i j : ℕ), ⟪HilbertSpace.mk ⋯, HilbertSpace.mk ⋯⟫_ℂ = if i = j then 1 else 0
  intro n pQ:HarmonicOscillatorn:ℕp:ℕ⊢ ⟪HilbertSpace.mk ⋯, HilbertSpace.mk ⋯⟫_ℂ = if n = p then 1 else 0
  by_cases hnp : n = pposQ:HarmonicOscillatorn:ℕp:ℕhnp:n = p⊢ ⟪HilbertSpace.mk ⋯, HilbertSpace.mk ⋯⟫_ℂ = if n = p then 1 else 0negQ:HarmonicOscillatorn:ℕp:ℕhnp:¬n = p⊢ ⟪HilbertSpace.mk ⋯, HilbertSpace.mk ⋯⟫_ℂ = if n = p then 1 else 0
  ·posQ:HarmonicOscillatorn:ℕp:ℕhnp:n = p⊢ ⟪HilbertSpace.mk ⋯, HilbertSpace.mk ⋯⟫_ℂ = if n = p then 1 else 0 simp only [hnp, reduceIte]posQ:HarmonicOscillatorn:ℕp:ℕhnp:n = p⊢ ⟪HilbertSpace.mk ⋯, HilbertSpace.mk ⋯⟫_ℂ = 1
    exact Q.eigenfunction_normalized pAll goals completed! 🐙
  ·negQ:HarmonicOscillatorn:ℕp:ℕhnp:¬n = p⊢ ⟪HilbertSpace.mk ⋯, HilbertSpace.mk ⋯⟫_ℂ = if n = p then 1 else 0 simp only [hnp, reduceIte]negQ:HarmonicOscillatorn:ℕp:ℕhnp:¬n = p⊢ ⟪HilbertSpace.mk ⋯, HilbertSpace.mk ⋯⟫_ℂ = 0
    exact Q.eigenfunction_orthogonal hnpAll goals completed! 🐙

The eigenfunctions are linearly independent.

lemma eigenfunction_linearIndependent :
    LinearIndependent ℂ (fun n => HilbertSpace.mk (Q.eigenfunction_memHS n)) :=
  Q.eigenfunction_orthonormal.linearIndependent