Time ordering of states

Time ordering for states

def FieldSpecification.timeOrderRel {𝓕 : FieldSpecification} : 𝓕.FieldOp → 𝓕.FieldOp → Prop

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.

Equations

• FieldSpecification.timeOrderRel (FieldSpecification.FieldOp.outAsymp a) x✝ = True
• FieldSpecification.timeOrderRel (FieldSpecification.FieldOp.position φ0) (FieldSpecification.FieldOp.position φ1) = (φ1.2 0 ≤ φ0.2 0)
• FieldSpecification.timeOrderRel (FieldSpecification.FieldOp.position a) (FieldSpecification.FieldOp.inAsymp a_1) = True
• FieldSpecification.timeOrderRel (FieldSpecification.FieldOp.position a) (FieldSpecification.FieldOp.outAsymp a_1) = False
• FieldSpecification.timeOrderRel (FieldSpecification.FieldOp.inAsymp a) (FieldSpecification.FieldOp.outAsymp a_1) = False
• FieldSpecification.timeOrderRel (FieldSpecification.FieldOp.inAsymp a) (FieldSpecification.FieldOp.position a_1) = False
• FieldSpecification.timeOrderRel (FieldSpecification.FieldOp.inAsymp a) (FieldSpecification.FieldOp.inAsymp a_1) = True

noncomputable instance FieldSpecification.instDecidableTimeOrderRel {𝓕 : FieldSpecification} (φ φ' : 𝓕.FieldOp) : Decidable (timeOrderRel φ φ')

The relation timeOrderRel is decidable, but not computable so due to Real.decidableLE.

Equations

• FieldSpecification.instDecidableTimeOrderRel (FieldSpecification.FieldOp.outAsymp a) x✝ = isTrue True.intro
• FieldSpecification.instDecidableTimeOrderRel (FieldSpecification.FieldOp.position φ0) (FieldSpecification.FieldOp.position φ1) = inferInstanceAs (Decidable (φ1.2 0 ≤ φ0.2 0))
• FieldSpecification.instDecidableTimeOrderRel (FieldSpecification.FieldOp.position a) (FieldSpecification.FieldOp.inAsymp a_1) = isTrue True.intro
• FieldSpecification.instDecidableTimeOrderRel (FieldSpecification.FieldOp.position a) (FieldSpecification.FieldOp.outAsymp a_1) = isFalse ⋯
• FieldSpecification.instDecidableTimeOrderRel (FieldSpecification.FieldOp.inAsymp a) (FieldSpecification.FieldOp.outAsymp a_1) = isFalse ⋯
• FieldSpecification.instDecidableTimeOrderRel (FieldSpecification.FieldOp.inAsymp a) (FieldSpecification.FieldOp.position a_1) = isFalse ⋯
• FieldSpecification.instDecidableTimeOrderRel (FieldSpecification.FieldOp.inAsymp a) (FieldSpecification.FieldOp.inAsymp a_1) = isTrue True.intro

instance FieldSpecification.instIsTotalFieldOpTimeOrderRel {𝓕 : FieldSpecification} : IsTotal 𝓕.FieldOp timeOrderRel

Time ordering is total.

instance FieldSpecification.instIsTransFieldOpTimeOrderRel {𝓕 : FieldSpecification} : IsTrans 𝓕.FieldOp timeOrderRel

Time ordering is transitive.

def FieldSpecification.maxTimeFieldPos {𝓕 : FieldSpecification} (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) : ℕ

Given a list φ :: φs of states, the (zero-based) position of the state which is of maximum time. For example

• 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.

Equations

• FieldSpecification.maxTimeFieldPos φ φs = ↑(PhysLean.List.insertionSortMinPos FieldSpecification.timeOrderRel φ φs)

theorem FieldSpecification.maxTimeFieldPos_lt_length {𝓕 : FieldSpecification} (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) : maxTimeFieldPos φ φs < (φ :: φs).length

def FieldSpecification.maxTimeField {𝓕 : FieldSpecification} (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) : 𝓕.FieldOp

Given a list φ :: φs of states, the left-most state of maximum time, if there are more. As an example:

• 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.

Equations

• FieldSpecification.maxTimeField φ φs = PhysLean.List.insertionSortMin FieldSpecification.timeOrderRel φ φs

def FieldSpecification.eraseMaxTimeField {𝓕 : FieldSpecification} (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) : List 𝓕.FieldOp

Given a list φ :: φs of states, the list with the left-most state of maximum time removed. As an example:

• 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)].

Equations

• FieldSpecification.eraseMaxTimeField φ φs = PhysLean.List.insertionSortDropMinPos FieldSpecification.timeOrderRel φ φs

@[simp]

theorem FieldSpecification.eraseMaxTimeField_length {𝓕 : FieldSpecification} (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) : (eraseMaxTimeField φ φs).length = φs.length

theorem FieldSpecification.maxTimeFieldPos_lt_eraseMaxTimeField_length_succ {𝓕 : FieldSpecification} (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) : maxTimeFieldPos φ φs < (eraseMaxTimeField φ φs).length.succ

def FieldSpecification.maxTimeFieldPosFin {𝓕 : FieldSpecification} (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) : Fin (eraseMaxTimeField φ φs).length.succ

Given a list φ :: φs of states, the position of the left-most state of maximum time as an element of Fin (eraseMaxTimeField φ φs).length.succ. As an example:

• for the list [φ1(t = 4), φ2(t = 5), φ3(t = 3), φ4(t = 5)] this would return ⟨1,...⟩.

Equations

• FieldSpecification.maxTimeFieldPosFin φ φs = PhysLean.List.insertionSortMinPosFin FieldSpecification.timeOrderRel φ φs

theorem FieldSpecification.lt_maxTimeFieldPosFin_not_timeOrder {𝓕 : FieldSpecification} (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) (i : Fin (eraseMaxTimeField φ φs).length) (hi : (maxTimeFieldPosFin φ φs).succAbove i < maxTimeFieldPosFin φ φs) : ¬timeOrderRel (eraseMaxTimeField φ φs)[↑i] (maxTimeField φ φs)

theorem FieldSpecification.timeOrder_maxTimeField {𝓕 : FieldSpecification} (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) (i : Fin (eraseMaxTimeField φ φs).length) : timeOrderRel (maxTimeField φ φs) (eraseMaxTimeField φ φs)[↑i]

def FieldSpecification.timeOrderSign {𝓕 : FieldSpecification} (φs : List 𝓕.FieldOp) : ℂ

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.

Equations

• FieldSpecification.timeOrderSign φs = Wick.koszulSign 𝓕.fieldOpStatistic FieldSpecification.timeOrderRel φs

@[simp]

theorem FieldSpecification.timeOrderSign_nil {𝓕 : FieldSpecification} : timeOrderSign [] = 1

theorem FieldSpecification.timeOrderSign_pair_ordered {𝓕 : FieldSpecification} {φ ψ : 𝓕.FieldOp} (h : timeOrderRel φ ψ) : timeOrderSign [φ, ψ] = 1

theorem FieldSpecification.timeOrderSign_pair_not_ordered {𝓕 : FieldSpecification} {φ ψ : 𝓕.FieldOp} (h : ¬timeOrderRel φ ψ) : timeOrderSign [φ, ψ] = (FieldStatistic.exchangeSign (𝓕.fieldOpStatistic φ)) (𝓕.fieldOpStatistic ψ)

theorem FieldSpecification.timerOrderSign_of_eraseMaxTimeField {𝓕 : FieldSpecification} (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) : timeOrderSign (eraseMaxTimeField φ φs) = timeOrderSign (φ :: φs) * (FieldStatistic.exchangeSign (𝓕.fieldOpStatistic (maxTimeField φ φs))) (FieldStatistic.ofList 𝓕.fieldOpStatistic (List.take (maxTimeFieldPos φ φs) (φ :: φs)))

def FieldSpecification.timeOrderList {𝓕 : FieldSpecification} (φs : List 𝓕.FieldOp) : List 𝓕.FieldOp

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)]

Equations

• FieldSpecification.timeOrderList φs = List.insertionSort FieldSpecification.timeOrderRel φs

theorem FieldSpecification.timeOrderList_pair_ordered {𝓕 : FieldSpecification} {φ ψ : 𝓕.FieldOp} (h : timeOrderRel φ ψ) : timeOrderList [φ, ψ] = [φ, ψ]

theorem FieldSpecification.timeOrderList_pair_not_ordered {𝓕 : FieldSpecification} {φ ψ : 𝓕.FieldOp} (h : ¬timeOrderRel φ ψ) : timeOrderList [φ, ψ] = [ψ, φ]

@[simp]

theorem FieldSpecification.timeOrderList_nil {𝓕 : FieldSpecification} : timeOrderList [] = []

theorem FieldSpecification.timeOrderList_eq_maxTimeField_timeOrderList {𝓕 : FieldSpecification} (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) : timeOrderList (φ :: φs) = maxTimeField φ φs :: timeOrderList (eraseMaxTimeField φ φs)

Time ordering for CrAnFieldOp

timeOrderRel

def FieldSpecification.crAnTimeOrderRel {𝓕 : FieldSpecification} (a b : 𝓕.CrAnFieldOp) : Prop

For a field specification 𝓕, 𝓕.crAnTimeOrderRel is a relation on 𝓕.CrAnFieldOp representing time ordering. It is defined such that 𝓕.crAnTimeOrderRel φ₀ φ₁ is true if and only if one of the following holds

• φ₀ is an outgoing asymptotic operator
• φ₁ is an incoming asymptotic field operator
• φ₀ and φ₁ are both position field operators where the SpaceTime point of φ₀ has a time greater than or equal to that of φ₁.

Thus, colloquially 𝓕.crAnTimeOrderRel φ₀ φ₁ if φ₀ has time greater than or equal to φ₁. The use of greater than rather then less than is because on ordering lists of operators it is needed that the operator with the greatest time is to the left.

Equations

• FieldSpecification.crAnTimeOrderRel a b = FieldSpecification.timeOrderRel a.fst b.fst

noncomputable instance FieldSpecification.instDecidableCrAnTimeOrderRel {𝓕 : FieldSpecification} (φ φ' : 𝓕.CrAnFieldOp) : Decidable (crAnTimeOrderRel φ φ')

The relation crAnTimeOrderRel is decidable, but not computable so due to Real.decidableLE.

Equations

• FieldSpecification.instDecidableCrAnTimeOrderRel φ φ' = inferInstanceAs (Decidable (FieldSpecification.timeOrderRel φ.fst φ'.fst))

instance FieldSpecification.instIsTotalCrAnFieldOpCrAnTimeOrderRel {𝓕 : FieldSpecification} : IsTotal 𝓕.CrAnFieldOp crAnTimeOrderRel

Time ordering of CrAnFieldOp is total.

instance FieldSpecification.instIsTransCrAnFieldOpCrAnTimeOrderRel {𝓕 : FieldSpecification} : IsTrans 𝓕.CrAnFieldOp crAnTimeOrderRel

Time ordering of CrAnFieldOp is transitive.

@[simp]

theorem FieldSpecification.crAnTimeOrderRel_refl {𝓕 : FieldSpecification} (φ : 𝓕.CrAnFieldOp) : crAnTimeOrderRel φ φ

def FieldSpecification.crAnTimeOrderSign {𝓕 : FieldSpecification} (φs : List 𝓕.CrAnFieldOp) : ℂ

For a field specification 𝓕, and a list φs of 𝓕.CrAnFieldOp, 𝓕.crAnTimeOrderSign φs is the sign corresponding to the number of ferimionic-fermionic exchanges undertaken to time-order (i.e. order with respect to 𝓕.crAnTimeOrderRel) φs using the insertion sort algorithm.

Equations

• FieldSpecification.crAnTimeOrderSign φs = Wick.koszulSign 𝓕.crAnStatistics FieldSpecification.crAnTimeOrderRel φs

@[simp]

theorem FieldSpecification.crAnTimeOrderSign_nil {𝓕 : FieldSpecification} : crAnTimeOrderSign [] = 1

theorem FieldSpecification.crAnTimeOrderSign_pair_ordered {𝓕 : FieldSpecification} {φ ψ : 𝓕.CrAnFieldOp} (h : crAnTimeOrderRel φ ψ) : crAnTimeOrderSign [φ, ψ] = 1

theorem FieldSpecification.crAnTimeOrderSign_pair_not_ordered {𝓕 : FieldSpecification} {φ ψ : 𝓕.CrAnFieldOp} (h : ¬crAnTimeOrderRel φ ψ) : crAnTimeOrderSign [φ, ψ] = (FieldStatistic.exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ)

theorem FieldSpecification.crAnTimeOrderSign_swap_eq_time {𝓕 : FieldSpecification} {φ ψ : 𝓕.CrAnFieldOp} (h1 : crAnTimeOrderRel φ ψ) (h2 : crAnTimeOrderRel ψ φ) (φs φs' : List 𝓕.CrAnFieldOp) : crAnTimeOrderSign (φs ++ φ :: ψ :: φs') = crAnTimeOrderSign (φs ++ ψ :: φ :: φs')

def FieldSpecification.crAnTimeOrderList {𝓕 : FieldSpecification} (φs : List 𝓕.CrAnFieldOp) : List 𝓕.CrAnFieldOp

For a field specification 𝓕, and a list φs of 𝓕.CrAnFieldOp, 𝓕.crAnTimeOrderList φs is the list φs time-ordered using the insertion sort algorithm.

Equations

• FieldSpecification.crAnTimeOrderList φs = List.insertionSort FieldSpecification.crAnTimeOrderRel φs

@[simp]

theorem FieldSpecification.crAnTimeOrderList_nil {𝓕 : FieldSpecification} : crAnTimeOrderList [] = []

theorem FieldSpecification.crAnTimeOrderList_pair_ordered {𝓕 : FieldSpecification} {φ ψ : 𝓕.CrAnFieldOp} (h : crAnTimeOrderRel φ ψ) : crAnTimeOrderList [φ, ψ] = [φ, ψ]

theorem FieldSpecification.crAnTimeOrderList_pair_not_ordered {𝓕 : FieldSpecification} {φ ψ : 𝓕.CrAnFieldOp} (h : ¬crAnTimeOrderRel φ ψ) : crAnTimeOrderList [φ, ψ] = [ψ, φ]

theorem FieldSpecification.orderedInsert_swap_eq_time {𝓕 : FieldSpecification} {φ ψ : 𝓕.CrAnFieldOp} (h1 : crAnTimeOrderRel φ ψ) (h2 : crAnTimeOrderRel ψ φ) (φs : List 𝓕.CrAnFieldOp) : List.orderedInsert crAnTimeOrderRel φ (List.orderedInsert crAnTimeOrderRel ψ φs) = List.takeWhile (fun (b : 𝓕.CrAnFieldOp) => decide ¬crAnTimeOrderRel ψ b) φs ++ φ :: ψ :: List.dropWhile (fun (b : 𝓕.CrAnFieldOp) => decide ¬crAnTimeOrderRel ψ b) φs

theorem FieldSpecification.orderedInsert_in_swap_eq_time {𝓕 : FieldSpecification} {φ ψ φ' : 𝓕.CrAnFieldOp} (h1 : crAnTimeOrderRel φ ψ) (h2 : crAnTimeOrderRel ψ φ) (φs φs' : List 𝓕.CrAnFieldOp) : ∃ (l1 : List 𝓕.CrAnFieldOp) (l2 : List 𝓕.CrAnFieldOp), List.orderedInsert crAnTimeOrderRel φ' (φs ++ φ :: ψ :: φs') = l1 ++ φ :: ψ :: l2 ∧ List.orderedInsert crAnTimeOrderRel φ' (φs ++ ψ :: φ :: φs') = l1 ++ ψ :: φ :: l2

theorem FieldSpecification.crAnTimeOrderList_swap_eq_time {𝓕 : FieldSpecification} {φ ψ : 𝓕.CrAnFieldOp} (h1 : crAnTimeOrderRel φ ψ) (h2 : crAnTimeOrderRel ψ φ) (φs φs' : List 𝓕.CrAnFieldOp) : ∃ (l1 : List 𝓕.CrAnFieldOp) (l2 : List 𝓕.CrAnFieldOp), crAnTimeOrderList (φs ++ φ :: ψ :: φs') = l1 ++ φ :: ψ :: l2 ∧ crAnTimeOrderList (φs ++ ψ :: φ :: φs') = l1 ++ ψ :: φ :: l2

Relationship to sections

theorem FieldSpecification.koszulSignInsert_crAnTimeOrderRel_crAnSection {𝓕 : FieldSpecification} {φ : 𝓕.FieldOp} {ψ : 𝓕.CrAnFieldOp} (h : ψ.fst = φ) {φs : List 𝓕.FieldOp} (ψs : CrAnSection φs) : Wick.koszulSignInsert 𝓕.crAnStatistics crAnTimeOrderRel ψ ↑ψs = Wick.koszulSignInsert 𝓕.fieldOpStatistic timeOrderRel φ φs

@[simp]

theorem FieldSpecification.crAnTimeOrderSign_crAnSection {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} (ψs : CrAnSection φs) : crAnTimeOrderSign ↑ψs = timeOrderSign φs

theorem FieldSpecification.orderedInsert_crAnTimeOrderRel_crAnSection {𝓕 : FieldSpecification} {φ : 𝓕.FieldOp} {ψ : 𝓕.CrAnFieldOp} (h : ψ.fst = φ) {φs : List 𝓕.FieldOp} (ψs : CrAnSection φs) : List.map 𝓕.crAnFieldOpToFieldOp (List.orderedInsert crAnTimeOrderRel ψ ↑ψs) = List.orderedInsert timeOrderRel φ φs

theorem FieldSpecification.crAnTimeOrderList_crAnSection_is_crAnSection {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} (ψs : CrAnSection φs) : List.map 𝓕.crAnFieldOpToFieldOp (crAnTimeOrderList ↑ψs) = timeOrderList φs

def FieldSpecification.crAnSectionTimeOrder {𝓕 : FieldSpecification} (φs : List 𝓕.FieldOp) (ψs : CrAnSection φs) : CrAnSection (timeOrderList φs)

Time ordering of sections of a list of states.

Equations

• FieldSpecification.crAnSectionTimeOrder φs ψs = ⟨FieldSpecification.crAnTimeOrderList ↑ψs, ⋯⟩

theorem FieldSpecification.orderedInsert_crAnTimeOrderRel_injective {𝓕 : FieldSpecification} {ψ ψ' : 𝓕.CrAnFieldOp} (h : ψ.fst = ψ'.fst) {φs : List 𝓕.FieldOp} (ψs ψs' : CrAnSection φs) (ho : List.orderedInsert crAnTimeOrderRel ψ ↑ψs = List.orderedInsert crAnTimeOrderRel ψ' ↑ψs') : ψ = ψ' ∧ ψs = ψs'

theorem FieldSpecification.crAnSectionTimeOrder_injective {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} : Function.Injective (crAnSectionTimeOrder φs)

theorem FieldSpecification.crAnSectionTimeOrder_bijective {𝓕 : FieldSpecification} (φs : List 𝓕.FieldOp) : Function.Bijective (crAnSectionTimeOrder φs)

theorem FieldSpecification.sum_crAnSections_timeOrder {𝓕 : FieldSpecification} {M : Type u_1} {φs : List 𝓕.FieldOp} [AddCommMonoid M] (f : CrAnSection (timeOrderList φs) → M) : ∑ s : CrAnSection (timeOrderList φs), f s = ∑ s : CrAnSection φs, f (crAnSectionTimeOrder φs s)

normTimeOrderRel

def FieldSpecification.normTimeOrderRel {𝓕 : FieldSpecification} (a b : 𝓕.CrAnFieldOp) : Prop

The time ordering relation on CrAnFieldOp such that if two CrAnFieldOp have the same time, we normal order them.

Equations

• FieldSpecification.normTimeOrderRel a b = (FieldSpecification.crAnTimeOrderRel a b ∧ (FieldSpecification.crAnTimeOrderRel b a → FieldSpecification.normalOrderRel a b))

noncomputable instance FieldSpecification.instDecidableNormTimeOrderRel {𝓕 : FieldSpecification} (φ φ' : 𝓕.CrAnFieldOp) : Decidable (normTimeOrderRel φ φ')

The relation normTimeOrderRel is decidable, but not computable so due to Real.decidableLE.

Equations

• FieldSpecification.instDecidableNormTimeOrderRel φ φ' = instDecidableAnd

instance FieldSpecification.instIsTotalCrAnFieldOpNormTimeOrderRel {𝓕 : FieldSpecification} : IsTotal 𝓕.CrAnFieldOp normTimeOrderRel

Norm-Time ordering of CrAnFieldOp is total.

instance FieldSpecification.instIsTransCrAnFieldOpNormTimeOrderRel {𝓕 : FieldSpecification} : IsTrans 𝓕.CrAnFieldOp normTimeOrderRel

Norm-Time ordering of CrAnFieldOp is transitive.

def FieldSpecification.normTimeOrderSign {𝓕 : FieldSpecification} (φs : List 𝓕.CrAnFieldOp) : ℂ

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.

Equations

• FieldSpecification.normTimeOrderSign φs = Wick.koszulSign 𝓕.crAnStatistics FieldSpecification.normTimeOrderRel φs

def FieldSpecification.normTimeOrderList {𝓕 : FieldSpecification} (φs : List 𝓕.CrAnFieldOp) : List 𝓕.CrAnFieldOp

Sort a list of CrAnFieldOp based on normTimeOrderRel.

Equations

• FieldSpecification.normTimeOrderList φs = List.insertionSort FieldSpecification.normTimeOrderRel φs