OAI/NumberTheory/OrdinaryCorrelations/HighTrace/SpecificationSlotCount.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.specificationSlotCount line 18
2. abbrev OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.GoodSpecificationTemplate line 19
3. abbrev OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.SpecificationFilling line 21
4. instance OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.(instance at line 24) line 24
5. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.SpecificationFilling.weight line 30
6. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.SpecificationFilling.weight_nonneg line 32
7. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.SpecificationFilling.decode line 34
8. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Specification.primeWeight line 42
9. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Specification.filling line 43
10. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Specification.decode_filling line 46
11. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Specification.weight_filling line 48
12. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.specificationMajorant line 57
13. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.specificationMajorant_le_filling line 60
14. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.specificationBudget line 77
15. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.specificationFilling_sum_le line 81