OAI/NumberTheory/OrdinaryCorrelations/HighTrace/ExceptionalBudget.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.exceptionalBudget line 19
2. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.eventually_const_mul_rpow_le line 21
3. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.eventually_log_ceil_le line 29
4. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.ceil_rpow_le_two line 44
5. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.source_entropy_scales line 50
6. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.RecordPacket.codeEntropyMass_eq line 66
7. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.RecordPacket.source_mass_le_log line 70
8. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.RecordPacket.source_entropy_degree_bound line 80
9. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.RecordPacket.source_entropy_base_bound line 110
10. theorem OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.RecordPacket.source_entropy_sublinear line 137