Documentation Verification Report

InsertSome

📁 Source: PhysLean/QFT/PerturbationTheory/WickContraction/Sign/InsertSome.lean

Statistics

Metric	Count
Definitions `signInsertSome`, `signInsertSomeCoef`, `signInsertSomeProd`	3
Theorems `signFinset_insertAndContract_some`, `signInsertSomeCoef_eq_finset`, `signInsertSomeCoef_if`, `signInsertSomeProd_eq_finset`, `signInsertSomeProd_eq_one_if`, `signInsertSomeProd_eq_prod_fin`, `signInsertSomeProd_eq_prod_prod`, `signInsertSome_mul_filter_contracted_of_lt`, `signInsertSome_mul_filter_contracted_of_not_lt`, `sign_insert_some`, `sign_insert_some_of_lt`, `sign_insert_some_of_not_lt`, `sign_insert_some_zero`, `stat_ofFinset_eq_one_of_gradingCompliant`, `stat_signFinset_insert_some_self_fst`, `stat_signFinset_insert_some_self_snd`	16
Total	19

WickContraction

Definitions

Name	Category	Theorems
`signInsertSome` 📖	CompOp	3 math math: `signInsertSome_mul_filter_contracted_of_lt`, `signInsertSome_mul_filter_contracted_of_not_lt`, `sign_insert_some`
`signInsertSomeCoef` 📖	CompOp	2 math math: `signInsertSomeCoef_eq_finset`, `signInsertSomeCoef_if`
`signInsertSomeProd` 📖	CompOp	4 math math: `signInsertSomeProd_eq_prod_fin`, `signInsertSomeProd_eq_finset`, `signInsertSomeProd_eq_one_if`, `signInsertSomeProd_eq_prod_prod`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`signFinset_insertAndContract_some` 📖	mathematical	—	`signFinset` `FieldSpecification.FieldOp` `insertAndContract` `uncontracted` `PhysLean.List.insertIdx_length_fin` `insertAndContractLiftFinset`	—	`PhysLean.List.insertIdx_length_fin` `insert_fin_eq_self` `insertAndContract_some_getDual?_self_eq` `insertAndContract_some_getDual?_some_eq` `succAbove_mem_insertAndContractLiftFinset` `insertAndContract_some_succAbove_getDual?_eq_option`
`signInsertSomeCoef_eq_finset` 📖	mathematical	`FieldSpecification.fieldOpStatistic` `FieldSpecification.FieldOp` `uncontracted`	`signInsertSomeCoef` `FieldStatistic` `FieldStatistic.instCommGroup` `FieldStatistic.exchangeSign` `FieldStatistic.ofFinset` `getDual?`	—	`PhysLean.List.insertIdx_length_fin` `signInsertSomeCoef_if` `stat_signFinset_insert_some_self_snd` `stat_signFinset_insert_some_self_fst`
`signInsertSomeCoef_if` 📖	mathematical	`FieldSpecification.fieldOpStatistic` `FieldSpecification.FieldOp` `uncontracted`	`signInsertSomeCoef` `FieldStatistic` `FieldStatistic.instCommGroup` `FieldStatistic.exchangeSign` `FieldStatistic.ofFinset` `signFinset` `insertAndContract` `PhysLean.List.insertIdx_length_fin`	—	`PhysLean.List.insertIdx_length_fin` `insertAndContract_sndFieldOfContract_some_incl` `insertAndContract_fstFieldOfContract_some_incl` `PhysLean.List.insertIdx_getElem_fin`
`signInsertSomeProd_eq_finset` 📖	mathematical	`FieldSpecification.fieldOpStatistic` `FieldSpecification.FieldOp` `uncontracted` `GradingCompliant`	`signInsertSomeProd` `FieldStatistic` `FieldStatistic.instCommGroup` `FieldStatistic.exchangeSign` `FieldStatistic.ofFinset` `getDual?`	—	`signInsertSomeProd_eq_prod_fin` `FieldStatistic.ofFinset_eq_prod`
`signInsertSomeProd_eq_one_if` 📖	mathematical	`FieldSpecification.fieldOpStatistic` `FieldSpecification.FieldOp` `uncontracted`	`signInsertSomeProd` `fstFieldOfContract` `sndFieldOfContract` `FieldStatistic` `FieldStatistic.instCommGroup` `FieldStatistic.exchangeSign`	—	`signInsertSomeProd.eq_1`
`signInsertSomeProd_eq_prod_fin` 📖	mathematical	`FieldSpecification.fieldOpStatistic` `FieldSpecification.FieldOp` `uncontracted` `GradingCompliant`	`signInsertSomeProd` `getDual?` `FieldStatistic` `FieldStatistic.instCommGroup` `FieldStatistic.exchangeSign`	—	`getDual?_isSome_of_mem` `signInsertSomeProd_eq_prod_prod`
`signInsertSomeProd_eq_prod_prod` 📖	mathematical	`FieldSpecification.fieldOpStatistic` `FieldSpecification.FieldOp` `uncontracted` `GradingCompliant`	`signInsertSomeProd` `getDual?` `getDual?_isSome_of_mem` `FieldStatistic` `FieldStatistic.instCommGroup` `FieldStatistic.exchangeSign`	—	`getDual?_isSome_of_mem` `signInsertSomeProd_eq_one_if` `fstFieldOfContract_mem` `sndFieldOfContract_mem` `prod_finset_eq_mul_fst_snd` `sndFieldOfContract_getDual?` `fstFieldOfContract_lt_sndFieldOfContract` `fstFieldOfContract_getDual?`
`signInsertSome_mul_filter_contracted_of_lt` 📖	mathematical	`FieldSpecification.FieldOp` `uncontracted` `GradingCompliant` `FieldSpecification.fieldOpStatistic`	`signInsertSome` `FieldStatistic` `FieldStatistic.instCommGroup` `FieldStatistic.exchangeSign` `FieldStatistic.ofFinset`	—	`signInsertSome.eq_1` `signInsertSomeProd_eq_finset` `signInsertSomeCoef_eq_finset` `FieldStatistic.mul_eq_iff_eq_mul` `FieldStatistic.ofFinset_union_disjoint` `FieldStatistic.ofFinset_union` `FieldStatistic.mul_eq_one_iff` `stat_ofFinset_eq_one_of_gradingCompliant` `getDual?_getDual?_get_get`
`signInsertSome_mul_filter_contracted_of_not_lt` 📖	mathematical	`FieldSpecification.FieldOp` `uncontracted` `GradingCompliant` `FieldSpecification.fieldOpStatistic`	`signInsertSome` `FieldStatistic` `FieldStatistic.instCommGroup` `FieldStatistic.exchangeSign` `FieldStatistic.ofFinset`	—	`signInsertSome.eq_1` `signInsertSomeProd_eq_finset` `signInsertSomeCoef_eq_finset` `FieldStatistic.mul_eq_iff_eq_mul` `FieldStatistic.ofFinset_union` `FieldStatistic.mul_eq_one_iff` `stat_ofFinset_eq_one_of_gradingCompliant` `getDual?_getDual?_get_get`
`sign_insert_some` 📖	mathematical	—	`sign` `FieldSpecification.FieldOp` `insertAndContract` `uncontracted` `signInsertSome`	—	`sign.eq_1` `signInsertSome.eq_1` `signInsertSomeProd.eq_1` `PhysLean.List.insertIdx_length_fin` `insertAndContract_some_prod_contractions` `insertAndContract_sndFieldOfContract` `PhysLean.List.insertIdx_getElem_fin` `insertAndContract_fstFieldOfContract` `signFinset_insertAndContract_some` `stat_ofFinset_of_insertAndContractLiftFinset` `FieldStatistic.ofFinset_erase` `succAbove_mem_insertAndContractLiftFinset` `FieldStatistic.exchangeSign_symm` `FieldStatistic.ofFinset_insert`
`sign_insert_some_of_lt` 📖	mathematical	`FieldSpecification.FieldOp` `uncontracted` `GradingCompliant` `FieldSpecification.fieldOpStatistic`	`sign` `insertAndContract` `FieldStatistic` `FieldStatistic.instCommGroup` `FieldStatistic.exchangeSign` `FieldStatistic.ofFinset`	—	`sign_insert_some` `signInsertSome_mul_filter_contracted_of_lt` `FieldStatistic.exchangeSign_mul_self`
`sign_insert_some_of_not_lt` 📖	mathematical	`FieldSpecification.FieldOp` `uncontracted` `GradingCompliant` `FieldSpecification.fieldOpStatistic`	`sign` `insertAndContract` `FieldStatistic` `FieldStatistic.instCommGroup` `FieldStatistic.exchangeSign` `FieldStatistic.ofFinset`	—	`sign_insert_some` `signInsertSome_mul_filter_contracted_of_not_lt` `FieldStatistic.exchangeSign_mul_self`
`sign_insert_some_zero` 📖	mathematical	`GradingCompliant` `FieldSpecification.fieldOpStatistic` `FieldSpecification.FieldOp` `uncontracted`	`sign` `insertAndContract` `FieldStatistic` `FieldStatistic.instCommGroup` `FieldStatistic.exchangeSign` `FieldStatistic.ofFinset`	—	`sign_insert_some_of_not_lt` `FieldStatistic.ofFinset_empty`
`stat_ofFinset_eq_one_of_gradingCompliant` 📖	mathematical	`GradingCompliant` `FieldSpecification.FieldOp` `getDual?`	`FieldStatistic.ofFinset` `FieldSpecification.fieldOpStatistic` `FieldStatistic` `FieldStatistic.instCommGroup`	—	`FieldStatistic.ofFinset_eq_prod` `fstFieldOfContract_mem` `sndFieldOfContract_mem` `prod_finset_eq_mul_fst_snd` `fstFieldOfContract_getDual?` `sndFieldOfContract_getDual?` `FieldStatistic.mul_self`
`stat_signFinset_insert_some_self_fst` 📖	mathematical	—	`FieldStatistic.ofFinset` `FieldSpecification.FieldOp` `FieldSpecification.fieldOpStatistic` `signFinset` `insertAndContract` `uncontracted` `PhysLean.List.insertIdx_length_fin` `getDual?`	—	`PhysLean.List.insertIdx_length_fin` `PhysLean.List.get_eq_insertIdx_succAbove` `FieldStatistic.ofFinset_finset_map` `insert_fin_eq_self` `insertAndContract_some_getDual?_self_eq` `insertAndContract_some_getDual?_some_eq` `insertAndContract_some_succAbove_getDual?_eq_option`
`stat_signFinset_insert_some_self_snd` 📖	mathematical	—	`FieldStatistic.ofFinset` `FieldSpecification.FieldOp` `FieldSpecification.fieldOpStatistic` `signFinset` `insertAndContract` `uncontracted` `PhysLean.List.insertIdx_length_fin` `getDual?`	—	`PhysLean.List.insertIdx_length_fin` `PhysLean.List.get_eq_insertIdx_succAbove` `FieldStatistic.ofFinset_finset_map` `insert_fin_eq_self` `insertAndContract_some_getDual?_self_eq` `insertAndContract_some_getDual?_some_eq` `insertAndContract_some_succAbove_getDual?_eq_option`

---

← Back to Index