PhysLean Documentation

PhysLean.QFT.PerturbationTheory.FieldSpecification.NormalOrder

Normal Ordering of states #

source
def FieldSpecification.normalOrderRel {𝓕 : FieldSpecification} :
𝓕.CrAnFieldOp β†’ 𝓕.CrAnFieldOp β†’ Prop

For a field specification 𝓕, 𝓕.normalOrderRel is a relation on 𝓕.CrAnFieldOp representing normal ordering. It is defined such that 𝓕.normalOrderRel Ο†β‚€ φ₁ is true if one of the following is true

  • Ο†β‚€ is a field creation operator
  • φ₁ is a field annihilation operator.

Thus, colloquially 𝓕.normalOrderRel Ο†β‚€ φ₁ says the creation operators are less than annihilation operators.

Equations
Instances For
    source
    instance FieldSpecification.instIsTotalCrAnFieldOpNormalOrderRel {𝓕 : FieldSpecification} :
    IsTotal 𝓕.CrAnFieldOp normalOrderRel

    Normal ordering is total.

    source
    instance FieldSpecification.instIsTransCrAnFieldOpNormalOrderRel {𝓕 : FieldSpecification} :
    IsTrans 𝓕.CrAnFieldOp normalOrderRel

    Normal ordering is transitive.

    source
    instance FieldSpecification.instDecidableNormalOrderRel {𝓕 : FieldSpecification} (Ο† Ο†' : 𝓕.CrAnFieldOp) :
    Decidable (normalOrderRel Ο† Ο†')

    A decidable instance on the normal ordering relation.

    Equations

    Normal order sign. #

    source
    def FieldSpecification.normalOrderSign {𝓕 : FieldSpecification} (Ο†s : List 𝓕.CrAnFieldOp) :
    β„‚

    For a field specification 𝓕, and a list Ο†s of 𝓕.CrAnFieldOp, 𝓕.normalOrderSign Ο†s is the sign corresponding to the number of fermionic-fermionic exchanges undertaken to normal-order Ο†s using the insertion sort algorithm.

    Equations
    Instances For
      source
      @[simp]
      theorem FieldSpecification.normalOrderSign_mul_self {𝓕 : FieldSpecification} (Ο†s : List 𝓕.CrAnFieldOp) :
      normalOrderSign Ο†s * normalOrderSign Ο†s = 1
      source
      theorem FieldSpecification.koszulSignInsert_create {𝓕 : FieldSpecification} (Ο† : 𝓕.CrAnFieldOp) (hΟ† : 𝓕.crAnFieldOpToCreateAnnihilate Ο† = CreateAnnihilate.create) (Ο†s : List 𝓕.CrAnFieldOp) :
      Wick.koszulSignInsert 𝓕.crAnStatistics normalOrderRel Ο† Ο†s = 1
      source
      theorem FieldSpecification.normalOrderSign_cons_create {𝓕 : FieldSpecification} (Ο† : 𝓕.CrAnFieldOp) (hΟ† : 𝓕.crAnFieldOpToCreateAnnihilate Ο† = CreateAnnihilate.create) (Ο†s : List 𝓕.CrAnFieldOp) :
      normalOrderSign (Ο† :: Ο†s) = normalOrderSign Ο†s
      source
      @[simp]
      theorem FieldSpecification.normalOrderSign_singleton {𝓕 : FieldSpecification} (Ο† : 𝓕.CrAnFieldOp) :
      normalOrderSign [Ο†] = 1
      source
      @[simp]
      theorem FieldSpecification.normalOrderSign_nil {𝓕 : FieldSpecification} :
      normalOrderSign [] = 1
      source
      theorem FieldSpecification.koszulSignInsert_append_annihilate {𝓕 : FieldSpecification} (Ο†' Ο† : 𝓕.CrAnFieldOp) (hΟ† : 𝓕.crAnFieldOpToCreateAnnihilate Ο† = CreateAnnihilate.annihilate) (Ο†s : List 𝓕.CrAnFieldOp) :
      Wick.koszulSignInsert 𝓕.crAnStatistics normalOrderRel Ο†' (Ο†s ++ [Ο†]) = Wick.koszulSignInsert 𝓕.crAnStatistics normalOrderRel Ο†' Ο†s
      source
      theorem FieldSpecification.normalOrderSign_append_annihilate {𝓕 : FieldSpecification} (Ο† : 𝓕.CrAnFieldOp) (hΟ† : 𝓕.crAnFieldOpToCreateAnnihilate Ο† = CreateAnnihilate.annihilate) (Ο†s : List 𝓕.CrAnFieldOp) :
      normalOrderSign (Ο†s ++ [Ο†]) = normalOrderSign Ο†s
      source
      theorem FieldSpecification.koszulSignInsert_annihilate_cons_create {𝓕 : FieldSpecification} (Ο†c Ο†a : 𝓕.CrAnFieldOp) (hΟ†c : 𝓕.crAnFieldOpToCreateAnnihilate Ο†c = CreateAnnihilate.create) (hΟ†a : 𝓕.crAnFieldOpToCreateAnnihilate Ο†a = CreateAnnihilate.annihilate) (Ο†s : List 𝓕.CrAnFieldOp) :
      Wick.koszulSignInsert 𝓕.crAnStatistics normalOrderRel Ο†a (Ο†c :: Ο†s) = (FieldStatistic.exchangeSign (𝓕.crAnStatistics Ο†c)) (𝓕.crAnStatistics Ο†a) * Wick.koszulSignInsert 𝓕.crAnStatistics normalOrderRel Ο†a Ο†s
      source
      theorem FieldSpecification.normalOrderSign_swap_create_annihilate_fst {𝓕 : FieldSpecification} (Ο†c Ο†a : 𝓕.CrAnFieldOp) (hΟ†c : 𝓕.crAnFieldOpToCreateAnnihilate Ο†c = CreateAnnihilate.create) (hΟ†a : 𝓕.crAnFieldOpToCreateAnnihilate Ο†a = CreateAnnihilate.annihilate) (Ο†s : List 𝓕.CrAnFieldOp) :
      normalOrderSign (Ο†c :: Ο†a :: Ο†s) = (FieldStatistic.exchangeSign (𝓕.crAnStatistics Ο†c)) (𝓕.crAnStatistics Ο†a) * normalOrderSign (Ο†a :: Ο†c :: Ο†s)
      source
      theorem FieldSpecification.koszulSignInsert_swap {𝓕 : FieldSpecification} (Ο† Ο†c Ο†a : 𝓕.CrAnFieldOp) (Ο†s Ο†s' : List 𝓕.CrAnFieldOp) :
      Wick.koszulSignInsert 𝓕.crAnStatistics normalOrderRel Ο† (Ο†s ++ Ο†a :: Ο†c :: Ο†s') = Wick.koszulSignInsert 𝓕.crAnStatistics normalOrderRel Ο† (Ο†s ++ Ο†c :: Ο†a :: Ο†s')
      source
      theorem FieldSpecification.normalOrderSign_swap_create_annihilate {𝓕 : FieldSpecification} (Ο†c Ο†a : 𝓕.CrAnFieldOp) (hΟ†c : 𝓕.crAnFieldOpToCreateAnnihilate Ο†c = CreateAnnihilate.create) (hΟ†a : 𝓕.crAnFieldOpToCreateAnnihilate Ο†a = CreateAnnihilate.annihilate) (Ο†s Ο†s' : List 𝓕.CrAnFieldOp) :
      normalOrderSign (Ο†s ++ Ο†c :: Ο†a :: Ο†s') = (FieldStatistic.exchangeSign (𝓕.crAnStatistics Ο†c)) (𝓕.crAnStatistics Ο†a) * normalOrderSign (Ο†s ++ Ο†a :: Ο†c :: Ο†s')
      source
      theorem FieldSpecification.normalOrderSign_swap_create_create_fst {𝓕 : FieldSpecification} (Ο†c Ο†c' : 𝓕.CrAnFieldOp) (hΟ†c : 𝓕.crAnFieldOpToCreateAnnihilate Ο†c = CreateAnnihilate.create) (hΟ†c' : 𝓕.crAnFieldOpToCreateAnnihilate Ο†c' = CreateAnnihilate.create) (Ο†s : List 𝓕.CrAnFieldOp) :
      normalOrderSign (Ο†c :: Ο†c' :: Ο†s) = normalOrderSign (Ο†c' :: Ο†c :: Ο†s)
      source
      theorem FieldSpecification.normalOrderSign_swap_create_create {𝓕 : FieldSpecification} (Ο†c Ο†c' : 𝓕.CrAnFieldOp) (hΟ†c : 𝓕.crAnFieldOpToCreateAnnihilate Ο†c = CreateAnnihilate.create) (hΟ†c' : 𝓕.crAnFieldOpToCreateAnnihilate Ο†c' = CreateAnnihilate.create) (Ο†s Ο†s' : List 𝓕.CrAnFieldOp) :
      normalOrderSign (Ο†s ++ Ο†c :: Ο†c' :: Ο†s') = normalOrderSign (Ο†s ++ Ο†c' :: Ο†c :: Ο†s')
      source
      theorem FieldSpecification.normalOrderSign_swap_annihilate_annihilate_fst {𝓕 : FieldSpecification} (Ο†a Ο†a' : 𝓕.CrAnFieldOp) (hΟ†a : 𝓕.crAnFieldOpToCreateAnnihilate Ο†a = CreateAnnihilate.annihilate) (hΟ†a' : 𝓕.crAnFieldOpToCreateAnnihilate Ο†a' = CreateAnnihilate.annihilate) (Ο†s : List 𝓕.CrAnFieldOp) :
      normalOrderSign (Ο†a :: Ο†a' :: Ο†s) = normalOrderSign (Ο†a' :: Ο†a :: Ο†s)
      source
      theorem FieldSpecification.normalOrderSign_swap_annihilate_annihilate {𝓕 : FieldSpecification} (Ο†a Ο†a' : 𝓕.CrAnFieldOp) (hΟ†a : 𝓕.crAnFieldOpToCreateAnnihilate Ο†a = CreateAnnihilate.annihilate) (hΟ†a' : 𝓕.crAnFieldOpToCreateAnnihilate Ο†a' = CreateAnnihilate.annihilate) (Ο†s Ο†s' : List 𝓕.CrAnFieldOp) :
      normalOrderSign (Ο†s ++ Ο†a :: Ο†a' :: Ο†s') = normalOrderSign (Ο†s ++ Ο†a' :: Ο†a :: Ο†s')

      ##Β Normal order of lists

      source
      def FieldSpecification.normalOrderList {𝓕 : FieldSpecification} (Ο†s : List 𝓕.CrAnFieldOp) :
      List 𝓕.CrAnFieldOp

      For a field specification 𝓕, and a list Ο†s of 𝓕.CrAnFieldOp, 𝓕.normalOrderList Ο†s is the list Ο†s normal-ordered using the insertion sort algorithm. It puts creation operators on the left and annihilation operators on the right. For example:

      𝓕.normalOrderList [Ο†1c, Ο†1a, Ο†2c, Ο†2a] = [Ο†1c, Ο†2c, Ο†1a, Ο†2a]

      Equations
      Instances For
        source
        @[simp]
        theorem FieldSpecification.normalOrderList_nil {𝓕 : FieldSpecification} :
        normalOrderList [] = []
        source
        @[simp]
        theorem FieldSpecification.normalOrderList_statistics {𝓕 : FieldSpecification} (Ο†s : List 𝓕.CrAnFieldOp) :
        FieldStatistic.ofList 𝓕.crAnStatistics (normalOrderList Ο†s) = FieldStatistic.ofList 𝓕.crAnStatistics Ο†s
        source
        theorem FieldSpecification.orderedInsert_create {𝓕 : FieldSpecification} (Ο† : 𝓕.CrAnFieldOp) (hΟ† : 𝓕.crAnFieldOpToCreateAnnihilate Ο† = CreateAnnihilate.create) (Ο†s : List 𝓕.CrAnFieldOp) :
        List.orderedInsert normalOrderRel Ο† Ο†s = Ο† :: Ο†s
        source
        theorem FieldSpecification.normalOrderList_cons_create {𝓕 : FieldSpecification} (Ο† : 𝓕.CrAnFieldOp) (hΟ† : 𝓕.crAnFieldOpToCreateAnnihilate Ο† = CreateAnnihilate.create) (Ο†s : List 𝓕.CrAnFieldOp) :
        normalOrderList (Ο† :: Ο†s) = Ο† :: normalOrderList Ο†s
        source
        theorem FieldSpecification.orderedInsert_append_annihilate {𝓕 : FieldSpecification} (Ο†' Ο† : 𝓕.CrAnFieldOp) (hΟ† : 𝓕.crAnFieldOpToCreateAnnihilate Ο† = CreateAnnihilate.annihilate) (Ο†s : List 𝓕.CrAnFieldOp) :
        List.orderedInsert normalOrderRel Ο†' (Ο†s ++ [Ο†]) = List.orderedInsert normalOrderRel Ο†' Ο†s ++ [Ο†]
        source
        theorem FieldSpecification.normalOrderList_append_annihilate {𝓕 : FieldSpecification} (Ο† : 𝓕.CrAnFieldOp) (hΟ† : 𝓕.crAnFieldOpToCreateAnnihilate Ο† = CreateAnnihilate.annihilate) (Ο†s : List 𝓕.CrAnFieldOp) :
        normalOrderList (Ο†s ++ [Ο†]) = normalOrderList Ο†s ++ [Ο†]
        source
        theorem FieldSpecification.normalOrder_swap_create_annihilate_fst {𝓕 : FieldSpecification} (Ο†c Ο†a : 𝓕.CrAnFieldOp) (hΟ†c : 𝓕.crAnFieldOpToCreateAnnihilate Ο†c = CreateAnnihilate.create) (hΟ†a : 𝓕.crAnFieldOpToCreateAnnihilate Ο†a = CreateAnnihilate.annihilate) (Ο†s : List 𝓕.CrAnFieldOp) :
        normalOrderList (Ο†c :: Ο†a :: Ο†s) = normalOrderList (Ο†a :: Ο†c :: Ο†s)
        source
        theorem FieldSpecification.normalOrderList_swap_create_annihilate {𝓕 : FieldSpecification} (Ο†c Ο†a : 𝓕.CrAnFieldOp) (hΟ†c : 𝓕.crAnFieldOpToCreateAnnihilate Ο†c = CreateAnnihilate.create) (hΟ†a : 𝓕.crAnFieldOpToCreateAnnihilate Ο†a = CreateAnnihilate.annihilate) (Ο†s Ο†s' : List 𝓕.CrAnFieldOp) :
        normalOrderList (Ο†s ++ Ο†c :: Ο†a :: Ο†s') = normalOrderList (Ο†s ++ Ο†a :: Ο†c :: Ο†s')
        source
        def FieldSpecification.normalOrderEquiv {𝓕 : FieldSpecification} {Ο†s : List 𝓕.CrAnFieldOp} :
        Fin Ο†s.length ≃ Fin (normalOrderList Ο†s).length

        For a list of creation and annihilation states, the equivalence between Fin Ο†s.length and Fin (normalOrderList Ο†s).length taking each position in Ο†s to it's corresponding position in the normal ordered list. This assumes that we are using the insertion sort method. For example:

        • For [Ο†1c, Ο†1a, Ο†2c, Ο†2a] this equivalence sends 0 ↦ 0, 1 ↦ 2, 2 ↦ 1, 3 ↦ 3.
        Equations
        Instances For
          source
          theorem FieldSpecification.sum_normalOrderList_length {𝓕 : FieldSpecification} {M : Type} [AddCommMonoid M] (Ο†s : List 𝓕.CrAnFieldOp) (f : Fin (normalOrderList Ο†s).length β†’ M) :
          βˆ‘ n : Fin (normalOrderList Ο†s).length, f n = βˆ‘ n : Fin Ο†s.length, f (normalOrderEquiv n)
          source
          @[simp]
          theorem FieldSpecification.normalOrderList_get_normalOrderEquiv {𝓕 : FieldSpecification} {Ο†s : List 𝓕.CrAnFieldOp} (n : Fin Ο†s.length) :
          (normalOrderList Ο†s)[↑(normalOrderEquiv n)] = Ο†s[↑n]
          source
          @[simp]
          theorem FieldSpecification.normalOrderList_eraseIdx_normalOrderEquiv {𝓕 : FieldSpecification} {Ο†s : List 𝓕.CrAnFieldOp} (n : Fin Ο†s.length) :
          (normalOrderList Ο†s).eraseIdx ↑(normalOrderEquiv n) = normalOrderList (Ο†s.eraseIdx ↑n)
          source
          theorem FieldSpecification.normalOrderSign_eraseIdx {𝓕 : FieldSpecification} (Ο†s : List 𝓕.CrAnFieldOp) (i : Fin Ο†s.length) :
          normalOrderSign (Ο†s.eraseIdx ↑i) = normalOrderSign Ο†s * (FieldStatistic.exchangeSign (𝓕.crAnStatistics (Ο†s.get i))) (FieldStatistic.ofList 𝓕.crAnStatistics (List.take (↑i) Ο†s)) * (FieldStatistic.exchangeSign (𝓕.crAnStatistics (Ο†s.get i))) (FieldStatistic.ofList 𝓕.crAnStatistics (List.take (↑(normalOrderEquiv i)) (normalOrderList Ο†s)))

          For a field specification 𝓕, a list Ο†s = φ₀…φₙ of 𝓕.CrAnFieldOp and an i < Ο†s.length, then normalOrderSign (Ο†β‚€β€¦Ο†α΅’β‚‹β‚Ο†α΅’β‚Šβ‚β€¦Ο†β‚™) is equal to the product of

          • normalOrderSign φ₀…φₙ,
          • 𝓒(Ο†α΅’, φ₀…φᡒ₋₁) i.e. the sign needed to remove Ο†α΅’ from φ₀…φₙ,
          • 𝓒(Ο†α΅’, _) where _ is the list of elements appearing before Ο†α΅’ after normal ordering, i.e. the sign needed to insert Ο†α΅’ back into the normal-ordered list at the correct place.
          source
          theorem FieldSpecification.orderedInsert_createFilter_append_annihilate {𝓕 : FieldSpecification} (Ο† : 𝓕.CrAnFieldOp) (hΟ† : 𝓕.crAnFieldOpToCreateAnnihilate Ο† = CreateAnnihilate.annihilate) (Ο†s Ο†s' : List 𝓕.CrAnFieldOp) :
          List.orderedInsert normalOrderRel Ο† (createFilter Ο†s ++ Ο†s') = createFilter Ο†s ++ List.orderedInsert normalOrderRel Ο† Ο†s'
          source
          theorem FieldSpecification.orderedInsert_annihilateFilter {𝓕 : FieldSpecification} (Ο† : 𝓕.CrAnFieldOp) (Ο†s : List 𝓕.CrAnFieldOp) :
          List.orderedInsert normalOrderRel Ο† (annihilateFilter Ο†s) = Ο† :: annihilateFilter Ο†s
          source
          theorem FieldSpecification.orderedInsert_createFilter_append_annihilateFilter_annihilate {𝓕 : FieldSpecification} (Ο† : 𝓕.CrAnFieldOp) (hΟ† : 𝓕.crAnFieldOpToCreateAnnihilate Ο† = CreateAnnihilate.annihilate) (Ο†s : List 𝓕.CrAnFieldOp) :
          List.orderedInsert normalOrderRel Ο† (createFilter Ο†s ++ annihilateFilter Ο†s) = createFilter Ο†s ++ Ο† :: annihilateFilter Ο†s
          source
          theorem FieldSpecification.normalOrderList_eq_createFilter_append_annihilateFilter {𝓕 : FieldSpecification} (Ο†s : List 𝓕.CrAnFieldOp) :
          normalOrderList Ο†s = createFilter Ο†s ++ annihilateFilter Ο†s