/- 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.NormalOrder import HepLean.PerturbationTheory.Algebras.CrAnAlgebra.SuperCommute 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 namespace CrAnAlgebra noncomputable section /-- The linear map on the free creation and annihlation algebra defined as the map taking a list of CrAnStates to the normal-ordered list of states multiplied by the sign corresponding to the number of fermionic-fermionic exchanges done in ordering. -/ def normalOrderF : CrAnAlgebra 𝓕 β†’β‚—[β„‚] CrAnAlgebra 𝓕 := Basis.constr ofCrAnListBasis β„‚ fun Ο†s => normalOrderSign Ο†s β€’ ofCrAnList (normalOrderList Ο†s) @[inherit_doc normalOrderF] scoped[FieldSpecification.CrAnAlgebra] notation "𝓝ᢠ(" a ")" => normalOrderF a lemma normalOrderF_ofCrAnList (Ο†s : List 𝓕.CrAnStates) : 𝓝ᢠ(ofCrAnList Ο†s) = normalOrderSign Ο†s β€’ ofCrAnList (normalOrderList Ο†s) := by rw [← ofListBasis_eq_ofList, normalOrderF, Basis.constr_basis] lemma ofCrAnList_eq_normalOrderF (Ο†s : List 𝓕.CrAnStates) : ofCrAnList (normalOrderList Ο†s) = normalOrderSign Ο†s β€’ 𝓝ᢠ(ofCrAnList Ο†s) := by rw [normalOrderF_ofCrAnList, normalOrderList, smul_smul, normalOrderSign, Wick.koszulSign_mul_self, one_smul] lemma normalOrderF_one : normalOrderF (𝓕 := 𝓕) 1 = 1 := by rw [← ofCrAnList_nil, normalOrderF_ofCrAnList, normalOrderSign_nil, normalOrderList_nil, ofCrAnList_nil, one_smul] /-! ## Normal ordering with a creation operator on the left or annihilation on the right -/ lemma normalOrderF_ofCrAnList_cons_create (Ο† : 𝓕.CrAnStates) (hΟ† : 𝓕 |>ᢜ Ο† = CreateAnnihilate.create) (Ο†s : List 𝓕.CrAnStates) : 𝓝ᢠ(ofCrAnList (Ο† :: Ο†s)) = ofCrAnState Ο† * 𝓝ᢠ(ofCrAnList Ο†s) := by rw [normalOrderF_ofCrAnList, normalOrderSign_cons_create Ο† hΟ†, normalOrderList_cons_create Ο† hΟ† Ο†s] rw [ofCrAnList_cons, normalOrderF_ofCrAnList, mul_smul_comm] lemma normalOrderF_create_mul (Ο† : 𝓕.CrAnStates) (hΟ† : 𝓕 |>ᢜ Ο† = CreateAnnihilate.create) (a : CrAnAlgebra 𝓕) : 𝓝ᢠ(ofCrAnState Ο† * a) = ofCrAnState Ο† * 𝓝ᢠ(a) := by change (normalOrderF βˆ˜β‚— mulLinearMap (ofCrAnState Ο†)) a = (mulLinearMap (ofCrAnState Ο†) βˆ˜β‚— normalOrderF) a refine LinearMap.congr_fun (ofCrAnListBasis.ext fun l ↦ ?_) a simp only [mulLinearMap, LinearMap.coe_mk, AddHom.coe_mk, ofListBasis_eq_ofList, LinearMap.coe_comp, Function.comp_apply] rw [← ofCrAnList_cons, normalOrderF_ofCrAnList_cons_create Ο† hΟ†] lemma normalOrderF_ofCrAnList_append_annihilate (Ο† : 𝓕.CrAnStates) (hΟ† : 𝓕 |>ᢜ Ο† = CreateAnnihilate.annihilate) (Ο†s : List 𝓕.CrAnStates) : 𝓝ᢠ(ofCrAnList (Ο†s ++ [Ο†])) = 𝓝ᢠ(ofCrAnList Ο†s) * ofCrAnState Ο† := by rw [normalOrderF_ofCrAnList, normalOrderSign_append_annihlate Ο† hΟ† Ο†s, normalOrderList_append_annihilate Ο† hΟ† Ο†s, ofCrAnList_append, ofCrAnList_singleton, normalOrderF_ofCrAnList, smul_mul_assoc] lemma normalOrderF_mul_annihilate (Ο† : 𝓕.CrAnStates) (hΟ† : 𝓕 |>ᢜ Ο† = CreateAnnihilate.annihilate) (a : CrAnAlgebra 𝓕) : 𝓝ᢠ(a * ofCrAnState Ο†) = 𝓝ᢠ(a) * ofCrAnState Ο† := by change (normalOrderF βˆ˜β‚— mulLinearMap.flip (ofCrAnState Ο†)) a = (mulLinearMap.flip (ofCrAnState Ο†) βˆ˜β‚— normalOrderF) a refine LinearMap.congr_fun (ofCrAnListBasis.ext fun l ↦ ?_) a simp only [mulLinearMap, ofListBasis_eq_ofList, LinearMap.coe_comp, Function.comp_apply, LinearMap.flip_apply, LinearMap.coe_mk, AddHom.coe_mk] rw [← ofCrAnList_singleton, ← ofCrAnList_append, ofCrAnList_singleton, normalOrderF_ofCrAnList_append_annihilate Ο† hΟ†] lemma normalOrderF_crPartF_mul (Ο† : 𝓕.States) (a : CrAnAlgebra 𝓕) : 𝓝ᢠ(crPartF Ο† * a) = crPartF Ο† * 𝓝ᢠ(a) := by match Ο† with | .inAsymp Ο† => rw [crPartF] exact normalOrderF_create_mul ⟨States.inAsymp Ο†, ()⟩ rfl a | .position Ο† => rw [crPartF] exact normalOrderF_create_mul _ rfl _ | .outAsymp Ο† => simp lemma normalOrderF_mul_anPartF (Ο† : 𝓕.States) (a : CrAnAlgebra 𝓕) : 𝓝ᢠ(a * anPartF Ο†) = 𝓝ᢠ(a) * anPartF Ο† := by match Ο† with | .inAsymp Ο† => simp | .position Ο† => rw [anPartF] exact normalOrderF_mul_annihilate _ rfl _ | .outAsymp Ο† => rw [anPartF] refine normalOrderF_mul_annihilate _ rfl _ /-! ## Normal ordering for an adjacent creation and annihliation state The main result of this section is `normalOrderF_superCommuteF_annihilate_create`. -/ lemma normalOrderF_swap_create_annihlate_ofCrAnList_ofCrAnList (Ο†c Ο†a : 𝓕.CrAnStates) (hΟ†c : 𝓕 |>ᢜ Ο†c = CreateAnnihilate.create) (hΟ†a : 𝓕 |>ᢜ Ο†a = CreateAnnihilate.annihilate) (Ο†s Ο†s' : List 𝓕.CrAnStates) : 𝓝ᢠ(ofCrAnList Ο†s' * ofCrAnState Ο†c * ofCrAnState Ο†a * ofCrAnList Ο†s) = 𝓒(𝓕 |>β‚› Ο†c, 𝓕 |>β‚› Ο†a) β€’ 𝓝ᢠ(ofCrAnList Ο†s' * ofCrAnState Ο†a * ofCrAnState Ο†c * ofCrAnList Ο†s) := by rw [mul_assoc, mul_assoc, ← ofCrAnList_cons, ← ofCrAnList_cons, ← ofCrAnList_append] rw [normalOrderF_ofCrAnList, normalOrderSign_swap_create_annihlate Ο†c Ο†a hΟ†c hΟ†a] rw [normalOrderList_swap_create_annihlate Ο†c Ο†a hΟ†c hΟ†a, ← smul_smul, ← normalOrderF_ofCrAnList] rw [ofCrAnList_append, ofCrAnList_cons, ofCrAnList_cons] noncomm_ring lemma normalOrderF_swap_create_annihlate_ofCrAnList (Ο†c Ο†a : 𝓕.CrAnStates) (hΟ†c : 𝓕 |>ᢜ Ο†c = CreateAnnihilate.create) (hΟ†a : 𝓕 |>ᢜ Ο†a = CreateAnnihilate.annihilate) (Ο†s : List 𝓕.CrAnStates) (a : 𝓕.CrAnAlgebra) : 𝓝ᢠ(ofCrAnList Ο†s * ofCrAnState Ο†c * ofCrAnState Ο†a * a) = 𝓒(𝓕 |>β‚› Ο†c, 𝓕 |>β‚› Ο†a) β€’ 𝓝ᢠ(ofCrAnList Ο†s * ofCrAnState Ο†a * ofCrAnState Ο†c * a) := by change (normalOrderF βˆ˜β‚— mulLinearMap (ofCrAnList Ο†s * ofCrAnState Ο†c * ofCrAnState Ο†a)) a = (smulLinearMap _ βˆ˜β‚— normalOrderF βˆ˜β‚— mulLinearMap (ofCrAnList Ο†s * ofCrAnState Ο†a * ofCrAnState Ο†c)) a refine LinearMap.congr_fun (ofCrAnListBasis.ext fun l ↦ ?_) a simp only [mulLinearMap, LinearMap.coe_mk, AddHom.coe_mk, ofListBasis_eq_ofList, LinearMap.coe_comp, Function.comp_apply, instCommGroup.eq_1] rw [normalOrderF_swap_create_annihlate_ofCrAnList_ofCrAnList Ο†c Ο†a hΟ†c hΟ†a] rfl lemma normalOrderF_swap_create_annihlate (Ο†c Ο†a : 𝓕.CrAnStates) (hΟ†c : 𝓕 |>ᢜ Ο†c = CreateAnnihilate.create) (hΟ†a : 𝓕 |>ᢜ Ο†a = CreateAnnihilate.annihilate) (a b : 𝓕.CrAnAlgebra) : 𝓝ᢠ(a * ofCrAnState Ο†c * ofCrAnState Ο†a * b) = 𝓒(𝓕 |>β‚› Ο†c, 𝓕 |>β‚› Ο†a) β€’ 𝓝ᢠ(a * ofCrAnState Ο†a * ofCrAnState Ο†c * b) := by rw [mul_assoc, mul_assoc, mul_assoc, mul_assoc] change (normalOrderF βˆ˜β‚— mulLinearMap.flip (ofCrAnState Ο†c * (ofCrAnState Ο†a * b))) a = (smulLinearMap (𝓒(𝓕 |>β‚› Ο†c, 𝓕 |>β‚› Ο†a)) βˆ˜β‚— normalOrderF βˆ˜β‚— mulLinearMap.flip (ofCrAnState Ο†a * (ofCrAnState Ο†c * b))) a refine LinearMap.congr_fun (ofCrAnListBasis.ext fun l ↦ ?_) _ simp only [mulLinearMap, ofListBasis_eq_ofList, LinearMap.coe_comp, Function.comp_apply, LinearMap.flip_apply, LinearMap.coe_mk, AddHom.coe_mk, instCommGroup.eq_1, ← mul_assoc, normalOrderF_swap_create_annihlate_ofCrAnList Ο†c Ο†a hΟ†c hΟ†a] rfl lemma normalOrderF_superCommuteF_create_annihilate (Ο†c Ο†a : 𝓕.CrAnStates) (hΟ†c : 𝓕 |>ᢜ Ο†c = CreateAnnihilate.create) (hΟ†a : 𝓕 |>ᢜ Ο†a = CreateAnnihilate.annihilate) (a b : 𝓕.CrAnAlgebra) : 𝓝ᢠ(a * [ofCrAnState Ο†c, ofCrAnState Ο†a]β‚›ca * b) = 0 := by simp only [superCommuteF_ofCrAnState_ofCrAnState, instCommGroup.eq_1, Algebra.smul_mul_assoc] rw [mul_sub, sub_mul, map_sub, ← smul_mul_assoc, ← mul_assoc, ← mul_assoc, normalOrderF_swap_create_annihlate Ο†c Ο†a hΟ†c hΟ†a] simp lemma normalOrderF_superCommuteF_annihilate_create (Ο†c Ο†a : 𝓕.CrAnStates) (hΟ†c : 𝓕 |>ᢜ Ο†c = CreateAnnihilate.create) (hΟ†a : 𝓕 |>ᢜ Ο†a = CreateAnnihilate.annihilate) (a b : 𝓕.CrAnAlgebra) : 𝓝ᢠ(a * [ofCrAnState Ο†a, ofCrAnState Ο†c]β‚›ca * b) = 0 := by rw [superCommuteF_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] exact Or.inr (normalOrderF_superCommuteF_create_annihilate Ο†c Ο†a hΟ†c hΟ†a ..) lemma normalOrderF_swap_crPartF_anPartF (Ο† Ο†' : 𝓕.States) (a b : CrAnAlgebra 𝓕) : 𝓝ᢠ(a * (crPartF Ο†) * (anPartF Ο†') * b) = 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› Ο†') β€’ 𝓝ᢠ(a * (anPartF Ο†') * (crPartF Ο†) * b) := by match Ο†, Ο†' with | _, .inAsymp Ο†' => simp | .outAsymp Ο†, _ => simp | .position Ο†, .position Ο†' => simp only [crPartF_position, anPartF_position, instCommGroup.eq_1] rw [normalOrderF_swap_create_annihlate] simp only [instCommGroup.eq_1, crAnStatistics, Function.comp_apply, crAnStatesToStates_prod] rfl; rfl | .inAsymp Ο†, .outAsymp Ο†' => simp only [crPartF_negAsymp, anPartF_posAsymp, instCommGroup.eq_1] rw [normalOrderF_swap_create_annihlate] simp only [instCommGroup.eq_1, crAnStatistics, Function.comp_apply, crAnStatesToStates_prod] rfl; rfl | .inAsymp Ο†, .position Ο†' => simp only [crPartF_negAsymp, anPartF_position, instCommGroup.eq_1] rw [normalOrderF_swap_create_annihlate] simp only [instCommGroup.eq_1, crAnStatistics, Function.comp_apply, crAnStatesToStates_prod] rfl; rfl | .position Ο†, .outAsymp Ο†' => simp only [crPartF_position, anPartF_posAsymp, instCommGroup.eq_1] rw [normalOrderF_swap_create_annihlate] simp only [instCommGroup.eq_1, crAnStatistics, Function.comp_apply, crAnStatesToStates_prod] rfl; rfl /-! ## Normal ordering for an anPartF and crPartF Using the results from above. -/ lemma normalOrderF_swap_anPartF_crPartF (Ο† Ο†' : 𝓕.States) (a b : CrAnAlgebra 𝓕) : 𝓝ᢠ(a * (anPartF Ο†) * (crPartF Ο†') * b) = 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› Ο†') β€’ 𝓝ᢠ(a * (crPartF Ο†') * (anPartF Ο†) * b) := by simp [normalOrderF_swap_crPartF_anPartF, smul_smul] lemma normalOrderF_superCommuteF_crPartF_anPartF (Ο† Ο†' : 𝓕.States) (a b : CrAnAlgebra 𝓕) : 𝓝ᢠ(a * superCommuteF (crPartF Ο†) (anPartF Ο†') * b) = 0 := by match Ο†, Ο†' with | _, .inAsymp Ο†' => simp | .outAsymp Ο†', _ => simp | .position Ο†, .position Ο†' => rw [crPartF_position, anPartF_position] exact normalOrderF_superCommuteF_create_annihilate _ _ rfl rfl .. | .inAsymp Ο†, .outAsymp Ο†' => rw [crPartF_negAsymp, anPartF_posAsymp] exact normalOrderF_superCommuteF_create_annihilate _ _ rfl rfl .. | .inAsymp Ο†, .position Ο†' => rw [crPartF_negAsymp, anPartF_position] exact normalOrderF_superCommuteF_create_annihilate _ _ rfl rfl .. | .position Ο†, .outAsymp Ο†' => rw [crPartF_position, anPartF_posAsymp] exact normalOrderF_superCommuteF_create_annihilate _ _ rfl rfl .. lemma normalOrderF_superCommuteF_anPartF_crPartF (Ο† Ο†' : 𝓕.States) (a b : CrAnAlgebra 𝓕) : 𝓝ᢠ(a * superCommuteF (anPartF Ο†) (crPartF Ο†') * b) = 0 := by match Ο†, Ο†' with | .inAsymp Ο†', _ => simp | _, .outAsymp Ο†' => simp | .position Ο†, .position Ο†' => rw [anPartF_position, crPartF_position] exact normalOrderF_superCommuteF_annihilate_create _ _ rfl rfl .. | .outAsymp Ο†', .inAsymp Ο† => simp only [anPartF_posAsymp, crPartF_negAsymp] exact normalOrderF_superCommuteF_annihilate_create _ _ rfl rfl .. | .position Ο†', .inAsymp Ο† => simp only [anPartF_position, crPartF_negAsymp] exact normalOrderF_superCommuteF_annihilate_create _ _ rfl rfl .. | .outAsymp Ο†, .position Ο†' => simp only [anPartF_posAsymp, crPartF_position] exact normalOrderF_superCommuteF_annihilate_create _ _ rfl rfl .. /-! ## The normal ordering of a product of two states -/ @[simp] lemma normalOrderF_crPartF_mul_crPartF (Ο† Ο†' : 𝓕.States) : 𝓝ᢠ(crPartF Ο† * crPartF Ο†') = crPartF Ο† * crPartF Ο†' := by rw [normalOrderF_crPartF_mul] conv_lhs => rw [← mul_one (crPartF Ο†')] rw [normalOrderF_crPartF_mul, normalOrderF_one] simp @[simp] lemma normalOrderF_anPartF_mul_anPartF (Ο† Ο†' : 𝓕.States) : 𝓝ᢠ(anPartF Ο† * anPartF Ο†') = anPartF Ο† * anPartF Ο†' := by rw [normalOrderF_mul_anPartF] conv_lhs => rw [← one_mul (anPartF Ο†)] rw [normalOrderF_mul_anPartF, normalOrderF_one] simp @[simp] lemma normalOrderF_crPartF_mul_anPartF (Ο† Ο†' : 𝓕.States) : 𝓝ᢠ(crPartF Ο† * anPartF Ο†') = crPartF Ο† * anPartF Ο†' := by rw [normalOrderF_crPartF_mul] conv_lhs => rw [← one_mul (anPartF Ο†')] rw [normalOrderF_mul_anPartF, normalOrderF_one] simp @[simp] lemma normalOrderF_anPartF_mul_crPartF (Ο† Ο†' : 𝓕.States) : 𝓝ᢠ(anPartF Ο† * crPartF Ο†') = 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› Ο†') β€’ (crPartF Ο†' * anPartF Ο†) := by conv_lhs => rw [← one_mul (anPartF Ο† * crPartF Ο†')] conv_lhs => rw [← mul_one (1 * (anPartF Ο† * crPartF Ο†'))] rw [← mul_assoc, normalOrderF_swap_anPartF_crPartF] simp lemma normalOrderF_ofState_mul_ofState (Ο† Ο†' : 𝓕.States) : 𝓝ᢠ(ofState Ο† * ofState Ο†') = crPartF Ο† * crPartF Ο†' + 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› Ο†') β€’ (crPartF Ο†' * anPartF Ο†) + crPartF Ο† * anPartF Ο†' + anPartF Ο† * anPartF Ο†' := by rw [ofState_eq_crPartF_add_anPartF, ofState_eq_crPartF_add_anPartF, mul_add, add_mul, add_mul] simp only [map_add, normalOrderF_crPartF_mul_crPartF, normalOrderF_anPartF_mul_crPartF, instCommGroup.eq_1, normalOrderF_crPartF_mul_anPartF, normalOrderF_anPartF_mul_anPartF] abel /-! ## Normal order with super commutors -/ TODO "Split the following two lemmas up into smaller parts." lemma normalOrderF_superCommuteF_ofCrAnList_create_create_ofCrAnList (Ο†c Ο†c' : 𝓕.CrAnStates) (hΟ†c : 𝓕 |>ᢜ Ο†c = CreateAnnihilate.create) (hΟ†c' : 𝓕 |>ᢜ Ο†c' = CreateAnnihilate.create) (Ο†s Ο†s' : List 𝓕.CrAnStates) : (𝓝ᢠ(ofCrAnList Ο†s * [ofCrAnState Ο†c, ofCrAnState Ο†c']β‚›ca * ofCrAnList Ο†s')) = normalOrderSign (Ο†s ++ Ο†c' :: Ο†c :: Ο†s') β€’ (ofCrAnList (createFilter Ο†s) * [ofCrAnState Ο†c, ofCrAnState Ο†c']β‚›ca * ofCrAnList (createFilter Ο†s') * ofCrAnList (annihilateFilter (Ο†s ++ Ο†s'))) := by rw [superCommuteF_ofCrAnState_ofCrAnState, mul_sub, sub_mul, map_sub] conv_lhs => lhs; rhs rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, ← ofCrAnList_append, ← ofCrAnList_append, ← ofCrAnList_append] conv_lhs => lhs rw [normalOrderF_ofCrAnList, normalOrderList_eq_createFilter_append_annihilateFilter] rw [createFilter_append, createFilter_append, createFilter_append, createFilter_singleton_create _ hΟ†c, createFilter_singleton_create _ hΟ†c'] rw [annihilateFilter_append, annihilateFilter_append, annihilateFilter_append, annihilateFilter_singleton_create _ hΟ†c, annihilateFilter_singleton_create _ hΟ†c'] enter [2, 1, 2] simp only [List.singleton_append, List.append_assoc, List.cons_append, List.append_nil, instCommGroup.eq_1, Algebra.smul_mul_assoc, Algebra.mul_smul_comm, map_smul] rw [← annihilateFilter_append] conv_lhs => rhs; rhs rw [smul_mul_assoc, Algebra.mul_smul_comm, smul_mul_assoc] rhs rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, ← ofCrAnList_append, ← ofCrAnList_append, ← ofCrAnList_append] conv_lhs => rhs rw [map_smul] rhs rw [normalOrderF_ofCrAnList, normalOrderList_eq_createFilter_append_annihilateFilter] rw [createFilter_append, createFilter_append, createFilter_append, createFilter_singleton_create _ hΟ†c, createFilter_singleton_create _ hΟ†c'] rw [annihilateFilter_append, annihilateFilter_append, annihilateFilter_append, annihilateFilter_singleton_create _ hΟ†c, annihilateFilter_singleton_create _ hΟ†c'] enter [2, 1, 2] simp only [List.singleton_append, List.append_assoc, List.cons_append, instCommGroup.eq_1, List.append_nil, Algebra.smul_mul_assoc] rw [← annihilateFilter_append] conv_lhs => lhs; lhs simp conv_lhs => rhs; rhs; lhs simp rw [normalOrderSign_swap_create_create Ο†c Ο†c' hΟ†c hΟ†c'] rw [smul_smul, mul_comm, ← smul_smul] rw [← smul_sub, ofCrAnList_append, ofCrAnList_append, ofCrAnList_append] conv_lhs => rhs; rhs rw [ofCrAnList_append, ofCrAnList_append, ofCrAnList_append] rw [← smul_mul_assoc, ← smul_mul_assoc, ← Algebra.mul_smul_comm] rw [← sub_mul, ← sub_mul, ← mul_sub, ofCrAnList_append, ofCrAnList_singleton, ofCrAnList_singleton] rw [ofCrAnList_append, ofCrAnList_singleton, ofCrAnList_singleton, smul_mul_assoc] lemma normalOrderF_superCommuteF_ofCrAnList_annihilate_annihilate_ofCrAnList (Ο†a Ο†a' : 𝓕.CrAnStates) (hΟ†a : 𝓕 |>ᢜ Ο†a = CreateAnnihilate.annihilate) (hΟ†a' : 𝓕 |>ᢜ Ο†a' = CreateAnnihilate.annihilate) (Ο†s Ο†s' : List 𝓕.CrAnStates) : 𝓝ᢠ(ofCrAnList Ο†s * [ofCrAnState Ο†a, ofCrAnState Ο†a']β‚›ca * ofCrAnList Ο†s') = normalOrderSign (Ο†s ++ Ο†a' :: Ο†a :: Ο†s') β€’ (ofCrAnList (createFilter (Ο†s ++ Ο†s')) * ofCrAnList (annihilateFilter Ο†s) * [ofCrAnState Ο†a, ofCrAnState Ο†a']β‚›ca * ofCrAnList (annihilateFilter Ο†s')) := by rw [superCommuteF_ofCrAnState_ofCrAnState, mul_sub, sub_mul, map_sub] conv_lhs => lhs; rhs rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, ← ofCrAnList_append, ← ofCrAnList_append, ← ofCrAnList_append] conv_lhs => lhs rw [normalOrderF_ofCrAnList, normalOrderList_eq_createFilter_append_annihilateFilter] rw [createFilter_append, createFilter_append, createFilter_append, createFilter_singleton_annihilate _ hΟ†a, createFilter_singleton_annihilate _ hΟ†a'] rw [annihilateFilter_append, annihilateFilter_append, annihilateFilter_append, annihilateFilter_singleton_annihilate _ hΟ†a, annihilateFilter_singleton_annihilate _ hΟ†a'] enter [2, 1, 1] simp only [List.singleton_append, List.append_assoc, List.cons_append, List.append_nil, instCommGroup.eq_1, Algebra.smul_mul_assoc, Algebra.mul_smul_comm, map_smul] rw [← createFilter_append] conv_lhs => rhs; rhs rw [smul_mul_assoc] rw [Algebra.mul_smul_comm, smul_mul_assoc] rhs rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, ← ofCrAnList_append, ← ofCrAnList_append, ← ofCrAnList_append] conv_lhs => rhs rw [map_smul] rhs rw [normalOrderF_ofCrAnList, normalOrderList_eq_createFilter_append_annihilateFilter] rw [createFilter_append, createFilter_append, createFilter_append, createFilter_singleton_annihilate _ hΟ†a, createFilter_singleton_annihilate _ hΟ†a'] rw [annihilateFilter_append, annihilateFilter_append, annihilateFilter_append, annihilateFilter_singleton_annihilate _ hΟ†a, annihilateFilter_singleton_annihilate _ hΟ†a'] enter [2, 1, 1] simp only [List.singleton_append, List.append_assoc, List.cons_append, instCommGroup.eq_1, List.append_nil, Algebra.smul_mul_assoc] rw [← createFilter_append] conv_lhs => lhs; lhs simp conv_lhs => rhs; rhs; lhs simp rw [normalOrderSign_swap_annihilate_annihilate Ο†a Ο†a' hΟ†a hΟ†a'] rw [smul_smul, mul_comm, ← smul_smul] rw [← smul_sub, ofCrAnList_append, ofCrAnList_append, ofCrAnList_append] conv_lhs => rhs; rhs rw [ofCrAnList_append, ofCrAnList_append, ofCrAnList_append] rw [← Algebra.mul_smul_comm, ← smul_mul_assoc, ← Algebra.mul_smul_comm] rw [← mul_sub, ← sub_mul, ← mul_sub] apply congrArg conv_rhs => rw [mul_assoc, mul_assoc] apply congrArg rw [mul_assoc] apply congrArg rw [ofCrAnList_append, ofCrAnList_singleton, ofCrAnList_singleton] rw [ofCrAnList_append, ofCrAnList_singleton, ofCrAnList_singleton, smul_mul_assoc] /-! ## Super commututators involving a normal order. -/ lemma ofCrAnList_superCommuteF_normalOrderF_ofCrAnList (Ο†s Ο†s' : List 𝓕.CrAnStates) : [ofCrAnList Ο†s, 𝓝ᢠ(ofCrAnList Ο†s')]β‚›ca = ofCrAnList Ο†s * 𝓝ᢠ(ofCrAnList Ο†s') - 𝓒(𝓕 |>β‚› Ο†s, 𝓕 |>β‚› Ο†s') β€’ 𝓝ᢠ(ofCrAnList Ο†s') * ofCrAnList Ο†s := by simp [normalOrderF_ofCrAnList, map_smul, superCommuteF_ofCrAnList_ofCrAnList, ofCrAnList_append, smul_sub, smul_smul, mul_comm] lemma ofCrAnList_superCommuteF_normalOrderF_ofStateList (Ο†s : List 𝓕.CrAnStates) (Ο†s' : List 𝓕.States) : [ofCrAnList Ο†s, 𝓝ᢠ(ofStateList Ο†s')]β‚›ca = ofCrAnList Ο†s * 𝓝ᢠ(ofStateList Ο†s') - 𝓒(𝓕 |>β‚› Ο†s, 𝓕 |>β‚› Ο†s') β€’ 𝓝ᢠ(ofStateList Ο†s') * ofCrAnList Ο†s := by rw [ofStateList_sum, map_sum, Finset.mul_sum, Finset.smul_sum, Finset.sum_mul, ← Finset.sum_sub_distrib, map_sum] congr funext n rw [ofCrAnList_superCommuteF_normalOrderF_ofCrAnList, CrAnSection.statistics_eq_state_statistics] /-! ## Multiplications with normal order written in terms of super commute. -/ lemma ofCrAnList_mul_normalOrderF_ofStateList_eq_superCommuteF (Ο†s : List 𝓕.CrAnStates) (Ο†s' : List 𝓕.States) : ofCrAnList Ο†s * 𝓝ᢠ(ofStateList Ο†s') = 𝓒(𝓕 |>β‚› Ο†s, 𝓕 |>β‚› Ο†s') β€’ 𝓝ᢠ(ofStateList Ο†s') * ofCrAnList Ο†s + [ofCrAnList Ο†s, 𝓝ᢠ(ofStateList Ο†s')]β‚›ca := by simp [ofCrAnList_superCommuteF_normalOrderF_ofStateList] lemma ofCrAnState_mul_normalOrderF_ofStateList_eq_superCommuteF (Ο† : 𝓕.CrAnStates) (Ο†s' : List 𝓕.States) : ofCrAnState Ο† * 𝓝ᢠ(ofStateList Ο†s') = 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› Ο†s') β€’ 𝓝ᢠ(ofStateList Ο†s') * ofCrAnState Ο† + [ofCrAnState Ο†, 𝓝ᢠ(ofStateList Ο†s')]β‚›ca := by simp [← ofCrAnList_singleton, ofCrAnList_mul_normalOrderF_ofStateList_eq_superCommuteF] lemma anPartF_mul_normalOrderF_ofStateList_eq_superCommuteF (Ο† : 𝓕.States) (Ο†s' : List 𝓕.States) : anPartF Ο† * 𝓝ᢠ(ofStateList Ο†s') = 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› Ο†s') β€’ 𝓝ᢠ(ofStateList Ο†s' * anPartF Ο†) + [anPartF Ο†, 𝓝ᢠ(ofStateList Ο†s')]β‚›ca := by rw [normalOrderF_mul_anPartF] match Ο† with | .inAsymp Ο† => simp | .position Ο† => simp [ofCrAnState_mul_normalOrderF_ofStateList_eq_superCommuteF, crAnStatistics] | .outAsymp Ο† => simp [ofCrAnState_mul_normalOrderF_ofStateList_eq_superCommuteF, crAnStatistics] end end CrAnAlgebra end FieldSpecification