/- 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.CrAnAlgebra.NormalOrder import HepLean.PerturbationTheory.Koszul.KoszulSign /-! # Normal ordering of the operator algebra -/ namespace FieldSpecification variable {๐“• : FieldSpecification} namespace ProtoOperatorAlgebra variable {๐“ž : ProtoOperatorAlgebra ๐“•} open CrAnAlgebra open FieldStatistic /-! ## Normal order of super-commutators. The main result of this section is `crAnF_normalOrderF_superCommuteF_eq_zero_mul`. -/ lemma crAnF_normalOrderF_superCommuteF_ofCrAnList_create_create_ofCrAnList (ฯ†c ฯ†c' : ๐“•.CrAnStates) (hฯ†c : ๐“• |>แถœ ฯ†c = CreateAnnihilate.create) (hฯ†c' : ๐“• |>แถœ ฯ†c' = CreateAnnihilate.create) (ฯ†s ฯ†s' : List ๐“•.CrAnStates) : ๐“ž.crAnF (๐“แถ (ofCrAnList ฯ†s * [ofCrAnState ฯ†c, ofCrAnState ฯ†c']โ‚›ca * ofCrAnList ฯ†s')) = 0 := by rw [normalOrderF_superCommuteF_ofCrAnList_create_create_ofCrAnList ฯ†c ฯ†c' hฯ†c hฯ†c' ฯ†s ฯ†s'] rw [map_smul, map_mul, map_mul, map_mul, ๐“ž.superCommuteF_create_create ฯ†c ฯ†c' hฯ†c hฯ†c'] simp lemma crAnF_normalOrderF_superCommuteF_ofCrAnList_annihilate_annihilate_ofCrAnList (ฯ†a ฯ†a' : ๐“•.CrAnStates) (hฯ†a : ๐“• |>แถœ ฯ†a = CreateAnnihilate.annihilate) (hฯ†a' : ๐“• |>แถœ ฯ†a' = CreateAnnihilate.annihilate) (ฯ†s ฯ†s' : List ๐“•.CrAnStates) : ๐“ž.crAnF (๐“แถ (ofCrAnList ฯ†s * [ofCrAnState ฯ†a, ofCrAnState ฯ†a']โ‚›ca * ofCrAnList ฯ†s')) = 0 := by 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_annihilate_annihilate ฯ†a ฯ†a' hฯ†a hฯ†a'] simp lemma crAnF_normalOrderF_superCommuteF_ofCrAnList_ofCrAnList_eq_zero (ฯ†a ฯ†a' : ๐“•.CrAnStates) (ฯ†s ฯ†s' : List ๐“•.CrAnStates) : ๐“ž.crAnF (normalOrderF (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_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_annihilate_annihilate ฯ†a ฯ†a' hฯ†a hฯ†a'] simp lemma crAnF_normalOrderF_superCommuteF_ofCrAnList_eq_zero (ฯ†a ฯ†a' : ๐“•.CrAnStates) (ฯ†s : List ๐“•.CrAnStates) (a : ๐“•.CrAnAlgebra) : ๐“ž.crAnF (normalOrderF (ofCrAnList ฯ†s * [ofCrAnState ฯ†a, ofCrAnState ฯ†a']โ‚›ca * a)) = 0 := by change (๐“ž.crAnF.toLinearMap โˆ˜โ‚— normalOrderF โˆ˜โ‚— mulLinearMap ((ofCrAnList ฯ†s * [ofCrAnState ฯ†a, ofCrAnState ฯ†a']โ‚›ca))) a = 0 have hf : ๐“ž.crAnF.toLinearMap โˆ˜โ‚— normalOrderF โˆ˜โ‚— mulLinearMap (ofCrAnList ฯ†s * [ofCrAnState ฯ†a, ofCrAnState ฯ†a']โ‚›ca) = 0 := by apply ofCrAnListBasis.ext intro l simp only [ofListBasis_eq_ofList, LinearMap.coe_comp, Function.comp_apply, AlgHom.toLinearMap_apply, LinearMap.zero_apply] exact crAnF_normalOrderF_superCommuteF_ofCrAnList_ofCrAnList_eq_zero ฯ†a ฯ†a' ฯ†s l rw [hf] simp lemma crAnF_normalOrderF_superCommuteF_ofCrAnState_eq_zero_mul (ฯ†a ฯ†a' : ๐“•.CrAnStates) (a b : ๐“•.CrAnAlgebra) : ๐“ž.crAnF (normalOrderF (a * [ofCrAnState ฯ†a, ofCrAnState ฯ†a']โ‚›ca * b)) = 0 := by rw [mul_assoc] change (๐“ž.crAnF.toLinearMap โˆ˜โ‚— normalOrderF โˆ˜โ‚— mulLinearMap.flip ([ofCrAnState ฯ†a, ofCrAnState ฯ†a']โ‚›ca * b)) a = 0 have hf : ๐“ž.crAnF.toLinearMap โˆ˜โ‚— normalOrderF โˆ˜โ‚— mulLinearMap.flip ([ofCrAnState ฯ†a, ofCrAnState ฯ†a']โ‚›ca * b) = 0 := by apply ofCrAnListBasis.ext intro l simp only [mulLinearMap, 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 crAnF_normalOrderF_superCommuteF_ofCrAnList_eq_zero ฯ†a ฯ†a' _ _ rw [hf] simp lemma crAnF_normalOrderF_superCommuteF_ofCrAnState_ofCrAnList_eq_zero_mul (ฯ†a : ๐“•.CrAnStates) (ฯ†s : List ๐“•.CrAnStates) (a b : ๐“•.CrAnAlgebra) : ๐“ž.crAnF (normalOrderF (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 [crAnF_normalOrderF_superCommuteF_ofCrAnState_eq_zero_mul] lemma crAnF_normalOrderF_superCommuteF_ofCrAnList_ofCrAnState_eq_zero_mul (ฯ†a : ๐“•.CrAnStates) (ฯ†s : List ๐“•.CrAnStates) (a b : ๐“•.CrAnAlgebra) : ๐“ž.crAnF (normalOrderF (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 [crAnF_normalOrderF_superCommuteF_ofCrAnState_ofCrAnList_eq_zero_mul] simp lemma crAnF_normalOrderF_superCommuteF_ofCrAnList_ofCrAnList_eq_zero_mul (ฯ†s ฯ†s' : List ๐“•.CrAnStates) (a b : ๐“•.CrAnAlgebra) : ๐“ž.crAnF (normalOrderF (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 [crAnF_normalOrderF_superCommuteF_ofCrAnList_ofCrAnState_eq_zero_mul] lemma crAnF_normalOrderF_superCommuteF_ofCrAnList_eq_zero_mul (ฯ†s : List ๐“•.CrAnStates) (a b c : ๐“•.CrAnAlgebra) : ๐“ž.crAnF (normalOrderF (a * [ofCrAnList ฯ†s, c]โ‚›ca * b)) = 0 := by change (๐“ž.crAnF.toLinearMap โˆ˜โ‚— normalOrderF โˆ˜โ‚— mulLinearMap.flip b โˆ˜โ‚— mulLinearMap a โˆ˜โ‚— superCommuteF (ofCrAnList ฯ†s)) c = 0 have hf : (๐“ž.crAnF.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, ofListBasis_eq_ofList, LinearMap.coe_comp, Function.comp_apply, LinearMap.flip_apply, AlgHom.toLinearMap_apply, LinearMap.zero_apply] rw [crAnF_normalOrderF_superCommuteF_ofCrAnList_ofCrAnList_eq_zero_mul] rw [hf] simp @[simp] lemma crAnF_normalOrderF_superCommuteF_eq_zero_mul (a b c d : ๐“•.CrAnAlgebra) : ๐“ž.crAnF (normalOrderF (a * [d, c]โ‚›ca * b)) = 0 := by change (๐“ž.crAnF.toLinearMap โˆ˜โ‚— normalOrderF โˆ˜โ‚— mulLinearMap.flip b โˆ˜โ‚— mulLinearMap a โˆ˜โ‚— superCommuteF.flip c) d = 0 have hf : (๐“ž.crAnF.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, ofListBasis_eq_ofList, LinearMap.coe_comp, Function.comp_apply, LinearMap.flip_apply, AlgHom.toLinearMap_apply, LinearMap.zero_apply] rw [crAnF_normalOrderF_superCommuteF_ofCrAnList_eq_zero_mul] rw [hf] simp @[simp] lemma crAnF_normalOrderF_superCommuteF_eq_zero_mul_right (b c d : ๐“•.CrAnAlgebra) : ๐“ž.crAnF (normalOrderF ([d, c]โ‚›ca * b)) = 0 := by rw [โ† crAnF_normalOrderF_superCommuteF_eq_zero_mul 1 b c d] simp @[simp] lemma crAnF_normalOrderF_superCommuteF_eq_zero_mul_left (a c d : ๐“•.CrAnAlgebra) : ๐“ž.crAnF (normalOrderF (a * [d, c]โ‚›ca)) = 0 := by rw [โ† crAnF_normalOrderF_superCommuteF_eq_zero_mul a 1 c d] simp @[simp] lemma crAnF_normalOrderF_superCommuteF_eq_zero (c d : ๐“•.CrAnAlgebra) : ๐“ž.crAnF (normalOrderF [d, c]โ‚›ca) = 0 := by rw [โ† crAnF_normalOrderF_superCommuteF_eq_zero_mul 1 1 c d] simp /-! ## Swapping terms in a normal order. -/ lemma crAnF_normalOrderF_ofState_ofState_swap (ฯ† ฯ†' : ๐“•.States) : ๐“ž.crAnF (normalOrderF (ofState ฯ† * ofState ฯ†')) = ๐“ข(๐“• |>โ‚› ฯ†, ๐“• |>โ‚› ฯ†') โ€ข ๐“ž.crAnF (normalOrderF (ofState ฯ†' * ofState ฯ†)) := by rw [โ† ofStateList_singleton, โ† ofStateList_singleton, ofStateList_mul_ofStateList_eq_superCommuteF] simp lemma crAnF_normalOrderF_ofCrAnState_ofCrAnList_swap (ฯ† : ๐“•.CrAnStates) (ฯ†s : List ๐“•.CrAnStates) : ๐“ž.crAnF (normalOrderF (ofCrAnState ฯ† * ofCrAnList ฯ†s)) = ๐“ข(๐“• |>โ‚› ฯ†, ๐“• |>โ‚› ฯ†s) โ€ข ๐“ž.crAnF (normalOrderF (ofCrAnList ฯ†s * ofCrAnState ฯ†)) := by rw [โ† ofCrAnList_singleton, ofCrAnList_mul_ofCrAnList_eq_superCommuteF] simp lemma crAnF_normalOrderF_ofCrAnState_ofStatesList_swap (ฯ† : ๐“•.CrAnStates) (ฯ†' : List ๐“•.States) : ๐“ž.crAnF (normalOrderF (ofCrAnState ฯ† * ofStateList ฯ†')) = ๐“ข(๐“• |>โ‚› ฯ†, ๐“• |>โ‚› ฯ†') โ€ข ๐“ž.crAnF (normalOrderF (ofStateList ฯ†' * ofCrAnState ฯ†)) := by rw [โ† ofCrAnList_singleton, ofCrAnList_mul_ofStateList_eq_superCommuteF] simp lemma crAnF_normalOrderF_anPartF_ofStatesList_swap (ฯ† : ๐“•.States) (ฯ†' : List ๐“•.States) : ๐“ž.crAnF (normalOrderF (anPartF ฯ† * ofStateList ฯ†')) = ๐“ข(๐“• |>โ‚› ฯ†, ๐“• |>โ‚› ฯ†') โ€ข ๐“ž.crAnF (normalOrderF (ofStateList ฯ†' * anPartF ฯ†)) := by match ฯ† with | .inAsymp ฯ† => simp | .position ฯ† => simp only [anPartF_position, instCommGroup.eq_1] rw [crAnF_normalOrderF_ofCrAnState_ofStatesList_swap] rfl | .outAsymp ฯ† => simp only [anPartF_posAsymp, instCommGroup.eq_1] rw [crAnF_normalOrderF_ofCrAnState_ofStatesList_swap] rfl lemma crAnF_normalOrderF_ofStatesList_anPartF_swap (ฯ† : ๐“•.States) (ฯ†' : List ๐“•.States) : ๐“ž.crAnF (normalOrderF (ofStateList ฯ†' * anPartF ฯ†)) = ๐“ข(๐“• |>โ‚› ฯ†, ๐“• |>โ‚› ฯ†') โ€ข ๐“ž.crAnF (normalOrderF (anPartF ฯ† * ofStateList ฯ†')) := by rw [crAnF_normalOrderF_anPartF_ofStatesList_swap] simp [smul_smul, FieldStatistic.exchangeSign_mul_self] lemma crAnF_normalOrderF_ofStatesList_mul_anPartF_swap (ฯ† : ๐“•.States) (ฯ†' : List ๐“•.States) : ๐“ž.crAnF (normalOrderF (ofStateList ฯ†') * anPartF ฯ†) = ๐“ข(๐“• |>โ‚› ฯ†, ๐“• |>โ‚› ฯ†') โ€ข ๐“ž.crAnF (normalOrderF (anPartF ฯ† * ofStateList ฯ†')) := by rw [โ† normalOrderF_mul_anPartF] rw [crAnF_normalOrderF_ofStatesList_anPartF_swap] /-! ## Super commutators with a normal ordered term as sums -/ lemma crAnF_ofCrAnState_superCommuteF_normalOrderF_ofCrAnList_eq_sum (ฯ† : ๐“•.CrAnStates) (ฯ†s : List ๐“•.CrAnStates) : ๐“ž.crAnF ([ofCrAnState ฯ†, normalOrderF (ofCrAnList ฯ†s)]โ‚›ca) = โˆ‘ n : Fin ฯ†s.length, ๐“ข(๐“• |>โ‚› ฯ†, ๐“• |>โ‚› (ฯ†s.take n)) โ€ข ๐“ž.crAnF ([ofCrAnState ฯ†, ofCrAnState ฯ†s[n]]โ‚›ca) * ๐“ž.crAnF (normalOrderF (ofCrAnList (ฯ†s.eraseIdx n))) := by rw [normalOrderF_ofCrAnList, map_smul, map_smul] rw [crAnF_superCommuteF_ofCrAnState_ofCrAnList_eq_sum, sum_normalOrderList_length] simp only [instCommGroup.eq_1, List.get_eq_getElem, normalOrderList_get_normalOrderEquiv, normalOrderList_eraseIdx_normalOrderEquiv, Algebra.smul_mul_assoc, map_sum, map_smul, map_mul, Finset.smul_sum, Fin.getElem_fin] congr funext n rw [ofCrAnList_eq_normalOrderF, map_smul, 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 [๐“ž.superCommuteF_different_statistics _ _ hs] simp lemma crAnF_ofCrAnState_superCommuteF_normalOrderF_ofStateList_eq_sum (ฯ† : ๐“•.CrAnStates) (ฯ†s : List ๐“•.States) : ๐“ž.crAnF ([ofCrAnState ฯ†, normalOrderF (ofStateList ฯ†s)]โ‚›ca) = โˆ‘ n : Fin ฯ†s.length, ๐“ข(๐“• |>โ‚› ฯ†, ๐“• |>โ‚› (ฯ†s.take n)) โ€ข ๐“ž.crAnF ([ofCrAnState ฯ†, ofState ฯ†s[n]]โ‚›ca) * ๐“ž.crAnF (normalOrderF (ofStateList (ฯ†s.eraseIdx n))) := by conv_lhs => rw [ofStateList_sum, map_sum, map_sum, map_sum] enter [2, s] rw [crAnF_ofCrAnState_superCommuteF_normalOrderF_ofCrAnList_eq_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, โ† ofState, โ† map_sum, โ† map_sum, โ† ofStateList_sum] /-- Within a proto-operator algebra we have that `[anPartF ฯ†, ๐“แถ (ฯ†s)] = โˆ‘ i, sแตข โ€ข [anPartF ฯ†, ฯ†แตข]โ‚›ca * ๐“แถ (ฯ†โ‚€โ€ฆฯ†แตขโ‚‹โ‚ฯ†แตขโ‚Šโ‚โ€ฆฯ†โ‚™)` where `sแตข` is the exchange sign for `ฯ†` and `ฯ†โ‚€โ€ฆฯ†แตขโ‚‹โ‚`. The origin of this result is - `superCommuteF_ofCrAnList_ofCrAnList_eq_sum` -/ lemma crAnF_anPartF_superCommuteF_normalOrderF_ofStateList_eq_sum (ฯ† : ๐“•.States) (ฯ†s : List ๐“•.States) : ๐“ž.crAnF ([anPartF ฯ†, ๐“แถ (ฯ†s)]โ‚›ca) = โˆ‘ n : Fin ฯ†s.length, ๐“ข(๐“• |>โ‚› ฯ†, ๐“• |>โ‚› (ฯ†s.take n)) โ€ข ๐“ž.crAnF ([anPartF ฯ†, ofState ฯ†s[n]]โ‚›ca) * ๐“ž.crAnF ๐“แถ (ฯ†s.eraseIdx n) := by match ฯ† with | .inAsymp ฯ† => simp | .position ฯ† => simp only [anPartF_position, instCommGroup.eq_1, Fin.getElem_fin, Algebra.smul_mul_assoc] rw [crAnF_ofCrAnState_superCommuteF_normalOrderF_ofStateList_eq_sum] simp [crAnStatistics] | .outAsymp ฯ† => simp only [anPartF_posAsymp, instCommGroup.eq_1, Fin.getElem_fin, Algebra.smul_mul_assoc] rw [crAnF_ofCrAnState_superCommuteF_normalOrderF_ofStateList_eq_sum] simp [crAnStatistics] /-! ## Multiplying with normal ordered terms -/ /-- Within a proto-operator algebra we have that `anPartF ฯ† * ๐“แถ (ฯ†โ‚€ฯ†โ‚โ€ฆฯ†โ‚™) = ๐“แถ ((anPartF ฯ†)ฯ†โ‚€ฯ†โ‚โ€ฆฯ†โ‚™) + [anpart ฯ†, ๐“แถ (ฯ†โ‚€ฯ†โ‚โ€ฆฯ†โ‚™)]โ‚›ca`. -/ lemma crAnF_anPartF_mul_normalOrderF_ofStatesList_eq_superCommuteF (ฯ† : ๐“•.States) (ฯ†' : List ๐“•.States) : ๐“ž.crAnF (anPartF ฯ† * normalOrderF (ofStateList ฯ†')) = ๐“ž.crAnF (normalOrderF (anPartF ฯ† * ofStateList ฯ†')) + ๐“ž.crAnF ([anPartF ฯ†, normalOrderF (ofStateList ฯ†')]โ‚›ca) := by rw [anPartF_mul_normalOrderF_ofStateList_eq_superCommuteF] simp only [instCommGroup.eq_1, map_add, map_smul] congr rw [crAnF_normalOrderF_anPartF_ofStatesList_swap] /-- Within a proto-operator algebra we have that `ฯ† * ๐“แถ (ฯ†โ‚€ฯ†โ‚โ€ฆฯ†โ‚™) = ๐“แถ (ฯ†ฯ†โ‚€ฯ†โ‚โ€ฆฯ†โ‚™) + [anpart ฯ†, ๐“แถ (ฯ†โ‚€ฯ†โ‚โ€ฆฯ†โ‚™)]โ‚›ca`. -/ lemma crAnF_ofState_mul_normalOrderF_ofStatesList_eq_superCommuteF (ฯ† : ๐“•.States) (ฯ†s : List ๐“•.States) : ๐“ž.crAnF (ofState ฯ† * ๐“แถ (ฯ†s)) = ๐“ž.crAnF (normalOrderF (ofState ฯ† * ofStateList ฯ†s)) + ๐“ž.crAnF ([anPartF ฯ†, ๐“แถ (ฯ†s)]โ‚›ca) := by conv_lhs => rw [ofState_eq_crPartF_add_anPartF] rw [add_mul, map_add, crAnF_anPartF_mul_normalOrderF_ofStatesList_eq_superCommuteF, โ† add_assoc, โ† normalOrderF_crPartF_mul, โ† map_add] conv_lhs => lhs rw [โ† map_add, โ† add_mul, โ† ofState_eq_crPartF_add_anPartF] /-- In the expansion of `ofState ฯ† * normalOrderF (ofStateList ฯ†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)) : ๐“ž.A := match n with | none => 1 | some n => ๐“ข(๐“• |>โ‚› ฯ†, ๐“• |>โ‚› (ฯ†s.take n)) โ€ข ๐“ž.crAnF ([anPartF ฯ†, ofState ฯ†s[n]]โ‚›ca) /-- Within a proto-operator algebra, `ฯ† * N(ฯ†โ‚€ฯ†โ‚โ€ฆฯ†โ‚™) = N(ฯ†ฯ†โ‚€ฯ†โ‚โ€ฆฯ†โ‚™) + โˆ‘ i, (sแตข โ€ข [anPartF ฯ†, ฯ†แตข]โ‚›) * N(ฯ†โ‚€ฯ†โ‚โ€ฆฯ†แตขโ‚‹โ‚ฯ†แตขโ‚Šโ‚โ€ฆฯ†โ‚™)`, where `sโ‚™` is the exchange sign for `ฯ†` and `ฯ†โ‚€ฯ†โ‚โ€ฆฯ†แตขโ‚‹โ‚`. -/ lemma crAnF_ofState_mul_normalOrderF_ofStatesList_eq_sum (ฯ† : ๐“•.States) (ฯ†s : List ๐“•.States) : ๐“ž.crAnF (ofState ฯ† * normalOrderF (ofStateList ฯ†s)) = โˆ‘ n : Option (Fin ฯ†s.length), contractStateAtIndex ฯ† ฯ†s n * ๐“ž.crAnF (normalOrderF (ofStateList (HepLean.List.optionEraseZ ฯ†s ฯ† n))) := by rw [crAnF_ofState_mul_normalOrderF_ofStatesList_eq_superCommuteF] rw [crAnF_anPartF_superCommuteF_normalOrderF_ofStateList_eq_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 crAnF_ofState_normalOrderF_insert (ฯ† : ๐“•.States) (ฯ†s : List ๐“•.States) (k : Fin ฯ†s.length.succ) : ๐“ž.crAnF (normalOrderF (ofStateList (ฯ† :: ฯ†s))) = ๐“ข(๐“• |>โ‚› ฯ†, ๐“• |>โ‚› ฯ†s.take k) โ€ข ๐“ž.crAnF (normalOrderF (ofStateList (ฯ†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 [ofStateList_append, ofStateList_append] rw [ofStateList_mul_ofStateList_eq_superCommuteF, add_mul] simp only [instCommGroup.eq_1, Nat.succ_eq_add_one, ofList_singleton, Algebra.smul_mul_assoc, map_add, map_smul, crAnF_normalOrderF_superCommuteF_eq_zero_mul_right, add_zero, smul_smul, exchangeSign_mul_self_swap, one_smul] rw [โ† ofStateList_append, โ† ofStateList_append] simp end ProtoOperatorAlgebra end FieldSpecification