From 256a1c3e94df78be6329b7161386a963b74fa923 Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Tue, 4 Feb 2025 15:53:27 +0000 Subject: [PATCH] refactor: Note --- .../FieldOpAlgebra/WicksTheorem.lean | 18 +++++++++++++----- .../FieldOpFreeAlgebra/Basic.lean | 8 +++++++- .../FieldStatistics/Basic.lean | 3 ++- .../WickContraction/Card.lean | 3 +++ scripts/MetaPrograms/notes.lean | 14 ++------------ 5 files changed, 27 insertions(+), 19 deletions(-) diff --git a/HepLean/PerturbationTheory/FieldOpAlgebra/WicksTheorem.lean b/HepLean/PerturbationTheory/FieldOpAlgebra/WicksTheorem.lean index 80622e4..c3e58f1 100644 --- a/HepLean/PerturbationTheory/FieldOpAlgebra/WicksTheorem.lean +++ b/HepLean/PerturbationTheory/FieldOpAlgebra/WicksTheorem.lean @@ -342,11 +342,19 @@ lemma wicks_theorem_congr {φs φs' : List 𝓕.FieldOp} (h : φs = φs') : simp remark wicks_theorem_context := " - Wick's theorem is one of the most important results in perturbative quantum field theory. - It expresses a time-ordered product of fields as a sum of terms consisting of - time-contractions of pairs of fields multiplied by the normal-ordered product of - the remaining fields. Wick's theorem is also the precursor to the diagrammatic - approach to quantum field theory called Feynman diagrams." + In perturbation 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 + to Feynman diagrams. + + There is are actually three different versions of Wick's theorem used. + The static version, the time-dependent version, and the normal-ordered time-dependent version. + HepLean 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 + one does not have to worry about the minus-signs picked up on exchanging fields." /-- Wick's theorem for time-ordered products of bosonic and fermionic fields. The time ordered product `T(φ₀φ₁…φₙ)` is equal to the sum of terms, diff --git a/HepLean/PerturbationTheory/FieldOpFreeAlgebra/Basic.lean b/HepLean/PerturbationTheory/FieldOpFreeAlgebra/Basic.lean index 30d6f70..f20cc45 100644 --- a/HepLean/PerturbationTheory/FieldOpFreeAlgebra/Basic.lean +++ b/HepLean/PerturbationTheory/FieldOpFreeAlgebra/Basic.lean @@ -35,7 +35,7 @@ namespace FieldSpecification variable {𝓕 : FieldSpecification} /-- For a field specification `𝓕`, the algebra `𝓕.FieldOpFreeAlgebra` is - the algebra generated by creation and annihilation parts of field operators defined in + the free algebra generated by creation and annihilation parts of field operators defined in `𝓕.CrAnFieldOp`. It represents the algebra containing all possible products and linear combinations of creation and annihilation parts of field operators, without imposing any conditions. @@ -44,6 +44,12 @@ abbrev FieldOpFreeAlgebra (𝓕 : FieldSpecification) : Type := FreeAlgebra ℂ namespace FieldOpFreeAlgebra +remark naming_convention := " + For mathematicial objects defined in relation to `FieldOpFreeAlgebra` we will often postfix + their names with an `F` 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 + as a quotient of `FieldOpFreeAlgebra`." + /-- Maps a creation and annihlation state to the creation and annihlation free-algebra. -/ def ofCrAnOpF (φ : 𝓕.CrAnFieldOp) : FieldOpFreeAlgebra 𝓕 := FreeAlgebra.ι ℂ φ diff --git a/HepLean/PerturbationTheory/FieldStatistics/Basic.lean b/HepLean/PerturbationTheory/FieldStatistics/Basic.lean index 90c5066..c8d28eb 100644 --- a/HepLean/PerturbationTheory/FieldStatistics/Basic.lean +++ b/HepLean/PerturbationTheory/FieldStatistics/Basic.lean @@ -26,7 +26,8 @@ namespace FieldStatistic variable {𝓕 : Type} -/-- Field statistics form a commuative group isomorphic to `ℤ₂`. -/ +/-- Field statistics form a commuative group isomorphic to `ℤ₂` in which `bosonic` is the identity + and `fermionic` is the non-trivial element. -/ @[simp] instance : CommGroup FieldStatistic where one := bosonic diff --git a/HepLean/PerturbationTheory/WickContraction/Card.lean b/HepLean/PerturbationTheory/WickContraction/Card.lean index ac1c197..275c361 100644 --- a/HepLean/PerturbationTheory/WickContraction/Card.lean +++ b/HepLean/PerturbationTheory/WickContraction/Card.lean @@ -236,6 +236,9 @@ def cardFun : ℕ → ℕ | 1 => 1 | Nat.succ (Nat.succ n) => cardFun (Nat.succ n) + (n + 1) * cardFun n +/-- The number of Wick contractions for `n : ℕ` fields, i.e. the cardinality of + `WickContraction n`, is equal to the terms in + Online Encyclopedia of Integer Sequences (OEIS) A000085. -/ theorem card_eq_cardFun : (n : ℕ) → Fintype.card (WickContraction n) = cardFun n | 0 => by decide | 1 => by decide diff --git a/scripts/MetaPrograms/notes.lean b/scripts/MetaPrograms/notes.lean index 2792bfa..efa8d8e 100644 --- a/scripts/MetaPrograms/notes.lean +++ b/scripts/MetaPrograms/notes.lean @@ -125,28 +125,18 @@ def perturbationTheory : Note where as it appears in HepLean. We start with some basic definitions.", .h1 "Field operators", .h2 "Field statistics", - .p "A quantum field can either be a bosonic or fermionic. This information is - contained in the inductive type `FieldStatistic`. This is defined as follows:", .name `FieldStatistic, - .p "Field statistics form a commuative group isomorphic to ℤ₂, with - the bosonic element of `FieldStatistic` being the identity element.", - .p "Most of our use of field statistics will come by comparing two field statistics - and picking up a minus sign when they are both fermionic. This concept is - made precise using the notion of an exchange sign, defined as:", + .name `FieldStatistic.instCommGroup, .name `FieldStatistic.exchangeSign, - .p "We use the notation `𝓢(a,b)` as shorthand for the exchange sign of `a` and `b`.", .h2 "Field specifications", .name `fieldSpecification_intro, .name `FieldSpecification, - .p "Some examples of `FieldSpecification`s are given below:", - .name `FieldSpecification.singleBoson, - .name `FieldSpecification.singleFermion, - .name `FieldSpecification.doubleBosonDoubleFermion, .h2 "Field operators", .name `FieldSpecification.FieldOp, .name `FieldSpecification.CrAnFieldOp, .h2 "Field-operator free algebra", .name `FieldSpecification.FieldOpFreeAlgebra, + .name `FieldSpecification.FieldOpFreeAlgebra.naming_convention, .name `FieldSpecification.FieldOpFreeAlgebra.superCommuteF, .h2 "Field-operator algebra", .name `FieldSpecification.FieldOpAlgebra,