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

refactor: Rename States to FieldOps

Browse source
This commit is contained in:
jstoobysmith 2025-02-03 11:28:14 +00:00
parent 171e80fc04
commit 8f41de5785
36 changed files with 946 additions and 946 deletions
Download patch file Download diff file Expand all files Collapse all files

30
HepLean/PerturbationTheory/FieldSpecification/Basic.lean
View file

@ -16,7 +16,7 @@ In this module is the definition of a field specification.
A field specification is a structure consisting of a type of fields and a
the field statistics of each field.
From each field we can create three different types of `States`.
From each field we can create three different types of `FieldOp`.
- Negative asymptotic states.
- Position states.
- Positive asymptotic states.
@ -52,27 +52,27 @@ def IncomingAsymptotic : Type := 𝓕.Fields × Lorentz.Contr 4
def OutgoingAsymptotic : Type := 𝓕.Fields × Lorentz.Contr 4
/-- A position state is a field and a space-time position. -/
def PositionStates : Type := 𝓕.Fields × SpaceTime
def PositionFieldOp : Type := 𝓕.Fields × SpaceTime
/-- The type States is the inductive type combining the asymptotic states and position states. -/
inductive States (𝓕 : FieldSpecification) where
| inAsymp : 𝓕.IncomingAsymptotic → 𝓕.States
| position : 𝓕.PositionStates → 𝓕.States
| outAsymp : 𝓕.OutgoingAsymptotic → 𝓕.States
/-- The type FieldOp is the inductive type combining the asymptotic states and position states. -/
inductive FieldOp (𝓕 : FieldSpecification) where
| inAsymp : 𝓕.IncomingAsymptotic → 𝓕.FieldOp
| position : 𝓕.PositionFieldOp → 𝓕.FieldOp
| outAsymp : 𝓕.OutgoingAsymptotic → 𝓕.FieldOp
/-- Taking a state to its underlying field. -/
def statesToField : 𝓕.States → 𝓕.Fields
| States.inAsymp φ => φ.1
| States.position φ => φ.1
| States.outAsymp φ => φ.1
def fieldOpToField : 𝓕.FieldOp → 𝓕.Fields
| FieldOp.inAsymp φ => φ.1
| FieldOp.position φ => φ.1
| FieldOp.outAsymp φ => φ.1
/-- The bool on `States` which is true only for position states. -/
def statesIsPosition : 𝓕.States → Bool
| States.position _ => true
/-- The bool on `FieldOp` which is true only for position states. -/
def statesIsPosition : 𝓕.FieldOp → Bool
| FieldOp.position _ => true
| _ => false
/-- The statistics associated to a state. -/
def statesStatistic : 𝓕.States → FieldStatistic := 𝓕.statistics ∘ 𝓕.statesToField
def statesStatistic : 𝓕.FieldOp → FieldStatistic := 𝓕.statistics ∘ 𝓕.fieldOpToField
/-- The field statistics associated with a state. -/
scoped[FieldSpecification] notation 𝓕 "|>ₛ" φ => statesStatistic 𝓕 φ

102
HepLean/PerturbationTheory/FieldSpecification/CrAnFieldOp.lean Normal file
View file

@ -0,0 +1,102 @@
/-
Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.PerturbationTheory.FieldSpecification.Basic
import HepLean.PerturbationTheory.CreateAnnihilate
/-!
# Creation and annihilation states
Called `CrAnFieldOp` for short here.
Given a field specification, in addition to defining states
(see: `HepLean.PerturbationTheory.FieldSpecification.Basic`),
we can also define creation and annihilation states.
These are similar to states but come with an additional specification of whether they correspond to
creation or annihilation operators.
In particular we have the following creation and annihilation states for each field:
- Negative asymptotic states - with the implicit specification that it is a creation state.
- Position states with a creation specification.
- Position states with an annihilation specification.
- Positive asymptotic states - with the implicit specification that it is an annihilation state.
In this module in addition to defining `CrAnFieldOp` we also define some maps:
- The map `crAnFieldOpToFieldOp` takes a `CrAnFieldOp` to its state in `FieldOp`.
- The map `crAnFieldOpToCreateAnnihilate` takes a `CrAnFieldOp` to its corresponding
`CreateAnnihilate` value.
- The map `crAnStatistics` takes a `CrAnFieldOp` to its corresponding `FieldStatistic`
(bosonic or fermionic).
-/
namespace FieldSpecification
variable (𝓕 : FieldSpecification)
/-- 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
there is two. -/
def fieldOpToCrAnType : 𝓕.FieldOp → Type
| FieldOp.inAsymp _ => Unit
| FieldOp.position _ => CreateAnnihilate
| FieldOp.outAsymp _ => Unit
/-- The instance of a finite type on `𝓕.fieldOpToCreateAnnihilateType i`. -/
instance : ∀ i, Fintype (𝓕.fieldOpToCrAnType i) := fun i =>
match i with
| FieldOp.inAsymp _ => inferInstanceAs (Fintype Unit)
| FieldOp.position _ => inferInstanceAs (Fintype CreateAnnihilate)
| FieldOp.outAsymp _ => inferInstanceAs (Fintype Unit)
/-- The instance of a decidable equality on `𝓕.fieldOpToCreateAnnihilateType i`. -/
instance : ∀ i, DecidableEq (𝓕.fieldOpToCrAnType i) := fun i =>
match i with
| FieldOp.inAsymp _ => inferInstanceAs (DecidableEq Unit)
| FieldOp.position _ => inferInstanceAs (DecidableEq CreateAnnihilate)
| FieldOp.outAsymp _ => inferInstanceAs (DecidableEq Unit)
/-- The equivalence between `𝓕.fieldOpToCreateAnnihilateType i` and
`𝓕.fieldOpToCreateAnnihilateType j` from an equality `i = j`. -/
def fieldOpToCreateAnnihilateTypeCongr : {i j : 𝓕.FieldOp} → i = j →
𝓕.fieldOpToCrAnType i ≃ 𝓕.fieldOpToCrAnType j
| _, _, rfl => Equiv.refl _
/-- A creation and annihlation 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 CrAnFieldOp : Type := Σ (s : 𝓕.FieldOp), 𝓕.fieldOpToCrAnType s
/-- The map from creation and annihlation states to their underlying states. -/
def crAnFieldOpToFieldOp : 𝓕.CrAnFieldOp → 𝓕.FieldOp := Sigma.fst
@[simp]
lemma crAnFieldOpToFieldOp_prod (s : 𝓕.FieldOp) (t : 𝓕.fieldOpToCrAnType s) :
𝓕.crAnFieldOpToFieldOp ⟨s, t⟩ = s := rfl
/-- The map from creation and annihlation states to the type `CreateAnnihilate`
specifying if a state is a creation or an annihilation state. -/
def crAnFieldOpToCreateAnnihilate : 𝓕.CrAnFieldOp → CreateAnnihilate
| ⟨FieldOp.inAsymp _, _⟩ => CreateAnnihilate.create
| ⟨FieldOp.position _, CreateAnnihilate.create⟩ => CreateAnnihilate.create
| ⟨FieldOp.position _, CreateAnnihilate.annihilate⟩ => CreateAnnihilate.annihilate
| ⟨FieldOp.outAsymp _, _⟩ => CreateAnnihilate.annihilate
/-- Takes a `CrAnFieldOp` state to its corresponding fields statistic (bosonic or fermionic). -/
def crAnStatistics : 𝓕.CrAnFieldOp → FieldStatistic :=
𝓕.statesStatistic ∘ 𝓕.crAnFieldOpToFieldOp
/-- The field statistic of a `CrAnState`. -/
scoped[FieldSpecification] notation 𝓕 "|>ₛ" φ =>
(crAnStatistics 𝓕) φ
/-- The field statistic of a list of `CrAnState`s. -/
scoped[FieldSpecification] notation 𝓕 "|>ₛ" φ => FieldStatistic.ofList
(crAnStatistics 𝓕) φ
/-- The `CreateAnnihilate` value of a `CrAnState`s, i.e. whether it is a creation or
annihilation operator. -/
scoped[FieldSpecification] infixl:80 "|>ᶜ" =>
crAnFieldOpToCreateAnnihilate
end FieldSpecification

130
HepLean/PerturbationTheory/FieldSpecification/CrAnSection.lean
View file

@ -3,7 +3,7 @@ Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.PerturbationTheory.FieldSpecification.CrAnStates
import HepLean.PerturbationTheory.FieldSpecification.CrAnFieldOp
/-!
# Creation and annihlation sections
@ -11,13 +11,13 @@ import HepLean.PerturbationTheory.FieldSpecification.CrAnStates
In the module
`HepLean.PerturbationTheory.FieldSpecification.Basic`
we defined states for a field specification, and in the module
`HepLean.PerturbationTheory.FieldStatistics.CrAnStates`
we defined a refinement of states called `CrAnStates` which distinquishes between the
`HepLean.PerturbationTheory.FieldStatistics.CrAnFieldOp`
we defined a refinement of states called `CrAnFieldOp` which distinquishes between the
creation and annihilation components of states.
There exists, in particular, a map from `CrAnStates` to `States` called `crAnStatesToStates`.
There exists, in particular, a map from `CrAnFieldOp` to `FieldOp` called `crAnFieldOpToFieldOp`.
Given a list of `States`, `φs`, in this module we define a section of `φs` to be a list of
`CrAnStates`, `ψs`, such that under the map `crAnStatesToStates`, `ψs` is mapped to `φs`.
Given a list of `FieldOp`, `φs`, in this module we define a section of `φs` to be a list of
`CrAnFieldOp`, `ψs`, such that under the map `crAnFieldOpToFieldOp`, `ψs` is mapped to `φs`.
That is to say, the states underlying `ψs` are the states in `φs`.
We denote these sections as `CrAnSection φs`.
@ -31,30 +31,30 @@ In this module we define various properties of `CrAnSection`.
namespace FieldSpecification
variable {𝓕 : FieldSpecification}
/-- The sections in `𝓕.CrAnStates` over a list `φs : List 𝓕.States`.
/-- The sections in `𝓕.CrAnFieldOp` over a list `φs : List 𝓕.FieldOp`.
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. -/
def CrAnSection (φs : List 𝓕.States) : Type :=
{ψs : List 𝓕.CrAnStates // ψs.map 𝓕.crAnStatesToStates = φs}
-- Π i, 𝓕.statesToCreateAnnihilateType (φs.get i)
def CrAnSection (φs : List 𝓕.FieldOp) : Type :=
{ψs : List 𝓕.CrAnFieldOp // ψs.map 𝓕.crAnFieldOpToFieldOp = φs}
-- Π i, 𝓕.fieldOpToCreateAnnihilateType (φs.get i)
namespace CrAnSection
open FieldStatistic
variable {𝓕 : FieldSpecification} {φs : List 𝓕.States}
variable {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp}
@[simp]
lemma length_eq (ψs : CrAnSection φs) : ψs.1.length = φs.length := by
simpa using congrArg List.length ψs.2
/-- The tail of a section for `φs`. -/
def tail : {φs : List 𝓕.States} → (ψs : CrAnSection φs) → CrAnSection φs.tail
def tail : {φs : List 𝓕.FieldOp} → (ψs : CrAnSection φs) → CrAnSection φs.tail
| [], ⟨[], h⟩ => ⟨[], h⟩
| φ :: φs, ⟨[], h⟩ => False.elim (by simp at h)
| φ :: φs, ⟨ψ :: ψs, h⟩ => ⟨ψs, by rw [List.map_cons, List.cons.injEq] at h; exact h.2⟩
lemma head_state_eq {φ : 𝓕.States} : (ψs : CrAnSection (φ :: φs)) →
lemma head_state_eq {φ : 𝓕.FieldOp} : (ψs : CrAnSection (φ :: φs)) →
(ψs.1.head (by simp [← List.length_pos_iff_ne_nil])).1 = φ
| ⟨[], h⟩ => False.elim (by simp at h)
| ⟨ψ :: ψs, h⟩ => by
@ -72,14 +72,14 @@ lemma take_statistics_eq_take_state_statistics (ψs : CrAnSection φs) n :
simp only [instCommGroup, List.map_take]
rw [← List.map_comp_map, Function.comp_apply, ψs.2]
/-- The head of a section for `φ :: φs` as an element in `𝓕.statesToCreateAnnihilateType φ`. -/
def head : {φ : 𝓕.States} → (ψs : CrAnSection (φ :: φs)) →
𝓕.statesToCrAnType φ
/-- The head of a section for `φ :: φs` as an element in `𝓕.fieldOpToCreateAnnihilateType φ`. -/
def head : {φ : 𝓕.FieldOp} → (ψs : CrAnSection (φ :: φs)) →
𝓕.fieldOpToCrAnType φ
| φ, ⟨[], h⟩ => False.elim (by simp at h)
| φ, ⟨ψ :: ψs, h⟩ => 𝓕.statesToCreateAnnihilateTypeCongr (by
| φ, ⟨ψ :: ψs, h⟩ => 𝓕.fieldOpToCreateAnnihilateTypeCongr (by
simpa using head_state_eq ⟨ψ :: ψs, h⟩) ψ.2
lemma eq_head_cons_tail {φ : 𝓕.States} {ψs : CrAnSection (φ :: φs)} :
lemma eq_head_cons_tail {φ : 𝓕.FieldOp} {ψs : CrAnSection (φ :: φs)} :
ψs.1 = ⟨φ, head ψs⟩ :: ψs.tail.1 := by
match ψs with
| ⟨[], h⟩ => exact False.elim (by simp at h)
@ -90,13 +90,13 @@ lemma eq_head_cons_tail {φ : 𝓕.States} {ψs : CrAnSection (φ :: φs)} :
rfl
/-- The creation of a section from for `φ : φs` from a section for `φs` and a
element of `𝓕.statesToCreateAnnihilateType φ`. -/
def cons {φ : 𝓕.States} (ψ : 𝓕.statesToCrAnType φ) (ψs : CrAnSection φs) :
element of `𝓕.fieldOpToCreateAnnihilateType φ`. -/
def cons {φ : 𝓕.FieldOp} (ψ : 𝓕.fieldOpToCrAnType φ) (ψs : CrAnSection φs) :
CrAnSection (φ :: φs) := ⟨⟨φ, ψ⟩ :: ψs.1, by
simp [List.map_cons, ψs.2]⟩
/-- For the empty list of states there is only one `CrAnSection`. Corresponding to the
empty list of `CrAnStates`. -/
empty list of `CrAnFieldOp`. -/
def nilEquiv : CrAnSection (𝓕 := 𝓕) [] ≃ Unit where
toFun _ := ()
invFun _ := ⟨[], rfl⟩
@ -108,10 +108,10 @@ def nilEquiv : CrAnSection (𝓕 := 𝓕) [] ≃ Unit where
simp
/-- The creation and annihlation sections for a singleton list is given by
a choice of `𝓕.statesToCreateAnnihilateType φ`. If `φ` is a asymptotic state
a choice of `𝓕.fieldOpToCreateAnnihilateType φ`. If `φ` is a asymptotic state
there is no choice here, else there are two choices. -/
def singletonEquiv {φ : 𝓕.States} : CrAnSection [φ] ≃
𝓕.statesToCrAnType φ where
def singletonEquiv {φ : 𝓕.FieldOp} : CrAnSection [φ] ≃
𝓕.fieldOpToCrAnType φ where
toFun ψs := ψs.head
invFun ψ := ⟨[⟨φ, ψ⟩], by simp⟩
left_inv ψs := by
@ -128,8 +128,8 @@ def singletonEquiv {φ : 𝓕.States} : CrAnSection [φ] ≃
/-- An equivalence seperating the head of a creation and annhilation section
from the tail. -/
def consEquiv {φ : 𝓕.States} {φs : List 𝓕.States} : CrAnSection (φ :: φs) ≃
𝓕.statesToCrAnType φ × CrAnSection φs where
def consEquiv {φ : 𝓕.FieldOp} {φs : List 𝓕.FieldOp} : CrAnSection (φ :: φs) ≃
𝓕.fieldOpToCrAnType φ × CrAnSection φs where
toFun ψs := ⟨ψs.head, ψs.tail⟩
invFun ψψs :=
match ψψs with
@ -143,7 +143,7 @@ def consEquiv {φ : 𝓕.States} {φs : List 𝓕.States} : CrAnSection (φ ::
/-- The instance of a finite type on `CrAnSection`s defined recursively through
`consEquiv`. -/
instance fintype : (φs : List 𝓕.States) → Fintype (CrAnSection φs)
instance fintype : (φs : List 𝓕.FieldOp) → Fintype (CrAnSection φs)
| [] => Fintype.ofEquiv _ nilEquiv.symm
| _ :: φs =>
haveI : Fintype (CrAnSection φs) := fintype φs
@ -154,34 +154,34 @@ lemma card_nil_eq : Fintype.card (CrAnSection (𝓕 := 𝓕) []) = 1 := by
rw [Fintype.ofEquiv_card nilEquiv.symm]
simp
lemma card_cons_eq {φ : 𝓕.States} {φs : List 𝓕.States} :
Fintype.card (CrAnSection (φ :: φs)) = Fintype.card (𝓕.statesToCrAnType φ) *
lemma card_cons_eq {φ : 𝓕.FieldOp} {φs : List 𝓕.FieldOp} :
Fintype.card (CrAnSection (φ :: φs)) = Fintype.card (𝓕.fieldOpToCrAnType φ) *
Fintype.card (CrAnSection φs) := by
rw [Fintype.ofEquiv_card consEquiv.symm]
simp
lemma card_eq_mul : {φs : List 𝓕.States} → Fintype.card (CrAnSection φs) =
lemma card_eq_mul : {φs : List 𝓕.FieldOp} → Fintype.card (CrAnSection φs) =
2 ^ (List.countP 𝓕.statesIsPosition φs)
| [] => by
simp
| States.position _ :: φs => by
| FieldOp.position _ :: φs => by
simp only [statesIsPosition, List.countP_cons_of_pos]
rw [card_cons_eq]
rw [card_eq_mul]
simp only [statesToCrAnType, CreateAnnihilate.CreateAnnihilate_card_eq_two]
simp only [fieldOpToCrAnType, CreateAnnihilate.CreateAnnihilate_card_eq_two]
ring
| States.inAsymp x_ :: φs => by
| FieldOp.inAsymp x_ :: φs => by
simp only [statesIsPosition, Bool.false_eq_true, not_false_eq_true, List.countP_cons_of_neg]
rw [card_cons_eq]
rw [card_eq_mul]
simp [statesToCrAnType]
| States.outAsymp _ :: φs => by
simp [fieldOpToCrAnType]
| FieldOp.outAsymp _ :: φs => by
simp only [statesIsPosition, Bool.false_eq_true, not_false_eq_true, List.countP_cons_of_neg]
rw [card_cons_eq]
rw [card_eq_mul]
simp [statesToCrAnType]
simp [fieldOpToCrAnType]
lemma card_perm_eq {φs φs' : List 𝓕.States} (h : φs.Perm φs') :
lemma card_perm_eq {φs φs' : List 𝓕.FieldOp} (h : φs.Perm φs') :
Fintype.card (CrAnSection φs) = Fintype.card (CrAnSection φs') := by
rw [card_eq_mul, card_eq_mul]
congr 1
@ -195,7 +195,7 @@ lemma sum_nil (f : CrAnSection (𝓕 := 𝓕) [] → M) [AddCommMonoid M] :
rfl
lemma sum_cons (f : CrAnSection (φ :: φs) → M) [AddCommMonoid M] :
∑ (s : CrAnSection (φ :: φs)), f s = ∑ (a : 𝓕.statesToCrAnType φ),
∑ (s : CrAnSection (φ :: φs)), f s = ∑ (a : 𝓕.fieldOpToCrAnType φ),
∑ (s : CrAnSection φs), f (cons a s) := by
rw [← consEquiv.symm.sum_comp, Fintype.sum_prod_type]
rfl
@ -208,24 +208,24 @@ lemma sum_over_length {s : CrAnSection φs} (f : Fin s.1.length → M)
/-- The equivalence between `CrAnSection φs` and
`CrAnSection φs'` induced by an equality `φs = φs'`. -/
def congr : {φs φs' : List 𝓕.States} → (h : φs = φs') →
def congr : {φs φs' : List 𝓕.FieldOp} → (h : φs = φs') →
CrAnSection φs ≃ CrAnSection φs'
| _, _, rfl => Equiv.refl _
@[simp]
lemma congr_fst {φs φs' : List 𝓕.States} (h : φs = φs') (ψs : CrAnSection φs) :
lemma congr_fst {φs φs' : List 𝓕.FieldOp} (h : φs = φs') (ψs : CrAnSection φs) :
(congr h ψs).1 = ψs.1 := by
cases h
rfl
@[simp]
lemma congr_symm {φs φs' : List 𝓕.States} (h : φs = φs') :
lemma congr_symm {φs φs' : List 𝓕.FieldOp} (h : φs = φs') :
(congr h).symm = congr h.symm := by
cases h
rfl
@[simp]
lemma congr_trans_apply {φs φs' φs'' : List 𝓕.States} (h1 : φs = φs') (h2 : φs' = φs'')
lemma congr_trans_apply {φs φs' φs'' : List 𝓕.FieldOp} (h1 : φs = φs') (h2 : φs' = φs'')
(ψs : CrAnSection φs) :
(congr h2 (congr h1 ψs)) = congr (by rw [h1, h2]) ψs := by
subst h1 h2
@ -236,7 +236,7 @@ def take (n : ℕ) (ψs : CrAnSection φs) : CrAnSection (φs.take n) :=
⟨ψs.1.take n, by simp [ψs.2]⟩
@[simp]
lemma take_congr {φs φs' : List 𝓕.States} (h : φs = φs') (n : ℕ)
lemma take_congr {φs φs' : List 𝓕.FieldOp} (h : φs = φs') (n : ℕ)
(ψs : CrAnSection φs) :
(take n (congr h ψs)) = congr (by rw [h]) (take n ψs) := by
subst h
@ -247,31 +247,31 @@ def drop (n : ℕ) (ψs : CrAnSection φs) : CrAnSection (φs.drop n) :=
⟨ψs.1.drop n, by simp [ψs.2]⟩
@[simp]
lemma drop_congr {φs φs' : List 𝓕.States} (h : φs = φs') (n : ℕ)
lemma drop_congr {φs φs' : List 𝓕.FieldOp} (h : φs = φs') (n : ℕ)
(ψs : CrAnSection φs) :
(drop n (congr h ψs)) = congr (by rw [h]) (drop n ψs) := by
subst h
rfl
/-- Appends two sections and their underlying lists. -/
def append {φs φs' : List 𝓕.States} (ψs : CrAnSection φs)
def append {φs φs' : List 𝓕.FieldOp} (ψs : CrAnSection φs)
(ψs' : CrAnSection φs') : CrAnSection (φs ++ φs') :=
⟨ψs.1 ++ ψs'.1, by simp [ψs.2, ψs'.2]⟩
lemma append_assoc {φs φs' φs'' : List 𝓕.States} (ψs : CrAnSection φs)
lemma append_assoc {φs φs' φs'' : List 𝓕.FieldOp} (ψs : CrAnSection φs)
(ψs' : CrAnSection φs') (ψs'' : CrAnSection φs'') :
append ψs (append ψs' ψs'') = congr (by simp) (append (append ψs ψs') ψs'') := by
apply Subtype.ext
simp [append]
lemma append_assoc' {φs φs' φs'' : List 𝓕.States} (ψs : CrAnSection φs)
lemma append_assoc' {φs φs' φs'' : List 𝓕.FieldOp} (ψs : CrAnSection φs)
(ψs' : CrAnSection φs') (ψs'' : CrAnSection φs'') :
(append (append ψs ψs') ψs'') = congr (by simp) (append ψs (append ψs' ψs'')) := by
apply Subtype.ext
simp [append]
lemma singletonEquiv_append_eq_cons {φs : List 𝓕.States} {φ : 𝓕.States}
(ψs : CrAnSection φs) (ψ : 𝓕.statesToCrAnType φ) :
lemma singletonEquiv_append_eq_cons {φs : List 𝓕.FieldOp} {φ : 𝓕.FieldOp}
(ψs : CrAnSection φs) (ψ : 𝓕.fieldOpToCrAnType φ) :
append (singletonEquiv.symm ψ) ψs = cons ψ ψs := by
apply Subtype.ext
simp [append, cons, singletonEquiv]
@ -282,35 +282,35 @@ lemma take_append_drop {n : ℕ} (ψs : CrAnSection φs) :
apply Subtype.ext
simp [take, drop, append]
lemma congr_append {φs1 φs1' φs2 φs2' : List 𝓕.States} (h1 : φs1 = φs1') (h2 : φs2 = φs2')
lemma congr_append {φs1 φs1' φs2 φs2' : List 𝓕.FieldOp} (h1 : φs1 = φs1') (h2 : φs2 = φs2')
(ψs1 : CrAnSection φs1) (ψs2 : CrAnSection φs2) :
(append (congr h1 ψs1) (congr h2 ψs2)) = congr (by rw [h1, h2]) (append ψs1 ψs2) := by
subst h1 h2
rfl
@[simp]
lemma congr_fst_append {φs1 φs1' φs2 : List 𝓕.States} (h1 : φs1 = φs1')
lemma congr_fst_append {φs1 φs1' φs2 : List 𝓕.FieldOp} (h1 : φs1 = φs1')
(ψs1 : CrAnSection φs1) (ψs2 : CrAnSection φs2) :
(append (congr h1 ψs1) (ψs2)) = congr (by rw [h1]) (append ψs1 ψs2) := by
subst h1
rfl
@[simp]
lemma congr_snd_append {φs1 φs2 φs2' : List 𝓕.States} (h2 : φs2 = φs2')
lemma congr_snd_append {φs1 φs2 φs2' : List 𝓕.FieldOp} (h2 : φs2 = φs2')
(ψs1 : CrAnSection φs1) (ψs2 : CrAnSection φs2) :
(append ψs1 (congr h2 ψs2)) = congr (by rw [h2]) (append ψs1 ψs2) := by
subst h2
rfl
@[simp]
lemma take_left {φs φs' : List 𝓕.States} (ψs : CrAnSection φs)
lemma take_left {φs φs' : List 𝓕.FieldOp} (ψs : CrAnSection φs)
(ψs' : CrAnSection φs') :
take φs.length (ψs.append ψs') = congr (by simp) ψs := by
apply Subtype.ext
simp [take, append]
@[simp]
lemma drop_left {φs φs' : List 𝓕.States} (ψs : CrAnSection φs)
lemma drop_left {φs φs' : List 𝓕.FieldOp} (ψs : CrAnSection φs)
(ψs' : CrAnSection φs') :
drop φs.length (ψs.append ψs') = congr (by simp) ψs' := by
apply Subtype.ext
@ -319,7 +319,7 @@ lemma drop_left {φs φs' : List 𝓕.States} (ψs : CrAnSection φs)
/-- The equivalence between `CrAnSection (φs ++ φs')` and
`CrAnSection φs × CrAnSection φs` formed by `append`, `take`
and `drop` and their interrelationship. -/
def appendEquiv {φs φs' : List 𝓕.States} : CrAnSection (φs ++ φs') ≃
def appendEquiv {φs φs' : List 𝓕.FieldOp} : CrAnSection (φs ++ φs') ≃
CrAnSection φs × CrAnSection φs' where
toFun ψs := (congr (List.take_left φs φs') (take φs.length ψs),
congr (List.drop_left φs φs') (drop φs.length ψs))
@ -349,8 +349,8 @@ def eraseIdx (n : ℕ) (ψs : CrAnSection φs) : CrAnSection (φs.eraseIdx n) :=
⟨ψs.1.eraseIdx n, by simp [ψs.2]⟩
/-- The equivalence formed by extracting an element from a section. -/
def eraseIdxEquiv (n : ℕ) (φs : List 𝓕.States) (hn : n < φs.length) :
CrAnSection φs ≃ 𝓕.statesToCrAnType φs[n] ×
def eraseIdxEquiv (n : ℕ) (φs : List 𝓕.FieldOp) (hn : n < φs.length) :
CrAnSection φs ≃ 𝓕.fieldOpToCrAnType φs[n] ×
CrAnSection (φs.eraseIdx n) :=
(congr (by simp only [List.take_concat_get', List.take_append_drop])).trans <|
appendEquiv.trans <|
@ -372,8 +372,8 @@ lemma eraseIdxEquiv_apply_snd {n : ℕ} (ψs : CrAnSection φs) (hn : n < φs.le
simp only [Nat.succ_eq_add_one, le_add_iff_nonneg_right, zero_le, inf_of_le_left]
exact Eq.symm (List.eraseIdx_eq_take_drop_succ ψs.1 n)
lemma eraseIdxEquiv_symm_eq_take_cons_drop {n : ℕ} (φs : List 𝓕.States) (hn : n < φs.length)
(a : 𝓕.statesToCrAnType φs[n]) (s : CrAnSection (φs.eraseIdx n)) :
lemma eraseIdxEquiv_symm_eq_take_cons_drop {n : ℕ} (φs : List 𝓕.FieldOp) (hn : n < φs.length)
(a : 𝓕.fieldOpToCrAnType φs[n]) (s : CrAnSection (φs.eraseIdx n)) :
(eraseIdxEquiv n φs hn).symm ⟨a, s⟩ =
congr (by
rw [HepLean.List.take_eraseIdx_same, HepLean.List.drop_eraseIdx_succ]
@ -394,8 +394,8 @@ lemma eraseIdxEquiv_symm_eq_take_cons_drop {n : ℕ} (φs : List 𝓕.States) (h
rw [hn]
@[simp]
lemma eraseIdxEquiv_symm_getElem {n : ℕ} (φs : List 𝓕.States) (hn : n < φs.length)
(a : 𝓕.statesToCrAnType φs[n]) (s : CrAnSection (φs.eraseIdx n)) :
lemma eraseIdxEquiv_symm_getElem {n : ℕ} (φs : List 𝓕.FieldOp) (hn : n < φs.length)
(a : 𝓕.fieldOpToCrAnType φs[n]) (s : CrAnSection (φs.eraseIdx n)) :
getElem ((eraseIdxEquiv n φs hn).symm ⟨a,s⟩).1 n
(by rw [length_eq]; exact hn) = ⟨φs[n], a⟩ := by
rw [eraseIdxEquiv_symm_eq_take_cons_drop]
@ -409,16 +409,16 @@ lemma eraseIdxEquiv_symm_getElem {n : ℕ} (φs : List 𝓕.States) (hn : n < φ
simp [h0]
@[simp]
lemma eraseIdxEquiv_symm_eraseIdx {n : ℕ} (φs : List 𝓕.States) (hn : n < φs.length)
(a : 𝓕.statesToCrAnType φs[n]) (s : CrAnSection (φs.eraseIdx n)) :
lemma eraseIdxEquiv_symm_eraseIdx {n : ℕ} (φs : List 𝓕.FieldOp) (hn : n < φs.length)
(a : 𝓕.fieldOpToCrAnType φs[n]) (s : CrAnSection (φs.eraseIdx n)) :
((eraseIdxEquiv n φs hn).symm ⟨a, s⟩).1.eraseIdx n = s.1 := by
change (((eraseIdxEquiv n φs hn).symm ⟨a, s⟩).eraseIdx n).1 = _
rw [← eraseIdxEquiv_apply_snd _ hn]
simp
lemma sum_eraseIdxEquiv (n : ℕ) (φs : List 𝓕.States) (hn : n < φs.length)
lemma sum_eraseIdxEquiv (n : ℕ) (φs : List 𝓕.FieldOp) (hn : n < φs.length)
(f : CrAnSection φs → M) [AddCommMonoid M] : ∑ (s : CrAnSection φs), f s =
∑ (a : 𝓕.statesToCrAnType φs[n]), ∑ (s : CrAnSection (φs.eraseIdx n)),
∑ (a : 𝓕.fieldOpToCrAnType φs[n]), ∑ (s : CrAnSection (φs.eraseIdx n)),
f ((eraseIdxEquiv n φs hn).symm ⟨a, s⟩) := by
rw [← (eraseIdxEquiv n φs hn).symm.sum_comp]
rw [Fintype.sum_prod_type]

102
HepLean/PerturbationTheory/FieldSpecification/CrAnStates.lean
View file

@ -1,102 +0,0 @@
/-
Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.PerturbationTheory.FieldSpecification.Basic
import HepLean.PerturbationTheory.CreateAnnihilate
/-!
# Creation and annihilation states
Called `CrAnStates` for short here.
Given a field specification, in addition to defining states
(see: `HepLean.PerturbationTheory.FieldSpecification.Basic`),
we can also define creation and annihilation states.
These are similar to states but come with an additional specification of whether they correspond to
creation or annihilation operators.
In particular we have the following creation and annihilation states for each field:
- Negative asymptotic states - with the implicit specification that it is a creation state.
- Position states with a creation specification.
- Position states with an annihilation specification.
- Positive asymptotic states - with the implicit specification that it is an annihilation state.
In this module in addition to defining `CrAnStates` we also define some maps:
- The map `crAnStatesToStates` takes a `CrAnStates` to its state in `States`.
- The map `crAnStatesToCreateAnnihilate` takes a `CrAnStates` to its corresponding
`CreateAnnihilate` value.
- The map `crAnStatistics` takes a `CrAnStates` to its corresponding `FieldStatistic`
(bosonic or fermionic).
-/
namespace FieldSpecification
variable (𝓕 : FieldSpecification)
/-- 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
there is two. -/
def statesToCrAnType : 𝓕.States → Type
| States.inAsymp _ => Unit
| States.position _ => CreateAnnihilate
| States.outAsymp _ => Unit
/-- The instance of a finite type on `𝓕.statesToCreateAnnihilateType i`. -/
instance : ∀ i, Fintype (𝓕.statesToCrAnType i) := fun i =>
match i with
| States.inAsymp _ => inferInstanceAs (Fintype Unit)
| States.position _ => inferInstanceAs (Fintype CreateAnnihilate)
| States.outAsymp _ => inferInstanceAs (Fintype Unit)
/-- The instance of a decidable equality on `𝓕.statesToCreateAnnihilateType i`. -/
instance : ∀ i, DecidableEq (𝓕.statesToCrAnType i) := fun i =>
match i with
| States.inAsymp _ => inferInstanceAs (DecidableEq Unit)
| States.position _ => inferInstanceAs (DecidableEq CreateAnnihilate)
| States.outAsymp _ => inferInstanceAs (DecidableEq Unit)
/-- The equivalence between `𝓕.statesToCreateAnnihilateType i` and
`𝓕.statesToCreateAnnihilateType j` from an equality `i = j`. -/
def statesToCreateAnnihilateTypeCongr : {i j : 𝓕.States} → i = j →
𝓕.statesToCrAnType i ≃ 𝓕.statesToCrAnType j
| _, _, rfl => Equiv.refl _
/-- A creation and annihlation 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 CrAnStates : Type := Σ (s : 𝓕.States), 𝓕.statesToCrAnType s
/-- The map from creation and annihlation states to their underlying states. -/
def crAnStatesToStates : 𝓕.CrAnStates → 𝓕.States := Sigma.fst
@[simp]
lemma crAnStatesToStates_prod (s : 𝓕.States) (t : 𝓕.statesToCrAnType s) :
𝓕.crAnStatesToStates ⟨s, t⟩ = s := rfl
/-- The map from creation and annihlation states to the type `CreateAnnihilate`
specifying if a state is a creation or an annihilation state. -/
def crAnStatesToCreateAnnihilate : 𝓕.CrAnStates → CreateAnnihilate
| ⟨States.inAsymp _, _⟩ => CreateAnnihilate.create
| ⟨States.position _, CreateAnnihilate.create⟩ => CreateAnnihilate.create
| ⟨States.position _, CreateAnnihilate.annihilate⟩ => CreateAnnihilate.annihilate
| ⟨States.outAsymp _, _⟩ => CreateAnnihilate.annihilate
/-- Takes a `CrAnStates` state to its corresponding fields statistic (bosonic or fermionic). -/
def crAnStatistics : 𝓕.CrAnStates → FieldStatistic :=
𝓕.statesStatistic ∘ 𝓕.crAnStatesToStates
/-- The field statistic of a `CrAnState`. -/
scoped[FieldSpecification] notation 𝓕 "|>ₛ" φ =>
(crAnStatistics 𝓕) φ
/-- The field statistic of a list of `CrAnState`s. -/
scoped[FieldSpecification] notation 𝓕 "|>ₛ" φ => FieldStatistic.ofList
(crAnStatistics 𝓕) φ
/-- The `CreateAnnihilate` value of a `CrAnState`s, i.e. whether it is a creation or
annihilation operator. -/
scoped[FieldSpecification] infixl:80 "|>ᶜ" =>
crAnStatesToCreateAnnihilate
end FieldSpecification

36
HepLean/PerturbationTheory/FieldSpecification/Filters.lean
View file

@ -3,10 +3,10 @@ Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.PerturbationTheory.FieldSpecification.CrAnStates
import HepLean.PerturbationTheory.FieldSpecification.CrAnFieldOp
/-!
# Filters of lists of CrAnStates
# Filters of lists of CrAnFieldOp
-/
@ -17,34 +17,34 @@ variable {𝓕 : FieldSpecification}
the creation states. As a schematic example, for the list:
- `[φ1c, φ1a, φ2c, φ2a]` this will return `[φ1c, φ2c]`.
-/
def createFilter (φs : List 𝓕.CrAnStates) : List 𝓕.CrAnStates :=
def createFilter (φs : List 𝓕.CrAnFieldOp) : List 𝓕.CrAnFieldOp :=
List.filter (fun φ => 𝓕 |>ᶜ φ = CreateAnnihilate.create) φs
lemma createFilter_cons_create {φ : 𝓕.CrAnStates}
(hφ : 𝓕 |>ᶜ φ = CreateAnnihilate.create) (φs : List 𝓕.CrAnStates) :
lemma createFilter_cons_create {φ : 𝓕.CrAnFieldOp}
(hφ : 𝓕 |>ᶜ φ = CreateAnnihilate.create) (φs : List 𝓕.CrAnFieldOp) :
createFilter (φ :: φs) = φ :: createFilter φs := by
simp only [createFilter]
rw [List.filter_cons_of_pos]
simp [hφ]
lemma createFilter_cons_annihilate {φ : 𝓕.CrAnStates}
(hφ : 𝓕 |>ᶜ φ = CreateAnnihilate.annihilate) (φs : List 𝓕.CrAnStates) :
lemma createFilter_cons_annihilate {φ : 𝓕.CrAnFieldOp}
(hφ : 𝓕 |>ᶜ φ = CreateAnnihilate.annihilate) (φs : List 𝓕.CrAnFieldOp) :
createFilter (φ :: φs) = createFilter φs := by
simp only [createFilter]
rw [List.filter_cons_of_neg]
simp [hφ]
lemma createFilter_append (φs φs' : List 𝓕.CrAnStates) :
lemma createFilter_append (φs φs' : List 𝓕.CrAnFieldOp) :
createFilter (φs ++ φs') = createFilter φs ++ createFilter φs' := by
rw [createFilter, List.filter_append]
rfl
lemma createFilter_singleton_create (φ : 𝓕.CrAnStates)
lemma createFilter_singleton_create (φ : 𝓕.CrAnFieldOp)
(hφ : 𝓕 |>ᶜ φ = CreateAnnihilate.create) :
createFilter [φ] = [φ] := by
simp [createFilter, hφ]
lemma createFilter_singleton_annihilate (φ : 𝓕.CrAnStates)
lemma createFilter_singleton_annihilate (φ : 𝓕.CrAnFieldOp)
(hφ : 𝓕 |>ᶜ φ = CreateAnnihilate.annihilate) : createFilter [φ] = [] := by
simp [createFilter, hφ]
@ -53,34 +53,34 @@ lemma createFilter_singleton_annihilate (φ : 𝓕.CrAnStates)
As a schematic example, for the list:
- `[φ1c, φ1a, φ2c, φ2a]` this will return `[φ1a, φ2a]`.
-/
def annihilateFilter (φs : List 𝓕.CrAnStates) : List 𝓕.CrAnStates :=
def annihilateFilter (φs : List 𝓕.CrAnFieldOp) : List 𝓕.CrAnFieldOp :=
List.filter (fun φ => 𝓕 |>ᶜ φ = CreateAnnihilate.annihilate) φs
lemma annihilateFilter_cons_create {φ : 𝓕.CrAnStates}
(hφ : 𝓕 |>ᶜ φ = CreateAnnihilate.create) (φs : List 𝓕.CrAnStates) :
lemma annihilateFilter_cons_create {φ : 𝓕.CrAnFieldOp}
(hφ : 𝓕 |>ᶜ φ = CreateAnnihilate.create) (φs : List 𝓕.CrAnFieldOp) :
annihilateFilter (φ :: φs) = annihilateFilter φs := by
simp only [annihilateFilter]
rw [List.filter_cons_of_neg]
simp [hφ]
lemma annihilateFilter_cons_annihilate {φ : 𝓕.CrAnStates}
(hφ : 𝓕 |>ᶜ φ = CreateAnnihilate.annihilate) (φs : List 𝓕.CrAnStates) :
lemma annihilateFilter_cons_annihilate {φ : 𝓕.CrAnFieldOp}
(hφ : 𝓕 |>ᶜ φ = CreateAnnihilate.annihilate) (φs : List 𝓕.CrAnFieldOp) :
annihilateFilter (φ :: φs) = φ :: annihilateFilter φs := by
simp only [annihilateFilter]
rw [List.filter_cons_of_pos]
simp [hφ]
lemma annihilateFilter_append (φs φs' : List 𝓕.CrAnStates) :
lemma annihilateFilter_append (φs φs' : List 𝓕.CrAnFieldOp) :
annihilateFilter (φs ++ φs') = annihilateFilter φs ++ annihilateFilter φs' := by
rw [annihilateFilter, List.filter_append]
rfl
lemma annihilateFilter_singleton_create (φ : 𝓕.CrAnStates)
lemma annihilateFilter_singleton_create (φ : 𝓕.CrAnFieldOp)
(hφ : 𝓕 |>ᶜ φ = CreateAnnihilate.create) :
annihilateFilter [φ] = [] := by
simp [annihilateFilter, hφ]
lemma annihilateFilter_singleton_annihilate (φ : 𝓕.CrAnStates)
lemma annihilateFilter_singleton_annihilate (φ : 𝓕.CrAnFieldOp)
(hφ : 𝓕 |>ᶜ φ = CreateAnnihilate.annihilate) :
annihilateFilter [φ] = [φ] := by
simp [annihilateFilter, hφ]

110
HepLean/PerturbationTheory/FieldSpecification/NormalOrder.lean
View file

@ -21,19 +21,19 @@ variable {𝓕 : FieldSpecification}
- `φ1` is a creation operator
or
- `φ2` is an annihlate operator. -/
def normalOrderRel : 𝓕.CrAnStates → 𝓕.CrAnStates → Prop :=
def normalOrderRel : 𝓕.CrAnFieldOp → 𝓕.CrAnFieldOp → Prop :=
fun a b => CreateAnnihilate.normalOrder (𝓕 |>ᶜ a) (𝓕 |>ᶜ b)
/-- Normal ordering is total. -/
instance : IsTotal 𝓕.CrAnStates 𝓕.normalOrderRel where
instance : IsTotal 𝓕.CrAnFieldOp 𝓕.normalOrderRel where
total _ _ := total_of CreateAnnihilate.normalOrder _ _
/-- Normal ordering is transitive. -/
instance : IsTrans 𝓕.CrAnStates 𝓕.normalOrderRel where
instance : IsTrans 𝓕.CrAnFieldOp 𝓕.normalOrderRel where
trans _ _ _ := fun h h' => IsTrans.trans (α := CreateAnnihilate) _ _ _ h h'
/-- A decidable instance on the normal ordering relation. -/
instance (φ φ' : 𝓕.CrAnStates) : Decidable (normalOrderRel φ φ') :=
instance (φ φ' : 𝓕.CrAnFieldOp) : Decidable (normalOrderRel φ φ') :=
CreateAnnihilate.instDecidableNormalOrder (𝓕 |>ᶜ φ) (𝓕 |>ᶜ φ')
/-!
@ -45,16 +45,16 @@ instance (φ φ' : 𝓕.CrAnStates) : Decidable (normalOrderRel φ φ') :=
/-- The sign associated with putting a list of creation and annihlation states into normal order
(with the creation operators on the left).
We pick up a minus sign for every fermion paired crossed. -/
def normalOrderSign (φs : List 𝓕.CrAnStates) : ℂ :=
def normalOrderSign (φs : List 𝓕.CrAnFieldOp) : ℂ :=
Wick.koszulSign 𝓕.crAnStatistics 𝓕.normalOrderRel φs
@[simp]
lemma normalOrderSign_mul_self (φs : List 𝓕.CrAnStates) :
lemma normalOrderSign_mul_self (φs : List 𝓕.CrAnFieldOp) :
normalOrderSign φs * normalOrderSign φs = 1 := by
simp [normalOrderSign, Wick.koszulSign, Wick.koszulSign_mul_self]
lemma koszulSignInsert_create (φ : 𝓕.CrAnStates)
(hφ : 𝓕 |>ᶜ φ = CreateAnnihilate.create) : (φs : List 𝓕.CrAnStates) →
lemma koszulSignInsert_create (φ : 𝓕.CrAnFieldOp)
(hφ : 𝓕 |>ᶜ φ = CreateAnnihilate.create) : (φs : List 𝓕.CrAnFieldOp) →
Wick.koszulSignInsert 𝓕.crAnStatistics normalOrderRel φ φs = 1
| [] => rfl
| φ' :: φs => by
@ -65,21 +65,21 @@ lemma koszulSignInsert_create (φ : 𝓕.CrAnStates)
rw [hφ]
dsimp [CreateAnnihilate.normalOrder]
lemma normalOrderSign_cons_create (φ : 𝓕.CrAnStates)
(hφ : 𝓕 |>ᶜ φ = CreateAnnihilate.create) (φs : List 𝓕.CrAnStates) :
lemma normalOrderSign_cons_create (φ : 𝓕.CrAnFieldOp)
(hφ : 𝓕 |>ᶜ φ = CreateAnnihilate.create) (φs : List 𝓕.CrAnFieldOp) :
normalOrderSign (φ :: φs) = normalOrderSign φs := by
simp [normalOrderSign, Wick.koszulSign, koszulSignInsert_create φ hφ φs]
@[simp]
lemma normalOrderSign_singleton (φ : 𝓕.CrAnStates) : normalOrderSign [φ] = 1 := by
lemma normalOrderSign_singleton (φ : 𝓕.CrAnFieldOp) : normalOrderSign [φ] = 1 := by
simp [normalOrderSign]
@[simp]
lemma normalOrderSign_nil : normalOrderSign (𝓕 := 𝓕) [] = 1 := rfl
lemma koszulSignInsert_append_annihilate (φ' φ : 𝓕.CrAnStates)
lemma koszulSignInsert_append_annihilate (φ' φ : 𝓕.CrAnFieldOp)
(hφ : 𝓕 |>ᶜ φ = CreateAnnihilate.annihilate) :
(φs : List 𝓕.CrAnStates) →
(φs : List 𝓕.CrAnFieldOp) →
Wick.koszulSignInsert 𝓕.crAnStatistics normalOrderRel φ' (φs ++ [φ]) =
Wick.koszulSignInsert 𝓕.crAnStatistics normalOrderRel φ' φs
| [] => by
@ -90,9 +90,9 @@ lemma koszulSignInsert_append_annihilate (φ' φ : 𝓕.CrAnStates)
dsimp only [List.cons_append, Wick.koszulSignInsert]
rw [koszulSignInsert_append_annihilate φ' φ hφ φs]
lemma normalOrderSign_append_annihlate (φ : 𝓕.CrAnStates)
lemma normalOrderSign_append_annihlate (φ : 𝓕.CrAnFieldOp)
(hφ : 𝓕 |>ᶜ φ = CreateAnnihilate.annihilate) :
(φs : List 𝓕.CrAnStates) →
(φs : List 𝓕.CrAnFieldOp) →
normalOrderSign (φs ++ [φ]) = normalOrderSign φs
| [] => by simp
| φ' :: φs => by
@ -101,10 +101,10 @@ lemma normalOrderSign_append_annihlate (φ : 𝓕.CrAnStates)
dsimp only [normalOrderSign] at hi
rw [hi, koszulSignInsert_append_annihilate φ' φ hφ φs]
lemma koszulSignInsert_annihilate_cons_create (φc φa : 𝓕.CrAnStates)
lemma koszulSignInsert_annihilate_cons_create (φc φa : 𝓕.CrAnFieldOp)
(hφc : 𝓕 |>ᶜ φc = CreateAnnihilate.create)
(hφa : 𝓕 |>ᶜ φa = CreateAnnihilate.annihilate)
(φs : List 𝓕.CrAnStates) :
(φs : List 𝓕.CrAnFieldOp) :
Wick.koszulSignInsert 𝓕.crAnStatistics normalOrderRel φa (φc :: φs)
= FieldStatistic.exchangeSign (𝓕.crAnStatistics φc) (𝓕.crAnStatistics φa) *
Wick.koszulSignInsert 𝓕.crAnStatistics normalOrderRel φa φs := by
@ -116,10 +116,10 @@ lemma koszulSignInsert_annihilate_cons_create (φc φa : 𝓕.CrAnStates)
rw [normalOrderRel, hφa, hφc]
simp [CreateAnnihilate.normalOrder]
lemma normalOrderSign_swap_create_annihlate_fst (φc φa : 𝓕.CrAnStates)
lemma normalOrderSign_swap_create_annihlate_fst (φc φa : 𝓕.CrAnFieldOp)
(hφc : 𝓕 |>ᶜ φc = CreateAnnihilate.create)
(hφa : 𝓕 |>ᶜ φa = CreateAnnihilate.annihilate)
(φs : List 𝓕.CrAnStates) :
(φs : List 𝓕.CrAnFieldOp) :
normalOrderSign (φc :: φa :: φs) =
FieldStatistic.exchangeSign (𝓕.crAnStatistics φc) (𝓕.crAnStatistics φa) *
normalOrderSign (φa :: φc :: φs) := by
@ -131,14 +131,14 @@ lemma normalOrderSign_swap_create_annihlate_fst (φc φa : 𝓕.CrAnStates)
rw [one_mul, normalOrderSign_cons_create φc hφc φs]
rfl
lemma koszulSignInsert_swap (φ φc φa : 𝓕.CrAnStates) (φs φs' : List 𝓕.CrAnStates) :
lemma koszulSignInsert_swap (φ φc φa : 𝓕.CrAnFieldOp) (φs φs' : List 𝓕.CrAnFieldOp) :
Wick.koszulSignInsert 𝓕.crAnStatistics normalOrderRel φ (φs ++ φa :: φc :: φs')
= Wick.koszulSignInsert 𝓕.crAnStatistics normalOrderRel φ (φs ++ φc :: φa :: φs') :=
Wick.koszulSignInsert_eq_perm _ _ _ _ _ (List.Perm.append_left φs (List.Perm.swap φc φa φs'))
lemma normalOrderSign_swap_create_annihlate (φc φa : 𝓕.CrAnStates)
lemma normalOrderSign_swap_create_annihlate (φc φa : 𝓕.CrAnFieldOp)
(hφc : 𝓕 |>ᶜ φc = CreateAnnihilate.create) (hφa : 𝓕 |>ᶜ φa = CreateAnnihilate.annihilate) :
(φs φs' : List 𝓕.CrAnStates) → normalOrderSign (φs ++ φc :: φa :: φs') =
(φs φs' : List 𝓕.CrAnFieldOp) → normalOrderSign (φs ++ φc :: φa :: φs') =
FieldStatistic.exchangeSign (𝓕.crAnStatistics φc) (𝓕.crAnStatistics φa) *
normalOrderSign (φs ++ φa :: φc :: φs')
| [], φs' => normalOrderSign_swap_create_annihlate_fst φc φa hφc hφa φs'
@ -154,16 +154,16 @@ lemma normalOrderSign_swap_create_annihlate (φc φa : 𝓕.CrAnStates)
left
rw [koszulSignInsert_swap]
lemma normalOrderSign_swap_create_create_fst (φc φc' : 𝓕.CrAnStates)
lemma normalOrderSign_swap_create_create_fst (φc φc' : 𝓕.CrAnFieldOp)
(hφc : 𝓕 |>ᶜ φc = CreateAnnihilate.create) (hφc' : 𝓕 |>ᶜ φc' = CreateAnnihilate.create)
(φs : List 𝓕.CrAnStates) :
(φs : List 𝓕.CrAnFieldOp) :
normalOrderSign (φc :: φc' :: φs) = normalOrderSign (φc' :: φc :: φs) := by
rw [normalOrderSign_cons_create φc hφc, normalOrderSign_cons_create φc' hφc']
rw [normalOrderSign_cons_create φc' hφc', normalOrderSign_cons_create φc hφc]
lemma normalOrderSign_swap_create_create (φc φc' : 𝓕.CrAnStates)
lemma normalOrderSign_swap_create_create (φc φc' : 𝓕.CrAnFieldOp)
(hφc : 𝓕 |>ᶜ φc = CreateAnnihilate.create) (hφc' : 𝓕 |>ᶜ φc' = CreateAnnihilate.create) :
(φs φs' : List 𝓕.CrAnStates) →
(φs φs' : List 𝓕.CrAnFieldOp) →
normalOrderSign (φs ++ φc :: φc' :: φs') = normalOrderSign (φs ++ φc' :: φc :: φs')
| [], φs' => by
exact normalOrderSign_swap_create_create_fst φc φc' hφc hφc' φs'
@ -177,10 +177,10 @@ lemma normalOrderSign_swap_create_create (φc φc' : 𝓕.CrAnStates)
apply Or.inl (Wick.koszulSignInsert_eq_perm _ _ _ _ _ _)
exact List.Perm.append_left φs (List.Perm.swap φc' φc φs')
lemma normalOrderSign_swap_annihilate_annihilate_fst (φa φa' : 𝓕.CrAnStates)
lemma normalOrderSign_swap_annihilate_annihilate_fst (φa φa' : 𝓕.CrAnFieldOp)
(hφa : 𝓕 |>ᶜ φa = CreateAnnihilate.annihilate)
(hφa' : 𝓕 |>ᶜ φa' = CreateAnnihilate.annihilate)
(φs : List 𝓕.CrAnStates) :
(φs : List 𝓕.CrAnFieldOp) :
normalOrderSign (φa :: φa' :: φs) =
normalOrderSign (φa' :: φa :: φs) := by
rw [normalOrderSign, normalOrderSign]
@ -195,9 +195,9 @@ lemma normalOrderSign_swap_annihilate_annihilate_fst (φa φa' : 𝓕.CrAnStates
· simp [normalOrderRel, hφa, hφa', CreateAnnihilate.normalOrder]
· rw [NonUnitalNormedCommRing.mul_comm]
lemma normalOrderSign_swap_annihilate_annihilate (φa φa' : 𝓕.CrAnStates)
lemma normalOrderSign_swap_annihilate_annihilate (φa φa' : 𝓕.CrAnFieldOp)
(hφa : 𝓕 |>ᶜ φa = CreateAnnihilate.annihilate)
(hφa' : 𝓕 |>ᶜ φa' = CreateAnnihilate.annihilate) : (φs φs' : List 𝓕.CrAnStates) →
(hφa' : 𝓕 |>ᶜ φa' = CreateAnnihilate.annihilate) : (φs φs' : List 𝓕.CrAnFieldOp) →
normalOrderSign (φs ++ φa :: φa' :: φs') = normalOrderSign (φs ++ φa' :: φa :: φs')
| [], φs' => by
exact normalOrderSign_swap_annihilate_annihilate_fst φa φa' hφa hφa' φs'
@ -225,7 +225,7 @@ open FieldStatistic
To give some schematic. For example:
- `normalOrderList [φ1c, φ1a, φ2c, φ2a] = [φ1c, φ2c, φ1a, φ2a]`
-/
def normalOrderList (φs : List 𝓕.CrAnStates) : List 𝓕.CrAnStates :=
def normalOrderList (φs : List 𝓕.CrAnFieldOp) : List 𝓕.CrAnFieldOp :=
List.insertionSort 𝓕.normalOrderRel φs
@[simp]
@ -233,13 +233,13 @@ lemma normalOrderList_nil : normalOrderList (𝓕 := 𝓕) [] = [] := by
simp [normalOrderList]
@[simp]
lemma normalOrderList_statistics (φs : List 𝓕.CrAnStates) :
lemma normalOrderList_statistics (φs : List 𝓕.CrAnFieldOp) :
(𝓕 |>ₛ (normalOrderList φs)) = 𝓕 |>ₛ φs := by
simp [normalOrderList, List.insertionSort]
lemma orderedInsert_create (φ : 𝓕.CrAnStates)
lemma orderedInsert_create (φ : 𝓕.CrAnFieldOp)
(hφ : 𝓕 |>ᶜ φ = CreateAnnihilate.create) :
(φs : List 𝓕.CrAnStates) → List.orderedInsert normalOrderRel φ φs = φ :: φs
(φs : List 𝓕.CrAnFieldOp) → List.orderedInsert normalOrderRel φ φs = φ :: φs
| [] => rfl
| φ' :: φs => by
dsimp only [List.orderedInsert.eq_2]
@ -248,15 +248,15 @@ lemma orderedInsert_create (φ : 𝓕.CrAnStates)
rw [hφ]
dsimp [CreateAnnihilate.normalOrder]
lemma normalOrderList_cons_create (φ : 𝓕.CrAnStates)
(hφ : 𝓕 |>ᶜ φ = CreateAnnihilate.create) (φs : List 𝓕.CrAnStates) :
lemma normalOrderList_cons_create (φ : 𝓕.CrAnFieldOp)
(hφ : 𝓕 |>ᶜ φ = CreateAnnihilate.create) (φs : List 𝓕.CrAnFieldOp) :
normalOrderList (φ :: φs) = φ :: normalOrderList φs := by
simp only [normalOrderList, List.insertionSort]
rw [orderedInsert_create φ hφ]
lemma orderedInsert_append_annihilate (φ' φ : 𝓕.CrAnStates)
lemma orderedInsert_append_annihilate (φ' φ : 𝓕.CrAnFieldOp)
(hφ : 𝓕 |>ᶜ φ = CreateAnnihilate.annihilate) :
(φs : List 𝓕.CrAnStates) → List.orderedInsert normalOrderRel φ' (φs ++ [φ]) =
(φs : List 𝓕.CrAnFieldOp) → List.orderedInsert normalOrderRel φ' (φs ++ [φ]) =
List.orderedInsert normalOrderRel φ' φs ++ [φ]
| [] => by
simp [Wick.koszulSignInsert, normalOrderRel, hφ]
@ -268,9 +268,9 @@ lemma orderedInsert_append_annihilate (φ' φ : 𝓕.CrAnStates)
next h => simp_all only [List.cons_append]
next h => simp_all only [List.cons_append]
lemma normalOrderList_append_annihilate (φ : 𝓕.CrAnStates)
lemma normalOrderList_append_annihilate (φ : 𝓕.CrAnFieldOp)
(hφ : 𝓕 |>ᶜ φ = CreateAnnihilate.annihilate) :
(φs : List 𝓕.CrAnStates) →
(φs : List 𝓕.CrAnFieldOp) →
normalOrderList (φs ++ [φ]) = normalOrderList φs ++ [φ]
| [] => by simp [normalOrderList]
| φ' :: φs => by
@ -279,10 +279,10 @@ lemma normalOrderList_append_annihilate (φ : 𝓕.CrAnStates)
dsimp only [normalOrderList] at hi
rw [hi, orderedInsert_append_annihilate φ' φ hφ]
lemma normalOrder_swap_create_annihlate_fst (φc φa : 𝓕.CrAnStates)
lemma normalOrder_swap_create_annihlate_fst (φc φa : 𝓕.CrAnFieldOp)
(hφc : 𝓕 |>ᶜ φc = CreateAnnihilate.create)
(hφa : 𝓕 |>ᶜ φa = CreateAnnihilate.annihilate)
(φs : List 𝓕.CrAnStates) :
(φs : List 𝓕.CrAnFieldOp) :
normalOrderList (φc :: φa :: φs) = normalOrderList (φa :: φc :: φs) := by
rw [normalOrderList_cons_create φc hφc (φa :: φs)]
conv_rhs =>
@ -297,10 +297,10 @@ lemma normalOrder_swap_create_annihlate_fst (φc φa : 𝓕.CrAnStates)
dsimp [CreateAnnihilate.normalOrder] at h
· rfl
lemma normalOrderList_swap_create_annihlate (φc φa : 𝓕.CrAnStates)
lemma normalOrderList_swap_create_annihlate (φc φa : 𝓕.CrAnFieldOp)
(hφc : 𝓕 |>ᶜ φc = CreateAnnihilate.create)
(hφa : 𝓕 |>ᶜ φa = CreateAnnihilate.annihilate) :
(φs φs' : List 𝓕.CrAnStates) →
(φs φs' : List 𝓕.CrAnFieldOp) →
normalOrderList (φs ++ φc :: φa :: φs') = normalOrderList (φs ++ φa :: φc :: φs')
| [], φs' => normalOrder_swap_create_annihlate_fst φc φa hφc hφa φs'
| φ :: φs, φs' => by
@ -316,16 +316,16 @@ lemma normalOrderList_swap_create_annihlate (φc φa : 𝓕.CrAnStates)
For example:
- For `[φ1c, φ1a, φ2c, φ2a]` this equivalence sends `0 ↦ 0`, `1 ↦ 2`, `2 ↦ 1`, `3 ↦ 3`.
-/
def normalOrderEquiv {φs : List 𝓕.CrAnStates} : Fin φs.length ≃ Fin (normalOrderList φs).length :=
def normalOrderEquiv {φs : List 𝓕.CrAnFieldOp} : Fin φs.length ≃ Fin (normalOrderList φs).length :=
HepLean.List.insertionSortEquiv 𝓕.normalOrderRel φs
lemma sum_normalOrderList_length {M : Type} [AddCommMonoid M]
(φs : List 𝓕.CrAnStates) (f : Fin (normalOrderList φs).length → M) :
(φs : List 𝓕.CrAnFieldOp) (f : Fin (normalOrderList φs).length → M) :
∑ (n : Fin (normalOrderList φs).length), f n = ∑ (n : Fin φs.length), f (normalOrderEquiv n) :=
Eq.symm (Equiv.sum_comp normalOrderEquiv f)
@[simp]
lemma normalOrderList_get_normalOrderEquiv {φs : List 𝓕.CrAnStates} (n : Fin φs.length) :
lemma normalOrderList_get_normalOrderEquiv {φs : List 𝓕.CrAnFieldOp} (n : Fin φs.length) :
(normalOrderList φs)[(normalOrderEquiv n).val] = φs[n.val] := by
change (normalOrderList φs).get (normalOrderEquiv n) = _
simp only [normalOrderList, normalOrderEquiv]
@ -333,21 +333,21 @@ lemma normalOrderList_get_normalOrderEquiv {φs : List 𝓕.CrAnStates} (n : Fin
simp
@[simp]
lemma normalOrderList_eraseIdx_normalOrderEquiv {φs : List 𝓕.CrAnStates} (n : Fin φs.length) :
lemma normalOrderList_eraseIdx_normalOrderEquiv {φs : List 𝓕.CrAnFieldOp} (n : Fin φs.length) :
(normalOrderList φs).eraseIdx (normalOrderEquiv n).val =
normalOrderList (φs.eraseIdx n.val) := by
simp only [normalOrderList, normalOrderEquiv]
rw [HepLean.List.eraseIdx_insertionSort_fin]
lemma normalOrderSign_eraseIdx (φs : List 𝓕.CrAnStates) (n : Fin φs.length) :
lemma normalOrderSign_eraseIdx (φs : List 𝓕.CrAnFieldOp) (n : Fin φs.length) :
normalOrderSign (φs.eraseIdx n) = normalOrderSign φs *
𝓢(𝓕 |>ₛ (φs.get n), 𝓕 |>ₛ (φs.take n)) *
𝓢(𝓕 |>ₛ (φs.get n), 𝓕 |>ₛ ((normalOrderList φs).take (normalOrderEquiv n))) := by
rw [normalOrderSign, Wick.koszulSign_eraseIdx, ← normalOrderSign]
rfl
lemma orderedInsert_createFilter_append_annihilate (φ : 𝓕.CrAnStates)
(hφ : 𝓕 |>ᶜ φ = CreateAnnihilate.annihilate) : (φs φs' : List 𝓕.CrAnStates) →
lemma orderedInsert_createFilter_append_annihilate (φ : 𝓕.CrAnFieldOp)
(hφ : 𝓕 |>ᶜ φ = CreateAnnihilate.annihilate) : (φs φs' : List 𝓕.CrAnFieldOp) →
List.orderedInsert normalOrderRel φ (createFilter φs ++ φs') =
createFilter φs ++ List.orderedInsert normalOrderRel φ φs'
| [], φs' => by simp [createFilter]
@ -359,7 +359,7 @@ lemma orderedInsert_createFilter_append_annihilate (φ : 𝓕.CrAnStates)
simp [normalOrderRel, hφ, hφ', CreateAnnihilate.normalOrder]
· rw [createFilter_cons_annihilate hφ', orderedInsert_createFilter_append_annihilate φ hφ φs]
lemma orderedInsert_annihilateFilter (φ : 𝓕.CrAnStates) : (φs : List 𝓕.CrAnStates) →
lemma orderedInsert_annihilateFilter (φ : 𝓕.CrAnFieldOp) : (φs : List 𝓕.CrAnFieldOp) →
List.orderedInsert normalOrderRel φ (annihilateFilter φs) =
φ :: annihilateFilter φs
| [] => by simp [annihilateFilter]
@ -377,13 +377,13 @@ lemma orderedInsert_annihilateFilter (φ : 𝓕.CrAnStates) : (φs : List 𝓕.C
· rw [hφ]
simp [CreateAnnihilate.normalOrder]
lemma orderedInsert_createFilter_append_annihilateFilter_annihilate (φ : 𝓕.CrAnStates)
(hφ : 𝓕 |>ᶜ φ = CreateAnnihilate.annihilate) (φs : List 𝓕.CrAnStates) :
lemma orderedInsert_createFilter_append_annihilateFilter_annihilate (φ : 𝓕.CrAnFieldOp)
(hφ : 𝓕 |>ᶜ φ = CreateAnnihilate.annihilate) (φs : List 𝓕.CrAnFieldOp) :
List.orderedInsert normalOrderRel φ (createFilter φs ++ annihilateFilter φs) =
createFilter φs ++ φ :: annihilateFilter φs := by
rw [orderedInsert_createFilter_append_annihilate φ hφ, orderedInsert_annihilateFilter]
lemma normalOrderList_eq_createFilter_append_annihilateFilter : (φs : List 𝓕.CrAnStates) →
lemma normalOrderList_eq_createFilter_append_annihilateFilter : (φs : List 𝓕.CrAnFieldOp) →
normalOrderList φs = createFilter φs ++ annihilateFilter φs
| [] => by simp [normalOrderList, createFilter, annihilateFilter]
| φ :: φs => by

192
HepLean/PerturbationTheory/FieldSpecification/TimeOrder.lean
View file

@ -23,28 +23,28 @@ variable {𝓕 : FieldSpecification}
/-- The time ordering relation on states. We have that `timeOrderRel φ0 φ1` is true
if and only if `φ1` has a time less-then or equal to `φ0`, or `φ1` is a negative
asymptotic state, or `φ0` is a positive asymptotic state. -/
def timeOrderRel : 𝓕.States → 𝓕.States → Prop
| States.outAsymp _, _ => True
| States.position φ0, States.position φ1 => φ1.2 0 ≤ φ0.2 0
| States.position _, States.inAsymp _ => True
| States.position _, States.outAsymp _ => False
| States.inAsymp _, States.outAsymp _ => False
| States.inAsymp _, States.position _ => False
| States.inAsymp _, States.inAsymp _ => True
def timeOrderRel : 𝓕.FieldOp → 𝓕.FieldOp → Prop
| FieldOp.outAsymp _, _ => True
| FieldOp.position φ0, FieldOp.position φ1 => φ1.2 0 ≤ φ0.2 0
| FieldOp.position _, FieldOp.inAsymp _ => True
| FieldOp.position _, FieldOp.outAsymp _ => False
| FieldOp.inAsymp _, FieldOp.outAsymp _ => False
| FieldOp.inAsymp _, FieldOp.position _ => False
| FieldOp.inAsymp _, FieldOp.inAsymp _ => True
/-- The relation `timeOrderRel` is decidable, but not computablly so due to
`Real.decidableLE`. -/
noncomputable instance : (φ φ' : 𝓕.States) → Decidable (timeOrderRel φ φ')
| States.outAsymp _, _ => isTrue True.intro
| States.position φ0, States.position φ1 => inferInstanceAs (Decidable (φ1.2 0 ≤ φ0.2 0))
| States.position _, States.inAsymp _ => isTrue True.intro
| States.position _, States.outAsymp _ => isFalse (fun a => a)
| States.inAsymp _, States.outAsymp _ => isFalse (fun a => a)
| States.inAsymp _, States.position _ => isFalse (fun a => a)
| States.inAsymp _, States.inAsymp _ => isTrue True.intro
noncomputable instance : (φ φ' : 𝓕.FieldOp) → Decidable (timeOrderRel φ φ')
| FieldOp.outAsymp _, _ => isTrue True.intro
| FieldOp.position φ0, FieldOp.position φ1 => inferInstanceAs (Decidable (φ1.2 0 ≤ φ0.2 0))
| FieldOp.position _, FieldOp.inAsymp _ => isTrue True.intro
| FieldOp.position _, FieldOp.outAsymp _ => isFalse (fun a => a)
| FieldOp.inAsymp _, FieldOp.outAsymp _ => isFalse (fun a => a)
| FieldOp.inAsymp _, FieldOp.position _ => isFalse (fun a => a)
| FieldOp.inAsymp _, FieldOp.inAsymp _ => isTrue True.intro
/-- Time ordering is total. -/
instance : IsTotal 𝓕.States 𝓕.timeOrderRel where
instance : IsTotal 𝓕.FieldOp 𝓕.timeOrderRel where
total a b := by
cases a <;> cases b <;>
simp only [or_self, or_false, or_true, timeOrderRel, Fin.isValue, implies_true, imp_self,
@ -52,7 +52,7 @@ instance : IsTotal 𝓕.States 𝓕.timeOrderRel where
exact LinearOrder.le_total _ _
/-- Time ordering is transitive. -/
instance : IsTrans 𝓕.States 𝓕.timeOrderRel where
instance : IsTrans 𝓕.FieldOp 𝓕.timeOrderRel where
trans a b c := by
cases a <;> cases b <;> cases c <;>
simp only [timeOrderRel, Fin.isValue, implies_true, imp_self, IsEmpty.forall_iff]
@ -68,10 +68,10 @@ open HepLean.List
- for the list `[φ1(t = 4), φ2(t = 5), φ3(t = 3), φ4(t = 5)]` this would return `1`.
This is defined for a list `φ :: φs` instead of `φs` to ensure that such a position exists.
-/
def maxTimeFieldPos (φ : 𝓕.States) (φs : List 𝓕.States) : ℕ :=
def maxTimeFieldPos (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) : ℕ :=
insertionSortMinPos timeOrderRel φ φs
lemma maxTimeFieldPos_lt_length (φ : 𝓕.States) (φs : List 𝓕.States) :
lemma maxTimeFieldPos_lt_length (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) :
maxTimeFieldPos φ φs < (φ :: φs).length := by
simp [maxTimeFieldPos]
@ -80,7 +80,7 @@ lemma maxTimeFieldPos_lt_length (φ : 𝓕.States) (φs : List 𝓕.States) :
- for the list `[φ1(t = 4), φ2(t = 5), φ3(t = 3), φ4(t = 5)]` this would return `φ2(t = 5)`.
It is the state at the position `maxTimeFieldPos φ φs`.
-/
def maxTimeField (φ : 𝓕.States) (φs : List 𝓕.States) : 𝓕.States :=
def maxTimeField (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) : 𝓕.FieldOp :=
insertionSortMin timeOrderRel φ φs
/-- Given a list `φ :: φs` of states, the list with the left-most state of maximum
@ -89,15 +89,15 @@ def maxTimeField (φ : 𝓕.States) (φs : List 𝓕.States) : 𝓕.States :=
- for the list `[φ1(t = 4), φ2(t = 5), φ3(t = 3), φ4(t = 5)]` this would return
`[φ1(t = 4), φ3(t = 3), φ4(t = 5)]`.
-/
def eraseMaxTimeField (φ : 𝓕.States) (φs : List 𝓕.States) : List 𝓕.States :=
def eraseMaxTimeField (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) : List 𝓕.FieldOp :=
insertionSortDropMinPos timeOrderRel φ φs
@[simp]
lemma eraseMaxTimeField_length (φ : 𝓕.States) (φs : List 𝓕.States) :
lemma eraseMaxTimeField_length (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) :
(eraseMaxTimeField φ φs).length = φs.length := by
simp [eraseMaxTimeField, insertionSortDropMinPos, eraseIdx_length']
lemma maxTimeFieldPos_lt_eraseMaxTimeField_length_succ (φ : 𝓕.States) (φs : List 𝓕.States) :
lemma maxTimeFieldPos_lt_eraseMaxTimeField_length_succ (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) :
maxTimeFieldPos φ φs < (eraseMaxTimeField φ φs).length.succ := by
simp only [eraseMaxTimeField_length, Nat.succ_eq_add_one]
exact maxTimeFieldPos_lt_length φ φs
@ -107,17 +107,17 @@ lemma maxTimeFieldPos_lt_eraseMaxTimeField_length_succ (φ : 𝓕.States) (φs :
As an example:
- for the list `[φ1(t = 4), φ2(t = 5), φ3(t = 3), φ4(t = 5)]` this would return `⟨1,...⟩`.
-/
def maxTimeFieldPosFin (φ : 𝓕.States) (φs : List 𝓕.States) :
def maxTimeFieldPosFin (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) :
Fin (eraseMaxTimeField φ φs).length.succ :=
insertionSortMinPosFin timeOrderRel φ φs
lemma lt_maxTimeFieldPosFin_not_timeOrder (φ : 𝓕.States) (φs : List 𝓕.States)
lemma lt_maxTimeFieldPosFin_not_timeOrder (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
(i : Fin (eraseMaxTimeField φ φs).length)
(hi : (maxTimeFieldPosFin φ φs).succAbove i < maxTimeFieldPosFin φ φs) :
¬ timeOrderRel ((eraseMaxTimeField φ φs)[i.val]) (maxTimeField φ φs) := by
exact insertionSortMin_lt_mem_insertionSortDropMinPos_of_lt timeOrderRel φ φs i hi
lemma timeOrder_maxTimeField (φ : 𝓕.States) (φs : List 𝓕.States)
lemma timeOrder_maxTimeField (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
(i : Fin (eraseMaxTimeField φ φs).length) :
timeOrderRel (maxTimeField φ φs) ((eraseMaxTimeField φ φs)[i.val]) := by
exact insertionSortMin_lt_mem_insertionSortDropMinPos timeOrderRel φ φs _
@ -125,7 +125,7 @@ lemma timeOrder_maxTimeField (φ : 𝓕.States) (φs : List 𝓕.States)
/-- The sign associated with putting a list of states into time order (with
the state of greatest time to the left).
We pick up a minus sign for every fermion paired crossed. -/
def timeOrderSign (φs : List 𝓕.States) : ℂ :=
def timeOrderSign (φs : List 𝓕.FieldOp) : ℂ :=
Wick.koszulSign 𝓕.statesStatistic 𝓕.timeOrderRel φs
@[simp]
@ -133,19 +133,19 @@ lemma timeOrderSign_nil : timeOrderSign (𝓕 := 𝓕) [] = 1 := by
simp only [timeOrderSign]
rfl
lemma timeOrderSign_pair_ordered {φ ψ : 𝓕.States} (h : timeOrderRel φ ψ) :
lemma timeOrderSign_pair_ordered {φ ψ : 𝓕.FieldOp} (h : timeOrderRel φ ψ) :
timeOrderSign [φ, ψ] = 1 := by
simp only [timeOrderSign, Wick.koszulSign, Wick.koszulSignInsert, mul_one, ite_eq_left_iff,
ite_eq_right_iff, and_imp]
exact fun h' => False.elim (h' h)
lemma timeOrderSign_pair_not_ordered {φ ψ : 𝓕.States} (h : ¬ timeOrderRel φ ψ) :
lemma timeOrderSign_pair_not_ordered {φ ψ : 𝓕.FieldOp} (h : ¬ timeOrderRel φ ψ) :
timeOrderSign [φ, ψ] = 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ψ) := by
simp only [timeOrderSign, Wick.koszulSign, Wick.koszulSignInsert, mul_one, instCommGroup.eq_1]
rw [if_neg h]
simp [FieldStatistic.exchangeSign_eq_if]
lemma timerOrderSign_of_eraseMaxTimeField (φ : 𝓕.States) (φs : List 𝓕.States) :
lemma timerOrderSign_of_eraseMaxTimeField (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) :
timeOrderSign (eraseMaxTimeField φ φs) = timeOrderSign (φ :: φs) *
𝓢(𝓕 |>ₛ maxTimeField φ φs, 𝓕 |>ₛ (φ :: φs).take (maxTimeFieldPos φ φs)) := by
rw [eraseMaxTimeField, insertionSortDropMinPos, timeOrderSign,
@ -156,16 +156,16 @@ lemma timerOrderSign_of_eraseMaxTimeField (φ : 𝓕.States) (φs : List 𝓕.St
/-- The time ordering of a list of states. A schematic example is:
- `normalOrderList [φ1(t = 4), φ2(t = 5), φ3(t = 3), φ4(t = 5)]` is equal to
`[φ2(t = 5), φ4(t = 5), φ1(t = 4), φ3(t = 3)]` -/
def timeOrderList (φs : List 𝓕.States) : List 𝓕.States :=
def timeOrderList (φs : List 𝓕.FieldOp) : List 𝓕.FieldOp :=
List.insertionSort 𝓕.timeOrderRel φs
lemma timeOrderList_pair_ordered {φ ψ : 𝓕.States} (h : timeOrderRel φ ψ) :
lemma timeOrderList_pair_ordered {φ ψ : 𝓕.FieldOp} (h : timeOrderRel φ ψ) :
timeOrderList [φ, ψ] = [φ, ψ] := by
simp only [timeOrderList, List.insertionSort, List.orderedInsert, ite_eq_left_iff,
List.cons.injEq, and_true]
exact fun h' => False.elim (h' h)
lemma timeOrderList_pair_not_ordered {φ ψ : 𝓕.States} (h : ¬ timeOrderRel φ ψ) :
lemma timeOrderList_pair_not_ordered {φ ψ : 𝓕.FieldOp} (h : ¬ timeOrderRel φ ψ) :
timeOrderList [φ, ψ] = [ψ, φ] := by
simp only [timeOrderList, List.insertionSort, List.orderedInsert, ite_eq_right_iff,
List.cons.injEq, and_true]
@ -175,13 +175,13 @@ lemma timeOrderList_pair_not_ordered {φ ψ : 𝓕.States} (h : ¬ timeOrderRel
lemma timeOrderList_nil : timeOrderList (𝓕 := 𝓕) [] = [] := by
simp [timeOrderList]
lemma timeOrderList_eq_maxTimeField_timeOrderList (φ : 𝓕.States) (φs : List 𝓕.States) :
lemma timeOrderList_eq_maxTimeField_timeOrderList (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) :
timeOrderList (φ :: φs) = maxTimeField φ φs :: timeOrderList (eraseMaxTimeField φ φs) := by
exact insertionSort_eq_insertionSortMin_cons timeOrderRel φ φs
/-!
## Time ordering for CrAnStates
## Time ordering for CrAnFieldOp
-/
@ -191,30 +191,30 @@ lemma timeOrderList_eq_maxTimeField_timeOrderList (φ : 𝓕.States) (φs : List
-/
/-- The time ordering relation on CrAnStates. -/
def crAnTimeOrderRel (a b : 𝓕.CrAnStates) : Prop := 𝓕.timeOrderRel a.1 b.1
/-- The time ordering relation on CrAnFieldOp. -/
def crAnTimeOrderRel (a b : 𝓕.CrAnFieldOp) : Prop := 𝓕.timeOrderRel a.1 b.1
/-- The relation `crAnTimeOrderRel` is decidable, but not computablly so due to
`Real.decidableLE`. -/
noncomputable instance (φ φ' : 𝓕.CrAnStates) : Decidable (crAnTimeOrderRel φ φ') :=
noncomputable instance (φ φ' : 𝓕.CrAnFieldOp) : Decidable (crAnTimeOrderRel φ φ') :=
inferInstanceAs (Decidable (𝓕.timeOrderRel φ.1 φ'.1))
/-- Time ordering of `CrAnStates` is total. -/
instance : IsTotal 𝓕.CrAnStates 𝓕.crAnTimeOrderRel where
/-- Time ordering of `CrAnFieldOp` is total. -/
instance : IsTotal 𝓕.CrAnFieldOp 𝓕.crAnTimeOrderRel where
total a b := IsTotal.total (r := 𝓕.timeOrderRel) a.1 b.1
/-- Time ordering of `CrAnStates` is transitive. -/
instance : IsTrans 𝓕.CrAnStates 𝓕.crAnTimeOrderRel where
/-- Time ordering of `CrAnFieldOp` is transitive. -/
instance : IsTrans 𝓕.CrAnFieldOp 𝓕.crAnTimeOrderRel where
trans a b c := IsTrans.trans (r := 𝓕.timeOrderRel) a.1 b.1 c.1
@[simp]
lemma crAnTimeOrderRel_refl (φ : 𝓕.CrAnStates) : crAnTimeOrderRel φ φ := by
lemma crAnTimeOrderRel_refl (φ : 𝓕.CrAnFieldOp) : crAnTimeOrderRel φ φ := by
exact (IsTotal.to_isRefl (r := 𝓕.crAnTimeOrderRel)).refl φ
/-- The sign associated with putting a list of `CrAnStates` into time order (with
/-- The sign associated with putting a list of `CrAnFieldOp` into time order (with
the state of greatest time to the left).
We pick up a minus sign for every fermion paired crossed. -/
def crAnTimeOrderSign (φs : List 𝓕.CrAnStates) : ℂ :=
def crAnTimeOrderSign (φs : List 𝓕.CrAnFieldOp) : ℂ :=
Wick.koszulSign 𝓕.crAnStatistics 𝓕.crAnTimeOrderRel φs
@[simp]
@ -222,45 +222,45 @@ lemma crAnTimeOrderSign_nil : crAnTimeOrderSign (𝓕 := 𝓕) [] = 1 := by
simp only [crAnTimeOrderSign]
rfl
lemma crAnTimeOrderSign_pair_ordered {φ ψ : 𝓕.CrAnStates} (h : crAnTimeOrderRel φ ψ) :
lemma crAnTimeOrderSign_pair_ordered {φ ψ : 𝓕.CrAnFieldOp} (h : crAnTimeOrderRel φ ψ) :
crAnTimeOrderSign [φ, ψ] = 1 := by
simp only [crAnTimeOrderSign, Wick.koszulSign, Wick.koszulSignInsert, mul_one, ite_eq_left_iff,
ite_eq_right_iff, and_imp]
exact fun h' => False.elim (h' h)
lemma crAnTimeOrderSign_pair_not_ordered {φ ψ : 𝓕.CrAnStates} (h : ¬ crAnTimeOrderRel φ ψ) :
lemma crAnTimeOrderSign_pair_not_ordered {φ ψ : 𝓕.CrAnFieldOp} (h : ¬ crAnTimeOrderRel φ ψ) :
crAnTimeOrderSign [φ, ψ] = 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ψ) := by
simp only [crAnTimeOrderSign, Wick.koszulSign, Wick.koszulSignInsert, mul_one, instCommGroup.eq_1]
rw [if_neg h]
simp [FieldStatistic.exchangeSign_eq_if]
lemma crAnTimeOrderSign_swap_eq_time {φ ψ : 𝓕.CrAnStates}
(h1 : crAnTimeOrderRel φ ψ) (h2 : crAnTimeOrderRel ψ φ) (φs φs' : List 𝓕.CrAnStates) :
lemma crAnTimeOrderSign_swap_eq_time {φ ψ : 𝓕.CrAnFieldOp}
(h1 : crAnTimeOrderRel φ ψ) (h2 : crAnTimeOrderRel ψ φ) (φs φs' : List 𝓕.CrAnFieldOp) :
crAnTimeOrderSign (φs ++ φ :: ψ :: φs') = crAnTimeOrderSign (φs ++ ψ :: φ :: φs') := by
exact Wick.koszulSign_swap_eq_rel _ _ h1 h2 _ _
/-- Sort a list of `CrAnStates` based on `crAnTimeOrderRel`. -/
def crAnTimeOrderList (φs : List 𝓕.CrAnStates) : List 𝓕.CrAnStates :=
/-- Sort a list of `CrAnFieldOp` based on `crAnTimeOrderRel`. -/
def crAnTimeOrderList (φs : List 𝓕.CrAnFieldOp) : List 𝓕.CrAnFieldOp :=
List.insertionSort 𝓕.crAnTimeOrderRel φs
@[simp]
lemma crAnTimeOrderList_nil : crAnTimeOrderList (𝓕 := 𝓕) [] = [] := by
simp [crAnTimeOrderList]
lemma crAnTimeOrderList_pair_ordered {φ ψ : 𝓕.CrAnStates} (h : crAnTimeOrderRel φ ψ) :
lemma crAnTimeOrderList_pair_ordered {φ ψ : 𝓕.CrAnFieldOp} (h : crAnTimeOrderRel φ ψ) :
crAnTimeOrderList [φ, ψ] = [φ, ψ] := by
simp only [crAnTimeOrderList, List.insertionSort, List.orderedInsert, ite_eq_left_iff,
List.cons.injEq, and_true]
exact fun h' => False.elim (h' h)
lemma crAnTimeOrderList_pair_not_ordered {φ ψ : 𝓕.CrAnStates} (h : ¬ crAnTimeOrderRel φ ψ) :
lemma crAnTimeOrderList_pair_not_ordered {φ ψ : 𝓕.CrAnFieldOp} (h : ¬ crAnTimeOrderRel φ ψ) :
crAnTimeOrderList [φ, ψ] = [ψ, φ] := by
simp only [crAnTimeOrderList, List.insertionSort, List.orderedInsert, ite_eq_right_iff,
List.cons.injEq, and_true]
exact fun h' => False.elim (h h')
lemma orderedInsert_swap_eq_time {φ ψ : 𝓕.CrAnStates}
(h1 : crAnTimeOrderRel φ ψ) (h2 : crAnTimeOrderRel ψ φ) (φs : List 𝓕.CrAnStates) :
lemma orderedInsert_swap_eq_time {φ ψ : 𝓕.CrAnFieldOp}
(h1 : crAnTimeOrderRel φ ψ) (h2 : crAnTimeOrderRel ψ φ) (φs : List 𝓕.CrAnFieldOp) :
List.orderedInsert crAnTimeOrderRel φ (List.orderedInsert crAnTimeOrderRel ψ φs) =
List.takeWhile (fun b => ¬ crAnTimeOrderRel ψ b) φs ++ φ :: ψ ::
List.dropWhile (fun b => ¬ crAnTimeOrderRel ψ b) φs := by
@ -268,7 +268,7 @@ lemma orderedInsert_swap_eq_time {φ ψ : 𝓕.CrAnStates}
simp only [decide_not]
rw [List.orderedInsert_eq_take_drop]
simp only [decide_not]
have h1 (b : 𝓕.CrAnStates) : (crAnTimeOrderRel φ b) ↔ (crAnTimeOrderRel ψ b) :=
have h1 (b : 𝓕.CrAnFieldOp) : (crAnTimeOrderRel φ b) ↔ (crAnTimeOrderRel ψ b) :=
Iff.intro (fun h => IsTrans.trans _ _ _ h2 h) (fun h => IsTrans.trans _ _ _ h1 h)
simp only [h1]
rw [List.takeWhile_append]
@ -286,12 +286,12 @@ lemma orderedInsert_swap_eq_time {φ ψ : 𝓕.CrAnStates}
intro y hy
simpa using List.mem_takeWhile_imp hy
lemma orderedInsert_in_swap_eq_time {φ ψ φ': 𝓕.CrAnStates} (h1 : crAnTimeOrderRel φ ψ)
(h2 : crAnTimeOrderRel ψ φ) : (φs φs' : List 𝓕.CrAnStates) → ∃ l1 l2,
lemma orderedInsert_in_swap_eq_time {φ ψ φ': 𝓕.CrAnFieldOp} (h1 : crAnTimeOrderRel φ ψ)
(h2 : crAnTimeOrderRel ψ φ) : (φs φs' : List 𝓕.CrAnFieldOp) → ∃ l1 l2,
List.orderedInsert crAnTimeOrderRel φ' (φs ++ φ :: ψ :: φs') = l1 ++ φ :: ψ :: l2 ∧
List.orderedInsert crAnTimeOrderRel φ' (φs ++ ψ :: φ :: φs') = l1 ++ ψ :: φ :: l2
| [], φs' => by
have h1 (b : 𝓕.CrAnStates) : (crAnTimeOrderRel b φ) ↔ (crAnTimeOrderRel b ψ) :=
have h1 (b : 𝓕.CrAnFieldOp) : (crAnTimeOrderRel b φ) ↔ (crAnTimeOrderRel b ψ) :=
Iff.intro (fun h => IsTrans.trans _ _ _ h h1) (fun h => IsTrans.trans _ _ _ h h2)
by_cases h : crAnTimeOrderRel φ' φ
· simp only [List.orderedInsert, h, ↓reduceIte, ← h1 φ']
@ -312,10 +312,10 @@ lemma orderedInsert_in_swap_eq_time {φ ψ φ': 𝓕.CrAnStates} (h1 : crAnTimeO
use (φ'' :: l1), l2
simp
lemma crAnTimeOrderList_swap_eq_time {φ ψ : 𝓕.CrAnStates}
lemma crAnTimeOrderList_swap_eq_time {φ ψ : 𝓕.CrAnFieldOp}
(h1 : crAnTimeOrderRel φ ψ) (h2 : crAnTimeOrderRel ψ φ) :
(φs φs' : List 𝓕.CrAnStates) →
∃ (l1 l2 : List 𝓕.CrAnStates),
(φs φs' : List 𝓕.CrAnFieldOp) →
∃ (l1 l2 : List 𝓕.CrAnFieldOp),
crAnTimeOrderList (φs ++ φ :: ψ :: φs') = l1 ++ φ :: ψ :: l2 ∧
crAnTimeOrderList (φs ++ ψ :: φ :: φs') = l1 ++ ψ :: φ :: l2
| [], φs' => by
@ -325,7 +325,7 @@ lemma crAnTimeOrderList_swap_eq_time {φ ψ : 𝓕.CrAnStates}
List.dropWhile (fun b => ¬ crAnTimeOrderRel ψ b) (List.insertionSort crAnTimeOrderRel φs')
apply And.intro
· exact orderedInsert_swap_eq_time h1 h2 _
· have h1' (b : 𝓕.CrAnStates) : (crAnTimeOrderRel φ b) ↔ (crAnTimeOrderRel ψ b) :=
· have h1' (b : 𝓕.CrAnFieldOp) : (crAnTimeOrderRel φ b) ↔ (crAnTimeOrderRel ψ b) :=
Iff.intro (fun h => IsTrans.trans _ _ _ h2 h) (fun h => IsTrans.trans _ _ _ h1 h)
simp only [← h1', decide_not]
simpa using orderedInsert_swap_eq_time h2 h1 _
@ -344,8 +344,8 @@ lemma crAnTimeOrderList_swap_eq_time {φ ψ : 𝓕.CrAnStates}
## Relationship to sections
-/
lemma koszulSignInsert_crAnTimeOrderRel_crAnSection {φ : 𝓕.States} {ψ : 𝓕.CrAnStates}
(h : ψ.1 = φ) : {φs : List 𝓕.States} → (ψs : CrAnSection φs) →
lemma koszulSignInsert_crAnTimeOrderRel_crAnSection {φ : 𝓕.FieldOp} {ψ : 𝓕.CrAnFieldOp}
(h : ψ.1 = φ) : {φs : List 𝓕.FieldOp} → (ψs : CrAnSection φs) →
Wick.koszulSignInsert 𝓕.crAnStatistics 𝓕.crAnTimeOrderRel ψ ψs.1 =
Wick.koszulSignInsert 𝓕.statesStatistic 𝓕.timeOrderRel φ φs
| [], ⟨[], h⟩ => by
@ -357,14 +357,14 @@ lemma koszulSignInsert_crAnTimeOrderRel_crAnSection {φ : 𝓕.States} {ψ :
rw [hi]
congr
· exact h1.1
· simp only [crAnStatistics, crAnStatesToStates, Function.comp_apply]
· simp only [crAnStatistics, crAnFieldOpToFieldOp, Function.comp_apply]
congr
· simp only [crAnStatistics, crAnStatesToStates, Function.comp_apply]
· simp only [crAnStatistics, crAnFieldOpToFieldOp, Function.comp_apply]
congr
exact h1.1
@[simp]
lemma crAnTimeOrderSign_crAnSection : {φs : List 𝓕.States} → (ψs : CrAnSection φs) →
lemma crAnTimeOrderSign_crAnSection : {φs : List 𝓕.FieldOp} → (ψs : CrAnSection φs) →
crAnTimeOrderSign ψs.1 = timeOrderSign φs
| [], ⟨[], h⟩ => by
simp
@ -375,9 +375,9 @@ lemma crAnTimeOrderSign_crAnSection : {φs : List 𝓕.States} → (ψs : CrAnSe
· rw [koszulSignInsert_crAnTimeOrderRel_crAnSection h.1 ⟨ψs, h.2⟩]
· exact crAnTimeOrderSign_crAnSection ⟨ψs, h.2⟩
lemma orderedInsert_crAnTimeOrderRel_crAnSection {φ : 𝓕.States} {ψ : 𝓕.CrAnStates}
(h : ψ.1 = φ) : {φs : List 𝓕.States} → (ψs : CrAnSection φs) →
(List.orderedInsert 𝓕.crAnTimeOrderRel ψ ψs.1).map 𝓕.crAnStatesToStates =
lemma orderedInsert_crAnTimeOrderRel_crAnSection {φ : 𝓕.FieldOp} {ψ : 𝓕.CrAnFieldOp}
(h : ψ.1 = φ) : {φs : List 𝓕.FieldOp} → (ψs : CrAnSection φs) →
(List.orderedInsert 𝓕.crAnTimeOrderRel ψ ψs.1).map 𝓕.crAnFieldOpToFieldOp =
List.orderedInsert 𝓕.timeOrderRel φ φs
| [], ⟨[], _⟩ => by
simp only [List.orderedInsert, List.map_cons, List.map_nil, List.cons.injEq, and_true]
@ -388,18 +388,18 @@ lemma orderedInsert_crAnTimeOrderRel_crAnSection {φ : 𝓕.States} {ψ : 𝓕.C
by_cases hr : timeOrderRel φ φ'
· simp only [hr, ↓reduceIte]
rw [← h1.1] at hr
simp only [crAnStatesToStates] at hr
simp only [crAnFieldOpToFieldOp] at hr
simp only [hr, ↓reduceIte, List.map_cons, List.cons.injEq]
exact And.intro h (And.intro h1.1 h1.2)
· simp only [hr, ↓reduceIte]
rw [← h1.1] at hr
simp only [crAnStatesToStates] at hr
simp only [crAnFieldOpToFieldOp] at hr
simp only [hr, ↓reduceIte, List.map_cons, List.cons.injEq]
apply And.intro h1.1
exact orderedInsert_crAnTimeOrderRel_crAnSection h ⟨ψs, h1.2⟩
lemma crAnTimeOrderList_crAnSection_is_crAnSection : {φs : List 𝓕.States} → (ψs : CrAnSection φs) →
(crAnTimeOrderList ψs.1).map 𝓕.crAnStatesToStates = timeOrderList φs
lemma crAnTimeOrderList_crAnSection_is_crAnSection : {φs : List 𝓕.FieldOp} → (ψs : CrAnSection φs) →
(crAnTimeOrderList ψs.1).map 𝓕.crAnFieldOpToFieldOp = timeOrderList φs
| [], ⟨[], h⟩ => by
simp
| φ :: φs, ⟨ψ :: ψs, h⟩ => by
@ -409,12 +409,12 @@ lemma crAnTimeOrderList_crAnSection_is_crAnSection : {φs : List 𝓕.States}
crAnTimeOrderList_crAnSection_is_crAnSection ⟨ψs, h.2⟩⟩
/-- Time ordering of sections of a list of states. -/
def crAnSectionTimeOrder (φs : List 𝓕.States) (ψs : CrAnSection φs) :
def crAnSectionTimeOrder (φs : List 𝓕.FieldOp) (ψs : CrAnSection φs) :
CrAnSection (timeOrderList φs) :=
⟨crAnTimeOrderList ψs.1, crAnTimeOrderList_crAnSection_is_crAnSection ψs⟩
lemma orderedInsert_crAnTimeOrderRel_injective {ψ ψ' : 𝓕.CrAnStates} (h : ψ.1 = ψ'.1) :
{φs : List 𝓕.States} → (ψs ψs' : 𝓕.CrAnSection φs) →
lemma orderedInsert_crAnTimeOrderRel_injective {ψ ψ' : 𝓕.CrAnFieldOp} (h : ψ.1 = ψ'.1) :
{φs : List 𝓕.FieldOp} → (ψs ψs' : 𝓕.CrAnSection φs) →
(ho : List.orderedInsert crAnTimeOrderRel ψ ψs.1 =
List.orderedInsert crAnTimeOrderRel ψ' ψs'.1) → ψ = ψ' ∧ ψs = ψs'
| [], ⟨[], _⟩, ⟨[], _⟩, h => by
@ -430,7 +430,7 @@ lemma orderedInsert_crAnTimeOrderRel_injective {ψ ψ' : 𝓕.CrAnStates} (h :
· simp_all
· simp only [crAnTimeOrderRel] at hr hr2
simp_all only
rw [crAnStatesToStates] at h1 h1'
rw [crAnFieldOpToFieldOp] at h1 h1'
rw [h1.1] at hr
rw [h1'.1] at hr2
exact False.elim (hr2 hr)
@ -438,7 +438,7 @@ lemma orderedInsert_crAnTimeOrderRel_injective {ψ ψ' : 𝓕.CrAnStates} (h :
by_cases hr2 : crAnTimeOrderRel ψ' ψ1'
· simp only [crAnTimeOrderRel] at hr hr2
simp_all only
rw [crAnStatesToStates] at h1 h1'
rw [crAnFieldOpToFieldOp] at h1 h1'
rw [h1.1] at hr
rw [h1'.1] at hr2
exact False.elim (hr hr2)
@ -450,7 +450,7 @@ lemma orderedInsert_crAnTimeOrderRel_injective {ψ ψ' : 𝓕.CrAnStates} (h :
rw [Subtype.eq_iff] at ih'
exact ih'.2
lemma crAnSectionTimeOrder_injective : {φs : List 𝓕.States} →
lemma crAnSectionTimeOrder_injective : {φs : List 𝓕.FieldOp} →
Function.Injective (𝓕.crAnSectionTimeOrder φs)
| [], ⟨[], _⟩, ⟨[], _⟩ => by
simp
@ -462,7 +462,7 @@ lemma crAnSectionTimeOrder_injective : {φs : List 𝓕.States} →
rw [Subtype.eq_iff] at h1
simp only [crAnTimeOrderList, List.insertionSort] at h1
simp only [List.map_cons, List.cons.injEq] at h h'
rw [crAnStatesToStates] at h h'
rw [crAnFieldOpToFieldOp] at h h'
have hin := orderedInsert_crAnTimeOrderRel_injective (by rw [h.1, h'.1])
(𝓕.crAnSectionTimeOrder φs ⟨ψs, h.2⟩)
(𝓕.crAnSectionTimeOrder φs ⟨ψs', h'.2⟩) h1
@ -471,7 +471,7 @@ lemma crAnSectionTimeOrder_injective : {φs : List 𝓕.States} →
rw [Subtype.ext_iff] at hl
simpa using hl
lemma crAnSectionTimeOrder_bijective (φs : List 𝓕.States) :
lemma crAnSectionTimeOrder_bijective (φs : List 𝓕.FieldOp) :
Function.Bijective (𝓕.crAnSectionTimeOrder φs) := by
rw [Fintype.bijective_iff_injective_and_card]
apply And.intro crAnSectionTimeOrder_injective
@ -479,7 +479,7 @@ lemma crAnSectionTimeOrder_bijective (φs : List 𝓕.States) :
simp only [timeOrderList]
exact List.Perm.symm (List.perm_insertionSort timeOrderRel φs)
lemma sum_crAnSections_timeOrder {φs : List 𝓕.States} [AddCommMonoid M]
lemma sum_crAnSections_timeOrder {φs : List 𝓕.FieldOp} [AddCommMonoid M]
(f : CrAnSection (timeOrderList φs) → M) : ∑ s, f s = ∑ s, f (𝓕.crAnSectionTimeOrder φs s) := by
erw [(Equiv.ofBijective _ (𝓕.crAnSectionTimeOrder_bijective φs)).sum_comp]
@ -489,18 +489,18 @@ lemma sum_crAnSections_timeOrder {φs : List 𝓕.States} [AddCommMonoid M]
-/
/-- The time ordering relation on `CrAnStates` such that if two CrAnStates have the same
/-- The time ordering relation on `CrAnFieldOp` such that if two CrAnFieldOp have the same
time, we normal order them. -/
def normTimeOrderRel (a b : 𝓕.CrAnStates) : Prop :=
def normTimeOrderRel (a b : 𝓕.CrAnFieldOp) : Prop :=
crAnTimeOrderRel a b ∧ (crAnTimeOrderRel b a → normalOrderRel a b)
/-- The relation `normTimeOrderRel` is decidable, but not computablly so due to
`Real.decidableLE`. -/
noncomputable instance (φ φ' : 𝓕.CrAnStates) : Decidable (normTimeOrderRel φ φ') :=
noncomputable instance (φ φ' : 𝓕.CrAnFieldOp) : Decidable (normTimeOrderRel φ φ') :=
instDecidableAnd
/-- Norm-Time ordering of `CrAnStates` is total. -/
instance : IsTotal 𝓕.CrAnStates 𝓕.normTimeOrderRel where
/-- Norm-Time ordering of `CrAnFieldOp` is total. -/
instance : IsTotal 𝓕.CrAnFieldOp 𝓕.normTimeOrderRel where
total a b := by
simp only [normTimeOrderRel]
match IsTotal.total (r := 𝓕.crAnTimeOrderRel) a b,
@ -518,8 +518,8 @@ instance : IsTotal 𝓕.CrAnStates 𝓕.normTimeOrderRel where
· simp [hn]
| Or.inr h1, Or.inr h2 => simp [h1, h2]
/-- Norm-Time ordering of `CrAnStates` is transitive. -/
instance : IsTrans 𝓕.CrAnStates 𝓕.normTimeOrderRel where
/-- Norm-Time ordering of `CrAnFieldOp` is transitive. -/
instance : IsTrans 𝓕.CrAnFieldOp 𝓕.normTimeOrderRel where
trans a b c := by
intro h1 h2
simp_all only [normTimeOrderRel]
@ -530,14 +530,14 @@ instance : IsTrans 𝓕.CrAnStates 𝓕.normTimeOrderRel where
· exact IsTrans.trans _ _ _ h2.1 hc
· exact IsTrans.trans _ _ _ hc h1.1
/-- The sign associated with putting a list of `CrAnStates` into normal-time order (with
/-- The sign associated with putting a list of `CrAnFieldOp` into normal-time order (with
the state of greatest time to the left).
We pick up a minus sign for every fermion paired crossed. -/
def normTimeOrderSign (φs : List 𝓕.CrAnStates) : ℂ :=
def normTimeOrderSign (φs : List 𝓕.CrAnFieldOp) : ℂ :=
Wick.koszulSign 𝓕.crAnStatistics 𝓕.normTimeOrderRel φs
/-- Sort a list of `CrAnStates` based on `normTimeOrderRel`. -/
def normTimeOrderList (φs : List 𝓕.CrAnStates) : List 𝓕.CrAnStates :=
/-- Sort a list of `CrAnFieldOp` based on `normTimeOrderRel`. -/
def normTimeOrderList (φs : List 𝓕.CrAnFieldOp) : List 𝓕.CrAnFieldOp :=
List.insertionSort 𝓕.normTimeOrderRel φs
end