TimeOrder

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

Statistics

Metric	Count
Definitions timeOrderF, «term𝓣ᶠ(_)»»)	2
Theorems timeOrderF_eq_maxTimeField_mul, timeOrderF_eq_maxTimeField_mul_finset, timeOrderF_ofCrAnListF, timeOrderF_ofFieldOpF_ofFieldOpF_not_ordered, timeOrderF_ofFieldOpF_ofFieldOpF_not_ordered_eq_timeOrderF, timeOrderF_ofFieldOpF_ofFieldOpF_ordered, timeOrderF_ofFieldOpListF, timeOrderF_ofFieldOpListF_nil, timeOrderF_ofFieldOpListF_singleton, timeOrderF_superCommuteF_ofCrAnOpF_ofCrAnOpF_eq_time, timeOrderF_superCommuteF_ofCrAnOpF_ofCrAnOpF_not_crAnTimeOrderRel, timeOrderF_superCommuteF_ofCrAnOpF_ofCrAnOpF_not_crAnTimeOrderRel_left, timeOrderF_superCommuteF_ofCrAnOpF_ofCrAnOpF_not_crAnTimeOrderRel_mid, timeOrderF_superCommuteF_ofCrAnOpF_ofCrAnOpF_not_crAnTimeOrderRel_right, timeOrderF_superCommuteF_ofCrAnOpF_superCommuteF_all_not_crAnTimeOrderRel, timeOrderF_superCommuteF_ofCrAnOpF_superCommuteF_not_crAnTimeOrderRel, timeOrderF_superCommuteF_ofCrAnOpF_superCommuteF_not_crAnTimeOrderRel', timeOrderF_superCommuteF_superCommuteF_ofCrAnOpF_not_crAnTimeOrderRel, timeOrderF_timeOrderF_left, timeOrderF_timeOrderF_mid, timeOrderF_timeOrderF_right	21
Total	23

FieldSpecification.FieldOpFreeAlgebra

Definitions

Name	Category	Theorems
timeOrderF 📖	CompOp	29 math math: timeOrderF_superCommuteF_ofCrAnOpF_ofCrAnOpF_not_crAnTimeOrderRel_mid, timeOrderF_eq_maxTimeField_mul, timeOrderF_ofFieldOpListF_singleton, FieldSpecification.WickAlgebra.ι_timeOrderF_superCommuteF_superCommuteF_ofCrAnListF, timeOrderF_superCommuteF_ofCrAnOpF_ofCrAnOpF_not_crAnTimeOrderRel, timeOrderF_eq_maxTimeField_mul_finset, timeOrderF_superCommuteF_ofCrAnOpF_ofCrAnOpF_not_crAnTimeOrderRel_left, timeOrderF_ofFieldOpF_ofFieldOpF_not_ordered, timeOrderF_superCommuteF_ofCrAnOpF_ofCrAnOpF_eq_time, timeOrderF_ofFieldOpF_ofFieldOpF_not_ordered_eq_timeOrderF, FieldSpecification.WickAlgebra.timeOrder_eq_ι_timeOrderF, FieldSpecification.WickAlgebra.ι_timeOrderF_superCommuteF_superCommuteF, timeOrderF_superCommuteF_ofCrAnOpF_ofCrAnOpF_not_crAnTimeOrderRel_right, timeOrderF_timeOrderF_mid, timeOrderF_ofFieldOpListF_nil, timeOrderF_superCommuteF_ofCrAnOpF_superCommuteF_not_crAnTimeOrderRel, timeOrderF_timeOrderF_left, FieldSpecification.WickAlgebra.ι_timeOrderF_superCommuteF_eq_time, timeOrderF_ofFieldOpListF, timeOrderF_ofCrAnListF, FieldSpecification.WickAlgebra.ι_timeOrderF_superCommuteF_neq_time, FieldSpecification.WickAlgebra.ι_timeOrderF_superCommuteF_superCommuteF_eq_time_ofCrAnListF, timeOrderF_superCommuteF_superCommuteF_ofCrAnOpF_not_crAnTimeOrderRel, timeOrderF_ofFieldOpF_ofFieldOpF_ordered, timeOrderF_timeOrderF_right, timeOrderF_superCommuteF_ofCrAnOpF_superCommuteF_not_crAnTimeOrderRel', FieldSpecification.WickAlgebra.ι_timeOrderF_eq_of_equiv, FieldSpecification.WickAlgebra.ι_timeOrderF_zero_of_mem_ideal, timeOrderF_superCommuteF_ofCrAnOpF_superCommuteF_all_not_crAnTimeOrderRel
«term𝓣ᶠ(_)» 📖» "API Documentation")	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
timeOrderF_eq_maxTimeField_mul 📖	mathematical	—	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp timeOrderF ofFieldOpListF FieldSpecification.FieldOp FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign FieldSpecification.fieldOpStatistic FieldSpecification.maxTimeField FieldStatistic.ofList FieldSpecification.maxTimeFieldPos ofFieldOpF FieldSpecification.eraseMaxTimeField	—	timeOrderF_ofFieldOpListF FieldSpecification.timeOrderList_eq_maxTimeField_timeOrderList ofFieldOpListF_cons FieldSpecification.timerOrderSign_of_eraseMaxTimeField FieldStatistic.exchangeSign_mul_self
timeOrderF_eq_maxTimeField_mul_finset 📖	mathematical	—	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp timeOrderF ofFieldOpListF FieldSpecification.FieldOp FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign FieldSpecification.fieldOpStatistic FieldSpecification.maxTimeField FieldStatistic.ofFinset FieldSpecification.eraseMaxTimeField FieldSpecification.maxTimeFieldPosFin ofFieldOpF	—	timeOrderF_eq_maxTimeField_mul FieldStatistic.ofList_perm PhysLean.List.eraseIdx_length PhysLean.List.eraseIdx_get PhysLean.List.insertionSortMin_lt_length_succ
timeOrderF_ofCrAnListF 📖	mathematical	—	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp timeOrderF ofCrAnListF FieldSpecification.crAnTimeOrderSign FieldSpecification.crAnTimeOrderList	—	ofListBasis_eq_ofList
timeOrderF_ofFieldOpF_ofFieldOpF_not_ordered 📖	mathematical	FieldSpecification.timeOrderRel	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp timeOrderF ofFieldOpF FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign FieldSpecification.fieldOpStatistic	—	ofFieldOpListF_singleton ofFieldOpListF_append timeOrderF_ofFieldOpListF FieldSpecification.timeOrderSign_pair_not_ordered FieldSpecification.timeOrderList_pair_not_ordered
timeOrderF_ofFieldOpF_ofFieldOpF_not_ordered_eq_timeOrderF 📖	mathematical	FieldSpecification.timeOrderRel	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp timeOrderF ofFieldOpF FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign FieldSpecification.fieldOpStatistic	—	timeOrderF_ofFieldOpF_ofFieldOpF_not_ordered timeOrderF_ofFieldOpF_ofFieldOpF_ordered FieldSpecification.instIsTotalFieldOpTimeOrderRel
timeOrderF_ofFieldOpF_ofFieldOpF_ordered 📖	mathematical	FieldSpecification.timeOrderRel	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp timeOrderF ofFieldOpF	—	ofFieldOpListF_singleton ofFieldOpListF_append timeOrderF_ofFieldOpListF FieldSpecification.timeOrderSign_pair_ordered FieldSpecification.timeOrderList_pair_ordered
timeOrderF_ofFieldOpListF 📖	mathematical	—	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp timeOrderF ofFieldOpListF FieldSpecification.timeOrderSign FieldSpecification.timeOrderList	—	ofFieldOpListF_sum timeOrderF_ofCrAnListF FieldSpecification.crAnTimeOrderSign_crAnSection FieldSpecification.sum_crAnSections_timeOrder
timeOrderF_ofFieldOpListF_nil 📖	mathematical	—	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp timeOrderF ofFieldOpListF FieldSpecification.FieldOp	—	timeOrderF_ofFieldOpListF
timeOrderF_ofFieldOpListF_singleton 📖	mathematical	—	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp timeOrderF ofFieldOpListF FieldSpecification.FieldOp	—	timeOrderF_ofFieldOpListF Wick.koszulSign_singleton
timeOrderF_superCommuteF_ofCrAnOpF_ofCrAnOpF_eq_time 📖	mathematical	FieldSpecification.crAnTimeOrderRel	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp timeOrderF superCommuteF ofCrAnOpF	—	superCommuteF_ofCrAnOpF_ofCrAnOpF ofCrAnListF_singleton ofCrAnListF_append timeOrderF_ofCrAnListF FieldSpecification.crAnTimeOrderSign_pair_ordered FieldSpecification.crAnTimeOrderList_pair_ordered
timeOrderF_superCommuteF_ofCrAnOpF_ofCrAnOpF_not_crAnTimeOrderRel 📖	mathematical	FieldSpecification.crAnTimeOrderRel	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp timeOrderF superCommuteF ofCrAnOpF	—	superCommuteF_ofCrAnOpF_ofCrAnOpF ofCrAnListF_singleton ofCrAnListF_append timeOrderF_ofCrAnListF FieldSpecification.crAnTimeOrderSign_pair_not_ordered FieldSpecification.crAnTimeOrderList_pair_not_ordered FieldSpecification.instIsTotalCrAnFieldOpCrAnTimeOrderRel FieldSpecification.crAnTimeOrderSign_pair_ordered FieldStatistic.exchangeSign_symm FieldSpecification.crAnTimeOrderList_pair_ordered
timeOrderF_superCommuteF_ofCrAnOpF_ofCrAnOpF_not_crAnTimeOrderRel_left 📖	mathematical	FieldSpecification.crAnTimeOrderRel	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp timeOrderF superCommuteF ofCrAnOpF	—	timeOrderF_timeOrderF_left timeOrderF_superCommuteF_ofCrAnOpF_ofCrAnOpF_not_crAnTimeOrderRel
timeOrderF_superCommuteF_ofCrAnOpF_ofCrAnOpF_not_crAnTimeOrderRel_mid 📖	mathematical	FieldSpecification.crAnTimeOrderRel	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp timeOrderF superCommuteF ofCrAnOpF	—	timeOrderF_timeOrderF_mid timeOrderF_superCommuteF_ofCrAnOpF_ofCrAnOpF_not_crAnTimeOrderRel
timeOrderF_superCommuteF_ofCrAnOpF_ofCrAnOpF_not_crAnTimeOrderRel_right 📖	mathematical	FieldSpecification.crAnTimeOrderRel	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp timeOrderF superCommuteF ofCrAnOpF	—	timeOrderF_timeOrderF_right timeOrderF_superCommuteF_ofCrAnOpF_ofCrAnOpF_not_crAnTimeOrderRel
timeOrderF_superCommuteF_ofCrAnOpF_superCommuteF_all_not_crAnTimeOrderRel 📖	mathematical	FieldSpecification.crAnTimeOrderRel	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp timeOrderF superCommuteF ofCrAnOpF	—	timeOrderF_superCommuteF_superCommuteF_ofCrAnOpF_not_crAnTimeOrderRel superCommuteF_ofCrAnOpF_ofCrAnOpF_symm FieldSpecification.instIsTransCrAnFieldOpCrAnTimeOrderRel timeOrderF_superCommuteF_ofCrAnOpF_superCommuteF_not_crAnTimeOrderRel timeOrderF_superCommuteF_ofCrAnOpF_superCommuteF_not_crAnTimeOrderRel'
timeOrderF_superCommuteF_ofCrAnOpF_superCommuteF_not_crAnTimeOrderRel 📖	mathematical	FieldSpecification.crAnTimeOrderRel	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp timeOrderF superCommuteF ofCrAnOpF	—	ofCrAnListF_singleton summerCommute_jacobi_ofCrAnListF FieldStatistic.ofList_singleton timeOrderF_superCommuteF_superCommuteF_ofCrAnOpF_not_crAnTimeOrderRel superCommuteF_ofCrAnOpF_ofCrAnOpF_symm
timeOrderF_superCommuteF_ofCrAnOpF_superCommuteF_not_crAnTimeOrderRel' 📖	mathematical	FieldSpecification.crAnTimeOrderRel	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp timeOrderF superCommuteF ofCrAnOpF	—	ofCrAnListF_singleton summerCommute_jacobi_ofCrAnListF FieldStatistic.ofList_singleton superCommuteF_ofCrAnOpF_ofCrAnOpF_symm timeOrderF_superCommuteF_superCommuteF_ofCrAnOpF_not_crAnTimeOrderRel
timeOrderF_superCommuteF_superCommuteF_ofCrAnOpF_not_crAnTimeOrderRel 📖	mathematical	FieldSpecification.crAnTimeOrderRel	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp timeOrderF superCommuteF ofCrAnOpF	—	bosonicProjF_add_fermionicProjF bosonic_superCommuteF timeOrderF_superCommuteF_ofCrAnOpF_ofCrAnOpF_not_crAnTimeOrderRel_left timeOrderF_superCommuteF_ofCrAnOpF_ofCrAnOpF_not_crAnTimeOrderRel_right ofCrAnListF_singleton superCommuteF_ofCrAnListF_ofCrAnListF_bosonic_or_fermionic superCommuteF_bonsonic superCommuteF_fermionic_fermionic
timeOrderF_timeOrderF_left 📖	mathematical	—	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp timeOrderF	—	timeOrderF_timeOrderF_mid
timeOrderF_timeOrderF_mid 📖	mathematical	—	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp timeOrderF	—	ofListBasis_eq_ofList timeOrderF_ofCrAnListF Wick.koszulSign_of_append_eq_insertionSort FieldSpecification.instIsTotalCrAnFieldOpCrAnTimeOrderRel FieldSpecification.instIsTransCrAnFieldOpCrAnTimeOrderRel PhysLean.List.insertionSort_append_insertionSort_append
timeOrderF_timeOrderF_right 📖	mathematical	—	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp timeOrderF	—	timeOrderF_timeOrderF_mid

---

← Back to Index