NormalOrder

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

Statistics

Metric	Count
Definitions normalOrderF, «term𝓝ᶠ(_)»»)	2
Theorems anPartF_mul_normalOrderF_ofFieldOpListF_eq_superCommuteF, normalOrderF_anPartF_mul_anPartF, normalOrderF_anPartF_mul_crPartF, normalOrderF_crPartF_mul, normalOrderF_crPartF_mul_anPartF, normalOrderF_crPartF_mul_crPartF, normalOrderF_create_mul, normalOrderF_mul_anPartF, normalOrderF_mul_annihilate, normalOrderF_normalOrderF_left, normalOrderF_normalOrderF_mid, normalOrderF_normalOrderF_right, normalOrderF_ofCrAnListF, normalOrderF_ofCrAnListF_append_annihilate, normalOrderF_ofCrAnListF_cons_create, normalOrderF_ofFieldOpF_mul_ofFieldOpF, normalOrderF_one, normalOrderF_superCommuteF_anPartF_crPartF, normalOrderF_superCommuteF_annihilate_create, normalOrderF_superCommuteF_crPartF_anPartF, normalOrderF_superCommuteF_create_annihilate, normalOrderF_superCommuteF_ofCrAnListF_annihilate_annihilate_ofCrAnListF, normalOrderF_superCommuteF_ofCrAnListF_create_create_ofCrAnListF, normalOrderF_swap_anPartF_crPartF, normalOrderF_swap_crPartF_anPartF, normalOrderF_swap_create_annihilate, normalOrderF_swap_create_annihilate_ofCrAnListF, normalOrderF_swap_create_annihilate_ofCrAnListF_ofCrAnListF, ofCrAnListF_eq_normalOrderF, ofCrAnListF_mul_normalOrderF_ofFieldOpListF_eq_superCommuteF, ofCrAnListF_superCommuteF_normalOrderF_ofCrAnListF, ofCrAnListF_superCommuteF_normalOrderF_ofFieldOpListF, ofCrAnOpF_mul_normalOrderF_ofFieldOpListF_eq_superCommuteF	33
Total	35

FieldSpecification.FieldOpFreeAlgebra

Definitions

Name	Category	Theorems
normalOrderF 📖	CompOp	48 math math: normalOrderF_mul_anPartF, FieldSpecification.WickAlgebra.ι_normalOrderF_superCommuteF_eq_zero, normalOrderF_ofCrAnListF, ofCrAnOpF_mul_normalOrderF_ofFieldOpListF_eq_superCommuteF, normalOrderF_swap_crPartF_anPartF, FieldSpecification.WickAlgebra.ι_normalOrderF_eq_of_equiv, normalOrderF_superCommuteF_ofCrAnListF_annihilate_annihilate_ofCrAnListF, FieldSpecification.WickAlgebra.ι_normalOrderF_superCommuteF_eq_zero_mul_left, FieldSpecification.WickAlgebra.normalOrder_eq_ι_normalOrderF, normalOrderF_ofCrAnListF_cons_create, normalOrderF_swap_create_annihilate_ofCrAnListF, FieldSpecification.WickAlgebra.ι_normalOrderF_superCommuteF_ofCrAnListF_ofCrAnOpF_eq_zero_mul, normalOrderF_mul_annihilate, normalOrderF_crPartF_mul_crPartF, normalOrderF_crPartF_mul_anPartF, ofCrAnListF_eq_normalOrderF, normalOrderF_anPartF_mul_crPartF, normalOrderF_swap_anPartF_crPartF, FieldSpecification.WickAlgebra.ι_normalOrderF_superCommuteF_ofCrAnListF_ofCrAnListF_eq_zero_mul, ofCrAnListF_superCommuteF_normalOrderF_ofCrAnListF, ofCrAnListF_mul_normalOrderF_ofFieldOpListF_eq_superCommuteF, normalOrderF_superCommuteF_ofCrAnListF_create_create_ofCrAnListF, normalOrderF_swap_create_annihilate_ofCrAnListF_ofCrAnListF, FieldSpecification.WickAlgebra.ι_normalOrderF_superCommuteF_ofCrAnListF_ofCrAnListF_eq_zero, FieldSpecification.WickAlgebra.ι_normalOrderF_superCommuteF_eq_zero_mul_mul_right, FieldSpecification.WickAlgebra.ι_normalOrderF_zero_of_mem_ideal, normalOrderF_superCommuteF_crPartF_anPartF, normalOrderF_superCommuteF_create_annihilate, normalOrderF_crPartF_mul, normalOrderF_swap_create_annihilate, normalOrderF_normalOrderF_right, normalOrderF_anPartF_mul_anPartF, FieldSpecification.WickAlgebra.ι_normalOrder_superCommuteF_eq_zero_mul_right, normalOrderF_one, FieldSpecification.WickAlgebra.ι_normalOrderF_superCommuteF_eq_zero_mul, normalOrderF_create_mul, normalOrderF_ofFieldOpF_mul_ofFieldOpF, ofCrAnListF_superCommuteF_normalOrderF_ofFieldOpListF, normalOrderF_superCommuteF_anPartF_crPartF, FieldSpecification.WickAlgebra.ι_normalOrderF_superCommuteF_ofCrAnListF_eq_zero, normalOrderF_normalOrderF_mid, normalOrderF_superCommuteF_annihilate_create, normalOrderF_ofCrAnListF_append_annihilate, anPartF_mul_normalOrderF_ofFieldOpListF_eq_superCommuteF, FieldSpecification.WickAlgebra.ι_normalOrderF_superCommuteF_ofCrAnListF_eq_zero_mul, FieldSpecification.WickAlgebra.ι_normalOrderF_superCommuteF_ofCrAnOpF_ofCrAnListF_eq_zero_mul, FieldSpecification.WickAlgebra.ι_normalOrderF_superCommuteF_ofCrAnOpF_eq_zero_mul, normalOrderF_normalOrderF_left
«term𝓝ᶠ(_)» 📖» "API Documentation")	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
anPartF_mul_normalOrderF_ofFieldOpListF_eq_superCommuteF 📖	mathematical	—	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp anPartF normalOrderF ofFieldOpListF FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign FieldSpecification.fieldOpStatistic FieldStatistic.ofList FieldSpecification.FieldOp superCommuteF	—	normalOrderF_mul_anPartF anPartF_negAsymp anPartF_position ofCrAnOpF_mul_normalOrderF_ofFieldOpListF_eq_superCommuteF anPartF_posAsymp
normalOrderF_anPartF_mul_anPartF 📖	mathematical	—	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp normalOrderF anPartF	—	normalOrderF_mul_anPartF normalOrderF_one
normalOrderF_anPartF_mul_crPartF 📖	mathematical	—	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp normalOrderF anPartF crPartF FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign FieldSpecification.fieldOpStatistic	—	normalOrderF_swap_anPartF_crPartF normalOrderF_crPartF_mul_anPartF
normalOrderF_crPartF_mul 📖	mathematical	—	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp normalOrderF crPartF	—	crPartF.eq_1 normalOrderF_create_mul crPartF.eq_2 crPartF_posAsymp
normalOrderF_crPartF_mul_anPartF 📖	mathematical	—	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp normalOrderF crPartF anPartF	—	normalOrderF_crPartF_mul normalOrderF_mul_anPartF normalOrderF_one
normalOrderF_crPartF_mul_crPartF 📖	mathematical	—	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp normalOrderF crPartF	—	normalOrderF_crPartF_mul normalOrderF_one
normalOrderF_create_mul 📖	mathematical	FieldSpecification.crAnFieldOpToCreateAnnihilate CreateAnnihilate.create	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp normalOrderF ofCrAnOpF	—	ofListBasis_eq_ofList ofCrAnListF_cons normalOrderF_ofCrAnListF_cons_create
normalOrderF_mul_anPartF 📖	mathematical	—	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp normalOrderF anPartF	—	anPartF_negAsymp anPartF.eq_2 normalOrderF_mul_annihilate anPartF.eq_3
normalOrderF_mul_annihilate 📖	mathematical	FieldSpecification.crAnFieldOpToCreateAnnihilate CreateAnnihilate.annihilate	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp normalOrderF ofCrAnOpF	—	ofListBasis_eq_ofList ofCrAnListF_singleton ofCrAnListF_append normalOrderF_ofCrAnListF_append_annihilate
normalOrderF_normalOrderF_left 📖	mathematical	—	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp normalOrderF	—	normalOrderF_normalOrderF_mid
normalOrderF_normalOrderF_mid 📖	mathematical	—	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp normalOrderF	—	ofListBasis_eq_ofList normalOrderF_ofCrAnListF Wick.koszulSign_of_append_eq_insertionSort FieldSpecification.instIsTotalCrAnFieldOpNormalOrderRel FieldSpecification.instIsTransCrAnFieldOpNormalOrderRel PhysLean.List.insertionSort_append_insertionSort_append
normalOrderF_normalOrderF_right 📖	mathematical	—	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp normalOrderF	—	normalOrderF_normalOrderF_mid
normalOrderF_ofCrAnListF 📖	mathematical	—	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp normalOrderF ofCrAnListF FieldSpecification.normalOrderSign FieldSpecification.normalOrderList	—	ofListBasis_eq_ofList normalOrderF.eq_1
normalOrderF_ofCrAnListF_append_annihilate 📖	mathematical	FieldSpecification.crAnFieldOpToCreateAnnihilate CreateAnnihilate.annihilate	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp normalOrderF ofCrAnListF ofCrAnOpF	—	normalOrderF_ofCrAnListF FieldSpecification.normalOrderSign_append_annihilate FieldSpecification.normalOrderList_append_annihilate ofCrAnListF_append ofCrAnListF_singleton
normalOrderF_ofCrAnListF_cons_create 📖	mathematical	FieldSpecification.crAnFieldOpToCreateAnnihilate CreateAnnihilate.create	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp normalOrderF ofCrAnListF ofCrAnOpF	—	normalOrderF_ofCrAnListF FieldSpecification.normalOrderSign_cons_create FieldSpecification.normalOrderList_cons_create ofCrAnListF_cons
normalOrderF_ofFieldOpF_mul_ofFieldOpF 📖	mathematical	—	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp normalOrderF ofFieldOpF crPartF FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign FieldSpecification.fieldOpStatistic anPartF	—	ofFieldOpF_eq_crPartF_add_anPartF normalOrderF_crPartF_mul_crPartF normalOrderF_anPartF_mul_crPartF normalOrderF_crPartF_mul_anPartF normalOrderF_anPartF_mul_anPartF
normalOrderF_one 📖	mathematical	—	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp normalOrderF	—	ofCrAnListF_nil normalOrderF_ofCrAnListF FieldSpecification.normalOrderSign_nil FieldSpecification.normalOrderList_nil
normalOrderF_superCommuteF_anPartF_crPartF 📖	mathematical	—	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp normalOrderF superCommuteF anPartF crPartF	—	anPartF_negAsymp crPartF_posAsymp anPartF_position crPartF_position normalOrderF_superCommuteF_annihilate_create anPartF_posAsymp crPartF_negAsymp
normalOrderF_superCommuteF_annihilate_create 📖	mathematical	FieldSpecification.crAnFieldOpToCreateAnnihilate CreateAnnihilate.create CreateAnnihilate.annihilate	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp normalOrderF superCommuteF ofCrAnOpF	—	superCommuteF_ofCrAnOpF_ofCrAnOpF_symm normalOrderF_superCommuteF_create_annihilate
normalOrderF_superCommuteF_crPartF_anPartF 📖	mathematical	—	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp normalOrderF superCommuteF crPartF anPartF	—	anPartF_negAsymp crPartF_posAsymp crPartF_position anPartF_position normalOrderF_superCommuteF_create_annihilate crPartF_negAsymp anPartF_posAsymp
normalOrderF_superCommuteF_create_annihilate 📖	mathematical	FieldSpecification.crAnFieldOpToCreateAnnihilate CreateAnnihilate.create CreateAnnihilate.annihilate	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp normalOrderF superCommuteF ofCrAnOpF	—	superCommuteF_ofCrAnOpF_ofCrAnOpF normalOrderF_swap_create_annihilate
normalOrderF_superCommuteF_ofCrAnListF_annihilate_annihilate_ofCrAnListF 📖	mathematical	FieldSpecification.crAnFieldOpToCreateAnnihilate CreateAnnihilate.annihilate	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp normalOrderF ofCrAnListF superCommuteF ofCrAnOpF FieldSpecification.normalOrderSign FieldSpecification.createFilter FieldSpecification.annihilateFilter	—	superCommuteF_ofCrAnOpF_ofCrAnOpF ofCrAnListF_singleton ofCrAnListF_append normalOrderF_ofCrAnListF FieldSpecification.normalOrderList_eq_createFilter_append_annihilateFilter FieldSpecification.createFilter_append FieldSpecification.createFilter_singleton_annihilate FieldSpecification.annihilateFilter_append FieldSpecification.annihilateFilter_singleton_annihilate FieldSpecification.normalOrderSign_swap_annihilate_annihilate
normalOrderF_superCommuteF_ofCrAnListF_create_create_ofCrAnListF 📖	mathematical	FieldSpecification.crAnFieldOpToCreateAnnihilate CreateAnnihilate.create	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp normalOrderF ofCrAnListF superCommuteF ofCrAnOpF FieldSpecification.normalOrderSign FieldSpecification.createFilter FieldSpecification.annihilateFilter	—	superCommuteF_ofCrAnOpF_ofCrAnOpF ofCrAnListF_singleton ofCrAnListF_append normalOrderF_ofCrAnListF FieldSpecification.normalOrderList_eq_createFilter_append_annihilateFilter FieldSpecification.createFilter_append FieldSpecification.createFilter_singleton_create FieldSpecification.annihilateFilter_append FieldSpecification.annihilateFilter_singleton_create FieldSpecification.normalOrderSign_swap_create_create
normalOrderF_swap_anPartF_crPartF 📖	mathematical	—	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp normalOrderF anPartF crPartF FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign FieldSpecification.fieldOpStatistic	—	normalOrderF_swap_crPartF_anPartF FieldStatistic.exchangeSign_mul_self_swap
normalOrderF_swap_crPartF_anPartF 📖	mathematical	—	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp normalOrderF crPartF anPartF FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign FieldSpecification.fieldOpStatistic	—	anPartF_negAsymp crPartF_posAsymp crPartF_position anPartF_position normalOrderF_swap_create_annihilate crPartF_negAsymp anPartF_posAsymp
normalOrderF_swap_create_annihilate 📖	mathematical	FieldSpecification.crAnFieldOpToCreateAnnihilate CreateAnnihilate.create CreateAnnihilate.annihilate	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp normalOrderF ofCrAnOpF FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign FieldSpecification.crAnStatistics	—	ofListBasis_eq_ofList normalOrderF_swap_create_annihilate_ofCrAnListF
normalOrderF_swap_create_annihilate_ofCrAnListF 📖	mathematical	FieldSpecification.crAnFieldOpToCreateAnnihilate CreateAnnihilate.create CreateAnnihilate.annihilate	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp normalOrderF ofCrAnListF ofCrAnOpF FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign FieldSpecification.crAnStatistics	—	ofListBasis_eq_ofList normalOrderF_swap_create_annihilate_ofCrAnListF_ofCrAnListF
normalOrderF_swap_create_annihilate_ofCrAnListF_ofCrAnListF 📖	mathematical	FieldSpecification.crAnFieldOpToCreateAnnihilate CreateAnnihilate.create CreateAnnihilate.annihilate	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp normalOrderF ofCrAnListF ofCrAnOpF FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign FieldSpecification.crAnStatistics	—	ofCrAnListF_cons ofCrAnListF_append normalOrderF_ofCrAnListF FieldSpecification.normalOrderSign_swap_create_annihilate FieldSpecification.normalOrderList_swap_create_annihilate
ofCrAnListF_eq_normalOrderF 📖	mathematical	—	ofCrAnListF FieldSpecification.normalOrderList FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.normalOrderSign normalOrderF	—	normalOrderF_ofCrAnListF FieldSpecification.normalOrderList.eq_1 FieldSpecification.normalOrderSign.eq_1 Wick.koszulSign_mul_self
ofCrAnListF_mul_normalOrderF_ofFieldOpListF_eq_superCommuteF 📖	mathematical	—	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp ofCrAnListF normalOrderF ofFieldOpListF FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign FieldStatistic.ofList FieldSpecification.crAnStatistics FieldSpecification.FieldOp FieldSpecification.fieldOpStatistic superCommuteF	—	ofCrAnListF_superCommuteF_normalOrderF_ofFieldOpListF
ofCrAnListF_superCommuteF_normalOrderF_ofCrAnListF 📖	mathematical	—	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp superCommuteF ofCrAnListF normalOrderF FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign FieldStatistic.ofList FieldSpecification.crAnStatistics	—	normalOrderF_ofCrAnListF superCommuteF_ofCrAnListF_ofCrAnListF ofCrAnListF_append FieldSpecification.normalOrderList_statistics
ofCrAnListF_superCommuteF_normalOrderF_ofFieldOpListF 📖	mathematical	—	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp superCommuteF ofCrAnListF normalOrderF ofFieldOpListF FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign FieldStatistic.ofList FieldSpecification.crAnStatistics FieldSpecification.FieldOp FieldSpecification.fieldOpStatistic	—	ofFieldOpListF_sum ofCrAnListF_superCommuteF_normalOrderF_ofCrAnListF FieldSpecification.CrAnSection.statistics_eq_state_statistics
ofCrAnOpF_mul_normalOrderF_ofFieldOpListF_eq_superCommuteF 📖	mathematical	—	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp ofCrAnOpF normalOrderF ofFieldOpListF FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign FieldSpecification.crAnStatistics FieldStatistic.ofList FieldSpecification.FieldOp FieldSpecification.fieldOpStatistic superCommuteF	—	ofCrAnListF_mul_normalOrderF_ofFieldOpListF_eq_superCommuteF FieldStatistic.ofList_singleton

---

← Back to Index