OAI/NumberTheory/OrdinaryCorrelations/HighTrace/TreeOccurrencesEmptyOfFree.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.treeOccurrences_empty_of_free_core line 17
2. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.treeOccurrences_singleton_of_free line 23
3. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.freeTreeWeight line 34
4. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.freeTreeWeight_nonneg line 37
5. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.primeBound line 41
6. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.primeBound_nonneg line 47
7. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.no_tree_of_not_nonempty line 56
8. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.fixed_mean_le_primeBound line 62
9. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.free_core_mean_le_primeBound line 73
10. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.free_center_mean_le_primeBound line 84
11. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.product_index_split line 100
12. theorem OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.assignedKernelIntegral_le_all_prime_bounds line 108