diff --git a/HepLean.lean b/HepLean.lean index 880efb65..94920199 100644 --- a/HepLean.lean +++ b/HepLean.lean @@ -124,13 +124,12 @@ import HepLean.Meta.TransverseTactics import HepLean.PerturbationTheory.Algebras.CrAnAlgebra.Basic import HepLean.PerturbationTheory.Algebras.CrAnAlgebra.NormalOrder import HepLean.PerturbationTheory.Algebras.CrAnAlgebra.SuperCommute +import HepLean.PerturbationTheory.Algebras.CrAnAlgebra.TimeOrder import HepLean.PerturbationTheory.Algebras.FieldOpAlgebra.Basic import HepLean.PerturbationTheory.Algebras.FieldOpAlgebra.NormalOrder import HepLean.PerturbationTheory.Algebras.ProtoOperatorAlgebra.Basic import HepLean.PerturbationTheory.Algebras.ProtoOperatorAlgebra.NormalOrder import HepLean.PerturbationTheory.Algebras.ProtoOperatorAlgebra.TimeContraction -import HepLean.PerturbationTheory.Algebras.StateAlgebra.Basic -import HepLean.PerturbationTheory.Algebras.StateAlgebra.TimeOrder import HepLean.PerturbationTheory.CreateAnnihilate import HepLean.PerturbationTheory.FeynmanDiagrams.Basic import HepLean.PerturbationTheory.FeynmanDiagrams.Instances.ComplexScalar diff --git a/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/Basic.lean b/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/Basic.lean index fb42671d..255d2886 100644 --- a/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/Basic.lean +++ b/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/Basic.lean @@ -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.Algebras.StateAlgebra.Basic +import HepLean.PerturbationTheory.FieldSpecification.CrAnStates import HepLean.PerturbationTheory.FieldSpecification.CrAnSection /-! @@ -43,8 +43,6 @@ abbrev CrAnAlgebra (𝓕 : FieldSpecification) : Type := FreeAlgebra β„‚ 𝓕.Cr namespace CrAnAlgebra -open StateAlgebra - /-- Maps a creation and annihlation state to the creation and annihlation free-algebra. -/ def ofCrAnState (Ο† : 𝓕.CrAnStates) : CrAnAlgebra 𝓕 := FreeAlgebra.ΞΉ β„‚ Ο† @@ -71,15 +69,6 @@ lemma ofCrAnList_singleton (Ο† : 𝓕.CrAnStates) : def ofState (Ο† : 𝓕.States) : CrAnAlgebra 𝓕 := βˆ‘ (i : 𝓕.statesToCrAnType Ο†), ofCrAnState βŸ¨Ο†, i⟩ -/-- The algebra map from the state free-algebra to the creation and annihlation free-algebra. -/ -def ofStateAlgebra : StateAlgebra 𝓕 →ₐ[β„‚] CrAnAlgebra 𝓕 := - FreeAlgebra.lift β„‚ ofState - -@[simp] -lemma ofStateAlgebra_ofState (Ο† : 𝓕.States) : - ofStateAlgebra (StateAlgebra.ofState Ο†) = ofState Ο† := by - simp [ofStateAlgebra, StateAlgebra.ofState] - /-- Maps a list of states to the creation and annihilation free-algebra by taking the product of their sums of creation and annihlation operators. Roughly `[Ο†1, Ο†2]` gets sent to `(Ο†1ᢜ+ Ο†1ᡃ) * (Ο†2ᢜ+ Ο†2ᡃ)` etc. -/ @@ -102,14 +91,6 @@ lemma ofStateList_append (Ο†s Ο†s' : List 𝓕.States) : dsimp only [ofStateList] rw [List.map_append, List.prod_append] -lemma ofStateAlgebra_ofList_eq_ofStateList : (Ο†s : List 𝓕.States) β†’ - ofStateAlgebra (ofList Ο†s) = ofStateList Ο†s - | [] => by simp [ofStateList] - | Ο† :: Ο†s => by - rw [ofStateList_cons, StateAlgebra.ofList_cons, map_mul, ofStateAlgebra_ofState, - mul_eq_mul_left_iff] - exact .inl (ofStateAlgebra_ofList_eq_ofStateList Ο†s) - lemma ofStateList_sum (Ο†s : List 𝓕.States) : ofStateList Ο†s = βˆ‘ (s : CrAnSection Ο†s), ofCrAnList s.1 := by induction Ο†s with @@ -132,8 +113,7 @@ lemma ofStateList_sum (Ο†s : List 𝓕.States) : /-- The algebra map taking an element of the free-state algbra to the part of it in the creation and annihlation free algebra spanned by creation operators. -/ -def crPart : 𝓕.StateAlgebra →ₐ[β„‚] 𝓕.CrAnAlgebra := - FreeAlgebra.lift β„‚ fun Ο† => +def crPart : 𝓕.States β†’ 𝓕.CrAnAlgebra := fun Ο† => match Ο† with | States.inAsymp Ο† => ofCrAnState ⟨States.inAsymp Ο†, ()⟩ | States.position Ο† => ofCrAnState ⟨States.position Ο†, CreateAnnihilate.create⟩ @@ -141,25 +121,24 @@ def crPart : 𝓕.StateAlgebra →ₐ[β„‚] 𝓕.CrAnAlgebra := @[simp] lemma crPart_negAsymp (Ο† : 𝓕.IncomingAsymptotic) : - crPart (StateAlgebra.ofState (States.inAsymp Ο†)) = ofCrAnState ⟨States.inAsymp Ο†, ()⟩ := by - simp [crPart, StateAlgebra.ofState] + crPart (States.inAsymp Ο†) = ofCrAnState ⟨States.inAsymp Ο†, ()⟩ := by + simp [crPart] @[simp] lemma crPart_position (Ο† : 𝓕.PositionStates) : - crPart (StateAlgebra.ofState (States.position Ο†)) = + crPart (States.position Ο†) = ofCrAnState ⟨States.position Ο†, CreateAnnihilate.create⟩ := by - simp [crPart, StateAlgebra.ofState] + simp [crPart] @[simp] lemma crPart_posAsymp (Ο† : 𝓕.OutgoingAsymptotic) : - crPart (StateAlgebra.ofState (States.outAsymp Ο†)) = 0 := by - simp [crPart, StateAlgebra.ofState] + crPart (States.outAsymp Ο†) = 0 := by + simp [crPart] /-- The algebra map taking an element of the free-state algbra to the part of it in the creation and annihilation free algebra spanned by annihilation operators. -/ -def anPart : 𝓕.StateAlgebra →ₐ[β„‚] 𝓕.CrAnAlgebra := - FreeAlgebra.lift β„‚ fun Ο† => +def anPart : 𝓕.States β†’ 𝓕.CrAnAlgebra := fun Ο† => match Ο† with | States.inAsymp _ => 0 | States.position Ο† => ofCrAnState ⟨States.position Ο†, CreateAnnihilate.annihilate⟩ @@ -167,22 +146,22 @@ def anPart : 𝓕.StateAlgebra →ₐ[β„‚] 𝓕.CrAnAlgebra := @[simp] lemma anPart_negAsymp (Ο† : 𝓕.IncomingAsymptotic) : - anPart (StateAlgebra.ofState (States.inAsymp Ο†)) = 0 := by - simp [anPart, StateAlgebra.ofState] + anPart (States.inAsymp Ο†) = 0 := by + simp [anPart] @[simp] lemma anPart_position (Ο† : 𝓕.PositionStates) : - anPart (StateAlgebra.ofState (States.position Ο†)) = + anPart (States.position Ο†) = ofCrAnState ⟨States.position Ο†, CreateAnnihilate.annihilate⟩ := by - simp [anPart, StateAlgebra.ofState] + simp [anPart] @[simp] lemma anPart_posAsymp (Ο† : 𝓕.OutgoingAsymptotic) : - anPart (StateAlgebra.ofState (States.outAsymp Ο†)) = ofCrAnState ⟨States.outAsymp Ο†, ()⟩ := by - simp [anPart, StateAlgebra.ofState] + anPart (States.outAsymp Ο†) = ofCrAnState ⟨States.outAsymp Ο†, ()⟩ := by + simp [anPart] lemma ofState_eq_crPart_add_anPart (Ο† : 𝓕.States) : - ofState Ο† = crPart (StateAlgebra.ofState Ο†) + anPart (StateAlgebra.ofState Ο†) := by + ofState Ο† = crPart Ο† + anPart Ο† := by rw [ofState] cases Ο† with | inAsymp Ο† => simp [statesToCrAnType] diff --git a/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/NormalOrder.lean b/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/NormalOrder.lean index 6d17345e..e6839f5c 100644 --- a/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/NormalOrder.lean +++ b/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/NormalOrder.lean @@ -93,27 +93,27 @@ lemma normalOrder_mul_annihilate (Ο† : 𝓕.CrAnStates) normalOrder_ofCrAnList_append_annihilate Ο† hΟ†] lemma normalOrder_crPart_mul (Ο† : 𝓕.States) (a : CrAnAlgebra 𝓕) : - 𝓝(crPart (StateAlgebra.ofState Ο†) * a) = - crPart (StateAlgebra.ofState Ο†) * 𝓝(a) := by + 𝓝(crPart Ο† * a) = + crPart Ο† * 𝓝(a) := by match Ο† with | .inAsymp Ο† => - rw [crPart, StateAlgebra.ofState, FreeAlgebra.lift_ΞΉ_apply] + rw [crPart] exact normalOrder_create_mul ⟨States.inAsymp Ο†, ()⟩ rfl a | .position Ο† => - rw [crPart, StateAlgebra.ofState, FreeAlgebra.lift_ΞΉ_apply] + rw [crPart] exact normalOrder_create_mul _ rfl _ | .outAsymp Ο† => simp lemma normalOrder_mul_anPart (Ο† : 𝓕.States) (a : CrAnAlgebra 𝓕) : - 𝓝(a * anPart (StateAlgebra.ofState Ο†)) = - 𝓝(a) * anPart (StateAlgebra.ofState Ο†) := by + 𝓝(a * anPart Ο†) = + 𝓝(a) * anPart Ο† := by match Ο† with | .inAsymp Ο† => simp | .position Ο† => - rw [anPart, StateAlgebra.ofState, FreeAlgebra.lift_ΞΉ_apply] + rw [anPart] exact normalOrder_mul_annihilate _ rfl _ | .outAsymp Ο† => - rw [anPart, StateAlgebra.ofState, FreeAlgebra.lift_ΞΉ_apply] + rw [anPart] refine normalOrder_mul_annihilate _ rfl _ /-! @@ -182,9 +182,9 @@ lemma normalOrder_superCommute_annihilate_create (Ο†c Ο†a : 𝓕.CrAnStates) exact Or.inr (normalOrder_superCommute_create_annihilate Ο†c Ο†a hΟ†c hΟ†a ..) lemma normalOrder_swap_crPart_anPart (Ο† Ο†' : 𝓕.States) (a b : CrAnAlgebra 𝓕) : - 𝓝(a * (crPart (StateAlgebra.ofState Ο†)) * (anPart (StateAlgebra.ofState Ο†')) * b) = + 𝓝(a * (crPart Ο†) * (anPart Ο†') * b) = 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› Ο†') β€’ - 𝓝(a * (anPart (StateAlgebra.ofState Ο†')) * (crPart (StateAlgebra.ofState Ο†)) * b) := by + 𝓝(a * (anPart Ο†') * (crPart Ο†) * b) := by match Ο†, Ο†' with | _, .inAsymp Ο†' => simp | .outAsymp Ο†, _ => simp @@ -218,14 +218,14 @@ Using the results from above. -/ lemma normalOrder_swap_anPart_crPart (Ο† Ο†' : 𝓕.States) (a b : CrAnAlgebra 𝓕) : - 𝓝(a * (anPart (StateAlgebra.ofState Ο†)) * (crPart (StateAlgebra.ofState Ο†')) * b) = - 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› Ο†') β€’ 𝓝(a * (crPart (StateAlgebra.ofState Ο†')) * - (anPart (StateAlgebra.ofState Ο†)) * b) := by + 𝓝(a * (anPart Ο†) * (crPart Ο†') * b) = + 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› Ο†') β€’ 𝓝(a * (crPart Ο†') * + (anPart Ο†) * b) := by simp [normalOrder_swap_crPart_anPart, smul_smul] lemma normalOrder_superCommute_crPart_anPart (Ο† Ο†' : 𝓕.States) (a b : CrAnAlgebra 𝓕) : 𝓝(a * superCommute - (crPart (StateAlgebra.ofState Ο†)) (anPart (StateAlgebra.ofState Ο†')) * b) = 0 := by + (crPart Ο†) (anPart Ο†') * b) = 0 := by match Ο†, Ο†' with | _, .inAsymp Ο†' => simp | .outAsymp Ο†', _ => simp @@ -244,7 +244,7 @@ lemma normalOrder_superCommute_crPart_anPart (Ο† Ο†' : 𝓕.States) (a b : CrAnA lemma normalOrder_superCommute_anPart_crPart (Ο† Ο†' : 𝓕.States) (a b : CrAnAlgebra 𝓕) : 𝓝(a * superCommute - (anPart (StateAlgebra.ofState Ο†)) (crPart (StateAlgebra.ofState Ο†')) * b) = 0 := by + (anPart Ο†) (crPart Ο†') * b) = 0 := by match Ο†, Ο†' with | .inAsymp Ο†', _ => simp | _, .outAsymp Ο†' => simp @@ -269,49 +269,49 @@ lemma normalOrder_superCommute_anPart_crPart (Ο† Ο†' : 𝓕.States) (a b : CrAnA @[simp] lemma normalOrder_crPart_mul_crPart (Ο† Ο†' : 𝓕.States) : - 𝓝(crPart (StateAlgebra.ofState Ο†) * crPart (StateAlgebra.ofState Ο†')) = - crPart (StateAlgebra.ofState Ο†) * crPart (StateAlgebra.ofState Ο†') := by + 𝓝(crPart Ο† * crPart Ο†') = + crPart Ο† * crPart Ο†' := by rw [normalOrder_crPart_mul] - conv_lhs => rw [← mul_one (crPart (StateAlgebra.ofState Ο†'))] + conv_lhs => rw [← mul_one (crPart Ο†')] rw [normalOrder_crPart_mul, normalOrder_one] simp @[simp] lemma normalOrder_anPart_mul_anPart (Ο† Ο†' : 𝓕.States) : - 𝓝(anPart (StateAlgebra.ofState Ο†) * anPart (StateAlgebra.ofState Ο†')) = - anPart (StateAlgebra.ofState Ο†) * anPart (StateAlgebra.ofState Ο†') := by + 𝓝(anPart Ο† * anPart Ο†') = + anPart Ο† * anPart Ο†' := by rw [normalOrder_mul_anPart] - conv_lhs => rw [← one_mul (anPart (StateAlgebra.ofState Ο†))] + conv_lhs => rw [← one_mul (anPart Ο†)] rw [normalOrder_mul_anPart, normalOrder_one] simp @[simp] lemma normalOrder_crPart_mul_anPart (Ο† Ο†' : 𝓕.States) : - 𝓝(crPart (StateAlgebra.ofState Ο†) * anPart (StateAlgebra.ofState Ο†')) = - crPart (StateAlgebra.ofState Ο†) * anPart (StateAlgebra.ofState Ο†') := by + 𝓝(crPart Ο† * anPart Ο†') = + crPart Ο† * anPart Ο†' := by rw [normalOrder_crPart_mul] - conv_lhs => rw [← one_mul (anPart (StateAlgebra.ofState Ο†'))] + conv_lhs => rw [← one_mul (anPart Ο†')] rw [normalOrder_mul_anPart, normalOrder_one] simp @[simp] lemma normalOrder_anPart_mul_crPart (Ο† Ο†' : 𝓕.States) : - 𝓝(anPart (StateAlgebra.ofState Ο†) * crPart (StateAlgebra.ofState Ο†')) = + 𝓝(anPart Ο† * crPart Ο†') = 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› Ο†') β€’ - (crPart (StateAlgebra.ofState Ο†') * anPart (StateAlgebra.ofState Ο†)) := by - conv_lhs => rw [← one_mul (anPart (StateAlgebra.ofState Ο†) * crPart (StateAlgebra.ofState Ο†'))] - conv_lhs => rw [← mul_one (1 * (anPart (StateAlgebra.ofState Ο†) * - crPart (StateAlgebra.ofState Ο†')))] + (crPart Ο†' * anPart Ο†) := by + conv_lhs => rw [← one_mul (anPart Ο† * crPart Ο†')] + conv_lhs => rw [← mul_one (1 * (anPart Ο† * + crPart Ο†'))] rw [← mul_assoc, normalOrder_swap_anPart_crPart] simp lemma normalOrder_ofState_mul_ofState (Ο† Ο†' : 𝓕.States) : 𝓝(ofState Ο† * ofState Ο†') = - crPart (StateAlgebra.ofState Ο†) * crPart (StateAlgebra.ofState Ο†') + + crPart Ο† * crPart Ο†' + 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› Ο†') β€’ - (crPart (StateAlgebra.ofState Ο†') * anPart (StateAlgebra.ofState Ο†)) + - crPart (StateAlgebra.ofState Ο†) * anPart (StateAlgebra.ofState Ο†') + - anPart (StateAlgebra.ofState Ο†) * anPart (StateAlgebra.ofState Ο†') := by + (crPart Ο†' * anPart Ο†) + + crPart Ο† * anPart Ο†' + + anPart Ο† * anPart Ο†' := by rw [ofState_eq_crPart_add_anPart, ofState_eq_crPart_add_anPart, mul_add, add_mul, add_mul] simp only [map_add, normalOrder_crPart_mul_crPart, normalOrder_anPart_mul_crPart, instCommGroup.eq_1, normalOrder_crPart_mul_anPart, normalOrder_anPart_mul_anPart] @@ -497,9 +497,9 @@ lemma ofCrAnState_mul_normalOrder_ofStateList_eq_superCommute (Ο† : 𝓕.CrAnSta lemma anPart_mul_normalOrder_ofStateList_eq_superCommute (Ο† : 𝓕.States) (Ο†s' : List 𝓕.States) : - anPart (StateAlgebra.ofState Ο†) * 𝓝(ofStateList Ο†s') = - 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› Ο†s') β€’ 𝓝(ofStateList Ο†s' * anPart (StateAlgebra.ofState Ο†)) - + [anPart (StateAlgebra.ofState Ο†), 𝓝(ofStateList Ο†s')]β‚›ca := by + anPart Ο† * 𝓝(ofStateList Ο†s') = + 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› Ο†s') β€’ 𝓝(ofStateList Ο†s' * anPart Ο†) + + [anPart Ο†, 𝓝(ofStateList Ο†s')]β‚›ca := by rw [normalOrder_mul_anPart] match Ο† with | .inAsymp Ο† => simp diff --git a/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/SuperCommute.lean b/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/SuperCommute.lean index fb87733e..292dc309 100644 --- a/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/SuperCommute.lean +++ b/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/SuperCommute.lean @@ -14,8 +14,6 @@ variable {𝓕 : FieldSpecification} namespace CrAnAlgebra -open StateAlgebra - /-! ## The super commutor on the CrAnAlgebra. @@ -97,9 +95,9 @@ lemma superCommute_ofStateList_ofState (Ο†s : List 𝓕.States) (Ο† : 𝓕.State simp lemma superCommute_anPart_crPart (Ο† Ο†' : 𝓕.States) : - [anPart (StateAlgebra.ofState Ο†), crPart (StateAlgebra.ofState Ο†')]β‚›ca = - anPart (StateAlgebra.ofState Ο†) * crPart (StateAlgebra.ofState Ο†') - - 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› Ο†') β€’ crPart (StateAlgebra.ofState Ο†') * anPart (StateAlgebra.ofState Ο†) := by + [anPart Ο†, crPart Ο†']β‚›ca = + anPart Ο† * crPart Ο†' - + 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› Ο†') β€’ crPart Ο†' * anPart Ο† := by match Ο†, Ο†' with | States.inAsymp Ο†, _ => simp @@ -126,10 +124,10 @@ lemma superCommute_anPart_crPart (Ο† Ο†' : 𝓕.States) : simp [crAnStatistics, ← ofCrAnList_append] lemma superCommute_crPart_anPart (Ο† Ο†' : 𝓕.States) : - [crPart (StateAlgebra.ofState Ο†), anPart (StateAlgebra.ofState Ο†')]β‚›ca = - crPart (StateAlgebra.ofState Ο†) * anPart (StateAlgebra.ofState Ο†') - + [crPart Ο†, anPart Ο†']β‚›ca = + crPart Ο† * anPart Ο†' - 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› Ο†') β€’ - anPart (StateAlgebra.ofState Ο†') * crPart (StateAlgebra.ofState Ο†) := by + anPart Ο†' * crPart Ο† := by match Ο†, Ο†' with | States.outAsymp Ο†, _ => simp only [crPart_posAsymp, map_zero, LinearMap.zero_apply, zero_mul, instCommGroup.eq_1, @@ -155,10 +153,10 @@ lemma superCommute_crPart_anPart (Ο† Ο†' : 𝓕.States) : simp [crAnStatistics, ← ofCrAnList_append] lemma superCommute_crPart_crPart (Ο† Ο†' : 𝓕.States) : - [crPart (StateAlgebra.ofState Ο†), crPart (StateAlgebra.ofState Ο†')]β‚›ca = - crPart (StateAlgebra.ofState Ο†) * crPart (StateAlgebra.ofState Ο†') - + [crPart Ο†, crPart Ο†']β‚›ca = + crPart Ο† * crPart Ο†' - 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› Ο†') β€’ - crPart (StateAlgebra.ofState Ο†') * crPart (StateAlgebra.ofState Ο†) := by + crPart Ο†' * crPart Ο† := by match Ο†, Ο†' with | States.outAsymp Ο†, _ => simp only [crPart_posAsymp, map_zero, LinearMap.zero_apply, zero_mul, instCommGroup.eq_1, @@ -183,10 +181,10 @@ lemma superCommute_crPart_crPart (Ο† Ο†' : 𝓕.States) : simp [crAnStatistics, ← ofCrAnList_append] lemma superCommute_anPart_anPart (Ο† Ο†' : 𝓕.States) : - [anPart (StateAlgebra.ofState Ο†), anPart (StateAlgebra.ofState Ο†')]β‚›ca = - anPart (StateAlgebra.ofState Ο†) * anPart (StateAlgebra.ofState Ο†') - + [anPart Ο†, anPart Ο†']β‚›ca = + anPart Ο† * anPart Ο†' - 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› Ο†') β€’ - anPart (StateAlgebra.ofState Ο†') * anPart (StateAlgebra.ofState Ο†) := by + anPart Ο†' * anPart Ο† := by match Ο†, Ο†' with | States.inAsymp Ο†, _ => simp @@ -210,9 +208,9 @@ lemma superCommute_anPart_anPart (Ο† Ο†' : 𝓕.States) : simp [crAnStatistics, ← ofCrAnList_append] lemma superCommute_crPart_ofStateList (Ο† : 𝓕.States) (Ο†s : List 𝓕.States) : - [crPart (StateAlgebra.ofState Ο†), ofStateList Ο†s]β‚›ca = - crPart (StateAlgebra.ofState Ο†) * ofStateList Ο†s - 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› Ο†s) β€’ ofStateList Ο†s * - crPart (StateAlgebra.ofState Ο†) := by + [crPart Ο†, ofStateList Ο†s]β‚›ca = + crPart Ο† * ofStateList Ο†s - 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› Ο†s) β€’ ofStateList Ο†s * + crPart Ο† := by match Ο† with | States.inAsymp Ο† => simp only [crPart_negAsymp, instCommGroup.eq_1, Algebra.smul_mul_assoc] @@ -226,9 +224,9 @@ lemma superCommute_crPart_ofStateList (Ο† : 𝓕.States) (Ο†s : List 𝓕.States simp lemma superCommute_anPart_ofStateList (Ο† : 𝓕.States) (Ο†s : List 𝓕.States) : - [anPart (StateAlgebra.ofState Ο†), ofStateList Ο†s]β‚›ca = - anPart (StateAlgebra.ofState Ο†) * ofStateList Ο†s - 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› Ο†s) β€’ - ofStateList Ο†s * anPart (StateAlgebra.ofState Ο†) := by + [anPart Ο†, ofStateList Ο†s]β‚›ca = + anPart Ο† * ofStateList Ο†s - 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› Ο†s) β€’ + ofStateList Ο†s * anPart Ο† := by match Ο† with | States.inAsymp Ο† => simp @@ -242,16 +240,16 @@ lemma superCommute_anPart_ofStateList (Ο† : 𝓕.States) (Ο†s : List 𝓕.States simp [crAnStatistics] lemma superCommute_crPart_ofState (Ο† Ο†' : 𝓕.States) : - [crPart (StateAlgebra.ofState Ο†), ofState Ο†']β‚›ca = - crPart (StateAlgebra.ofState Ο†) * ofState Ο†' - - 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› Ο†') β€’ ofState Ο†' * crPart (StateAlgebra.ofState Ο†) := by + [crPart Ο†, ofState Ο†']β‚›ca = + crPart Ο† * ofState Ο†' - + 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› Ο†') β€’ ofState Ο†' * crPart Ο† := by rw [← ofStateList_singleton, superCommute_crPart_ofStateList] simp lemma superCommute_anPart_ofState (Ο† Ο†' : 𝓕.States) : - [anPart (StateAlgebra.ofState Ο†), ofState Ο†']β‚›ca = - anPart (StateAlgebra.ofState Ο†) * ofState Ο†' - - 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› Ο†') β€’ ofState Ο†' * anPart (StateAlgebra.ofState Ο†) := by + [anPart Ο†, ofState Ο†']β‚›ca = + anPart Ο† * ofState Ο†' - + 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› Ο†') β€’ ofState Ο†' * anPart Ο† := by rw [← ofStateList_singleton, superCommute_anPart_ofStateList] simp @@ -294,31 +292,30 @@ lemma ofStateList_mul_ofState_eq_superCommute (Ο†s : List 𝓕.States) (Ο† : simp lemma crPart_mul_anPart_eq_superCommute (Ο† Ο†' : 𝓕.States) : - crPart (StateAlgebra.ofState Ο†) * anPart (StateAlgebra.ofState Ο†') = - 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› Ο†') β€’ anPart (StateAlgebra.ofState Ο†') * crPart (StateAlgebra.ofState Ο†) + - [crPart (StateAlgebra.ofState Ο†), anPart (StateAlgebra.ofState Ο†')]β‚›ca := by + crPart Ο† * anPart Ο†' = + 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› Ο†') β€’ anPart Ο†' * crPart Ο† + + [crPart Ο†, anPart Ο†']β‚›ca := by rw [superCommute_crPart_anPart] simp lemma anPart_mul_crPart_eq_superCommute (Ο† Ο†' : 𝓕.States) : - anPart (StateAlgebra.ofState Ο†) * crPart (StateAlgebra.ofState Ο†') = + anPart Ο† * crPart Ο†' = 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› Ο†') β€’ - crPart (StateAlgebra.ofState Ο†') * anPart (StateAlgebra.ofState Ο†) + - [anPart (StateAlgebra.ofState Ο†), crPart (StateAlgebra.ofState Ο†')]β‚›ca := by + crPart Ο†' * anPart Ο† + + [anPart Ο†, crPart Ο†']β‚›ca := by rw [superCommute_anPart_crPart] simp lemma crPart_mul_crPart_eq_superCommute (Ο† Ο†' : 𝓕.States) : - crPart (StateAlgebra.ofState Ο†) * crPart (StateAlgebra.ofState Ο†') = - 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› Ο†') β€’ crPart (StateAlgebra.ofState Ο†') * crPart (StateAlgebra.ofState Ο†) + - [crPart (StateAlgebra.ofState Ο†), crPart (StateAlgebra.ofState Ο†')]β‚›ca := by + crPart Ο† * crPart Ο†' = + 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› Ο†') β€’ crPart Ο†' * crPart Ο† + + [crPart Ο†, crPart Ο†']β‚›ca := by rw [superCommute_crPart_crPart] simp lemma anPart_mul_anPart_eq_superCommute (Ο† Ο†' : 𝓕.States) : - anPart (StateAlgebra.ofState Ο†) * anPart (StateAlgebra.ofState Ο†') = - 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› Ο†') β€’ anPart (StateAlgebra.ofState Ο†') * anPart (StateAlgebra.ofState Ο†) + - [anPart (StateAlgebra.ofState Ο†), anPart (StateAlgebra.ofState Ο†')]β‚›ca := by + anPart Ο† * anPart Ο†' = 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› Ο†') β€’ anPart Ο†' * anPart Ο† + + [anPart Ο†, anPart Ο†']β‚›ca := by rw [superCommute_anPart_anPart] simp diff --git a/HepLean/PerturbationTheory/Algebras/StateAlgebra/TimeOrder.lean b/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/TimeOrder.lean similarity index 62% rename from HepLean/PerturbationTheory/Algebras/StateAlgebra/TimeOrder.lean rename to HepLean/PerturbationTheory/Algebras/CrAnAlgebra/TimeOrder.lean index e56e27ef..fbd28ce0 100644 --- a/HepLean/PerturbationTheory/Algebras/StateAlgebra/TimeOrder.lean +++ b/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/TimeOrder.lean @@ -4,61 +4,80 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ import HepLean.PerturbationTheory.FieldSpecification.TimeOrder +import HepLean.PerturbationTheory.Algebras.CrAnAlgebra.SuperCommute import HepLean.PerturbationTheory.Koszul.KoszulSign /-! -# Time ordering on the state algebra +# Time Ordering in the CrAnAlgebra -/ namespace FieldSpecification variable {𝓕 : FieldSpecification} -noncomputable section +open FieldStatistic -namespace StateAlgebra +namespace CrAnAlgebra -open FieldStatistic +noncomputable section open HepLean.List +/-! + +## Time order + +-/ + +/-- Time ordering for the `CrAnAlgebra`. -/ +def timeOrder : CrAnAlgebra 𝓕 β†’β‚—[β„‚] CrAnAlgebra 𝓕 := + Basis.constr ofCrAnListBasis β„‚ fun Ο†s => + crAnTimeOrderSign Ο†s β€’ ofCrAnList (crAnTimeOrderList Ο†s) + -/-- The linear map on the free state algebra defined as the map taking - a list of states to the time-ordered list of states multiplied by - the sign corresponding to the number of fermionic-fermionic - exchanges done in ordering. -/ -def timeOrder : StateAlgebra 𝓕 β†’β‚—[β„‚] StateAlgebra 𝓕 := - Basis.constr ofListBasis β„‚ fun Ο†s => - timeOrderSign Ο†s β€’ ofList (timeOrderList Ο†s) +@[inherit_doc timeOrder] +scoped[FieldSpecification.CrAnAlgebra] notation "𝓣ᢠ(" a ")" => timeOrder a -lemma timeOrder_ofList (Ο†s : List 𝓕.States) : - timeOrder (ofList Ο†s) = timeOrderSign Ο†s β€’ ofList (timeOrderList Ο†s) := by +lemma timeOrder_ofCrAnList (Ο†s : List 𝓕.CrAnStates) : + 𝓣ᢠ(ofCrAnList Ο†s) = crAnTimeOrderSign Ο†s β€’ ofCrAnList (crAnTimeOrderList Ο†s) := by rw [← ofListBasis_eq_ofList] simp only [timeOrder, Basis.constr_basis] -lemma timeOrder_ofList_nil : timeOrder (𝓕 := 𝓕) (ofList []) = 1 := by - rw [timeOrder_ofList] +lemma timeOrder_ofStateList (Ο†s : List 𝓕.States) : + 𝓣ᢠ(ofStateList Ο†s) = timeOrderSign Ο†s β€’ ofStateList (timeOrderList Ο†s) := by + conv_lhs => + rw [ofStateList_sum, map_sum] + enter [2, x] + rw [timeOrder_ofCrAnList] + simp only [crAnTimeOrderSign_crAnSection] + rw [← Finset.smul_sum] + congr + rw [ofStateList_sum, sum_crAnSections_timeOrder] + rfl + + +lemma timeOrder_ofStateList_nil : timeOrder (𝓕 := 𝓕) (ofStateList []) = 1 := by + rw [timeOrder_ofStateList] simp [timeOrderSign, Wick.koszulSign, timeOrderList] @[simp] -lemma timeOrder_ofList_singleton (Ο† : 𝓕.States) : timeOrder (ofList [Ο†]) = ofList [Ο†] := by - simp [timeOrder_ofList, timeOrderSign, timeOrderList] +lemma timeOrder_ofStateList_singleton (Ο† : 𝓕.States) : 𝓣ᢠ(ofStateList [Ο†]) = ofStateList [Ο†] := by + simp [timeOrder_ofStateList, timeOrderSign, timeOrderList] lemma timeOrder_ofState_ofState_ordered {Ο† ψ : 𝓕.States} (h : timeOrderRel Ο† ψ) : - timeOrder (ofState Ο† * ofState ψ) = ofState Ο† * ofState ψ := by - rw [← ofList_singleton, ← ofList_singleton, ← ofList_append, timeOrder_ofList] + 𝓣ᢠ(ofState Ο† * ofState ψ) = ofState Ο† * ofState ψ := by + rw [← ofStateList_singleton, ← ofStateList_singleton, ← ofStateList_append, timeOrder_ofStateList] simp only [List.singleton_append] rw [timeOrderSign_pair_ordered h, timeOrderList_pair_ordered h] simp -lemma timeOrder_ofState_ofState_not_ordered {Ο† ψ : 𝓕.States} (h :Β¬ timeOrderRel Ο† ψ) : - timeOrder (ofState Ο† * ofState ψ) = - 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› ψ) β€’ ofState ψ * ofState Ο† := by - rw [← ofList_singleton, ← ofList_singleton, ← ofList_append, timeOrder_ofList] +lemma timeOrder_ofState_ofState_not_ordered {Ο† ψ : 𝓕.States} (h : Β¬ timeOrderRel Ο† ψ) : + 𝓣ᢠ(ofState Ο† * ofState ψ) = 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› ψ) β€’ ofState ψ * ofState Ο† := by + rw [← ofStateList_singleton, ← ofStateList_singleton, + ← ofStateList_append, timeOrder_ofStateList] simp only [List.singleton_append, instCommGroup.eq_1, Algebra.smul_mul_assoc] rw [timeOrderSign_pair_not_ordered h, timeOrderList_pair_not_ordered h] - simp [← ofList_append] + simp [← ofStateList_append] -lemma timeOrder_ofState_ofState_not_ordered_eq_timeOrder {Ο† ψ : 𝓕.States} (h :Β¬ timeOrderRel Ο† ψ) : - timeOrder (ofState Ο† * ofState ψ) = - 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› ψ) β€’ timeOrder (ofState ψ * ofState Ο†) := by +lemma timeOrder_ofState_ofState_not_ordered_eq_timeOrder {Ο† ψ : 𝓕.States} (h : Β¬ timeOrderRel Ο† ψ) : + 𝓣ᢠ(ofState Ο† * ofState ψ) = 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› ψ) β€’ 𝓣ᢠ(ofState ψ * ofState Ο†) := by rw [timeOrder_ofState_ofState_not_ordered h] rw [timeOrder_ofState_ofState_ordered] simp only [instCommGroup.eq_1, Algebra.smul_mul_assoc] @@ -69,11 +88,11 @@ lemma timeOrder_ofState_ofState_not_ordered_eq_timeOrder {Ο† ψ : 𝓕.States} ( where `Ο†α΅’` is the state which has maximum time and `s` is the exchange sign of `Ο†α΅’` and `φ₀φ₁…φᡒ₋₁`. -/ lemma timeOrder_eq_maxTimeField_mul (Ο† : 𝓕.States) (Ο†s : List 𝓕.States) : - timeOrder (ofList (Ο† :: Ο†s)) = + 𝓣ᢠ(ofStateList (Ο† :: Ο†s)) = 𝓒(𝓕 |>β‚› maxTimeField Ο† Ο†s, 𝓕 |>β‚› (Ο† :: Ο†s).take (maxTimeFieldPos Ο† Ο†s)) β€’ - ofState (maxTimeField Ο† Ο†s) * timeOrder (ofList (eraseMaxTimeField Ο† Ο†s)) := by - rw [timeOrder_ofList, timeOrderList_eq_maxTimeField_timeOrderList] - rw [ofList_cons, timeOrder_ofList] + ofState (maxTimeField Ο† Ο†s) * 𝓣ᢠ(ofStateList (eraseMaxTimeField Ο† Ο†s)) := by + rw [timeOrder_ofStateList, timeOrderList_eq_maxTimeField_timeOrderList] + rw [ofStateList_cons, timeOrder_ofStateList] simp only [instCommGroup.eq_1, Algebra.mul_smul_comm, Algebra.smul_mul_assoc, smul_smul] congr rw [timerOrderSign_of_eraseMaxTimeField, mul_assoc] @@ -84,10 +103,10 @@ lemma timeOrder_eq_maxTimeField_mul (Ο† : 𝓕.States) (Ο†s : List 𝓕.States) which has maximum time and `s` is the exchange sign of `Ο†α΅’` and `φ₀φ₁…φᡒ₋₁`. Here `s` is written using finite sets. -/ lemma timeOrder_eq_maxTimeField_mul_finset (Ο† : 𝓕.States) (Ο†s : List 𝓕.States) : - timeOrder (ofList (Ο† :: Ο†s)) = 𝓒(𝓕 |>β‚› maxTimeField Ο† Ο†s, 𝓕 |>β‚› ⟨(eraseMaxTimeField Ο† Ο†s).get, + 𝓣ᢠ(ofStateList (Ο† :: Ο†s)) = 𝓒(𝓕 |>β‚› maxTimeField Ο† Ο†s, 𝓕 |>β‚› ⟨(eraseMaxTimeField Ο† Ο†s).get, (Finset.filter (fun x => (maxTimeFieldPosFin Ο† Ο†s).succAbove x < maxTimeFieldPosFin Ο† Ο†s) Finset.univ)⟩) β€’ - StateAlgebra.ofState (maxTimeField Ο† Ο†s) * timeOrder (ofList (eraseMaxTimeField Ο† Ο†s)) := by + ofState (maxTimeField Ο† Ο†s) * 𝓣ᢠ(ofStateList (eraseMaxTimeField Ο† Ο†s)) := by rw [timeOrder_eq_maxTimeField_mul] congr 3 apply FieldStatistic.ofList_perm @@ -130,6 +149,18 @@ lemma timeOrder_eq_maxTimeField_mul_finset (Ο† : 𝓕.States) (Ο†s : List 𝓕.S (Finset.filter (fun x => (maxTimeFieldPosFin Ο† Ο†s).succAbove x < maxTimeFieldPosFin Ο† Ο†s) Finset.univ) -end StateAlgebra + +/-! + +## Norm-time order + +-/ +/-- The normal-time ordering on `CrAnAlgebra`. -/ +def normTimeOrder : CrAnAlgebra 𝓕 β†’β‚—[β„‚] CrAnAlgebra 𝓕 := + Basis.constr ofCrAnListBasis β„‚ fun Ο†s => + normTimeOrderSign Ο†s β€’ ofCrAnList (normTimeOrderList Ο†s) end + +end CrAnAlgebra + end FieldSpecification diff --git a/HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/Basic.lean b/HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/Basic.lean index d93827b3..033436f6 100644 --- a/HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/Basic.lean +++ b/HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/Basic.lean @@ -15,7 +15,6 @@ import Mathlib.Algebra.RingQuot namespace FieldSpecification open CrAnAlgebra -open StateAlgebra open ProtoOperatorAlgebra open HepLean.List open WickContraction @@ -43,6 +42,7 @@ abbrev FieldOpAlgebra : Type := (TwoSidedIdeal.span 𝓕.fieldOpIdealSet).ringCo namespace FieldOpAlgebra variable {𝓕 : FieldSpecification} +/-- The instance of a setoid on `CrAnAlgebra` from the ideal `TwoSidedIdeal`. -/ instance : Setoid (CrAnAlgebra 𝓕) := (TwoSidedIdeal.span 𝓕.fieldOpIdealSet).ringCon.toSetoid lemma equiv_iff_sub_mem_ideal (x y : CrAnAlgebra 𝓕) : @@ -76,7 +76,7 @@ lemma ΞΉ_of_mem_fieldOpIdealSet (x : CrAnAlgebra 𝓕) (hx : x ∈ 𝓕.fieldOpI simpa using hx lemma ΞΉ_superCommute_ofCrAnState_ofCrAnState_mem_center (Ο† ψ : 𝓕.CrAnStates) : - ΞΉ [ofCrAnState Ο†, ofCrAnState ψ]β‚›ca ∈ Subalgebra.center β„‚ (FieldOpAlgebra 𝓕) := by + ΞΉ [ofCrAnState Ο†, ofCrAnState ψ]β‚›ca ∈ Subalgebra.center β„‚ 𝓕.FieldOpAlgebra := by rw [Subalgebra.mem_center_iff] intro b obtain ⟨b, rfl⟩ := ΞΉ_surjective b diff --git a/HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/NormalOrder.lean b/HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/NormalOrder.lean index 805928c0..7bb2b32d 100644 --- a/HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/NormalOrder.lean +++ b/HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/NormalOrder.lean @@ -12,7 +12,6 @@ import HepLean.PerturbationTheory.Algebras.FieldOpAlgebra.Basic namespace FieldSpecification open CrAnAlgebra -open StateAlgebra open ProtoOperatorAlgebra open HepLean.List open WickContraction diff --git a/HepLean/PerturbationTheory/Algebras/ProtoOperatorAlgebra/Basic.lean b/HepLean/PerturbationTheory/Algebras/ProtoOperatorAlgebra/Basic.lean index 0bcd0675..23a49b89 100644 --- a/HepLean/PerturbationTheory/Algebras/ProtoOperatorAlgebra/Basic.lean +++ b/HepLean/PerturbationTheory/Algebras/ProtoOperatorAlgebra/Basic.lean @@ -60,7 +60,7 @@ lemma crAnF_superCommute_ofCrAnState_ofState_mem_center (Ο† : 𝓕.CrAnStates) ( exact π“ž.superCommute_crAn_center Ο† ⟨ψ, x⟩ lemma crAnF_superCommute_anPart_ofState_mem_center (Ο† ψ : 𝓕.States) : - π“ž.crAnF [anPart (StateAlgebra.ofState Ο†), ofState ψ]β‚›ca ∈ Subalgebra.center β„‚ π“ž.A := by + π“ž.crAnF [anPart Ο†, ofState ψ]β‚›ca ∈ Subalgebra.center β„‚ π“ž.A := by match Ο† with | States.inAsymp _ => simp only [anPart_negAsymp, map_zero, LinearMap.zero_apply] @@ -83,7 +83,7 @@ lemma crAnF_superCommute_ofCrAnState_ofState_diff_grade_zero (Ο† : 𝓕.CrAnStat lemma crAnF_superCommute_anPart_ofState_diff_grade_zero (Ο† ψ : 𝓕.States) (h : (𝓕 |>β‚› Ο†) β‰  (𝓕 |>β‚› ψ)) : - π“ž.crAnF [anPart (StateAlgebra.ofState Ο†), ofState ψ]β‚›ca = 0 := by + π“ž.crAnF [anPart Ο†, ofState ψ]β‚›ca = 0 := by match Ο† with | States.inAsymp _ => simp @@ -105,7 +105,7 @@ lemma crAnF_superCommute_ofState_ofState_mem_center (Ο† ψ : 𝓕.States) : exact crAnF_superCommute_ofCrAnState_ofState_mem_center π“ž βŸ¨Ο†, x⟩ ψ lemma crAnF_superCommute_anPart_anPart (Ο† ψ : 𝓕.States) : - π“ž.crAnF [anPart (StateAlgebra.ofState Ο†), anPart (StateAlgebra.ofState ψ)]β‚›ca = 0 := by + π“ž.crAnF [anPart Ο†, anPart ψ]β‚›ca = 0 := by match Ο†, ψ with | _, States.inAsymp _ => simp @@ -133,7 +133,7 @@ lemma crAnF_superCommute_anPart_anPart (Ο† ψ : 𝓕.States) : rfl lemma crAnF_superCommute_crPart_crPart (Ο† ψ : 𝓕.States) : - π“ž.crAnF [crPart (StateAlgebra.ofState Ο†), crPart (StateAlgebra.ofState ψ)]β‚›ca = 0 := by + π“ž.crAnF [crPart Ο†, crPart ψ]β‚›ca = 0 := by match Ο†, ψ with | _, States.outAsymp _ => simp diff --git a/HepLean/PerturbationTheory/Algebras/ProtoOperatorAlgebra/NormalOrder.lean b/HepLean/PerturbationTheory/Algebras/ProtoOperatorAlgebra/NormalOrder.lean index eda33ddb..88ff755f 100644 --- a/HepLean/PerturbationTheory/Algebras/ProtoOperatorAlgebra/NormalOrder.lean +++ b/HepLean/PerturbationTheory/Algebras/ProtoOperatorAlgebra/NormalOrder.lean @@ -213,9 +213,9 @@ lemma crAnF_normalOrder_ofCrAnState_ofStatesList_swap (Ο† : 𝓕.CrAnStates) lemma crAnF_normalOrder_anPart_ofStatesList_swap (Ο† : 𝓕.States) (Ο†' : List 𝓕.States) : - π“ž.crAnF (normalOrder (anPart (StateAlgebra.ofState Ο†) * ofStateList Ο†')) = + π“ž.crAnF (normalOrder (anPart Ο† * ofStateList Ο†')) = 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› Ο†') β€’ - π“ž.crAnF (normalOrder (ofStateList Ο†' * anPart (StateAlgebra.ofState Ο†))) := by + π“ž.crAnF (normalOrder (ofStateList Ο†' * anPart Ο†)) := by match Ο† with | .inAsymp Ο† => simp @@ -229,17 +229,17 @@ lemma crAnF_normalOrder_anPart_ofStatesList_swap (Ο† : 𝓕.States) rfl lemma crAnF_normalOrder_ofStatesList_anPart_swap (Ο† : 𝓕.States) (Ο†' : List 𝓕.States) : - π“ž.crAnF (normalOrder (ofStateList Ο†' * anPart (StateAlgebra.ofState Ο†))) + π“ž.crAnF (normalOrder (ofStateList Ο†' * anPart Ο†)) = 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› Ο†') β€’ - π“ž.crAnF (normalOrder (anPart (StateAlgebra.ofState Ο†) * ofStateList Ο†')) := by + π“ž.crAnF (normalOrder (anPart Ο† * ofStateList Ο†')) := by rw [crAnF_normalOrder_anPart_ofStatesList_swap] simp [smul_smul, FieldStatistic.exchangeSign_mul_self] lemma crAnF_normalOrder_ofStatesList_mul_anPart_swap (Ο† : 𝓕.States) (Ο†' : List 𝓕.States) : - π“ž.crAnF (normalOrder (ofStateList Ο†') * anPart (StateAlgebra.ofState Ο†)) = + π“ž.crAnF (normalOrder (ofStateList Ο†') * anPart Ο†) = 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› Ο†') β€’ - π“ž.crAnF (normalOrder (anPart (StateAlgebra.ofState Ο†) * ofStateList Ο†')) := by + π“ž.crAnF (normalOrder (anPart Ο† * ofStateList Ο†')) := by rw [← normalOrder_mul_anPart] rw [crAnF_normalOrder_ofStatesList_anPart_swap] @@ -307,9 +307,9 @@ The origin of this result is - `superCommute_ofCrAnList_ofCrAnList_eq_sum` -/ lemma crAnF_anPart_superCommute_normalOrder_ofStateList_eq_sum (Ο† : 𝓕.States) (Ο†s : List 𝓕.States) : - π“ž.crAnF ([anPart (StateAlgebra.ofState Ο†), 𝓝(Ο†s)]β‚›ca) = + π“ž.crAnF ([anPart Ο†, 𝓝(Ο†s)]β‚›ca) = βˆ‘ n : Fin Ο†s.length, 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› (Ο†s.take n)) β€’ - π“ž.crAnF ([anPart (StateAlgebra.ofState Ο†), ofState Ο†s[n]]β‚›ca) * π“ž.crAnF 𝓝(Ο†s.eraseIdx n) := by + π“ž.crAnF ([anPart Ο†, ofState Ο†s[n]]β‚›ca) * π“ž.crAnF 𝓝(Ο†s.eraseIdx n) := by match Ο† with | .inAsymp Ο† => simp @@ -333,9 +333,9 @@ Within a proto-operator algebra we have that -/ lemma crAnF_anPart_mul_normalOrder_ofStatesList_eq_superCommute (Ο† : 𝓕.States) (Ο†' : List 𝓕.States) : - π“ž.crAnF (anPart (StateAlgebra.ofState Ο†) * normalOrder (ofStateList Ο†')) = - π“ž.crAnF (normalOrder (anPart (StateAlgebra.ofState Ο†) * ofStateList Ο†')) + - π“ž.crAnF ([anPart (StateAlgebra.ofState Ο†), normalOrder (ofStateList Ο†')]β‚›ca) := by + π“ž.crAnF (anPart Ο† * normalOrder (ofStateList Ο†')) = + π“ž.crAnF (normalOrder (anPart Ο† * ofStateList Ο†')) + + π“ž.crAnF ([anPart Ο†, normalOrder (ofStateList Ο†')]β‚›ca) := by rw [anPart_mul_normalOrder_ofStateList_eq_superCommute] simp only [instCommGroup.eq_1, map_add, map_smul] congr @@ -348,7 +348,7 @@ Within a proto-operator algebra we have that lemma crAnF_ofState_mul_normalOrder_ofStatesList_eq_superCommute (Ο† : 𝓕.States) (Ο†s : List 𝓕.States) : π“ž.crAnF (ofState Ο† * 𝓝(Ο†s)) = π“ž.crAnF (normalOrder (ofState Ο† * ofStateList Ο†s)) + - π“ž.crAnF ([anPart (StateAlgebra.ofState Ο†), 𝓝(Ο†s)]β‚›ca) := by + π“ž.crAnF ([anPart Ο†, 𝓝(Ο†s)]β‚›ca) := by conv_lhs => rw [ofState_eq_crPart_add_anPart] rw [add_mul, map_add, crAnF_anPart_mul_normalOrder_ofStatesList_eq_superCommute, ← add_assoc, ← normalOrder_crPart_mul, ← map_add] @@ -363,7 +363,7 @@ noncomputable def contractStateAtIndex (Ο† : 𝓕.States) (Ο†s : List 𝓕.State match n with | none => 1 | some n => 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› (Ο†s.take n)) β€’ - π“ž.crAnF ([anPart (StateAlgebra.ofState Ο†), ofState Ο†s[n]]β‚›ca) + π“ž.crAnF ([anPart Ο†, ofState Ο†s[n]]β‚›ca) /-- Within a proto-operator algebra, diff --git a/HepLean/PerturbationTheory/Algebras/ProtoOperatorAlgebra/TimeContraction.lean b/HepLean/PerturbationTheory/Algebras/ProtoOperatorAlgebra/TimeContraction.lean index ab1567f9..353d7e28 100644 --- a/HepLean/PerturbationTheory/Algebras/ProtoOperatorAlgebra/TimeContraction.lean +++ b/HepLean/PerturbationTheory/Algebras/ProtoOperatorAlgebra/TimeContraction.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ import HepLean.PerturbationTheory.Algebras.ProtoOperatorAlgebra.NormalOrder -import HepLean.PerturbationTheory.Algebras.StateAlgebra.TimeOrder +import HepLean.PerturbationTheory.Algebras.CrAnAlgebra.TimeOrder /-! # Time contractions @@ -28,24 +28,21 @@ open FieldStatistic as their time ordering in the state algebra minus their normal ordering in the creation and annihlation algebra, both mapped to `π“ž.A`.. -/ def timeContract (Ο† ψ : 𝓕.States) : π“ž.A := - π“ž.crAnF (ofStateAlgebra (StateAlgebra.timeOrder (StateAlgebra.ofState Ο† * StateAlgebra.ofState ψ)) - - 𝓝(ofState Ο† * ofState ψ)) + π“ž.crAnF (𝓣ᢠ(ofState Ο† * ofState ψ) - 𝓝(ofState Ο† * ofState ψ)) lemma timeContract_eq_smul (Ο† ψ : 𝓕.States) : π“ž.timeContract Ο† ψ = - π“ž.crAnF (ofStateAlgebra (StateAlgebra.timeOrder - (StateAlgebra.ofState Ο† * StateAlgebra.ofState ψ)) + π“ž.crAnF (𝓣ᢠ(ofState Ο† * ofState ψ) + (-1 : β„‚) β€’ 𝓝(ofState Ο† * ofState ψ)) := by rfl lemma timeContract_of_timeOrderRel (Ο† ψ : 𝓕.States) (h : timeOrderRel Ο† ψ) : - π“ž.timeContract Ο† ψ = π“ž.crAnF ([anPart (StateAlgebra.ofState Ο†), ofState ψ]β‚›ca) := by + π“ž.timeContract Ο† ψ = π“ž.crAnF ([anPart Ο†, ofState ψ]β‚›ca) := by conv_rhs => rw [ofState_eq_crPart_add_anPart] rw [map_add, map_add, crAnF_superCommute_anPart_anPart, superCommute_anPart_crPart] simp only [timeContract, instCommGroup.eq_1, Algebra.smul_mul_assoc, add_zero] - rw [StateAlgebra.timeOrder_ofState_ofState_ordered h] + rw [timeOrder_ofState_ofState_ordered h] rw [normalOrder_ofState_mul_ofState] - rw [map_mul] - simp only [ofStateAlgebra_ofState, instCommGroup.eq_1] + simp only [instCommGroup.eq_1] rw [ofState_eq_crPart_add_anPart, ofState_eq_crPart_add_anPart] simp only [mul_add, add_mul] abel_nf @@ -56,9 +53,9 @@ lemma timeContract_of_not_timeOrderRel (Ο† ψ : 𝓕.States) (h : Β¬ timeOrderRe simp only [Int.reduceNeg, one_smul, map_add] rw [map_smul] rw [crAnF_normalOrder_ofState_ofState_swap] - rw [StateAlgebra.timeOrder_ofState_ofState_not_ordered_eq_timeOrder h] + rw [timeOrder_ofState_ofState_not_ordered_eq_timeOrder h] rw [timeContract_eq_smul] - simp only [FieldStatistic.instCommGroup.eq_1, map_smul, one_smul, map_add, smul_add] + simp only [instCommGroup.eq_1, map_smul, map_add, smul_add] rw [smul_smul, smul_smul, mul_comm] lemma timeContract_mem_center (Ο† ψ : 𝓕.States) : π“ž.timeContract Ο† ψ ∈ Subalgebra.center β„‚ π“ž.A := by diff --git a/HepLean/PerturbationTheory/Algebras/StateAlgebra/Basic.lean b/HepLean/PerturbationTheory/Algebras/StateAlgebra/Basic.lean deleted file mode 100644 index 124d94e9..00000000 --- a/HepLean/PerturbationTheory/Algebras/StateAlgebra/Basic.lean +++ /dev/null @@ -1,98 +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.CrAnStates -/-! - -# State algebra - -From the states associated with a field specification we can form a free algebra -generated by these states. We call this the state algebra, or the state free-algebra. - -The state free-algebra has minimal assumptions, yet can be used to concretely define time-ordering. - -In `HepLean.PerturbationTheory.Algebras.CrAnAlgebra.Basic` -we defined a related free-algebra generated by creation and annihilation states. - --/ - -namespace FieldSpecification -variable {𝓕 : FieldSpecification} - -/-- The state free-algebra. - The free algebra generated by `States`, - that is a position based states or assymptotic states. - As a module `StateAlgebra` is spanned by lists of `States`. -/ -abbrev StateAlgebra (𝓕 : FieldSpecification) : Type := FreeAlgebra β„‚ 𝓕.States - -namespace StateAlgebra - -open FieldStatistic - -/-- The element of the states free-algebra generated by a single state. -/ -def ofState (Ο† : 𝓕.States) : StateAlgebra 𝓕 := - FreeAlgebra.ΞΉ β„‚ Ο† - -/-- The element of the states free-algebra generated by a list of states. -/ -def ofList (Ο†s : List 𝓕.States) : StateAlgebra 𝓕 := - (List.map ofState Ο†s).prod - -@[simp] -lemma ofList_nil : ofList ([] : List 𝓕.States) = 1 := rfl - -lemma ofList_singleton (Ο† : 𝓕.States) : ofList [Ο†] = ofState Ο† := by - simp [ofList] - -lemma ofList_append (Ο†s ψs : List 𝓕.States) : - ofList (Ο†s ++ ψs) = ofList Ο†s * ofList ψs := by - rw [ofList, List.map_append, List.prod_append] - rfl - -lemma ofList_cons (Ο† : 𝓕.States) (Ο†s : List 𝓕.States) : - ofList (Ο† :: Ο†s) = ofState Ο† * ofList Ο†s := rfl - -/-- The basis of the free state algebra formed by lists of states. -/ -noncomputable def ofListBasis : Basis (List 𝓕.States) β„‚ 𝓕.StateAlgebra where - repr := FreeAlgebra.equivMonoidAlgebraFreeMonoid.toLinearEquiv - -@[simp] -lemma ofListBasis_eq_ofList (Ο†s : List 𝓕.States) : - ofListBasis Ο†s = ofList Ο†s := by - simp only [ofListBasis, FreeAlgebra.equivMonoidAlgebraFreeMonoid, MonoidAlgebra.of_apply, - Basis.coe_ofRepr, AlgEquiv.toLinearEquiv_symm, AlgEquiv.toLinearEquiv_apply, - AlgEquiv.ofAlgHom_symm_apply, ofList] - erw [MonoidAlgebra.lift_apply] - simp only [zero_smul, Finsupp.sum_single_index, one_smul] - rw [@FreeMonoid.lift_apply] - simp only [List.prod] - match Ο†s with - | [] => rfl - | Ο† :: Ο†s => - erw [List.map_cons] - -/-! - -## The super commutor on the state algebra. - --/ - -/-- The super commutor on the free state algebra. For two bosonic operators - or a bosonic and fermionic operator this corresponds to the usual commutator - whilst for two fermionic operators this corresponds to the anti-commutator. -/ -noncomputable def superCommute : 𝓕.StateAlgebra β†’β‚—[β„‚] 𝓕.StateAlgebra β†’β‚—[β„‚] 𝓕.StateAlgebra := - Basis.constr ofListBasis β„‚ fun Ο†s => - Basis.constr ofListBasis β„‚ fun Ο†s' => - ofList (Ο†s ++ Ο†s') - 𝓒(𝓕 |>β‚› Ο†s, 𝓕 |>β‚› Ο†s') β€’ ofList (Ο†s' ++ Ο†s) - -local notation "⟨" Ο†s "," Ο†s' "βŸ©β‚›" => superCommute Ο†s Ο†s' - -lemma superCommute_ofList (Ο†s Ο†s' : List 𝓕.States) : ⟨ofList Ο†s, ofList Ο†s'βŸ©β‚› = - ofList (Ο†s ++ Ο†s') - 𝓒(𝓕 |>β‚› Ο†s, 𝓕 |>β‚› Ο†s') β€’ ofList (Ο†s' ++ Ο†s) := by - rw [← ofListBasis_eq_ofList, ← ofListBasis_eq_ofList] - simp only [superCommute, Basis.constr_basis] - -end StateAlgebra - -end FieldSpecification diff --git a/HepLean/PerturbationTheory/CreateAnnihilate.lean b/HepLean/PerturbationTheory/CreateAnnihilate.lean index 1bcbc364..1947847e 100644 --- a/HepLean/PerturbationTheory/CreateAnnihilate.lean +++ b/HepLean/PerturbationTheory/CreateAnnihilate.lean @@ -67,4 +67,8 @@ lemma sum_eq {M : Type} [AddCommMonoid M] (f : CreateAnnihilate β†’ M) : change βˆ‘ i in {create, annihilate}, f i = f create + f annihilate simp +@[simp] +lemma CreateAnnihilate_card_eq_two : Fintype.card CreateAnnihilate = 2 := by + rfl + end CreateAnnihilate diff --git a/HepLean/PerturbationTheory/FieldSpecification/Basic.lean b/HepLean/PerturbationTheory/FieldSpecification/Basic.lean index 7aec6b37..cbe795fe 100644 --- a/HepLean/PerturbationTheory/FieldSpecification/Basic.lean +++ b/HepLean/PerturbationTheory/FieldSpecification/Basic.lean @@ -66,6 +66,11 @@ def statesToField : 𝓕.States β†’ 𝓕.Fields | States.position Ο† => Ο†.1 | States.outAsymp Ο† => Ο†.1 +/-- The bool on `States` which is true only for position states. -/ +def statesIsPosition : 𝓕.States β†’ Bool + | States.position _ => true + | _ => false + /-- The statistics associated to a state. -/ def statesStatistic : 𝓕.States β†’ FieldStatistic := 𝓕.statistics ∘ 𝓕.statesToField diff --git a/HepLean/PerturbationTheory/FieldSpecification/CrAnSection.lean b/HepLean/PerturbationTheory/FieldSpecification/CrAnSection.lean index b66ed1a7..e251ffec 100644 --- a/HepLean/PerturbationTheory/FieldSpecification/CrAnSection.lean +++ b/HepLean/PerturbationTheory/FieldSpecification/CrAnSection.lean @@ -149,6 +149,44 @@ instance fintype : (Ο†s : List 𝓕.States) β†’ Fintype (CrAnSection Ο†s) haveI : Fintype (CrAnSection Ο†s) := fintype Ο†s Fintype.ofEquiv _ consEquiv.symm +@[simp] +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 Ο†) * + Fintype.card (CrAnSection Ο†s) := by + rw [Fintype.ofEquiv_card consEquiv.symm] + simp + +lemma card_eq_mul : {Ο†s : List 𝓕.States} β†’ Fintype.card (CrAnSection Ο†s) = + 2 ^ (List.countP 𝓕.statesIsPosition Ο†s) + | [] => by + simp + | States.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] + ring + | States.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 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] + +lemma card_perm_eq {Ο†s Ο†s' : List 𝓕.States} (h : Ο†s.Perm Ο†s') : + Fintype.card (CrAnSection Ο†s) = Fintype.card (CrAnSection Ο†s') := by + rw [card_eq_mul, card_eq_mul] + congr 1 + exact List.Perm.countP_congr h fun x => congrFun rfl + @[simp] lemma sum_nil (f : CrAnSection (𝓕 := 𝓕) [] β†’ M) [AddCommMonoid M] : βˆ‘ (s : CrAnSection []), f s = f ⟨[], rfl⟩ := by diff --git a/HepLean/PerturbationTheory/FieldSpecification/TimeOrder.lean b/HepLean/PerturbationTheory/FieldSpecification/TimeOrder.lean index 7cf30ed7..ea74d71e 100644 --- a/HepLean/PerturbationTheory/FieldSpecification/TimeOrder.lean +++ b/HepLean/PerturbationTheory/FieldSpecification/TimeOrder.lean @@ -4,8 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ import HepLean.Mathematics.List.InsertionSort -import HepLean.PerturbationTheory.Algebras.StateAlgebra.Basic -import HepLean.PerturbationTheory.Koszul.KoszulSign +import HepLean.PerturbationTheory.FieldSpecification.NormalOrder /-! # Time ordering of states @@ -15,6 +14,12 @@ import HepLean.PerturbationTheory.Koszul.KoszulSign namespace FieldSpecification variable {𝓕 : FieldSpecification} +/-! + +## Time ordering for states + +-/ + /-- 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. -/ @@ -123,6 +128,11 @@ lemma timeOrder_maxTimeField (Ο† : 𝓕.States) (Ο†s : List 𝓕.States) def timeOrderSign (Ο†s : List 𝓕.States) : β„‚ := Wick.koszulSign 𝓕.statesStatistic 𝓕.timeOrderRel Ο†s +@[simp] +lemma timeOrderSign_nil : timeOrderSign (𝓕 := 𝓕) [] = 1 := by + simp only [timeOrderSign] + rfl + lemma timeOrderSign_pair_ordered {Ο† ψ : 𝓕.States} (h : timeOrderRel Ο† ψ) : timeOrderSign [Ο†, ψ] = 1 := by simp only [timeOrderSign, Wick.koszulSign, Wick.koszulSignInsert, mul_one, ite_eq_left_iff, @@ -169,5 +179,253 @@ lemma timeOrderList_eq_maxTimeField_timeOrderList (Ο† : 𝓕.States) (Ο†s : List timeOrderList (Ο† :: Ο†s) = maxTimeField Ο† Ο†s :: timeOrderList (eraseMaxTimeField Ο† Ο†s) := by exact insertionSort_eq_insertionSortMin_cons timeOrderRel Ο† Ο†s +/-! + +## Time ordering for CrAnStates + +-/ + +/-! + +## timeOrderRel + +-/ + +/-- The time ordering relation on CrAnStates. -/ +def crAnTimeOrderRel (a b : 𝓕.CrAnStates) : Prop := 𝓕.timeOrderRel a.1 b.1 + +/-- The relation `crAnTimeOrderRel` is decidable, but not computablly so due to + `Real.decidableLE`. -/ +noncomputable instance (Ο† Ο†' : 𝓕.CrAnStates) : Decidable (crAnTimeOrderRel Ο† Ο†') := + inferInstanceAs (Decidable (𝓕.timeOrderRel Ο†.1 Ο†'.1)) + +/-- Time ordering of `CrAnStates` is total. -/ +instance : IsTotal 𝓕.CrAnStates 𝓕.crAnTimeOrderRel where + total a b := IsTotal.total (r := 𝓕.timeOrderRel) a.1 b.1 + +/-- Time ordering of `CrAnStates` is transitive. -/ +instance : IsTrans 𝓕.CrAnStates 𝓕.crAnTimeOrderRel where + trans a b c := IsTrans.trans (r := 𝓕.timeOrderRel) a.1 b.1 c.1 + +/-- The sign associated with putting a list of `CrAnStates` 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) : β„‚ := + Wick.koszulSign 𝓕.crAnStatistics 𝓕.crAnTimeOrderRel Ο†s + +@[simp] +lemma crAnTimeOrderSign_nil : crAnTimeOrderSign (𝓕 := 𝓕) [] = 1 := by + simp only [crAnTimeOrderSign] + rfl + +/-- Sort a list of `CrAnStates` based on `crAnTimeOrderRel`. -/ +def crAnTimeOrderList (Ο†s : List 𝓕.CrAnStates) : List 𝓕.CrAnStates := + List.insertionSort 𝓕.crAnTimeOrderRel Ο†s + +@[simp] +lemma crAnTimeOrderList_nil : crAnTimeOrderList (𝓕 := 𝓕) [] = [] := by + simp [crAnTimeOrderList] + +/-! + +## Relationship to sections +-/ + +lemma koszulSignInsert_crAnTimeOrderRel_crAnSection {Ο† : 𝓕.States} {ψ : 𝓕.CrAnStates} + (h : ψ.1 = Ο†) : {Ο†s : List 𝓕.States} β†’ (ψs : CrAnSection Ο†s) β†’ + Wick.koszulSignInsert 𝓕.crAnStatistics 𝓕.crAnTimeOrderRel ψ ψs.1 = + Wick.koszulSignInsert 𝓕.statesStatistic 𝓕.timeOrderRel Ο† Ο†s + | [], ⟨[], h⟩ => by + simp [Wick.koszulSignInsert] + | Ο†' :: Ο†s, ⟨ψ' :: ψs, h1⟩ => by + simp only [Wick.koszulSignInsert, crAnTimeOrderRel, h] + simp only [List.map_cons, List.cons.injEq] at h1 + have hi := koszulSignInsert_crAnTimeOrderRel_crAnSection h (Ο†s := Ο†s) ⟨ψs, h1.2⟩ + rw [hi] + congr + Β· exact h1.1 + Β· simp only [crAnStatistics, crAnStatesToStates, Function.comp_apply] + congr + Β· simp only [crAnStatistics, crAnStatesToStates, Function.comp_apply] + congr + exact h1.1 + +@[simp] +lemma crAnTimeOrderSign_crAnSection : {Ο†s : List 𝓕.States} β†’ (ψs : CrAnSection Ο†s) β†’ + crAnTimeOrderSign ψs.1 = timeOrderSign Ο†s + | [], ⟨[], h⟩ => by + simp + | Ο† :: Ο†s, ⟨ψ :: ψs, h⟩ => by + simp only [crAnTimeOrderSign, Wick.koszulSign, timeOrderSign] + simp only [List.map_cons, List.cons.injEq] at h + congr 1 + Β· 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 = + List.orderedInsert 𝓕.timeOrderRel Ο† Ο†s + | [], ⟨[], _⟩ => by + simp only [List.orderedInsert, List.map_cons, List.map_nil, List.cons.injEq, and_true] + exact h + | Ο†' :: Ο†s, ⟨ψ' :: ψs, h1⟩ => by + simp only [List.orderedInsert, crAnTimeOrderRel, h] + simp only [List.map_cons, List.cons.injEq] at h1 + by_cases hr : timeOrderRel Ο† Ο†' + Β· simp only [hr, ↓reduceIte] + rw [← h1.1] at hr + simp only [crAnStatesToStates] 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 [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 + | [], ⟨[], h⟩ => by + simp + | Ο† :: Ο†s, ⟨ψ :: ψs, h⟩ => by + simp only [crAnTimeOrderList, List.insertionSort, timeOrderList] + simp only [List.map_cons, List.cons.injEq] at h + exact orderedInsert_crAnTimeOrderRel_crAnSection h.1 ⟨(List.insertionSort crAnTimeOrderRel ψs), + crAnTimeOrderList_crAnSection_is_crAnSection ⟨ψs, h.2⟩⟩ + +/-- Time ordering of sections of a list of states. -/ +def crAnSectionTimeOrder (Ο†s : List 𝓕.States) (ψ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) β†’ + (ho : List.orderedInsert crAnTimeOrderRel ψ ψs.1 = + List.orderedInsert crAnTimeOrderRel ψ' ψs'.1) β†’ ψ = ψ' ∧ ψs = ψs' + | [], ⟨[], _⟩, ⟨[], _⟩, h => by + simp only [List.orderedInsert, List.cons.injEq, and_true] at h + simpa using h + | Ο† :: Ο†s, ⟨ψ1 :: ψs, h1⟩, ⟨ψ1' :: ψs', h1'⟩, ho => by + simp only [List.map_cons, List.cons.injEq] at h1 h1' + have ih := orderedInsert_crAnTimeOrderRel_injective h ⟨ψs, h1.2⟩ ⟨ψs', h1'.2⟩ + simp only [List.orderedInsert] at ho + by_cases hr : crAnTimeOrderRel ψ ψ1 + Β· simp_all only [ite_true] + by_cases hr2 : crAnTimeOrderRel ψ' ψ1' + Β· simp_all + Β· simp only [crAnTimeOrderRel] at hr hr2 + simp_all only + rw [crAnStatesToStates] at h1 h1' + rw [h1.1] at hr + rw [h1'.1] at hr2 + exact False.elim (hr2 hr) + Β· simp_all only [ite_false] + by_cases hr2 : crAnTimeOrderRel ψ' ψ1' + Β· simp only [crAnTimeOrderRel] at hr hr2 + simp_all only + rw [crAnStatesToStates] at h1 h1' + rw [h1.1] at hr + rw [h1'.1] at hr2 + exact False.elim (hr hr2) + Β· simp only [hr2, ↓reduceIte, List.cons.injEq] at ho + have ih' := ih ho.2 + simp_all only [and_self, implies_true, not_false_eq_true, true_and] + apply Subtype.ext + simp only [List.cons.injEq, true_and] + rw [Subtype.eq_iff] at ih' + exact ih'.2 + +lemma crAnSectionTimeOrder_injective : {Ο†s : List 𝓕.States} β†’ + Function.Injective (𝓕.crAnSectionTimeOrder Ο†s) + | [], ⟨[], _⟩, ⟨[], _⟩ => by + simp + | Ο† :: Ο†s, ⟨ψ :: ψs, h⟩, ⟨ψ' :: ψs', h'⟩ => by + intro h1 + apply Subtype.ext + simp only [List.cons.injEq] + simp only [crAnSectionTimeOrder] at h1 + 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' + have hin := orderedInsert_crAnTimeOrderRel_injective (by rw [h.1, h'.1]) + (𝓕.crAnSectionTimeOrder Ο†s ⟨ψs, h.2⟩) + (𝓕.crAnSectionTimeOrder Ο†s ⟨ψs', h'.2⟩) h1 + apply And.intro hin.1 + have hl := crAnSectionTimeOrder_injective hin.2 + rw [Subtype.ext_iff] at hl + simpa using hl + +lemma crAnSectionTimeOrder_bijective (Ο†s : List 𝓕.States) : + Function.Bijective (𝓕.crAnSectionTimeOrder Ο†s) := by + rw [Fintype.bijective_iff_injective_and_card] + apply And.intro crAnSectionTimeOrder_injective + apply CrAnSection.card_perm_eq + simp only [timeOrderList] + exact List.Perm.symm (List.perm_insertionSort timeOrderRel Ο†s) + +lemma sum_crAnSections_timeOrder {Ο†s : List 𝓕.States} [AddCommMonoid M] + (f : CrAnSection (timeOrderList Ο†s) β†’ M) : βˆ‘ s, f s = βˆ‘ s, f (𝓕.crAnSectionTimeOrder Ο†s s) := by + erw [(Equiv.ofBijective _ (𝓕.crAnSectionTimeOrder_bijective Ο†s)).sum_comp] + +/-! + +## normTimeOrderRel + +-/ + +/-- The time ordering relation on `CrAnStates` such that if two CrAnStates have the same + time, we normal order them. -/ +def normTimeOrderRel (a b : 𝓕.CrAnStates) : 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 Ο† Ο†') := + instDecidableAnd + +/-- Norm-Time ordering of `CrAnStates` is total. -/ +instance : IsTotal 𝓕.CrAnStates 𝓕.normTimeOrderRel where + total a b := by + simp only [normTimeOrderRel] + match IsTotal.total (r := 𝓕.crAnTimeOrderRel) a b, + IsTotal.total (r := 𝓕.normalOrderRel) a b with + | Or.inl h1, Or.inl h2 => simp [h1, h2] + | Or.inr h1, Or.inl h2 => + simp only [h1, h2, imp_self, and_true, true_and] + by_cases hn : crAnTimeOrderRel a b + Β· simp [hn] + Β· simp [hn] + | Or.inl h1, Or.inr h2 => + simp only [h1, true_and, h2, imp_self, and_true] + by_cases hn : crAnTimeOrderRel b a + Β· simp [hn] + Β· simp [hn] + | Or.inr h1, Or.inr h2 => simp [h1, h2] + +/-- Norm-Time ordering of `CrAnStates` is transitive. -/ +instance : IsTrans 𝓕.CrAnStates 𝓕.normTimeOrderRel where + trans a b c := by + intro h1 h2 + simp_all only [normTimeOrderRel] + apply And.intro + Β· exact IsTrans.trans _ _ _ h1.1 h2.1 + Β· intro hc + refine IsTrans.trans _ _ _ (h1.2 ?_) (h2.2 ?_) + Β· 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 state of greatest time to the left). + We pick up a minus sign for every fermion paired crossed. -/ +def normTimeOrderSign (Ο†s : List 𝓕.CrAnStates) : β„‚ := + Wick.koszulSign 𝓕.crAnStatistics 𝓕.normTimeOrderRel Ο†s + +/-- Sort a list of `CrAnStates` based on `normTimeOrderRel`. -/ +def normTimeOrderList (Ο†s : List 𝓕.CrAnStates) : List 𝓕.CrAnStates := + List.insertionSort 𝓕.normTimeOrderRel Ο†s + end end FieldSpecification diff --git a/HepLean/PerturbationTheory/WickContraction/Involutions.lean b/HepLean/PerturbationTheory/WickContraction/Involutions.lean index a08d06b0..3a17f35b 100644 --- a/HepLean/PerturbationTheory/WickContraction/Involutions.lean +++ b/HepLean/PerturbationTheory/WickContraction/Involutions.lean @@ -3,10 +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.WickContraction.Uncontracted -import HepLean.PerturbationTheory.Algebras.StateAlgebra.TimeOrder -import HepLean.PerturbationTheory.Algebras.ProtoOperatorAlgebra.TimeContraction -import HepLean.PerturbationTheory.WickContraction.InsertAndContract +import HepLean.PerturbationTheory.WickContraction.Basic /-! # Involution associated with a contraction diff --git a/HepLean/PerturbationTheory/WickContraction/IsFull.lean b/HepLean/PerturbationTheory/WickContraction/IsFull.lean index 8eb6a9da..51a060af 100644 --- a/HepLean/PerturbationTheory/WickContraction/IsFull.lean +++ b/HepLean/PerturbationTheory/WickContraction/IsFull.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ import HepLean.Mathematics.Fin.Involutions +import HepLean.PerturbationTheory.WickContraction.ExtractEquiv import HepLean.PerturbationTheory.WickContraction.Involutions /-! diff --git a/HepLean/PerturbationTheory/WickContraction/TimeContract.lean b/HepLean/PerturbationTheory/WickContraction/TimeContract.lean index cc4da1a1..4a584453 100644 --- a/HepLean/PerturbationTheory/WickContraction/TimeContract.lean +++ b/HepLean/PerturbationTheory/WickContraction/TimeContract.lean @@ -88,7 +88,7 @@ lemma timeConract_insertAndContract_some_eq_mul_contractStateAtIndex_lt Β· simp only [hik, ↓reduceIte, MulMemClass.coe_mul] rw [π“ž.timeContract_of_timeOrderRel] trans (1 : β„‚) β€’ (π“ž.crAnF ((CrAnAlgebra.superCommute - (CrAnAlgebra.anPart (StateAlgebra.ofState Ο†))) (CrAnAlgebra.ofState Ο†s[k.1])) * + (CrAnAlgebra.anPart Ο†)) (CrAnAlgebra.ofState Ο†s[k.1])) * ↑(timeContract π“ž Ο†sΞ›)) Β· simp simp only [smul_smul] diff --git a/HepLean/PerturbationTheory/WicksTheorem.lean b/HepLean/PerturbationTheory/WicksTheorem.lean index ca2cbf19..9f1e24a6 100644 --- a/HepLean/PerturbationTheory/WicksTheorem.lean +++ b/HepLean/PerturbationTheory/WicksTheorem.lean @@ -19,7 +19,6 @@ Wick's theorem is related to Isserlis' theorem in mathematics. namespace FieldSpecification variable {𝓕 : FieldSpecification} {π“ž : 𝓕.ProtoOperatorAlgebra} open CrAnAlgebra -open StateAlgebra open ProtoOperatorAlgebra open HepLean.List open WickContraction @@ -318,9 +317,9 @@ lemma wick_term_cons_eq_sum_wick_term (Ο† : 𝓕.States) (Ο†s : List 𝓕.States /-- Wick's theorem for the empty list. -/ lemma wicks_theorem_nil : - π“ž.crAnF (ofStateAlgebra (timeOrder (ofList []))) = βˆ‘ (nilΞ› : WickContraction [].length), + π“ž.crAnF (𝓣ᢠ(ofStateList [])) = βˆ‘ (nilΞ› : WickContraction [].length), (nilΞ›.sign β€’ nilΞ›.timeContract π“ž) * π“ž.crAnF 𝓝([nilΞ›]ᡘᢜ) := by - rw [timeOrder_ofList_nil] + rw [timeOrder_ofStateList_nil] simp only [map_one, List.length_nil, Algebra.smul_mul_assoc] rw [sum_WickContraction_nil, uncontractedListGet, nil_zero_uncontractedList] simp only [List.map_nil] @@ -352,12 +351,12 @@ remark wicks_theorem_context := " - The product of time-contractions of the contracted pairs of `c`. - The normal-ordering of the uncontracted fields in `c`. -/ -theorem wicks_theorem : (Ο†s : List 𝓕.States) β†’ π“ž.crAnF (ofStateAlgebra (timeOrder (ofList Ο†s))) = +theorem wicks_theorem : (Ο†s : List 𝓕.States) β†’ π“ž.crAnF (𝓣ᢠ(ofStateList Ο†s)) = βˆ‘ (Ο†sΞ› : WickContraction Ο†s.length), (Ο†sΞ›.sign β€’ Ο†sΞ›.timeContract π“ž) * π“ž.crAnF 𝓝([Ο†sΞ›]ᡘᢜ) | [] => wicks_theorem_nil | Ο† :: Ο†s => by have ih := wicks_theorem (eraseMaxTimeField Ο† Ο†s) - rw [timeOrder_eq_maxTimeField_mul_finset, map_mul, map_mul, ih, Finset.mul_sum] + rw [timeOrder_eq_maxTimeField_mul_finset, map_mul, ih, Finset.mul_sum] have h1 : Ο† :: Ο†s = (eraseMaxTimeField Ο† Ο†s).insertIdx (maxTimeFieldPosFin Ο† Ο†s) (maxTimeField Ο† Ο†s) := by simp only [eraseMaxTimeField, insertionSortDropMinPos, List.length_cons, Nat.succ_eq_add_one, @@ -369,8 +368,8 @@ theorem wicks_theorem : (Ο†s : List 𝓕.States) β†’ π“ž.crAnF (ofStateAlgebra funext c have ht := Subalgebra.mem_center_iff.mp (Subalgebra.smul_mem (Subalgebra.center β„‚ π“ž.A) (WickContraction.timeContract π“ž c).2 (sign (eraseMaxTimeField Ο† Ο†s) c)) - rw [map_smul, map_smul, Algebra.smul_mul_assoc, ← mul_assoc, ht, mul_assoc, ← map_mul] - rw [ofStateAlgebra_ofState, wick_term_cons_eq_sum_wick_term (π“ž := π“ž) + rw [map_smul, Algebra.smul_mul_assoc, ← mul_assoc, ht, mul_assoc, ← map_mul] + rw [wick_term_cons_eq_sum_wick_term (π“ž := π“ž) (maxTimeField Ο† Ο†s) (eraseMaxTimeField Ο† Ο†s) (maxTimeFieldPosFin Ο† Ο†s) c] trans (1 : β„‚) β€’ βˆ‘ k : Option { x // x ∈ c.uncontracted }, sign (List.insertIdx (↑(maxTimeFieldPosFin Ο† Ο†s)) (maxTimeField Ο† Ο†s) (eraseMaxTimeField Ο† Ο†s)) diff --git a/scripts/MetaPrograms/notes.lean b/scripts/MetaPrograms/notes.lean index 64c4ad43..b708f079 100644 --- a/scripts/MetaPrograms/notes.lean +++ b/scripts/MetaPrograms/notes.lean @@ -144,12 +144,9 @@ def perturbationTheory : Note where .p "We will want to consider all three of these types of states simultanously so we define and inductive type `States` which is the disjoint union of these three types of states.", .name `FieldSpecification.States, - .name `FieldSpecification.StateAlgebra, .h2 "Time ordering", .name `FieldSpecification.timeOrderRel, .name `FieldSpecification.timeOrderSign, - .name `FieldSpecification.StateAlgebra.timeOrder, - .name `FieldSpecification.StateAlgebra.timeOrder_eq_maxTimeField_mul_finset, .h2 "Creation and annihilation states", .h2 "Normal ordering", .h2 "Proto-operator algebra",