/- 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.FieldOpFreeAlgebra.NormalOrder import HepLean.PerturbationTheory.Algebras.FieldOpAlgebra.SuperCommute /-! # Normal Ordering on Field operator algebra -/ namespace FieldSpecification open FieldOpFreeAlgebra open HepLean.List open FieldStatistic namespace FieldOpAlgebra variable {๐“• : FieldSpecification} /-! ## Normal order on super-commutators. The main result of this is `ฮน_normalOrderF_superCommuteF_eq_zero_mul` which states that applying `ฮน` to the normal order of something containing a super-commutator is zero. -/ lemma ฮน_normalOrderF_superCommuteF_ofCrAnList_ofCrAnList_eq_zero (ฯ†a ฯ†a' : ๐“•.CrAnStates) (ฯ†s ฯ†s' : List ๐“•.CrAnStates) : ฮน ๐“แถ (ofCrAnList ฯ†s * [ofCrAnState ฯ†a, ofCrAnState ฯ†a']โ‚›ca * ofCrAnList ฯ†s') = 0 := by rcases CreateAnnihilate.eq_create_or_annihilate (๐“• |>แถœ ฯ†a) with hฯ†a | hฯ†a <;> rcases CreateAnnihilate.eq_create_or_annihilate (๐“• |>แถœ ฯ†a') with hฯ†a' | hฯ†a' ยท rw [normalOrderF_superCommuteF_ofCrAnList_create_create_ofCrAnList ฯ†a ฯ†a' hฯ†a hฯ†a' ฯ†s ฯ†s'] rw [map_smul, map_mul, map_mul, map_mul, ฮน_superCommuteF_of_create_create ฯ†a ฯ†a' hฯ†a hฯ†a'] simp ยท rw [normalOrderF_superCommuteF_create_annihilate ฯ†a ฯ†a' hฯ†a hฯ†a' (ofCrAnList ฯ†s) (ofCrAnList ฯ†s')] simp ยท rw [normalOrderF_superCommuteF_annihilate_create ฯ†a' ฯ†a hฯ†a' hฯ†a (ofCrAnList ฯ†s) (ofCrAnList ฯ†s')] simp ยท rw [normalOrderF_superCommuteF_ofCrAnList_annihilate_annihilate_ofCrAnList ฯ†a ฯ†a' hฯ†a hฯ†a' ฯ†s ฯ†s'] rw [map_smul, map_mul, map_mul, map_mul, ฮน_superCommuteF_of_annihilate_annihilate ฯ†a ฯ†a' hฯ†a hฯ†a'] simp lemma ฮน_normalOrderF_superCommuteF_ofCrAnList_eq_zero (ฯ†a ฯ†a' : ๐“•.CrAnStates) (ฯ†s : List ๐“•.CrAnStates) (a : ๐“•.FieldOpFreeAlgebra) : ฮน ๐“แถ (ofCrAnList ฯ†s * [ofCrAnState ฯ†a, ofCrAnState ฯ†a']โ‚›ca * a) = 0 := by have hf : ฮน.toLinearMap โˆ˜โ‚— normalOrderF โˆ˜โ‚— mulLinearMap (ofCrAnList ฯ†s * [ofCrAnState ฯ†a, ofCrAnState ฯ†a']โ‚›ca) = 0 := by apply ofCrAnListBasis.ext intro l simp only [FieldOpFreeAlgebra.ofListBasis_eq_ofList, LinearMap.coe_comp, Function.comp_apply, AlgHom.toLinearMap_apply, LinearMap.zero_apply] exact ฮน_normalOrderF_superCommuteF_ofCrAnList_ofCrAnList_eq_zero ฯ†a ฯ†a' ฯ†s l change (ฮน.toLinearMap โˆ˜โ‚— normalOrderF โˆ˜โ‚— mulLinearMap ((ofCrAnList ฯ†s * [ofCrAnState ฯ†a, ofCrAnState ฯ†a']โ‚›ca))) a = 0 rw [hf] simp lemma ฮน_normalOrderF_superCommuteF_ofCrAnState_eq_zero_mul (ฯ†a ฯ†a' : ๐“•.CrAnStates) (a b : ๐“•.FieldOpFreeAlgebra) : ฮน ๐“แถ (a * [ofCrAnState ฯ†a, ofCrAnState ฯ†a']โ‚›ca * b) = 0 := by rw [mul_assoc] change (ฮน.toLinearMap โˆ˜โ‚— normalOrderF โˆ˜โ‚— mulLinearMap.flip ([ofCrAnState ฯ†a, ofCrAnState ฯ†a']โ‚›ca * b)) a = 0 have hf : ฮน.toLinearMap โˆ˜โ‚— normalOrderF โˆ˜โ‚— mulLinearMap.flip ([ofCrAnState ฯ†a, ofCrAnState ฯ†a']โ‚›ca * b) = 0 := by apply ofCrAnListBasis.ext intro l simp only [mulLinearMap, FieldOpFreeAlgebra.ofListBasis_eq_ofList, LinearMap.coe_comp, Function.comp_apply, LinearMap.flip_apply, LinearMap.coe_mk, AddHom.coe_mk, AlgHom.toLinearMap_apply, LinearMap.zero_apply] rw [โ† mul_assoc] exact ฮน_normalOrderF_superCommuteF_ofCrAnList_eq_zero ฯ†a ฯ†a' _ _ rw [hf] simp lemma ฮน_normalOrderF_superCommuteF_ofCrAnState_ofCrAnList_eq_zero_mul (ฯ†a : ๐“•.CrAnStates) (ฯ†s : List ๐“•.CrAnStates) (a b : ๐“•.FieldOpFreeAlgebra) : ฮน ๐“แถ (a * [ofCrAnState ฯ†a, ofCrAnList ฯ†s]โ‚›ca * b) = 0 := by rw [โ† ofCrAnList_singleton, superCommuteF_ofCrAnList_ofCrAnList_eq_sum] rw [Finset.mul_sum, Finset.sum_mul] rw [map_sum, map_sum] apply Fintype.sum_eq_zero intro n rw [โ† mul_assoc, โ† mul_assoc] rw [mul_assoc _ _ b, ofCrAnList_singleton] rw [ฮน_normalOrderF_superCommuteF_ofCrAnState_eq_zero_mul] lemma ฮน_normalOrderF_superCommuteF_ofCrAnList_ofCrAnState_eq_zero_mul (ฯ†a : ๐“•.CrAnStates) (ฯ†s : List ๐“•.CrAnStates) (a b : ๐“•.FieldOpFreeAlgebra) : ฮน ๐“แถ (a * [ofCrAnList ฯ†s, ofCrAnState ฯ†a]โ‚›ca * b) = 0 := by rw [โ† ofCrAnList_singleton, superCommuteF_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 [ฮน_normalOrderF_superCommuteF_ofCrAnState_ofCrAnList_eq_zero_mul] simp lemma ฮน_normalOrderF_superCommuteF_ofCrAnList_ofCrAnList_eq_zero_mul (ฯ†s ฯ†s' : List ๐“•.CrAnStates) (a b : ๐“•.FieldOpFreeAlgebra) : ฮน ๐“แถ (a * [ofCrAnList ฯ†s, ofCrAnList ฯ†s']โ‚›ca * b) = 0 := by rw [superCommuteF_ofCrAnList_ofCrAnList_eq_sum, Finset.mul_sum, Finset.sum_mul] rw [map_sum, map_sum] apply Fintype.sum_eq_zero intro n rw [โ† mul_assoc, โ† mul_assoc] rw [mul_assoc _ _ b] rw [ฮน_normalOrderF_superCommuteF_ofCrAnList_ofCrAnState_eq_zero_mul] lemma ฮน_normalOrderF_superCommuteF_ofCrAnList_eq_zero_mul (ฯ†s : List ๐“•.CrAnStates) (a b c : ๐“•.FieldOpFreeAlgebra) : ฮน ๐“แถ (a * [ofCrAnList ฯ†s, c]โ‚›ca * b) = 0 := by change (ฮน.toLinearMap โˆ˜โ‚— normalOrderF โˆ˜โ‚— mulLinearMap.flip b โˆ˜โ‚— mulLinearMap a โˆ˜โ‚— superCommuteF (ofCrAnList ฯ†s)) c = 0 have hf : (ฮน.toLinearMap โˆ˜โ‚— normalOrderF โˆ˜โ‚— mulLinearMap.flip b โˆ˜โ‚— mulLinearMap a โˆ˜โ‚— superCommuteF (ofCrAnList ฯ†s)) = 0 := by apply ofCrAnListBasis.ext intro ฯ†s' simp only [mulLinearMap, LinearMap.coe_mk, AddHom.coe_mk, FieldOpFreeAlgebra.ofListBasis_eq_ofList, LinearMap.coe_comp, Function.comp_apply, LinearMap.flip_apply, AlgHom.toLinearMap_apply, LinearMap.zero_apply] rw [ฮน_normalOrderF_superCommuteF_ofCrAnList_ofCrAnList_eq_zero_mul] rw [hf] simp @[simp] lemma ฮน_normalOrderF_superCommuteF_eq_zero_mul (a b c d : ๐“•.FieldOpFreeAlgebra) : ฮน ๐“แถ (a * [d, c]โ‚›ca * b) = 0 := by change (ฮน.toLinearMap โˆ˜โ‚— normalOrderF โˆ˜โ‚— mulLinearMap.flip b โˆ˜โ‚— mulLinearMap a โˆ˜โ‚— superCommuteF.flip c) d = 0 have hf : (ฮน.toLinearMap โˆ˜โ‚— normalOrderF โˆ˜โ‚— mulLinearMap.flip b โˆ˜โ‚— mulLinearMap a โˆ˜โ‚— superCommuteF.flip c) = 0 := by apply ofCrAnListBasis.ext intro ฯ†s simp only [mulLinearMap, LinearMap.coe_mk, AddHom.coe_mk, FieldOpFreeAlgebra.ofListBasis_eq_ofList, LinearMap.coe_comp, Function.comp_apply, LinearMap.flip_apply, AlgHom.toLinearMap_apply, LinearMap.zero_apply] rw [ฮน_normalOrderF_superCommuteF_ofCrAnList_eq_zero_mul] rw [hf] simp @[simp] lemma ฮน_normalOrder_superCommuteF_eq_zero_mul_right (b c d : ๐“•.FieldOpFreeAlgebra) : ฮน ๐“แถ ([d, c]โ‚›ca * b) = 0 := by rw [โ† ฮน_normalOrderF_superCommuteF_eq_zero_mul 1 b c d] simp @[simp] lemma ฮน_normalOrderF_superCommuteF_eq_zero_mul_left (a c d : ๐“•.FieldOpFreeAlgebra) : ฮน ๐“แถ (a * [d, c]โ‚›ca) = 0 := by rw [โ† ฮน_normalOrderF_superCommuteF_eq_zero_mul a 1 c d] simp @[simp] lemma ฮน_normalOrderF_superCommuteF_eq_zero_mul_mul_right (a b1 b2 c d: ๐“•.FieldOpFreeAlgebra) : ฮน ๐“แถ (a * [d, c]โ‚›ca * b1 * b2) = 0 := by rw [โ† ฮน_normalOrderF_superCommuteF_eq_zero_mul a (b1 * b2) c d] congr 2 noncomm_ring @[simp] lemma ฮน_normalOrderF_superCommuteF_eq_zero (c d : ๐“•.FieldOpFreeAlgebra) : ฮน ๐“แถ ([d, c]โ‚›ca) = 0 := by rw [โ† ฮน_normalOrderF_superCommuteF_eq_zero_mul 1 1 c d] simp /-! ## Defining normal order for `FiedOpAlgebra`. -/ lemma ฮน_normalOrderF_zero_of_mem_ideal (a : ๐“•.FieldOpFreeAlgebra) (h : a โˆˆ TwoSidedIdeal.span ๐“•.fieldOpIdealSet) : ฮน ๐“แถ (a) = 0 := by rw [TwoSidedIdeal.mem_span_iff_mem_addSubgroup_closure] at h let p {k : Set ๐“•.FieldOpFreeAlgebra} (a : FieldOpFreeAlgebra ๐“•) (h : a โˆˆ AddSubgroup.closure k) := ฮน ๐“แถ (a) = 0 change p a h apply AddSubgroup.closure_induction ยท intro x hx obtain โŸจa, ha, b, hb, rflโŸฉ := Set.mem_mul.mp hx obtain โŸจa, ha, c, hc, rflโŸฉ := ha simp only [p] simp only [fieldOpIdealSet, exists_prop, exists_and_left, Set.mem_setOf_eq] at hc match hc with | Or.inl hc => obtain โŸจฯ†a, ฯ†a', hฯ†a, hฯ†a', rflโŸฉ := hc simp [mul_sub, sub_mul, โ† mul_assoc] | Or.inr (Or.inl hc) => obtain โŸจฯ†a, ฯ†a', hฯ†a, hฯ†a', rflโŸฉ := hc simp [mul_sub, sub_mul, โ† mul_assoc] | Or.inr (Or.inr (Or.inl hc)) => obtain โŸจฯ†a, ฯ†a', hฯ†a, hฯ†a', rflโŸฉ := hc simp [mul_sub, sub_mul, โ† mul_assoc] | Or.inr (Or.inr (Or.inr hc)) => obtain โŸจฯ†a, ฯ†a', hฯ†a, hฯ†a', rflโŸฉ := hc simp [mul_sub, sub_mul, โ† mul_assoc] ยท simp [p] ยท intro x y hx hy simp only [map_add, p] intro h1 h2 simp [h1, h2] ยท intro x hx simp [p] lemma ฮน_normalOrderF_eq_of_equiv (a b : ๐“•.FieldOpFreeAlgebra) (h : a โ‰ˆ b) : ฮน ๐“แถ (a) = ฮน ๐“แถ (b) := by rw [equiv_iff_sub_mem_ideal] at h rw [LinearMap.sub_mem_ker_iff.mp] simp only [LinearMap.mem_ker, โ† map_sub] exact ฮน_normalOrderF_zero_of_mem_ideal (a - b) h /-- Normal ordering on `FieldOpAlgebra`. -/ noncomputable def normalOrder : FieldOpAlgebra ๐“• โ†’โ‚—[โ„‚] FieldOpAlgebra ๐“• where toFun := Quotient.lift (ฮน.toLinearMap โˆ˜โ‚— normalOrderF) ฮน_normalOrderF_eq_of_equiv map_add' x y := by obtain โŸจx, rflโŸฉ := ฮน_surjective x obtain โŸจy, rflโŸฉ := ฮน_surjective y rw [โ† map_add, ฮน_apply, ฮน_apply, ฮน_apply] rw [Quotient.lift_mk, Quotient.lift_mk, Quotient.lift_mk] simp map_smul' c y := by obtain โŸจy, rflโŸฉ := ฮน_surjective y rw [โ† map_smul, ฮน_apply, ฮน_apply] simp @[inherit_doc normalOrder] scoped[FieldSpecification.FieldOpAlgebra] notation "๐“(" a ")" => normalOrder a /-! ## Properties of normal ordering. -/ lemma normalOrder_eq_ฮน_normalOrderF (a : ๐“•.FieldOpFreeAlgebra) : ๐“(ฮน a) = ฮน ๐“แถ (a) := rfl lemma normalOrder_ofCrAnFieldOpList (ฯ†s : List ๐“•.CrAnStates) : ๐“(ofCrAnFieldOpList ฯ†s) = normalOrderSign ฯ†s โ€ข ofCrAnFieldOpList (normalOrderList ฯ†s) := by rw [ofCrAnFieldOpList, normalOrder_eq_ฮน_normalOrderF, normalOrderF_ofCrAnList] rfl @[simp] lemma normalOrder_one_eq_one : normalOrder (๐“• := ๐“•) 1 = 1 := by have h1 : 1 = ofCrAnFieldOpList (๐“• := ๐“•) [] := by simp [ofCrAnFieldOpList] rw [h1] rw [normalOrder_ofCrAnFieldOpList] simp lemma ofCrAnFieldOpList_eq_normalOrder (ฯ†s : List ๐“•.CrAnStates) : ofCrAnFieldOpList (normalOrderList ฯ†s) = normalOrderSign ฯ†s โ€ข ๐“(ofCrAnFieldOpList ฯ†s) := by rw [normalOrder_ofCrAnFieldOpList, smul_smul, normalOrderSign, Wick.koszulSign_mul_self, one_smul] lemma normalOrder_normalOrder_mid (a b c : ๐“•.FieldOpAlgebra) : ๐“(a * b * c) = ๐“(a * ๐“(b) * c) := by obtain โŸจa, rflโŸฉ := ฮน_surjective a obtain โŸจb, rflโŸฉ := ฮน_surjective b obtain โŸจc, rflโŸฉ := ฮน_surjective c rw [normalOrder_eq_ฮน_normalOrderF] simp only [โ† map_mul] rw [normalOrder_eq_ฮน_normalOrderF] rw [normalOrderF_normalOrderF_mid] rfl lemma normalOrder_normalOrder_left (a b : ๐“•.FieldOpAlgebra) : ๐“(a * b) = ๐“(๐“(a) * b) := by obtain โŸจa, rflโŸฉ := ฮน_surjective a obtain โŸจb, rflโŸฉ := ฮน_surjective b rw [normalOrder_eq_ฮน_normalOrderF] simp only [โ† map_mul] rw [normalOrder_eq_ฮน_normalOrderF] rw [normalOrderF_normalOrderF_left] rfl lemma normalOrder_normalOrder_right (a b : ๐“•.FieldOpAlgebra) : ๐“(a * b) = ๐“(a * ๐“(b)) := by obtain โŸจa, rflโŸฉ := ฮน_surjective a obtain โŸจb, rflโŸฉ := ฮน_surjective b rw [normalOrder_eq_ฮน_normalOrderF] simp only [โ† map_mul] rw [normalOrder_eq_ฮน_normalOrderF] rw [normalOrderF_normalOrderF_right] rfl lemma normalOrder_normalOrder (a : ๐“•.FieldOpAlgebra) : ๐“(๐“(a)) = ๐“(a) := by trans ๐“(๐“(a) * 1) ยท simp ยท rw [โ† normalOrder_normalOrder_left] simp /-! ## mul anpart and crpart -/ lemma normalOrder_mul_anPart (ฯ† : ๐“•.States) (a : ๐“•.FieldOpAlgebra) : ๐“(a * anPart ฯ†) = ๐“(a) * anPart ฯ† := by obtain โŸจa, rflโŸฉ := ฮน_surjective a rw [anPart, โ† map_mul, normalOrder_eq_ฮน_normalOrderF, normalOrderF_mul_anPartF] rfl lemma crPart_mul_normalOrder (ฯ† : ๐“•.States) (a : ๐“•.FieldOpAlgebra) : ๐“(crPart ฯ† * a) = crPart ฯ† * ๐“(a) := by obtain โŸจa, rflโŸฉ := ฮน_surjective a rw [crPart, โ† map_mul, normalOrder_eq_ฮน_normalOrderF, normalOrderF_crPartF_mul] rfl /-! ### Normal order and super commutes -/ @[simp] lemma normalOrder_superCommute_eq_zero (a b : ๐“•.FieldOpAlgebra) : ๐“([a, b]โ‚›) = 0 := by obtain โŸจa, rflโŸฉ := ฮน_surjective a obtain โŸจb, rflโŸฉ := ฮน_surjective b rw [superCommute_eq_ฮน_superCommuteF, normalOrder_eq_ฮน_normalOrderF] simp @[simp] lemma normalOrder_superCommute_left_eq_zero (a b c: ๐“•.FieldOpAlgebra) : ๐“([a, b]โ‚› * c) = 0 := by obtain โŸจa, rflโŸฉ := ฮน_surjective a obtain โŸจb, rflโŸฉ := ฮน_surjective b obtain โŸจc, rflโŸฉ := ฮน_surjective c rw [superCommute_eq_ฮน_superCommuteF, โ† map_mul, normalOrder_eq_ฮน_normalOrderF] simp @[simp] lemma normalOrder_superCommute_right_eq_zero (a b c: ๐“•.FieldOpAlgebra) : ๐“(c * [a, b]โ‚›) = 0 := by obtain โŸจa, rflโŸฉ := ฮน_surjective a obtain โŸจb, rflโŸฉ := ฮน_surjective b obtain โŸจc, rflโŸฉ := ฮน_surjective c rw [superCommute_eq_ฮน_superCommuteF, โ† map_mul, normalOrder_eq_ฮน_normalOrderF] simp @[simp] lemma normalOrder_superCommute_mid_eq_zero (a b c d : ๐“•.FieldOpAlgebra) : ๐“(a * [c, d]โ‚› * b) = 0 := by obtain โŸจa, rflโŸฉ := ฮน_surjective a obtain โŸจb, rflโŸฉ := ฮน_surjective b obtain โŸจc, rflโŸฉ := ฮน_surjective c obtain โŸจd, rflโŸฉ := ฮน_surjective d rw [superCommute_eq_ฮน_superCommuteF, โ† map_mul, โ† map_mul, normalOrder_eq_ฮน_normalOrderF] simp /-! ### Swapping terms in a normal order. -/ lemma normalOrder_ofFieldOp_ofFieldOp_swap (ฯ† ฯ†' : ๐“•.States) : ๐“(ofFieldOp ฯ† * ofFieldOp ฯ†') = ๐“ข(๐“• |>โ‚› ฯ†, ๐“• |>โ‚› ฯ†') โ€ข ๐“(ofFieldOp ฯ†' * ofFieldOp ฯ†) := by rw [ofFieldOp_mul_ofFieldOp_eq_superCommute] simp lemma normalOrder_ofCrAnFieldOp_ofCrAnFieldOpList (ฯ† : ๐“•.CrAnStates) (ฯ†s : List ๐“•.CrAnStates) : ๐“(ofCrAnFieldOp ฯ† * ofCrAnFieldOpList ฯ†s) = ๐“ข(๐“• |>โ‚› ฯ†, ๐“• |>โ‚› ฯ†s) โ€ข ๐“(ofCrAnFieldOpList ฯ†s * ofCrAnFieldOp ฯ†) := by rw [โ† ofCrAnFieldOpList_singleton, ofCrAnFieldOpList_mul_ofCrAnFieldOpList_eq_superCommute] simp lemma normalOrder_ofCrAnFieldOp_ofFieldOpList_swap (ฯ† : ๐“•.CrAnStates) (ฯ†' : List ๐“•.States) : ๐“(ofCrAnFieldOp ฯ† * ofFieldOpList ฯ†') = ๐“ข(๐“• |>โ‚› ฯ†, ๐“• |>โ‚› ฯ†') โ€ข ๐“(ofFieldOpList ฯ†' * ofCrAnFieldOp ฯ†) := by rw [โ† ofCrAnFieldOpList_singleton, ofCrAnFieldOpList_mul_ofFieldOpList_eq_superCommute] simp lemma normalOrder_anPart_ofFieldOpList_swap (ฯ† : ๐“•.States) (ฯ†' : List ๐“•.States) : ๐“(anPart ฯ† * ofFieldOpList ฯ†') = ๐“ข(๐“• |>โ‚› ฯ†, ๐“• |>โ‚› ฯ†') โ€ข ๐“(ofFieldOpList ฯ†' * anPart ฯ†) := by match ฯ† with | .inAsymp ฯ† => simp | .position ฯ† => simp only [anPart_position, instCommGroup.eq_1] rw [normalOrder_ofCrAnFieldOp_ofFieldOpList_swap] rfl | .outAsymp ฯ† => simp only [anPart_posAsymp, instCommGroup.eq_1] rw [normalOrder_ofCrAnFieldOp_ofFieldOpList_swap] rfl lemma normalOrder_ofFieldOpList_anPart_swap (ฯ† : ๐“•.States) (ฯ†' : List ๐“•.States) : ๐“(ofFieldOpList ฯ†' * anPart ฯ†) = ๐“ข(๐“• |>โ‚› ฯ†, ๐“• |>โ‚› ฯ†') โ€ข ๐“(anPart ฯ† * ofFieldOpList ฯ†') := by rw [normalOrder_anPart_ofFieldOpList_swap] simp [smul_smul, FieldStatistic.exchangeSign_mul_self] lemma normalOrder_ofFieldOpList_mul_anPart_swap (ฯ† : ๐“•.States) (ฯ†s : List ๐“•.States) : ๐“(ofFieldOpList ฯ†s) * anPart ฯ† = ๐“ข(๐“• |>โ‚› ฯ†, ๐“• |>โ‚› ฯ†s) โ€ข ๐“(anPart ฯ† * ofFieldOpList ฯ†s) := by rw [โ† normalOrder_mul_anPart] rw [normalOrder_ofFieldOpList_anPart_swap] lemma anPart_mul_normalOrder_ofFieldOpList_eq_superCommute (ฯ† : ๐“•.States) (ฯ†s' : List ๐“•.States) : anPart ฯ† * ๐“(ofFieldOpList ฯ†s') = ๐“ข(๐“• |>โ‚› ฯ†, ๐“• |>โ‚› ฯ†s') โ€ข ๐“(ofFieldOpList ฯ†s' * anPart ฯ†) + [anPart ฯ†, ๐“(ofFieldOpList ฯ†s')]โ‚› := by rw [anPart, ofFieldOpList, normalOrder_eq_ฮน_normalOrderF, โ† map_mul] rw [anPartF_mul_normalOrderF_ofFieldOpListF_eq_superCommuteF] simp only [instCommGroup.eq_1, map_add, map_smul] rfl /-! ## Super commutators with a normal ordered term as sums -/ lemma ofCrAnFieldOp_superCommute_normalOrder_ofCrAnFieldOpList_sum (ฯ† : ๐“•.CrAnStates) (ฯ†s : List ๐“•.CrAnStates) : [ofCrAnFieldOp ฯ†, ๐“(ofCrAnFieldOpList ฯ†s)]โ‚› = โˆ‘ n : Fin ฯ†s.length, ๐“ข(๐“• |>โ‚› ฯ†, ๐“• |>โ‚› (ฯ†s.take n)) โ€ข [ofCrAnFieldOp ฯ†, ofCrAnFieldOp ฯ†s[n]]โ‚› * ๐“(ofCrAnFieldOpList (ฯ†s.eraseIdx n)) := by rw [normalOrder_ofCrAnFieldOpList, map_smul] rw [superCommute_ofCrAnFieldOp_ofCrAnFieldOpList_eq_sum, Finset.smul_sum, sum_normalOrderList_length] congr funext n simp only [instCommGroup.eq_1, List.get_eq_getElem, normalOrderList_get_normalOrderEquiv, normalOrderList_eraseIdx_normalOrderEquiv, Algebra.smul_mul_assoc, Fin.getElem_fin] rw [ofCrAnFieldOpList_eq_normalOrder, mul_smul_comm, smul_smul, smul_smul] by_cases hs : (๐“• |>โ‚› ฯ†) = (๐“• |>โ‚› ฯ†s[n]) ยท congr erw [normalOrderSign_eraseIdx, โ† hs] trans (normalOrderSign ฯ†s * normalOrderSign ฯ†s) * (๐“ข(๐“• |>โ‚› (ฯ†s.get n), ๐“• |>โ‚› ((normalOrderList ฯ†s).take (normalOrderEquiv n))) * ๐“ข(๐“• |>โ‚› (ฯ†s.get n), ๐“• |>โ‚› ((normalOrderList ฯ†s).take (normalOrderEquiv n)))) * ๐“ข(๐“• |>โ‚› (ฯ†s.get n), ๐“• |>โ‚› (ฯ†s.take n)) ยท ring_nf rw [hs] rfl ยท simp [hs] ยท erw [superCommute_diff_statistic hs] simp lemma ofCrAnFieldOp_superCommute_normalOrder_ofFieldOpList_sum (ฯ† : ๐“•.CrAnStates) (ฯ†s : List ๐“•.States) : [ofCrAnFieldOp ฯ†, ๐“(ofFieldOpList ฯ†s)]โ‚› = โˆ‘ n : Fin ฯ†s.length, ๐“ข(๐“• |>โ‚› ฯ†, ๐“• |>โ‚› (ฯ†s.take n)) โ€ข [ofCrAnFieldOp ฯ†, ofFieldOp ฯ†s[n]]โ‚› * ๐“(ofFieldOpList (ฯ†s.eraseIdx n)) := by conv_lhs => rw [ofFieldOpList_eq_sum, map_sum, map_sum] enter [2, s] rw [ofCrAnFieldOp_superCommute_normalOrder_ofCrAnFieldOpList_sum, CrAnSection.sum_over_length] enter [2, n] rw [CrAnSection.take_statistics_eq_take_state_statistics, smul_mul_assoc] rw [Finset.sum_comm] refine Finset.sum_congr rfl (fun n _ => ?_) simp only [instCommGroup.eq_1, Fin.coe_cast, Fin.getElem_fin, CrAnSection.sum_eraseIdxEquiv n _ n.prop, CrAnSection.eraseIdxEquiv_symm_getElem, CrAnSection.eraseIdxEquiv_symm_eraseIdx, โ† Finset.smul_sum, Algebra.smul_mul_assoc] conv_lhs => enter [2, 2, n] rw [โ† Finset.mul_sum] rw [โ† Finset.sum_mul, โ† map_sum, โ† map_sum, โ† ofFieldOp_eq_sum, โ† ofFieldOpList_eq_sum] /-- Within a proto-operator algebra we have that `[anPartF ฯ†, ๐“(ฯ†s)] = โˆ‘ i, sแตข โ€ข [anPartF ฯ†, ฯ†แตข]โ‚› * ๐“(ฯ†โ‚€โ€ฆฯ†แตขโ‚‹โ‚ฯ†แตขโ‚Šโ‚โ€ฆฯ†โ‚™)` where `sแตข` is the exchange sign for `ฯ†` and `ฯ†โ‚€โ€ฆฯ†แตขโ‚‹โ‚`. -/ lemma anPart_superCommute_normalOrder_ofFieldOpList_sum (ฯ† : ๐“•.States) (ฯ†s : List ๐“•.States) : [anPart ฯ†, ๐“(ofFieldOpList ฯ†s)]โ‚› = โˆ‘ n : Fin ฯ†s.length, ๐“ข(๐“• |>โ‚› ฯ†, ๐“• |>โ‚› (ฯ†s.take n)) โ€ข [anPart ฯ†, ofState ฯ†s[n]]โ‚› * ๐“(ofFieldOpList (ฯ†s.eraseIdx n)) := by match ฯ† with | .inAsymp ฯ† => simp | .position ฯ† => simp only [anPart_position, instCommGroup.eq_1, Fin.getElem_fin, Algebra.smul_mul_assoc] rw [ofCrAnFieldOp_superCommute_normalOrder_ofFieldOpList_sum] simp only [instCommGroup.eq_1, crAnStatistics, Function.comp_apply, crAnStatesToStates_prod, Fin.getElem_fin, Algebra.smul_mul_assoc] rfl | .outAsymp ฯ† => simp only [anPart_posAsymp, instCommGroup.eq_1, Fin.getElem_fin, Algebra.smul_mul_assoc] rw [ofCrAnFieldOp_superCommute_normalOrder_ofFieldOpList_sum] simp only [instCommGroup.eq_1, crAnStatistics, Function.comp_apply, crAnStatesToStates_prod, Fin.getElem_fin, Algebra.smul_mul_assoc] rfl /-! ## Multiplying with normal ordered terms -/ /-- Within a proto-operator algebra we have that `anPartF ฯ† * ๐“(ฯ†โ‚€ฯ†โ‚โ€ฆฯ†โ‚™) = ๐“((anPart ฯ†)ฯ†โ‚€ฯ†โ‚โ€ฆฯ†โ‚™) + [anpart ฯ†, ๐“(ฯ†โ‚€ฯ†โ‚โ€ฆฯ†โ‚™)]โ‚›`. -/ lemma anPart_mul_normalOrder_ofFieldOpList_eq_superCommute_reorder (ฯ† : ๐“•.States) (ฯ†s : List ๐“•.States) : anPart ฯ† * ๐“(ofFieldOpList ฯ†s) = ๐“(anPart ฯ† * ofFieldOpList ฯ†s) + [anPart ฯ†, ๐“(ofFieldOpList ฯ†s)]โ‚› := by rw [anPart_mul_normalOrder_ofFieldOpList_eq_superCommute] simp only [instCommGroup.eq_1, add_left_inj] rw [normalOrder_anPart_ofFieldOpList_swap] /-- Within a proto-operator algebra we have that `ฯ† * ๐“แถ (ฯ†โ‚€ฯ†โ‚โ€ฆฯ†โ‚™) = ๐“แถ (ฯ†ฯ†โ‚€ฯ†โ‚โ€ฆฯ†โ‚™) + [anpart ฯ†, ๐“แถ (ฯ†โ‚€ฯ†โ‚โ€ฆฯ†โ‚™)]โ‚›ca`. -/ lemma ofFieldOp_mul_normalOrder_ofFieldOpList_eq_superCommute (ฯ† : ๐“•.States) (ฯ†s : List ๐“•.States) : ofFieldOp ฯ† * ๐“(ofFieldOpList ฯ†s) = ๐“(ofFieldOp ฯ† * ofFieldOpList ฯ†s) + [anPart ฯ†, ๐“(ofFieldOpList ฯ†s)]โ‚› := by conv_lhs => rw [ofFieldOp_eq_crPart_add_anPart] rw [add_mul, anPart_mul_normalOrder_ofFieldOpList_eq_superCommute_reorder, โ† add_assoc, โ† crPart_mul_normalOrder, โ† map_add] conv_lhs => lhs rw [โ† add_mul, โ† ofFieldOp_eq_crPart_add_anPart] /-- In the expansion of `ofState ฯ† * normalOrderF (ofFieldOpListF ฯ†s)` the element of `๐“ž.A` associated with contracting `ฯ†` with the (optional) `n`th element of `ฯ†s`. -/ noncomputable def contractStateAtIndex (ฯ† : ๐“•.States) (ฯ†s : List ๐“•.States) (n : Option (Fin ฯ†s.length)) : ๐“•.FieldOpAlgebra := match n with | none => 1 | some n => ๐“ข(๐“• |>โ‚› ฯ†, ๐“• |>โ‚› (ฯ†s.take n)) โ€ข [anPart ฯ†, ofFieldOp ฯ†s[n]]โ‚› /-- Within a proto-operator algebra, `ฯ† * N(ฯ†โ‚€ฯ†โ‚โ€ฆฯ†โ‚™) = N(ฯ†ฯ†โ‚€ฯ†โ‚โ€ฆฯ†โ‚™) + โˆ‘ i, (sแตข โ€ข [anPartF ฯ†, ฯ†แตข]โ‚›) * N(ฯ†โ‚€ฯ†โ‚โ€ฆฯ†แตขโ‚‹โ‚ฯ†แตขโ‚Šโ‚โ€ฆฯ†โ‚™)`, where `sโ‚™` is the exchange sign for `ฯ†` and `ฯ†โ‚€ฯ†โ‚โ€ฆฯ†แตขโ‚‹โ‚`. -/ lemma ofFieldOp_mul_normalOrder_ofFieldOpList_eq_sum (ฯ† : ๐“•.States) (ฯ†s : List ๐“•.States) : ofFieldOp ฯ† * ๐“(ofFieldOpList ฯ†s) = โˆ‘ n : Option (Fin ฯ†s.length), contractStateAtIndex ฯ† ฯ†s n * ๐“(ofFieldOpList (HepLean.List.optionEraseZ ฯ†s ฯ† n)) := by rw [ofFieldOp_mul_normalOrder_ofFieldOpList_eq_superCommute] rw [anPart_superCommute_normalOrder_ofFieldOpList_sum] simp only [instCommGroup.eq_1, Fin.getElem_fin, Algebra.smul_mul_assoc, contractStateAtIndex, Fintype.sum_option, one_mul] rfl /-! ## Cons vs insertIdx for a normal ordered term. -/ /-- Within a proto-operator algebra, `N(ฯ†ฯ†โ‚€ฯ†โ‚โ€ฆฯ†โ‚™) = s โ€ข N(ฯ†โ‚€โ€ฆฯ†โ‚–โ‚‹โ‚ฯ†ฯ†โ‚–โ€ฆฯ†โ‚™)`, where `s` is the exchange sign for `ฯ†` and `ฯ†โ‚€โ€ฆฯ†โ‚–โ‚‹โ‚`. -/ lemma ofFieldOpList_normalOrder_insert (ฯ† : ๐“•.States) (ฯ†s : List ๐“•.States) (k : Fin ฯ†s.length.succ) : ๐“(ofFieldOpList (ฯ† :: ฯ†s)) = ๐“ข(๐“• |>โ‚› ฯ†, ๐“• |>โ‚› ฯ†s.take k) โ€ข ๐“(ofFieldOpList (ฯ†s.insertIdx k ฯ†)) := by have hl : ฯ†s.insertIdx k ฯ† = ฯ†s.take k ++ [ฯ†] ++ ฯ†s.drop k := by rw [HepLean.List.insertIdx_eq_take_drop] simp rw [hl] rw [ofFieldOpList_append, ofFieldOpList_append] rw [ofFieldOpList_mul_ofFieldOpList_eq_superCommute, add_mul] simp only [instCommGroup.eq_1, Nat.succ_eq_add_one, ofList_singleton, Algebra.smul_mul_assoc, map_add, map_smul, normalOrder_superCommute_left_eq_zero, add_zero, smul_smul, exchangeSign_mul_self_swap, one_smul] rw [โ† ofFieldOpList_append, โ† ofFieldOpList_append] simp /-! ## The normal ordering of a product of two states -/ @[simp] lemma normalOrder_crPart_mul_crPart (ฯ† ฯ†' : ๐“•.States) : ๐“(crPart ฯ† * crPart ฯ†') = crPart ฯ† * crPart ฯ†' := by rw [crPart, crPart, โ† map_mul, normalOrder_eq_ฮน_normalOrderF, normalOrderF_crPartF_mul_crPartF] @[simp] lemma normalOrder_anPart_mul_anPart (ฯ† ฯ†' : ๐“•.States) : ๐“(anPart ฯ† * anPart ฯ†') = anPart ฯ† * anPart ฯ†' := by rw [anPart, anPart, โ† map_mul, normalOrder_eq_ฮน_normalOrderF, normalOrderF_anPartF_mul_anPartF] @[simp] lemma normalOrder_crPart_mul_anPart (ฯ† ฯ†' : ๐“•.States) : ๐“(crPart ฯ† * anPart ฯ†') = crPart ฯ† * anPart ฯ†' := by rw [crPart, anPart, โ† map_mul, normalOrder_eq_ฮน_normalOrderF, normalOrderF_crPartF_mul_anPartF] @[simp] lemma normalOrder_anPart_mul_crPart (ฯ† ฯ†' : ๐“•.States) : ๐“(anPart ฯ† * crPart ฯ†') = ๐“ข(๐“• |>โ‚› ฯ†, ๐“• |>โ‚› ฯ†') โ€ข crPart ฯ†' * anPart ฯ† := by rw [anPart, crPart, โ† map_mul, normalOrder_eq_ฮน_normalOrderF, normalOrderF_anPartF_mul_crPartF] simp lemma normalOrder_ofFieldOp_mul_ofFieldOp (ฯ† ฯ†' : ๐“•.States) : ๐“(ofFieldOp ฯ† * ofFieldOp ฯ†') = crPart ฯ† * crPart ฯ†' + ๐“ข(๐“• |>โ‚› ฯ†, ๐“• |>โ‚› ฯ†') โ€ข (crPart ฯ†' * anPart ฯ†) + crPart ฯ† * anPart ฯ†' + anPart ฯ† * anPart ฯ†' := by rw [ofFieldOp, ofFieldOp, โ† map_mul, normalOrder_eq_ฮน_normalOrderF, normalOrderF_ofState_mul_ofState] rfl end FieldOpAlgebra end FieldSpecification