Documentation Verification Report

WickTerm

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

Statistics

MetricCount
DefinitionswickTerm
1
Theoremsmul_wickTerm_eq_sum, wickTerm_empty_nil, wickTerm_insert_none, wickTerm_insert_some
4
Total5

WickContraction

Definitions

NameCategoryTheorems
wickTerm 📖CompOp
10 mathmath: wickTerm_insert_some, FieldSpecification.wicks_theorem_congr, FieldSpecification.WickAlgebra.wicks_theorem_normal_order_empty, wickTerm_insert_none, FieldSpecification.WickAlgebra.wicks_theorem_normal_order, wickTerm_empty_nil, mul_wickTerm_eq_sum, FieldSpecification.WickAlgebra.normalOrder_timeOrder_ofFieldOpList_eq_not_haveEqTime_sub_inductive, FieldSpecification.wicks_theorem, FieldSpecification.WickAlgebra.timeOrder_haveEqTime_split

Theorems

NameKindAssumesProvesValidatesDepends On
mul_wickTerm_eq_sum 📖mathematicalFieldSpecification.timeOrderRel
FieldSpecification.FieldOp
FieldSpecification.WickAlgebra
FieldSpecification.FieldOpFreeAlgebra
FieldSpecification.CrAnFieldOp
FieldSpecification.fieldOpIdealSet
FieldSpecification.WickAlgebra.ofFieldOp
wickTerm
FieldStatistic
FieldStatistic.instCommGroup
FieldStatistic.exchangeSign
FieldSpecification.fieldOpStatistic
FieldStatistic.ofFinset
uncontracted
insertAndContract
wickTerm.eq_1
FieldSpecification.WickAlgebra.ofFieldOp_mul_normalOrder_ofFieldOpList_eq_sum
uncontractedFieldOpEquiv_list_sum
wickTerm_insert_none
FieldStatistic.exchangeSign_mul_self
wickTerm_insert_some
wickTerm_empty_nil 📖mathematicalwickTerm
FieldSpecification.FieldOp
empty
FieldSpecification.WickAlgebra
FieldSpecification.FieldOpFreeAlgebra
FieldSpecification.CrAnFieldOp
FieldSpecification.fieldOpIdealSet
wickTerm.eq_1
sign_empty
timeContract_empty
uncontractedListGet_empty
FieldSpecification.WickAlgebra.normalOrder_ofFieldOpList_nil
wickTerm_insert_none 📖mathematicalwickTerm
FieldSpecification.FieldOp
insertAndContract
uncontracted
FieldSpecification.WickAlgebra
FieldSpecification.FieldOpFreeAlgebra
FieldSpecification.CrAnFieldOp
FieldSpecification.fieldOpIdealSet
FieldStatistic
FieldStatistic.instCommGroup
FieldStatistic.exchangeSign
FieldSpecification.fieldOpStatistic
FieldStatistic.ofFinset
sign
timeContract
FieldSpecification.WickAlgebra.normalOrder
FieldSpecification.WickAlgebra.ofFieldOpList
uncontractedListGet
wickTerm.eq_1
FieldSpecification.WickAlgebra.normalOrder_uncontracted_none
sign_insert_none
timeContract_insert_none
FieldStatistic.ofFinset_union
timeContract_of_not_gradingCompliant
wickTerm_insert_some 📖mathematicalFieldSpecification.timeOrderRel
FieldSpecification.FieldOp
wickTerm
insertAndContract
uncontracted
FieldSpecification.WickAlgebra
FieldSpecification.FieldOpFreeAlgebra
FieldSpecification.CrAnFieldOp
FieldSpecification.fieldOpIdealSet
FieldStatistic
FieldStatistic.instCommGroup
FieldStatistic.exchangeSign
FieldSpecification.fieldOpStatistic
FieldStatistic.ofFinset
sign
FieldSpecification.WickAlgebra.contractStateAtIndex
uncontractedListGet
uncontractedFieldOpEquiv
timeContract
FieldSpecification.WickAlgebra.normalOrder
FieldSpecification.WickAlgebra.ofFieldOpList
PhysLean.List.optionEraseZ
wickTerm.eq_1
timeContract_insert_some_of_not_lt
FieldSpecification.WickAlgebra.normalOrder_uncontracted_some
sign_insert_some_of_lt
FieldStatistic.exchangeSign_mul_self
timeContract_insert_some_of_lt
sign_insert_some_of_not_lt
FieldSpecification.WickAlgebra.timeContract_mem_center
timeContract_insertAndContract_some
uncontractedList_getElem_uncontractedIndexEquiv_symm
FieldSpecification.WickAlgebra.timeContract_zero_of_diff_grade
FieldSpecification.WickAlgebra.superCommute_anPart_ofFieldOpF_diff_grade_zero
timeContract_of_not_gradingCompliant

---

← Back to Index