Basic

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

Statistics

Metric	Count
Definitions `WickContraction`, `GradingCompliant`, `congr`, `congrLift`, `congrLiftInv`, `contractEquivFinTwo`, `empty`, `fstFieldOfContract`, `getDual?`, `instDecidableEq`, `sigmaContractedEquiv`, `sndFieldOfContract`	12
Theorems `card_congr`, `card_zero_iff_empty`, `congrLiftInv_rfl`, `congrLift_bijective`, `congrLift_injective`, `congrLift_rfl`, `congrLift_surjective`, `congr_contractions`, `congr_refl`, `congr_trans`, `congr_trans_apply`, `eq_filter_mem_self`, `eq_fstFieldOfContract_of_mem`, `eq_sndFieldOfContract_of_mem`, `exists_pair_of_not_eq_empty`, `finset_eq_fstFieldOfContract_sndFieldOfContract`, `fstFieldOfContract_congr`, `fstFieldOfContract_getDual?`, `fstFieldOfContract_getDual?_isSome`, `fstFieldOfContract_le_sndFieldOfContract`, `fstFieldOfContract_lt_sndFieldOfContract`, `fstFieldOfContract_mem`, `fstFieldOfContract_neq_sndFieldOfContract`, `getDual?_congr`, `getDual?_congr_get`, `getDual?_eq_some_iff_mem`, `getDual?_eq_some_neq`, `getDual?_getDual?_get_get`, `getDual?_getDual?_get_isSome`, `getDual?_getDual?_get_not_none`, `getDual?_get_self_mem`, `getDual?_get_self_neq`, `getDual?_isSome_iff`, `getDual?_isSome_of_mem`, `getDual?_one_eq_none`, `gradingCompliant_congr`, `mem_congr_iff`, `prod_finset_eq_mul_fst_snd`, `self_getDual?_get_mem`, `self_neq_getDual?_get`, `sndFieldOfContract_congr`, `sndFieldOfContract_getDual?`, `sndFieldOfContract_getDual?_isSome`, `sndFieldOfContract_mem`	44
Total	56

WickContraction

Definitions

Name	Category	Theorems
`GradingCompliant` 📖	MathDef	1 math math: `gradingCompliant_congr`
`congr` 📖	CompOp	23 math math: `getDual?_congr`, `congr_contractions`, `EqTimeOnly.eqTimeOnly_congr`, `gradingCompliant_congr`, `congr_uncontractedList`, `card_congr`, `join_assoc`, `congr_trans`, `sum_extractEquiv_congr`, `sndFieldOfContract_congr`, `congrLift_injective`, `mem_congr_iff`, `congrLiftInv_rfl`, `congr_trans_apply`, `sign_congr`, `congr_uncontracted`, `extractEquiv_apply_congr_symm_apply`, `fstFieldOfContract_congr`, `join_congr`, `congrLift_bijective`, `congr_refl`, `empty_join`, `congrLift_surjective`
`congrLift` 📖	CompOp	12 math math: `insertAndContract_fstFieldOfContract`, `insertAndContract_sndFieldOfContract`, `insertAndContract_sndFieldOfContract_some_incl`, `sndFieldOfContract_congr`, `congrLift_injective`, `congrLift_rfl`, `insertAndContract_some_prod_contractions`, `fstFieldOfContract_congr`, `insertAndContract_none_prod_contractions`, `insertAndContract_fstFieldOfContract_some_incl`, `congrLift_bijective`, `congrLift_surjective`
`congrLiftInv` 📖	CompOp	1 math math: `congrLiftInv_rfl`
`contractEquivFinTwo` 📖	CompOp	—
`empty` 📖	CompOp	23 math math: `sign_empty`, `getDual?_empty_eq_none`, `card_zero_iff_empty`, `join_empty`, `mem_uncontracted_empty`, `empty_not_haveEqTime`, `uncontractedListEmd_empty`, `wickTerm_empty_nil`, `EqTimeOnly.empty_mem`, `uncontractedListGet_empty`, `timeContract_empty`, `nil_zero_uncontractedList`, `FieldSpecification.WickAlgebra.normalOrder_timeOrder_ofFieldOpList_eq_eqTimeOnly_empty`, `uncontracted_empty`, `staticWickTerm_empty_nil`, `uncontractedList_empty`, `sum_haveEqTime`, `uncontracted_card_eq_iff`, `FieldSpecification.WickAlgebra.normalOrder_timeOrder_ofFieldOpList_eq_not_haveEqTime_sub_inductive`, `FieldSpecification.WickAlgebra.timeOrder_ofFieldOpList_eq_eqTimeOnly_empty`, `FieldSpecification.WickAlgebra.timeOrder_haveEqTime_split`, `sum_WickContraction_nil`, `empty_join`
`fstFieldOfContract` 📖	CompOp	26 math math: `prod_finset_eq_mul_fst_snd`, `sign_right_eq_prod_mul_prod`, `join_fstFieldOfContract_joinLiftRight`, `join_singleton_sign_right`, `sndFieldOfContract_getDual?`, `insertAndContract_fstFieldOfContract`, `join_fstFieldOfContract_joinLiftLeft`, `fstFieldOfContract_le_sndFieldOfContract`, `fstFieldOfContract_getDual?`, `signInsertSomeProd_eq_one_if`, `EqTimeOnly.eqTimeOnly_iff_forall_finset`, `joinSignRightExtra_eq_i_j_finset_eq_if`, `insertAndContractNat_fstFieldOfContract`, `singleton_fstFieldOfContract`, `subContraction_fstFieldOfContract`, `finset_eq_fstFieldOfContract_sndFieldOfContract`, `haveEqTime_iff_finset`, `fstFieldOfContract_congr`, `insertAndContract_fstFieldOfContract_some_incl`, `fstFieldOfContract_lt_sndFieldOfContract`, `fstFieldOfContract_mem`, `eq_fstFieldOfContract_of_mem`, `quotContraction_fstFieldOfContract_uncontractedListEmd`, `fstFieldOfContract_getDual?_isSome`, `signInsertNone_eq_mul_fst_snd`, `subContraction_singleton_eq_singleton`
`getDual?` 📖	CompOp	56 math math: `join_getDual?_apply_uncontractedListEmb_eq_none_iff`, `join_singleton_signFinset_eq_filter`, `consAddContract_getDual?_zero`, `getDual?_empty_eq_none`, `getDual?_congr`, `sndFieldOfContract_getDual?`, `signInsertSomeProd_eq_prod_fin`, `getDual?_eq_some_iff_mem`, `insertAndContract_some_getDual?_self_eq`, `insertAndContract_none_succAbove_getDual?_eq_none_iff`, `insertAndContractNat_some_getDual?_neq_none`, `insertAndContract_some_getDual?_self_not_none`, `signInsertSomeCoef_eq_finset`, `getDual?_isSome_iff`, `singleton_getDual?_eq_none_iff_neq`, `insertAndContractNat_some_getDual?_of_neq`, `insertAndContract_none_succAbove_getDual?_isSome_iff`, `fromInvolution_getDual?_isSome`, `wickContraction_zero_some_eq_sum`, `getDual?_eq_none_iff_mem_uncontracted`, `signInsertSomeProd_eq_finset`, `consAddContract_getDual?_self_succ`, `signInsertNone_eq_filter_map`, `insertAndContract_none_getDual?_self`, `insertAndContract_some_succAbove_getDual?_eq_option`, `getDual?_isSome_of_mem`, `mem_erase_uncontracted_iff`, `insertAndContractNat_bijective`, `fstFieldOfContract_getDual?`, `wickContraction_zero_none_card`, `insertAndContract_isSome_getDual?_self`, `insertAndContractNat_some_getDual?_eq`, `join_getDual?_apply_uncontractedListEmb_isSome_iff`, `join_getDual?_apply_uncontractedListEmb`, `insertAndContractNat_succAbove_getDual?_isSome_iff`, `wickContraction_card_eq_sum_zero_none_isSome`, `sndFieldOfContract_getDual?_isSome`, `insertAndContractNat_succAbove_getDual?_eq_none_iff`, `join_singleton_getDual?_left`, `signInsertNone_eq_prod_getDual?_Some`, `stat_signFinset_insert_some_self_fst`, `insertAndContractNat_none_getDual?_eq_none`, `join_singleton_getDual?_right`, `getDual?_one_eq_none`, `getDualErase_isSome_iff_getDual?_isSome`, `insertAndContract_some_getDual?_some_eq`, `join_singleton_left_signFinset_eq_filter`, `insertAndContractNat_none_getDual?_isNone`, `signInsertNone_eq_filterset`, `signInsertSomeProd_eq_prod_prod`, `stat_signFinset_insert_some_self_snd`, `insertAndContractNat_some_getDual?_neq_isSome`, `sign_insert_none`, `wickContraction_zero_some_eq_mul`, `consAddContract_bijection`, `fstFieldOfContract_getDual?_isSome`
`instDecidableEq` 📖	CompOp	5 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`
`sigmaContractedEquiv` 📖	CompOp	—
`sndFieldOfContract` 📖	CompOp	26 math math: `prod_finset_eq_mul_fst_snd`, `sign_right_eq_prod_mul_prod`, `join_singleton_sign_right`, `sndFieldOfContract_mem`, `sndFieldOfContract_getDual?`, `subContraction_sndFieldOfContract`, `insertAndContract_sndFieldOfContract`, `fstFieldOfContract_le_sndFieldOfContract`, `fstFieldOfContract_getDual?`, `signInsertSomeProd_eq_one_if`, `EqTimeOnly.eqTimeOnly_iff_forall_finset`, `singleton_sndFieldOfContract`, `insertAndContract_sndFieldOfContract_some_incl`, `joinSignRightExtra_eq_i_j_finset_eq_if`, `insertAndContractNat_sndFieldOfContract`, `sndFieldOfContract_congr`, `quotContraction_sndFieldOfContract_uncontractedListEmd`, `sndFieldOfContract_getDual?_isSome`, `finset_eq_fstFieldOfContract_sndFieldOfContract`, `haveEqTime_iff_finset`, `join_sndFieldOfContract_joinLift`, `fstFieldOfContract_lt_sndFieldOfContract`, `join_sndFieldOfContract_joinLiftRight`, `eq_sndFieldOfContract_of_mem`, `signInsertNone_eq_mul_fst_snd`, `subContraction_singleton_eq_singleton`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_congr` 📖	mathematical	—	`WickContraction` `congr`	—	—
`card_zero_iff_empty` 📖	mathematical	—	`empty`	—	`empty.eq_1`
`congrLiftInv_rfl` 📖	mathematical	—	`congrLiftInv` `WickContraction` `congr`	—	—
`congrLift_bijective` 📖	mathematical	—	`WickContraction` `congr` `congrLift`	—	`congrLift_injective` `congrLift_surjective`
`congrLift_injective` 📖	mathematical	—	`WickContraction` `congr` `congrLift`	—	`congrLift_rfl`
`congrLift_rfl` 📖	mathematical	—	`congrLift`	—	—
`congrLift_surjective` 📖	mathematical	—	`WickContraction` `congr` `congrLift`	—	`congrLift_rfl`
`congr_contractions` 📖	mathematical	—	`WickContraction` `congr`	—	—
`congr_refl` 📖	mathematical	—	`WickContraction` `congr`	—	—
`congr_trans` 📖	mathematical	—	`WickContraction` `congr`	—	—
`congr_trans_apply` 📖	mathematical	—	`WickContraction` `congr`	—	—
`eq_filter_mem_self` 📖	—	—	—	—	—
`eq_fstFieldOfContract_of_mem` 📖	mathematical	—	`fstFieldOfContract`	—	`finset_eq_fstFieldOfContract_sndFieldOfContract` `fstFieldOfContract_lt_sndFieldOfContract`
`eq_sndFieldOfContract_of_mem` 📖	mathematical	—	`sndFieldOfContract`	—	`finset_eq_fstFieldOfContract_sndFieldOfContract` `fstFieldOfContract_lt_sndFieldOfContract`
`exists_pair_of_not_eq_empty` 📖	—	—	—	—	—
`finset_eq_fstFieldOfContract_sndFieldOfContract` 📖	mathematical	—	`fstFieldOfContract` `sndFieldOfContract`	—	—
`fstFieldOfContract_congr` 📖	mathematical	—	`fstFieldOfContract` `WickContraction` `congr` `congrLift`	—	`congrLift_rfl`
`fstFieldOfContract_getDual?` 📖	mathematical	—	`getDual?` `fstFieldOfContract` `sndFieldOfContract`	—	—
`fstFieldOfContract_getDual?_isSome` 📖	mathematical	—	`getDual?` `fstFieldOfContract`	—	`getDual?_isSome_iff` `fstFieldOfContract_mem`
`fstFieldOfContract_le_sndFieldOfContract` 📖	mathematical	—	`fstFieldOfContract` `sndFieldOfContract`	—	—
`fstFieldOfContract_lt_sndFieldOfContract` 📖	mathematical	—	`fstFieldOfContract` `sndFieldOfContract`	—	`fstFieldOfContract_le_sndFieldOfContract` `fstFieldOfContract_neq_sndFieldOfContract`
`fstFieldOfContract_mem` 📖	mathematical	—	`fstFieldOfContract`	—	`finset_eq_fstFieldOfContract_sndFieldOfContract`
`fstFieldOfContract_neq_sndFieldOfContract` 📖	—	—	—	—	`finset_eq_fstFieldOfContract_sndFieldOfContract`
`getDual?_congr` 📖	mathematical	—	`getDual?` `WickContraction` `congr`	—	—
`getDual?_congr_get` 📖	mathematical	`getDual?` `WickContraction` `congr`	`getDual?_congr`	—	`getDual?_congr`
`getDual?_eq_some_iff_mem` 📖	mathematical	—	`getDual?`	—	—
`getDual?_eq_some_neq` 📖	—	`getDual?`	—	—	`getDual?_eq_some_iff_mem`
`getDual?_getDual?_get_get` 📖	—	`getDual?`	—	—	—
`getDual?_getDual?_get_isSome` 📖	—	`getDual?`	—	—	`getDual?_getDual?_get_get`
`getDual?_getDual?_get_not_none` 📖	—	`getDual?`	—	—	`getDual?_getDual?_get_get`
`getDual?_get_self_mem` 📖	—	`getDual?`	—	—	`getDual?_eq_some_iff_mem`
`getDual?_get_self_neq` 📖	—	`getDual?`	—	—	—
`getDual?_isSome_iff` 📖	mathematical	—	`getDual?`	—	`getDual?.eq_1`
`getDual?_isSome_of_mem` 📖	mathematical	—	`getDual?`	—	`getDual?_isSome_iff`
`getDual?_one_eq_none` 📖	mathematical	—	`getDual?`	—	`getDual?_eq_some_iff_mem`
`gradingCompliant_congr` 📖	mathematical	—	`GradingCompliant` `WickContraction` `FieldSpecification.FieldOp` `congr`	—	—
`mem_congr_iff` 📖	mathematical	—	`WickContraction` `congr`	—	—
`prod_finset_eq_mul_fst_snd` 📖	mathematical	—	`fstFieldOfContract` `fstFieldOfContract_mem` `sndFieldOfContract` `sndFieldOfContract_mem`	—	`fstFieldOfContract_mem` `sndFieldOfContract_mem`
`self_getDual?_get_mem` 📖	—	`getDual?`	—	—	`getDual?_eq_some_iff_mem`
`self_neq_getDual?_get` 📖	—	`getDual?`	—	—	—
`sndFieldOfContract_congr` 📖	mathematical	—	`sndFieldOfContract` `WickContraction` `congr` `congrLift`	—	`congrLift_rfl`
`sndFieldOfContract_getDual?` 📖	mathematical	—	`getDual?` `sndFieldOfContract` `fstFieldOfContract`	—	`getDual?_eq_some_iff_mem` `finset_eq_fstFieldOfContract_sndFieldOfContract`
`sndFieldOfContract_getDual?_isSome` 📖	mathematical	—	`getDual?` `sndFieldOfContract`	—	`getDual?_isSome_iff` `sndFieldOfContract_mem`
`sndFieldOfContract_mem` 📖	mathematical	—	`sndFieldOfContract`	—	`finset_eq_fstFieldOfContract_sndFieldOfContract`

(root)

Definitions

Name	Category	Theorems
`WickContraction` 📖	CompOp	53 math math: `WickContraction.uncontractedList_extractEquiv_symm_none`, `FieldSpecification.wicks_theorem_congr`, `WickContraction.getDual?_congr`, `WickContraction.congr_contractions`, `FieldSpecification.WickAlgebra.wicks_theorem_normal_order_empty`, `WickContraction.insertAndContractNat_getDualErase`, `WickContraction.EqTimeOnly.eqTimeOnly_congr`, `WickContraction.card_of_isfull_even`, `WickContraction.consAddContract_injective`, `WickContraction.gradingCompliant_congr`, `WickContraction.uncontractedList_extractEquiv_symm_some`, `WickContraction.congr_uncontractedList`, `WickContraction.wickContraction_zero_some_eq_sum`, `WickContraction.card_congr`, `WickContraction.join_assoc`, `FieldSpecification.WickAlgebra.wicks_theorem_normal_order`, `WickContraction.card_of_isfull_odd`, `WickContraction.insertAndContractNat_bijective`, `WickContraction.extractEquiv_symm_none_uncontracted`, `WickContraction.congr_trans`, `WickContraction.wickContraction_zero_none_card`, `WickContraction.sum_extractEquiv_congr`, `FieldSpecification.WickAlgebra.static_wick_theorem`, `WickContraction.uncontractedCongr_some`, `FieldSpecification.WickAlgebra.normalOrder_timeOrder_ofFieldOpList_eq_eqTimeOnly_empty`, `WickContraction.sndFieldOfContract_congr`, `WickContraction.insertAndContractNat_injective`, `WickContraction.congrLift_injective`, `WickContraction.wickContraction_card_eq_sum_zero_none_isSome`, `WickContraction.mem_congr_iff`, `WickContraction.congrLiftInv_rfl`, `WickContraction.congr_trans_apply`, `WickContraction.sign_congr`, `WickContraction.sum_haveEqTime`, `WickContraction.congr_uncontracted`, `WickContraction.extractEquiv_apply_congr_symm_apply`, `WickContraction.insertLift_sum`, `WickContraction.fstFieldOfContract_congr`, `FieldSpecification.WickAlgebra.normalOrder_timeOrder_ofFieldOpList_eq_not_haveEqTime_sub_inductive`, `WickContraction.join_congr`, `FieldSpecification.WickAlgebra.timeOrder_ofFieldOpList_eq_eqTimeOnly_empty`, `WickContraction.card_eq_cardFun`, `WickContraction.congrLift_bijective`, `WickContraction.congr_refl`, `WickContraction.wickContraction_zero_some_eq_mul`, `FieldSpecification.wicks_theorem`, `FieldSpecification.WickAlgebra.timeOrder_haveEqTime_split`, `WickContraction.sum_WickContraction_nil`, `WickContraction.consAddContract_bijection`, `WickContraction.empty_join`, `FieldSpecification.WickAlgebra.timeOrder_ofFieldOpList_eqTimeOnly`, `WickContraction.congrLift_surjective`, `WickContraction.uncontractedListEmd_congr`

---

← Back to Index