UncontractedList

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

Statistics

Metric	Count
Definitions `uncontractedFieldOpEquiv`, `uncontractedIndexEquiv`, `uncontractedList`, `uncontractedListEmd`, `uncontractedListGet`, `uncontractedListOrderPos`, `«term[_]ᵘᶜ»`	7
Theorems `congr_uncontractedList`, `filter_uncontractedList`, `fin_finset_sort_map_monotone`, `fin_list_sorted_indexOf_filter_le_mem`, `fin_list_sorted_indexOf_mem`, `fin_list_sorted_monotone_sorted`, `fin_list_sorted_split`, `fin_list_sorted_succAboveEmb_sorted`, `getElem_uncontractedListEmd`, `nil_zero_uncontractedList`, `orderedInsert_eq_insertIdx_of_fin_list_sorted`, `orderedInsert_of_fin_list_sorted`, `orderedInsert_succAboveEmb_uncontractedList_eq_insertIdx`, `take_uncontractedIndexEquiv_symm`, `take_uncontractedListOrderPos_eq_filter`, `take_uncontractedListOrderPos_eq_filter_sort`, `uncontractedFieldOpEquiv_list_sum`, `uncontractedFieldOpEquiv_none`, `uncontractedIndexEquiv_symm_eq_filter_length`, `uncontractedListEmd_congr`, `uncontractedListEmd_empty`, `uncontractedListEmd_finset_disjoint_left`, `uncontractedListEmd_finset_not_mem`, `uncontractedListEmd_mem_uncontracted`, `uncontractedListEmd_strictMono`, `uncontractedListEmd_surjective_mem_uncontracted`, `uncontractedListEmd_toFun_eq_get`, `uncontractedListGet_empty`, `uncontractedListOrderPos_lt_length_add_one`, `uncontractedList_empty`, `uncontractedList_eq_sort`, `uncontractedList_extractEquiv_symm_none`, `uncontractedList_extractEquiv_symm_some`, `uncontractedList_getElem_uncontractedIndexEquiv_symm`, `uncontractedList_get_mem_uncontracted`, `uncontractedList_length_eq_card`, `uncontractedList_mem_iff`, `uncontractedList_nodup`, `uncontractedList_sorted`, `uncontractedList_sorted_lt`, `uncontractedList_succAboveEmb_eraseIdx_eq_sort`, `uncontractedList_succAboveEmb_eraseIdx_nodup`, `uncontractedList_succAboveEmb_eraseIdx_sorted`, `uncontractedList_succAboveEmb_eraseIdx_toFinset`, `uncontractedList_succAboveEmb_nodup`, `uncontractedList_succAboveEmb_sorted`, `uncontractedList_succAboveEmb_toFinset`, `uncontractedList_succAbove_orderedInsert_eq_sort`, `uncontractedList_succAbove_orderedInsert_nodup`, `uncontractedList_succAbove_orderedInsert_sorted`, `uncontractedList_succAbove_orderedInsert_toFinset`, `uncontractedList_toFinset`	52
Total	59

WickContraction

Definitions

Name	Category	Theorems
`uncontractedFieldOpEquiv` 📖	CompOp	8 math math: `wickTerm_insert_some`, `staticContract_insert_some_of_lt`, `staticWickTerm_insert_zero_some`, `timeContract_insert_some_of_not_lt`, `timeContract_insert_some_of_lt`, `uncontractedFieldOpEquiv_list_sum`, `FieldSpecification.WickAlgebra.normalOrder_uncontracted_some`, `uncontractedFieldOpEquiv_none`
`uncontractedIndexEquiv` 📖	CompOp	4 math math: `uncontractedList_extractEquiv_symm_some`, `take_uncontractedIndexEquiv_symm`, `uncontractedList_getElem_uncontractedIndexEquiv_symm`, `uncontractedIndexEquiv_symm_eq_filter_length`
`uncontractedList` 📖	CompOp	33 math math: `uncontractedList_nodup`, `uncontractedList_extractEquiv_symm_none`, `uncontractedList_extractEquiv_symm_some`, `congr_uncontractedList`, `uncontractedList_succAboveEmb_eraseIdx_nodup`, `uncontractedList_sorted_lt`, `uncontractedList_get_mem_uncontracted`, `uncontractedList_succAbove_orderedInsert_toFinset`, `uncontractedList_length_eq_card`, `uncontractedListEmd_toFun_eq_get`, `uncontractedList_mem_iff`, `nil_zero_uncontractedList`, `take_uncontractedIndexEquiv_symm`, `uncontractedList_toFinset`, `uncontractedList_empty`, `uncontractedList_eq_sort`, `uncontractedList_succAboveEmb_nodup`, `orderedInsert_succAboveEmb_uncontractedList_eq_insertIdx`, `uncontractedList_succAbove_orderedInsert_eq_sort`, `uncontractedList_getElem_uncontractedIndexEquiv_symm`, `uncontractedList_succAbove_orderedInsert_nodup`, `take_uncontractedListOrderPos_eq_filter`, `join_uncontractedList_get`, `filter_uncontractedList`, `uncontractedList_succAbove_orderedInsert_sorted`, `uncontractedListOrderPos_lt_length_add_one`, `uncontractedList_succAboveEmb_toFinset`, `uncontractedList_sorted`, `uncontractedList_succAboveEmb_sorted`, `uncontractedList_succAboveEmb_eraseIdx_sorted`, `join_uncontractedList`, `take_uncontractedListOrderPos_eq_filter_sort`, `uncontractedIndexEquiv_symm_eq_filter_length`
`uncontractedListEmd` 📖	CompOp	32 math math: `mem_quotContraction_iff`, `join_getDual?_apply_uncontractedListEmb_eq_none_iff`, `signFinset_right_map_uncontractedListEmd_eq_filter`, `sign_right_eq_prod_mul_prod`, `join_fstFieldOfContract_joinLiftRight`, `join_singleton_sign_right`, `uncontractedListEmd_surjective_mem_uncontracted`, `mem_of_mem_quotContraction`, `stat_signFinset_right`, `mem_join_right_iff`, `uncontractedListEmd_finset_not_mem`, `getElem_uncontractedListEmd`, `uncontractedListEmd_toFun_eq_get`, `uncontractedListEmd_empty`, `join_eqTimeContractSet`, `join_uncontractedListEmb`, `joinSignRightExtra_eq_i_j_finset_eq_if`, `exists_mem_right_uncontracted_of_mem_join_uncontracted`, `join_getDual?_apply_uncontractedListEmb_isSome_iff`, `join_getDual?_apply_uncontractedListEmb`, `mem_subContraction_or_quotContraction`, `quotContraction_sndFieldOfContract_uncontractedListEmd`, `uncontractedListEmd_strictMono`, `uncontractedListEmd_mem_uncontracted`, `uncontractedListEmd_finset_disjoint_left`, `join_uncontractedList_get`, `quotContraction_fstFieldOfContract_uncontractedListEmd`, `join_sndFieldOfContract_joinLiftRight`, `join_uncontractedList`, `mem_join_uncontracted_of_mem_right_uncontracted`, `subContraction_uncontractedList_get`, `uncontractedListEmd_congr`
`uncontractedListGet` 📖	CompOp	73 math math: `wickTerm_insert_some`, `mem_quotContraction_iff`, `staticContract_insert_some_of_lt`, `join_getDual?_apply_uncontractedListEmb_eq_none_iff`, `insertAndContract_uncontractedList_none_zero`, `signFinset_right_map_uncontractedListEmd_eq_filter`, `staticWickTerm_insert_zero_some`, `EqTimeOnly.exists_join_singleton_of_card_ge_zero`, `sign_right_eq_prod_mul_prod`, `join_fstFieldOfContract_joinLiftRight`, `join_singleton_sign_right`, `join_sign_timeContract`, `join_card`, `uncontractedListEmd_surjective_mem_uncontracted`, `joinLift_injective`, `wickTerm_insert_none`, `stat_signFinset_right`, `mem_join_right_iff`, `quotContraction_gradingCompliant`, `uncontractedListEmd_finset_not_mem`, `joinLift_surjective`, `join_empty`, `getElem_uncontractedListEmd`, `uncontractedListEmd_toFun_eq_get`, `join_assoc`, `timeContract_insert_some_of_not_lt`, `join_timeContract`, `join_staticContract`, `uncontractedListEmd_empty`, `join_eqTimeContractSet`, `join_uncontractedListEmb`, `timeContract_insert_some_of_lt`, `join_sign`, `joinSignRightExtra_eq_i_j_finset_eq_if`, `uncontractedListGet_empty`, `exists_mem_right_uncontracted_of_mem_join_uncontracted`, `uncontractedFieldOpEquiv_list_sum`, `join_getDual?_apply_uncontractedListEmb_isSome_iff`, `join_getDual?_apply_uncontractedListEmb`, `FieldSpecification.WickAlgebra.normalOrder_timeOrder_ofFieldOpList_eq_eqTimeOnly_empty`, `mem_subContraction_or_quotContraction`, `quotContraction_sndFieldOfContract_uncontractedListEmd`, `insertAndContract_uncontractedList_none_map`, `FieldSpecification.WickAlgebra.normalOrder_uncontracted_none`, `uncontractedListEmd_mem_uncontracted`, `sum_haveEqTime`, `exists_join_singleton_of_card_ge_zero`, `uncontractedListEmd_finset_disjoint_left`, `Perm.perm_uncontractedList`, `join_sign_induction`, `join_uncontractedList_get`, `FieldSpecification.WickAlgebra.normalOrder_uncontracted_some`, `subContraction_card_plus_quotContraction_card_eq`, `FieldSpecification.WickAlgebra.normalOrder_timeOrder_ofFieldOpList_eq_not_haveEqTime_sub_inductive`, `join_congr`, `FieldSpecification.WickAlgebra.timeOrder_ofFieldOpList_eq_eqTimeOnly_empty`, `quotContraction_eqTimeContractSet_not_haveEqTime`, `EqTimeOnly.quotContraction_eqTimeOnly`, `staticWickTerm_insert_zero_none`, `prod_join`, `joinLift_bijective`, `quotContraction_fstFieldOfContract_uncontractedListEmd`, `join_sndFieldOfContract_joinLiftRight`, `join_uncontractedList`, `join_uncontractedListGet`, `FieldSpecification.WickAlgebra.timeOrder_haveEqTime_split`, `joinLiftRight_injective`, `empty_join`, `FieldSpecification.WickAlgebra.timeOrder_ofFieldOpList_eqTimeOnly`, `join_sign_singleton`, `uncontractedFieldOpEquiv_none`, `subContraction_uncontractedList_get`, `uncontractedListEmd_congr`
`uncontractedListOrderPos` 📖	CompOp	5 math math: `insertAndContract_uncontractedList_none_map`, `orderedInsert_succAboveEmb_uncontractedList_eq_insertIdx`, `take_uncontractedListOrderPos_eq_filter`, `uncontractedListOrderPos_lt_length_add_one`, `take_uncontractedListOrderPos_eq_filter_sort`
`«term[_]ᵘᶜ»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`congr_uncontractedList` 📖	mathematical	—	`uncontractedList` `WickContraction` `congr`	—	—
`filter_uncontractedList` 📖	mathematical	—	`uncontractedList` `uncontracted`	—	`uncontractedList_sorted` `uncontractedList_nodup` `uncontractedList_mem_iff`
`fin_finset_sort_map_monotone` 📖	—	—	—	—	`fin_list_sorted_monotone_sorted`
`fin_list_sorted_indexOf_filter_le_mem` 📖	—	—	—	—	—
`fin_list_sorted_indexOf_mem` 📖	—	—	—	—	`fin_list_sorted_split` `fin_list_sorted_indexOf_filter_le_mem`
`fin_list_sorted_monotone_sorted` 📖	—	—	—	—	—
`fin_list_sorted_split` 📖	—	—	—	—	—
`fin_list_sorted_succAboveEmb_sorted` 📖	—	—	—	—	`fin_list_sorted_monotone_sorted`
`getElem_uncontractedListEmd` 📖	mathematical	—	`FieldSpecification.FieldOp` `uncontractedListGet` `uncontractedListEmd`	—	—
`nil_zero_uncontractedList` 📖	mathematical	—	`uncontractedList` `empty`	—	—
`orderedInsert_eq_insertIdx_of_fin_list_sorted` 📖	—	—	—	—	`PhysLean.List.insertIdx_eq_take_drop` `orderedInsert_of_fin_list_sorted` `fin_list_sorted_split`
`orderedInsert_of_fin_list_sorted` 📖	—	—	—	—	`fin_list_sorted_split`
`orderedInsert_succAboveEmb_uncontractedList_eq_insertIdx` 📖	mathematical	—	`uncontractedList` `uncontractedListOrderPos`	—	`orderedInsert_eq_insertIdx_of_fin_list_sorted` `uncontractedList_succAboveEmb_sorted`
`take_uncontractedIndexEquiv_symm` 📖	mathematical	—	`uncontractedList` `uncontracted` `uncontractedIndexEquiv`	—	`fin_list_sorted_split` `uncontractedList_sorted` `uncontractedIndexEquiv_symm_eq_filter_length`
`take_uncontractedListOrderPos_eq_filter` 📖	mathematical	—	`uncontractedListOrderPos` `uncontractedList`	—	`fin_list_sorted_split` `uncontractedList_sorted`
`take_uncontractedListOrderPos_eq_filter_sort` 📖	mathematical	—	`uncontractedListOrderPos` `uncontractedList` `uncontracted`	—	`take_uncontractedListOrderPos_eq_filter` `uncontractedList_sorted` `uncontractedList_nodup` `uncontractedList_eq_sort`
`uncontractedFieldOpEquiv_list_sum` 📖	mathematical	—	`FieldSpecification.FieldOp` `uncontractedListGet` `uncontracted` `uncontractedFieldOpEquiv`	—	—
`uncontractedFieldOpEquiv_none` 📖	mathematical	—	`FieldSpecification.FieldOp` `uncontracted` `uncontractedListGet` `uncontractedFieldOpEquiv`	—	—
`uncontractedIndexEquiv_symm_eq_filter_length` 📖	mathematical	—	`uncontractedList` `uncontracted` `uncontractedIndexEquiv`	—	`fin_list_sorted_indexOf_mem` `uncontractedList_sorted` `uncontractedList_mem_iff`
`uncontractedListEmd_congr` 📖	mathematical	—	`uncontractedListEmd` `FieldSpecification.FieldOp` `uncontractedListGet` `WickContraction`	—	—
`uncontractedListEmd_empty` 📖	mathematical	—	`uncontractedListEmd` `empty` `FieldSpecification.FieldOp` `uncontractedListGet` `uncontractedListGet_empty`	—	`uncontractedListGet_empty` `uncontractedList_get_mem_uncontracted` `uncontractedList_empty`
`uncontractedListEmd_finset_disjoint_left` 📖	mathematical	`FieldSpecification.FieldOp`	`uncontractedListGet` `uncontractedListEmd`	—	`uncontractedListEmd_mem_uncontracted` `mem_uncontracted_iff_not_contracted`
`uncontractedListEmd_finset_not_mem` 📖	mathematical	—	`FieldSpecification.FieldOp` `uncontractedListGet` `uncontractedListEmd`	—	`uncontractedListEmd_finset_disjoint_left`
`uncontractedListEmd_mem_uncontracted` 📖	mathematical	—	`FieldSpecification.FieldOp` `uncontracted` `uncontractedListGet` `uncontractedListEmd`	—	—
`uncontractedListEmd_strictMono` 📖	mathematical	`FieldSpecification.FieldOp` `uncontractedListGet`	`uncontractedListEmd`	—	`uncontractedList_sorted_lt`
`uncontractedListEmd_surjective_mem_uncontracted` 📖	mathematical	`FieldSpecification.FieldOp` `uncontracted`	`uncontractedListGet` `uncontractedListEmd`	—	—
`uncontractedListEmd_toFun_eq_get` 📖	mathematical	—	`FieldSpecification.FieldOp` `uncontractedListGet` `uncontractedListEmd` `uncontractedList`	—	—
`uncontractedListGet_empty` 📖	mathematical	—	`uncontractedListGet` `empty` `FieldSpecification.FieldOp`	—	`uncontractedList_empty`
`uncontractedListOrderPos_lt_length_add_one` 📖	mathematical	—	`uncontractedListOrderPos` `uncontractedList`	—	—
`uncontractedList_empty` 📖	mathematical	—	`uncontractedList` `empty`	—	`uncontracted_empty`
`uncontractedList_eq_sort` 📖	mathematical	—	`uncontractedList` `uncontracted`	—	`uncontractedList_toFinset` `uncontractedList_nodup` `uncontractedList_sorted`
`uncontractedList_extractEquiv_symm_none` 📖	mathematical	—	`uncontractedList` `WickContraction` `uncontracted` `extractEquiv`	—	`uncontractedList_eq_sort` `extractEquiv_symm_none_uncontracted` `uncontractedList_succAbove_orderedInsert_eq_sort`
`uncontractedList_extractEquiv_symm_some` 📖	mathematical	—	`uncontractedList` `WickContraction` `uncontracted` `extractEquiv` `uncontractedIndexEquiv`	—	`uncontractedList_eq_sort` `uncontractedList_succAboveEmb_eraseIdx_eq_sort` `uncontractedList_getElem_uncontractedIndexEquiv_symm` `insertAndContractNat_some_uncontracted`
`uncontractedList_getElem_uncontractedIndexEquiv_symm` 📖	mathematical	—	`uncontractedList` `uncontracted` `uncontractedIndexEquiv`	—	—
`uncontractedList_get_mem_uncontracted` 📖	mathematical	—	`uncontracted` `uncontractedList`	—	`uncontractedList_mem_iff`
`uncontractedList_length_eq_card` 📖	mathematical	—	`uncontractedList` `uncontracted`	—	`uncontractedList_eq_sort`
`uncontractedList_mem_iff` 📖	mathematical	—	`uncontractedList` `uncontracted`	—	—
`uncontractedList_nodup` 📖	mathematical	—	`uncontractedList`	—	`uncontractedList.eq_1`
`uncontractedList_sorted` 📖	mathematical	—	`uncontractedList`	—	`uncontractedList.eq_1`
`uncontractedList_sorted_lt` 📖	mathematical	—	`uncontractedList`	—	`uncontractedList.eq_1`
`uncontractedList_succAboveEmb_eraseIdx_eq_sort` 📖	mathematical	`uncontractedList`	`uncontracted`	—	`uncontractedList_succAboveEmb_eraseIdx_toFinset` `uncontractedList_succAboveEmb_eraseIdx_nodup` `uncontractedList_succAboveEmb_eraseIdx_sorted`
`uncontractedList_succAboveEmb_eraseIdx_nodup` 📖	mathematical	—	`uncontractedList`	—	`uncontractedList_succAboveEmb_nodup`
`uncontractedList_succAboveEmb_eraseIdx_sorted` 📖	mathematical	—	`uncontractedList`	—	`PhysLean.List.eraseIdx_sorted` `uncontractedList_succAboveEmb_sorted`
`uncontractedList_succAboveEmb_eraseIdx_toFinset` 📖	mathematical	`uncontractedList`	`uncontracted`	—	`PhysLean.List.mem_eraseIdx_nodup` `uncontractedList_succAboveEmb_nodup`
`uncontractedList_succAboveEmb_nodup` 📖	mathematical	—	`uncontractedList`	—	`uncontractedList_nodup`
`uncontractedList_succAboveEmb_sorted` 📖	mathematical	—	`uncontractedList`	—	`fin_list_sorted_succAboveEmb_sorted` `uncontractedList_sorted`
`uncontractedList_succAboveEmb_toFinset` 📖	mathematical	—	`uncontractedList` `uncontracted`	—	`uncontractedList_toFinset`
`uncontractedList_succAbove_orderedInsert_eq_sort` 📖	mathematical	—	`uncontractedList` `uncontracted`	—	`uncontractedList_succAbove_orderedInsert_toFinset` `uncontractedList_succAbove_orderedInsert_nodup` `uncontractedList_succAbove_orderedInsert_sorted`
`uncontractedList_succAbove_orderedInsert_nodup` 📖	mathematical	—	`uncontractedList`	—	`uncontractedList_succAboveEmb_nodup`
`uncontractedList_succAbove_orderedInsert_sorted` 📖	mathematical	—	`uncontractedList`	—	`uncontractedList_succAboveEmb_sorted`
`uncontractedList_succAbove_orderedInsert_toFinset` 📖	mathematical	—	`uncontractedList` `uncontracted`	—	`uncontractedList_toFinset`
`uncontractedList_toFinset` 📖	mathematical	—	`uncontractedList` `uncontracted`	—	—

---

← Back to Index