diff --git a/HepLean.lean b/HepLean.lean index e6509a71..393c6758 100644 --- a/HepLean.lean +++ b/HepLean.lean @@ -121,9 +121,9 @@ 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.OperatorAlgebra.Basic -import HepLean.PerturbationTheory.Algebras.OperatorAlgebra.NormalOrder -import HepLean.PerturbationTheory.Algebras.OperatorAlgebra.TimeContraction +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 diff --git a/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/NormalOrder.lean b/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/NormalOrder.lean index 2ad05fcb..d5a99b07 100644 --- a/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/NormalOrder.lean +++ b/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/NormalOrder.lean @@ -10,17 +10,19 @@ import HepLean.PerturbationTheory.Koszul.KoszulSign # Normal Ordering in the CrAnAlgebra +In the module +`HepLean.PerturbationTheory.FieldSpecification.NormalOrder` +we defined the normal ordering of a list of `CrAnStates`. +In this module we extend the normal ordering to a linear map on `CrAnAlgebra`. + +We derive properties of this normal ordering. -/ namespace FieldSpecification variable {𝓕 : FieldSpecification} open FieldStatistic -/-! -## Normal order on the CrAnAlgebra - --/ namespace CrAnAlgebra noncomputable section @@ -51,6 +53,12 @@ lemma normalOrder_one : normalOrder (𝓕 := 𝓕) 1 = 1 := by rw [← ofCrAnList_nil, normalOrder_ofCrAnList] simp +/-! + +## Normal ordering with a creation operator on the left or annihilation on the right + +-/ + lemma normalOrder_ofCrAnList_cons_create (Ο† : 𝓕.CrAnStates) (hΟ† : 𝓕 |>ᢜ Ο† = CreateAnnihilate.create) (Ο†s : List 𝓕.CrAnStates) : normalOrder (ofCrAnList (Ο† :: Ο†s)) = @@ -95,9 +103,48 @@ lemma normalOrder_mul_annihilate (Ο† : 𝓕.CrAnStates) rw [← ofCrAnList_singleton, ← ofCrAnList_append, ofCrAnList_singleton] rw [normalOrder_ofCrAnList_append_annihilate Ο† hΟ†] +lemma normalOrder_crPart_mul (Ο† : 𝓕.States) (a : CrAnAlgebra 𝓕) : + normalOrder (crPart (StateAlgebra.ofState Ο†) * a) = + crPart (StateAlgebra.ofState Ο†) * normalOrder a := by + match Ο† with + | .negAsymp Ο† => + dsimp only [crPart, StateAlgebra.ofState] + simp only [FreeAlgebra.lift_ΞΉ_apply] + exact normalOrder_create_mul ⟨States.negAsymp Ο†, ()⟩ rfl a + | .position Ο† => + dsimp only [crPart, StateAlgebra.ofState] + simp only [FreeAlgebra.lift_ΞΉ_apply] + refine normalOrder_create_mul _ ?_ _ + simp [crAnStatesToCreateAnnihilate] + | .posAsymp Ο† => + simp + +lemma normalOrder_mul_anPart (Ο† : 𝓕.States) (a : CrAnAlgebra 𝓕) : + normalOrder (a * anPart (StateAlgebra.ofState Ο†)) = + normalOrder a * anPart (StateAlgebra.ofState Ο†) := by + match Ο† with + | .negAsymp Ο† => + simp + | .position Ο† => + dsimp only [anPart, StateAlgebra.ofState] + simp only [FreeAlgebra.lift_ΞΉ_apply] + refine normalOrder_mul_annihilate _ ?_ _ + simp [crAnStatesToCreateAnnihilate] + | .posAsymp Ο† => + dsimp only [anPart, StateAlgebra.ofState] + simp only [FreeAlgebra.lift_ΞΉ_apply] + refine normalOrder_mul_annihilate _ ?_ _ + simp [crAnStatesToCreateAnnihilate] + +/-! + +## Normal ordering for an adjacent creation and annihliation state + +The main result of this section is `normalOrder_superCommute_annihilate_create`. +-/ + lemma normalOrder_swap_create_annihlate_ofCrAnList_ofCrAnList (Ο†c Ο†a : 𝓕.CrAnStates) - (hΟ†c : 𝓕 |>ᢜ Ο†c = CreateAnnihilate.create) - (hΟ†a : 𝓕 |>ᢜ Ο†a = CreateAnnihilate.annihilate) + (hΟ†c : 𝓕 |>ᢜ Ο†c = CreateAnnihilate.create) (hΟ†a : 𝓕 |>ᢜ Ο†a = CreateAnnihilate.annihilate) (Ο†s Ο†s' : List 𝓕.CrAnStates) : normalOrder (ofCrAnList Ο†s' * ofCrAnState Ο†c * ofCrAnState Ο†a * ofCrAnList Ο†s) = 𝓒(𝓕 |>β‚› Ο†c, 𝓕 |>β‚› Ο†a) β€’ @@ -111,8 +158,7 @@ lemma normalOrder_swap_create_annihlate_ofCrAnList_ofCrAnList (Ο†c Ο†a : 𝓕.Cr noncomm_ring lemma normalOrder_swap_create_annihlate_ofCrAnList (Ο†c Ο†a : 𝓕.CrAnStates) - (hΟ†c : 𝓕 |>ᢜ Ο†c = CreateAnnihilate.create) - (hΟ†a : 𝓕 |>ᢜ Ο†a = CreateAnnihilate.annihilate) + (hΟ†c : 𝓕 |>ᢜ Ο†c = CreateAnnihilate.create) (hΟ†a : 𝓕 |>ᢜ Ο†a = CreateAnnihilate.annihilate) (Ο†s : List 𝓕.CrAnStates) (a : 𝓕.CrAnAlgebra) : normalOrder (ofCrAnList Ο†s * ofCrAnState Ο†c * ofCrAnState Ο†a * a) = 𝓒(𝓕 |>β‚› Ο†c, 𝓕 |>β‚› Ο†a) β€’ @@ -129,8 +175,7 @@ lemma normalOrder_swap_create_annihlate_ofCrAnList (Ο†c Ο†a : 𝓕.CrAnStates) rfl lemma normalOrder_swap_create_annihlate (Ο†c Ο†a : 𝓕.CrAnStates) - (hΟ†c : 𝓕 |>ᢜ Ο†c = CreateAnnihilate.create) - (hΟ†a : 𝓕 |>ᢜ Ο†a = CreateAnnihilate.annihilate) + (hΟ†c : 𝓕 |>ᢜ Ο†c = CreateAnnihilate.create) (hΟ†a : 𝓕 |>ᢜ Ο†a = CreateAnnihilate.annihilate) (a b : 𝓕.CrAnAlgebra) : normalOrder (a * ofCrAnState Ο†c * ofCrAnState Ο†a * b) = 𝓒(𝓕 |>β‚› Ο†c, 𝓕 |>β‚› Ο†a) β€’ @@ -149,11 +194,10 @@ lemma normalOrder_swap_create_annihlate (Ο†c Ο†a : 𝓕.CrAnStates) rfl lemma normalOrder_superCommute_create_annihilate (Ο†c Ο†a : 𝓕.CrAnStates) - (hΟ†c : 𝓕 |>ᢜ Ο†c = CreateAnnihilate.create) - (hΟ†a : 𝓕 |>ᢜ Ο†a = CreateAnnihilate.annihilate) + (hΟ†c : 𝓕 |>ᢜ Ο†c = CreateAnnihilate.create) (hΟ†a : 𝓕 |>ᢜ Ο†a = CreateAnnihilate.annihilate) (a b : 𝓕.CrAnAlgebra) : normalOrder (a * superCommute (ofCrAnState Ο†c) (ofCrAnState Ο†a) * b) = 0 := by - rw [superCommute_ofCrAnState] + rw [superCommute_ofCrAnState_ofCrAnState] simp only [instCommGroup.eq_1, Algebra.smul_mul_assoc] rw [mul_sub, sub_mul, map_sub, ← smul_mul_assoc] rw [← mul_assoc, ← mul_assoc] @@ -162,49 +206,15 @@ lemma normalOrder_superCommute_create_annihilate (Ο†c Ο†a : 𝓕.CrAnStates) map_smul, sub_self] lemma normalOrder_superCommute_annihilate_create (Ο†c Ο†a : 𝓕.CrAnStates) - (hΟ†c : 𝓕 |>ᢜ Ο†c = CreateAnnihilate.create) - (hΟ†a : 𝓕 |>ᢜ Ο†a = CreateAnnihilate.annihilate) + (hΟ†c : 𝓕 |>ᢜ Ο†c = CreateAnnihilate.create) (hΟ†a : 𝓕 |>ᢜ Ο†a = CreateAnnihilate.annihilate) (a b : 𝓕.CrAnAlgebra) : normalOrder (a * superCommute (ofCrAnState Ο†a) (ofCrAnState Ο†c) * b) = 0 := by - rw [superCommute_ofCrAnState_symm] + rw [superCommute_ofCrAnState_ofCrAnState_symm] simp only [instCommGroup.eq_1, neg_smul, mul_neg, Algebra.mul_smul_comm, neg_mul, Algebra.smul_mul_assoc, map_neg, map_smul, neg_eq_zero, smul_eq_zero] apply Or.inr exact normalOrder_superCommute_create_annihilate Ο†c Ο†a hΟ†c hΟ†a a b -lemma normalOrder_crPart_mul (Ο† : 𝓕.States) (a : CrAnAlgebra 𝓕) : - normalOrder (crPart (StateAlgebra.ofState Ο†) * a) = - crPart (StateAlgebra.ofState Ο†) * normalOrder a := by - match Ο† with - | .negAsymp Ο† => - dsimp only [crPart, StateAlgebra.ofState] - simp only [FreeAlgebra.lift_ΞΉ_apply] - exact normalOrder_create_mul ⟨States.negAsymp Ο†, ()⟩ rfl a - | .position Ο† => - dsimp only [crPart, StateAlgebra.ofState] - simp only [FreeAlgebra.lift_ΞΉ_apply] - refine normalOrder_create_mul _ ?_ _ - simp [crAnStatesToCreateAnnihilate] - | .posAsymp Ο† => - simp - -lemma normalOrder_mul_anPart (Ο† : 𝓕.States) (a : CrAnAlgebra 𝓕) : - normalOrder (a * anPart (StateAlgebra.ofState Ο†)) = - normalOrder a * anPart (StateAlgebra.ofState Ο†) := by - match Ο† with - | .negAsymp Ο† => - simp - | .position Ο† => - dsimp only [anPart, StateAlgebra.ofState] - simp only [FreeAlgebra.lift_ΞΉ_apply] - refine normalOrder_mul_annihilate _ ?_ _ - simp [crAnStatesToCreateAnnihilate] - | .posAsymp Ο† => - dsimp only [anPart, StateAlgebra.ofState] - simp only [FreeAlgebra.lift_ΞΉ_apply] - refine normalOrder_mul_annihilate _ ?_ _ - simp [crAnStatesToCreateAnnihilate] - lemma normalOrder_swap_crPart_anPart (Ο† Ο†' : 𝓕.States) (a b : CrAnAlgebra 𝓕) : normalOrder (a * (crPart (StateAlgebra.ofState Ο†)) * (anPart (StateAlgebra.ofState Ο†')) * b) = 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› Ο†') β€’ @@ -240,6 +250,14 @@ lemma normalOrder_swap_crPart_anPart (Ο† Ο†' : 𝓕.States) (a b : CrAnAlgebra rfl rfl +/-! + +## Normal ordering for an anPart and crPart + +Using the results from above. + +-/ + lemma normalOrder_swap_anPart_crPart (Ο† Ο†' : 𝓕.States) (a b : CrAnAlgebra 𝓕) : normalOrder (a * (anPart (StateAlgebra.ofState Ο†)) * (crPart (StateAlgebra.ofState Ο†')) * b) = 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› Ο†') β€’ normalOrder (a * (crPart (StateAlgebra.ofState Ο†')) * @@ -290,15 +308,80 @@ lemma normalOrder_superCommute_anPart_crPart (Ο† Ο†' : 𝓕.States) (a b : CrAnA simp only [anPart_posAsymp, crPart_position] refine normalOrder_superCommute_annihilate_create _ _ (by rfl) (by rfl) _ _ +/-! + +## The normal ordering of a product of two states + +-/ + +@[simp] +lemma normalOrder_crPart_mul_crPart (Ο† Ο†' : 𝓕.States) : + normalOrder (crPart (StateAlgebra.ofState Ο†) * crPart (StateAlgebra.ofState Ο†')) = + crPart (StateAlgebra.ofState Ο†) * crPart (StateAlgebra.ofState Ο†') := by + rw [normalOrder_crPart_mul] + conv_lhs => rw [← mul_one (crPart (StateAlgebra.ofState Ο†'))] + rw [normalOrder_crPart_mul, normalOrder_one] + simp + +@[simp] +lemma normalOrder_anPart_mul_anPart (Ο† Ο†' : 𝓕.States) : + normalOrder (anPart (StateAlgebra.ofState Ο†) * anPart (StateAlgebra.ofState Ο†')) = + anPart (StateAlgebra.ofState Ο†) * anPart (StateAlgebra.ofState Ο†') := by + rw [normalOrder_mul_anPart] + conv_lhs => rw [← one_mul (anPart (StateAlgebra.ofState Ο†))] + rw [normalOrder_mul_anPart, normalOrder_one] + simp + +@[simp] +lemma normalOrder_crPart_mul_anPart (Ο† Ο†' : 𝓕.States) : + normalOrder (crPart (StateAlgebra.ofState Ο†) * anPart (StateAlgebra.ofState Ο†')) = + crPart (StateAlgebra.ofState Ο†) * anPart (StateAlgebra.ofState Ο†') := by + rw [normalOrder_crPart_mul] + conv_lhs => rw [← one_mul (anPart (StateAlgebra.ofState Ο†'))] + rw [normalOrder_mul_anPart, normalOrder_one] + simp + +@[simp] +lemma normalOrder_anPart_mul_crPart (Ο† Ο†' : 𝓕.States) : + normalOrder (anPart (StateAlgebra.ofState Ο†) * crPart (StateAlgebra.ofState Ο†')) = + 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› Ο†') β€’ + (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 Ο†')))] + rw [← mul_assoc, normalOrder_swap_anPart_crPart] + simp + +lemma normalOrder_ofState_mul_ofState (Ο† Ο†' : 𝓕.States) : + normalOrder (ofState Ο† * ofState Ο†') = + crPart (StateAlgebra.ofState Ο†) * crPart (StateAlgebra.ofState Ο†') + + 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› Ο†') β€’ + (crPart (StateAlgebra.ofState Ο†') * anPart (StateAlgebra.ofState Ο†)) + + crPart (StateAlgebra.ofState Ο†) * anPart (StateAlgebra.ofState Ο†') + + anPart (StateAlgebra.ofState Ο†) * anPart (StateAlgebra.ofState Ο†') := by + rw [ofState_eq_crPart_add_anPart, ofState_eq_crPart_add_anPart] + rw [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] + abel + +/-! + +## Normal order with super commutors + +-/ + +/-! TODO: Split the following two lemmas up into smaller parts. -/ + lemma normalOrder_superCommute_ofCrAnList_create_create_ofCrAnList (Ο†c Ο†c' : 𝓕.CrAnStates) (hΟ†c : 𝓕 |>ᢜ Ο†c = CreateAnnihilate.create) (hΟ†c' : 𝓕 |>ᢜ Ο†c' = CreateAnnihilate.create) (Ο†s Ο†s' : List 𝓕.CrAnStates) : (normalOrder (ofCrAnList Ο†s * - superCommute (ofCrAnState Ο†c) (ofCrAnState Ο†c') * ofCrAnList Ο†s')) = + superCommute (ofCrAnState Ο†c) (ofCrAnState Ο†c') * ofCrAnList Ο†s')) = normalOrderSign (Ο†s ++ Ο†c' :: Ο†c :: Ο†s') β€’ (ofCrAnList (createFilter Ο†s) * superCommute (ofCrAnState Ο†c) (ofCrAnState Ο†c') * ofCrAnList (createFilter Ο†s') * ofCrAnList (annihilateFilter (Ο†s ++ Ο†s'))) := by - rw [superCommute_ofCrAnState] + rw [superCommute_ofCrAnState_ofCrAnState] rw [mul_sub, sub_mul, map_sub] conv_lhs => lhs @@ -372,7 +455,7 @@ lemma normalOrder_superCommute_ofCrAnList_annihilate_annihilate_ofCrAnList (ofCrAnList (createFilter (Ο†s ++ Ο†s')) * ofCrAnList (annihilateFilter Ο†s) * superCommute (ofCrAnState Ο†a) (ofCrAnState Ο†a') * ofCrAnList (annihilateFilter Ο†s')) := by - rw [superCommute_ofCrAnState] + rw [superCommute_ofCrAnState_ofCrAnState] rw [mul_sub, sub_mul, map_sub] conv_lhs => lhs @@ -440,62 +523,17 @@ lemma normalOrder_superCommute_ofCrAnList_annihilate_annihilate_ofCrAnList rw [ofCrAnList_append, ofCrAnList_singleton, ofCrAnList_singleton] rw [ofCrAnList_append, ofCrAnList_singleton, ofCrAnList_singleton, smul_mul_assoc] -@[simp] -lemma normalOrder_crPart_mul_crPart (Ο† Ο†' : 𝓕.States) : - normalOrder (crPart (StateAlgebra.ofState Ο†) * crPart (StateAlgebra.ofState Ο†')) = - crPart (StateAlgebra.ofState Ο†) * crPart (StateAlgebra.ofState Ο†') := by - rw [normalOrder_crPart_mul] - conv_lhs => rw [← mul_one (crPart (StateAlgebra.ofState Ο†'))] - rw [normalOrder_crPart_mul, normalOrder_one] - simp - -@[simp] -lemma normalOrder_anPart_mul_anPart (Ο† Ο†' : 𝓕.States) : - normalOrder (anPart (StateAlgebra.ofState Ο†) * anPart (StateAlgebra.ofState Ο†')) = - anPart (StateAlgebra.ofState Ο†) * anPart (StateAlgebra.ofState Ο†') := by - rw [normalOrder_mul_anPart] - conv_lhs => rw [← one_mul (anPart (StateAlgebra.ofState Ο†))] - rw [normalOrder_mul_anPart, normalOrder_one] - simp - -@[simp] -lemma normalOrder_crPart_mul_anPart (Ο† Ο†' : 𝓕.States) : - normalOrder (crPart (StateAlgebra.ofState Ο†) * anPart (StateAlgebra.ofState Ο†')) = - crPart (StateAlgebra.ofState Ο†) * anPart (StateAlgebra.ofState Ο†') := by - rw [normalOrder_crPart_mul] - conv_lhs => rw [← one_mul (anPart (StateAlgebra.ofState Ο†'))] - rw [normalOrder_mul_anPart, normalOrder_one] - simp +/-! -@[simp] -lemma normalOrder_anPart_mul_crPart (Ο† Ο†' : 𝓕.States) : - normalOrder (anPart (StateAlgebra.ofState Ο†) * crPart (StateAlgebra.ofState Ο†')) = - 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› Ο†') β€’ - (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 Ο†')))] - rw [← mul_assoc, normalOrder_swap_anPart_crPart] - simp +## Super commututators involving a normal order. -lemma normalOrder_ofState_mul_ofState (Ο† Ο†' : 𝓕.States) : - normalOrder (ofState Ο† * ofState Ο†') = - crPart (StateAlgebra.ofState Ο†) * crPart (StateAlgebra.ofState Ο†') + - 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› Ο†') β€’ - (crPart (StateAlgebra.ofState Ο†') * anPart (StateAlgebra.ofState Ο†)) + - crPart (StateAlgebra.ofState Ο†) * anPart (StateAlgebra.ofState Ο†') + - anPart (StateAlgebra.ofState Ο†) * anPart (StateAlgebra.ofState Ο†') := by - rw [ofState_eq_crPart_add_anPart, ofState_eq_crPart_add_anPart] - rw [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] - abel +-/ lemma ofCrAnList_superCommute_normalOrder_ofCrAnList (Ο†s Ο†s' : List 𝓕.CrAnStates) : ⟨ofCrAnList Ο†s, normalOrder (ofCrAnList Ο†s')βŸ©β‚›ca = ofCrAnList Ο†s * normalOrder (ofCrAnList Ο†s') - 𝓒(𝓕 |>β‚› Ο†s, 𝓕 |>β‚› Ο†s') β€’ normalOrder (ofCrAnList Ο†s') * ofCrAnList Ο†s := by - simp [normalOrder_ofCrAnList, map_smul, superCommute_ofCrAnList, ofCrAnList_append, + simp [normalOrder_ofCrAnList, map_smul, superCommute_ofCrAnList_ofCrAnList, ofCrAnList_append, smul_sub, smul_smul, mul_comm] lemma ofCrAnList_superCommute_normalOrder_ofStateList (Ο†s : List 𝓕.CrAnStates) @@ -509,6 +547,12 @@ lemma ofCrAnList_superCommute_normalOrder_ofStateList (Ο†s : List 𝓕.CrAnState rw [ofCrAnList_superCommute_normalOrder_ofCrAnList, CrAnSection.statistics_eq_state_statistics] +/-! + +## Multiplications with normal order written in terms of super commute. + +-/ + lemma ofCrAnList_mul_normalOrder_ofStateList_eq_superCommute (Ο†s : List 𝓕.CrAnStates) (Ο†s' : List 𝓕.States) : ofCrAnList Ο†s * normalOrder (ofStateList Ο†s') = diff --git a/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/SuperCommute.lean b/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/SuperCommute.lean index 605daaad..a2f2757d 100644 --- a/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/SuperCommute.lean +++ b/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/SuperCommute.lean @@ -37,11 +37,27 @@ noncomputable def superCommute : 𝓕.CrAnAlgebra β†’β‚—[β„‚] 𝓕.CrAnAlgebra whilst for two fermionic operators this corresponds to the anti-commutator. -/ scoped[FieldSpecification.CrAnAlgebra] notation "⟨" Ο†s "," Ο†s' "βŸ©β‚›ca" => superCommute Ο†s Ο†s' -lemma superCommute_ofCrAnList (Ο†s Ο†s' : List 𝓕.CrAnStates) : ⟨ofCrAnList Ο†s, ofCrAnList Ο†s'βŸ©β‚›ca = +/-! + +## The super commutor of different types of elements + +-/ + +lemma superCommute_ofCrAnList_ofCrAnList (Ο†s Ο†s' : List 𝓕.CrAnStates) : + ⟨ofCrAnList Ο†s, ofCrAnList Ο†s'βŸ©β‚›ca = ofCrAnList (Ο†s ++ Ο†s') - 𝓒(𝓕 |>β‚› Ο†s, 𝓕 |>β‚› Ο†s') β€’ ofCrAnList (Ο†s' ++ Ο†s) := by rw [← ofListBasis_eq_ofList, ← ofListBasis_eq_ofList] simp only [superCommute, Basis.constr_basis] +lemma superCommute_ofCrAnState_ofCrAnState (Ο† Ο†' : 𝓕.CrAnStates) : + ⟨ofCrAnState Ο†, ofCrAnState Ο†'βŸ©β‚›ca = + ofCrAnState Ο† * ofCrAnState Ο†' - 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› Ο†') β€’ ofCrAnState Ο†' * ofCrAnState Ο† := by + rw [← ofCrAnList_singleton, ← ofCrAnList_singleton] + rw [superCommute_ofCrAnList_ofCrAnList, ofCrAnList_append] + congr + rw [ofCrAnList_append] + rw [FieldStatistic.ofList_singleton, FieldStatistic.ofList_singleton, smul_mul_assoc] + lemma superCommute_ofCrAnList_ofStatesList (Ο†cas : List 𝓕.CrAnStates) (Ο†s : List 𝓕.States) : ⟨ofCrAnList Ο†cas, ofStateList Ο†sβŸ©β‚›ca = ofCrAnList Ο†cas * ofStateList Ο†s - 𝓒(𝓕 |>β‚› Ο†cas, 𝓕 |>β‚› Ο†s) β€’ ofStateList Ο†s * ofCrAnList Ο†cas := by @@ -49,7 +65,7 @@ lemma superCommute_ofCrAnList_ofStatesList (Ο†cas : List 𝓕.CrAnStates) (Ο†s : rw [map_sum] conv_lhs => enter [2, x] - rw [superCommute_ofCrAnList, CrAnSection.statistics_eq_state_statistics, + rw [superCommute_ofCrAnList_ofCrAnList, CrAnSection.statistics_eq_state_statistics, ofCrAnList_append, ofCrAnList_append] rw [Finset.sum_sub_distrib, ← Finset.mul_sum, ← Finset.smul_sum, ← Finset.sum_mul, ← ofStateList_sum] @@ -74,47 +90,16 @@ lemma superCommute_ofState_ofStatesList (Ο† : 𝓕.States) (Ο†s : List 𝓕.Stat rw [← ofStateList_singleton, superCommute_ofStateList_ofStatesList, ofStateList_singleton] simp -lemma superCommute_ofStateList_ofStates (Ο†s : List 𝓕.States) (Ο† : 𝓕.States) : +lemma superCommute_ofStateList_ofState (Ο†s : List 𝓕.States) (Ο† : 𝓕.States) : ⟨ofStateList Ο†s, ofState Ο†βŸ©β‚›ca = ofStateList Ο†s * ofState Ο† - 𝓒(𝓕 |>β‚› Ο†s, 𝓕 |>β‚› Ο†) β€’ ofState Ο† * ofStateList Ο†s := by rw [← ofStateList_singleton, superCommute_ofStateList_ofStatesList, ofStateList_singleton] simp -lemma ofCrAnList_mul_ofCrAnList_eq_superCommute (Ο†s Ο†s' : List 𝓕.CrAnStates) : - ofCrAnList Ο†s * ofCrAnList Ο†s' = 𝓒(𝓕 |>β‚› Ο†s, 𝓕 |>β‚› Ο†s') β€’ ofCrAnList Ο†s' * ofCrAnList Ο†s - + ⟨ofCrAnList Ο†s, ofCrAnList Ο†s'βŸ©β‚›ca := by - rw [superCommute_ofCrAnList] - simp [ofCrAnList_append] - -lemma ofCrAnState_mul_ofCrAnList_eq_superCommute (Ο† : 𝓕.CrAnStates) (Ο†s' : List 𝓕.CrAnStates) : - ofCrAnState Ο† * ofCrAnList Ο†s' = 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› Ο†s') β€’ ofCrAnList Ο†s' * ofCrAnState Ο† - + ⟨ofCrAnState Ο†, ofCrAnList Ο†s'βŸ©β‚›ca := by - rw [← ofCrAnList_singleton, ofCrAnList_mul_ofCrAnList_eq_superCommute] - simp - -lemma ofStateList_mul_ofStateList_eq_superCommute (Ο†s Ο†s' : List 𝓕.States) : - ofStateList Ο†s * ofStateList Ο†s' = 𝓒(𝓕 |>β‚› Ο†s, 𝓕 |>β‚› Ο†s') β€’ ofStateList Ο†s' * ofStateList Ο†s - + ⟨ofStateList Ο†s, ofStateList Ο†s'βŸ©β‚›ca := by - rw [superCommute_ofStateList_ofStatesList] - simp - -lemma ofState_mul_ofStateList_eq_superCommute (Ο† : 𝓕.States) (Ο†s' : List 𝓕.States) : - ofState Ο† * ofStateList Ο†s' = 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› Ο†s') β€’ ofStateList Ο†s' * ofState Ο† - + ⟨ofState Ο†, ofStateList Ο†s'βŸ©β‚›ca := by - rw [superCommute_ofState_ofStatesList] - simp - -lemma ofStateList_mul_ofState_eq_superCommute (Ο†s : List 𝓕.States) (Ο† : 𝓕.States) : - ofStateList Ο†s * ofState Ο† = 𝓒(𝓕 |>β‚› Ο†s, 𝓕 |>β‚› Ο†) β€’ ofState Ο† * ofStateList Ο†s - + ⟨ofStateList Ο†s, ofState Ο†βŸ©β‚›ca := by - rw [superCommute_ofStateList_ofStates] - 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 + 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› Ο†') β€’ crPart (StateAlgebra.ofState Ο†') * anPart (StateAlgebra.ofState Ο†) := by match Ο†, Ο†' with | States.negAsymp Ο†, _ => simp @@ -123,21 +108,21 @@ lemma superCommute_anPart_crPart (Ο† Ο†' : 𝓕.States) : sub_self] | States.position Ο†, States.position Ο†' => simp only [anPart_position, crPart_position, instCommGroup.eq_1, Algebra.smul_mul_assoc] - rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, superCommute_ofCrAnList] + rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, superCommute_ofCrAnList_ofCrAnList] simp [crAnStatistics, ← ofCrAnList_append] | States.posAsymp Ο†, States.position Ο†' => simp only [anPart_posAsymp, crPart_position, instCommGroup.eq_1, Algebra.smul_mul_assoc] - rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, superCommute_ofCrAnList] + rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, superCommute_ofCrAnList_ofCrAnList] simp [crAnStatistics, ← ofCrAnList_append] | States.position Ο†, States.negAsymp Ο†' => simp only [anPart_position, crPart_negAsymp, instCommGroup.eq_1, Algebra.smul_mul_assoc] - rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, superCommute_ofCrAnList] + rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, superCommute_ofCrAnList_ofCrAnList] simp only [List.singleton_append, instCommGroup.eq_1, crAnStatistics, FieldStatistic.ofList_singleton, Function.comp_apply, crAnStatesToStates_prod, ← ofCrAnList_append] | States.posAsymp Ο†, States.negAsymp Ο†' => simp only [anPart_posAsymp, crPart_negAsymp, instCommGroup.eq_1, Algebra.smul_mul_assoc] - rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, superCommute_ofCrAnList] + rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, superCommute_ofCrAnList_ofCrAnList] simp [crAnStatistics, ← ofCrAnList_append] lemma superCommute_crPart_anPart (Ο† Ο†' : 𝓕.States) : @@ -154,19 +139,19 @@ lemma superCommute_crPart_anPart (Ο† Ο†' : 𝓕.States) : sub_self] | States.position Ο†, States.position Ο†' => simp only [crPart_position, anPart_position, instCommGroup.eq_1, Algebra.smul_mul_assoc] - rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, superCommute_ofCrAnList] + rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, superCommute_ofCrAnList_ofCrAnList] simp [crAnStatistics, ← ofCrAnList_append] | States.position Ο†, States.posAsymp Ο†' => simp only [crPart_position, anPart_posAsymp, instCommGroup.eq_1, Algebra.smul_mul_assoc] - rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, superCommute_ofCrAnList] + rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, superCommute_ofCrAnList_ofCrAnList] simp [crAnStatistics, ← ofCrAnList_append] | States.negAsymp Ο†, States.position Ο†' => simp only [crPart_negAsymp, anPart_position, instCommGroup.eq_1, Algebra.smul_mul_assoc] - rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, superCommute_ofCrAnList] + rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, superCommute_ofCrAnList_ofCrAnList] simp [crAnStatistics, ← ofCrAnList_append] | States.negAsymp Ο†, States.posAsymp Ο†' => simp only [crPart_negAsymp, anPart_posAsymp, instCommGroup.eq_1, Algebra.smul_mul_assoc] - rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, superCommute_ofCrAnList] + rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, superCommute_ofCrAnList_ofCrAnList] simp [crAnStatistics, ← ofCrAnList_append] lemma superCommute_crPart_crPart (Ο† Ο†' : 𝓕.States) : @@ -182,19 +167,19 @@ lemma superCommute_crPart_crPart (Ο† Ο†' : 𝓕.States) : simp only [crPart_posAsymp, map_zero, mul_zero, instCommGroup.eq_1, smul_zero, zero_mul, sub_self] | States.position Ο†, States.position Ο†' => simp only [crPart_position, instCommGroup.eq_1, Algebra.smul_mul_assoc] - rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, superCommute_ofCrAnList] + rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, superCommute_ofCrAnList_ofCrAnList] simp [crAnStatistics, ← ofCrAnList_append] | States.position Ο†, States.negAsymp Ο†' => simp only [crPart_position, crPart_negAsymp, instCommGroup.eq_1, Algebra.smul_mul_assoc] - rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, superCommute_ofCrAnList] + rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, superCommute_ofCrAnList_ofCrAnList] simp [crAnStatistics, ← ofCrAnList_append] | States.negAsymp Ο†, States.position Ο†' => simp only [crPart_negAsymp, crPart_position, instCommGroup.eq_1, Algebra.smul_mul_assoc] - rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, superCommute_ofCrAnList] + rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, superCommute_ofCrAnList_ofCrAnList] simp [crAnStatistics, ← ofCrAnList_append] | States.negAsymp Ο†, States.negAsymp Ο†' => simp only [crPart_negAsymp, instCommGroup.eq_1, Algebra.smul_mul_assoc] - rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, superCommute_ofCrAnList] + rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, superCommute_ofCrAnList_ofCrAnList] simp [crAnStatistics, ← ofCrAnList_append] lemma superCommute_anPart_anPart (Ο† Ο†' : 𝓕.States) : @@ -209,54 +194,22 @@ lemma superCommute_anPart_anPart (Ο† Ο†' : 𝓕.States) : simp | States.position Ο†, States.position Ο†' => simp only [anPart_position, instCommGroup.eq_1, Algebra.smul_mul_assoc] - rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, superCommute_ofCrAnList] + rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, superCommute_ofCrAnList_ofCrAnList] simp [crAnStatistics, ← ofCrAnList_append] | States.position Ο†, States.posAsymp Ο†' => simp only [anPart_position, anPart_posAsymp, instCommGroup.eq_1, Algebra.smul_mul_assoc] - rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, superCommute_ofCrAnList] + rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, superCommute_ofCrAnList_ofCrAnList] simp [crAnStatistics, ← ofCrAnList_append] | States.posAsymp Ο†, States.position Ο†' => simp only [anPart_posAsymp, anPart_position, instCommGroup.eq_1, Algebra.smul_mul_assoc] - rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, superCommute_ofCrAnList] + rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, superCommute_ofCrAnList_ofCrAnList] simp [crAnStatistics, ← ofCrAnList_append] | States.posAsymp Ο†, States.posAsymp Ο†' => simp only [anPart_posAsymp, instCommGroup.eq_1, Algebra.smul_mul_assoc] - rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, superCommute_ofCrAnList] + rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, superCommute_ofCrAnList_ofCrAnList] simp [crAnStatistics, ← ofCrAnList_append] -lemma crPart_anPart_eq_superCommute (Ο† Ο†' : 𝓕.States) : - crPart (StateAlgebra.ofState Ο†) * anPart (StateAlgebra.ofState Ο†') = - 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› Ο†') β€’ - anPart (StateAlgebra.ofState Ο†') * crPart (StateAlgebra.ofState Ο†) + - ⟨crPart (StateAlgebra.ofState Ο†), anPart (StateAlgebra.ofState Ο†')βŸ©β‚›ca := by - rw [superCommute_crPart_anPart] - simp - -lemma anPart_crPart_eq_superCommute (Ο† Ο†' : 𝓕.States) : - anPart (StateAlgebra.ofState Ο†) * crPart (StateAlgebra.ofState Ο†') = - 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› Ο†') β€’ - crPart (StateAlgebra.ofState Ο†') * anPart (StateAlgebra.ofState Ο†) + - ⟨anPart (StateAlgebra.ofState Ο†), crPart (StateAlgebra.ofState Ο†')βŸ©β‚›ca := by - rw [superCommute_anPart_crPart] - simp - -lemma crPart_crPart_eq_superCommute (Ο† Ο†' : 𝓕.States) : - crPart (StateAlgebra.ofState Ο†) * crPart (StateAlgebra.ofState Ο†') = - 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› Ο†') β€’ - crPart (StateAlgebra.ofState Ο†') * crPart (StateAlgebra.ofState Ο†) + - ⟨crPart (StateAlgebra.ofState Ο†), crPart (StateAlgebra.ofState Ο†')βŸ©β‚›ca := by - rw [superCommute_crPart_crPart] - simp - -lemma anPart_anPart_eq_superCommute (Ο† Ο†' : 𝓕.States) : - anPart (StateAlgebra.ofState Ο†) * anPart (StateAlgebra.ofState Ο†') = - 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› Ο†') β€’ - anPart (StateAlgebra.ofState Ο†') * anPart (StateAlgebra.ofState Ο†) + - ⟨anPart (StateAlgebra.ofState Ο†), anPart (StateAlgebra.ofState Ο†')βŸ©β‚›ca := by - rw [superCommute_anPart_anPart] - simp - -lemma superCommute_crPart_ofStatesList (Ο† : 𝓕.States) (Ο†s : List 𝓕.States) : +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 @@ -272,7 +225,7 @@ lemma superCommute_crPart_ofStatesList (Ο† : 𝓕.States) (Ο†s : List 𝓕.State | States.posAsymp Ο† => simp -lemma superCommute_anPart_ofStatesList (Ο† : 𝓕.States) (Ο†s : List 𝓕.States) : +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 @@ -291,32 +244,100 @@ lemma superCommute_anPart_ofStatesList (Ο† : 𝓕.States) (Ο†s : List 𝓕.State lemma superCommute_crPart_ofState (Ο† Ο†' : 𝓕.States) : ⟨crPart (StateAlgebra.ofState Ο†), ofState Ο†'βŸ©β‚›ca = crPart (StateAlgebra.ofState Ο†) * ofState Ο†' - - 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› Ο†') β€’ - ofState Ο†' * crPart (StateAlgebra.ofState Ο†) := by - rw [← ofStateList_singleton, superCommute_crPart_ofStatesList] + 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› Ο†') β€’ ofState Ο†' * crPart (StateAlgebra.ofState Ο†) := 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 + rw [← ofStateList_singleton, superCommute_anPart_ofStateList] + simp + +/-! + +## Mul equal superCommute + +Lemmas which rewrite a multiplication of two elements of the algebra as their commuted +multiplication with a sign plus the super commutor. + +-/ +lemma ofCrAnList_mul_ofCrAnList_eq_superCommute (Ο†s Ο†s' : List 𝓕.CrAnStates) : + ofCrAnList Ο†s * ofCrAnList Ο†s' = 𝓒(𝓕 |>β‚› Ο†s, 𝓕 |>β‚› Ο†s') β€’ ofCrAnList Ο†s' * ofCrAnList Ο†s + + ⟨ofCrAnList Ο†s, ofCrAnList Ο†s'βŸ©β‚›ca := by + rw [superCommute_ofCrAnList_ofCrAnList] + simp [ofCrAnList_append] + +lemma ofCrAnState_mul_ofCrAnList_eq_superCommute (Ο† : 𝓕.CrAnStates) (Ο†s' : List 𝓕.CrAnStates) : + ofCrAnState Ο† * ofCrAnList Ο†s' = 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› Ο†s') β€’ ofCrAnList Ο†s' * ofCrAnState Ο† + + ⟨ofCrAnState Ο†, ofCrAnList Ο†s'βŸ©β‚›ca := by + rw [← ofCrAnList_singleton, ofCrAnList_mul_ofCrAnList_eq_superCommute] + simp + +lemma ofStateList_mul_ofStateList_eq_superCommute (Ο†s Ο†s' : List 𝓕.States) : + ofStateList Ο†s * ofStateList Ο†s' = 𝓒(𝓕 |>β‚› Ο†s, 𝓕 |>β‚› Ο†s') β€’ ofStateList Ο†s' * ofStateList Ο†s + + ⟨ofStateList Ο†s, ofStateList Ο†s'βŸ©β‚›ca := by + rw [superCommute_ofStateList_ofStatesList] + simp + +lemma ofState_mul_ofStateList_eq_superCommute (Ο† : 𝓕.States) (Ο†s' : List 𝓕.States) : + ofState Ο† * ofStateList Ο†s' = 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› Ο†s') β€’ ofStateList Ο†s' * ofState Ο† + + ⟨ofState Ο†, ofStateList Ο†s'βŸ©β‚›ca := by + rw [superCommute_ofState_ofStatesList] + simp + +lemma ofStateList_mul_ofState_eq_superCommute (Ο†s : List 𝓕.States) (Ο† : 𝓕.States) : + ofStateList Ο†s * ofState Ο† = 𝓒(𝓕 |>β‚› Ο†s, 𝓕 |>β‚› Ο†) β€’ ofState Ο† * ofStateList Ο†s + + ⟨ofStateList Ο†s, ofState Ο†βŸ©β‚›ca := by + rw [superCommute_ofStateList_ofState] + 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 + rw [superCommute_crPart_anPart] + simp + +lemma anPart_mul_crPart_eq_superCommute (Ο† Ο†' : 𝓕.States) : + anPart (StateAlgebra.ofState Ο†) * crPart (StateAlgebra.ofState Ο†') = 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› Ο†') β€’ - ofState Ο†' * anPart (StateAlgebra.ofState Ο†) := by - rw [← ofStateList_singleton, superCommute_anPart_ofStatesList] + crPart (StateAlgebra.ofState Ο†') * anPart (StateAlgebra.ofState Ο†) + + ⟨anPart (StateAlgebra.ofState Ο†), crPart (StateAlgebra.ofState Ο†')βŸ©β‚›ca := by + rw [superCommute_anPart_crPart] simp -lemma superCommute_ofCrAnState (Ο† Ο†' : 𝓕.CrAnStates) : ⟨ofCrAnState Ο†, ofCrAnState Ο†'βŸ©β‚›ca = - ofCrAnState Ο† * ofCrAnState Ο†' - 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› Ο†') β€’ ofCrAnState Ο†' * ofCrAnState Ο† := by - rw [← ofCrAnList_singleton, ← ofCrAnList_singleton] - rw [superCommute_ofCrAnList, ofCrAnList_append] - congr - rw [ofCrAnList_append] - rw [FieldStatistic.ofList_singleton, FieldStatistic.ofList_singleton, smul_mul_assoc] +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 + 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 + rw [superCommute_anPart_anPart] + simp + +lemma ofCrAnList_mul_ofStateList_eq_superCommute (Ο†s : List 𝓕.CrAnStates) (Ο†s' : List 𝓕.States) : + ofCrAnList Ο†s * ofStateList Ο†s' = 𝓒(𝓕 |>β‚› Ο†s, 𝓕 |>β‚› Ο†s') β€’ ofStateList Ο†s' * ofCrAnList Ο†s + + ⟨ofCrAnList Ο†s, ofStateList Ο†s'βŸ©β‚›ca := by + rw [superCommute_ofCrAnList_ofStatesList] + simp + +/-! -lemma superCommute_ofCrAnList_symm (Ο†s Ο†s' : List 𝓕.CrAnStates) : +## Symmetry of the super commutor. + +-/ + +lemma superCommute_ofCrAnList_ofCrAnList_symm (Ο†s Ο†s' : List 𝓕.CrAnStates) : ⟨ofCrAnList Ο†s, ofCrAnList Ο†s'βŸ©β‚›ca = - (- 𝓒(𝓕 |>β‚› Ο†s, 𝓕 |>β‚› Ο†s')) β€’ - ⟨ofCrAnList Ο†s', ofCrAnList Ο†sβŸ©β‚›ca := by - rw [superCommute_ofCrAnList, superCommute_ofCrAnList, smul_sub] + (- 𝓒(𝓕 |>β‚› Ο†s, 𝓕 |>β‚› Ο†s')) β€’ ⟨ofCrAnList Ο†s', ofCrAnList Ο†sβŸ©β‚›ca := by + rw [superCommute_ofCrAnList_ofCrAnList, superCommute_ofCrAnList_ofCrAnList, smul_sub] simp only [instCommGroup.eq_1, neg_smul, sub_neg_eq_add] rw [smul_smul] conv_rhs => @@ -325,10 +346,10 @@ lemma superCommute_ofCrAnList_symm (Ο†s Ο†s' : List 𝓕.CrAnStates) : simp only [one_smul] abel -lemma superCommute_ofCrAnState_symm (Ο† Ο†' : 𝓕.CrAnStates) : +lemma superCommute_ofCrAnState_ofCrAnState_symm (Ο† Ο†' : 𝓕.CrAnStates) : ⟨ofCrAnState Ο†, ofCrAnState Ο†'βŸ©β‚›ca = (- 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› Ο†')) β€’ ⟨ofCrAnState Ο†', ofCrAnState Ο†βŸ©β‚›ca := by - rw [superCommute_ofCrAnState, superCommute_ofCrAnState] + rw [superCommute_ofCrAnState_ofCrAnState, superCommute_ofCrAnState_ofCrAnState] rw [smul_sub] simp only [instCommGroup.eq_1, Algebra.smul_mul_assoc, neg_smul, sub_neg_eq_add] rw [smul_smul] @@ -338,21 +359,26 @@ lemma superCommute_ofCrAnState_symm (Ο† Ο†' : 𝓕.CrAnStates) : simp only [one_smul] abel +/-! + +## Splitting the super commutor on lists into sums. + +-/ lemma superCommute_ofCrAnList_ofCrAnList_cons (Ο† : 𝓕.CrAnStates) (Ο†s Ο†s' : List 𝓕.CrAnStates) : ⟨ofCrAnList Ο†s, ofCrAnList (Ο† :: Ο†s')βŸ©β‚›ca = ⟨ofCrAnList Ο†s, ofCrAnState Ο†βŸ©β‚›ca * ofCrAnList Ο†s' + 𝓒(𝓕 |>β‚› Ο†s, 𝓕 |>β‚› Ο†) β€’ ofCrAnState Ο† * ⟨ofCrAnList Ο†s, ofCrAnList Ο†s'βŸ©β‚›ca := by - rw [superCommute_ofCrAnList] + rw [superCommute_ofCrAnList_ofCrAnList] conv_rhs => lhs - rw [← ofCrAnList_singleton, superCommute_ofCrAnList, sub_mul, ← ofCrAnList_append] + rw [← ofCrAnList_singleton, superCommute_ofCrAnList_ofCrAnList, sub_mul, ← ofCrAnList_append] rhs rw [FieldStatistic.ofList_singleton, ofCrAnList_append, ofCrAnList_singleton, smul_mul_assoc, mul_assoc, ← ofCrAnList_append] conv_rhs => rhs - rw [superCommute_ofCrAnList, mul_sub, smul_mul_assoc] + rw [superCommute_ofCrAnList_ofCrAnList, mul_sub, smul_mul_assoc] simp only [instCommGroup.eq_1, List.cons_append, List.append_assoc, List.nil_append, Algebra.mul_smul_comm, Algebra.smul_mul_assoc, sub_add_sub_cancel, sub_right_inj] rw [← ofCrAnList_cons, smul_smul, FieldStatistic.ofList_cons_eq_mul] @@ -378,12 +404,6 @@ lemma superCommute_ofCrAnList_ofStateList_cons (Ο† : 𝓕.States) (Ο†s : List rw [ofStateList_cons, mul_assoc, smul_smul, FieldStatistic.ofList_cons_eq_mul] simp [mul_comm] -lemma ofCrAnList_mul_ofStateList_eq_superCommute (Ο†s : List 𝓕.CrAnStates) (Ο†s' : List 𝓕.States) : - ofCrAnList Ο†s * ofStateList Ο†s' = 𝓒(𝓕 |>β‚› Ο†s, 𝓕 |>β‚› Ο†s') β€’ ofStateList Ο†s' * ofCrAnList Ο†s - + ⟨ofCrAnList Ο†s, ofStateList Ο†s'βŸ©β‚›ca := by - rw [superCommute_ofCrAnList_ofStatesList] - simp - lemma superCommute_ofCrAnList_ofCrAnList_eq_sum (Ο†s : List 𝓕.CrAnStates) : (Ο†s' : List 𝓕.CrAnStates) β†’ ⟨ofCrAnList Ο†s, ofCrAnList Ο†s'βŸ©β‚›ca = @@ -391,7 +411,7 @@ lemma superCommute_ofCrAnList_ofCrAnList_eq_sum (Ο†s : List 𝓕.CrAnStates) : ofCrAnList (Ο†s'.take n) * ⟨ofCrAnList Ο†s, ofCrAnState (Ο†s'.get n)βŸ©β‚›ca * ofCrAnList (Ο†s'.drop (n + 1)) | [] => by - simp [← ofCrAnList_nil, superCommute_ofCrAnList] + simp [← ofCrAnList_nil, superCommute_ofCrAnList_ofCrAnList] | Ο† :: Ο†s' => by rw [superCommute_ofCrAnList_ofCrAnList_cons, superCommute_ofCrAnList_ofCrAnList_eq_sum Ο†s Ο†s'] conv_rhs => erw [Fin.sum_univ_succ] @@ -400,8 +420,7 @@ lemma superCommute_ofCrAnList_ofCrAnList_eq_sum (Ο†s : List 𝓕.CrAnStates) : Β· simp [Finset.mul_sum, smul_smul, ofCrAnList_cons, mul_assoc, FieldStatistic.ofList_cons_eq_mul, mul_comm] -lemma superCommute_ofCrAnList_ofStateList_eq_sum (Ο†s : List 𝓕.CrAnStates) : - (Ο†s' : List 𝓕.States) β†’ +lemma superCommute_ofCrAnList_ofStateList_eq_sum (Ο†s : List 𝓕.CrAnStates) : (Ο†s' : List 𝓕.States) β†’ ⟨ofCrAnList Ο†s, ofStateList Ο†s'βŸ©β‚›ca = βˆ‘ (n : Fin Ο†s'.length), 𝓒(𝓕 |>β‚› Ο†s, 𝓕 |>β‚› List.take n Ο†s') β€’ ofStateList (Ο†s'.take n) * ⟨ofCrAnList Ο†s, ofState (Ο†s'.get n)βŸ©β‚›ca * diff --git a/HepLean/PerturbationTheory/Algebras/OperatorAlgebra/Basic.lean b/HepLean/PerturbationTheory/Algebras/ProtoOperatorAlgebra/Basic.lean similarity index 97% rename from HepLean/PerturbationTheory/Algebras/OperatorAlgebra/Basic.lean rename to HepLean/PerturbationTheory/Algebras/ProtoOperatorAlgebra/Basic.lean index 47aada6b..db2709d7 100644 --- a/HepLean/PerturbationTheory/Algebras/OperatorAlgebra/Basic.lean +++ b/HepLean/PerturbationTheory/Algebras/ProtoOperatorAlgebra/Basic.lean @@ -18,7 +18,7 @@ open CrAnAlgebra to be isomorphic to the actual operator algebra of a field theory. These properties are sufficent to prove certain theorems about the Operator algebra in particular Wick's theorem. -/ -structure OperatorAlgebra where +structure ProtoOperatorAlgebra where /-- The algebra representing the operator algebra. -/ A : Type /-- The instance of the type `A` as a semi-ring. -/ @@ -43,9 +43,9 @@ structure OperatorAlgebra where (_ : Β¬ (𝓕 |>β‚› Ο†) = (𝓕 |>β‚› Ο†')), crAnF (superCommute (ofCrAnState Ο†) (ofCrAnState Ο†')) = 0 -namespace OperatorAlgebra +namespace ProtoOperatorAlgebra open FieldStatistic -variable {𝓕 : FieldSpecification} (π“ž : 𝓕.OperatorAlgebra) +variable {𝓕 : FieldSpecification} (π“ž : 𝓕.ProtoOperatorAlgebra) /-- The algebra `π“ž.A` carries the instance of a semi-ring induced via `A_seimRing`. -/ instance : Semiring π“ž.A := π“ž.A_semiRing @@ -198,5 +198,5 @@ lemma crAnF_superCommute_ofCrAnState_ofStateList_eq_sum (Ο† : 𝓕.CrAnStates) ( Β· congr rw [← map_mul, ← ofStateList_append, ← List.eraseIdx_eq_take_drop_succ] -end OperatorAlgebra +end ProtoOperatorAlgebra end FieldSpecification diff --git a/HepLean/PerturbationTheory/Algebras/OperatorAlgebra/NormalOrder.lean b/HepLean/PerturbationTheory/Algebras/ProtoOperatorAlgebra/NormalOrder.lean similarity index 94% rename from HepLean/PerturbationTheory/Algebras/OperatorAlgebra/NormalOrder.lean rename to HepLean/PerturbationTheory/Algebras/ProtoOperatorAlgebra/NormalOrder.lean index 97fdc6c7..0c5a5382 100644 --- a/HepLean/PerturbationTheory/Algebras/OperatorAlgebra/NormalOrder.lean +++ b/HepLean/PerturbationTheory/Algebras/ProtoOperatorAlgebra/NormalOrder.lean @@ -14,11 +14,19 @@ import HepLean.PerturbationTheory.Koszul.KoszulSign namespace FieldSpecification variable {𝓕 : FieldSpecification} -namespace OperatorAlgebra -variable {π“ž : OperatorAlgebra 𝓕} +namespace ProtoOperatorAlgebra +variable {π“ž : ProtoOperatorAlgebra 𝓕} open CrAnAlgebra open FieldStatistic +/-! + +## Normal order of super-commutators. + +The main result of this section is +`crAnF_normalOrder_superCommute_eq_zero_mul`. + +-/ lemma crAnF_normalOrder_superCommute_ofCrAnList_create_create_ofCrAnList (Ο†c Ο†c' : 𝓕.CrAnStates) (hΟ†c : 𝓕 |>ᢜ Ο†c = CreateAnnihilate.create) @@ -111,7 +119,7 @@ lemma crAnF_normalOrder_superCommute_ofCrAnList_ofCrAnState_eq_zero_mul (Ο†a : (Ο†s : List 𝓕.CrAnStates) (a b : 𝓕.CrAnAlgebra) : π“ž.crAnF (normalOrder (a * superCommute (ofCrAnList Ο†s) (ofCrAnState Ο†a) * b)) = 0 := by - rw [← ofCrAnList_singleton, superCommute_ofCrAnList_symm, ofCrAnList_singleton] + rw [← ofCrAnList_singleton, superCommute_ofCrAnList_ofCrAnList_symm, ofCrAnList_singleton] simp only [FieldStatistic.instCommGroup.eq_1, FieldStatistic.ofList_singleton, mul_neg, Algebra.mul_smul_comm, neg_mul, Algebra.smul_mul_assoc, map_neg, map_smul] rw [crAnF_normalOrder_superCommute_ofCrAnState_ofCrAnList_eq_zero_mul] @@ -180,27 +188,18 @@ lemma crAnF_normalOrder_superCommute_eq_zero rw [← crAnF_normalOrder_superCommute_eq_zero_mul 1 1 c d] simp +/-! + +## Swapping terms in a normal order. + +-/ + lemma crAnF_normalOrder_ofState_ofState_swap (Ο† Ο†' : 𝓕.States) : π“ž.crAnF (normalOrder (ofState Ο† * ofState Ο†')) = - 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› Ο†') β€’ - π“ž.crAnF (normalOrder (ofState Ο†' * ofState Ο†)) := by - conv_lhs => - rhs - rhs - rw [ofState_eq_crPart_add_anPart, ofState_eq_crPart_add_anPart] - rw [mul_add, add_mul, add_mul] - rw [crPart_crPart_eq_superCommute, crPart_anPart_eq_superCommute, - anPart_anPart_eq_superCommute, anPart_crPart_eq_superCommute] - simp only [FieldStatistic.instCommGroup.eq_1, Algebra.smul_mul_assoc, map_add, map_smul, - normalOrder_crPart_mul_crPart, normalOrder_crPart_mul_anPart, normalOrder_anPart_mul_crPart, - normalOrder_anPart_mul_anPart, map_mul, crAnF_normalOrder_superCommute_eq_zero, add_zero] - rw [normalOrder_ofState_mul_ofState] - simp only [FieldStatistic.instCommGroup.eq_1, map_add, map_mul, map_smul, smul_add] - rw [smul_smul] - simp only [FieldStatistic.exchangeSign_mul_self_swap, one_smul] - abel - -open FieldStatistic + 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› Ο†') β€’ π“ž.crAnF (normalOrder (ofState Ο†' * ofState Ο†)) := by + rw [← ofStateList_singleton, ← ofStateList_singleton, + ofStateList_mul_ofStateList_eq_superCommute] + simp lemma crAnF_normalOrder_ofCrAnState_ofCrAnList_swap (Ο† : 𝓕.CrAnStates) (Ο†s : List 𝓕.CrAnStates) : @@ -249,6 +248,11 @@ lemma crAnF_normalOrder_ofStatesList_mul_anPart_swap (Ο† : 𝓕.States) rw [← normalOrder_mul_anPart] rw [crAnF_normalOrder_ofStatesList_anPart_swap] +/-! + +## Super commutators with a normal ordered term as sums + +-/ lemma crAnF_ofCrAnState_superCommute_normalOrder_ofCrAnList_eq_sum (Ο† : 𝓕.CrAnStates) (Ο†s : List 𝓕.CrAnStates) : π“ž.crAnF (⟨ofCrAnState Ο†, normalOrder (ofCrAnList Ο†s)βŸ©β‚›ca) = βˆ‘ n : Fin Ο†s.length, 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› (Ο†s.take n)) β€’ @@ -316,6 +320,11 @@ lemma crAnF_anPart_superCommute_normalOrder_ofStateList_eq_sum (Ο† : 𝓕.States rw [crAnF_ofCrAnState_superCommute_normalOrder_ofStateList_eq_sum] simp [crAnStatistics] +/-! + +## Multiplying with normal ordered terms + +-/ lemma crAnF_anPart_mul_normalOrder_ofStatesList_eq_superCommute (Ο† : 𝓕.States) (Ο†' : List 𝓕.States) : π“ž.crAnF (anPart (StateAlgebra.ofState Ο†) * normalOrder (ofStateList Ο†')) = @@ -359,6 +368,12 @@ lemma crAnF_ofState_mul_normalOrder_ofStatesList_eq_sum (Ο† : 𝓕.States) Fintype.sum_option, one_mul] rfl +/-! + +## Cons vs insertIdx for a normal ordered term. + +-/ + lemma crAnF_ofState_normalOrder_insert (Ο† : 𝓕.States) (Ο†s : List 𝓕.States) (k : Fin Ο†s.length.succ) : π“ž.crAnF (normalOrder (ofStateList (Ο† :: Ο†s))) = @@ -375,6 +390,6 @@ lemma crAnF_ofState_normalOrder_insert (Ο† : 𝓕.States) (Ο†s : List 𝓕.State rw [← ofStateList_append, ← ofStateList_append] simp -end OperatorAlgebra +end ProtoOperatorAlgebra end FieldSpecification diff --git a/HepLean/PerturbationTheory/Algebras/OperatorAlgebra/TimeContraction.lean b/HepLean/PerturbationTheory/Algebras/ProtoOperatorAlgebra/TimeContraction.lean similarity index 95% rename from HepLean/PerturbationTheory/Algebras/OperatorAlgebra/TimeContraction.lean rename to HepLean/PerturbationTheory/Algebras/ProtoOperatorAlgebra/TimeContraction.lean index 7c9be942..b854bd89 100644 --- a/HepLean/PerturbationTheory/Algebras/OperatorAlgebra/TimeContraction.lean +++ b/HepLean/PerturbationTheory/Algebras/ProtoOperatorAlgebra/TimeContraction.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.OperatorAlgebra.NormalOrder +import HepLean.PerturbationTheory.Algebras.ProtoOperatorAlgebra.NormalOrder import HepLean.PerturbationTheory.Algebras.StateAlgebra.TimeOrder /-! @@ -19,9 +19,9 @@ variable {𝓕 : FieldSpecification} open CrAnAlgebra noncomputable section -namespace OperatorAlgebra +namespace ProtoOperatorAlgebra -variable (π“ž : 𝓕.OperatorAlgebra) +variable (π“ž : 𝓕.ProtoOperatorAlgebra) open FieldStatistic /-- The time contraction of two States as an element of `π“ž.A` defined @@ -86,7 +86,7 @@ lemma timeContract_zero_of_diff_grade (Ο† ψ : 𝓕.States) (h : (𝓕 |>β‚› Ο†) have ht := IsTotal.total (r := 𝓕.timeOrderRel) Ο† ψ simp_all -end OperatorAlgebra +end ProtoOperatorAlgebra end end FieldSpecification diff --git a/HepLean/PerturbationTheory/Algebras/StateAlgebra/Basic.lean b/HepLean/PerturbationTheory/Algebras/StateAlgebra/Basic.lean index c8a3d8a4..124d94e9 100644 --- a/HepLean/PerturbationTheory/Algebras/StateAlgebra/Basic.lean +++ b/HepLean/PerturbationTheory/Algebras/StateAlgebra/Basic.lean @@ -13,8 +13,7 @@ generated by these states. We call this the state algebra, or the state free-alg The state free-algebra has minimal assumptions, yet can be used to concretely define time-ordering. -In -`HepLean.PerturbationTheory.Algebras.CrAnAlgebra.Basic` +In `HepLean.PerturbationTheory.Algebras.CrAnAlgebra.Basic` we defined a related free-algebra generated by creation and annihilation states. -/ diff --git a/HepLean/PerturbationTheory/FieldSpecification/Examples.lean b/HepLean/PerturbationTheory/FieldSpecification/Examples.lean index dfb714cb..c93cbbb6 100644 --- a/HepLean/PerturbationTheory/FieldSpecification/Examples.lean +++ b/HepLean/PerturbationTheory/FieldSpecification/Examples.lean @@ -8,7 +8,6 @@ import HepLean.PerturbationTheory.FieldSpecification.Basic # Specific examples of field specifications - -/ namespace FieldSpecification diff --git a/HepLean/PerturbationTheory/FieldSpecification/Filters.lean b/HepLean/PerturbationTheory/FieldSpecification/Filters.lean index 4ce9bfff..b4316c85 100644 --- a/HepLean/PerturbationTheory/FieldSpecification/Filters.lean +++ b/HepLean/PerturbationTheory/FieldSpecification/Filters.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.OperatorAlgebra.Basic +import HepLean.PerturbationTheory.Algebras.ProtoOperatorAlgebra.Basic import HepLean.PerturbationTheory.Koszul.KoszulSign /-! diff --git a/HepLean/PerturbationTheory/FieldSpecification/NormalOrder.lean b/HepLean/PerturbationTheory/FieldSpecification/NormalOrder.lean index 4d631279..9bdacdf0 100644 --- a/HepLean/PerturbationTheory/FieldSpecification/NormalOrder.lean +++ b/HepLean/PerturbationTheory/FieldSpecification/NormalOrder.lean @@ -3,15 +3,13 @@ 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.OperatorAlgebra.Basic +import HepLean.PerturbationTheory.Algebras.ProtoOperatorAlgebra.Basic import HepLean.PerturbationTheory.Koszul.KoszulSign import HepLean.PerturbationTheory.FieldSpecification.Filters /-! # Normal Ordering of states - - -/ namespace FieldSpecification diff --git a/HepLean/PerturbationTheory/WickContraction/Basic.lean b/HepLean/PerturbationTheory/WickContraction/Basic.lean index 52ceed07..c6eec580 100644 --- a/HepLean/PerturbationTheory/WickContraction/Basic.lean +++ b/HepLean/PerturbationTheory/WickContraction/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.OperatorAlgebra.NormalOrder +import HepLean.PerturbationTheory.Algebras.ProtoOperatorAlgebra.NormalOrder import HepLean.Mathematics.List.InsertIdx /-! diff --git a/HepLean/PerturbationTheory/WickContraction/Involutions.lean b/HepLean/PerturbationTheory/WickContraction/Involutions.lean index 96343aa3..e5961ee2 100644 --- a/HepLean/PerturbationTheory/WickContraction/Involutions.lean +++ b/HepLean/PerturbationTheory/WickContraction/Involutions.lean @@ -5,7 +5,7 @@ Authors: Joseph Tooby-Smith -/ import HepLean.PerturbationTheory.WickContraction.Uncontracted import HepLean.PerturbationTheory.Algebras.StateAlgebra.TimeOrder -import HepLean.PerturbationTheory.Algebras.OperatorAlgebra.TimeContraction +import HepLean.PerturbationTheory.Algebras.ProtoOperatorAlgebra.TimeContraction import HepLean.PerturbationTheory.WickContraction.InsertList /-! diff --git a/HepLean/PerturbationTheory/WickContraction/IsFull.lean b/HepLean/PerturbationTheory/WickContraction/IsFull.lean index 7a3d8a07..8eb6a9da 100644 --- a/HepLean/PerturbationTheory/WickContraction/IsFull.lean +++ b/HepLean/PerturbationTheory/WickContraction/IsFull.lean @@ -19,6 +19,7 @@ namespace WickContraction variable {n : β„•} (c : WickContraction n) open HepLean.List open FieldStatistic +open Nat /-- A contraction is full if there are no uncontracted fields, i.e. the finite set of uncontracted fields is empty. -/ @@ -46,8 +47,6 @@ def isFullInvolutionEquiv : {c : WickContraction n // IsFull c} ≃ left_inv c := by simp right_inv f := by simp -open Nat - /-- If `n` is even then the number of full contractions is `(n-1)!!`. -/ theorem card_of_isfull_even (he : Even n) : Fintype.card {c : WickContraction n // IsFull c} = (n - 1)β€Ό := by diff --git a/HepLean/PerturbationTheory/WickContraction/Sign.lean b/HepLean/PerturbationTheory/WickContraction/Sign.lean index 88406152..2c1091a8 100644 --- a/HepLean/PerturbationTheory/WickContraction/Sign.lean +++ b/HepLean/PerturbationTheory/WickContraction/Sign.lean @@ -85,8 +85,7 @@ lemma signFinset_insertList_none (Ο† : 𝓕.States) (Ο†s : List 𝓕.States) lemma stat_ofFinset_of_insertListLiftFinset (Ο† : 𝓕.States) (Ο†s : List 𝓕.States) (i : Fin Ο†s.length.succ) (a : Finset (Fin Ο†s.length)) : - (𝓕 |>β‚› ⟨(Ο†s.insertIdx i Ο†).get, insertListLiftFinset Ο† i a⟩) = - 𝓕 |>β‚› βŸ¨Ο†s.get, a⟩ := by + (𝓕 |>β‚› ⟨(Ο†s.insertIdx i Ο†).get, insertListLiftFinset Ο† i a⟩) = 𝓕 |>β‚› βŸ¨Ο†s.get, a⟩ := by simp only [ofFinset, Nat.succ_eq_add_one] congr 1 rw [get_eq_insertIdx_succAbove Ο† _ i] @@ -823,8 +822,7 @@ lemma stat_signFinset_insert_some_self_fst simpa [Option.get_map] using hy2 lemma stat_signFinset_insert_some_self_snd (Ο† : 𝓕.States) (Ο†s : List 𝓕.States) - (c : WickContraction Ο†s.length) - (i : Fin Ο†s.length.succ) (j : c.uncontracted) : + (c : WickContraction Ο†s.length) (i : Fin Ο†s.length.succ) (j : c.uncontracted) : (𝓕 |>β‚› ⟨(Ο†s.insertIdx i Ο†).get, (signFinset (c.insertList Ο† Ο†s i (some j)) (finCongr (insertIdx_length_fin Ο† Ο†s i).symm (i.succAbove j)) @@ -832,8 +830,7 @@ lemma stat_signFinset_insert_some_self_snd (Ο† : 𝓕.States) (Ο†s : List 𝓕.S 𝓕 |>β‚› βŸ¨Ο†s.get, (Finset.univ.filter (fun x => j < x ∧ i.succAbove x < i ∧ ((c.getDual? x = none) ∨ βˆ€ (h : (c.getDual? x).isSome), j < ((c.getDual? x).get h))))⟩ := by - rw [get_eq_insertIdx_succAbove Ο† _ i] - rw [ofFinset_finset_map] + rw [get_eq_insertIdx_succAbove Ο† _ i, ofFinset_finset_map] swap refine (Equiv.comp_injective i.succAbove (finCongr (Eq.symm (insertIdx_length_fin Ο† Ο†s i)))).mpr ?hi.a @@ -905,55 +902,43 @@ lemma stat_signFinset_insert_some_self_snd (Ο† : 𝓕.States) (Ο†s : List 𝓕.S exact Fin.succAbove_lt_succAbove_iff.mpr hy2 lemma signInsertSomeCoef_eq_finset (Ο† : 𝓕.States) (Ο†s : List 𝓕.States) - (c : WickContraction Ο†s.length) - (i : Fin Ο†s.length.succ) (j : c.uncontracted) (hΟ†j : (𝓕 |>β‚› Ο†) = (𝓕 |>β‚› Ο†s[j.1])) : - c.signInsertSomeCoef Ο† Ο†s i j = + (c : WickContraction Ο†s.length) (i : Fin Ο†s.length.succ) (j : c.uncontracted) + (hΟ†j : (𝓕 |>β‚› Ο†) = (𝓕 |>β‚› Ο†s[j.1])) : c.signInsertSomeCoef Ο† Ο†s i j = if i < i.succAbove j then - 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› βŸ¨Ο†s.get, - (Finset.univ.filter (fun x => i < i.succAbove x ∧ x < j ∧ ((c.getDual? x = none) ∨ - βˆ€ (h : (c.getDual? x).isSome), i < i.succAbove ((c.getDual? x).get h))))⟩) else - 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› βŸ¨Ο†s.get, - (Finset.univ.filter (fun x => j < x ∧ i.succAbove x < i ∧ ((c.getDual? x = none) ∨ - βˆ€ (h : (c.getDual? x).isSome), j < ((c.getDual? x).get h))))⟩) := by - rw [signInsertSomeCoef_if] - rw [stat_signFinset_insert_some_self_snd] - rw [stat_signFinset_insert_some_self_fst] + 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› βŸ¨Ο†s.get, + (Finset.univ.filter (fun x => i < i.succAbove x ∧ x < j ∧ ((c.getDual? x = none) ∨ + βˆ€ (h : (c.getDual? x).isSome), i < i.succAbove ((c.getDual? x).get h))))⟩) + else + 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› βŸ¨Ο†s.get, + (Finset.univ.filter (fun x => j < x ∧ i.succAbove x < i ∧ ((c.getDual? x = none) ∨ + βˆ€ (h : (c.getDual? x).isSome), j < ((c.getDual? x).get h))))⟩) := by + rw [signInsertSomeCoef_if, stat_signFinset_insert_some_self_snd, + stat_signFinset_insert_some_self_fst] simp [hΟ†j] lemma signInsertSome_mul_filter_contracted_of_lt (Ο† : 𝓕.States) (Ο†s : List 𝓕.States) (c : WickContraction Ο†s.length) (i : Fin Ο†s.length.succ) (k : c.uncontracted) - (hk : i.succAbove k < i) - (hg : GradingCompliant Ο†s c ∧ 𝓕.statesStatistic Ο† = 𝓕.statesStatistic Ο†s[k.1]) : + (hk : i.succAbove k < i) (hg : GradingCompliant Ο†s c ∧ (𝓕 |>β‚› Ο†) = 𝓕 |>β‚› Ο†s[k.1]) : signInsertSome Ο† Ο†s c i k * 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› βŸ¨Ο†s.get, c.uncontracted.filter (fun x => x ≀ ↑k)⟩) = 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› βŸ¨Ο†s.get, Finset.univ.filter (fun x => i.succAbove x < i)⟩) := by - rw [signInsertSome, signInsertSomeProd_eq_finset, signInsertSomeCoef_eq_finset] - rw [if_neg (by omega), ← map_mul, ← map_mul] + rw [signInsertSome, signInsertSomeProd_eq_finset (hΟ†j := hg.2) (hg := hg.1), + signInsertSomeCoef_eq_finset (hΟ†j := hg.2), if_neg (by omega), ← map_mul, ← map_mul] congr 1 rw [mul_eq_iff_eq_mul, ofFinset_union_disjoint] swap - Β· rw [Finset.disjoint_filter] + Β· /- Disjointness needed for `ofFinset_union_disjoint`. -/ + rw [Finset.disjoint_filter] intro j _ h simp only [Nat.succ_eq_add_one, not_lt, not_and, not_forall, not_or, not_le] intro h1 use h1 omega - trans 𝓕 |>β‚› βŸ¨Ο†s.get, (Finset.filter (fun x => - (↑k < x ∧ i.succAbove x < i ∧ (c.getDual? x = none ∨ - βˆ€ (h : (c.getDual? x).isSome = true), ↑k < (c.getDual? x).get h)) - ∨ ((c.getDual? x).isSome = true ∧ - βˆ€ (h : (c.getDual? x).isSome = true), x < ↑k ∧ - (i.succAbove x < i ∧ i < i.succAbove ((c.getDual? x).get h) ∨ - ↑k < (c.getDual? x).get h ∧ Β¬i.succAbove x < i))) Finset.univ)⟩ - Β· congr - ext j - simp rw [ofFinset_union, ← mul_eq_one_iff, ofFinset_union] simp only [Nat.succ_eq_add_one, not_lt] - apply stat_ofFinset_eq_one_of_gradingCompliant - Β· exact hg.1 - /- the getDual? is none case-/ - Β· intro j hn + apply stat_ofFinset_eq_one_of_gradingCompliant _ _ _ hg.1 + Β· /- The `c.getDual? i = none` case for `stat_ofFinset_eq_one_of_gradingCompliant`. -/ + intro j hn simp only [uncontracted, Finset.mem_sdiff, Finset.mem_union, Finset.mem_filter, Finset.mem_univ, hn, Option.isSome_none, Bool.false_eq_true, IsEmpty.forall_iff, or_self, and_true, or_false, true_and, and_self, Finset.mem_inter, not_and, not_lt, Classical.not_imp, not_le, and_imp] @@ -978,8 +963,8 @@ lemma signInsertSome_mul_filter_contracted_of_lt (Ο† : 𝓕.States) (Ο†s : List apply Fin.ne_succAbove i j omega Β· exact h1' - /- the getDual? is some case-/ - Β· intro j hj + Β· /- The `(c.getDual? i).isSome` case for `stat_ofFinset_eq_one_of_gradingCompliant`. -/ + intro j hj have hn : Β¬ c.getDual? j = none := by exact Option.isSome_iff_ne_none.mp hj simp only [uncontracted, Finset.mem_sdiff, Finset.mem_union, Finset.mem_filter, Finset.mem_univ, hn, hj, forall_true_left, false_or, true_and, and_false, false_and, Finset.mem_inter, @@ -1033,28 +1018,24 @@ lemma signInsertSome_mul_filter_contracted_of_lt (Ο† : 𝓕.States) (Ο†s : List Β· simp_all only [Fin.getElem_fin, ne_eq, not_lt, false_and, false_or, or_false, and_self, or_true, imp_self] omega - Β· exact hg.2 - Β· exact hg.2 - Β· exact hg.1 lemma signInsertSome_mul_filter_contracted_of_not_lt (Ο† : 𝓕.States) (Ο†s : List 𝓕.States) (c : WickContraction Ο†s.length) (i : Fin Ο†s.length.succ) (k : c.uncontracted) - (hk : Β¬ i.succAbove k < i) - (hg : GradingCompliant Ο†s c ∧ 𝓕.statesStatistic Ο† = 𝓕.statesStatistic Ο†s[k.1]) : + (hk : Β¬ i.succAbove k < i) (hg : GradingCompliant Ο†s c ∧ (𝓕 |>β‚› Ο†) = 𝓕 |>β‚› Ο†s[k.1]) : signInsertSome Ο† Ο†s c i k * 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› βŸ¨Ο†s.get, c.uncontracted.filter (fun x => x < ↑k)⟩) = 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› βŸ¨Ο†s.get, Finset.univ.filter (fun x => i.succAbove x < i)⟩) := by have hik : i.succAbove ↑k β‰  i := by exact Fin.succAbove_ne i ↑k - rw [signInsertSome, signInsertSomeProd_eq_finset, signInsertSomeCoef_eq_finset] - rw [if_pos (by omega), ← map_mul, ← map_mul] + rw [signInsertSome, signInsertSomeProd_eq_finset (hΟ†j := hg.2) (hg := hg.1), + signInsertSomeCoef_eq_finset (hΟ†j := hg.2), if_pos (by omega), ← map_mul, ← map_mul] congr 1 rw [mul_eq_iff_eq_mul, ofFinset_union, ofFinset_union] apply (mul_eq_one_iff _ _).mp rw [ofFinset_union] simp only [Nat.succ_eq_add_one, not_lt] - apply stat_ofFinset_eq_one_of_gradingCompliant - Β· exact hg.1 - Β· intro j hj + apply stat_ofFinset_eq_one_of_gradingCompliant _ _ _ hg.1 + Β· /- The `c.getDual? i = none` case for `stat_ofFinset_eq_one_of_gradingCompliant`. -/ + intro j hj have hijsucc : i.succAbove j β‰  i := by exact Fin.succAbove_ne i j simp only [uncontracted, Finset.mem_sdiff, Finset.mem_union, Finset.mem_filter, Finset.mem_univ, hj, Option.isSome_none, Bool.false_eq_true, IsEmpty.forall_iff, or_self, and_true, true_and, @@ -1072,7 +1053,8 @@ lemma signInsertSome_mul_filter_contracted_of_not_lt (Ο† : 𝓕.States) (Ο†s : L omega simp only [hij, true_and] at h ⊒ omega - Β· intro j hj + Β· /- The `(c.getDual? i).isSome` case for `stat_ofFinset_eq_one_of_gradingCompliant`. -/ + intro j hj have hn : Β¬ c.getDual? j = none := by exact Option.isSome_iff_ne_none.mp hj have hijSuc : i.succAbove j β‰  i := by exact Fin.succAbove_ne i j have hkneqj : ↑k β‰  j := by @@ -1136,8 +1118,5 @@ lemma signInsertSome_mul_filter_contracted_of_not_lt (Ο† : 𝓕.States) (Ο†s : L simp only [hijn, true_and, hijn', and_false, or_false, or_true, imp_false, not_lt, forall_const] exact fun h => lt_of_le_of_ne h (Fin.succAbove_ne i ((c.getDual? j).get hj)) - Β· exact hg.2 - Β· exact hg.2 - Β· exact hg.1 end WickContraction diff --git a/HepLean/PerturbationTheory/WickContraction/TimeContract.lean b/HepLean/PerturbationTheory/WickContraction/TimeContract.lean index b4d2fe30..362045a5 100644 --- a/HepLean/PerturbationTheory/WickContraction/TimeContract.lean +++ b/HepLean/PerturbationTheory/WickContraction/TimeContract.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ import HepLean.PerturbationTheory.WickContraction.Sign -import HepLean.PerturbationTheory.Algebras.OperatorAlgebra.TimeContraction +import HepLean.PerturbationTheory.Algebras.ProtoOperatorAlgebra.TimeContraction /-! # Time contractions @@ -18,23 +18,17 @@ namespace WickContraction variable {n : β„•} (c : WickContraction n) open HepLean.List -/-! - -## Time contract. - --/ - /-- Given a Wick contraction `c` associated with a list `Ο†s`, the product of all time-contractions of pairs of contracted elements in `Ο†s`, as a member of the center of `π“ž.A`. -/ -noncomputable def timeContract (π“ž : 𝓕.OperatorAlgebra) {Ο†s : List 𝓕.States} +noncomputable def timeContract (π“ž : 𝓕.ProtoOperatorAlgebra) {Ο†s : List 𝓕.States} (c : WickContraction Ο†s.length) : Subalgebra.center β„‚ π“ž.A := ∏ (a : c.1), βŸ¨π“ž.timeContract (Ο†s.get (c.fstFieldOfContract a)) (Ο†s.get (c.sndFieldOfContract a)), π“ž.timeContract_mem_center _ _⟩ @[simp] -lemma timeContract_insertList_none (π“ž : 𝓕.OperatorAlgebra) (Ο† : 𝓕.States) (Ο†s : List 𝓕.States) +lemma timeContract_insertList_none (π“ž : 𝓕.ProtoOperatorAlgebra) (Ο† : 𝓕.States) (Ο†s : List 𝓕.States) (c : WickContraction Ο†s.length) (i : Fin Ο†s.length.succ) : (c.insertList Ο† Ο†s i none).timeContract π“ž = c.timeContract π“ž := by rw [timeContract, insertList_none_prod_contractions] @@ -42,7 +36,7 @@ lemma timeContract_insertList_none (π“ž : 𝓕.OperatorAlgebra) (Ο† : 𝓕.Stat ext a simp -lemma timeConract_insertList_some (π“ž : 𝓕.OperatorAlgebra) (Ο† : 𝓕.States) (Ο†s : List 𝓕.States) +lemma timeConract_insertList_some (π“ž : 𝓕.ProtoOperatorAlgebra) (Ο† : 𝓕.States) (Ο†s : List 𝓕.States) (c : WickContraction Ο†s.length) (i : Fin Ο†s.length.succ) (j : c.uncontracted) : (c.insertList Ο† Ο†s i (some j)).timeContract π“ž = (if i < i.succAbove j then @@ -62,7 +56,7 @@ lemma timeConract_insertList_some (π“ž : 𝓕.OperatorAlgebra) (Ο† : 𝓕.State open FieldStatistic lemma timeConract_insertList_some_eq_mul_contractStateAtIndex_lt - (π“ž : 𝓕.OperatorAlgebra) (Ο† : 𝓕.States) (Ο†s : List 𝓕.States) + (π“ž : 𝓕.ProtoOperatorAlgebra) (Ο† : 𝓕.States) (Ο†s : List 𝓕.States) (c : WickContraction Ο†s.length) (i : Fin Ο†s.length.succ) (k : c.uncontracted) (ht : 𝓕.timeOrderRel Ο† Ο†s[k.1]) (hik : i < i.succAbove k) : (c.insertList Ο† Ο†s i (some k)).timeContract π“ž = @@ -71,9 +65,9 @@ lemma timeConract_insertList_some_eq_mul_contractStateAtIndex_lt ((uncontractedStatesEquiv Ο†s c) (some k)) * c.timeContract π“ž) := by rw [timeConract_insertList_some] simp only [Nat.succ_eq_add_one, Fin.getElem_fin, ite_mul, instCommGroup.eq_1, - OperatorAlgebra.contractStateAtIndex, uncontractedStatesEquiv, Equiv.optionCongr_apply, + ProtoOperatorAlgebra.contractStateAtIndex, uncontractedStatesEquiv, Equiv.optionCongr_apply, Equiv.coe_trans, Option.map_some', Function.comp_apply, finCongr_apply, Fin.coe_cast, - List.getElem_map, uncontractedList_getElem_uncontractedFinEquiv_symm, List.get_eq_getElem, + List.getElem_map, uncontractedList_getElem_uncontractedIndexEquiv_symm, List.get_eq_getElem, Algebra.smul_mul_assoc] Β· simp only [hik, ↓reduceIte, MulMemClass.coe_mul] rw [π“ž.timeContract_of_timeOrderRel] @@ -83,21 +77,21 @@ lemma timeConract_insertList_some_eq_mul_contractStateAtIndex_lt Β· simp simp only [smul_smul] congr - have h1 : ofList 𝓕.statesStatistic (List.take (↑(c.uncontractedFinEquiv.symm k)) + have h1 : ofList 𝓕.statesStatistic (List.take (↑(c.uncontractedIndexEquiv.symm k)) (List.map Ο†s.get c.uncontractedList)) = (𝓕 |>β‚› βŸ¨Ο†s.get, (Finset.filter (fun x => x < k) c.uncontracted)⟩) := by simp only [ofFinset] congr rw [← List.map_take] congr - rw [take_uncontractedFinEquiv_symm] + rw [take_uncontractedIndexEquiv_symm] rw [filter_uncontractedList] rw [h1] simp only [exchangeSign_mul_self] Β· exact ht lemma timeConract_insertList_some_eq_mul_contractStateAtIndex_not_lt - (π“ž : 𝓕.OperatorAlgebra) (Ο† : 𝓕.States) (Ο†s : List 𝓕.States) + (π“ž : 𝓕.ProtoOperatorAlgebra) (Ο† : 𝓕.States) (Ο†s : List 𝓕.States) (c : WickContraction Ο†s.length) (i : Fin Ο†s.length.succ) (k : c.uncontracted) (ht : Β¬ 𝓕.timeOrderRel Ο†s[k.1] Ο†) (hik : Β¬ i < i.succAbove k) : (c.insertList Ο† Ο†s i (some k)).timeContract π“ž = @@ -106,22 +100,22 @@ lemma timeConract_insertList_some_eq_mul_contractStateAtIndex_not_lt ((uncontractedStatesEquiv Ο†s c) (some k)) * c.timeContract π“ž) := by rw [timeConract_insertList_some] simp only [Nat.succ_eq_add_one, Fin.getElem_fin, ite_mul, instCommGroup.eq_1, - OperatorAlgebra.contractStateAtIndex, uncontractedStatesEquiv, Equiv.optionCongr_apply, + ProtoOperatorAlgebra.contractStateAtIndex, uncontractedStatesEquiv, Equiv.optionCongr_apply, Equiv.coe_trans, Option.map_some', Function.comp_apply, finCongr_apply, Fin.coe_cast, - List.getElem_map, uncontractedList_getElem_uncontractedFinEquiv_symm, List.get_eq_getElem, + List.getElem_map, uncontractedList_getElem_uncontractedIndexEquiv_symm, List.get_eq_getElem, Algebra.smul_mul_assoc] simp only [hik, ↓reduceIte, MulMemClass.coe_mul] rw [π“ž.timeContract_of_not_timeOrderRel, π“ž.timeContract_of_timeOrderRel] simp only [instCommGroup.eq_1, Algebra.smul_mul_assoc, smul_smul] congr - have h1 : ofList 𝓕.statesStatistic (List.take (↑(c.uncontractedFinEquiv.symm k)) + have h1 : ofList 𝓕.statesStatistic (List.take (↑(c.uncontractedIndexEquiv.symm k)) (List.map Ο†s.get c.uncontractedList)) = (𝓕 |>β‚› βŸ¨Ο†s.get, (Finset.filter (fun x => x < k) c.uncontracted)⟩) := by simp only [ofFinset] congr rw [← List.map_take] congr - rw [take_uncontractedFinEquiv_symm, filter_uncontractedList] + rw [take_uncontractedIndexEquiv_symm, filter_uncontractedList] rw [h1] trans 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› βŸ¨Ο†s.get, {k.1}⟩) Β· rw [exchangeSign_symm, ofFinset_singleton] @@ -148,7 +142,7 @@ lemma timeConract_insertList_some_eq_mul_contractStateAtIndex_not_lt simp_all only [Fin.getElem_fin, Nat.succ_eq_add_one, not_lt, false_or] exact ht -lemma timeContract_of_not_gradingCompliant (π“ž : 𝓕.OperatorAlgebra) (Ο†s : List 𝓕.States) +lemma timeContract_of_not_gradingCompliant (π“ž : 𝓕.ProtoOperatorAlgebra) (Ο†s : List 𝓕.States) (c : WickContraction Ο†s.length) (h : Β¬ GradingCompliant Ο†s c) : c.timeContract π“ž = 0 := by rw [timeContract] @@ -159,7 +153,7 @@ lemma timeContract_of_not_gradingCompliant (π“ž : 𝓕.OperatorAlgebra) (Ο†s : simp only [Finset.univ_eq_attach, Finset.mem_attach] apply Subtype.eq simp only [List.get_eq_getElem, ZeroMemClass.coe_zero] - rw [OperatorAlgebra.timeContract_zero_of_diff_grade] + rw [ProtoOperatorAlgebra.timeContract_zero_of_diff_grade] simp [ha2] end WickContraction diff --git a/HepLean/PerturbationTheory/WickContraction/UncontractedList.lean b/HepLean/PerturbationTheory/WickContraction/UncontractedList.lean index 674edbc0..e3aed04f 100644 --- a/HepLean/PerturbationTheory/WickContraction/UncontractedList.lean +++ b/HepLean/PerturbationTheory/WickContraction/UncontractedList.lean @@ -219,6 +219,99 @@ lemma uncontractedList_length_eq_card (c : WickContraction n) : rw [uncontractedList_eq_sort] exact Finset.length_sort fun x1 x2 => x1 ≀ x2 +lemma filter_uncontractedList (c : WickContraction n) (p : Fin n β†’ Prop) [DecidablePred p] : + (c.uncontractedList.filter p) = (c.uncontracted.filter p).sort (Β· ≀ Β·) := by + have h1 : (c.uncontractedList.filter p).Sorted (Β· ≀ Β·) := by + apply List.Sorted.filter + exact uncontractedList_sorted c + have h2 : (c.uncontractedList.filter p).Nodup := by + refine List.Nodup.filter _ ?_ + exact uncontractedList_nodup c + have h3 : (c.uncontractedList.filter p).toFinset = (c.uncontracted.filter p) := by + ext a + simp only [List.toFinset_filter, decide_eq_true_eq, Finset.mem_filter, List.mem_toFinset, + and_congr_left_iff] + rw [uncontractedList_mem_iff] + simp + have hx := (List.toFinset_sort (Β· ≀ Β·) h2).mpr h1 + rw [← hx, h3] + +/-! + +## uncontractedIndexEquiv + +-/ + +/-- The equivalence between the positions of `c.uncontractedList` i.e. elements of + `Fin (c.uncontractedList).length` and the finite set `c.uncontracted` considered as a finite type. +-/ +def uncontractedIndexEquiv (c : WickContraction n) : + Fin (c.uncontractedList).length ≃ c.uncontracted where + toFun i := ⟨c.uncontractedList.get i, c.uncontractedList_get_mem_uncontracted i⟩ + invFun i := ⟨List.indexOf i.1 c.uncontractedList, + List.indexOf_lt_length.mpr ((c.uncontractedList_mem_iff i.1).mpr i.2)⟩ + left_inv i := by + ext + exact List.get_indexOf (uncontractedList_nodup c) _ + right_inv i := by + ext + simp + +@[simp] +lemma uncontractedList_getElem_uncontractedIndexEquiv_symm (k : c.uncontracted) : + c.uncontractedList[(c.uncontractedIndexEquiv.symm k).val] = k := by + simp [uncontractedIndexEquiv] + +lemma uncontractedIndexEquiv_symm_eq_filter_length (k : c.uncontracted) : + (c.uncontractedIndexEquiv.symm k).val = + (List.filter (fun i => i < k.val) c.uncontractedList).length := by + simp only [uncontractedIndexEquiv, List.get_eq_getElem, Equiv.coe_fn_symm_mk] + rw [fin_list_sorted_indexOf_mem] + Β· simp + Β· exact uncontractedList_sorted c + Β· rw [uncontractedList_mem_iff] + exact k.2 + +lemma take_uncontractedIndexEquiv_symm (k : c.uncontracted) : + c.uncontractedList.take (c.uncontractedIndexEquiv.symm k).val = + c.uncontractedList.filter (fun i => i < k.val) := by + have hl := fin_list_sorted_split c.uncontractedList (uncontractedList_sorted c) k.val + conv_lhs => + rhs + rw [hl] + rw [uncontractedIndexEquiv_symm_eq_filter_length] + simp + +/-! + +## uncontractedStatesEquiv + +-/ + +/-- The equivalence between the type `Option c.uncontracted` for `WickContraction Ο†s.length` and + `Option (Fin (c.uncontractedList.map Ο†s.get).length)`, that is optional positions of + `c.uncontractedList.map Ο†s.get` induced by `uncontractedIndexEquiv`. -/ +def uncontractedStatesEquiv (Ο†s : List 𝓕.States) (c : WickContraction Ο†s.length) : + Option c.uncontracted ≃ Option (Fin (c.uncontractedList.map Ο†s.get).length) := + Equiv.optionCongr (c.uncontractedIndexEquiv.symm.trans (finCongr (by simp))) + +@[simp] +lemma uncontractedStatesEquiv_none (Ο†s : List 𝓕.States) (c : WickContraction Ο†s.length) : + (uncontractedStatesEquiv Ο†s c).toFun none = none := by + simp [uncontractedStatesEquiv] + +lemma uncontractedStatesEquiv_list_sum [AddCommMonoid Ξ±] (Ο†s : List 𝓕.States) + (c : WickContraction Ο†s.length) (f : Option (Fin (c.uncontractedList.map Ο†s.get).length) β†’ Ξ±) : + βˆ‘ (i : Option (Fin (c.uncontractedList.map Ο†s.get).length)), f i = + βˆ‘ (i : Option c.uncontracted), f (c.uncontractedStatesEquiv Ο†s i) := by + rw [(c.uncontractedStatesEquiv Ο†s).sum_comp] + +/-! + +## Uncontracted List for extractEquiv symm none + +-/ + lemma uncontractedList_succAboveEmb_sorted (c : WickContraction n) (i : Fin n.succ) : ((List.map i.succAboveEmb c.uncontractedList)).Sorted (Β· ≀ Β·) := by apply fin_list_sorted_succAboveEmb_sorted @@ -230,33 +323,54 @@ lemma uncontractedList_succAboveEmb_nodup (c : WickContraction n) (i : Fin n.suc Β· exact Function.Embedding.injective i.succAboveEmb Β· exact uncontractedList_nodup c -lemma uncontractedList_succAboveEmb_toFinset (c : WickContraction n) (i : Fin n.succ) : - (List.map i.succAboveEmb c.uncontractedList).toFinset = - (Finset.map i.succAboveEmb c.uncontracted) := by +lemma uncontractedList_succAbove_orderedInsert_nodup (c : WickContraction n) (i : Fin n.succ) : + (List.orderedInsert (Β· ≀ Β·) i (List.map i.succAboveEmb c.uncontractedList)).Nodup := by + have h1 : (List.orderedInsert (Β· ≀ Β·) i (List.map i.succAboveEmb c.uncontractedList)).Perm + (i :: List.map i.succAboveEmb c.uncontractedList) := by + exact List.perm_orderedInsert (fun x1 x2 => x1 ≀ x2) i _ + apply List.Perm.nodup h1.symm + simp only [Nat.succ_eq_add_one, List.nodup_cons, List.mem_map, not_exists, + not_and] + apply And.intro + Β· intro x _ + exact Fin.succAbove_ne i x + Β· exact uncontractedList_succAboveEmb_nodup c i + +lemma uncontractedList_succAbove_orderedInsert_sorted (c : WickContraction n) (i : Fin n.succ) : + (List.orderedInsert (Β· ≀ Β·) i + (List.map i.succAboveEmb c.uncontractedList)).Sorted (Β· ≀ Β·) := by + refine List.Sorted.orderedInsert i (List.map (⇑i.succAboveEmb) c.uncontractedList) ?_ + exact uncontractedList_succAboveEmb_sorted c i + +lemma uncontractedList_succAbove_orderedInsert_toFinset (c : WickContraction n) (i : Fin n.succ) : + (List.orderedInsert (Β· ≀ Β·) i (List.map i.succAboveEmb c.uncontractedList)).toFinset = + (Insert.insert i (Finset.map i.succAboveEmb c.uncontracted)) := by ext a - simp only [Fin.coe_succAboveEmb, List.mem_toFinset, List.mem_map, Finset.mem_map, - Fin.succAboveEmb_apply] - rw [← c.uncontractedList_toFinset] + simp only [Nat.succ_eq_add_one, Fin.coe_succAboveEmb, List.mem_toFinset, List.mem_orderedInsert, + List.mem_map, Finset.mem_insert, Finset.mem_map, Fin.succAboveEmb_apply] + rw [← uncontractedList_toFinset] simp -lemma uncontractedList_succAboveEmb_eq_sort(c : WickContraction n) (i : Fin n.succ) : - (List.map i.succAboveEmb c.uncontractedList) = - (c.uncontracted.map i.succAboveEmb).sort (Β· ≀ Β·) := by - rw [← uncontractedList_succAboveEmb_toFinset] +lemma uncontractedList_succAbove_orderedInsert_eq_sort (c : WickContraction n) (i : Fin n.succ) : + (List.orderedInsert (Β· ≀ Β·) i (List.map i.succAboveEmb c.uncontractedList)) = + (Insert.insert i (Finset.map i.succAboveEmb c.uncontracted)).sort (Β· ≀ Β·) := by + rw [← uncontractedList_succAbove_orderedInsert_toFinset] symm refine (List.toFinset_sort (Ξ± := Fin n.succ) (Β· ≀ Β·) ?_).mpr ?_ - Β· exact uncontractedList_succAboveEmb_nodup c i - Β· exact uncontractedList_succAboveEmb_sorted c i + Β· exact uncontractedList_succAbove_orderedInsert_nodup c i + Β· exact uncontractedList_succAbove_orderedInsert_sorted c i -lemma uncontractedList_succAboveEmb_eraseIdx_sorted (c : WickContraction n) (i : Fin n.succ) - (k: β„•) : ((List.map i.succAboveEmb c.uncontractedList).eraseIdx k).Sorted (Β· ≀ Β·) := by - apply HepLean.List.eraseIdx_sorted - exact uncontractedList_succAboveEmb_sorted c i +lemma uncontractedList_extractEquiv_symm_none (c : WickContraction n) (i : Fin n.succ) : + ((extractEquiv i).symm ⟨c, none⟩).uncontractedList = + List.orderedInsert (Β· ≀ Β·) i (List.map i.succAboveEmb c.uncontractedList) := by + rw [uncontractedList_eq_sort, extractEquiv_symm_none_uncontracted] + rw [uncontractedList_succAbove_orderedInsert_eq_sort] -lemma uncontractedList_succAboveEmb_eraseIdx_nodup (c : WickContraction n) (i : Fin n.succ) (k: β„•) : - ((List.map i.succAboveEmb c.uncontractedList).eraseIdx k).Nodup := by - refine List.Nodup.eraseIdx k ?_ - exact uncontractedList_succAboveEmb_nodup c i +/-! + +## Uncontracted List for extractEquiv symm some + +-/ lemma uncontractedList_succAboveEmb_eraseIdx_toFinset (c : WickContraction n) (i : Fin n.succ) (k : β„•) (hk : k < c.uncontractedList.length) : @@ -286,6 +400,16 @@ lemma uncontractedList_succAboveEmb_eraseIdx_toFinset (c : WickContraction n) (i simp_all [uncontractedList] exact uncontractedList_succAboveEmb_nodup c i +lemma uncontractedList_succAboveEmb_eraseIdx_sorted (c : WickContraction n) (i : Fin n.succ) + (k: β„•) : ((List.map i.succAboveEmb c.uncontractedList).eraseIdx k).Sorted (Β· ≀ Β·) := by + apply HepLean.List.eraseIdx_sorted + exact uncontractedList_succAboveEmb_sorted c i + +lemma uncontractedList_succAboveEmb_eraseIdx_nodup (c : WickContraction n) (i : Fin n.succ) (k: β„•) : + ((List.map i.succAboveEmb c.uncontractedList).eraseIdx k).Nodup := by + refine List.Nodup.eraseIdx k ?_ + exact uncontractedList_succAboveEmb_nodup c i + lemma uncontractedList_succAboveEmb_eraseIdx_eq_sort (c : WickContraction n) (i : Fin n.succ) (k : β„•) (hk : k < c.uncontractedList.length) : ((List.map i.succAboveEmb c.uncontractedList).eraseIdx k) = @@ -297,48 +421,34 @@ lemma uncontractedList_succAboveEmb_eraseIdx_eq_sort (c : WickContraction n) (i Β· exact uncontractedList_succAboveEmb_eraseIdx_nodup c i k Β· exact uncontractedList_succAboveEmb_eraseIdx_sorted c i k -lemma uncontractedList_succAbove_orderedInsert_sorted (c : WickContraction n) (i : Fin n.succ) : - (List.orderedInsert (Β· ≀ Β·) i - (List.map i.succAboveEmb c.uncontractedList)).Sorted (Β· ≀ Β·) := by - refine List.Sorted.orderedInsert i (List.map (⇑i.succAboveEmb) c.uncontractedList) ?_ - exact uncontractedList_succAboveEmb_sorted c i - -lemma uncontractedList_succAbove_orderedInsert_nodup (c : WickContraction n) (i : Fin n.succ) : - (List.orderedInsert (Β· ≀ Β·) i (List.map i.succAboveEmb c.uncontractedList)).Nodup := by - have h1 : (List.orderedInsert (Β· ≀ Β·) i (List.map i.succAboveEmb c.uncontractedList)).Perm - (i :: List.map i.succAboveEmb c.uncontractedList) := by - exact List.perm_orderedInsert (fun x1 x2 => x1 ≀ x2) i _ - apply List.Perm.nodup h1.symm - simp only [Nat.succ_eq_add_one, List.nodup_cons, List.mem_map, not_exists, - not_and] - apply And.intro - Β· intro x _ - exact Fin.succAbove_ne i x - Β· exact uncontractedList_succAboveEmb_nodup c i +lemma uncontractedList_extractEquiv_symm_some (c : WickContraction n) (i : Fin n.succ) + (k : c.uncontracted) : ((extractEquiv i).symm ⟨c, some k⟩).uncontractedList = + ((c.uncontractedList).map i.succAboveEmb).eraseIdx (c.uncontractedIndexEquiv.symm k) := by + rw [uncontractedList_eq_sort] + rw [uncontractedList_succAboveEmb_eraseIdx_eq_sort] + swap + simp only [Fin.is_lt] + congr + simp only [Nat.succ_eq_add_one, extractEquiv, Equiv.coe_fn_symm_mk, + uncontractedList_getElem_uncontractedIndexEquiv_symm, Fin.succAboveEmb_apply] + rw [insert_some_uncontracted] + ext a + simp -lemma uncontractedList_succAbove_orderedInsert_toFinset (c : WickContraction n) (i : Fin n.succ) : - (List.orderedInsert (Β· ≀ Β·) i (List.map i.succAboveEmb c.uncontractedList)).toFinset = - (Insert.insert i (Finset.map i.succAboveEmb c.uncontracted)) := by +lemma uncontractedList_succAboveEmb_toFinset (c : WickContraction n) (i : Fin n.succ) : + (List.map i.succAboveEmb c.uncontractedList).toFinset = + (Finset.map i.succAboveEmb c.uncontracted) := by ext a - simp only [Nat.succ_eq_add_one, Fin.coe_succAboveEmb, List.mem_toFinset, List.mem_orderedInsert, - List.mem_map, Finset.mem_insert, Finset.mem_map, Fin.succAboveEmb_apply] - rw [← uncontractedList_toFinset] + simp only [Fin.coe_succAboveEmb, List.mem_toFinset, List.mem_map, Finset.mem_map, + Fin.succAboveEmb_apply] + rw [← c.uncontractedList_toFinset] simp -lemma uncontractedList_succAbove_orderedInsert_eq_sort (c : WickContraction n) (i : Fin n.succ) : - (List.orderedInsert (Β· ≀ Β·) i (List.map i.succAboveEmb c.uncontractedList)) = - (Insert.insert i (Finset.map i.succAboveEmb c.uncontracted)).sort (Β· ≀ Β·) := by - rw [← uncontractedList_succAbove_orderedInsert_toFinset] - symm - refine (List.toFinset_sort (Ξ± := Fin n.succ) (Β· ≀ Β·) ?_).mpr ?_ - Β· exact uncontractedList_succAbove_orderedInsert_nodup c i - Β· exact uncontractedList_succAbove_orderedInsert_sorted c i +/-! -lemma uncontractedList_extractEquiv_symm_none (c : WickContraction n) (i : Fin n.succ) : - ((extractEquiv i).symm ⟨c, none⟩).uncontractedList = - List.orderedInsert (Β· ≀ Β·) i (List.map i.succAboveEmb c.uncontractedList) := by - rw [uncontractedList_eq_sort, extractEquiv_symm_none_uncontracted] - rw [uncontractedList_succAbove_orderedInsert_eq_sort] +## uncontractedListOrderPos + +-/ /-- Given a Wick contraction `c : WickContraction n` and a `Fin n.succ`, the number of elements of `c.uncontractedList` which are less then `i`. @@ -383,108 +493,18 @@ lemma orderedInsert_succAboveEmb_uncontractedList_eq_insertIdx (c : WickContract (List.orderedInsert (Β· ≀ Β·) i (List.map i.succAboveEmb c.uncontractedList)) = (List.map i.succAboveEmb c.uncontractedList).insertIdx (uncontractedListOrderPos c i) i := by rw [orderedInsert_eq_insertIdx_of_fin_list_sorted] - swap - exact uncontractedList_succAboveEmb_sorted c i - congr 1 - simp only [Nat.succ_eq_add_one, Fin.val_fin_lt, Fin.coe_succAboveEmb, uncontractedListOrderPos] - rw [List.filter_map] - simp only [List.length_map] - congr - funext x - simp only [Function.comp_apply, Fin.succAbove, decide_eq_decide] - split - simp only [Fin.lt_def, Fin.coe_castSucc] - rename_i h - simp_all only [Fin.lt_def, Fin.coe_castSucc, not_lt, Fin.val_succ] - omega - -/-- The equivalence between the positions of `c.uncontractedList` i.e. elements of - `Fin (c.uncontractedList).length` and the finite set `c.uncontracted` considered as a finite type. --/ -def uncontractedFinEquiv (c : WickContraction n) : - Fin (c.uncontractedList).length ≃ c.uncontracted where - toFun i := ⟨c.uncontractedList.get i, c.uncontractedList_get_mem_uncontracted i⟩ - invFun i := ⟨List.indexOf i.1 c.uncontractedList, - List.indexOf_lt_length.mpr ((c.uncontractedList_mem_iff i.1).mpr i.2)⟩ - left_inv i := by - ext - exact List.get_indexOf (uncontractedList_nodup c) _ - right_inv i := by - ext - simp - -@[simp] -lemma uncontractedList_getElem_uncontractedFinEquiv_symm (k : c.uncontracted) : - c.uncontractedList[(c.uncontractedFinEquiv.symm k).val] = k := by - simp [uncontractedFinEquiv] - -lemma uncontractedFinEquiv_symm_eq_filter_length (k : c.uncontracted) : - (c.uncontractedFinEquiv.symm k).val = - (List.filter (fun i => i < k.val) c.uncontractedList).length := by - simp only [uncontractedFinEquiv, List.get_eq_getElem, Equiv.coe_fn_symm_mk] - rw [fin_list_sorted_indexOf_mem] - Β· simp - Β· exact uncontractedList_sorted c - Β· rw [uncontractedList_mem_iff] - exact k.2 - -lemma take_uncontractedFinEquiv_symm (k : c.uncontracted) : - c.uncontractedList.take (c.uncontractedFinEquiv.symm k).val = - c.uncontractedList.filter (fun i => i < k.val) := by - have hl := fin_list_sorted_split c.uncontractedList (uncontractedList_sorted c) k.val - conv_lhs => - rhs - rw [hl] - rw [uncontractedFinEquiv_symm_eq_filter_length] - simp - -/-- The equivalence between the type `Option c.uncontracted` for `WickContraction Ο†s.length` and - `Option (Fin (c.uncontractedList.map Ο†s.get).length)`, that is optional positions of - `c.uncontractedList.map Ο†s.get` induced by `uncontractedFinEquiv`. -/ -def uncontractedStatesEquiv (Ο†s : List 𝓕.States) (c : WickContraction Ο†s.length) : - Option c.uncontracted ≃ Option (Fin (c.uncontractedList.map Ο†s.get).length) := - Equiv.optionCongr (c.uncontractedFinEquiv.symm.trans (finCongr (by simp))) - -@[simp] -lemma uncontractedStatesEquiv_none (Ο†s : List 𝓕.States) (c : WickContraction Ο†s.length) : - (uncontractedStatesEquiv Ο†s c).toFun none = none := by - simp [uncontractedStatesEquiv] - -lemma uncontractedStatesEquiv_list_sum [AddCommMonoid Ξ±] (Ο†s : List 𝓕.States) - (c : WickContraction Ο†s.length) (f : Option (Fin (c.uncontractedList.map Ο†s.get).length) β†’ Ξ±) : - βˆ‘ (i : Option (Fin (c.uncontractedList.map Ο†s.get).length)), f i = - βˆ‘ (i : Option c.uncontracted), f (c.uncontractedStatesEquiv Ο†s i) := by - rw [(c.uncontractedStatesEquiv Ο†s).sum_comp] - -lemma uncontractedList_extractEquiv_symm_some (c : WickContraction n) (i : Fin n.succ) - (k : c.uncontracted) : ((extractEquiv i).symm ⟨c, some k⟩).uncontractedList = - ((c.uncontractedList).map i.succAboveEmb).eraseIdx (c.uncontractedFinEquiv.symm k) := by - rw [uncontractedList_eq_sort] - rw [uncontractedList_succAboveEmb_eraseIdx_eq_sort] - swap - simp only [Fin.is_lt] - congr - simp only [Nat.succ_eq_add_one, extractEquiv, Equiv.coe_fn_symm_mk, - uncontractedList_getElem_uncontractedFinEquiv_symm, Fin.succAboveEmb_apply] - rw [insert_some_uncontracted] - ext a - simp - -lemma filter_uncontractedList (c : WickContraction n) (p : Fin n β†’ Prop) [DecidablePred p] : - (c.uncontractedList.filter p) = (c.uncontracted.filter p).sort (Β· ≀ Β·) := by - have h1 : (c.uncontractedList.filter p).Sorted (Β· ≀ Β·) := by - apply List.Sorted.filter - exact uncontractedList_sorted c - have h2 : (c.uncontractedList.filter p).Nodup := by - refine List.Nodup.filter _ ?_ - exact uncontractedList_nodup c - have h3 : (c.uncontractedList.filter p).toFinset = (c.uncontracted.filter p) := by - ext a - simp only [List.toFinset_filter, decide_eq_true_eq, Finset.mem_filter, List.mem_toFinset, - and_congr_left_iff] - rw [uncontractedList_mem_iff] - simp - have hx := (List.toFinset_sort (Β· ≀ Β·) h2).mpr h1 - rw [← hx, h3] + Β· congr 1 + simp only [Nat.succ_eq_add_one, Fin.val_fin_lt, Fin.coe_succAboveEmb, uncontractedListOrderPos] + rw [List.filter_map] + simp only [List.length_map] + congr + funext x + simp only [Function.comp_apply, Fin.succAbove, decide_eq_decide] + split + Β· simp only [Fin.lt_def, Fin.coe_castSucc] + Β· rename_i h + simp_all only [Fin.lt_def, Fin.coe_castSucc, not_lt, Fin.val_succ] + omega + Β· exact uncontractedList_succAboveEmb_sorted c i end WickContraction diff --git a/HepLean/PerturbationTheory/WicksTheorem.lean b/HepLean/PerturbationTheory/WicksTheorem.lean index a6f27ca9..cdb4a119 100644 --- a/HepLean/PerturbationTheory/WicksTheorem.lean +++ b/HepLean/PerturbationTheory/WicksTheorem.lean @@ -16,10 +16,10 @@ Wick's theorem is related to Isserlis' theorem in mathematics. -/ namespace FieldSpecification -variable {𝓕 : FieldSpecification} {π“ž : 𝓕.OperatorAlgebra} +variable {𝓕 : FieldSpecification} {π“ž : 𝓕.ProtoOperatorAlgebra} open CrAnAlgebra open StateAlgebra -open OperatorAlgebra +open ProtoOperatorAlgebra open HepLean.List open WickContraction open FieldStatistic @@ -192,7 +192,7 @@ lemma sign_timeContract_normalOrder_insertList_some (Ο† : 𝓕.States) (Ο†s : Li simp only [Nat.succ_eq_add_one, Fin.getElem_fin, ite_mul, Algebra.smul_mul_assoc, instCommGroup.eq_1, contractStateAtIndex, uncontractedStatesEquiv, Equiv.optionCongr_apply, Equiv.coe_trans, Option.map_some', Function.comp_apply, finCongr_apply, Fin.coe_cast, - List.getElem_map, uncontractedList_getElem_uncontractedFinEquiv_symm, List.get_eq_getElem] + List.getElem_map, uncontractedList_getElem_uncontractedIndexEquiv_symm, List.get_eq_getElem] by_cases h1 : i < i.succAbove ↑k Β· simp only [h1, ↓reduceIte, MulMemClass.coe_mul] rw [timeContract_zero_of_diff_grade]