NormalOrder

📁 Source: PhysLean/QFT/PerturbationTheory/FieldSpecification/NormalOrder.lean

Statistics

Metric	Count
Definitions instDecidableNormalOrderRel, normalOrderEquiv, normalOrderList, normalOrderRel, normalOrderSign	5
Theorems instIsTotalCrAnFieldOpNormalOrderRel, instIsTransCrAnFieldOpNormalOrderRel, koszulSignInsert_annihilate_cons_create, koszulSignInsert_append_annihilate, koszulSignInsert_create, koszulSignInsert_swap, normalOrderList_append_annihilate, normalOrderList_cons_create, normalOrderList_eq_createFilter_append_annihilateFilter, normalOrderList_eraseIdx_normalOrderEquiv, normalOrderList_get_normalOrderEquiv, normalOrderList_nil, normalOrderList_statistics, normalOrderList_swap_create_annihilate, normalOrderSign_append_annihilate, normalOrderSign_cons_create, normalOrderSign_eraseIdx, normalOrderSign_mul_self, normalOrderSign_nil, normalOrderSign_singleton, normalOrderSign_swap_annihilate_annihilate, normalOrderSign_swap_annihilate_annihilate_fst, normalOrderSign_swap_create_annihilate, normalOrderSign_swap_create_annihilate_fst, normalOrderSign_swap_create_create, normalOrderSign_swap_create_create_fst, normalOrder_swap_create_annihilate_fst, orderedInsert_annihilateFilter, orderedInsert_append_annihilate, orderedInsert_create, orderedInsert_createFilter_append_annihilate, orderedInsert_createFilter_append_annihilateFilter_annihilate, sum_normalOrderList_length	33
Total	38

FieldSpecification

Definitions

Name	Category	Theorems
instDecidableNormalOrderRel 📖	CompOp	9 math math: koszulSignInsert_create, orderedInsert_annihilateFilter, koszulSignInsert_swap, orderedInsert_append_annihilate, orderedInsert_createFilter_append_annihilateFilter_annihilate, koszulSignInsert_annihilate_cons_create, koszulSignInsert_append_annihilate, orderedInsert_createFilter_append_annihilate, orderedInsert_create
normalOrderEquiv 📖	CompOp	4 math math: normalOrderList_eraseIdx_normalOrderEquiv, sum_normalOrderList_length, normalOrderList_get_normalOrderEquiv, normalOrderSign_eraseIdx
normalOrderList 📖	CompOp	15 math math: FieldOpFreeAlgebra.normalOrderF_ofCrAnListF, normalOrderList_eraseIdx_normalOrderEquiv, WickAlgebra.ofCrAnList_eq_normalOrder, FieldOpFreeAlgebra.ofCrAnListF_eq_normalOrderF, normalOrderList_nil, sum_normalOrderList_length, normalOrderList_get_normalOrderEquiv, normalOrder_swap_create_annihilate_fst, normalOrderList_eq_createFilter_append_annihilateFilter, normalOrderList_swap_create_annihilate, WickAlgebra.normalOrder_ofCrAnList, normalOrderList_statistics, normalOrderList_cons_create, normalOrderSign_eraseIdx, normalOrderList_append_annihilate
normalOrderRel 📖	MathDef	11 math math: instIsTotalCrAnFieldOpNormalOrderRel, koszulSignInsert_create, orderedInsert_annihilateFilter, koszulSignInsert_swap, orderedInsert_append_annihilate, orderedInsert_createFilter_append_annihilateFilter_annihilate, koszulSignInsert_annihilate_cons_create, instIsTransCrAnFieldOpNormalOrderRel, koszulSignInsert_append_annihilate, orderedInsert_createFilter_append_annihilate, orderedInsert_create
normalOrderSign 📖	CompOp	18 math math: normalOrderSign_cons_create, normalOrderSign_swap_create_create_fst, normalOrderSign_singleton, FieldOpFreeAlgebra.normalOrderF_ofCrAnListF, normalOrderSign_swap_create_annihilate_fst, FieldOpFreeAlgebra.normalOrderF_superCommuteF_ofCrAnListF_annihilate_annihilate_ofCrAnListF, WickAlgebra.ofCrAnList_eq_normalOrder, FieldOpFreeAlgebra.ofCrAnListF_eq_normalOrderF, normalOrderSign_append_annihilate, FieldOpFreeAlgebra.normalOrderF_superCommuteF_ofCrAnListF_create_create_ofCrAnListF, normalOrderSign_swap_create_annihilate, normalOrderSign_nil, normalOrderSign_swap_create_create, WickAlgebra.normalOrder_ofCrAnList, normalOrderSign_mul_self, normalOrderSign_swap_annihilate_annihilate_fst, normalOrderSign_eraseIdx, normalOrderSign_swap_annihilate_annihilate

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsTotalCrAnFieldOpNormalOrderRel 📖	mathematical	—	CrAnFieldOp normalOrderRel	—	CreateAnnihilate.instIsTotalNormalOrder
instIsTransCrAnFieldOpNormalOrderRel 📖	mathematical	—	CrAnFieldOp normalOrderRel	—	CreateAnnihilate.instIsTransNormalOrder
koszulSignInsert_annihilate_cons_create 📖	mathematical	crAnFieldOpToCreateAnnihilate CreateAnnihilate.create CreateAnnihilate.annihilate	Wick.koszulSignInsert CrAnFieldOp crAnStatistics normalOrderRel instDecidableNormalOrderRel FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign	—	Wick.koszulSignInsert_cons Wick.koszulSignCons.eq_1 normalOrderRel.eq_1 FieldStatistic.exchangeSign_symm FieldStatistic.exchangeSign_eq_if
koszulSignInsert_append_annihilate 📖	mathematical	crAnFieldOpToCreateAnnihilate CreateAnnihilate.annihilate	Wick.koszulSignInsert CrAnFieldOp crAnStatistics normalOrderRel instDecidableNormalOrderRel	—	—
koszulSignInsert_create 📖	mathematical	crAnFieldOpToCreateAnnihilate CreateAnnihilate.create	Wick.koszulSignInsert CrAnFieldOp crAnStatistics normalOrderRel instDecidableNormalOrderRel	—	—
koszulSignInsert_swap 📖	mathematical	—	Wick.koszulSignInsert CrAnFieldOp crAnStatistics normalOrderRel instDecidableNormalOrderRel	—	Wick.koszulSignInsert_eq_perm
normalOrderList_append_annihilate 📖	mathematical	crAnFieldOpToCreateAnnihilate CreateAnnihilate.annihilate	normalOrderList CrAnFieldOp	—	orderedInsert_append_annihilate
normalOrderList_cons_create 📖	mathematical	crAnFieldOpToCreateAnnihilate CreateAnnihilate.create	normalOrderList CrAnFieldOp	—	orderedInsert_create
normalOrderList_eq_createFilter_append_annihilateFilter 📖	mathematical	—	normalOrderList CrAnFieldOp createFilter annihilateFilter	—	normalOrderList_cons_create normalOrderList.eq_1 CreateAnnihilate.eq_create_or_annihilate orderedInsert_createFilter_append_annihilateFilter_annihilate createFilter_cons_annihilate annihilateFilter_cons_annihilate
normalOrderList_eraseIdx_normalOrderEquiv 📖	mathematical	—	CrAnFieldOp normalOrderList normalOrderEquiv	—	PhysLean.List.eraseIdx_insertionSort_fin instIsTotalCrAnFieldOpNormalOrderRel instIsTransCrAnFieldOpNormalOrderRel
normalOrderList_get_normalOrderEquiv 📖	mathematical	—	CrAnFieldOp normalOrderList normalOrderEquiv	—	PhysLean.List.insertionSortEquiv_get
normalOrderList_nil 📖	mathematical	—	normalOrderList CrAnFieldOp	—	—
normalOrderList_statistics 📖	mathematical	—	FieldStatistic.ofList CrAnFieldOp crAnStatistics normalOrderList	—	FieldStatistic.ofList_insertionSort
normalOrderList_swap_create_annihilate 📖	mathematical	crAnFieldOpToCreateAnnihilate CreateAnnihilate.create CreateAnnihilate.annihilate	normalOrderList CrAnFieldOp	—	normalOrder_swap_create_annihilate_fst
normalOrderSign_append_annihilate 📖	mathematical	crAnFieldOpToCreateAnnihilate CreateAnnihilate.annihilate	normalOrderSign CrAnFieldOp	—	normalOrderSign_singleton koszulSignInsert_append_annihilate
normalOrderSign_cons_create 📖	mathematical	crAnFieldOpToCreateAnnihilate CreateAnnihilate.create	normalOrderSign CrAnFieldOp	—	koszulSignInsert_create
normalOrderSign_eraseIdx 📖	mathematical	—	normalOrderSign CrAnFieldOp FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign crAnStatistics FieldStatistic.ofList normalOrderList normalOrderEquiv	—	normalOrderSign.eq_1 Wick.koszulSign_eraseIdx instIsTotalCrAnFieldOpNormalOrderRel instIsTransCrAnFieldOpNormalOrderRel
normalOrderSign_mul_self 📖	mathematical	—	normalOrderSign	—	Wick.koszulSign_mul_self
normalOrderSign_nil 📖	mathematical	—	normalOrderSign CrAnFieldOp	—	—
normalOrderSign_singleton 📖	mathematical	—	normalOrderSign CrAnFieldOp	—	Wick.koszulSign_singleton
normalOrderSign_swap_annihilate_annihilate 📖	mathematical	crAnFieldOpToCreateAnnihilate CreateAnnihilate.annihilate	normalOrderSign CrAnFieldOp	—	normalOrderSign_swap_annihilate_annihilate_fst normalOrderSign.eq_1 Wick.koszulSignInsert_eq_perm
normalOrderSign_swap_annihilate_annihilate_fst 📖	mathematical	crAnFieldOpToCreateAnnihilate CreateAnnihilate.annihilate	normalOrderSign CrAnFieldOp	—	normalOrderSign.eq_1 Wick.koszulSignInsert_cons
normalOrderSign_swap_create_annihilate 📖	mathematical	crAnFieldOpToCreateAnnihilate CreateAnnihilate.create CreateAnnihilate.annihilate	normalOrderSign CrAnFieldOp FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign crAnStatistics	—	normalOrderSign_swap_create_annihilate_fst normalOrderSign.eq_1 Wick.koszulSign.eq_2 koszulSignInsert_swap
normalOrderSign_swap_create_annihilate_fst 📖	mathematical	crAnFieldOpToCreateAnnihilate CreateAnnihilate.create CreateAnnihilate.annihilate	normalOrderSign CrAnFieldOp FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign crAnStatistics	—	normalOrderSign_cons_create normalOrderSign.eq_1 Wick.koszulSign.eq_2 koszulSignInsert_annihilate_cons_create FieldStatistic.exchangeSign_mul_self
normalOrderSign_swap_create_create 📖	mathematical	crAnFieldOpToCreateAnnihilate CreateAnnihilate.create	normalOrderSign CrAnFieldOp	—	normalOrderSign_swap_create_create_fst normalOrderSign.eq_1 Wick.koszulSignInsert_eq_perm
normalOrderSign_swap_create_create_fst 📖	mathematical	crAnFieldOpToCreateAnnihilate CreateAnnihilate.create	normalOrderSign CrAnFieldOp	—	normalOrderSign_cons_create
normalOrder_swap_create_annihilate_fst 📖	mathematical	crAnFieldOpToCreateAnnihilate CreateAnnihilate.create CreateAnnihilate.annihilate	normalOrderList CrAnFieldOp	—	normalOrderList_cons_create normalOrderList.eq_1 normalOrderRel.eq_1
orderedInsert_annihilateFilter 📖	mathematical	—	CrAnFieldOp normalOrderRel instDecidableNormalOrderRel annihilateFilter	—	CreateAnnihilate.eq_create_or_annihilate annihilateFilter_cons_create annihilateFilter_cons_annihilate
orderedInsert_append_annihilate 📖	mathematical	crAnFieldOpToCreateAnnihilate CreateAnnihilate.annihilate	CrAnFieldOp normalOrderRel instDecidableNormalOrderRel	—	—
orderedInsert_create 📖	mathematical	crAnFieldOpToCreateAnnihilate CreateAnnihilate.create	CrAnFieldOp normalOrderRel instDecidableNormalOrderRel	—	—
orderedInsert_createFilter_append_annihilate 📖	mathematical	crAnFieldOpToCreateAnnihilate CreateAnnihilate.annihilate	CrAnFieldOp normalOrderRel instDecidableNormalOrderRel createFilter	—	CreateAnnihilate.eq_create_or_annihilate createFilter_cons_create createFilter_cons_annihilate
orderedInsert_createFilter_append_annihilateFilter_annihilate 📖	mathematical	crAnFieldOpToCreateAnnihilate CreateAnnihilate.annihilate	CrAnFieldOp normalOrderRel instDecidableNormalOrderRel createFilter annihilateFilter	—	orderedInsert_createFilter_append_annihilate orderedInsert_annihilateFilter
sum_normalOrderList_length 📖	mathematical	—	CrAnFieldOp normalOrderList normalOrderEquiv	—	—

---

← Back to Index