Documentation Verification Report

ExchangeSign

📁 Source: PhysLean/QFT/PerturbationTheory/FieldStatistics/ExchangeSign.lean

Statistics

Metric	Count
Definitions `exchangeSign`, `«term𝓢(_,_)»`»)	2
Theorems `bosonic_exchangeSign`, `exchangeSign_bosonic`, `exchangeSign_cocycle`, `exchangeSign_eq_if`, `exchangeSign_mul_self`, `exchangeSign_mul_self_swap`, `exchangeSign_ofList_cons`, `exchangeSign_symm`, `fermionic_exchangeSign_fermionic`	9
Total	11

FieldStatistic

Definitions

Name	Category	Theorems
`exchangeSign` 📖	CompOp	146 math math: `FieldSpecification.WickAlgebra.superCommute_ofCrAnOp_ofCrAnOp`, `FieldSpecification.WickAlgebra.timeOrder_ofFieldOp_ofFieldOp_not_ordered_eq_timeOrder`, `WickContraction.wickTerm_insert_some`, `FieldSpecification.WickAlgebra.normalOrder_ofFieldOp_mul_ofFieldOp`, `WickContraction.staticContract_insert_some_of_lt`, `Wick.koszulSign_eraseIdx_insertionSortMinPos`, `FieldSpecification.WickAlgebra.ofFieldOp_mul_ofFieldOpList_eq_superCommute`, `FieldSpecification.FieldOpFreeAlgebra.superCommuteF_anPartF_crPartF`, `FieldSpecification.FieldOpFreeAlgebra.superCommuteF_crPartF_crPartF`, `FieldSpecification.FieldOpFreeAlgebra.timeOrderF_eq_maxTimeField_mul`, `FieldSpecification.FieldOpFreeAlgebra.ofCrAnListF_mul_ofFieldOpListF_eq_superCommuteF`, `WickContraction.sign_right_eq_prod_mul_prod`, `WickContraction.join_singleton_sign_right`, `Wick.koszulSignInsert_eq_exchangeSign_take`, `FieldSpecification.FieldOpFreeAlgebra.timeOrderF_eq_maxTimeField_mul_finset`, `WickContraction.signInsertSomeProd_eq_prod_fin`, `FieldSpecification.FieldOpFreeAlgebra.ofCrAnOpF_mul_normalOrderF_ofFieldOpListF_eq_superCommuteF`, `FieldSpecification.WickAlgebra.ofFieldOpList_normalOrder_insert`, `FieldSpecification.WickAlgebra.anPart_mul_normalOrder_ofFieldOpList_eq_superCommute`, `FieldSpecification.FieldOpFreeAlgebra.normalOrderF_swap_crPartF_anPartF`, `FieldSpecification.normalOrderSign_swap_create_annihilate_fst`, `WickContraction.wickTerm_insert_none`, `WickContraction.signInsertSomeCoef_eq_finset`, `FieldSpecification.WickAlgebra.superCommute_ofCrAnOp_ofCrAnOp_symm`, `FieldSpecification.WickAlgebra.superCommute_ofCrAnList_ofCrAnList`, `FieldSpecification.FieldOpFreeAlgebra.timeOrderF_ofFieldOpF_ofFieldOpF_not_ordered`, `FieldSpecification.FieldOpFreeAlgebra.superCommuteF_crPartF_anPartF`, `FieldSpecification.WickAlgebra.ofCrAnOp_superCommute_normalOrder_ofCrAnList_sum`, `WickContraction.signInsertSome_mul_filter_contracted_of_lt`, `FieldSpecification.FieldOpFreeAlgebra.normalOrderF_swap_create_annihilate_ofCrAnListF`, `FieldSpecification.FieldOpFreeAlgebra.superCommuteF_ofCrAnListF_ofCrAnListF`, `FieldSpecification.FieldOpFreeAlgebra.superCommuteF_ofCrAnListF_ofCrAnListF_eq_sum`, `WickContraction.signInsertSomeProd_eq_finset`, `WickContraction.sign_insert_some_of_not_lt`, `FieldSpecification.FieldOpFreeAlgebra.superCommuteF_ofCrAnListF_ofFieldOpListF_cons`, `FieldSpecification.FieldOpFreeAlgebra.superCommuteF_ofFieldOpF_ofFieldOpFsList`, `WickContraction.signInsertNone_eq_filter_map`, `FieldSpecification.WickAlgebra.anPart_superCommute_normalOrder_ofFieldOpList_sum`, `FieldSpecification.WickAlgebra.timeOrder_eq_maxTimeField_mul_finset`, `exchangeSign_mul_self_swap`, `FieldSpecification.FieldOpFreeAlgebra.timeOrderF_ofFieldOpF_ofFieldOpF_not_ordered_eq_timeOrderF`, `exchangeSign_bosonic`, `FieldSpecification.WickAlgebra.timeContract_of_not_timeOrderRel_expand`, `FieldSpecification.WickAlgebra.superCommute_ofFieldOpList_ofFieldOpList`, `FieldSpecification.WickAlgebra.superCommute_ofCrAnList_ofFieldOpList`, `WickContraction.timeContract_insert_some_of_not_lt`, `FieldSpecification.FieldOpFreeAlgebra.crPartF_mul_anPartF_eq_superCommuteF`, `FieldSpecification.FieldOpFreeAlgebra.superCommuteF_crPartF_ofFieldOpListF`, `FieldSpecification.WickAlgebra.ofCrAnOp_mul_ofCrAnList_eq_superCommute`, `FieldSpecification.WickAlgebra.normalOrder_ofCrAnOp_ofFieldOpList_swap`, `FieldSpecification.FieldOpFreeAlgebra.ofFieldOpF_mul_ofFieldOpListF_eq_superCommuteF`, `FieldSpecification.FieldOpFreeAlgebra.normalOrderF_anPartF_mul_crPartF`, `WickContraction.join_singleton_sign_left`, `FieldSpecification.FieldOpFreeAlgebra.normalOrderF_swap_anPartF_crPartF`, `FieldSpecification.FieldOpFreeAlgebra.ofFieldOpListF_mul_ofFieldOpListF_eq_superCommuteF`, `FieldSpecification.FieldOpFreeAlgebra.ofCrAnListF_superCommuteF_normalOrderF_ofCrAnListF`, `WickContraction.signInsertSomeCoef_if`, `FieldSpecification.WickAlgebra.anPart_mul_anPart_swap`, `FieldSpecification.WickAlgebra.superCommute_anPart_ofFieldOp`, `FieldSpecification.FieldOpFreeAlgebra.ofCrAnListF_mul_normalOrderF_ofFieldOpListF_eq_superCommuteF`, `FieldSpecification.WickAlgebra.superCommute_ofFieldOp_ofFieldOpList`, `FieldSpecification.normalOrderSign_swap_create_annihilate`, `WickContraction.signInsertSomeProd_eq_one_if`, `FieldSpecification.FieldOpFreeAlgebra.superCommuteF_ofCrAnListF_ofFieldOpListF_eq_sum`, `FieldSpecification.FieldOpFreeAlgebra.normalOrderF_swap_create_annihilate_ofCrAnListF_ofCrAnListF`, `WickContraction.sign_insert_some_zero`, `FieldSpecification.FieldOpFreeAlgebra.ofCrAnOpF_mul_ofCrAnListF_eq_superCommuteF`, `FieldSpecification.WickAlgebra.superCommute_ofCrAnList_ofFieldOpList_eq_sum`, `WickContraction.timeContract_insert_some_of_lt`, `FieldSpecification.FieldOpFreeAlgebra.superCommuteF_anPartF_anPartF`, `FieldSpecification.WickAlgebra.superCommute_anPart_ofFieldOpList`, `WickContraction.joinSignRightExtra_eq_i_j_finset_eq_if`, `FieldSpecification.FieldOpFreeAlgebra.ofCrAnListF_mul_ofCrAnListF_eq_superCommuteF`, `WickContraction.signInsertSome_mul_filter_contracted_of_not_lt`, `FieldSpecification.WickAlgebra.superCommute_ofCrAnList_ofCrAnList_symm`, `exchangeSign_ofList_cons`, `FieldSpecification.WickAlgebra.superCommute_crPart_anPart`, `FieldSpecification.WickAlgebra.superCommute_crPart_ofFieldOpList`, `FieldSpecification.FieldOpFreeAlgebra.superCommuteF_ofCrAnOpF_ofCrAnOpF_symm`, `FieldSpecification.FieldOpFreeAlgebra.normalOrderF_swap_create_annihilate`, `exchangeSign_cocycle`, `FieldSpecification.FieldOpFreeAlgebra.superCommuteF_ofCrAnListF_ofFieldOpFsList`, `FieldSpecification.FieldOpFreeAlgebra.summerCommute_jacobi_ofCrAnListF`, `WickContraction.mul_wickTerm_eq_sum`, `FieldSpecification.FieldOpFreeAlgebra.anPartF_mul_anPartF_eq_superCommuteF`, `FieldSpecification.WickAlgebra.timeOrder_ofFieldOp_ofFieldOp_not_ordered`, `FieldSpecification.WickAlgebra.normalOrder_uncontracted_none`, `FieldSpecification.WickAlgebra.superCommute_ofFieldOpList_ofFieldOp`, `FieldSpecification.WickAlgebra.normalOrder_anPart_mul_crPart`, `FieldSpecification.FieldOpFreeAlgebra.superCommuteF_anPartF_ofFieldOpListF`, `exchangeSign_symm`, `FieldSpecification.koszulSignInsert_annihilate_cons_create`, `FieldSpecification.WickAlgebra.crPart_mul_crPart_swap`, `FieldSpecification.FieldOpFreeAlgebra.superCommuteF_anPartF_ofFieldOpF`, `FieldSpecification.FieldOpFreeAlgebra.superCommuteF_ofFieldOpListF_ofFieldOpFsList`, `FieldSpecification.WickAlgebra.normalOrder_ofFieldOpList_anPart_swap`, `WickContraction.signInsertNone_eq_prod_getDual?_Some`, `FieldSpecification.FieldOpFreeAlgebra.superCommuteF_fermionic_ofCrAnListF_eq_sum`, `FieldSpecification.WickAlgebra.ofFieldOp_mul_ofFieldOp_eq_superCommute`, `FieldSpecification.FieldOpFreeAlgebra.crPartF_mul_crPartF_eq_superCommuteF`, `FieldSpecification.FieldOpFreeAlgebra.superCommuteF_ofFieldOpListF_ofFieldOpF`, `exchangeSign_mul_self`, `FieldSpecification.timeOrderSign_pair_not_ordered`, `Wick.koszulSign_eraseIdx`, `FieldSpecification.WickAlgebra.ofCrAnList_mul_ofCrAnList_eq_superCommute`, `FieldSpecification.FieldOpFreeAlgebra.normalOrderF_ofFieldOpF_mul_ofFieldOpF`, `FieldSpecification.FieldOpFreeAlgebra.superCommuteF_ofCrAnOpF_ofCrAnOpF`, `FieldSpecification.WickAlgebra.anPart_mul_crPart_eq_superCommute`, `FieldSpecification.WickAlgebra.superCommute_anPart_crPart`, `FieldSpecification.FieldOpFreeAlgebra.ofCrAnListF_superCommuteF_normalOrderF_ofFieldOpListF`, `FieldSpecification.FieldOpFreeAlgebra.superCommuteF_ofCrAnListF_ofCrAnListF_symm`, `FieldSpecification.WickAlgebra.superCommute_ofCrAnOp_ofCrAnList_eq_sum`, `FieldSpecification.WickAlgebra.ofCrAnList_mul_ofFieldOpList_eq_superCommute`, `FieldSpecification.timerOrderSign_of_eraseMaxTimeField`, `WickContraction.singleton_sign_expand`, `FieldSpecification.FieldOpFreeAlgebra.anPartF_mul_crPartF_eq_superCommuteF`, `FieldSpecification.crAnTimeOrderSign_pair_not_ordered`, `bosonic_exchangeSign`, `FieldSpecification.WickAlgebra.superCommute_crPart_ofFieldOp`, `WickContraction.signInsertNone_eq_prod_prod`, `FieldSpecification.WickAlgebra.normalOrder_ofCrAnOp_ofCrAnList`, `Wick.koszulSignCons_eq_exchangeSign`, `FieldSpecification.WickAlgebra.superCommute_ofCrAnList_ofCrAnList_eq_sum`, `FieldSpecification.WickAlgebra.ofFieldOpList_mul_ofFieldOpList_eq_superCommute`, `FieldSpecification.WickAlgebra.normalOrder_anPart_ofFieldOpList_swap`, `FieldSpecification.WickAlgebra.normalOrder_ofFieldOpList_mul_anPart_swap`, `WickContraction.signInsertNone_eq_filterset`, `FieldSpecification.WickAlgebra.superCommute_ofCrAnOp_ofFieldOpList_eq_sum`, `WickContraction.signInsertSomeProd_eq_prod_prod`, `FieldSpecification.WickAlgebra.ofFieldOpList_mul_ofFieldOp_eq_superCommute`, `FieldSpecification.WickAlgebra.normalOrder_ofFieldOp_ofFieldOp_swap`, `exchangeSign_eq_if`, `WickContraction.sign_insert_some_of_lt`, `FieldSpecification.FieldOpFreeAlgebra.superCommuteF_ofCrAnListF_ofCrAnListF_cons`, `FieldSpecification.WickAlgebra.ofCrAnOp_superCommute_normalOrder_ofFieldOpList_sum`, `WickContraction.sign_insert_none`, `Wick.koszulSign_insertIdx`, `FieldSpecification.FieldOpFreeAlgebra.ofFieldOpListF_mul_ofFieldOpF_eq_superCommuteF`, `FieldSpecification.normalOrderSign_eraseIdx`, `FieldSpecification.WickAlgebra.crPart_mul_anPart_eq_superCommute`, `FieldSpecification.FieldOpFreeAlgebra.anPartF_mul_normalOrderF_ofFieldOpListF_eq_superCommuteF`, `FieldSpecification.FieldOpFreeAlgebra.superCommuteF_crPartF_ofFieldOpF`, `FieldSpecification.WickAlgebra.timeContract_of_not_timeOrderRel`, `fermionic_exchangeSign_fermionic`, `WickContraction.signInsertNone_eq_mul_fst_snd`, `FieldSpecification.WickAlgebra.timeContract_eq_superCommute`
`«term𝓢(_,_)»` 📖» "API Documentation")	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bosonic_exchangeSign` 📖	mathematical	—	`FieldStatistic` `instCommGroup` `exchangeSign` `bosonic`	—	`exchangeSign_symm` `exchangeSign_bosonic`
`exchangeSign_bosonic` 📖	mathematical	—	`FieldStatistic` `instCommGroup` `exchangeSign` `bosonic`	—	—
`exchangeSign_cocycle` 📖	mathematical	—	`FieldStatistic` `instCommGroup` `exchangeSign`	—	`mul_self` `bosonic_exchangeSign` `exchangeSign_bosonic` `mul_bosonic` `fermionic_exchangeSign_fermionic`
`exchangeSign_eq_if` 📖	mathematical	—	`FieldStatistic` `instCommGroup` `exchangeSign` `fermionic` `instDecidableEqFieldStatistic`	—	—
`exchangeSign_mul_self` 📖	mathematical	—	`FieldStatistic` `instCommGroup` `exchangeSign`	—	—
`exchangeSign_mul_self_swap` 📖	mathematical	—	`FieldStatistic` `instCommGroup` `exchangeSign`	—	—
`exchangeSign_ofList_cons` 📖	mathematical	—	`FieldStatistic` `instCommGroup` `exchangeSign` `ofList`	—	`ofList_cons_eq_mul`
`exchangeSign_symm` 📖	mathematical	—	`FieldStatistic` `instCommGroup` `exchangeSign`	—	—
`fermionic_exchangeSign_fermionic` 📖	mathematical	—	`FieldStatistic` `instCommGroup` `exchangeSign` `fermionic`	—	—

---

← Back to Index