OAI/NumberTheory/OrdinaryCorrelations/HighTrace/LitEdgesEmptyOfNo.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.litEdges_empty_of_no_tree line 16
2. theorem OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.charged_prime_le_background line 24
3. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.listLocal_has_residue line 54
4. theorem OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.list_no_tree_mean line 74
5. theorem OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.background_kernel_mean line 98