OAI/NumberTheory/OrdinaryCorrelations/HighTrace/LocalToken.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.LocalToken line 18
2. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.tokenEdges line 20
3. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.taggedPieces line 22
4. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.taggedPieces_cover line 27
5. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.localTokenWeight line 42
6. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.localTokenWeight_nonneg line 46
7. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.componentEdges_injOn line 54
8. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.taggedPieces_weight line 61
9. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.freePiece line 79
10. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.freePiece_edges line 83
11. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.freePiece_injective line 88
12. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.recordTokens line 95
13. theorem OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.recordTokens_cover line 104
14. theorem OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.recordTokens_recover_label line 133