/- 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.FieldOpFreeAlgebra.SuperCommute import HepLean.PerturbationTheory.Koszul.KoszulSign /-! # Normal Ordering in the FieldOpFreeAlgebra In the module `HepLean.PerturbationTheory.FieldSpecification.NormalOrder` we defined the normal ordering of a list of `CrAnFieldOp`. In this module we extend the normal ordering to a linear map on `FieldOpFreeAlgebra`. We derive properties of this normal ordering. -/ namespace FieldSpecification variable {๐“• : FieldSpecification} open FieldStatistic namespace FieldOpFreeAlgebra noncomputable section /-- For a field specification `๐“•`, `normalOrderF` is the linear map `FieldOpFreeAlgebra ๐“• โ†’โ‚—[โ„‚] FieldOpFreeAlgebra ๐“•` defined by its action on the basis `ofCrAnListF ฯ†s`, taking `ofCrAnListF ฯ†s` to `normalOrderSign ฯ†s โ€ข ofCrAnListF (normalOrderList ฯ†s)`. That is, `normalOrderF` normal-orders the field operators and multiplies by the sign of the normal order. The notation `๐“แถ (a)` is used for `normalOrderF a` for `a` an element of `FieldOpFreeAlgebra ๐“•`. -/ def normalOrderF : FieldOpFreeAlgebra ๐“• โ†’โ‚—[โ„‚] FieldOpFreeAlgebra ๐“• := Basis.constr ofCrAnListFBasis โ„‚ fun ฯ†s => normalOrderSign ฯ†s โ€ข ofCrAnListF (normalOrderList ฯ†s) @[inherit_doc normalOrderF] scoped[FieldSpecification.FieldOpFreeAlgebra] notation "๐“แถ (" a ")" => normalOrderF a lemma normalOrderF_ofCrAnListF (ฯ†s : List ๐“•.CrAnFieldOp) : ๐“แถ (ofCrAnListF ฯ†s) = normalOrderSign ฯ†s โ€ข ofCrAnListF (normalOrderList ฯ†s) := by rw [โ† ofListBasis_eq_ofList, normalOrderF, Basis.constr_basis] lemma ofCrAnListF_eq_normalOrderF (ฯ†s : List ๐“•.CrAnFieldOp) : ofCrAnListF (normalOrderList ฯ†s) = normalOrderSign ฯ†s โ€ข ๐“แถ (ofCrAnListF ฯ†s) := by rw [normalOrderF_ofCrAnListF, normalOrderList, smul_smul, normalOrderSign, Wick.koszulSign_mul_self, one_smul] lemma normalOrderF_one : normalOrderF (๐“• := ๐“•) 1 = 1 := by rw [โ† ofCrAnListF_nil, normalOrderF_ofCrAnListF, normalOrderSign_nil, normalOrderList_nil, ofCrAnListF_nil, one_smul] lemma normalOrderF_normalOrderF_mid (a b c : ๐“•.FieldOpFreeAlgebra) : ๐“แถ (a * b * c) = ๐“แถ (a * ๐“แถ (b) * c) := by let pc (c : ๐“•.FieldOpFreeAlgebra) (hc : c โˆˆ Submodule.span โ„‚ (Set.range ofCrAnListFBasis)) : Prop := ๐“แถ (a * b * c) = ๐“แถ (a * ๐“แถ (b) * c) change pc c (Basis.mem_span _ c) apply Submodule.span_induction ยท intro x hx obtain โŸจฯ†s, rflโŸฉ := hx simp only [ofListBasis_eq_ofList, pc] let pb (b : ๐“•.FieldOpFreeAlgebra) (hb : b โˆˆ Submodule.span โ„‚ (Set.range ofCrAnListFBasis)) : Prop := ๐“แถ (a * b * ofCrAnListF ฯ†s) = ๐“แถ (a * ๐“แถ (b) * ofCrAnListF ฯ†s) change pb b (Basis.mem_span _ b) apply Submodule.span_induction ยท intro x hx obtain โŸจฯ†s', rflโŸฉ := hx simp only [ofListBasis_eq_ofList, pb] let pa (a : ๐“•.FieldOpFreeAlgebra) (ha : a โˆˆ Submodule.span โ„‚ (Set.range ofCrAnListFBasis)) : Prop := ๐“แถ (a * ofCrAnListF ฯ†s' * ofCrAnListF ฯ†s) = ๐“แถ (a * ๐“แถ (ofCrAnListF ฯ†s') * ofCrAnListF ฯ†s) change pa a (Basis.mem_span _ a) apply Submodule.span_induction ยท intro x hx obtain โŸจฯ†s'', rflโŸฉ := hx simp only [ofListBasis_eq_ofList, pa] rw [normalOrderF_ofCrAnListF] simp only [โ† ofCrAnListF_append, Algebra.mul_smul_comm, Algebra.smul_mul_assoc, map_smul] rw [normalOrderF_ofCrAnListF, normalOrderF_ofCrAnListF, smul_smul] congr 1 ยท simp only [normalOrderSign, normalOrderList] rw [Wick.koszulSign_of_append_eq_insertionSort, mul_comm] ยท congr 1 simp only [normalOrderList] rw [HepLean.List.insertionSort_append_insertionSort_append] ยท simp [pa] ยท intro x y hx hy h1 h2 simp_all [pa, add_mul] ยท intro x hx h simp_all [pa] ยท simp [pb] ยท intro x y hx hy h1 h2 simp_all [pb, mul_add, add_mul] ยท intro x hx h simp_all [pb] ยท simp [pc] ยท intro x y hx hy h1 h2 simp_all [pc, mul_add] ยท intro x hx h hp simp_all [pc] lemma normalOrderF_normalOrderF_right (a b : ๐“•.FieldOpFreeAlgebra) : ๐“แถ (a * b) = ๐“แถ (a * ๐“แถ (b)) := by trans ๐“แถ (a * b * 1) ยท simp ยท rw [normalOrderF_normalOrderF_mid] simp lemma normalOrderF_normalOrderF_left (a b : ๐“•.FieldOpFreeAlgebra) : ๐“แถ (a * b) = ๐“แถ (๐“แถ (a) * b) := by trans ๐“แถ (1 * a * b) ยท simp ยท rw [normalOrderF_normalOrderF_mid] simp /-! ## Normal ordering with a creation operator on the left or annihilation on the right -/ lemma normalOrderF_ofCrAnListF_cons_create (ฯ† : ๐“•.CrAnFieldOp) (hฯ† : ๐“• |>แถœ ฯ† = CreateAnnihilate.create) (ฯ†s : List ๐“•.CrAnFieldOp) : ๐“แถ (ofCrAnListF (ฯ† :: ฯ†s)) = ofCrAnOpF ฯ† * ๐“แถ (ofCrAnListF ฯ†s) := by rw [normalOrderF_ofCrAnListF, normalOrderSign_cons_create ฯ† hฯ†, normalOrderList_cons_create ฯ† hฯ† ฯ†s] rw [ofCrAnListF_cons, normalOrderF_ofCrAnListF, mul_smul_comm] lemma normalOrderF_create_mul (ฯ† : ๐“•.CrAnFieldOp) (hฯ† : ๐“• |>แถœ ฯ† = CreateAnnihilate.create) (a : FieldOpFreeAlgebra ๐“•) : ๐“แถ (ofCrAnOpF ฯ† * a) = ofCrAnOpF ฯ† * ๐“แถ (a) := by change (normalOrderF โˆ˜โ‚— mulLinearMap (ofCrAnOpF ฯ†)) a = (mulLinearMap (ofCrAnOpF ฯ†) โˆ˜โ‚— normalOrderF) a refine LinearMap.congr_fun (ofCrAnListFBasis.ext fun l โ†ฆ ?_) a simp only [mulLinearMap, LinearMap.coe_mk, AddHom.coe_mk, ofListBasis_eq_ofList, LinearMap.coe_comp, Function.comp_apply] rw [โ† ofCrAnListF_cons, normalOrderF_ofCrAnListF_cons_create ฯ† hฯ†] lemma normalOrderF_ofCrAnListF_append_annihilate (ฯ† : ๐“•.CrAnFieldOp) (hฯ† : ๐“• |>แถœ ฯ† = CreateAnnihilate.annihilate) (ฯ†s : List ๐“•.CrAnFieldOp) : ๐“แถ (ofCrAnListF (ฯ†s ++ [ฯ†])) = ๐“แถ (ofCrAnListF ฯ†s) * ofCrAnOpF ฯ† := by rw [normalOrderF_ofCrAnListF, normalOrderSign_append_annihilate ฯ† hฯ† ฯ†s, normalOrderList_append_annihilate ฯ† hฯ† ฯ†s, ofCrAnListF_append, ofCrAnListF_singleton, normalOrderF_ofCrAnListF, smul_mul_assoc] lemma normalOrderF_mul_annihilate (ฯ† : ๐“•.CrAnFieldOp) (hฯ† : ๐“• |>แถœ ฯ† = CreateAnnihilate.annihilate) (a : FieldOpFreeAlgebra ๐“•) : ๐“แถ (a * ofCrAnOpF ฯ†) = ๐“แถ (a) * ofCrAnOpF ฯ† := by change (normalOrderF โˆ˜โ‚— mulLinearMap.flip (ofCrAnOpF ฯ†)) a = (mulLinearMap.flip (ofCrAnOpF ฯ†) โˆ˜โ‚— normalOrderF) a refine LinearMap.congr_fun (ofCrAnListFBasis.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 [โ† ofCrAnListF_singleton, โ† ofCrAnListF_append, ofCrAnListF_singleton, normalOrderF_ofCrAnListF_append_annihilate ฯ† hฯ†] lemma normalOrderF_crPartF_mul (ฯ† : ๐“•.FieldOp) (a : FieldOpFreeAlgebra ๐“•) : ๐“แถ (crPartF ฯ† * a) = crPartF ฯ† * ๐“แถ (a) := by match ฯ† with | .inAsymp ฯ† => rw [crPartF] exact normalOrderF_create_mul โŸจFieldOp.inAsymp ฯ†, ()โŸฉ rfl a | .position ฯ† => rw [crPartF] exact normalOrderF_create_mul _ rfl _ | .outAsymp ฯ† => simp lemma normalOrderF_mul_anPartF (ฯ† : ๐“•.FieldOp) (a : FieldOpFreeAlgebra ๐“•) : ๐“แถ (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_annihilate_ofCrAnListF_ofCrAnListF (ฯ†c ฯ†a : ๐“•.CrAnFieldOp) (hฯ†c : ๐“• |>แถœ ฯ†c = CreateAnnihilate.create) (hฯ†a : ๐“• |>แถœ ฯ†a = CreateAnnihilate.annihilate) (ฯ†s ฯ†s' : List ๐“•.CrAnFieldOp) : ๐“แถ (ofCrAnListF ฯ†s' * ofCrAnOpF ฯ†c * ofCrAnOpF ฯ†a * ofCrAnListF ฯ†s) = ๐“ข(๐“• |>โ‚› ฯ†c, ๐“• |>โ‚› ฯ†a) โ€ข ๐“แถ (ofCrAnListF ฯ†s' * ofCrAnOpF ฯ†a * ofCrAnOpF ฯ†c * ofCrAnListF ฯ†s) := by rw [mul_assoc, mul_assoc, โ† ofCrAnListF_cons, โ† ofCrAnListF_cons, โ† ofCrAnListF_append] rw [normalOrderF_ofCrAnListF, normalOrderSign_swap_create_annihilate ฯ†c ฯ†a hฯ†c hฯ†a] rw [normalOrderList_swap_create_annihilate ฯ†c ฯ†a hฯ†c hฯ†a, โ† smul_smul, โ† normalOrderF_ofCrAnListF] rw [ofCrAnListF_append, ofCrAnListF_cons, ofCrAnListF_cons] noncomm_ring lemma normalOrderF_swap_create_annihilate_ofCrAnListF (ฯ†c ฯ†a : ๐“•.CrAnFieldOp) (hฯ†c : ๐“• |>แถœ ฯ†c = CreateAnnihilate.create) (hฯ†a : ๐“• |>แถœ ฯ†a = CreateAnnihilate.annihilate) (ฯ†s : List ๐“•.CrAnFieldOp) (a : ๐“•.FieldOpFreeAlgebra) : ๐“แถ (ofCrAnListF ฯ†s * ofCrAnOpF ฯ†c * ofCrAnOpF ฯ†a * a) = ๐“ข(๐“• |>โ‚› ฯ†c, ๐“• |>โ‚› ฯ†a) โ€ข ๐“แถ (ofCrAnListF ฯ†s * ofCrAnOpF ฯ†a * ofCrAnOpF ฯ†c * a) := by change (normalOrderF โˆ˜โ‚— mulLinearMap (ofCrAnListF ฯ†s * ofCrAnOpF ฯ†c * ofCrAnOpF ฯ†a)) a = (smulLinearMap _ โˆ˜โ‚— normalOrderF โˆ˜โ‚— mulLinearMap (ofCrAnListF ฯ†s * ofCrAnOpF ฯ†a * ofCrAnOpF ฯ†c)) a refine LinearMap.congr_fun (ofCrAnListFBasis.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_annihilate_ofCrAnListF_ofCrAnListF ฯ†c ฯ†a hฯ†c hฯ†a] rfl lemma normalOrderF_swap_create_annihilate (ฯ†c ฯ†a : ๐“•.CrAnFieldOp) (hฯ†c : ๐“• |>แถœ ฯ†c = CreateAnnihilate.create) (hฯ†a : ๐“• |>แถœ ฯ†a = CreateAnnihilate.annihilate) (a b : ๐“•.FieldOpFreeAlgebra) : ๐“แถ (a * ofCrAnOpF ฯ†c * ofCrAnOpF ฯ†a * b) = ๐“ข(๐“• |>โ‚› ฯ†c, ๐“• |>โ‚› ฯ†a) โ€ข ๐“แถ (a * ofCrAnOpF ฯ†a * ofCrAnOpF ฯ†c * b) := by rw [mul_assoc, mul_assoc, mul_assoc, mul_assoc] change (normalOrderF โˆ˜โ‚— mulLinearMap.flip (ofCrAnOpF ฯ†c * (ofCrAnOpF ฯ†a * b))) a = (smulLinearMap (๐“ข(๐“• |>โ‚› ฯ†c, ๐“• |>โ‚› ฯ†a)) โˆ˜โ‚— normalOrderF โˆ˜โ‚— mulLinearMap.flip (ofCrAnOpF ฯ†a * (ofCrAnOpF ฯ†c * b))) a refine LinearMap.congr_fun (ofCrAnListFBasis.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_annihilate_ofCrAnListF ฯ†c ฯ†a hฯ†c hฯ†a] rfl lemma normalOrderF_superCommuteF_create_annihilate (ฯ†c ฯ†a : ๐“•.CrAnFieldOp) (hฯ†c : ๐“• |>แถœ ฯ†c = CreateAnnihilate.create) (hฯ†a : ๐“• |>แถœ ฯ†a = CreateAnnihilate.annihilate) (a b : ๐“•.FieldOpFreeAlgebra) : ๐“แถ (a * [ofCrAnOpF ฯ†c, ofCrAnOpF ฯ†a]โ‚›F * b) = 0 := by simp only [superCommuteF_ofCrAnOpF_ofCrAnOpF, instCommGroup.eq_1, Algebra.smul_mul_assoc] rw [mul_sub, sub_mul, map_sub, โ† smul_mul_assoc, โ† mul_assoc, โ† mul_assoc, normalOrderF_swap_create_annihilate ฯ†c ฯ†a hฯ†c hฯ†a] simp lemma normalOrderF_superCommuteF_annihilate_create (ฯ†c ฯ†a : ๐“•.CrAnFieldOp) (hฯ†c : ๐“• |>แถœ ฯ†c = CreateAnnihilate.create) (hฯ†a : ๐“• |>แถœ ฯ†a = CreateAnnihilate.annihilate) (a b : ๐“•.FieldOpFreeAlgebra) : ๐“แถ (a * [ofCrAnOpF ฯ†a, ofCrAnOpF ฯ†c]โ‚›F * b) = 0 := by rw [superCommuteF_ofCrAnOpF_ofCrAnOpF_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 (ฯ† ฯ†' : ๐“•.FieldOp) (a b : FieldOpFreeAlgebra ๐“•) : ๐“แถ (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_annihilate] simp only [instCommGroup.eq_1, crAnStatistics, Function.comp_apply, crAnFieldOpToFieldOp_prod] rfl; rfl | .inAsymp ฯ†, .outAsymp ฯ†' => simp only [crPartF_negAsymp, anPartF_posAsymp, instCommGroup.eq_1] rw [normalOrderF_swap_create_annihilate] simp only [instCommGroup.eq_1, crAnStatistics, Function.comp_apply, crAnFieldOpToFieldOp_prod] rfl; rfl | .inAsymp ฯ†, .position ฯ†' => simp only [crPartF_negAsymp, anPartF_position, instCommGroup.eq_1] rw [normalOrderF_swap_create_annihilate] simp only [instCommGroup.eq_1, crAnStatistics, Function.comp_apply, crAnFieldOpToFieldOp_prod] rfl; rfl | .position ฯ†, .outAsymp ฯ†' => simp only [crPartF_position, anPartF_posAsymp, instCommGroup.eq_1] rw [normalOrderF_swap_create_annihilate] simp only [instCommGroup.eq_1, crAnStatistics, Function.comp_apply, crAnFieldOpToFieldOp_prod] rfl; rfl /-! ## Normal ordering for an anPartF and crPartF Using the results from above. -/ lemma normalOrderF_swap_anPartF_crPartF (ฯ† ฯ†' : ๐“•.FieldOp) (a b : FieldOpFreeAlgebra ๐“•) : ๐“แถ (a * (anPartF ฯ†) * (crPartF ฯ†') * b) = ๐“ข(๐“• |>โ‚› ฯ†, ๐“• |>โ‚› ฯ†') โ€ข ๐“แถ (a * (crPartF ฯ†') * (anPartF ฯ†) * b) := by simp [normalOrderF_swap_crPartF_anPartF, smul_smul] lemma normalOrderF_superCommuteF_crPartF_anPartF (ฯ† ฯ†' : ๐“•.FieldOp) (a b : FieldOpFreeAlgebra ๐“•) : ๐“แถ (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 (ฯ† ฯ†' : ๐“•.FieldOp) (a b : FieldOpFreeAlgebra ๐“•) : ๐“แถ (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 (ฯ† ฯ†' : ๐“•.FieldOp) : ๐“แถ (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 (ฯ† ฯ†' : ๐“•.FieldOp) : ๐“แถ (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 (ฯ† ฯ†' : ๐“•.FieldOp) : ๐“แถ (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 (ฯ† ฯ†' : ๐“•.FieldOp) : ๐“แถ (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_ofFieldOpF_mul_ofFieldOpF (ฯ† ฯ†' : ๐“•.FieldOp) : ๐“แถ (ofFieldOpF ฯ† * ofFieldOpF ฯ†') = crPartF ฯ† * crPartF ฯ†' + ๐“ข(๐“• |>โ‚› ฯ†, ๐“• |>โ‚› ฯ†') โ€ข (crPartF ฯ†' * anPartF ฯ†) + crPartF ฯ† * anPartF ฯ†' + anPartF ฯ† * anPartF ฯ†' := by rw [ofFieldOpF_eq_crPartF_add_anPartF, ofFieldOpF_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_ofCrAnListF_create_create_ofCrAnListF (ฯ†c ฯ†c' : ๐“•.CrAnFieldOp) (hฯ†c : ๐“• |>แถœ ฯ†c = CreateAnnihilate.create) (hฯ†c' : ๐“• |>แถœ ฯ†c' = CreateAnnihilate.create) (ฯ†s ฯ†s' : List ๐“•.CrAnFieldOp) : (๐“แถ (ofCrAnListF ฯ†s * [ofCrAnOpF ฯ†c, ofCrAnOpF ฯ†c']โ‚›F * ofCrAnListF ฯ†s')) = normalOrderSign (ฯ†s ++ ฯ†c' :: ฯ†c :: ฯ†s') โ€ข (ofCrAnListF (createFilter ฯ†s) * [ofCrAnOpF ฯ†c, ofCrAnOpF ฯ†c']โ‚›F * ofCrAnListF (createFilter ฯ†s') * ofCrAnListF (annihilateFilter (ฯ†s ++ ฯ†s'))) := by rw [superCommuteF_ofCrAnOpF_ofCrAnOpF, mul_sub, sub_mul, map_sub] conv_lhs => lhs; rhs rw [โ† ofCrAnListF_singleton, โ† ofCrAnListF_singleton, โ† ofCrAnListF_append, โ† ofCrAnListF_append, โ† ofCrAnListF_append] conv_lhs => lhs rw [normalOrderF_ofCrAnListF, 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 [โ† ofCrAnListF_singleton, โ† ofCrAnListF_singleton, โ† ofCrAnListF_append, โ† ofCrAnListF_append, โ† ofCrAnListF_append] conv_lhs => rhs rw [map_smul] rhs rw [normalOrderF_ofCrAnListF, 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, ofCrAnListF_append, ofCrAnListF_append, ofCrAnListF_append] conv_lhs => rhs; rhs rw [ofCrAnListF_append, ofCrAnListF_append, ofCrAnListF_append] rw [โ† smul_mul_assoc, โ† smul_mul_assoc, โ† Algebra.mul_smul_comm] rw [โ† sub_mul, โ† sub_mul, โ† mul_sub, ofCrAnListF_append, ofCrAnListF_singleton, ofCrAnListF_singleton] rw [ofCrAnListF_append, ofCrAnListF_singleton, ofCrAnListF_singleton, smul_mul_assoc] lemma normalOrderF_superCommuteF_ofCrAnListF_annihilate_annihilate_ofCrAnListF (ฯ†a ฯ†a' : ๐“•.CrAnFieldOp) (hฯ†a : ๐“• |>แถœ ฯ†a = CreateAnnihilate.annihilate) (hฯ†a' : ๐“• |>แถœ ฯ†a' = CreateAnnihilate.annihilate) (ฯ†s ฯ†s' : List ๐“•.CrAnFieldOp) : ๐“แถ (ofCrAnListF ฯ†s * [ofCrAnOpF ฯ†a, ofCrAnOpF ฯ†a']โ‚›F * ofCrAnListF ฯ†s') = normalOrderSign (ฯ†s ++ ฯ†a' :: ฯ†a :: ฯ†s') โ€ข (ofCrAnListF (createFilter (ฯ†s ++ ฯ†s')) * ofCrAnListF (annihilateFilter ฯ†s) * [ofCrAnOpF ฯ†a, ofCrAnOpF ฯ†a']โ‚›F * ofCrAnListF (annihilateFilter ฯ†s')) := by rw [superCommuteF_ofCrAnOpF_ofCrAnOpF, mul_sub, sub_mul, map_sub] conv_lhs => lhs; rhs rw [โ† ofCrAnListF_singleton, โ† ofCrAnListF_singleton, โ† ofCrAnListF_append, โ† ofCrAnListF_append, โ† ofCrAnListF_append] conv_lhs => lhs rw [normalOrderF_ofCrAnListF, 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 [โ† ofCrAnListF_singleton, โ† ofCrAnListF_singleton, โ† ofCrAnListF_append, โ† ofCrAnListF_append, โ† ofCrAnListF_append] conv_lhs => rhs rw [map_smul] rhs rw [normalOrderF_ofCrAnListF, 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, ofCrAnListF_append, ofCrAnListF_append, ofCrAnListF_append] conv_lhs => rhs; rhs rw [ofCrAnListF_append, ofCrAnListF_append, ofCrAnListF_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 [ofCrAnListF_append, ofCrAnListF_singleton, ofCrAnListF_singleton] rw [ofCrAnListF_append, ofCrAnListF_singleton, ofCrAnListF_singleton, smul_mul_assoc] /-! ## Super commututators involving a normal order. -/ lemma ofCrAnListF_superCommuteF_normalOrderF_ofCrAnListF (ฯ†s ฯ†s' : List ๐“•.CrAnFieldOp) : [ofCrAnListF ฯ†s, ๐“แถ (ofCrAnListF ฯ†s')]โ‚›F = ofCrAnListF ฯ†s * ๐“แถ (ofCrAnListF ฯ†s') - ๐“ข(๐“• |>โ‚› ฯ†s, ๐“• |>โ‚› ฯ†s') โ€ข ๐“แถ (ofCrAnListF ฯ†s') * ofCrAnListF ฯ†s := by simp only [normalOrderF_ofCrAnListF, map_smul, superCommuteF_ofCrAnListF_ofCrAnListF, ofCrAnListF_append, instCommGroup.eq_1, normalOrderList_statistics, smul_sub, smul_smul, Algebra.mul_smul_comm, mul_comm, Algebra.smul_mul_assoc] lemma ofCrAnListF_superCommuteF_normalOrderF_ofFieldOpListF (ฯ†s : List ๐“•.CrAnFieldOp) (ฯ†s' : List ๐“•.FieldOp) : [ofCrAnListF ฯ†s, ๐“แถ (ofFieldOpListF ฯ†s')]โ‚›F = ofCrAnListF ฯ†s * ๐“แถ (ofFieldOpListF ฯ†s') - ๐“ข(๐“• |>โ‚› ฯ†s, ๐“• |>โ‚› ฯ†s') โ€ข ๐“แถ (ofFieldOpListF ฯ†s') * ofCrAnListF ฯ†s := by rw [ofFieldOpListF_sum, map_sum, Finset.mul_sum, Finset.smul_sum, Finset.sum_mul, โ† Finset.sum_sub_distrib, map_sum] congr funext n rw [ofCrAnListF_superCommuteF_normalOrderF_ofCrAnListF, CrAnSection.statistics_eq_state_statistics] /-! ## Multiplications with normal order written in terms of super commute. -/ lemma ofCrAnListF_mul_normalOrderF_ofFieldOpListF_eq_superCommuteF (ฯ†s : List ๐“•.CrAnFieldOp) (ฯ†s' : List ๐“•.FieldOp) : ofCrAnListF ฯ†s * ๐“แถ (ofFieldOpListF ฯ†s') = ๐“ข(๐“• |>โ‚› ฯ†s, ๐“• |>โ‚› ฯ†s') โ€ข ๐“แถ (ofFieldOpListF ฯ†s') * ofCrAnListF ฯ†s + [ofCrAnListF ฯ†s, ๐“แถ (ofFieldOpListF ฯ†s')]โ‚›F := by simp [ofCrAnListF_superCommuteF_normalOrderF_ofFieldOpListF] lemma ofCrAnOpF_mul_normalOrderF_ofFieldOpListF_eq_superCommuteF (ฯ† : ๐“•.CrAnFieldOp) (ฯ†s' : List ๐“•.FieldOp) : ofCrAnOpF ฯ† * ๐“แถ (ofFieldOpListF ฯ†s') = ๐“ข(๐“• |>โ‚› ฯ†, ๐“• |>โ‚› ฯ†s') โ€ข ๐“แถ (ofFieldOpListF ฯ†s') * ofCrAnOpF ฯ† + [ofCrAnOpF ฯ†, ๐“แถ (ofFieldOpListF ฯ†s')]โ‚›F := by simp [โ† ofCrAnListF_singleton, ofCrAnListF_mul_normalOrderF_ofFieldOpListF_eq_superCommuteF] lemma anPartF_mul_normalOrderF_ofFieldOpListF_eq_superCommuteF (ฯ† : ๐“•.FieldOp) (ฯ†s' : List ๐“•.FieldOp) : anPartF ฯ† * ๐“แถ (ofFieldOpListF ฯ†s') = ๐“ข(๐“• |>โ‚› ฯ†, ๐“• |>โ‚› ฯ†s') โ€ข ๐“แถ (ofFieldOpListF ฯ†s' * anPartF ฯ†) + [anPartF ฯ†, ๐“แถ (ofFieldOpListF ฯ†s')]โ‚›F := by rw [normalOrderF_mul_anPartF] match ฯ† with | .inAsymp ฯ† => simp | .position ฯ† => simp [ofCrAnOpF_mul_normalOrderF_ofFieldOpListF_eq_superCommuteF, crAnStatistics] | .outAsymp ฯ† => simp [ofCrAnOpF_mul_normalOrderF_ofFieldOpListF_eq_superCommuteF, crAnStatistics] end end FieldOpFreeAlgebra end FieldSpecification