OAI/NumberTheory/OrdinaryCorrelations/HighTrace/ModifiedWeightSameBand.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.modifiedWeight_same_band line 18
2. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.tokenWeight_same_band line 25
3. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.taggedTokens line 36
4. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.taggedTokens_of_none line 40
5. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.taggedTokens_of_some line 52
6. theorem OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.record_tokens_recovery line 59
7. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.recordTreeWeight_split line 74
8. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.untagged_implies_used line 89
9. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.taggedGroupFactor line 98
10. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.weighted_record_prime_split line 105
11. theorem OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.record_weight_factorization line 121