OAI/NumberTheory/OrdinaryCorrelations/HighTrace/GrowsSingleton.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.OrdinaryCorrelations.NumericalSubtrees.grows_singleton line 17
2. lemma OAI.OrdinaryCorrelations.NumericalSubtrees.singleton_mem_shapes line 34
3. theorem OAI.OrdinaryCorrelations.NumericalSubtrees.sum_singleton_corrections line 39
4. lemma OAI.OrdinaryCorrelations.NumericalSubtrees.good_singleton_raw line 56
5. lemma OAI.OrdinaryCorrelations.NumericalSubtrees.modified_raw_correction line 65
6. def OAI.OrdinaryCorrelations.NumericalSubtrees.goodEdges line 99
7. def OAI.OrdinaryCorrelations.NumericalSubtrees.badEdges line 101
8. lemma OAI.OrdinaryCorrelations.NumericalSubtrees.correction_sum line 103
9. theorem OAI.OrdinaryCorrelations.NumericalSubtrees.modified_center_subtree_sum line 110