OAI/NumberTheory/OrdinaryCorrelations/HighTrace/CodeEntropyMass.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.RecordPacket.codeEntropyMass line 20
2. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.RecordPacket.codeEntropyBase line 21
3. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.RecordPacket.codeEntropyDegree line 24
4. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.RecordPacket.codeEntropyMass_nonneg line 26
5. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.RecordPacket.codeEntropyBase_ge_two line 29
6. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.RecordPacket.metadata_polynomial_bound line 39
7. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.RecordPacket.exceptional_polynomial_bound line 64
8. theorem OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.RecordPacket.packet_entropy_polynomial line 92