OAI/NumberTheory/OrdinaryCorrelations/HighTrace/GapFilling.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.GapFilling line 20
2. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.GapFilling.weight line 25
3. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.GapFilling.weight_nonneg line 27
4. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.GapFilling.decode line 29
5. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.GapFilling.sum_weight line 32
6. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.NumericalLine.GapCertificate.encode line 44
7. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.NumericalLine.GapCertificate.decode_encode line 49
8. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.NumericalLine.GapCertificate.weight_encode line 53
9. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.NumericalLine.packedGapMass line 60
10. theorem OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.NumericalLine.packedGapMass_le_templateMass line 63