cleanup
This commit is contained in:
Pietro Monticone
parent
19cb08e05b
commit
89baced65e
14 changed files with 26 additions and 26 deletions
|
|
@ -86,7 +86,7 @@ lemma Bi_sum_quad (i : Fin 11) (f : Fin 11 → ℚ) :
|
|||
rw [quadBiLin.map_smul₂, Bi_Bj_quad hij.symm]
|
||||
exact Rat.mul_zero (f k)
|
||||
|
||||
/-- The coefficents of the quadratic equation in our basis. -/
|
||||
/-- The coefficients of the quadratic equation in our basis. -/
|
||||
@[simp]
|
||||
def quadCoeff : Fin 11 → ℚ := ![1, 1, 1, 1, 1, 1, 1, 1, 1, 0, 0]
|
||||
|
||||
|
|
|
|||
|
|
@ -148,7 +148,7 @@ lemma left_eq_neg_right : P.toFun Φ1 (- Φ1) =
|
|||
See e.g. https://inspirehep.net/literature/201299 and
|
||||
https://arxiv.org/pdf/hep-ph/0605184. -/
|
||||
|
||||
/-- The proposition on the coefficents for a potential to be bounded. -/
|
||||
/-- The proposition on the coefficients for a potential to be bounded. -/
|
||||
def IsBounded : Prop :=
|
||||
∃ c, ∀ Φ1 Φ2 x, c ≤ P.toFun Φ1 Φ2 x
|
||||
|
||||
|
|
|
|||
|
|
@ -208,7 +208,7 @@ instance isFull_decidable : Decidable c.IsFull := by
|
|||
apply decidable_of_decidable_of_iff hn.symm
|
||||
|
||||
/-- A structure specifying when a type `I` and a map `f :I → Type` corresponds to
|
||||
the splitting of a fields `φ` into a creation `n` and annihlation part `p`. -/
|
||||
the splitting of a fields `φ` into a creation `n` and annihilation part `p`. -/
|
||||
structure Splitting (f : 𝓕 → Type) [∀ i, Fintype (f i)]
|
||||
(le : (Σ i, f i) → (Σ i, f i) → Prop) [DecidableRel le] where
|
||||
/-- The creation part of the fields. The label `n` corresponds to the fact that
|
||||
|
|
@ -217,9 +217,9 @@ structure Splitting (f : 𝓕 → Type) [∀ i, Fintype (f i)]
|
|||
/-- The annhilation part of the fields. The label `p` corresponds to the fact that
|
||||
in normal ordering these feilds get pushed to the positive (right) direction. -/
|
||||
𝓑p : 𝓕 → (Σ i, f i)
|
||||
/-- The complex coefficent of creation part of a field `i`. This is usually `0` or `1`. -/
|
||||
/-- The complex coefficient of creation part of a field `i`. This is usually `0` or `1`. -/
|
||||
𝓧n : 𝓕 → ℂ
|
||||
/-- The complex coefficent of annhilation part of a field `i`. This is usually `0` or `1`. -/
|
||||
/-- The complex coefficient of annhilation part of a field `i`. This is usually `0` or `1`. -/
|
||||
𝓧p : 𝓕 → ℂ
|
||||
h𝓑 : ∀ i, ofListLift f [i] 1 = ofList [𝓑n i] (𝓧n i) + ofList [𝓑p i] (𝓧p i)
|
||||
h𝓑n : ∀ i j, le (𝓑n i) j
|
||||
|
|
|
|||
|
|
@ -7,11 +7,11 @@ import Mathlib.Order.Defs.Unbundled
|
|||
import Mathlib.Data.Fintype.Basic
|
||||
/-!
|
||||
|
||||
# Creation and annihlation parts of fields
|
||||
# Creation and annihilation parts of fields
|
||||
|
||||
-/
|
||||
|
||||
/-- The type specifing whether an operator is a creation or annihilation operator. -/
|
||||
/-- The type specifying whether an operator is a creation or annihilation operator. -/
|
||||
inductive CreateAnnihilate where
|
||||
| create : CreateAnnihilate
|
||||
| annihilate : CreateAnnihilate
|
||||
|
|
@ -29,7 +29,7 @@ instance : Fintype CreateAnnihilate where
|
|||
· refine Finset.insert_eq_self.mp ?_
|
||||
exact rfl
|
||||
|
||||
/-- The normal ordering on creation and annihlation operators.
|
||||
/-- The normal ordering on creation and annihilation operators.
|
||||
Creation operators are put to the left. -/
|
||||
def normalOrder : CreateAnnihilate → CreateAnnihilate → Prop
|
||||
| create, create => True
|
||||
|
|
|
|||
|
|
@ -33,7 +33,7 @@ def AsymptoticPosTime : Type := 𝓕.Fields × Lorentz.Contr 4
|
|||
/-- States specified by a field and a space-time position. -/
|
||||
def PositionStates : Type := 𝓕.Fields × SpaceTime
|
||||
|
||||
/-- The combintation of asymptotic states and position states. -/
|
||||
/-- The combination of asymptotic states and position states. -/
|
||||
inductive States (𝓕 : FieldStruct) where
|
||||
| negAsymp : 𝓕.AsymptoticNegTime → 𝓕.States
|
||||
| position : 𝓕.PositionStates → 𝓕.States
|
||||
|
|
|
|||
|
|
@ -7,15 +7,15 @@ import HepLean.PerturbationTheory.FieldStruct.Basic
|
|||
import HepLean.PerturbationTheory.CreateAnnihilate
|
||||
/-!
|
||||
|
||||
# Creation and annihlation parts of fields
|
||||
# Creation and annihilation parts of fields
|
||||
|
||||
-/
|
||||
|
||||
namespace FieldStruct
|
||||
variable (𝓕 : FieldStruct)
|
||||
|
||||
/-- To each state the specificaition of the type of creation and annihlation parts.
|
||||
For asymptotic staes there is only one allowed part, whilst for position states
|
||||
/-- To each state the specification of the type of creation and annihilation parts.
|
||||
For asymptotic states there is only one allowed part, whilst for position states
|
||||
there is two. -/
|
||||
def statesToCreateAnnihilateType : 𝓕.States → Type
|
||||
| States.negAsymp _ => Unit
|
||||
|
|
@ -42,19 +42,19 @@ def statesToCreateAnnihilateTypeCongr : {i j : 𝓕.States} → i = j →
|
|||
𝓕.statesToCreateAnnihilateType i ≃ 𝓕.statesToCreateAnnihilateType j
|
||||
| _, _, rfl => Equiv.refl _
|
||||
|
||||
/-- A creation and annihlation state is a state plus an valid specification of the
|
||||
/-- A creation and annihilation state is a state plus an valid specification of the
|
||||
creation or annihliation part of that state. (For asympotic states there is only one valid
|
||||
choice). -/
|
||||
def CreateAnnihilateStates : Type := Σ (s : 𝓕.States), 𝓕.statesToCreateAnnihilateType s
|
||||
|
||||
/-- The map from creation and annihlation states to their underlying states. -/
|
||||
/-- The map from creation and annihilation states to their underlying states. -/
|
||||
def createAnnihilateStatesToStates : 𝓕.CreateAnnihilateStates → 𝓕.States := Sigma.fst
|
||||
|
||||
@[simp]
|
||||
lemma createAnnihilateStatesToStates_prod (s : 𝓕.States) (t : 𝓕.statesToCreateAnnihilateType s) :
|
||||
𝓕.createAnnihilateStatesToStates ⟨s, t⟩ = s := rfl
|
||||
|
||||
/-- The map from creation and annihlation states to the type `CreateAnnihilate`
|
||||
/-- The map from creation and annihilation states to the type `CreateAnnihilate`
|
||||
specifying if a state is a creation or an annihilation state. -/
|
||||
def createAnnihlateStatesToCreateAnnihilate : 𝓕.CreateAnnihilateStates → CreateAnnihilate
|
||||
| ⟨States.negAsymp _, _⟩ => CreateAnnihilate.create
|
||||
|
|
@ -62,7 +62,7 @@ def createAnnihlateStatesToCreateAnnihilate : 𝓕.CreateAnnihilateStates → Cr
|
|||
| ⟨States.position _, CreateAnnihilate.annihilate⟩ => CreateAnnihilate.annihilate
|
||||
| ⟨States.posAsymp _, _⟩ => CreateAnnihilate.annihilate
|
||||
|
||||
/-- The normal ordering on creation and annihlation states. -/
|
||||
/-- The normal ordering on creation and annihilation states. -/
|
||||
def normalOrder : 𝓕.CreateAnnihilateStates → 𝓕.CreateAnnihilateStates → Prop :=
|
||||
fun a b => CreateAnnihilate.normalOrder (𝓕.createAnnihlateStatesToCreateAnnihilate a)
|
||||
(𝓕.createAnnihlateStatesToCreateAnnihilate b)
|
||||
|
|
|
|||
|
|
@ -7,7 +7,7 @@ import HepLean.PerturbationTheory.FieldStruct.CreateAnnihilate
|
|||
import HepLean.PerturbationTheory.CreateAnnihilate
|
||||
/-!
|
||||
|
||||
# Creation and annihlation sections
|
||||
# Creation and annihilation sections
|
||||
|
||||
-/
|
||||
|
||||
|
|
@ -68,7 +68,7 @@ def cons {φ : 𝓕.States} (ψ : 𝓕.statesToCreateAnnihilateType φ) (ψs : C
|
|||
CreateAnnihilateSect (φ :: φs) := ⟨⟨φ, ψ⟩ :: ψs.1, by
|
||||
simp [List.map_cons, ψs.2]⟩
|
||||
|
||||
/-- The creation and annihlation sections for a singleton list is given by
|
||||
/-- The creation and annihilation sections for a singleton list is given by
|
||||
a choice of `𝓕.statesToCreateAnnihilateType φ`. If `φ` is a asymptotic state
|
||||
there is no choice here, else there are two choices. -/
|
||||
def singletonEquiv {φ : 𝓕.States} : CreateAnnihilateSect [φ] ≃
|
||||
|
|
|
|||
|
|
@ -17,8 +17,8 @@ open FieldStatistic
|
|||
/-- The sections of `Σ i, f i` over a list `φs : List 𝓕`.
|
||||
In terms of physics, given some fields `φ₁...φₙ`, the different ways one can associate
|
||||
each field as a `creation` or an `annilation` operator. E.g. the number of terms
|
||||
`φ₁⁰φ₂¹...φₙ⁰` `φ₁¹φ₂¹...φₙ⁰` etc. If some fields are exclusively creation or annhilation
|
||||
operators at this point (e.g. ansymptotic states) this is accounted for. -/
|
||||
`φ₁⁰φ₂¹...φₙ⁰` `φ₁¹φ₂¹...φₙ⁰` etc. If some fields are exclusively creation or annihilation
|
||||
operators at this point (e.g. asymptotic states) this is accounted for. -/
|
||||
def CreateAnnihilateSect {𝓕 : Type} (f : 𝓕 → Type) (φs : List 𝓕) : Type :=
|
||||
Π i, f (φs.get i)
|
||||
|
||||
|
|
|
|||
|
|
@ -93,7 +93,7 @@ lemma sumFiber_ι (f : 𝓕 → Type) [∀ i, Fintype (f i)] (i : 𝓕) :
|
|||
/-- Given a list `l : List I` the corresponding element of `FreeAlgebra ℂ (Σ i, f i)`
|
||||
by mapping each `i : I` to the sum of it's fiber in `Σ i, f i` and taking the product of the
|
||||
result.
|
||||
For example, in terms of creation and annihlation opperators,
|
||||
For example, in terms of creation and annihilation opperators,
|
||||
`[φ₁, φ₂, φ₃]` gets taken to `(φ₁⁰ + φ₁¹)(φ₂⁰ + φ₂¹)(φ₃⁰ + φ₃¹)`.
|
||||
-/
|
||||
def ofListLift (f : 𝓕 → Type) [∀ i, Fintype (f i)] (l : List 𝓕) (x : ℂ) :
|
||||
|
|
|
|||
|
|
@ -23,7 +23,7 @@ variable {𝓕 : Type}
|
|||
if two fields are of a different grade then their super commutor lands on zero,
|
||||
and the `koszulOrder` (normal order) of any term with a super commutor of two fields present
|
||||
is zero.
|
||||
This can be thought as as a condtion on the operator algebra `A` as much as it can
|
||||
This can be thought as as a condition on the operator algebra `A` as much as it can
|
||||
on `F`. -/
|
||||
class OperatorMap {A : Type} [Semiring A] [Algebra ℂ A]
|
||||
(q : 𝓕 → FieldStatistic) (le : 𝓕 → 𝓕 → Prop)
|
||||
|
|
|
|||
|
|
@ -20,7 +20,7 @@ section
|
|||
|
||||
## Basic properties of lists
|
||||
|
||||
To be replaced with Mathlib or Lean definitions when/where appropraite.
|
||||
To be replaced with Mathlib or Lean definitions when/where appropriate.
|
||||
-/
|
||||
|
||||
lemma take_insert_same {I : Type} (i : I) :
|
||||
|
|
|
|||
|
|
@ -6,7 +6,7 @@ Authors: Joseph Tooby-Smith
|
|||
import HepLean.PerturbationTheory.Wick.Signs.KoszulSign
|
||||
/-!
|
||||
|
||||
# Static wick coefficent
|
||||
# Static wick coefficient
|
||||
|
||||
-/
|
||||
|
||||
|
|
|
|||
|
|
@ -6,7 +6,7 @@ Authors: Joseph Tooby-Smith
|
|||
import HepLean.PerturbationTheory.FieldStatistics
|
||||
/-!
|
||||
|
||||
# Super commutation coefficent.
|
||||
# Super commutation coefficient.
|
||||
|
||||
This is a complex number which is `-1` when commuting two fermionic operators and `1` otherwise.
|
||||
|
||||
|
|
|
|||
|
|
@ -264,7 +264,7 @@ lemma pos_𝓵_sol_exists_iff (h𝓵 : 0 < P.𝓵) (c : ℝ) : (∃ φ x, P.toFu
|
|||
|
||||
-/
|
||||
|
||||
/-- The proposition on the coefficents for a potential to be bounded. -/
|
||||
/-- The proposition on the coefficients for a potential to be bounded. -/
|
||||
def IsBounded : Prop :=
|
||||
∃ c, ∀ Φ x, c ≤ P.toFun Φ x
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue