DibyashanuPati/PhysLean
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix a few typos in docs/_data

Browse source
This commit is contained in:
Pietro Monticone 2025-03-08 23:02:17 +01:00
parent d65a63b39d
commit 4efce2ee0e
3 changed files with 51 additions and 51 deletions
Download patch file Download diff file Expand all files Collapse all files

4
docs/_data/TODO.yml
View file

@ -11,7 +11,7 @@
githubLink: https://github.com/HEPLean/HepLean/blob/master/HepLean/AnomalyCancellation/Basic.lean#L18
line: 18
- content: "Derive an ACC system from a guage algebra and fermionic representations."
- content: "Derive an ACC system from a gauge algebra and fermionic representations."
file: HepLean.AnomalyCancellation.Basic
githubLink: https://github.com/HEPLean/HepLean/blob/master/HepLean/AnomalyCancellation/Basic.lean#L17
line: 17
@ -103,7 +103,7 @@
githubLink: https://github.com/HEPLean/HepLean/blob/master/HepLean/Lorentz/Group/Restricted.lean#L14
line: 14
- content: "Generalize the inclusion of rotations into LorentzGroup to abitary dimension."
- content: "Generalize the inclusion of rotations into LorentzGroup to arbitrary dimension."
file: HepLean.Lorentz.Group.Rotations
githubLink: https://github.com/HEPLean/HepLean/blob/master/HepLean/Lorentz/Group/Rotations.lean#L14
line: 14

86
docs/_data/harmonicOscillator.yml
View file

@ -2,7 +2,7 @@
title: "The Quantum Harmonic Oscillator in Lean 4"
curators: Joseph Tooby-Smith
parts:
- type: h1
sectionNo: 1
content: "Introduction"
@ -17,13 +17,13 @@ parts:
Lean 4, as part of the larger project PhysLean.
What this means is that every definition and theorem in this note has been formally checked
for mathematical correctness for by a computer. There are a number of
motivations for doing this which are dicussed <a href = 'https://heplean.com'>here</a>."
motivations for doing this which are discussed <a href = 'https://heplean.com'>here</a>."
- type: p
content: "Note that we do not give every definition and theorem which is part of
the formalization.
Our goal is give key aspects, in such a way that we hope this note will be useful
to newcomers to Lean or those intrested in simply intrested in learning about the
to newcomers to Lean or those simply interested in learning about the
quantum harmonic oscillator."
- type: h1
@ -41,7 +41,7 @@ parts:
docString: |
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 `ℂ`.
from `ℝ` to `ℂ`.
declString: |
noncomputable abbrev HilbertSpace := MeasureTheory.Lp (α := ℝ) ℂ 2
declNo: "2.1"
@ -56,7 +56,7 @@ parts:
isThm: false
docString: |
The proposition `MemHS f` for a function `f : ℝ → ℂ` is defined
to be true if the function `f` can be lifted to the Hilbert space.
to be true if the function `f` can be lifted to the Hilbert space.
declString: |
def MemHS (f : ℝ → ℂ) : Prop := Memℒp f 2 MeasureTheory.volume
declNo: "2.2"
@ -70,8 +70,8 @@ parts:
isDef: false
isThm: false
docString: |
A function `f` statisfies `MemHS f` if and only if it is almost everywhere
strongly measurable, and square integrable.
A function `f` satisfies `MemHS f` if and only if it is almost everywhere
strongly measurable, and square integrable.
declString: |
lemma memHS_iff {f : ℝ → ℂ} : MemHS f ↔
AEStronglyMeasurable f ∧ Integrable (fun x => ‖f x‖ ^ 2) := by
@ -100,7 +100,7 @@ parts:
isThm: false
docString: |
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`.
is the element of the `HilbertSpace` defined by `f`.
declString: |
def mk {f : ℝ → ℂ} (hf : MemHS f) : HilbertSpace :=
⟨AEEqFun.mk f hf.1, (aeEqFun_mk_mem_iff f hf.1).mpr hf⟩
@ -121,7 +121,7 @@ parts:
docString: |
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.
an angular frequency `ω`. All three of these parameters are assumed to be positive.
declString: |
structure HarmonicOscillator where
/-- The mass of the particle. -/
@ -146,8 +146,8 @@ parts:
docString: |
For a harmonic oscillator, the Schrodinger Operator corresponding to it
is defined as the function from `ℝ → ℂ` to `ℝ → ℂ` taking
`ψ ↦ - ℏ^2 / (2 * m) * ψ'' + 1/2 * m * ω^2 * x^2 * ψ`.
`ψ ↦ - ℏ^2 / (2 * m) * ψ'' + 1/2 * m * ω^2 * x^2 * ψ`.
declString: |
noncomputable def schrodingerOperator (ψ : ℝ → ℂ) : ℝ → ℂ :=
fun y => - Q.ℏ ^ 2 / (2 * Q.m) * (deriv (deriv ψ) y) + 1/2 * Q.m * Q.ω^2 * y^2 * ψ y
@ -168,11 +168,11 @@ parts:
docString: |
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)`.
This polynomial will often be cast as a function `ℝ → ℝ` by evaluating the polynomial at `X`.
declString: |
noncomputable def physHermite : ℕ → Polynomial ℤ
| 0 => 1
@ -190,10 +190,10 @@ parts:
docString: |
The `n`th eigenfunction of the Harmonic oscillator is defined as the function `ℝ → ℂ`
taking `x : ℝ` to
`1/√(2^n n!) (m ω /(π ℏ))^(1/4) * physHermite n (√(m ω /ℏ) x) * e ^ (- m ω x^2/2ℏ)`.
declString: |
noncomputable def eigenfunction (n : ℕ) : ℝ → ℂ := fun x =>
1/Real.sqrt (2 ^ n * n !) * Real.sqrt (Real.sqrt (Q.m * Q.ω / (Real.pi * Q.ℏ))) *
@ -213,7 +213,7 @@ parts:
isDef: false
isThm: false
docString: |
The eigenfunctions are integrable.
The eigenfunctions are integrable.
declString: |
lemma eigenfunction_integrable (n : ℕ) : MeasureTheory.Integrable (Q.eigenfunction n) := by
rw [eigenfunction_eq]
@ -244,7 +244,7 @@ parts:
isDef: false
isThm: false
docString: |
The eigenfunctions are real.
The eigenfunctions are real.
declString: |
lemma eigenfunction_conj (n : ℕ) (x : ℝ) :
(starRingEnd ℂ) (Q.eigenfunction n x) = Q.eigenfunction n x := by
@ -262,7 +262,7 @@ parts:
isDef: false
isThm: false
docString: |
The eigenfunctions are almost everywhere strongly measurable.
The eigenfunctions are almost everywhere strongly measurable.
declString: |
lemma eigenfunction_aeStronglyMeasurable (n : ℕ) :
MeasureTheory.AEStronglyMeasurable (Q.eigenfunction n) :=
@ -278,7 +278,7 @@ parts:
isDef: false
isThm: false
docString: |
The eigenfunctions are square integrable.
The eigenfunctions are square integrable.
declString: |
lemma eigenfunction_square_integrable (n : ℕ) :
MeasureTheory.Integrable (fun x => ‖Q.eigenfunction n x‖ ^ 2) := by
@ -304,7 +304,7 @@ parts:
isDef: false
isThm: false
docString: |
The eigenfunctions are members of the Hilbert space.
The eigenfunctions are members of the Hilbert space.
declString: |
lemma eigenfunction_memHS (n : ℕ) : MemHS (Q.eigenfunction n) := by
rw [memHS_iff]
@ -322,7 +322,7 @@ parts:
isDef: false
isThm: false
docString: |
The eigenfunctions are differentiable.
The eigenfunctions are differentiable.
declString: |
lemma eigenfunction_differentiableAt (x : ℝ) (n : ℕ) :
DifferentiableAt ℝ (Q.eigenfunction n) x := by
@ -339,7 +339,7 @@ parts:
isDef: false
isThm: false
docString: |
The eigenfunctions are orthonormal within the Hilbert space.
The eigenfunctions are orthonormal within the Hilbert space.
declString: |
lemma eigenfunction_orthonormal :
Orthonormal ℂ (fun n => HilbertSpace.mk (Q.eigenfunction_memHS n)) := by
@ -365,7 +365,7 @@ parts:
isDef: true
isThm: false
docString: |
The `n`th eigenvalues for a Harmonic oscillator is defined as `(n + 1/2) * ℏ * ω`.
The `n`th eigenvalues for a Harmonic oscillator is defined as `(n + 1/2) * ℏ * ω`.
declString: |
noncomputable def eigenValue (n : ℕ) : ℝ := (n + 1/2) * Q.ℏ * Q.ω
declNo: "5.1"
@ -381,11 +381,11 @@ parts:
docString: |
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 proof of this result is done by explicit calculation of derivatives.
declString: |
theorem schrodingerOperator_eigenfunction (n : ℕ) :
Q.schrodingerOperator (Q.eigenfunction n) x =
@ -411,10 +411,10 @@ parts:
docString: |
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.
the proof of this result relies on the fact that Hermite polynomials span polynomials.
declString: |
lemma orthogonal_power_of_mem_orthogonal (f : ℝ → ℂ) (hf : MemHS f)
(hOrth : ∀ n : ℕ, ⟪HilbertSpace.mk (Q.eigenfunction_memHS n), HilbertSpace.mk hf⟫_ℂ = 0)
@ -467,13 +467,13 @@ parts:
docString: |
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.
along with integrability conditions.
declString: |
lemma orthogonal_exp_of_mem_orthogonal (f : ℝ → ℂ) (hf : MemHS f)
(hOrth : ∀ n : ℕ, ⟪HilbertSpace.mk (Q.eigenfunction_memHS n), HilbertSpace.mk hf⟫_ℂ = 0)
@ -645,12 +645,12 @@ parts:
docString: |
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`.
The proof of this result relies on `orthogonal_exp_of_mem_orthogonal`.
declString: |
lemma fourierIntegral_zero_of_mem_orthogonal (f : ℝ → ℂ) (hf : MemHS f)
(hOrth : ∀ n : ℕ, ⟪HilbertSpace.mk (Q.eigenfunction_memHS n), HilbertSpace.mk hf⟫_ℂ = 0) :
@ -682,14 +682,14 @@ parts:
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.
declString: |
theorem eigenfunction_completeness
(plancherel_theorem : ∀ {f : ℝ → ℂ} (hf : Integrable f volume) (_ : Memℒp f 2),
@ -711,4 +711,4 @@ parts:
simp
rw [hl]
simp
declNo: "6.4"
declNo: "6.4"

12
docs/_data/perturbationTheory.yml
View file

@ -16,7 +16,7 @@ parts:
In perturbative quantum field theory, Wick's theorem allows
us to expand expectation values of time-ordered products of fields in terms of normal-orders
and time contractions.
The theorem is used to simplify the calculation of scattering amplitudes, and is the precurser
The theorem is used to simplify the calculation of scattering amplitudes, and is the precursor
to Feynman diagrams.
There are actually three different versions of Wick's theorem used.
@ -24,12 +24,12 @@ parts:
PhysLean contains a formalization of all three of these theorems in complete generality for
mixtures of bosonic and fermionic fields.
The statement of these theorems for bosons is simplier then when fermions are involved, since
The statement of these theorems for bosons is simpler then when fermions are involved, since
one does not have to worry about the minus-signs picked up on exchanging fields.
- type: p
content: "In this note we walk through the important parts of the proof of the three versions of
Wick's theorem for field operators containing carrying both fermionic and bosonic statitics,
Wick's theorem for field operators containing carrying both fermionic and bosonic statistics,
as it appears in PhysLean. Not every lemma or definition is covered here.
The aim is to give just enough that the story can be understood."
@ -289,7 +289,7 @@ parts:
docString: |
The type `CreateAnnihilate` is the type containing two elements `create` and `annihilate`.
This type is used to specify if an operator is a creation, or annihilation, operator
or the sum thereof or integral thereover etc.
or the sum thereof or integral thereof etc.
declString: |
inductive CreateAnnihilate where
| create : CreateAnnihilate
@ -429,7 +429,7 @@ parts:
link: "https://github.com/HEPLean/PhysLean/blob/master/PhysLean/PerturbationTheory/FieldOpFreeAlgebra/Basic.lean#L43"
content: |
For mathematicial objects defined in relation to `FieldOpFreeAlgebra` the postfix `F`
For mathematical objects defined in relation to `FieldOpFreeAlgebra` the postfix `F`
may be given to
their names to indicate that they are related to the free algebra.
This is to avoid confusion when working within the context of `FieldOpAlgebra` which is defined
@ -1225,7 +1225,7 @@ parts:
isThm: false
docString: |
For a field specification `𝓕`, and a list `φs` of `𝓕.CrAnFieldOp`,
`𝓕.normalOrderList φs` is the list `φs` normal-ordered using ther
`𝓕.normalOrderList φs` is the list `φs` normal-ordered using the
insertion sort algorithm. It puts creation operators on the left and annihilation operators on
the right. For example: