WicksTheoremNormal

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

Statistics

Metric	Count
Definitions	0
Theorems normalOrder_timeOrder_ofFieldOpList_eq_eqTimeOnly_empty, normalOrder_timeOrder_ofFieldOpList_eq_not_haveEqTime_sub_inductive, timeOrder_haveEqTime_split, timeOrder_ofFieldOpList_eqTimeOnly, timeOrder_ofFieldOpList_eq_eqTimeOnly_empty, wicks_theorem_normal_order, wicks_theorem_normal_order_empty	7
Total	7

FieldSpecification.WickAlgebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
normalOrder_timeOrder_ofFieldOpList_eq_eqTimeOnly_empty 📖	mathematical	—	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet timeOrder normalOrder ofFieldOpList WickContraction FieldSpecification.FieldOp WickContraction.EqTimeOnly WickContraction.empty WickContraction.instDecidableEqTimeOnly WickContraction.instDecidableEq WickContraction.fintype_succ WickContraction.sign WickContraction.timeContract WickContraction.uncontractedListGet	—	timeOrder_ofFieldOpList_eq_eqTimeOnly_empty
normalOrder_timeOrder_ofFieldOpList_eq_not_haveEqTime_sub_inductive 📖	mathematical	—	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet timeOrder normalOrder ofFieldOpList WickContraction FieldSpecification.FieldOp WickContraction.HaveEqTime WickContraction.instDecidableHaveEqTime WickContraction.fintype_succ WickContraction.wickTerm WickContraction.EqTimeOnly WickContraction.empty WickContraction.instDecidableEqTimeOnly WickContraction.instDecidableEq WickContraction.sign WickContraction.timeContract WickContraction.uncontractedListGet	—	normalOrder_timeOrder_ofFieldOpList_eq_eqTimeOnly_empty timeOrder_haveEqTime_split
timeOrder_haveEqTime_split 📖	mathematical	—	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet timeOrder ofFieldOpList WickContraction FieldSpecification.FieldOp WickContraction.HaveEqTime WickContraction.instDecidableHaveEqTime WickContraction.fintype_succ WickContraction.sign WickContraction.timeContract normalOrder WickContraction.uncontractedListGet WickContraction.EqTimeOnly WickContraction.empty WickContraction.instDecidableEqTimeOnly WickContraction.instDecidableEq WickContraction.wickTerm	—	FieldSpecification.wicks_theorem WickContraction.sum_haveEqTime WickContraction.join_sign_timeContract WickContraction.join_uncontractedListGet
timeOrder_ofFieldOpList_eqTimeOnly 📖	mathematical	—	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet timeOrder ofFieldOpList WickContraction FieldSpecification.FieldOp WickContraction.EqTimeOnly WickContraction.instDecidableEqTimeOnly WickContraction.fintype_succ WickContraction.sign WickContraction.timeContract normalOrder WickContraction.uncontractedListGet	—	static_wick_theorem timeOrder_timeOrder_left WickContraction.EqTimeOnly.timeOrder_staticContract_of_not_mem WickContraction.EqTimeOnly.staticContract_eq_timeContract_of_eqTimeOnly WickContraction.EqTimeOnly.timeOrder_timeContract_mul_of_eqTimeOnly_left
timeOrder_ofFieldOpList_eq_eqTimeOnly_empty 📖	mathematical	—	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet timeOrder ofFieldOpList normalOrder WickContraction FieldSpecification.FieldOp WickContraction.EqTimeOnly WickContraction.empty WickContraction.instDecidableEqTimeOnly WickContraction.instDecidableEq WickContraction.fintype_succ WickContraction.sign WickContraction.timeContract WickContraction.uncontractedListGet	—	timeOrder_ofFieldOpList_eqTimeOnly WickContraction.sign_empty WickContraction.timeContract_empty WickContraction.uncontractedListGet_empty
wicks_theorem_normal_order 📖	mathematical	—	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet timeOrder normalOrder ofFieldOpList WickContraction FieldSpecification.FieldOp WickContraction.HaveEqTime WickContraction.instDecidableHaveEqTime WickContraction.fintype_succ WickContraction.wickTerm	—	wicks_theorem_normal_order_empty normalOrder_timeOrder_ofFieldOpList_eq_not_haveEqTime_sub_inductive WickContraction.uncontractedList_length_eq_card WickContraction.uncontracted_card_eq_iff WickContraction.uncontracted_card_le
wicks_theorem_normal_order_empty 📖	mathematical	—	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet timeOrder normalOrder ofFieldOpList FieldSpecification.FieldOp WickContraction WickContraction.HaveEqTime WickContraction.instDecidableHaveEqTime WickContraction.fintype_succ WickContraction.wickTerm	—	WickContraction.sign_empty WickContraction.timeContract_empty WickContraction.uncontractedListGet_empty normalOrder_ofCrAnList FieldSpecification.normalOrderList_nil ofCrAnList.eq_1 timeOrder_eq_ι_timeOrderF FieldSpecification.FieldOpFreeAlgebra.timeOrderF_ofCrAnListF FieldSpecification.crAnTimeOrderSign_nil FieldSpecification.crAnTimeOrderList_nil

---

← Back to Index