TimeOrder

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

Statistics

Metric	Count
Definitions timeOrder, «term𝓣(_)»»)	2
Theorems timeOrder_eq_maxTimeField_mul_finset, timeOrder_eq_ι_timeOrderF, timeOrder_ofFieldOpList_nil, timeOrder_ofFieldOpList_singleton, timeOrder_ofFieldOp_ofFieldOp_not_ordered, timeOrder_ofFieldOp_ofFieldOp_not_ordered_eq_timeOrder, timeOrder_ofFieldOp_ofFieldOp_ordered, timeOrder_superCommute_anPart_ofFieldOp_neq_time, timeOrder_superCommute_eq_time_left, timeOrder_superCommute_eq_time_mid, timeOrder_superCommute_neq_time, timeOrder_timeOrder, timeOrder_timeOrder_left, timeOrder_timeOrder_mid, timeOrder_timeOrder_right, ι_timeOrderF_eq_of_equiv, ι_timeOrderF_superCommuteF_eq_time, ι_timeOrderF_superCommuteF_neq_time, ι_timeOrderF_superCommuteF_superCommuteF, ι_timeOrderF_superCommuteF_superCommuteF_eq_time_ofCrAnListF, ι_timeOrderF_superCommuteF_superCommuteF_ofCrAnListF, ι_timeOrderF_zero_of_mem_ideal	22
Total	24

FieldSpecification.WickAlgebra

Definitions

Name	Category	Theorems
timeOrder 📖	CompOp	32 math math: timeOrder_ofFieldOp_ofFieldOp_not_ordered_eq_timeOrder, timeOrder_ofFieldOpList_nil, timeContract_eq_smul, timeOrder_ofFieldOpList_singleton, timeOrder_superCommute_eq_time_left, WickContraction.EqTimeOnly.timeOrder_staticContract_of_not_mem, wicks_theorem_normal_order_empty, timeOrder_superCommute_anPart_ofFieldOp_neq_time, timeOrder_timeOrder_left, WickContraction.EqTimeOnly.timeOrder_timeContract_mul_of_eqTimeOnly_mid, timeOrder_timeOrder, WickContraction.EqTimeOnly.timeOrder_timeContract_mul_of_eqTimeOnly_mid_induction, timeOrder_timeContract_eq_time_left, timeOrder_superCommute_eq_time_mid, timeOrder_eq_maxTimeField_mul_finset, timeOrder_eq_ι_timeOrderF, timeOrder_timeOrder_right, timeOrder_ofFieldOp_ofFieldOp_ordered, wicks_theorem_normal_order, timeOrder_timeContract_eq_time_mid, normalOrder_timeOrder_ofFieldOpList_eq_eqTimeOnly_empty, timeOrder_superCommute_neq_time, WickContraction.EqTimeOnly.timeOrder_timeContract_mul_of_eqTimeOnly_left, timeOrder_ofFieldOp_ofFieldOp_not_ordered, timeOrder_timeContract_neq_time, WickContraction.EqTimeOnly.timeOrder_timeContract_of_not_eqTimeOnly, normalOrder_timeOrder_ofFieldOpList_eq_not_haveEqTime_sub_inductive, timeOrder_ofFieldOpList_eq_eqTimeOnly_empty, timeOrder_timeOrder_mid, FieldSpecification.wicks_theorem, timeOrder_haveEqTime_split, timeOrder_ofFieldOpList_eqTimeOnly
«term𝓣(_)» 📖» "API Documentation")	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
timeOrder_eq_maxTimeField_mul_finset 📖	mathematical	—	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet timeOrder ofFieldOpList FieldSpecification.FieldOp FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign FieldSpecification.fieldOpStatistic FieldSpecification.maxTimeField FieldStatistic.ofFinset FieldSpecification.eraseMaxTimeField FieldSpecification.maxTimeFieldPosFin ofFieldOp	—	ofFieldOpList.eq_1 timeOrder_eq_ι_timeOrderF FieldSpecification.FieldOpFreeAlgebra.timeOrderF_eq_maxTimeField_mul_finset
timeOrder_eq_ι_timeOrderF 📖	mathematical	—	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet timeOrder ι FieldSpecification.FieldOpFreeAlgebra.timeOrderF	—	—
timeOrder_ofFieldOpList_nil 📖	mathematical	—	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet timeOrder ofFieldOpList FieldSpecification.FieldOp	—	ofFieldOpList.eq_1 timeOrder_eq_ι_timeOrderF FieldSpecification.FieldOpFreeAlgebra.timeOrderF_ofFieldOpListF_nil
timeOrder_ofFieldOpList_singleton 📖	mathematical	—	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet timeOrder ofFieldOpList FieldSpecification.FieldOp	—	ofFieldOpList.eq_1 timeOrder_eq_ι_timeOrderF FieldSpecification.FieldOpFreeAlgebra.timeOrderF_ofFieldOpListF_singleton
timeOrder_ofFieldOp_ofFieldOp_not_ordered 📖	mathematical	FieldSpecification.timeOrderRel	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet timeOrder ofFieldOp FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign FieldSpecification.fieldOpStatistic	—	ofFieldOp.eq_1 timeOrder_eq_ι_timeOrderF FieldSpecification.FieldOpFreeAlgebra.timeOrderF_ofFieldOpF_ofFieldOpF_not_ordered
timeOrder_ofFieldOp_ofFieldOp_not_ordered_eq_timeOrder 📖	mathematical	FieldSpecification.timeOrderRel	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet timeOrder ofFieldOp FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign FieldSpecification.fieldOpStatistic	—	ofFieldOp.eq_1 timeOrder_eq_ι_timeOrderF FieldSpecification.FieldOpFreeAlgebra.timeOrderF_ofFieldOpF_ofFieldOpF_not_ordered_eq_timeOrderF
timeOrder_ofFieldOp_ofFieldOp_ordered 📖	mathematical	FieldSpecification.timeOrderRel	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet timeOrder ofFieldOp	—	ofFieldOp.eq_1 timeOrder_eq_ι_timeOrderF FieldSpecification.FieldOpFreeAlgebra.timeOrderF_ofFieldOpF_ofFieldOpF_ordered
timeOrder_superCommute_anPart_ofFieldOp_neq_time 📖	mathematical	FieldSpecification.timeOrderRel	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet timeOrder superCommute anPart ofFieldOp	—	ofFieldOp_eq_sum anPart_inAsymp anPart_position timeOrder_superCommute_neq_time anPart_outAsymp
timeOrder_superCommute_eq_time_left 📖	mathematical	FieldSpecification.crAnTimeOrderRel	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet timeOrder superCommute ofCrAnOp	—	timeOrder_superCommute_eq_time_mid
timeOrder_superCommute_eq_time_mid 📖	mathematical	FieldSpecification.crAnTimeOrderRel	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet timeOrder superCommute ofCrAnOp	—	ofCrAnOp.eq_1 superCommute_eq_ι_superCommuteF ι_surjective timeOrder_eq_ι_timeOrderF ι_timeOrderF_superCommuteF_eq_time
timeOrder_superCommute_neq_time 📖	mathematical	FieldSpecification.crAnTimeOrderRel	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet timeOrder superCommute ofCrAnOp	—	ofCrAnOp.eq_1 superCommute_eq_ι_superCommuteF timeOrder_eq_ι_timeOrderF ι_timeOrderF_superCommuteF_neq_time
timeOrder_timeOrder 📖	mathematical	—	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet timeOrder	—	timeOrder_timeOrder_left
timeOrder_timeOrder_left 📖	mathematical	—	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet timeOrder	—	timeOrder_timeOrder_mid
timeOrder_timeOrder_mid 📖	mathematical	—	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet timeOrder	—	ι_surjective timeOrder_eq_ι_timeOrderF FieldSpecification.FieldOpFreeAlgebra.timeOrderF_timeOrderF_mid
timeOrder_timeOrder_right 📖	mathematical	—	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet timeOrder	—	timeOrder_timeOrder_mid
ι_timeOrderF_eq_of_equiv 📖	mathematical	FieldSpecification.FieldOpFreeAlgebra instSetoidFieldOpFreeAlgebra	FieldSpecification.WickAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet ι FieldSpecification.FieldOpFreeAlgebra.timeOrderF	—	ι_timeOrderF_zero_of_mem_ideal equiv_iff_sub_mem_ideal
ι_timeOrderF_superCommuteF_eq_time 📖	mathematical	FieldSpecification.crAnTimeOrderRel	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.WickAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet ι FieldSpecification.FieldOpFreeAlgebra.timeOrderF FieldSpecification.FieldOpFreeAlgebra.superCommuteF FieldSpecification.FieldOpFreeAlgebra.ofCrAnOpF	—	FieldSpecification.FieldOpFreeAlgebra.ofListBasis_eq_ofList FieldSpecification.FieldOpFreeAlgebra.ofCrAnListF_singleton FieldSpecification.FieldOpFreeAlgebra.superCommuteF_ofCrAnListF_ofCrAnListF FieldStatistic.ofList_singleton FieldSpecification.FieldOpFreeAlgebra.timeOrderF_ofCrAnListF FieldSpecification.crAnTimeOrderSign.eq_1 Wick.koszulSign_perm_eq FieldSpecification.instIsTransCrAnFieldOpCrAnTimeOrderRel Wick.koszulSign.congr_simp PhysLean.List.insertionSort_of_eq_list FieldSpecification.instIsTotalCrAnFieldOpCrAnTimeOrderRel FieldSpecification.crAnTimeOrderList.eq_1 FieldSpecification.FieldOpFreeAlgebra.ofCrAnListF_append FieldSpecification.FieldOpFreeAlgebra.superCommuteF_ofCrAnOpF_ofCrAnOpF ι_superCommuteF_ofCrAnOpF_ofCrAnOpF_mem_center PhysLean.List.insertionSort_of_takeWhile_filter ι_superCommuteF_of_diff_statistic Wick.koszulSign_eq_rel_eq_stat
ι_timeOrderF_superCommuteF_neq_time 📖	mathematical	FieldSpecification.crAnTimeOrderRel	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.WickAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet ι FieldSpecification.FieldOpFreeAlgebra.timeOrderF FieldSpecification.FieldOpFreeAlgebra.superCommuteF FieldSpecification.FieldOpFreeAlgebra.ofCrAnOpF	—	FieldSpecification.FieldOpFreeAlgebra.timeOrderF_timeOrderF_mid FieldSpecification.FieldOpFreeAlgebra.timeOrderF_superCommuteF_ofCrAnOpF_ofCrAnOpF_not_crAnTimeOrderRel FieldSpecification.FieldOpFreeAlgebra.superCommuteF_ofCrAnOpF_ofCrAnOpF_symm
ι_timeOrderF_superCommuteF_superCommuteF 📖	mathematical	—	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.WickAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet ι FieldSpecification.FieldOpFreeAlgebra.timeOrderF FieldSpecification.FieldOpFreeAlgebra.superCommuteF FieldSpecification.FieldOpFreeAlgebra.ofCrAnOpF	—	FieldSpecification.FieldOpFreeAlgebra.ofListBasis_eq_ofList ι_timeOrderF_superCommuteF_superCommuteF_ofCrAnListF
ι_timeOrderF_superCommuteF_superCommuteF_eq_time_ofCrAnListF 📖	mathematical	FieldSpecification.crAnTimeOrderRel	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.WickAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet ι FieldSpecification.FieldOpFreeAlgebra.timeOrderF FieldSpecification.FieldOpFreeAlgebra.ofCrAnListF FieldSpecification.FieldOpFreeAlgebra.superCommuteF FieldSpecification.FieldOpFreeAlgebra.ofCrAnOpF	—	PhysLean.List.insertionSort_of_eq_list FieldSpecification.instIsTotalCrAnFieldOpCrAnTimeOrderRel FieldSpecification.instIsTransCrAnFieldOpCrAnTimeOrderRel FieldSpecification.FieldOpFreeAlgebra.timeOrderF_ofCrAnListF FieldSpecification.crAnTimeOrderList.eq_1 FieldSpecification.FieldOpFreeAlgebra.ofCrAnListF_append FieldSpecification.crAnTimeOrderSign.eq_1 Wick.koszulSign_perm_eq FieldSpecification.FieldOpFreeAlgebra.ofCrAnListF_singleton FieldSpecification.FieldOpFreeAlgebra.superCommuteF_ofCrAnListF_ofCrAnListF FieldStatistic.ofList_singleton ι_superCommuteF_ofCrAnOpF_superCommuteF_ofCrAnOpF_ofCrAnOpF
ι_timeOrderF_superCommuteF_superCommuteF_ofCrAnListF 📖	mathematical	—	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.WickAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet ι FieldSpecification.FieldOpFreeAlgebra.timeOrderF FieldSpecification.FieldOpFreeAlgebra.ofCrAnListF FieldSpecification.FieldOpFreeAlgebra.superCommuteF FieldSpecification.FieldOpFreeAlgebra.ofCrAnOpF	—	ι_timeOrderF_superCommuteF_superCommuteF_eq_time_ofCrAnListF FieldSpecification.FieldOpFreeAlgebra.timeOrderF_timeOrderF_mid FieldSpecification.FieldOpFreeAlgebra.timeOrderF_superCommuteF_ofCrAnOpF_superCommuteF_all_not_crAnTimeOrderRel
ι_timeOrderF_zero_of_mem_ideal 📖	mathematical	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet	FieldSpecification.WickAlgebra ι FieldSpecification.FieldOpFreeAlgebra.timeOrderF	—	ι_timeOrderF_superCommuteF_superCommuteF ι_timeOrderF_superCommuteF_eq_time ι_superCommuteF_of_create_create ι_timeOrderF_superCommuteF_neq_time ι_superCommuteF_of_annihilate_annihilate ι_superCommuteF_of_diff_statistic

---

← Back to Index