feat: Notes for harmonic oscillator

PhysLean/Mathematics/SpecialFunctions/PhyscisistsHermite.lean

@@ -17,7 +17,12 @@ This file may eventually be upstreamed to Mathlib.
 open Polynomial
 namespace PhysLean
 
-/-- The Physicists Hermite polynomial. -/
+/-- The Physicists Hermite polynomial are defined as polynomials over `ℤ` in `X` recursively
+  with `physHermite 0 = 1` and
+
+  `physHermite (n + 1) = 2 • X * physHermite n - derivative (physHermite n)`.
+
+-/
 noncomputable def physHermite : ℕ → Polynomial ℤ
   | 0 => 1
   | n + 1 => 2 • X * physHermite n - derivative (physHermite n)
@@ -139,7 +144,8 @@ lemma physHermite_ne_zero {n : ℕ} : physHermite n ≠ 0 := by
   refine leadingCoeff_ne_zero.mp ?_
   simp
 
-/-- The physicists Hermite polynomial as a function from `ℝ` to `ℝ`. -/
+/-- The function `physHermiteFun` from `ℝ` to `ℝ` is defined by evaulation of
+ `physHermite` in `ℝ`. -/
 noncomputable def physHermiteFun (n : ℕ) : ℝ → ℝ := fun x => aeval x (physHermite n)
 
 @[simp]

PhysLean/Meta/Basic.lean

@@ -149,7 +149,7 @@ def getDeclStringNoDoc (name : Name) : CoreM String := do
     line.startsWith "def " ∨ line.startsWith "lemma " ∨ line.startsWith "inductive "
     ∨ line.startsWith "structure " ∨ line.startsWith "theorem "
     ∨ line.startsWith "instance " ∨ line.startsWith "abbrev " ∨
-    line.startsWith "noncomputable def "
+    line.startsWith "noncomputable def " ∨ line.startsWith "noncomputable abbrev "
   let lines := declerationString.splitOn "\n"
   match lines.findIdx? headerLine with
   | none => panic! s!"{name} has no header line"

PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Basic.lean

@@ -54,8 +54,9 @@ namespace QuantumMechanics
 
 namespace OneDimension
 
-/-- A quantum harmonic oscillator specified by a mass, a value of Plancck's and
-  an angular frequency. -/
+/-- A quantum harmonic oscillator specified by a three
+  real parameters: the mass of the particle `m`, a value of Planck's constant `ℏ`, and
+  an angular frequency `ω`. All three of these parameters are assumed to be positive. -/
 structure HarmonicOscillator where
   /-- The mass of the particle. -/
   m : ℝ
@@ -94,10 +95,10 @@ lemma ℏ_ne_zero : Q.ℏ ≠ 0 := by
   have h1 := Q.hℏ
   linarith
 
-/-- The Schrodinger Operator for the Harmonic oscillator on the space of functions.
+/-- For a harmonic oscillator, the Schrodinger Operator corresponding to it
+  is defined as the function from `ℝ → ℂ` to `ℝ → ℂ` taking
 
-  The prime `'` in the name is to signify that this is not defined on
-  equivalence classes of square integrable functions. -/
+  `ψ ↦ - ℏ^2 / (2 * m) * ψ'' + 1/2 * m * ω^2 * x^2 * ψ`. -/
 noncomputable def schrodingerOperator (ψ : ℝ → ℂ) : ℝ → ℂ :=
   fun y => - Q.ℏ ^ 2 / (2 * Q.m) * (deriv (deriv ψ) y) + 1/2 * Q.m * Q.ω^2 * y^2 * ψ y
 

PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Completeness.lean

@@ -256,6 +256,12 @@ lemma orthogonal_polynomial_of_mem_orthogonal (f : ℝ → ℂ) (hf : MemHS f)
     apply Integrable.smul
     exact Q.mul_physHermiteFun_integrable f hf i
 
+/-- If `f` is a function `ℝ → ℂ` satisfying `MemHS f` such that it is orthogonal
+  to all `eigenfunction n` then it is orthogonal to
+
+  `x ^ r * e ^ (- m ω x ^ 2 / (2 ℏ))`
+
+  the proof of this result relies on the fact that Hermite polynomials span polynomials. -/
 lemma orthogonal_power_of_mem_orthogonal (f : ℝ → ℂ) (hf : MemHS f)
     (hOrth : ∀ n : ℕ, ⟪HilbertSpace.mk (Q.eigenfunction_memHS n), HilbertSpace.mk hf⟫_ℂ = 0)
     (r : ℕ) :
@@ -297,6 +303,15 @@ lemma orthogonal_power_of_mem_orthogonal (f : ℝ → ℂ) (hf : MemHS f)
 
 open Finset
 
+/-- If `f` is a function `ℝ → ℂ` satisfying `MemHS f` such that it is orthogonal
+  to all `eigenfunction n` then it is orthogonal to
+
+  `e ^ (I c x) * e ^ (- m ω x ^ 2 / (2 ℏ))`
+
+  for any real `c`.
+  The proof of this result relies on the expansion of `e ^ (I c x)`
+  in terms of `x^r/r!` and using `orthogonal_power_of_mem_orthogonal`
+  along with integrablity conditions. -/
 lemma orthogonal_exp_of_mem_orthogonal (f : ℝ → ℂ) (hf : MemHS f)
     (hOrth : ∀ n : ℕ, ⟪HilbertSpace.mk (Q.eigenfunction_memHS n), HilbertSpace.mk hf⟫_ℂ = 0)
     (c : ℝ) : ∫ x : ℝ, Complex.exp (Complex.I * c * x) *
@@ -458,6 +473,14 @@ lemma orthogonal_exp_of_mem_orthogonal (f : ℝ → ℂ) (hf : MemHS f)
 open FourierTransform MeasureTheory Real Lp Memℒp Filter Complex Topology
   ComplexInnerProductSpace ComplexConjugate
 
+/-- If `f` is a function `ℝ → ℂ` satisfying `MemHS f` such that it is orthogonal
+  to all `eigenfunction n` then the fourier transform of
+
+  `f (x) * e ^ (- m ω x ^ 2 / (2 ℏ))`
+
+  is zero.
+
+  The proof of this result relies on `orthogonal_exp_of_mem_orthogonal`. -/
 lemma fourierIntegral_zero_of_mem_orthogonal (f : ℝ → ℂ) (hf : MemHS f)
     (hOrth : ∀ n : ℕ, ⟪HilbertSpace.mk (Q.eigenfunction_memHS n), HilbertSpace.mk hf⟫_ℂ = 0) :
     𝓕 (fun x => f x * Real.exp (- m * ω * x^2 / (2 * ℏ))) = 0 := by
@@ -537,7 +560,19 @@ lemma zero_of_orthogonal_eigenVector (f : HilbertSpace)
   obtain ⟨f, hf, rfl⟩ := HilbertSpace.mk_surjective f
   exact zero_of_orthogonal_mk Q f hf hOrth plancherel_theorem
 
-lemma completness_eigenvector
+/--
+  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 ^ (- m * ω * x^2 / (2 * ℏ)`
+
+  is zero for `f` orthogonal to all eigenfunctions, and hence the norm of `f` is zero.
+-/
+theorem eigenfunction_completeness
     (plancherel_theorem : ∀ {f : ℝ → ℂ} (hf : Integrable f volume) (_ : Memℒp f 2),
       eLpNorm (𝓕 f) 2 volume = eLpNorm f 2 volume) :
     (Submodule.span ℂ

PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Eigenfunction.lean

@@ -21,8 +21,12 @@ open Nat
 open PhysLean
 open HilbertSpace
 
-/-- The eigenfunctions for the Harmonic oscillator defined as a function
-  `ℝ → ℂ`. -/
+/-- The `n`th  eigenfunction of the Harmonic oscillator is defined as the function `ℝ → ℂ`
+  taking `x : ℝ` to
+
+  `1/√(2^n n!) (m ω /(π ℏ))^(1/4) * physHermiteFun n (√(m ω /ℏ) x) * e ^ (- m ω x^2/2ℏ)`.
+
+-/
 noncomputable def eigenfunction (n : ℕ) : ℝ → ℂ := fun x =>
   1/Real.sqrt (2 ^ n * n !) * Real.sqrt (Real.sqrt (Q.m * Q.ω / (Real.pi * Q.ℏ))) *
   physHermiteFun n (Real.sqrt (Q.m * Q.ω / Q.ℏ) * x) * Real.exp (- Q.m * Q.ω * x^2 / (2 * Q.ℏ))
@@ -380,7 +384,7 @@ lemma eigenfunction_orthogonal {n p : ℕ} (hnp : n ≠ p) :
     mul_one, Complex.ofReal_zero, mul_zero, c]
   exact hnp
 
-/-- The eigenvectors are orthonormal within the Hilbert space. s-/
+/-- The eigenfunctions are orthonormal within the Hilbert space. -/
 lemma eigenfunction_orthonormal :
     Orthonormal ℂ (fun n => HilbertSpace.mk (Q.eigenfunction_memHS n)) := by
   rw [orthonormal_iff_ite]

PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/TISE.lean

@@ -21,7 +21,7 @@ open Nat
 open PhysLean
 open HilbertSpace
 
-/-- The eigenvalues for the Harmonic oscillator. -/
+/-- The `n`th eigenvalues for a Harmonic oscillator is defined as `(n + 1/2) * ℏ * ω`. -/
 noncomputable def eigenValue (n : ℕ) : ℝ := (n + 1/2) * Q.ℏ * Q.ω
 
 lemma deriv_eigenfunction_zero : deriv (Q.eigenfunction 0) =
@@ -255,7 +255,13 @@ lemma schrodingerOperator_eigenfunction_succ_succ (n : ℕ) (x : ℝ) :
   field_simp
   ring
 
-/-- The eigenfunctions satisfy the time-independent Schrodinger equation. -/
+/-- The `n`th eigenfunction satisfies the time-independent Schrodinger equation with
+  respect to the `n`th eigenvalue. That is to say for `Q` a harmonic scillator,
+
+  `Q.schrodingerOperator (Q.eigenfunction n) x =  Q.eigenValue n * Q.eigenfunction n x`.
+
+  The prove of this result is done by explicit calculation of derivatives.
+-/
 theorem schrodingerOperator_eigenfunction (n : ℕ) :
     Q.schrodingerOperator (Q.eigenfunction n) x =
     Q.eigenValue n * Q.eigenfunction n x :=

PhysLean/QuantumMechanics/OneDimension/HilbertSpace/Basic.lean

@@ -22,20 +22,25 @@ namespace QuantumMechanics
 
 namespace OneDimension
 noncomputable section
-/-- The Hilbert space in 1d corresponding to square integbrable (equivalence classes)
-  of functions. -/
+
+/-- The Hilbert space for a one dimensional quantum system is defined as
+  the space of almost-everywhere equal equivalence classes of square integrable functions
+  from `ℝ` to `ℂ`. -/
 noncomputable abbrev HilbertSpace := MeasureTheory.Lp (α := ℝ) ℂ 2
 
 namespace HilbertSpace
 open MeasureTheory
 
-/-- The proposition which is true if a function `f` can be lifted to the Hilbert space. -/
+/-- The proposition `MemHS f` for a function `f : ℝ → ℂ` is defined
+  to be true if the function `f` can be lifted to the Hilbert space. -/
 def MemHS (f : ℝ → ℂ) : Prop := Memℒp f 2 MeasureTheory.volume
 
 lemma aeStronglyMeasurable_of_memHS {f : ℝ → ℂ} (h : MemHS f) :
     AEStronglyMeasurable f := by
   exact h.1
 
+/-- A function `f` statisfies `MemHS f` if and only if it is almost everywhere
+  strongly measurable, and square integrable. -/
 lemma memHS_iff {f : ℝ → ℂ} : MemHS f ↔
     AEStronglyMeasurable f ∧ Integrable (fun x => ‖f x‖ ^ 2) := by
   rw [MemHS]
@@ -61,7 +66,8 @@ lemma aeEqFun_mk_mem_iff (f : ℝ → ℂ) (hf : AEStronglyMeasurable f volume)
   apply MeasureTheory.memℒp_congr_ae
   exact AEEqFun.coeFn_mk f hf
 
-/-- The member of the Hilbert space from a `MemHS f`. -/
+/-- Given a function `f : ℝ → ℂ` such that `MemHS f` is true via `hf`, then `HilbertSpace.mk hf`
+  is the element of the `HilbertSpace` defined by `f`. -/
 def mk {f : ℝ → ℂ} (hf : MemHS f) : HilbertSpace :=
   ⟨AEEqFun.mk f hf.1, (aeEqFun_mk_mem_iff f hf.1).mpr hf⟩
 

docs/CuratedNotes/HarmonicOscillator.html

@@ -0,0 +1,105 @@
+---
+layout: default
+---
+<style>
+  body {
+    color: black;
+  }
+</style>
+
+<link rel="stylesheet" href="https://cdnjs.cloudflare.com/ajax/libs/highlight.js/11.9.0/styles/default.min.css">
+<script src="https://cdnjs.cloudflare.com/ajax/libs/highlight.js/11.9.0/highlight.min.js"></script>
+<script type="text/javascript" charset="UTF-8"
+  src="../assets/css/lean.min.js"></script>
+<script>hljs.highlightAll();</script>
+<!--- Toggle background color. -->
+<script>
+let isDefaultBackground = true;
+function toggleDyslexiaMode() {
+  document.body.style.backgroundColor = isDefaultBackground ? '#f4ecd8' : '#ffffff';
+  isDefaultBackground = !isDefaultBackground;
+}
+</script>
+<div style="text-align: right;">
+  <a href="#" onclick="toggleDyslexiaMode(); return false;" style="color: #2c5282; text-decoration: underline; cursor: pointer;">
+    Toggle background color
+  </a>
+</div>
+<!-- Note header (title, curators, notice etc.). -->
+<center><h1 style="font-size: 50px;">{{ site.data.harmonicOscillator.title }}</h1></center>
+<center><h2 style="font-size: 20px;">Note Authors: {{ site.data.harmonicOscillator.curators }}</h2></center>
+<!--  -->
+<style>
+  body {
+    font-family: "Times New Roman", Times, serif;
+  }
+</style>
+<br>
+<div style="border: 1px solid black; padding: 10px;">
+  <p>
+  These notes are created using an interactive theorem
+  prover called <a href="https://lean-lang.org">Lean</a>.
+  Lean formally checks definitions, theorems and proofs for correctness.
+  These notes are part of a much larger project called
+  <a href="https://github.com/HEPLean/PhysLean">PhysLean</a>, which aims to digitalize
+  high energy physics into Lean. Please consider contributing to this project.
+  <br><br>
+  Please provide feedback or suggestions for improvements by creating a GitHub issue
+  <a href="https://github.com/HEPLean/HepLean/issues">here</a>.
+  </p>
+</div>
+<!-- Table of content. -->
+<hr>
+<center><h2 style="font-size: 30px;">Table of content</h2></center>
+<p>
+{% for entry in site.data.harmonicOscillator.parts %}
+{% if entry.type == "h1" %}
+  <a href="#section-{{ entry.sectionNo }}" style="color: #2c5282;">{{ entry.sectionNo }}. {{ entry.content }}</a><br>
+{% endif %}
+{% if entry.type == "h2" %}
+&nbsp;&nbsp;&nbsp;&nbsp;<a href="#section-{{ entry.sectionNo }}"  style="color: #2c5282;">{{ entry.sectionNo }}. {{ entry.content }}</a><br>
+{% endif %}
+{% endfor %}
+</p>
+<hr>
+<!-- Main body. -->
+<br>
+{% for entry in site.data.harmonicOscillator.parts %}
+  {% if entry.type == "h1" %}
+    <h1 id="section-{{ entry.sectionNo }}">{{ entry.sectionNo }}. {{ entry.content }}</h1>
+  {% endif %}
+  {% if entry.type == "h2" %}
+    <h2 id="section-{{ entry.sectionNo }}">{{ entry.sectionNo }}. {{ entry.content }} </h2>
+  {% endif %}
+  {% if entry.type == "p" %}
+    <p>{{ entry.content }}</p>
+  {% endif %}
+  {% if entry.type == "warning" %}
+  <div class="alert alert-danger" role="alert">
+    <b>Warning:</b> {{ entry.content }}
+  </div>
+  {% endif %}
+  {% if entry.type == "name" %}
+
+  <div style=" padding: 10px; border-radius: 4px;">
+     <b id="decl-{{ entry.declNo }}">
+      <a href="#decl-{{ entry.declNo }}" style="color: black;">
+      {% if entry.isDef %}Definition{% else %}
+      {% if entry.isThm %}Theorem{% else %}Lemma{% endif %}{% endif %} {{ entry.declNo }}</a></b>
+      (<a href = "{{ entry.link }}" style="color: #2c5282;">{{ entry.name }}</a>)<b>:</b>
+      {% if entry.status == "incomplete" %}🚧{% endif %}
+      <div style="margin-left: 1em;">{{ entry.docString | markdownify}}</div>
+    <details class="code-block-container">
+    <summary style="font-size: 0.8em; margin-left: 1em;">Show Lean code:</summary>
+    <pre style="background: none; margin: 0;"><code class="language-lean">{{ entry.declString }}</code></pre>
+    </details>
+  </div>
+  {% endif %}
+  {% if entry.type == "remark" %}
+  <div style="padding: 10px; border-radius: 4px; border: 1px solid #e8e6e6;">
+    <a href = "{{ entry.link }}" style="color: #2c5282;">Remark: {{ entry.name}} </a>
+  {{ entry.content|markdownify }}
+  </div>
+  <br>
+  {% endif %}
+{% endfor %}

scripts/MetaPrograms/notes.lean

@@ -290,10 +290,57 @@ def perturbationTheory : Note where
     .name ``FieldSpecification.FieldOpAlgebra.wicks_theorem_normal_order .complete
     ]
 
+
+def harmonicOscillator : Note where
+  title := "The Quantum Harmonic Oscillator in Lean 4"
+  curators := ["Joseph Tooby-Smith"]
+  parts := [
+    .h1 "Introduction",
+    .p "The quantum harmonic oscillator is one of the foundational examples
+    of a 1d quantum mechanical system. It is perhaps the first example that
+    many undergraduate students encounter when learning quantum mechanics.",
+    .p "
+    This note shall present the digitilisation (or formalization) of the
+    quantum harmonic oscillator into the theorem prover Lean 4. This is part of a larger
+    project called PhysLean. Note not every definition and theorem is given here.",
+    .h1 "Hilbert Space",
+    .name ``QuantumMechanics.OneDimension.HilbertSpace .complete,
+    .name ``QuantumMechanics.OneDimension.HilbertSpace.MemHS .complete,
+    .name ``QuantumMechanics.OneDimension.HilbertSpace.memHS_iff .complete,
+    .name ``QuantumMechanics.OneDimension.HilbertSpace.mk .complete,
+    .h1 "The Schrodinger Operator",
+    .name ``QuantumMechanics.OneDimension.HarmonicOscillator .complete,
+    .name ``QuantumMechanics.OneDimension.HarmonicOscillator.schrodingerOperator .complete,
+    .h1 "The eigenfunctions of the Schrodinger Operator",
+    .name ``PhysLean.physHermite .complete,
+    .name ``PhysLean.physHermiteFun .complete,
+    .name ``QuantumMechanics.OneDimension.HarmonicOscillator.eigenfunction .complete,
+    .h2 "Properties of the eigenfunctions",
+    .name ``QuantumMechanics.OneDimension.HarmonicOscillator.eigenfunction_integrable .complete,
+    .name ``QuantumMechanics.OneDimension.HarmonicOscillator.eigenfunction_conj .complete,
+    .name ``QuantumMechanics.OneDimension.HarmonicOscillator.eigenfunction_aeStronglyMeasurable .complete,
+    .name ``QuantumMechanics.OneDimension.HarmonicOscillator.eigenfunction_square_integrable .complete,
+    .name ``QuantumMechanics.OneDimension.HarmonicOscillator.eigenfunction_memHS .complete,
+    .name ``QuantumMechanics.OneDimension.HarmonicOscillator.eigenfunction_differentiableAt .complete,
+    .name ``QuantumMechanics.OneDimension.HarmonicOscillator.eigenfunction_orthonormal .complete,
+    .h1 "The time-independent Schrodinger Equation",
+    .name ``QuantumMechanics.OneDimension.HarmonicOscillator.eigenValue .complete,
+    .name ``QuantumMechanics.OneDimension.HarmonicOscillator.schrodingerOperator_eigenfunction
+      .complete,
+    .h1 "Completeness",
+    .name ``QuantumMechanics.OneDimension.HarmonicOscillator.orthogonal_power_of_mem_orthogonal .complete,
+    .name ``QuantumMechanics.OneDimension.HarmonicOscillator.orthogonal_exp_of_mem_orthogonal .complete,
+    .name ``QuantumMechanics.OneDimension.HarmonicOscillator.fourierIntegral_zero_of_mem_orthogonal .complete,
+    .name ``QuantumMechanics.OneDimension.HarmonicOscillator.eigenfunction_completeness .complete,
+    ]
 unsafe def main (_ : List String) : IO UInt32 := do
   initSearchPath (← findSysroot)
   let ymlString ← CoreM.withImportModules #[`PhysLean] (perturbationTheory.toYML).run'
   let fileOut : System.FilePath := {toString := "./docs/_data/perturbationTheory.yml"}
-  IO.println (s!"YML file made.")
+  IO.println (s!"YML file made for perturbation theory.")
   IO.FS.writeFile fileOut ymlString
+  let ymlString2 ← CoreM.withImportModules #[`PhysLean] (harmonicOscillator.toYML).run'
+  let fileOut2 : System.FilePath := {toString := "./docs/_data/harmonicOscillator.yml"}
+  IO.println (s!"YML file made for harmonic oscillator.")
+  IO.FS.writeFile fileOut2 ymlString2
   pure 0