InsertAndContract

📁 Source: PhysLean/QFT/PerturbationTheory/WickContraction/InsertAndContract.lean

Statistics

Metric	Count
Definitions insertAndContract, insertAndContractLiftFinset, «term_↩Λ___»	3
Theorems insertAndContract_fstFieldOfContract, insertAndContract_fstFieldOfContract_some_incl, insertAndContract_isSome_getDual?_self, insertAndContract_none_getDual?_get_eq, insertAndContract_none_getDual?_self, insertAndContract_none_prod_contractions, insertAndContract_none_succAbove_getDual?_eq_none_iff, insertAndContract_none_succAbove_getDual?_isSome_iff, insertAndContract_sndFieldOfContract, insertAndContract_sndFieldOfContract_some_incl, insertAndContract_some_getDual?_self_eq, insertAndContract_some_getDual?_self_not_none, insertAndContract_some_getDual?_some_eq, insertAndContract_some_prod_contractions, insertAndContract_some_succAbove_getDual?_eq_option, insertAndContract_uncontractedList_none_map, insertAndContract_uncontractedList_none_zero, insertLift_sum, insert_fin_eq_self, self_not_mem_insertAndContractLiftFinset, stat_ofFinset_of_insertAndContractLiftFinset, succAbove_mem_insertAndContractLiftFinset	22
Total	25

WickContraction

Definitions

Name	Category	Theorems
insertAndContract 📖	CompOp	44 math math: wickTerm_insert_some, sign_insert_none_eq_signInsertNone_mul_sign, staticContract_insert_some_of_lt, insertAndContract_uncontractedList_none_zero, sign_insert_none_zero, staticWickTerm_insert_zero_some, insertAndContract_fstFieldOfContract, insertAndContract_some_getDual?_self_eq, insertAndContract_none_succAbove_getDual?_eq_none_iff, insertAndContract_some_getDual?_self_not_none, wickTerm_insert_none, insertAndContract_none_succAbove_getDual?_isSome_iff, sign_insert_some_of_not_lt, timeContract_insert_none, insertAndContract_sndFieldOfContract, insertAndContract_none_getDual?_self, timeContract_insert_some_of_not_lt, insertAndContract_some_succAbove_getDual?_eq_option, signInsertSomeCoef_if, sign_insert_some_zero, timeContract_insert_some_of_lt, insertAndContract_sndFieldOfContract_some_incl, staticContract_insert_some, insertAndContract_isSome_getDual?_self, mul_staticWickTerm_eq_sum, mul_wickTerm_eq_sum, insertAndContract_uncontractedList_none_map, FieldSpecification.WickAlgebra.normalOrder_uncontracted_none, signFinset_insertAndContract_some, stat_signFinset_insert_some_self_fst, insertLift_sum, staticContract_insert_none, insertAndContract_some_prod_contractions, FieldSpecification.WickAlgebra.normalOrder_uncontracted_some, sign_insert_some, insertAndContract_some_getDual?_some_eq, timeContract_insertAndContract_some, staticWickTerm_insert_zero_none, stat_signFinset_insert_some_self_snd, insertAndContract_none_prod_contractions, insertAndContract_fstFieldOfContract_some_incl, sign_insert_some_of_lt, sign_insert_none, signFinset_insertAndContract_none
insertAndContractLiftFinset 📖	CompOp	5 math math: self_not_mem_insertAndContractLiftFinset, stat_ofFinset_of_insertAndContractLiftFinset, succAbove_mem_insertAndContractLiftFinset, signFinset_insertAndContract_some, signFinset_insertAndContract_none
«term_↩Λ___» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
insertAndContract_fstFieldOfContract 📖	mathematical	—	fstFieldOfContract FieldSpecification.FieldOp insertAndContract congrLift PhysLean.List.insertIdx_length_fin insertAndContractNat insertLift	—	PhysLean.List.insertIdx_length_fin fstFieldOfContract_congr insertAndContractNat_fstFieldOfContract
insertAndContract_fstFieldOfContract_some_incl 📖	mathematical	—	fstFieldOfContract FieldSpecification.FieldOp insertAndContract uncontracted congrLift PhysLean.List.insertIdx_length_fin insertAndContractNat	—	PhysLean.List.insertIdx_length_fin eq_fstFieldOfContract_of_mem
insertAndContract_isSome_getDual?_self 📖	mathematical	—	FieldSpecification.FieldOp getDual? insertAndContract uncontracted PhysLean.List.insertIdx_length_fin	—	PhysLean.List.insertIdx_length_fin getDual?_congr insertAndContractNat_some_getDual?_eq
insertAndContract_none_getDual?_get_eq 📖	—	FieldSpecification.FieldOp getDual? insertAndContract uncontracted PhysLean.List.insertIdx_length_fin	—	—	PhysLean.List.insertIdx_length_fin getDual?_congr getDual?_congr_get insertAndContractNat_succAbove_getDual?_get
insertAndContract_none_getDual?_self 📖	mathematical	—	getDual? FieldSpecification.FieldOp insertAndContract uncontracted PhysLean.List.insertIdx_length_fin	—	PhysLean.List.insertIdx_length_fin getDual?_congr insertAndContractNat_none_getDual?_eq_none
insertAndContract_none_prod_contractions 📖	mathematical	—	FieldSpecification.FieldOp insertAndContract uncontracted congrLift PhysLean.List.insertIdx_length_fin insertAndContractNat insertLift	—	insertLift_none_bijective PhysLean.List.insertIdx_length_fin congrLift_bijective
insertAndContract_none_succAbove_getDual?_eq_none_iff 📖	mathematical	—	getDual? FieldSpecification.FieldOp insertAndContract uncontracted PhysLean.List.insertIdx_length_fin	—	PhysLean.List.insertIdx_length_fin getDual?_congr
insertAndContract_none_succAbove_getDual?_isSome_iff 📖	mathematical	—	FieldSpecification.FieldOp getDual? insertAndContract uncontracted PhysLean.List.insertIdx_length_fin	—	PhysLean.List.insertIdx_length_fin
insertAndContract_sndFieldOfContract 📖	mathematical	—	sndFieldOfContract FieldSpecification.FieldOp insertAndContract congrLift PhysLean.List.insertIdx_length_fin insertAndContractNat insertLift	—	PhysLean.List.insertIdx_length_fin sndFieldOfContract_congr insertAndContractNat_sndFieldOfContract
insertAndContract_sndFieldOfContract_some_incl 📖	mathematical	—	sndFieldOfContract FieldSpecification.FieldOp insertAndContract uncontracted congrLift PhysLean.List.insertIdx_length_fin insertAndContractNat	—	PhysLean.List.insertIdx_length_fin eq_sndFieldOfContract_of_mem
insertAndContract_some_getDual?_self_eq 📖	mathematical	—	getDual? FieldSpecification.FieldOp insertAndContract uncontracted PhysLean.List.insertIdx_length_fin	—	PhysLean.List.insertIdx_length_fin getDual?_congr insertAndContractNat_some_getDual?_eq
insertAndContract_some_getDual?_self_not_none 📖	mathematical	—	getDual? FieldSpecification.FieldOp insertAndContract uncontracted PhysLean.List.insertIdx_length_fin	—	PhysLean.List.insertIdx_length_fin getDual?_congr insertAndContractNat_some_getDual?_eq
insertAndContract_some_getDual?_some_eq 📖	mathematical	—	getDual? FieldSpecification.FieldOp insertAndContract uncontracted PhysLean.List.insertIdx_length_fin	—	PhysLean.List.insertIdx_length_fin getDual?_eq_some_iff_mem insertAndContract_some_getDual?_self_eq
insertAndContract_some_prod_contractions 📖	mathematical	—	FieldSpecification.FieldOp insertAndContract uncontracted congrLift PhysLean.List.insertIdx_length_fin insertAndContractNat insertLift	—	PhysLean.List.insertIdx_length_fin congrLift_bijective insertLiftSome_bijective
insertAndContract_some_succAbove_getDual?_eq_option 📖	mathematical	—	getDual? FieldSpecification.FieldOp insertAndContract uncontracted PhysLean.List.insertIdx_length_fin	—	PhysLean.List.insertIdx_length_fin getDual?_congr insertAndContractNat_some_getDual?_of_neq
insertAndContract_uncontractedList_none_map 📖	mathematical	—	uncontractedListGet FieldSpecification.FieldOp insertAndContract uncontracted uncontractedListOrderPos	—	congr_uncontractedList uncontractedList_extractEquiv_symm_none orderedInsert_succAboveEmb_uncontractedList_eq_insertIdx PhysLean.List.insertIdx_map PhysLean.List.insertIdx_length_fin PhysLean.List.insertIdx_getElem_fin
insertAndContract_uncontractedList_none_zero 📖	mathematical	—	uncontractedListGet FieldSpecification.FieldOp insertAndContract uncontracted	—	insertAndContract_uncontractedList_none_map
insertLift_sum 📖	mathematical	—	WickContraction FieldSpecification.FieldOp fintype_succ uncontracted insertAndContract	—	PhysLean.List.insertIdx_length_fin sum_extractEquiv_congr
insert_fin_eq_self 📖	mathematical	—	FieldSpecification.FieldOp PhysLean.List.insertIdx_length_fin	—	PhysLean.List.insertIdx_length_fin
self_not_mem_insertAndContractLiftFinset 📖	mathematical	—	FieldSpecification.FieldOp insertAndContractLiftFinset PhysLean.List.insertIdx_length_fin	—	PhysLean.List.insertIdx_length_fin
stat_ofFinset_of_insertAndContractLiftFinset 📖	mathematical	—	FieldStatistic.ofFinset FieldSpecification.FieldOp FieldSpecification.fieldOpStatistic insertAndContractLiftFinset	—	PhysLean.List.insertIdx_length_fin PhysLean.List.get_eq_insertIdx_succAbove fin_list_sorted_monotone_sorted insert_fin_eq_self succAbove_mem_insertAndContractLiftFinset
succAbove_mem_insertAndContractLiftFinset 📖	mathematical	—	FieldSpecification.FieldOp insertAndContractLiftFinset PhysLean.List.insertIdx_length_fin	—	PhysLean.List.insertIdx_length_fin

---

← Back to Index