Documentation Verification Report

TimeCond

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

Statistics

Metric	Count
Definitions `EqTimeOnly`, `HaveEqTime`, `eqTimeContractSet`, `hasEqTimeEquiv`, `instDecidableEqTimeOnly`, `instDecidableHaveEqTime`	6
Theorems `empty_mem`, `eqTimeOnly_congr`, `eqTimeOnly_iff_forall_finset`, `exists_join_singleton_of_card_ge_zero`, `exists_join_singleton_of_not_eqTimeOnly`, `quotContraction_eqTimeOnly`, `staticContract_eq_timeContract_of_eqTimeOnly`, `timeOrderRel_both_of_eqTimeOnly`, `timeOrderRel_of_eqTimeOnly_pair`, `timeOrder_staticContract_of_not_mem`, `timeOrder_timeContract_mul_of_eqTimeOnly_left`, `timeOrder_timeContract_mul_of_eqTimeOnly_mid`, `timeOrder_timeContract_mul_of_eqTimeOnly_mid_induction`, `timeOrder_timeContract_of_not_eqTimeOnly`, `empty_not_haveEqTime`, `eqTimeContractSet_of_mem_eqTimeOnly`, `eqTimeContractSet_of_not_haveEqTime`, `eqTimeContractSet_subset`, `hasEqTimeEquiv_ext_sigma`, `haveEqTime_iff_finset`, `join_eqTimeContractSet`, `join_haveEqTime_of_eqTimeOnly_nonEmpty`, `mem_of_mem_eqTimeContractSet`, `pair_mem_eqTimeContractSet_iff`, `quotContraction_eqTimeContractSet_not_haveEqTime`, `subContraction_eqTimeContractSet_eqTimeOnly`, `subContraction_eqTimeContractSet_not_empty_of_haveEqTime`, `sum_haveEqTime`	28
Total	34

WickContraction

Definitions

Name	Category	Theorems
`EqTimeOnly` 📖	MathDef	10 math math: `EqTimeOnly.eqTimeOnly_congr`, `EqTimeOnly.eqTimeOnly_iff_forall_finset`, `EqTimeOnly.empty_mem`, `FieldSpecification.WickAlgebra.normalOrder_timeOrder_ofFieldOpList_eq_eqTimeOnly_empty`, `sum_haveEqTime`, `FieldSpecification.WickAlgebra.normalOrder_timeOrder_ofFieldOpList_eq_not_haveEqTime_sub_inductive`, `FieldSpecification.WickAlgebra.timeOrder_ofFieldOpList_eq_eqTimeOnly_empty`, `subContraction_eqTimeContractSet_eqTimeOnly`, `FieldSpecification.WickAlgebra.timeOrder_haveEqTime_split`, `FieldSpecification.WickAlgebra.timeOrder_ofFieldOpList_eqTimeOnly`
`HaveEqTime` 📖	MathDef	9 math math: `FieldSpecification.WickAlgebra.wicks_theorem_normal_order_empty`, `empty_not_haveEqTime`, `FieldSpecification.WickAlgebra.wicks_theorem_normal_order`, `haveEqTime_iff_finset`, `sum_haveEqTime`, `FieldSpecification.WickAlgebra.normalOrder_timeOrder_ofFieldOpList_eq_not_haveEqTime_sub_inductive`, `quotContraction_eqTimeContractSet_not_haveEqTime`, `FieldSpecification.WickAlgebra.timeOrder_haveEqTime_split`, `join_haveEqTime_of_eqTimeOnly_nonEmpty`
`eqTimeContractSet` 📖	CompOp	7 math math: `join_eqTimeContractSet`, `pair_mem_eqTimeContractSet_iff`, `eqTimeContractSet_subset`, `quotContraction_eqTimeContractSet_not_haveEqTime`, `eqTimeContractSet_of_mem_eqTimeOnly`, `subContraction_eqTimeContractSet_eqTimeOnly`, `eqTimeContractSet_of_not_haveEqTime`
`hasEqTimeEquiv` 📖	CompOp	—
`instDecidableEqTimeOnly` 📖	CompOp	6 math math: `FieldSpecification.WickAlgebra.normalOrder_timeOrder_ofFieldOpList_eq_eqTimeOnly_empty`, `sum_haveEqTime`, `FieldSpecification.WickAlgebra.normalOrder_timeOrder_ofFieldOpList_eq_not_haveEqTime_sub_inductive`, `FieldSpecification.WickAlgebra.timeOrder_ofFieldOpList_eq_eqTimeOnly_empty`, `FieldSpecification.WickAlgebra.timeOrder_haveEqTime_split`, `FieldSpecification.WickAlgebra.timeOrder_ofFieldOpList_eqTimeOnly`
`instDecidableHaveEqTime` 📖	CompOp	5 math math: `FieldSpecification.WickAlgebra.wicks_theorem_normal_order_empty`, `FieldSpecification.WickAlgebra.wicks_theorem_normal_order`, `sum_haveEqTime`, `FieldSpecification.WickAlgebra.normalOrder_timeOrder_ofFieldOpList_eq_not_haveEqTime_sub_inductive`, `FieldSpecification.WickAlgebra.timeOrder_haveEqTime_split`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`empty_not_haveEqTime` 📖	mathematical	—	`HaveEqTime` `empty` `FieldSpecification.FieldOp`	—	`haveEqTime_iff_finset`
`eqTimeContractSet_of_mem_eqTimeOnly` 📖	mathematical	`EqTimeOnly`	`eqTimeContractSet` `FieldSpecification.FieldOp`	—	`EqTimeOnly.eqTimeOnly_iff_forall_finset`
`eqTimeContractSet_of_not_haveEqTime` 📖	mathematical	`HaveEqTime`	`eqTimeContractSet` `FieldSpecification.FieldOp`	—	`haveEqTime_iff_finset`
`eqTimeContractSet_subset` 📖	mathematical	—	`FieldSpecification.FieldOp` `eqTimeContractSet`	—	—
`hasEqTimeEquiv_ext_sigma` 📖	—	`WickContraction` `FieldSpecification.FieldOp` `EqTimeOnly` `empty` `uncontractedListGet` `HaveEqTime` `congr`	—	—	—
`haveEqTime_iff_finset` 📖	mathematical	—	`HaveEqTime` `FieldSpecification.timeOrderRel` `FieldSpecification.FieldOp` `fstFieldOfContract` `sndFieldOfContract`	—	`eq_fstFieldOfContract_of_mem` `eq_sndFieldOfContract_of_mem` `finset_eq_fstFieldOfContract_sndFieldOfContract`
`join_eqTimeContractSet` 📖	mathematical	—	`eqTimeContractSet` `join` `FieldSpecification.FieldOp` `uncontractedListGet` `uncontractedListEmd`	—	`mem_of_mem_eqTimeContractSet` `joinLiftLeft_or_joinLiftRight_of_mem_join` `join_fstFieldOfContract_joinLiftLeft` `join_sndFieldOfContract_joinLift` `join_fstFieldOfContract_joinLiftRight` `getElem_uncontractedListEmd` `join_sndFieldOfContract_joinLiftRight`
`join_haveEqTime_of_eqTimeOnly_nonEmpty` 📖	mathematical	`EqTimeOnly`	`HaveEqTime` `join`	—	`exists_pair_of_not_eq_empty`
`mem_of_mem_eqTimeContractSet` 📖	—	`FieldSpecification.FieldOp` `eqTimeContractSet`	—	—	—
`pair_mem_eqTimeContractSet_iff` 📖	mathematical	`FieldSpecification.FieldOp`	`eqTimeContractSet` `FieldSpecification.timeOrderRel`	—	`eq_fstFieldOfContract_of_mem` `eq_sndFieldOfContract_of_mem`
`quotContraction_eqTimeContractSet_not_haveEqTime` 📖	mathematical	—	`HaveEqTime` `uncontractedListGet` `subContraction` `eqTimeContractSet` `eqTimeContractSet_subset` `quotContraction`	—	`eqTimeContractSet_subset` `haveEqTime_iff_finset` `subContraction_uncontractedList_get` `mem_of_mem_quotContraction` `quotContraction_fstFieldOfContract_uncontractedListEmd` `quotContraction_sndFieldOfContract_uncontractedListEmd` `uncontractedListEmd_finset_not_mem`
`subContraction_eqTimeContractSet_eqTimeOnly` 📖	mathematical	—	`EqTimeOnly` `subContraction` `eqTimeContractSet` `eqTimeContractSet_subset`	—	`eqTimeContractSet_subset` `EqTimeOnly.eqTimeOnly_iff_forall_finset` `mem_of_mem_subContraction` `subContraction_fstFieldOfContract` `subContraction_sndFieldOfContract`
`subContraction_eqTimeContractSet_not_empty_of_haveEqTime` 📖	—	`HaveEqTime`	—	—	`eqTimeContractSet_subset` `pair_mem_eqTimeContractSet_iff`
`sum_haveEqTime` 📖	mathematical	—	`WickContraction` `FieldSpecification.FieldOp` `HaveEqTime` `instDecidableHaveEqTime` `fintype_succ` `EqTimeOnly` `empty` `instDecidableEqTimeOnly` `instDecidableEq` `uncontractedListGet` `join`	—	—

WickContraction.EqTimeOnly

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`empty_mem` 📖	mathematical	—	`WickContraction.EqTimeOnly` `WickContraction.empty` `FieldSpecification.FieldOp`	—	`eqTimeOnly_iff_forall_finset`
`eqTimeOnly_congr` 📖	mathematical	—	`WickContraction.EqTimeOnly` `WickContraction` `FieldSpecification.FieldOp` `WickContraction.congr`	—	—
`eqTimeOnly_iff_forall_finset` 📖	mathematical	—	`WickContraction.EqTimeOnly` `FieldSpecification.timeOrderRel` `FieldSpecification.FieldOp` `WickContraction.fstFieldOfContract` `WickContraction.sndFieldOfContract`	—	`timeOrderRel_both_of_eqTimeOnly` `WickContraction.finset_eq_fstFieldOfContract_sndFieldOfContract` `WickContraction.eq_fstFieldOfContract_of_mem` `WickContraction.eq_sndFieldOfContract_of_mem`
`exists_join_singleton_of_card_ge_zero` 📖	mathematical	`FieldSpecification.FieldOp` `WickContraction.EqTimeOnly`	`WickContraction.join` `WickContraction.singleton` `FieldSpecification.timeOrderRel` `WickContraction.uncontractedListGet`	—	`WickContraction.exists_contraction_pair_of_card_ge_zero` `WickContraction.fstFieldOfContract_lt_sndFieldOfContract` `WickContraction.subContraction_singleton_eq_singleton` `WickContraction.join_congr` `WickContraction.congr_trans_apply` `WickContraction.join_sub_quot` `timeOrderRel_both_of_eqTimeOnly` `WickContraction.finset_eq_fstFieldOfContract_sndFieldOfContract` `eqTimeOnly_congr` `quotContraction_eqTimeOnly` `WickContraction.card_congr` `WickContraction.subContraction_card_plus_quotContraction_card_eq`
`exists_join_singleton_of_not_eqTimeOnly` 📖	mathematical	`WickContraction.EqTimeOnly`	`WickContraction.join` `WickContraction.singleton` `FieldSpecification.FieldOp` `FieldSpecification.timeOrderRel`	—	`eqTimeOnly_iff_forall_finset` `WickContraction.fstFieldOfContract_lt_sndFieldOfContract` `WickContraction.subContraction_singleton_eq_singleton` `WickContraction.join_congr` `WickContraction.congr_trans_apply` `WickContraction.join_sub_quot`
`quotContraction_eqTimeOnly` 📖	mathematical	`WickContraction.EqTimeOnly` `FieldSpecification.FieldOp`	`WickContraction.uncontractedListGet` `WickContraction.subContraction` `WickContraction.quotContraction`	—	`eqTimeOnly_iff_forall_finset` `WickContraction.subContraction_uncontractedList_get` `WickContraction.mem_of_mem_quotContraction` `WickContraction.quotContraction_fstFieldOfContract_uncontractedListEmd` `WickContraction.quotContraction_sndFieldOfContract_uncontractedListEmd`
`staticContract_eq_timeContract_of_eqTimeOnly` 📖	mathematical	`WickContraction.EqTimeOnly`	`WickContraction.staticContract` `WickContraction.timeContract`	—	`FieldSpecification.WickAlgebra.timeContract_of_timeOrderRel` `timeOrderRel_of_eqTimeOnly_pair` `WickContraction.finset_eq_fstFieldOfContract_sndFieldOfContract`
`timeOrderRel_both_of_eqTimeOnly` 📖	mathematical	`FieldSpecification.FieldOp` `WickContraction.EqTimeOnly`	`FieldSpecification.timeOrderRel`	—	`timeOrderRel_of_eqTimeOnly_pair`
`timeOrderRel_of_eqTimeOnly_pair` 📖	mathematical	`FieldSpecification.FieldOp` `WickContraction.EqTimeOnly`	`FieldSpecification.timeOrderRel`	—	—
`timeOrder_staticContract_of_not_mem` 📖	mathematical	`WickContraction.EqTimeOnly`	`FieldSpecification.WickAlgebra` `FieldSpecification.FieldOpFreeAlgebra` `FieldSpecification.CrAnFieldOp` `FieldSpecification.fieldOpIdealSet` `FieldSpecification.WickAlgebra.timeOrder` `WickContraction.staticContract`	—	`exists_join_singleton_of_not_eqTimeOnly` `WickContraction.join_staticContract` `WickContraction.singleton_staticContract` `FieldSpecification.WickAlgebra.timeOrder_timeOrder_left` `FieldSpecification.WickAlgebra.timeOrder_superCommute_anPart_ofFieldOp_neq_time`
`timeOrder_timeContract_mul_of_eqTimeOnly_left` 📖	mathematical	`WickContraction.EqTimeOnly`	`FieldSpecification.WickAlgebra` `FieldSpecification.FieldOpFreeAlgebra` `FieldSpecification.CrAnFieldOp` `FieldSpecification.fieldOpIdealSet` `FieldSpecification.WickAlgebra.timeOrder` `WickContraction.timeContract`	—	`timeOrder_timeContract_mul_of_eqTimeOnly_mid`
`timeOrder_timeContract_mul_of_eqTimeOnly_mid` 📖	mathematical	`WickContraction.EqTimeOnly`	`FieldSpecification.WickAlgebra` `FieldSpecification.FieldOpFreeAlgebra` `FieldSpecification.CrAnFieldOp` `FieldSpecification.fieldOpIdealSet` `FieldSpecification.WickAlgebra.timeOrder` `WickContraction.timeContract`	—	`timeOrder_timeContract_mul_of_eqTimeOnly_mid_induction`
`timeOrder_timeContract_mul_of_eqTimeOnly_mid_induction` 📖	mathematical	`WickContraction.EqTimeOnly` `FieldSpecification.FieldOp`	`FieldSpecification.WickAlgebra` `FieldSpecification.FieldOpFreeAlgebra` `FieldSpecification.CrAnFieldOp` `FieldSpecification.fieldOpIdealSet` `FieldSpecification.WickAlgebra.timeOrder` `WickContraction.timeContract`	—	`WickContraction.timeContract_empty` `WickContraction.card_zero_iff_empty` `exists_join_singleton_of_card_ge_zero` `WickContraction.join_timeContract` `FieldSpecification.WickAlgebra.timeContract_mem_center` `WickContraction.singleton_timeContract` `FieldSpecification.WickAlgebra.timeOrder_timeContract_eq_time_mid`
`timeOrder_timeContract_of_not_eqTimeOnly` 📖	mathematical	`WickContraction.EqTimeOnly`	`FieldSpecification.WickAlgebra` `FieldSpecification.FieldOpFreeAlgebra` `FieldSpecification.CrAnFieldOp` `FieldSpecification.fieldOpIdealSet` `FieldSpecification.WickAlgebra.timeOrder` `WickContraction.timeContract`	—	`exists_join_singleton_of_not_eqTimeOnly` `WickContraction.join_timeContract` `FieldSpecification.WickAlgebra.timeContract_mem_center` `WickContraction.singleton_timeContract` `FieldSpecification.WickAlgebra.timeOrder_timeOrder_left` `FieldSpecification.WickAlgebra.timeOrder_timeContract_neq_time`

---

← Back to Index