OAI/NumberTheory/OrdinaryCorrelations/HighTrace/FreePieceWeight.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.freePiece_weight line 17
2. theorem OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.recordTokens_weight line 25
3. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.taggedPieces_lit_cover line 46
4. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.taggedPieces_tagged line 59
5. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.taggedPieces_nonempty line 65
6. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.recordTokens_fixed_lit line 73
7. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.recordTokens_fixed_tag line 87
8. theorem OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.recordTokens_injective_on_records line 106