Lemmas

📁 Source: PhysLean/QFT/PerturbationTheory/WickAlgebra/NormalOrder/Lemmas.lean

Statistics

Metric	Count
Definitions contractStateAtIndex	1
Theorems anPart_mul_normalOrder_ofFieldOpList_eq_superCommute, anPart_mul_normalOrder_ofFieldOpList_eq_superCommute_reorder, anPart_superCommute_normalOrder_ofFieldOpList_sum, crPart_mul_normalOrder, normalOrder_anPart_mul_anPart, normalOrder_anPart_mul_crPart, normalOrder_anPart_ofFieldOpList_swap, normalOrder_crPart_mul_anPart, normalOrder_crPart_mul_crPart, normalOrder_eq_ι_normalOrderF, normalOrder_mul_anPart, normalOrder_normalOrder, normalOrder_normalOrder_left, normalOrder_normalOrder_mid, normalOrder_normalOrder_right, normalOrder_ofCrAnList, normalOrder_ofCrAnList_nil, normalOrder_ofCrAnOp_ofCrAnList, normalOrder_ofCrAnOp_ofFieldOpList_swap, normalOrder_ofFieldOpList_anPart_swap, normalOrder_ofFieldOpList_mul_anPart_swap, normalOrder_ofFieldOpList_nil, normalOrder_ofFieldOp_mul_ofFieldOp, normalOrder_ofFieldOp_ofFieldOp_swap, normalOrder_one_eq_one, normalOrder_superCommute_eq_zero, normalOrder_superCommute_left_eq_zero, normalOrder_superCommute_mid_eq_zero, normalOrder_superCommute_right_eq_zero, ofCrAnList_eq_normalOrder, ofCrAnOp_superCommute_normalOrder_ofCrAnList_sum, ofCrAnOp_superCommute_normalOrder_ofFieldOpList_sum, ofFieldOpList_normalOrder_insert, ofFieldOp_mul_normalOrder_ofFieldOpList_eq_sum, ofFieldOp_mul_normalOrder_ofFieldOpList_eq_superCommute	35
Total	36

FieldSpecification.WickAlgebra

Definitions

Name	Category	Theorems
contractStateAtIndex 📖	CompOp	6 math math: WickContraction.wickTerm_insert_some, WickContraction.staticContract_insert_some_of_lt, WickContraction.staticWickTerm_insert_zero_some, WickContraction.timeContract_insert_some_of_not_lt, WickContraction.timeContract_insert_some_of_lt, ofFieldOp_mul_normalOrder_ofFieldOpList_eq_sum

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
anPart_mul_normalOrder_ofFieldOpList_eq_superCommute 📖	mathematical	—	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet anPart normalOrder ofFieldOpList FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign FieldSpecification.fieldOpStatistic FieldStatistic.ofList FieldSpecification.FieldOp superCommute	—	anPart.eq_1 ofFieldOpList.eq_1 normalOrder_eq_ι_normalOrderF FieldSpecification.FieldOpFreeAlgebra.anPartF_mul_normalOrderF_ofFieldOpListF_eq_superCommuteF
anPart_mul_normalOrder_ofFieldOpList_eq_superCommute_reorder 📖	mathematical	—	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet anPart normalOrder ofFieldOpList superCommute	—	anPart_mul_normalOrder_ofFieldOpList_eq_superCommute normalOrder_anPart_ofFieldOpList_swap
anPart_superCommute_normalOrder_ofFieldOpList_sum 📖	mathematical	—	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet superCommute anPart normalOrder ofFieldOpList FieldSpecification.FieldOp FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign FieldSpecification.fieldOpStatistic FieldStatistic.ofList FieldSpecification.FieldOpFreeAlgebra.ofFieldOpF	—	anPart_inAsymp anPart_position ofCrAnOp_superCommute_normalOrder_ofFieldOpList_sum anPart_outAsymp
crPart_mul_normalOrder 📖	mathematical	—	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet normalOrder crPart	—	ι_surjective crPart.eq_1 normalOrder_eq_ι_normalOrderF FieldSpecification.FieldOpFreeAlgebra.normalOrderF_crPartF_mul
normalOrder_anPart_mul_anPart 📖	mathematical	—	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet normalOrder anPart	—	anPart.eq_1 normalOrder_eq_ι_normalOrderF FieldSpecification.FieldOpFreeAlgebra.normalOrderF_anPartF_mul_anPartF
normalOrder_anPart_mul_crPart 📖	mathematical	—	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet normalOrder anPart crPart FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign FieldSpecification.fieldOpStatistic	—	anPart.eq_1 crPart.eq_1 normalOrder_eq_ι_normalOrderF FieldSpecification.FieldOpFreeAlgebra.normalOrderF_anPartF_mul_crPartF
normalOrder_anPart_ofFieldOpList_swap 📖	mathematical	—	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet normalOrder anPart ofFieldOpList FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign FieldSpecification.fieldOpStatistic FieldStatistic.ofList FieldSpecification.FieldOp	—	anPart_inAsymp anPart_position normalOrder_ofCrAnOp_ofFieldOpList_swap anPart_outAsymp
normalOrder_crPart_mul_anPart 📖	mathematical	—	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet normalOrder crPart anPart	—	crPart.eq_1 anPart.eq_1 normalOrder_eq_ι_normalOrderF FieldSpecification.FieldOpFreeAlgebra.normalOrderF_crPartF_mul_anPartF
normalOrder_crPart_mul_crPart 📖	mathematical	—	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet normalOrder crPart	—	crPart.eq_1 normalOrder_eq_ι_normalOrderF FieldSpecification.FieldOpFreeAlgebra.normalOrderF_crPartF_mul_crPartF
normalOrder_eq_ι_normalOrderF 📖	mathematical	—	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet normalOrder ι FieldSpecification.FieldOpFreeAlgebra.normalOrderF	—	—
normalOrder_mul_anPart 📖	mathematical	—	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet normalOrder anPart	—	ι_surjective anPart.eq_1 normalOrder_eq_ι_normalOrderF FieldSpecification.FieldOpFreeAlgebra.normalOrderF_mul_anPartF
normalOrder_normalOrder 📖	mathematical	—	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet normalOrder	—	normalOrder_normalOrder_left
normalOrder_normalOrder_left 📖	mathematical	—	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet normalOrder	—	ι_surjective normalOrder_eq_ι_normalOrderF FieldSpecification.FieldOpFreeAlgebra.normalOrderF_normalOrderF_left
normalOrder_normalOrder_mid 📖	mathematical	—	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet normalOrder	—	ι_surjective normalOrder_eq_ι_normalOrderF FieldSpecification.FieldOpFreeAlgebra.normalOrderF_normalOrderF_mid
normalOrder_normalOrder_right 📖	mathematical	—	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet normalOrder	—	ι_surjective normalOrder_eq_ι_normalOrderF FieldSpecification.FieldOpFreeAlgebra.normalOrderF_normalOrderF_right
normalOrder_ofCrAnList 📖	mathematical	—	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet normalOrder ofCrAnList FieldSpecification.normalOrderSign FieldSpecification.normalOrderList	—	ofCrAnList.eq_1 normalOrder_eq_ι_normalOrderF FieldSpecification.FieldOpFreeAlgebra.normalOrderF_ofCrAnListF
normalOrder_ofCrAnList_nil 📖	mathematical	—	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet normalOrder ofCrAnList	—	normalOrder_ofCrAnList FieldSpecification.normalOrderList_nil
normalOrder_ofCrAnOp_ofCrAnList 📖	mathematical	—	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet normalOrder ofCrAnOp ofCrAnList FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign FieldSpecification.crAnStatistics FieldStatistic.ofList	—	ofCrAnList_singleton ofCrAnList_mul_ofCrAnList_eq_superCommute FieldStatistic.ofList_singleton normalOrder_superCommute_eq_zero
normalOrder_ofCrAnOp_ofFieldOpList_swap 📖	mathematical	—	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet normalOrder ofCrAnOp ofFieldOpList FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign FieldSpecification.crAnStatistics FieldStatistic.ofList FieldSpecification.FieldOp FieldSpecification.fieldOpStatistic	—	ofCrAnList_singleton ofCrAnList_mul_ofFieldOpList_eq_superCommute FieldStatistic.ofList_singleton normalOrder_superCommute_eq_zero
normalOrder_ofFieldOpList_anPart_swap 📖	mathematical	—	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet normalOrder ofFieldOpList anPart FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign FieldSpecification.fieldOpStatistic FieldStatistic.ofList FieldSpecification.FieldOp	—	normalOrder_anPart_ofFieldOpList_swap FieldStatistic.exchangeSign_mul_self
normalOrder_ofFieldOpList_mul_anPart_swap 📖	mathematical	—	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet normalOrder ofFieldOpList anPart FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign FieldSpecification.fieldOpStatistic FieldStatistic.ofList FieldSpecification.FieldOp	—	normalOrder_mul_anPart normalOrder_ofFieldOpList_anPart_swap
normalOrder_ofFieldOpList_nil 📖	mathematical	—	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet normalOrder ofFieldOpList FieldSpecification.FieldOp	—	ofFieldOpList.eq_1 normalOrder_eq_ι_normalOrderF normalOrder_one_eq_one
normalOrder_ofFieldOp_mul_ofFieldOp 📖	mathematical	—	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet normalOrder ofFieldOp crPart FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign FieldSpecification.fieldOpStatistic anPart	—	ofFieldOp.eq_1 normalOrder_eq_ι_normalOrderF FieldSpecification.FieldOpFreeAlgebra.normalOrderF_ofFieldOpF_mul_ofFieldOpF
normalOrder_ofFieldOp_ofFieldOp_swap 📖	mathematical	—	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet normalOrder ofFieldOp FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign FieldSpecification.fieldOpStatistic	—	ofFieldOp_mul_ofFieldOp_eq_superCommute normalOrder_superCommute_eq_zero
normalOrder_one_eq_one 📖	mathematical	—	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet normalOrder	—	normalOrder_ofCrAnList FieldSpecification.normalOrderList_nil
normalOrder_superCommute_eq_zero 📖	mathematical	—	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet normalOrder superCommute	—	ι_surjective superCommute_eq_ι_superCommuteF normalOrder_eq_ι_normalOrderF ι_normalOrderF_superCommuteF_eq_zero
normalOrder_superCommute_left_eq_zero 📖	mathematical	—	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet normalOrder superCommute	—	ι_surjective superCommute_eq_ι_superCommuteF normalOrder_eq_ι_normalOrderF ι_normalOrder_superCommuteF_eq_zero_mul_right
normalOrder_superCommute_mid_eq_zero 📖	mathematical	—	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet normalOrder superCommute	—	ι_surjective superCommute_eq_ι_superCommuteF normalOrder_eq_ι_normalOrderF ι_normalOrderF_superCommuteF_eq_zero_mul
normalOrder_superCommute_right_eq_zero 📖	mathematical	—	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet normalOrder superCommute	—	ι_surjective superCommute_eq_ι_superCommuteF normalOrder_eq_ι_normalOrderF ι_normalOrderF_superCommuteF_eq_zero_mul_left
ofCrAnList_eq_normalOrder 📖	mathematical	—	ofCrAnList FieldSpecification.normalOrderList FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet FieldSpecification.normalOrderSign normalOrder	—	normalOrder_ofCrAnList FieldSpecification.normalOrderSign.eq_1 Wick.koszulSign_mul_self
ofCrAnOp_superCommute_normalOrder_ofCrAnList_sum 📖	mathematical	—	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet superCommute ofCrAnOp normalOrder ofCrAnList FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign FieldSpecification.crAnStatistics FieldStatistic.ofList	—	normalOrder_ofCrAnList superCommute_ofCrAnOp_ofCrAnList_eq_sum FieldSpecification.sum_normalOrderList_length FieldSpecification.normalOrderList_get_normalOrderEquiv FieldSpecification.normalOrderList_eraseIdx_normalOrderEquiv ofCrAnList_eq_normalOrder FieldSpecification.normalOrderSign_eraseIdx FieldSpecification.normalOrderSign_mul_self FieldStatistic.exchangeSign_mul_self superCommute_diff_statistic
ofCrAnOp_superCommute_normalOrder_ofFieldOpList_sum 📖	mathematical	—	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet superCommute ofCrAnOp normalOrder ofFieldOpList FieldSpecification.FieldOp FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign FieldSpecification.crAnStatistics FieldStatistic.ofList FieldSpecification.fieldOpStatistic ofFieldOp	—	FieldSpecification.CrAnSection.length_eq ofFieldOpList_eq_sum ofCrAnOp_superCommute_normalOrder_ofCrAnList_sum FieldSpecification.CrAnSection.sum_over_length FieldSpecification.CrAnSection.take_statistics_eq_take_state_statistics FieldSpecification.CrAnSection.sum_eraseIdxEquiv FieldSpecification.CrAnSection.eraseIdxEquiv_symm_getElem FieldSpecification.CrAnSection.eraseIdxEquiv_symm_eraseIdx ofFieldOp_eq_sum
ofFieldOpList_normalOrder_insert 📖	mathematical	—	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet normalOrder ofFieldOpList FieldSpecification.FieldOp FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign FieldSpecification.fieldOpStatistic FieldStatistic.ofList	—	PhysLean.List.insertIdx_eq_take_drop ofFieldOpList_append ofFieldOpList_mul_ofFieldOpList_eq_superCommute FieldStatistic.ofList_singleton normalOrder_superCommute_left_eq_zero FieldStatistic.exchangeSign_mul_self_swap
ofFieldOp_mul_normalOrder_ofFieldOpList_eq_sum 📖	mathematical	—	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet ofFieldOp normalOrder ofFieldOpList FieldSpecification.FieldOp contractStateAtIndex PhysLean.List.optionEraseZ	—	ofFieldOp_mul_normalOrder_ofFieldOpList_eq_superCommute anPart_superCommute_normalOrder_ofFieldOpList_sum
ofFieldOp_mul_normalOrder_ofFieldOpList_eq_superCommute 📖	mathematical	—	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet ofFieldOp normalOrder ofFieldOpList superCommute anPart	—	ofFieldOp_eq_crPart_add_anPart anPart_mul_normalOrder_ofFieldOpList_eq_superCommute_reorder crPart_mul_normalOrder

---

← Back to Index