TimeOrder

📁 Source: PhysLean/QFT/PerturbationTheory/FieldSpecification/TimeOrder.lean

Statistics

Metric	Count
Definitions `crAnSectionTimeOrder`, `crAnTimeOrderList`, `crAnTimeOrderRel`, `crAnTimeOrderSign`, `eraseMaxTimeField`, `instDecidableCrAnTimeOrderRel`, `instDecidableNormTimeOrderRel`, `instDecidableTimeOrderRel`, `maxTimeField`, `maxTimeFieldPos`, `maxTimeFieldPosFin`, `normTimeOrderList`, `normTimeOrderRel`, `normTimeOrderSign`, `timeOrderList`, `timeOrderRel`, `timeOrderSign`	17
Theorems `crAnSectionTimeOrder_bijective`, `crAnSectionTimeOrder_injective`, `crAnTimeOrderList_crAnSection_is_crAnSection`, `crAnTimeOrderList_nil`, `crAnTimeOrderList_pair_not_ordered`, `crAnTimeOrderList_pair_ordered`, `crAnTimeOrderList_swap_eq_time`, `crAnTimeOrderRel_refl`, `crAnTimeOrderSign_crAnSection`, `crAnTimeOrderSign_nil`, `crAnTimeOrderSign_pair_not_ordered`, `crAnTimeOrderSign_pair_ordered`, `crAnTimeOrderSign_swap_eq_time`, `eraseMaxTimeField_length`, `instIsTotalCrAnFieldOpCrAnTimeOrderRel`, `instIsTotalCrAnFieldOpNormTimeOrderRel`, `instIsTotalFieldOpTimeOrderRel`, `instIsTransCrAnFieldOpCrAnTimeOrderRel`, `instIsTransCrAnFieldOpNormTimeOrderRel`, `instIsTransFieldOpTimeOrderRel`, `koszulSignInsert_crAnTimeOrderRel_crAnSection`, `lt_maxTimeFieldPosFin_not_timeOrder`, `maxTimeFieldPos_lt_eraseMaxTimeField_length_succ`, `maxTimeFieldPos_lt_length`, `orderedInsert_crAnTimeOrderRel_crAnSection`, `orderedInsert_crAnTimeOrderRel_injective`, `orderedInsert_in_swap_eq_time`, `orderedInsert_swap_eq_time`, `sum_crAnSections_timeOrder`, `timeOrderList_eq_maxTimeField_timeOrderList`, `timeOrderList_nil`, `timeOrderList_pair_not_ordered`, `timeOrderList_pair_ordered`, `timeOrderSign_nil`, `timeOrderSign_pair_not_ordered`, `timeOrderSign_pair_ordered`, `timeOrder_maxTimeField`, `timerOrderSign_of_eraseMaxTimeField`	38
Total	55

FieldSpecification

Definitions

Name	Category	Theorems
`crAnSectionTimeOrder` 📖	CompOp	3 math math: `sum_crAnSections_timeOrder`, `crAnSectionTimeOrder_bijective`, `crAnSectionTimeOrder_injective`
`crAnTimeOrderList` 📖	CompOp	6 math math: `crAnTimeOrderList_swap_eq_time`, `crAnTimeOrderList_pair_ordered`, `crAnTimeOrderList_crAnSection_is_crAnSection`, `crAnTimeOrderList_pair_not_ordered`, `FieldOpFreeAlgebra.timeOrderF_ofCrAnListF`, `crAnTimeOrderList_nil`
`crAnTimeOrderRel` 📖	MathDef	5 math math: `koszulSignInsert_crAnTimeOrderRel_crAnSection`, `crAnTimeOrderRel_refl`, `instIsTransCrAnFieldOpCrAnTimeOrderRel`, `instIsTotalCrAnFieldOpCrAnTimeOrderRel`, `orderedInsert_crAnTimeOrderRel_crAnSection`
`crAnTimeOrderSign` 📖	CompOp	6 math math: `crAnTimeOrderSign_crAnSection`, `crAnTimeOrderSign_swap_eq_time`, `crAnTimeOrderSign_pair_ordered`, `FieldOpFreeAlgebra.timeOrderF_ofCrAnListF`, `crAnTimeOrderSign_nil`, `crAnTimeOrderSign_pair_not_ordered`
`eraseMaxTimeField` 📖	CompOp	8 math math: `FieldOpFreeAlgebra.timeOrderF_eq_maxTimeField_mul`, `timeOrderList_eq_maxTimeField_timeOrderList`, `FieldOpFreeAlgebra.timeOrderF_eq_maxTimeField_mul_finset`, `WickAlgebra.timeOrder_eq_maxTimeField_mul_finset`, `maxTimeFieldPos_lt_eraseMaxTimeField_length_succ`, `eraseMaxTimeField_length`, `timerOrderSign_of_eraseMaxTimeField`, `timeOrder_maxTimeField`
`instDecidableCrAnTimeOrderRel` 📖	CompOp	4 math math: `koszulSignInsert_crAnTimeOrderRel_crAnSection`, `orderedInsert_swap_eq_time`, `orderedInsert_crAnTimeOrderRel_crAnSection`, `orderedInsert_in_swap_eq_time`
`instDecidableNormTimeOrderRel` 📖	CompOp	—
`instDecidableTimeOrderRel` 📖	CompOp	3 math math: `koszulSignInsert_crAnTimeOrderRel_crAnSection`, `orderedInsert_crAnTimeOrderRel_crAnSection`, `WickAlgebra.timeContract_eq_superCommute`
`maxTimeField` 📖	CompOp	7 math math: `FieldOpFreeAlgebra.timeOrderF_eq_maxTimeField_mul`, `timeOrderList_eq_maxTimeField_timeOrderList`, `FieldOpFreeAlgebra.timeOrderF_eq_maxTimeField_mul_finset`, `WickAlgebra.timeOrder_eq_maxTimeField_mul_finset`, `lt_maxTimeFieldPosFin_not_timeOrder`, `timerOrderSign_of_eraseMaxTimeField`, `timeOrder_maxTimeField`
`maxTimeFieldPos` 📖	CompOp	4 math math: `FieldOpFreeAlgebra.timeOrderF_eq_maxTimeField_mul`, `maxTimeFieldPos_lt_length`, `maxTimeFieldPos_lt_eraseMaxTimeField_length_succ`, `timerOrderSign_of_eraseMaxTimeField`
`maxTimeFieldPosFin` 📖	CompOp	2 math math: `FieldOpFreeAlgebra.timeOrderF_eq_maxTimeField_mul_finset`, `WickAlgebra.timeOrder_eq_maxTimeField_mul_finset`
`normTimeOrderList` 📖	CompOp	1 math math: `FieldOpFreeAlgebra.normTimeOrder_ofCrAnListF`
`normTimeOrderRel` 📖	MathDef	2 math math: `instIsTransCrAnFieldOpNormTimeOrderRel`, `instIsTotalCrAnFieldOpNormTimeOrderRel`
`normTimeOrderSign` 📖	CompOp	1 math math: `FieldOpFreeAlgebra.normTimeOrder_ofCrAnListF`
`timeOrderList` 📖	CompOp	9 math math: `timeOrderList_eq_maxTimeField_timeOrderList`, `crAnTimeOrderList_crAnSection_is_crAnSection`, `timeOrderList_nil`, `FieldOpFreeAlgebra.timeOrderF_ofFieldOpListF`, `sum_crAnSections_timeOrder`, `timeOrderList_pair_not_ordered`, `timeOrderList_pair_ordered`, `crAnSectionTimeOrder_bijective`, `crAnSectionTimeOrder_injective`
`timeOrderRel` 📖	MathDef	14 math math: `WickContraction.EqTimeOnly.exists_join_singleton_of_card_ge_zero`, `WickContraction.EqTimeOnly.timeOrderRel_both_of_eqTimeOnly`, `instIsTotalFieldOpTimeOrderRel`, `WickContraction.EqTimeOnly.exists_join_singleton_of_not_eqTimeOnly`, `WickContraction.EqTimeOnly.eqTimeOnly_iff_forall_finset`, `koszulSignInsert_crAnTimeOrderRel_crAnSection`, `WickContraction.EqTimeOnly.timeOrderRel_of_eqTimeOnly_pair`, `lt_maxTimeFieldPosFin_not_timeOrder`, `WickContraction.haveEqTime_iff_finset`, `WickContraction.pair_mem_eqTimeContractSet_iff`, `orderedInsert_crAnTimeOrderRel_crAnSection`, `instIsTransFieldOpTimeOrderRel`, `timeOrder_maxTimeField`, `WickAlgebra.timeContract_eq_superCommute`
`timeOrderSign` 📖	CompOp	6 math math: `timeOrderSign_nil`, `timeOrderSign_pair_ordered`, `crAnTimeOrderSign_crAnSection`, `FieldOpFreeAlgebra.timeOrderF_ofFieldOpListF`, `timeOrderSign_pair_not_ordered`, `timerOrderSign_of_eraseMaxTimeField`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`crAnSectionTimeOrder_bijective` 📖	mathematical	—	`CrAnSection` `timeOrderList` `crAnSectionTimeOrder`	—	`crAnSectionTimeOrder_injective` `CrAnSection.card_perm_eq`
`crAnSectionTimeOrder_injective` 📖	mathematical	—	`CrAnSection` `timeOrderList` `crAnSectionTimeOrder`	—	`crAnFieldOpToFieldOp.eq_1` `orderedInsert_crAnTimeOrderRel_injective` `crAnTimeOrderList_crAnSection_is_crAnSection`
`crAnTimeOrderList_crAnSection_is_crAnSection` 📖	mathematical	—	`CrAnFieldOp` `FieldOp` `crAnFieldOpToFieldOp` `crAnTimeOrderList` `timeOrderList`	—	`crAnTimeOrderList_nil` `timeOrderList_nil` `orderedInsert_crAnTimeOrderRel_crAnSection`
`crAnTimeOrderList_nil` 📖	mathematical	—	`crAnTimeOrderList` `CrAnFieldOp`	—	—
`crAnTimeOrderList_pair_not_ordered` 📖	mathematical	`crAnTimeOrderRel`	`crAnTimeOrderList` `CrAnFieldOp`	—	—
`crAnTimeOrderList_pair_ordered` 📖	mathematical	`crAnTimeOrderRel`	`crAnTimeOrderList` `CrAnFieldOp`	—	—
`crAnTimeOrderList_swap_eq_time` 📖	mathematical	`crAnTimeOrderRel`	`crAnTimeOrderList` `CrAnFieldOp`	—	`orderedInsert_swap_eq_time` `instIsTransCrAnFieldOpCrAnTimeOrderRel` `crAnTimeOrderList.eq_1` `orderedInsert_in_swap_eq_time`
`crAnTimeOrderRel_refl` 📖	mathematical	—	`crAnTimeOrderRel`	—	`instIsTotalCrAnFieldOpCrAnTimeOrderRel`
`crAnTimeOrderSign_crAnSection` 📖	mathematical	—	`crAnTimeOrderSign` `CrAnFieldOp` `FieldOp` `crAnFieldOpToFieldOp` `timeOrderSign`	—	`crAnTimeOrderSign_nil` `timeOrderSign_nil` `koszulSignInsert_crAnTimeOrderRel_crAnSection`
`crAnTimeOrderSign_nil` 📖	mathematical	—	`crAnTimeOrderSign` `CrAnFieldOp`	—	—
`crAnTimeOrderSign_pair_not_ordered` 📖	mathematical	`crAnTimeOrderRel`	`crAnTimeOrderSign` `CrAnFieldOp` `FieldStatistic` `FieldStatistic.instCommGroup` `FieldStatistic.exchangeSign` `crAnStatistics`	—	`FieldStatistic.exchangeSign_eq_if`
`crAnTimeOrderSign_pair_ordered` 📖	mathematical	`crAnTimeOrderRel`	`crAnTimeOrderSign` `CrAnFieldOp`	—	—
`crAnTimeOrderSign_swap_eq_time` 📖	mathematical	`crAnTimeOrderRel`	`crAnTimeOrderSign` `CrAnFieldOp`	—	`Wick.koszulSign_swap_eq_rel`
`eraseMaxTimeField_length` 📖	mathematical	—	`FieldOp` `eraseMaxTimeField`	—	`PhysLean.List.eraseIdx_length'`
`instIsTotalCrAnFieldOpCrAnTimeOrderRel` 📖	mathematical	—	`CrAnFieldOp` `crAnTimeOrderRel`	—	`instIsTotalFieldOpTimeOrderRel`
`instIsTotalCrAnFieldOpNormTimeOrderRel` 📖	mathematical	—	`CrAnFieldOp` `normTimeOrderRel`	—	`instIsTotalCrAnFieldOpCrAnTimeOrderRel` `instIsTotalCrAnFieldOpNormalOrderRel`
`instIsTotalFieldOpTimeOrderRel` 📖	mathematical	—	`FieldOp` `timeOrderRel`	—	—
`instIsTransCrAnFieldOpCrAnTimeOrderRel` 📖	mathematical	—	`CrAnFieldOp` `crAnTimeOrderRel`	—	`instIsTransFieldOpTimeOrderRel`
`instIsTransCrAnFieldOpNormTimeOrderRel` 📖	mathematical	—	`CrAnFieldOp` `normTimeOrderRel`	—	`instIsTransCrAnFieldOpCrAnTimeOrderRel` `instIsTransCrAnFieldOpNormalOrderRel`
`instIsTransFieldOpTimeOrderRel` 📖	mathematical	—	`FieldOp` `timeOrderRel`	—	—
`koszulSignInsert_crAnTimeOrderRel_crAnSection` 📖	mathematical	`FieldOp` `fieldOpToCrAnType`	`Wick.koszulSignInsert` `CrAnFieldOp` `crAnStatistics` `crAnTimeOrderRel` `instDecidableCrAnTimeOrderRel` `crAnFieldOpToFieldOp` `fieldOpStatistic` `timeOrderRel` `instDecidableTimeOrderRel`	—	—
`lt_maxTimeFieldPosFin_not_timeOrder` 📖	mathematical	`FieldOp` `eraseMaxTimeField` `maxTimeFieldPosFin`	`timeOrderRel` `maxTimeField`	—	`PhysLean.List.insertionSortMin_lt_mem_insertionSortDropMinPos_of_lt`
`maxTimeFieldPos_lt_eraseMaxTimeField_length_succ` 📖	mathematical	—	`maxTimeFieldPos` `FieldOp` `eraseMaxTimeField`	—	`eraseMaxTimeField_length` `maxTimeFieldPos_lt_length`
`maxTimeFieldPos_lt_length` 📖	mathematical	—	`maxTimeFieldPos` `FieldOp`	—	—
`orderedInsert_crAnTimeOrderRel_crAnSection` 📖	mathematical	`FieldOp` `fieldOpToCrAnType`	`CrAnFieldOp` `crAnFieldOpToFieldOp` `crAnTimeOrderRel` `instDecidableCrAnTimeOrderRel` `timeOrderRel` `instDecidableTimeOrderRel`	—	—
`orderedInsert_crAnTimeOrderRel_injective` 📖	—	`FieldOp` `fieldOpToCrAnType` `CrAnFieldOp` `crAnTimeOrderRel` `instDecidableCrAnTimeOrderRel` `crAnFieldOpToFieldOp`	—	—	`crAnFieldOpToFieldOp.eq_1`
`orderedInsert_in_swap_eq_time` 📖	mathematical	`crAnTimeOrderRel`	`CrAnFieldOp` `instDecidableCrAnTimeOrderRel`	—	`instIsTransCrAnFieldOpCrAnTimeOrderRel`
`orderedInsert_swap_eq_time` 📖	mathematical	`crAnTimeOrderRel`	`CrAnFieldOp` `instDecidableCrAnTimeOrderRel`	—	`instIsTransCrAnFieldOpCrAnTimeOrderRel`
`sum_crAnSections_timeOrder` 📖	mathematical	—	`CrAnSection` `timeOrderList` `CrAnSection.fintype` `crAnSectionTimeOrder`	—	`crAnSectionTimeOrder_bijective`
`timeOrderList_eq_maxTimeField_timeOrderList` 📖	mathematical	—	`timeOrderList` `FieldOp` `maxTimeField` `eraseMaxTimeField`	—	`PhysLean.List.insertionSort_eq_insertionSortMin_cons` `instIsTotalFieldOpTimeOrderRel` `instIsTransFieldOpTimeOrderRel`
`timeOrderList_nil` 📖	mathematical	—	`timeOrderList` `FieldOp`	—	—
`timeOrderList_pair_not_ordered` 📖	mathematical	`timeOrderRel`	`timeOrderList` `FieldOp`	—	—
`timeOrderList_pair_ordered` 📖	mathematical	`timeOrderRel`	`timeOrderList` `FieldOp`	—	—
`timeOrderSign_nil` 📖	mathematical	—	`timeOrderSign` `FieldOp`	—	—
`timeOrderSign_pair_not_ordered` 📖	mathematical	`timeOrderRel`	`timeOrderSign` `FieldOp` `FieldStatistic` `FieldStatistic.instCommGroup` `FieldStatistic.exchangeSign` `fieldOpStatistic`	—	`FieldStatistic.exchangeSign_eq_if`
`timeOrderSign_pair_ordered` 📖	mathematical	`timeOrderRel`	`timeOrderSign` `FieldOp`	—	—
`timeOrder_maxTimeField` 📖	mathematical	—	`timeOrderRel` `maxTimeField` `FieldOp` `eraseMaxTimeField`	—	`PhysLean.List.insertionSortMin_lt_mem_insertionSortDropMinPos` `instIsTotalFieldOpTimeOrderRel` `instIsTransFieldOpTimeOrderRel`
`timerOrderSign_of_eraseMaxTimeField` 📖	mathematical	—	`timeOrderSign` `eraseMaxTimeField` `FieldOp` `FieldStatistic` `FieldStatistic.instCommGroup` `FieldStatistic.exchangeSign` `fieldOpStatistic` `maxTimeField` `FieldStatistic.ofList` `maxTimeFieldPos`	—	`eraseMaxTimeField.eq_1` `PhysLean.List.insertionSortDropMinPos.eq_1` `timeOrderSign.eq_1` `Wick.koszulSign_eraseIdx_insertionSortMinPos` `instIsTotalFieldOpTimeOrderRel` `instIsTransFieldOpTimeOrderRel` `maxTimeField.eq_1`

---

← Back to Index