TimeContraction

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

Statistics

Metric	Count
Definitions timeContract	1
Theorems normalOrder_timeContract, timeContract_eq_smul, timeContract_eq_superCommute, timeContract_inAsymp_inAsymp, timeContract_mem_center, timeContract_of_not_timeOrderRel, timeContract_of_not_timeOrderRel_expand, timeContract_of_timeOrderRel, timeContract_outAsymp_outAsymp, timeContract_zero_of_diff_grade, timeOrder_timeContract_eq_time_left, timeOrder_timeContract_eq_time_mid, timeOrder_timeContract_neq_time	13
Total	14

FieldSpecification.WickAlgebra

Definitions

Name	Category	Theorems
timeContract 📖	CompOp	15 math math: timeContract_eq_smul, timeContract_outAsymp_outAsymp, timeContract_zero_of_diff_grade, timeOrder_timeContract_eq_time_left, timeContract_of_not_timeOrderRel_expand, timeOrder_timeContract_eq_time_mid, timeContract_mem_center, timeOrder_timeContract_neq_time, timeContract_of_timeOrderRel, WickContraction.timeContract_insertAndContract_some, normalOrder_timeContract, timeContract_inAsymp_inAsymp, WickContraction.singleton_timeContract, timeContract_of_not_timeOrderRel, timeContract_eq_superCommute

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
normalOrder_timeContract 📖	mathematical	—	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet normalOrder timeContract	—	timeContract_of_timeOrderRel normalOrder_superCommute_eq_zero timeContract_of_not_timeOrderRel FieldSpecification.instIsTotalFieldOpTimeOrderRel
timeContract_eq_smul 📖	mathematical	—	timeContract FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet timeOrder ofFieldOp normalOrder	—	—
timeContract_eq_superCommute 📖	mathematical	—	timeContract FieldSpecification.WickAlgebra FieldSpecification.timeOrderRel FieldSpecification.instDecidableTimeOrderRel FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet superCommute anPart ofFieldOp FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign FieldSpecification.fieldOpStatistic	—	timeContract_of_timeOrderRel timeContract_of_not_timeOrderRel_expand
timeContract_inAsymp_inAsymp 📖	mathematical	—	timeContract FieldSpecification.FieldOp.inAsymp FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet	—	timeContract_eq_superCommute anPart_inAsymp
timeContract_mem_center 📖	mathematical	—	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet timeContract	—	timeContract_of_timeOrderRel superCommute_anPart_ofFieldOp_mem_center timeContract_of_not_timeOrderRel FieldSpecification.instIsTotalFieldOpTimeOrderRel
timeContract_of_not_timeOrderRel 📖	mathematical	FieldSpecification.timeOrderRel	timeContract FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign FieldSpecification.fieldOpStatistic	—	timeContract_eq_smul normalOrder_ofFieldOp_ofFieldOp_swap timeOrder_ofFieldOp_ofFieldOp_not_ordered_eq_timeOrder
timeContract_of_not_timeOrderRel_expand 📖	mathematical	FieldSpecification.timeOrderRel	timeContract FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign FieldSpecification.fieldOpStatistic superCommute anPart ofFieldOp	—	timeContract_of_not_timeOrderRel timeContract_of_timeOrderRel FieldSpecification.instIsTotalFieldOpTimeOrderRel
timeContract_of_timeOrderRel 📖	mathematical	FieldSpecification.timeOrderRel	timeContract FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet superCommute anPart ofFieldOp	—	ofFieldOp_eq_crPart_add_anPart superCommute_anPart_anPart superCommute_anPart_crPart timeOrder_ofFieldOp_ofFieldOp_ordered normalOrder_ofFieldOp_mul_ofFieldOp
timeContract_outAsymp_outAsymp 📖	mathematical	—	timeContract FieldSpecification.FieldOp.outAsymp FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet	—	timeContract_eq_superCommute anPart_outAsymp_eq_ofFieldOp superCommute_anPart_anPart
timeContract_zero_of_diff_grade 📖	mathematical	—	timeContract FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet	—	timeContract_of_timeOrderRel superCommute_anPart_ofFieldOpF_diff_grade_zero timeContract_of_not_timeOrderRel FieldSpecification.instIsTotalFieldOpTimeOrderRel
timeOrder_timeContract_eq_time_left 📖	mathematical	FieldSpecification.timeOrderRel	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet timeOrder timeContract	—	timeOrder_timeContract_eq_time_mid
timeOrder_timeContract_eq_time_mid 📖	mathematical	FieldSpecification.timeOrderRel	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet timeOrder timeContract	—	timeContract_of_timeOrderRel ofFieldOp_eq_sum anPart_inAsymp anPart_position timeOrder_superCommute_eq_time_mid anPart_outAsymp
timeOrder_timeContract_neq_time 📖	mathematical	FieldSpecification.timeOrderRel	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet timeOrder timeContract	—	timeContract_of_timeOrderRel ofFieldOp_eq_sum anPart_inAsymp anPart_position timeOrder_superCommute_neq_time anPart_outAsymp timeContract_of_not_timeOrderRel_expand

---

← Back to Index