OAI/NumberTheory/OrdinaryCorrelations/HighTrace/CardTreeVerticesLe.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.card_treeVertices_le line 15
2. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.background_numerator_le line 18
3. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.backgroundExponent_lower line 36
4. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.backgroundExponent_nonpos line 42
5. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.UsedPrime line 50
6. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.OmittedPrime line 53
7. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.tokenPrimeFactor line 56
8. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.tokenPrimeFactor_nonneg line 62
9. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.primeBound_factorization line 71
10. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.restorationError line 78
11. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.restorationError_nonneg line 81
12. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.background_sum_restored line 86
13. theorem OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.all_prime_bounds_restored line 100
14. abbrev OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.CenterIndex line 111
15. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.harmonicCenter line 112
16. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.bandDefect line 114
17. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.sum_backgroundExponent line 117
18. theorem OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.assignedKernelIntegral_restored line 137