OAI/NumberTheory/OrdinaryCorrelations/HighTrace/DisconnectedCertificate.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.NumericalLine.DisconnectedCertificate line 23
2. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.NumericalLine.disconnectedCertificate_exists line 34
3. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.NumericalLine.DisconnectedCertificate.encode line 61
4. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.NumericalLine.DisconnectedCertificate.decode_encode line 66
5. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.NumericalLine.DisconnectedCertificate.weight_encode line 69
6. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.NumericalLine.disconnectedCertificateMass line 77
7. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.NumericalLine.disconnectedCertificateMass_le_templateMass line 80
8. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.NumericalLine.disconnectedCertificateSum line 98
9. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.NumericalLine.disconnectedCertificateSum_le_mass line 103
10. theorem OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.NumericalLine.disconnectedCertificateSum_bound line 118