From c21ce36eb12127234d7a7c30ca9fe8f06fe8e5ce Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Wed, 26 Feb 2025 11:03:29 +0000 Subject: [PATCH] feat: Notes for harmonic oscillator --- .../SpecialFunctions/PhyscisistsHermite.lean | 10 +- PhysLean/Meta/Basic.lean | 2 +- .../HarmonicOscillator/Basic.lean | 11 +- .../HarmonicOscillator/Completeness.lean | 37 +++++- .../HarmonicOscillator/Eigenfunction.lean | 10 +- .../OneDimension/HarmonicOscillator/TISE.lean | 10 +- .../OneDimension/HilbertSpace/Basic.lean | 14 ++- docs/CuratedNotes/HarmonicOscillator.html | 105 ++++++++++++++++++ scripts/MetaPrograms/notes.lean | 49 +++++++- 9 files changed, 229 insertions(+), 19 deletions(-) create mode 100644 docs/CuratedNotes/HarmonicOscillator.html diff --git a/PhysLean/Mathematics/SpecialFunctions/PhyscisistsHermite.lean b/PhysLean/Mathematics/SpecialFunctions/PhyscisistsHermite.lean index 6fcc43d..e427644 100644 --- a/PhysLean/Mathematics/SpecialFunctions/PhyscisistsHermite.lean +++ b/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] diff --git a/PhysLean/Meta/Basic.lean b/PhysLean/Meta/Basic.lean index 8e4108a..3c39639 100644 --- a/PhysLean/Meta/Basic.lean +++ b/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" diff --git a/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Basic.lean b/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Basic.lean index ac88a78..2fe732d 100644 --- a/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Basic.lean +++ b/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 diff --git a/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Completeness.lean b/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Completeness.lean index df25d0d..08f5611 100644 --- a/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Completeness.lean +++ b/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 ℂ diff --git a/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Eigenfunction.lean b/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Eigenfunction.lean index 85c6534..1b1ea08 100644 --- a/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Eigenfunction.lean +++ b/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] diff --git a/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/TISE.lean b/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/TISE.lean index b07b662..44eb480 100644 --- a/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/TISE.lean +++ b/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 := diff --git a/PhysLean/QuantumMechanics/OneDimension/HilbertSpace/Basic.lean b/PhysLean/QuantumMechanics/OneDimension/HilbertSpace/Basic.lean index c4041a4..31eaf78 100644 --- a/PhysLean/QuantumMechanics/OneDimension/HilbertSpace/Basic.lean +++ b/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⟩ diff --git a/docs/CuratedNotes/HarmonicOscillator.html b/docs/CuratedNotes/HarmonicOscillator.html new file mode 100644 index 0000000..7f3bca8 --- /dev/null +++ b/docs/CuratedNotes/HarmonicOscillator.html @@ -0,0 +1,105 @@ +--- +layout: default +--- + + + + + + + + +
+ + Toggle background color + +
+ +

{{ site.data.harmonicOscillator.title }}

+

Note Authors: {{ site.data.harmonicOscillator.curators }}

+ + +
+
+

+ These notes are created using an interactive theorem + prover called Lean. + Lean formally checks definitions, theorems and proofs for correctness. + These notes are part of a much larger project called + PhysLean, which aims to digitalize + high energy physics into Lean. Please consider contributing to this project. +

+ Please provide feedback or suggestions for improvements by creating a GitHub issue + here. +

+
+ +
+

Table of content

+

+{% for entry in site.data.harmonicOscillator.parts %} +{% if entry.type == "h1" %} + {{ entry.sectionNo }}. {{ entry.content }}
+{% endif %} +{% if entry.type == "h2" %} +    {{ entry.sectionNo }}. {{ entry.content }}
+{% endif %} +{% endfor %} +

+
+ +
+{% for entry in site.data.harmonicOscillator.parts %} + {% if entry.type == "h1" %} +

{{ entry.sectionNo }}. {{ entry.content }}

+ {% endif %} + {% if entry.type == "h2" %} +

{{ entry.sectionNo }}. {{ entry.content }}

+ {% endif %} + {% if entry.type == "p" %} +

{{ entry.content }}

+ {% endif %} + {% if entry.type == "warning" %} + + {% endif %} + {% if entry.type == "name" %} + +
+ + + {% if entry.isDef %}Definition{% else %} + {% if entry.isThm %}Theorem{% else %}Lemma{% endif %}{% endif %} {{ entry.declNo }} + ({{ entry.name }}): + {% if entry.status == "incomplete" %}🚧{% endif %} +
{{ entry.docString | markdownify}}
+
+ Show Lean code: + 
{{ entry.declString }}
+
+
+ {% endif %} + {% if entry.type == "remark" %} +
+ Remark: {{ entry.name}} + {{ entry.content|markdownify }} +
+
+ {% endif %} +{% endfor %} diff --git a/scripts/MetaPrograms/notes.lean b/scripts/MetaPrograms/notes.lean index 0f5ea5b..8f630a0 100644 --- a/scripts/MetaPrograms/notes.lean +++ b/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