OAI/NumberTheory/OrdinaryCorrelations/HighTrace/IndexedWitnessFilling.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.IndexedWitnessFilling line 20
2. instance OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.(instance at line 24) line 24
3. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.IndexedWitnessFilling.weight line 33
4. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.IndexedWitnessFilling.weight_nonneg line 35
5. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.IndexedWitnessFilling.decode line 41
6. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.IndexedWitnessFilling.sum_weight line 44
7. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.WitnessConfiguration.Certificate.encode line 58
8. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.WitnessConfiguration.Certificate.decode_encode line 62
9. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.WitnessConfiguration.Certificate.weight_encode line 67
10. theorem OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.configurationMass_le_templateMass line 74